From af4a529dc480787bb97cf45a72ce3fa6391ad502 Mon Sep 17 00:00:00 2001
From: Valentyn Sobol <napster_1997@mail.ru>
Date: Tue, 23 Apr 2024 00:14:28 +0300
Subject: [PATCH] Fix Z3 assert and track (#159)

---
 .../ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt | 2 ++
 1 file changed, 2 insertions(+)

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
index 1bcc7ea53..76933ce3f 100644
--- 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 {