replaced LoopUnrollPass solver initialization (no solver home registr…

…ation required)
ftsrg · Sep 10, 2023 · 9b4a0ef · 9b4a0ef
1 parent d1f33e6
commit 9b4a0ef
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 2 deletions.
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
@@ -168,7 +168,6 @@ class XcfaCli(private val args: Array<String>) {
         val gsonForOutput = getGson()
         val logger = ConsoleLogger(logLevel)
         val explicitProperty: ErrorDetection = getExplicitProperty()
-        registerAllSolverManagers(solverHome, logger)
 
         // propagating input variables
         LbePass.level = lbeLevel
@@ -192,6 +191,7 @@ class XcfaCli(private val args: Array<String>) {
         // verification
         stopwatch.reset().start()
         logger.write(Logger.Level.INFO, "Starting verification of ${xcfa.name} using $backend")
+        registerAllSolverManagers(solverHome, logger)
         val config = parseConfigFromCli()
         if (strategy != Strategy.PORTFOLIO && printConfigFile != null) {
             printConfigFile!!.writeText(gsonForOutput.toJson(config))

diff --git a/subprojects/xcfa/xcfa/build.gradle.kts b/subprojects/xcfa/xcfa/build.gradle.kts
@@ -24,4 +24,5 @@ dependencies {
     implementation(project(":theta-c-frontend"))
     implementation(project(":theta-analysis"))
     implementation(project(":theta-solver"))
+    implementation(project(mapOf("path" to ":theta-solver-z3")))
 }
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LoopUnrollPass.kt
@@ -43,7 +43,7 @@ class LoopUnrollPass : ProcedurePass {
 
         var UNROLL_LIMIT = 50
 
-        private val solver: Solver = SolverManager.resolveSolverFactory("Z3").createSolver()
+        private val solver: Solver = Z3SolverFactory.getInstance().createSolver()
     }
 
     private val testedLoops = mutableSetOf<Loop>()