Updated XCFA Bounded Config for new BoundedChecker interface

ftsrg · Jan 27, 2025 · 9a8aca4 · 9a8aca4
1 parent 2bc3921
commit 9a8aca4
Show file tree

Hide file tree

Showing 2 changed files with 4 additions 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
@@ -253,6 +253,7 @@ constructor(
 			imcFpSolver.add(Not(img))
 			if (imcFpSolver.check().isUnsat) {
 				logger.write(Logger.Level.MAINSTEP, "Safety proven in IMC step\n")
+				imcFpSolver.popAll()
 				itpSolver.popAll()
 				return SafetyResult.safe(EmptyProof.getInstance(), BoundedStatistics(iteration))
 			}

diff --git a/.../xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt b/.../xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToBoundedChecker.kt
@@ -61,6 +61,9 @@ fun getBoundedChecker(
       itpSolver =
         tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver)
           ?.createItpSolver(),
+			imcFpSolver =
+        tryGetSolver(boundedConfig.itpConfig.itpSolver, boundedConfig.itpConfig.validateItpSolver)
+          ?.createSolver(),  
       imcEnabled = { !boundedConfig.itpConfig.disable },
       indSolver =
         tryGetSolver(boundedConfig.indConfig.indSolver, boundedConfig.indConfig.validateIndSolver)