fix: more accurate nbAddKt function

UnitTestBot · Aug 13, 2024 · 3c58a20 · 3c58a20
1 parent d4ab7a6
commit 3c58a20
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/...ain/kotlin/org/usvm/machine/interpreters/symbolic/operations/basic/MethodNotifications.kt b/...ain/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)
 }