Fixed order of solver add()

ftsrg · Feb 7, 2024 · b87b5f5 · b87b5f5
1 parent af0fe24
commit b87b5f5
Showing 1 changed file with 29 additions and 1 deletion.
diff --git a/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/...mmon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
@@ -95,7 +95,6 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
         bmcSolver.push()
         bmcSolver.add(unfoldedInitExpr)
         bmcSolver.add(exprs)
-        bmcSolver.add(Not(unfoldedPropExpr(indices.last())))
 
         if (lfPathOnly()) { // indices contains currIndex as last()
             for (indexing in indices) {
@@ -106,8 +105,16 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
                     bmcSolver.add(Not(allVarsSame))
                 }
             }
+
+            if (bmcSolver.check().isUnsat) {
+                bmcSolver.pop()
+                logger.write(Logger.Level.MAINSTEP, "Safety proven in BMC step\n")
+                return SafetyResult.safe<S, A>()
+            }
         }
 
+        bmcSolver.add(Not(unfoldedPropExpr(indices.last())))
+
         val ret = if (bmcSolver.check().isSat) {
             val trace = getTrace(bmcSolver.model)
             logger.write(Logger.Level.MAINSTEP, "CeX found in BMC step (length ${trace.length()})\n")
@@ -151,6 +158,27 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
         itpSolver.add(a, unfoldedInitExpr)
         itpSolver.add(a, exprs[0])
         itpSolver.add(b, exprs.subList(1, exprs.size))
+
+        if (lfPathOnly()) { // indices contains currIndex as last()
+            itpSolver.push()
+            for (indexing in indices) {
+                if (indexing != indices.last()) {
+                    val allVarsSame = And(vars.map {
+                        Eq(PathUtils.unfold(it.ref, indexing), PathUtils.unfold(it.ref, indices.last()))
+                    })
+                    itpSolver.add(a, Not(allVarsSame))
+                }
+            }
+
+            if (itpSolver.check().isUnsat) {
+                itpSolver.pop()
+                itpSolver.pop()
+                logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC/BMC step\n")
+                return SafetyResult.safe()
+            }
+            itpSolver.pop()
+        }
+
         itpSolver.add(b, Not(unfoldedPropExpr(indices.last())))
 
         val status = itpSolver.check()