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
index e0c908663e..7d73f4ace1 100644
--- 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
index cad8a876f0..1094a17c91 100644
--- 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
index c3d421bc79..2d461f42b0 100644
--- 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>()