From db73cbb28046d112e419f4d10a9c26f740b6a688 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 15 Feb 2024 18:12:57 +0100
Subject: [PATCH] Fixing iter lookup and missing state

---
 .../theta/analysis/algorithm/bounded/BoundedChecker.kt   | 9 ++++-----
 .../main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt | 2 +-
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
index 528df05d9d..20a478c067 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt
+++ b/subprojects/common/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
index d02b6ac0f3..e7725c1df2 100644
--- 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>()