Fixing iter lookup and missing state

ftsrg · Feb 15, 2024 · db73cbb · db73cbb
1 parent 017cad8
commit db73cbb
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
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
@@ -77,7 +77,7 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
     private val unfoldedPropExpr = { i: VarIndexing -> PathUtils.unfold(monolithicExpr.propExpr, i) }
     private val indices = mutableListOf(VarIndexingFactory.indexing(0))
     private val exprs = mutableListOf<Expr<BoolType>>()
-    private var lastIterLookup = Pair(0, 0)
+    private var kindLastIterLookup = 0
 
     init {
         check(bmcSolver != itpSolver || bmcSolver == null) { "Use distinct solvers for BMC and IMC!" }
@@ -108,12 +108,11 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
                     error("Bad configuration: induction check should always be preceded by a BMC/SAT check")
                 }
                 kind()?.let { return it }
-                lastIterLookup = lastIterLookup.copy(first = iteration)
+                kindLastIterLookup = iteration
             }
 
             if (imcEnabled(iteration)) {
                 itp()?.let { return it }
-                lastIterLookup = lastIterLookup.copy(second = iteration)
             }
         }
         return SafetyResult.unknown()
@@ -157,8 +156,8 @@ class BoundedChecker<S : ExprState, A : StmtAction> @JvmOverloads constructor(
 
         logger.write(Logger.Level.MAINSTEP, "\tStarting k-induction\n")
 
-        exprs.subList(lastIterLookup.first, exprs.size).forEach { indSolver.add(it) }
-        indices.subList(lastIterLookup.first, indices.size - 1).forEach { indSolver.add(unfoldedPropExpr(it)) }
+        exprs.subList(kindLastIterLookup, exprs.size).forEach { indSolver.add(it) }
+        indices.subList(kindLastIterLookup, indices.size - 1).forEach { indSolver.add(unfoldedPropExpr(it)) }
 
         return WithPushPop(indSolver).use {
             indSolver.add(Not(unfoldedPropExpr(indices.last())))

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -156,7 +156,7 @@ private fun backend(xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: Xc
     logger: Logger,
     uniqueLogger: Logger): SafetyResult<*, *> =
     if (config.backendConfig.backend == Backend.NONE) {
-        SafetyResult.unknown()
+        SafetyResult.unknown<State, Action>()
     } else {
         if (xcfa.procedures.all { it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION }) {
             SafetyResult.safe<State, Action>()