Fix Z3 assert and track (#159)

UnitTestBot · Apr 22, 2024 · af4a529 · af4a529
1 parent 81ec9b5
commit af4a529
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt
@@ -95,6 +95,8 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
         trackedAssertions.put(z3TrackVar, expr)
 
         solver.solverAssertAndTrack(z3Expr, z3TrackVar)
+
+        z3Ctx.assertPendingAxioms(solver)
     }
 
     override fun check(timeout: Duration): KSolverStatus = z3TryCheck {