Fixed k-ind

ftsrg · Feb 13, 2024 · 25d10d5 · 25d10d5
1 parent ee3088a
commit 25d10d5
Showing 1 changed file with 1 addition and 0 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
@@ -145,6 +145,7 @@ 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)) }
 
         return indSolver.pushPop {
             indSolver.add(Not(unfoldedPropExpr(indices.last())))