From 3c58a20a6dc3620f39bebf4abac95b1e5da7f2d4 Mon Sep 17 00:00:00 2001 From: nostromo Date: Tue, 13 Aug 2024 10:11:05 +0300 Subject: [PATCH] fix: more accurate nbAddKt function --- .../symbolic/operations/basic/MethodNotifications.kt | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt index 3da567f94..b26ee3aa6 100644 --- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt +++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt @@ -38,9 +38,14 @@ fun nbAddKt( context.ctx ) { context.curState ?: return + /* + The __add__ method corresponds both to the nb_add and sq_concat slots, + so it is crucial not to assert the presence of nb_add, but to fork on these + two possible options. + */ val nbAdd = left.evalIsSoft(context, HasNbAdd) or right.evalIsSoft(context, HasNbAdd) val sqConcat = left.evalIsSoft(context, HasSqConcat) and right.evalIsSoft(context, HasSqConcat) - pyAssert(context, context.ctx.mkImplies(nbAdd.not(), sqConcat)) + pyAssert(context, nbAdd.not() implies sqConcat) pyFork(context, nbAdd) }