diff --git a/README.md b/README.md
index c245d52f8..f61001d5f 100644
--- a/README.md
+++ b/README.md
@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
 ```
 
 ## Usage
diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
index ef65d7a5f..a27e674aa 100644
--- a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
+++ b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
@@ -9,7 +9,7 @@ plugins {
 }
 
 group = "org.ksmt"
-version = "0.5.0"
+version = "0.5.1"
 
 repositories {
     mavenCentral()
diff --git a/docs/custom-expressions.md b/docs/custom-expressions.md
index 67ab8a745..e38242978 100644
--- a/docs/custom-expressions.md
+++ b/docs/custom-expressions.md
@@ -216,8 +216,8 @@ class CustomSolver<C : KSolverConfiguration>(
         solver.assert(transformer.apply(expr))
 
     // expr can contain custom expressions -> rewrite
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        solver.assertAndTrack(transformer.apply(expr), trackVar)
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) =
+        solver.assertAndTrack(transformer.apply(expr))
 
     // assumptions can contain custom expressions -> rewrite
     override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus =
@@ -262,10 +262,10 @@ class CustomModel(
     override val uninterpretedSorts: Set<KUninterpretedSort>
         get() = model.uninterpretedSorts
 
-    override fun <T : KSort> interpretation(decl: KDecl<T>): KModel.KFuncInterp<T>? =
+    override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =
         model.interpretation(decl)
 
-    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KExpr<KUninterpretedSort>>? =
+    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
         model.uninterpretedSortUniverse(sort)
 
     override fun detach(): KModel = CustomModel(model.detach(), transformer)
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 55a66e543..ddbf983a7 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -18,7 +18,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")    
 }
 ```
 
@@ -26,9 +26,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.5.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.5.1")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 
@@ -315,9 +315,9 @@ with(ctx) {
 
         /**
          * Assert and track e2
-         * Track variable e2Track will appear in unsat core
+         * e2 will appear in unsat core
          * */
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
 
         /**
          * Check satisfiability with e3 assumed.
@@ -328,18 +328,15 @@ with(ctx) {
 
         // retrieve unsat core
         val core = solver.unsatCore()
-        println("unsat core = $core") // [track!fresh!0, (not c)]
+        println("unsat core = $core") // [(not (and b a)), (not c)]
 
         // simply asserted expression cannot be in unsat core
         println("e1 in core = ${e1 in core}") // false
-        /**
-         * An expression added with assertAndTrack cannot be in unsat core.
-         * The corresponding track variable is used instead of the expression itself.
-         */
-        println("e2 in core = ${e2 in core}") // false
-        println("e2Track in core = ${e2Track in core}") // true
 
-        //the assumed expression appears in unsat core as is
+        // an expression added with assertAndTrack appears in unsat core as is.
+        println("e2 in core = ${e2 in core}") // true
+
+        // the assumed expression appears in unsat core as is
         println("e3 in core = ${e3 in core}") // true
     }
 }
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index b82ed11eb..7046946d5 100644
--- a/examples/build.gradle.kts
+++ b/examples/build.gradle.kts
@@ -10,9 +10,9 @@ repositories {
 
 dependencies {
     // core
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
 }
 
 java {
diff --git a/examples/src/main/kotlin/CustomExpressions.kt b/examples/src/main/kotlin/CustomExpressions.kt
index 1bac4f248..e228d828a 100644
--- a/examples/src/main/kotlin/CustomExpressions.kt
+++ b/examples/src/main/kotlin/CustomExpressions.kt
@@ -1,7 +1,6 @@
 import org.ksmt.KContext
 import org.ksmt.cache.hash
 import org.ksmt.cache.structurallyEqual
-import org.ksmt.decl.KConstDecl
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KUninterpretedSortValue
@@ -13,6 +12,7 @@ import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
 import org.ksmt.solver.KSolverConfiguration
 import org.ksmt.solver.KSolverStatus
+import org.ksmt.solver.model.KFuncInterp
 import org.ksmt.sort.KBoolSort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KSort
@@ -174,8 +174,8 @@ class CustomSolver<C : KSolverConfiguration>(
         solver.assert(transformer.apply(expr))
 
     // expr can contain custom expressions -> rewrite
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        solver.assertAndTrack(transformer.apply(expr), trackVar)
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) =
+        solver.assertAndTrack(transformer.apply(expr))
 
     // assumptions can contain custom expressions -> rewrite
     override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus =
@@ -219,7 +219,7 @@ class CustomModel(
     override val uninterpretedSorts: Set<KUninterpretedSort>
         get() = model.uninterpretedSorts
 
-    override fun <T : KSort> interpretation(decl: KDecl<T>): KModel.KFuncInterp<T>? =
+    override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =
         model.interpretation(decl)
 
     override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
diff --git a/examples/src/main/kotlin/GettingStartedExample.kt b/examples/src/main/kotlin/GettingStartedExample.kt
index 32e617973..f33d8d501 100644
--- a/examples/src/main/kotlin/GettingStartedExample.kt
+++ b/examples/src/main/kotlin/GettingStartedExample.kt
@@ -231,9 +231,9 @@ private fun unsatCoreGenerationExample(ctx: KContext) =
 
             /**
              * Assert and track e2
-             * Track variable e2Track will appear in unsat core
+             * e2 will appear in unsat core
              * */
-            val e2Track = solver.assertAndTrack(e2)
+            solver.assertAndTrack(e2)
 
             /**
              * Check satisfiability with e3 assumed.
@@ -244,18 +244,15 @@ private fun unsatCoreGenerationExample(ctx: KContext) =
 
             // retrieve unsat core
             val core = solver.unsatCore()
-            println("unsat core = $core") // [track!fresh!0, (not c)]
+            println("unsat core = $core") // [(not (and b a)), (not c)]
 
             // simply asserted expression cannot be in unsat core
             println("e1 in core = ${e1 in core}") // false
-            /**
-             * An expression added with assertAndTrack cannot be in unsat core.
-             * The corresponding track variable is used instead of the expression itself.
-             */
-            println("e2 in core = ${e2 in core}") // false
-            println("e2Track in core = ${e2Track in core}") // true
 
-            //the assumed expression appears in unsat core as is
+            // an expression added with assertAndTrack appears in unsat core as is.
+            println("e2 in core = ${e2 in core}") // true
+
+            // the assumed expression appears in unsat core as is
             println("e3 in core = ${e3 in core}") // true
         }
     }
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
index abd7ef2a0..084c8cc67 100644
--- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
+++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
@@ -1,14 +1,16 @@
 package org.ksmt.solver.bitwuzla
 
+import it.unimi.dsi.fastutil.longs.LongOpenHashSet
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
 import org.ksmt.solver.KSolverStatus
+import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaResult
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
+import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTermArray
 import org.ksmt.solver.bitwuzla.bindings.Native
 import org.ksmt.sort.KBoolSort
 import kotlin.time.Duration
@@ -21,15 +23,19 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
     open val exprConverter: KBitwuzlaExprConverter by lazy {
         KBitwuzlaExprConverter(ctx, bitwuzlaCtx)
     }
+
     private var lastCheckStatus = KSolverStatus.UNKNOWN
+    private var lastReasonOfUnknown: String? = null
+    private var lastAssumptions: TrackedAssumptions? = null
+    private var lastModel: KBitwuzlaModel? = null
 
     init {
         Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_INCREMENTAL, value = 1)
         Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_PRODUCE_MODELS, value = 1)
     }
 
-    private var trackVars = mutableListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
-    private val trackVarsAssertionFrames = arrayListOf(trackVars)
+    private var trackedAssertions = mutableListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
+    private val trackVarsAssertionFrames = arrayListOf(trackedAssertions)
 
     override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) {
         KBitwuzlaSolverConfigurationImpl(bitwuzlaCtx.bitwuzla).configurator()
@@ -46,23 +52,23 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
         Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, assertionWithAxioms.assertion)
     }
 
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry {
-        ctx.ensureContextMatch(expr, trackVar)
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry {
+        ctx.ensureContextMatch(expr)
 
-        val trackVarExpr = ctx.mkConstApp(trackVar)
+        val trackVarExpr = ctx.mkFreshConst("track", ctx.boolSort)
         val trackedExpr = with(ctx) { !trackVarExpr or expr }
 
         assert(trackedExpr)
 
         val trackVarTerm = with(exprInternalizer) { trackVarExpr.internalize() }
-        trackVars += trackVarExpr to trackVarTerm
+        trackedAssertions += expr to trackVarTerm
     }
 
     override fun push(): Unit = bitwuzlaCtx.bitwuzlaTry {
         Native.bitwuzlaPush(bitwuzlaCtx.bitwuzla, nlevels = 1)
 
-        trackVars = trackVars.toMutableList()
-        trackVarsAssertionFrames.add(trackVars)
+        trackedAssertions = trackedAssertions.toMutableList()
+        trackVarsAssertionFrames.add(trackedAssertions)
 
         bitwuzlaCtx.createNestedDeclarationScope()
     }
@@ -80,7 +86,7 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
             bitwuzlaCtx.popDeclarationScope()
         }
 
-        trackVars = trackVarsAssertionFrames.last()
+        trackedAssertions = trackVarsAssertionFrames.last()
 
         Native.bitwuzlaPop(bitwuzlaCtx.bitwuzla, n.toInt())
     }
@@ -88,27 +94,20 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
     override fun check(timeout: Duration): KSolverStatus =
         checkWithAssumptions(emptyList(), timeout)
 
-    private val lastAssumptions = arrayListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
-
-    private fun assumeExpr(expr: KExpr<KBoolSort>, term: BitwuzlaTerm) {
-        lastAssumptions += expr to term
-        Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, term)
-    }
-
     override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus =
-        bitwuzlaCtx.bitwuzlaTry {
+        bitwuzlaTryCheck {
             ctx.ensureContextMatch(assumptions)
 
-            invalidatePreviousModel()
-            lastAssumptions.clear()
+            val currentAssumptions = TrackedAssumptions().also { lastAssumptions = it }
 
-            trackVars.forEach {
-                assumeExpr(it.first, it.second)
+            trackedAssertions.forEach {
+                currentAssumptions.assumeTrackedAssertion(it)
             }
 
-            assumptions.forEach {
-                val assumptionTerm = with(exprInternalizer) { it.internalize() }
-                assumeExpr(it, assumptionTerm)
+            with(exprInternalizer) {
+                assumptions.forEach {
+                    currentAssumptions.assumeAssumption(it, it.internalize())
+                }
             }
 
             checkWithTimeout(timeout).processCheckResult()
@@ -120,16 +119,6 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
         Native.bitwuzlaCheckSatTimeoutResult(bitwuzlaCtx.bitwuzla, timeout.inWholeMilliseconds)
     }
 
-    private var lastModel: KBitwuzlaModel? = null
-
-    /**
-     * Bitwuzla model is only valid until the next check-sat call.
-     * */
-    private fun invalidatePreviousModel() {
-        lastModel?.markInvalid()
-        lastModel = null
-    }
-
     override fun model(): KModel = bitwuzlaCtx.bitwuzlaTry {
         require(lastCheckStatus == KSolverStatus.SAT) { "Model are only available after SAT checks" }
         val model = lastModel ?: KBitwuzlaModel(
@@ -143,9 +132,8 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
 
     override fun unsatCore(): List<KExpr<KBoolSort>> = bitwuzlaCtx.bitwuzlaTry {
         require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" }
-        val unsatCore = Native.bitwuzlaGetUnsatAssumptions(bitwuzlaCtx.bitwuzla).toSet()
-
-        return lastAssumptions.filter { it.second in unsatCore }.map { it.first }
+        val unsatAssumptions = Native.bitwuzlaGetUnsatAssumptions(bitwuzlaCtx.bitwuzla)
+        lastAssumptions?.resolveUnsatCore(unsatAssumptions) ?: emptyList()
     }
 
     override fun reasonOfUnknown(): String = bitwuzlaCtx.bitwuzlaTry {
@@ -154,7 +142,7 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
         }
 
         // There is no way to retrieve reason of unknown from Bitwuzla in general case.
-        return "unknown"
+        return lastReasonOfUnknown ?: "unknown"
     }
 
     override fun interrupt() = bitwuzlaCtx.bitwuzlaTry {
@@ -170,4 +158,42 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
         BitwuzlaResult.BITWUZLA_UNSAT -> KSolverStatus.UNSAT
         BitwuzlaResult.BITWUZLA_UNKNOWN -> KSolverStatus.UNKNOWN
     }.also { lastCheckStatus = it }
+
+    private fun invalidateSolverState() {
+        /**
+         * Bitwuzla model is only valid until the next check-sat call.
+         * */
+        lastModel?.markInvalid()
+        lastModel = null
+
+        lastCheckStatus = KSolverStatus.UNKNOWN
+        lastReasonOfUnknown = null
+
+        lastAssumptions = null
+    }
+
+    private inline fun bitwuzlaTryCheck(body: () -> KSolverStatus): KSolverStatus = try {
+        invalidateSolverState()
+        body()
+    } catch (ex: BitwuzlaNativeException) {
+        lastReasonOfUnknown = ex.message
+        KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
+    }
+
+    private inner class TrackedAssumptions {
+        private val assumedExprs = arrayListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
+
+        fun assumeTrackedAssertion(trackedAssertion: Pair<KExpr<KBoolSort>, BitwuzlaTerm>) {
+            assumedExprs.add(trackedAssertion)
+            Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, trackedAssertion.second)
+        }
+
+        fun assumeAssumption(expr: KExpr<KBoolSort>, term: BitwuzlaTerm) =
+            assumeTrackedAssertion(expr to term)
+
+        fun resolveUnsatCore(unsatAssumptions: BitwuzlaTermArray): List<KExpr<KBoolSort>> {
+            val unsatCoreTerms = LongOpenHashSet(unsatAssumptions)
+            return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } }
+        }
+    }
 }
diff --git a/ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt b/ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt
index 8ba4ea5dc..aee9e4588 100644
--- a/ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt
+++ b/ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt
@@ -39,12 +39,12 @@ class SolverTest {
         val e3 = !c
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.checkWithAssumptions(listOf(e3))
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(2, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
         assertTrue(e3 in core)
     }
 
@@ -57,12 +57,12 @@ class SolverTest {
         val e2 = !(a and b)
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
     }
 
     @Test
@@ -76,17 +76,17 @@ class SolverTest {
 
         solver.push()
 
-        val track1 = solver.assertAndTrack(!a)
+        solver.assertAndTrack(!a)
 
         solver.push()
 
-        val track2 = solver.assertAndTrack(!b)
+        solver.assertAndTrack(!b)
 
         var status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         var core = solver.unsatCore()
         assertEquals(2, core.size)
-        assertTrue(track1 in core && track2 in core)
+        assertTrue(!a in core && !b in core)
 
         solver.pop()
 
@@ -96,7 +96,7 @@ class SolverTest {
         assertEquals(KSolverStatus.UNSAT, status)
         core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(track1 in core)
+        assertTrue(!a in core)
 
         solver.pop()
 
@@ -109,12 +109,12 @@ class SolverTest {
         val a by boolSort
         solver.assert(a)
         solver.push()
-        val track = solver.assertAndTrack(!a)
+        solver.assertAndTrack(!a)
         var status = solver.checkWithAssumptions(listOf(a))
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(track in core || a in core)
+        assertTrue(!a in core || a in core)
         solver.pop()
         status = solver.check()
         assertEquals(KSolverStatus.SAT, status)
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt
index a06d5343f..fa2d8e2fa 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt
@@ -1,6 +1,5 @@
 package org.ksmt.solver
 
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.sort.KBoolSort
 import kotlin.time.Duration
@@ -22,28 +21,12 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
     fun assert(expr: KExpr<KBoolSort>)
 
     /**
-     * Assert an expression into solver.
-     *
-     * @return [KBoolSort] constant which is used to track a given assertion
-     * in unsat cores.
-     * @see checkWithAssumptions
-     * @see unsatCore
-     * */
-    fun assertAndTrack(expr: KExpr<KBoolSort>): KExpr<KBoolSort> {
-        val trackVar = expr.ctx.mkFreshConstDecl("track", expr.ctx.boolSort)
-        assertAndTrack(expr, trackVar)
-        return trackVar.apply()
-    }
-
-    /**
-     * Assert an expression into solver.
+     * Assert an expression into solver and track it in unsat cores.
      *
-     * [trackVar] constant which is used to track a given assertion
-     * in unsat cores.
      * @see checkWithAssumptions
      * @see unsatCore
      * */
-    fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>)
+    fun assertAndTrack(expr: KExpr<KBoolSort>)
 
     /**
      * Create a backtracking point for assertion stack.
@@ -97,7 +80,7 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
      *
      * Unsat core consists only of:
      * 1. assumptions provided in [checkWithAssumptions]
-     * 2. track variables corresponding to expressions asserted with [assertAndTrack]
+     * 2. expressions asserted with [assertAndTrack]
      * */
     fun unsatCore(): List<KExpr<KBoolSort>>
 
diff --git a/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt b/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
index f330e5866..66495f34e 100644
--- a/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
+++ b/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
@@ -4,9 +4,7 @@ import io.github.cvc5.CVC5ApiException
 import io.github.cvc5.Result
 import io.github.cvc5.Solver
 import io.github.cvc5.Term
-import io.github.cvc5.UnknownExplanation
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
@@ -14,7 +12,7 @@ import org.ksmt.solver.KSolverException
 import org.ksmt.solver.KSolverStatus
 import org.ksmt.sort.KBoolSort
 import org.ksmt.utils.NativeLibraryLoader
-import java.util.TreeSet
+import java.util.TreeMap
 import kotlin.time.Duration
 import kotlin.time.DurationUnit
 
@@ -23,19 +21,19 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
     private val cvc5Ctx = KCvc5Context(solver, ctx)
 
     private val exprInternalizer by lazy { createExprInternalizer(cvc5Ctx) }
-    private val exprConverter: KCvc5ExprConverter by lazy { createExprConverter(cvc5Ctx) }
 
     private val currentScope: UInt
         get() = cvc5TrackedAssertions.lastIndex.toUInt()
 
     private var lastCheckStatus = KSolverStatus.UNKNOWN
-    private var cvc5LastUnknownExplanation: UnknownExplanation? = null
+    private var lastReasonOfUnknown: String? = null
+    private var lastModel: KCvc5Model? = null
+    // we need TreeMap here (hashcode not implemented in Term)
+    private var cvc5LastAssumptions: TreeMap<Term, KExpr<KBoolSort>>? = null
 
-    private var cvc5CurrentLevelTrackedAssertions = mutableListOf<Term>()
+    private var cvc5CurrentLevelTrackedAssertions = TreeMap<Term, KExpr<KBoolSort>>()
     private val cvc5TrackedAssertions = mutableListOf(cvc5CurrentLevelTrackedAssertions)
 
-    private var cvc5LastAssumptions = TreeSet<Term>()
-
     init {
         solver.setOption("produce-models", "true")
         solver.setOption("produce-unsat-cores", "true")
@@ -48,8 +46,6 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
 
     open fun createExprInternalizer(cvc5Ctx: KCvc5Context): KCvc5ExprInternalizer = KCvc5ExprInternalizer(cvc5Ctx)
 
-    open fun createExprConverter(cvc5Ctx: KCvc5Context): KCvc5ExprConverter = KCvc5ExprConverter(ctx, cvc5Ctx)
-
     override fun configure(configurator: KCvc5SolverConfiguration.() -> Unit) {
         KCvc5SolverConfigurationImpl(solver).configurator()
     }
@@ -63,21 +59,21 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
         cvc5Ctx.assertPendingAxioms(solver)
     }
 
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) {
-        ctx.ensureContextMatch(expr, trackVar)
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) {
+        ctx.ensureContextMatch(expr)
 
-        val trackVarApp = trackVar.apply()
+        val trackVarApp = ctx.mkFreshConst("track", ctx.boolSort)
         val cvc5TrackVar = with(exprInternalizer) { trackVarApp.internalizeExpr() }
         val trackedExpr = with(ctx) { trackVarApp implies expr }
 
-        cvc5CurrentLevelTrackedAssertions.add(cvc5TrackVar)
+        cvc5CurrentLevelTrackedAssertions[cvc5TrackVar] = expr
 
         assert(trackedExpr)
         solver.assertFormula(cvc5TrackVar)
     }
 
     override fun push() = solver.push().also {
-        cvc5CurrentLevelTrackedAssertions = mutableListOf()
+        cvc5CurrentLevelTrackedAssertions = TreeMap()
         cvc5TrackedAssertions.add(cvc5CurrentLevelTrackedAssertions)
 
         cvc5Ctx.push()
@@ -99,39 +95,36 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
         solver.pop(n.toInt())
     }
 
-    override fun check(timeout: Duration): KSolverStatus = cvc5Try {
-        invalidatePreviousModel()
-        cvc5LastAssumptions = TreeSet()
+    override fun check(timeout: Duration): KSolverStatus = cvc5TryCheck {
         solver.updateTimeout(timeout)
         solver.checkSat().processCheckResult()
     }
 
-    override fun reasonOfUnknown(): String = cvc5Try {
-        require(lastCheckStatus == KSolverStatus.UNKNOWN) { "Unknown reason is only available after UNKNOWN checks" }
-        cvc5LastUnknownExplanation?.name ?: "no explanation"
-    }
-
-    override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus = cvc5Try {
+    override fun checkWithAssumptions(
+        assumptions: List<KExpr<KBoolSort>>,
+        timeout: Duration
+    ): KSolverStatus = cvc5TryCheck {
         ctx.ensureContextMatch(assumptions)
-        invalidatePreviousModel()
 
-        val cvc5Assumptions = with(exprInternalizer) {
-            assumptions.map { it.internalizeExpr() }
-        }.toTypedArray()
+        val lastAssumptions = TreeMap<Term, KExpr<KBoolSort>>().also { cvc5LastAssumptions = it }
+        val cvc5Assumptions = Array(assumptions.size) { idx ->
+            val assumedExpr = assumptions[idx]
+            with(exprInternalizer) {
+                assumedExpr.internalizeExpr().also {
+                    lastAssumptions[it] = assumedExpr
+                }
+            }
+        }
 
-        cvc5LastAssumptions = cvc5Assumptions.toCollection(TreeSet())
         solver.updateTimeout(timeout)
         solver.checkSatAssuming(cvc5Assumptions).processCheckResult()
     }
 
-    private var lastModel: KCvc5Model? = null
-
-    /**
-     * Cvc5 model is only valid until the next check-sat call.
-     * */
-    private fun invalidatePreviousModel() {
-        lastModel?.markInvalid()
-        lastModel = null
+    override fun reasonOfUnknown(): String = cvc5Try {
+        require(lastCheckStatus == KSolverStatus.UNKNOWN) {
+            "Unknown reason is only available after UNKNOWN checks"
+        }
+        lastReasonOfUnknown ?: "no explanation"
     }
 
     override fun model(): KModel = cvc5Try {
@@ -150,12 +143,16 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
 
     override fun unsatCore(): List<KExpr<KBoolSort>> = cvc5Try {
         require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" }
-        // we need TreeSet here (hashcode not implemented in Term)
-        val cvc5TrackedVars = cvc5TrackedAssertions.flatten().toSortedSet()
+
         val cvc5FullCore = solver.unsatCore
-        val cvc5UnsatCore = cvc5FullCore.filter { it in cvc5TrackedVars || it in cvc5LastAssumptions }
 
-        with(exprConverter) { cvc5UnsatCore.map { it.convertExpr() } }
+        val trackedTerms = TreeMap<Term, KExpr<KBoolSort>>()
+        cvc5TrackedAssertions.forEach { frame ->
+            trackedTerms.putAll(frame)
+        }
+        cvc5LastAssumptions?.also { trackedTerms.putAll(it) }
+
+        cvc5FullCore.mapNotNull { trackedTerms[it] }
     }
 
     override fun close() {
@@ -179,7 +176,9 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
         else -> KSolverStatus.UNKNOWN
     }.also {
         lastCheckStatus = it
-        if (it == KSolverStatus.UNKNOWN) cvc5LastUnknownExplanation = this.unknownExplanation
+        if (it == KSolverStatus.UNKNOWN) {
+            lastReasonOfUnknown = this.unknownExplanation?.name
+        }
     }
 
     private fun Solver.updateTimeout(timeout: Duration) {
@@ -193,6 +192,27 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
         throw KSolverException(ex)
     }
 
+    private inline fun cvc5TryCheck(body: () -> KSolverStatus): KSolverStatus = try {
+        invalidateSolverState()
+        body()
+    } catch (ex: CVC5ApiException) {
+        lastReasonOfUnknown = ex.message
+        KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
+    }
+
+    private fun invalidateSolverState() {
+        /**
+         * Cvc5 model is only valid until the next check-sat call.
+         * */
+        lastModel?.markInvalid()
+        lastModel = null
+
+        lastCheckStatus = KSolverStatus.UNKNOWN
+        lastReasonOfUnknown = null
+
+        cvc5LastAssumptions = null
+    }
+
     companion object {
         init {
             if (System.getProperty("cvc5.skipLibraryLoad") != "true") {
diff --git a/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt b/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt
index 63715790f..9dee21f9d 100644
--- a/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt
+++ b/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt
@@ -142,12 +142,12 @@ class IncrementalApiTest {
         val e3 = !c
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.checkWithAssumptions(listOf(e3))
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(2, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
         assertTrue(e3 in core)
     }
 
@@ -160,12 +160,12 @@ class IncrementalApiTest {
         val e2 = !(a and b)
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
     }
 
     @Test
@@ -173,12 +173,12 @@ class IncrementalApiTest {
         val a = boolSort.mkConst("a")
         solver.assert(a)
         solver.push()
-        val track = solver.assertAndTrack(!a)
+        solver.assertAndTrack(!a)
         var status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(track in core)
+        assertTrue(!a in core)
         solver.pop()
         status = solver.check()
         assertEquals(KSolverStatus.SAT, status)
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
index 197d8f31a..9cd0df660 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
@@ -22,7 +22,7 @@ class SolverProtocolModel private constructor(
     private val _deleteSolver: RdCall<Unit, Unit>,
     private val _configure: RdCall<List<SolverConfigurationParam>, Unit>,
     private val _assert: RdCall<AssertParams, Unit>,
-    private val _assertAndTrack: RdCall<AssertAndTrackParams, Unit>,
+    private val _assertAndTrack: RdCall<AssertParams, Unit>,
     private val _push: RdCall<Unit, Unit>,
     private val _pop: RdCall<PopParams, Unit>,
     private val _check: RdCall<CheckParams, CheckResult>,
@@ -40,7 +40,6 @@ class SolverProtocolModel private constructor(
             serializers.register(CreateSolverParams)
             serializers.register(SolverConfigurationParam)
             serializers.register(AssertParams)
-            serializers.register(AssertAndTrackParams)
             serializers.register(PopParams)
             serializers.register(CheckParams)
             serializers.register(CheckResult)
@@ -78,7 +77,7 @@ class SolverProtocolModel private constructor(
         
         private val __SolverConfigurationParamListSerializer = SolverConfigurationParam.list()
         
-        const val serializationHash = 6654719566694323594L
+        const val serializationHash = 9141130720080102681L
         
     }
     override val serializersOwner: ISerializersOwner get() = SolverProtocolModel
@@ -109,7 +108,7 @@ class SolverProtocolModel private constructor(
     /**
      * Assert and track expression
      */
-    val assertAndTrack: RdCall<AssertAndTrackParams, Unit> get() = _assertAndTrack
+    val assertAndTrack: RdCall<AssertParams, Unit> get() = _assertAndTrack
     
     /**
      * Solver push
@@ -191,7 +190,7 @@ class SolverProtocolModel private constructor(
         RdCall<Unit, Unit>(FrameworkMarshallers.Void, FrameworkMarshallers.Void),
         RdCall<List<SolverConfigurationParam>, Unit>(__SolverConfigurationParamListSerializer, FrameworkMarshallers.Void),
         RdCall<AssertParams, Unit>(AssertParams, FrameworkMarshallers.Void),
-        RdCall<AssertAndTrackParams, Unit>(AssertAndTrackParams, FrameworkMarshallers.Void),
+        RdCall<AssertParams, Unit>(AssertParams, FrameworkMarshallers.Void),
         RdCall<Unit, Unit>(FrameworkMarshallers.Void, FrameworkMarshallers.Void),
         RdCall<PopParams, Unit>(PopParams, FrameworkMarshallers.Void),
         RdCall<CheckParams, CheckResult>(CheckParams, CheckResult),
@@ -248,69 +247,6 @@ val IProtocol.solverProtocolModel get() = getOrCreateExtension(SolverProtocolMod
 
 
 
-/**
- * #### Generated from [SolverProtocolModel.kt:51]
- */
-data class AssertAndTrackParams (
-    val expression: org.ksmt.KAst,
-    val trackVar: org.ksmt.KAst
-) : IPrintable {
-    //companion
-    
-    companion object : IMarshaller<AssertAndTrackParams> {
-        override val _type: KClass<AssertAndTrackParams> = AssertAndTrackParams::class
-        
-        @Suppress("UNCHECKED_CAST")
-        override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): AssertAndTrackParams  {
-            val expression = (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller<org.ksmt.KAst>).read(ctx, buffer)
-            val trackVar = (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller<org.ksmt.KAst>).read(ctx, buffer)
-            return AssertAndTrackParams(expression, trackVar)
-        }
-        
-        override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: AssertAndTrackParams)  {
-            (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller<org.ksmt.KAst>).write(ctx,buffer, value.expression)
-            (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller<org.ksmt.KAst>).write(ctx,buffer, value.trackVar)
-        }
-        
-        
-    }
-    //fields
-    //methods
-    //initializer
-    //secondary constructor
-    //equals trait
-    override fun equals(other: Any?): Boolean  {
-        if (this === other) return true
-        if (other == null || other::class != this::class) return false
-        
-        other as AssertAndTrackParams
-        
-        if (expression != other.expression) return false
-        if (trackVar != other.trackVar) return false
-        
-        return true
-    }
-    //hash code trait
-    override fun hashCode(): Int  {
-        var __r = 0
-        __r = __r*31 + expression.hashCode()
-        __r = __r*31 + trackVar.hashCode()
-        return __r
-    }
-    //pretty print
-    override fun print(printer: PrettyPrinter)  {
-        printer.println("AssertAndTrackParams (")
-        printer.indent {
-            print("expression = "); expression.print(printer); println()
-            print("trackVar = "); trackVar.print(printer); println()
-        }
-        printer.print(")")
-    }
-    //deepClone
-    //contexts
-}
-
-
 /**
  * #### Generated from [SolverProtocolModel.kt:47]
  */
@@ -369,7 +305,7 @@ data class AssertParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:60]
+ * #### Generated from [SolverProtocolModel.kt:55]
  */
 data class CheckParams (
     val timeout: Long
@@ -426,7 +362,7 @@ data class CheckParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:64]
+ * #### Generated from [SolverProtocolModel.kt:59]
  */
 data class CheckResult (
     val status: org.ksmt.solver.KSolverStatus
@@ -483,7 +419,7 @@ data class CheckResult (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:68]
+ * #### Generated from [SolverProtocolModel.kt:63]
  */
 data class CheckWithAssumptionsParams (
     val assumptions: List<org.ksmt.KAst>,
@@ -651,7 +587,7 @@ data class CreateSolverParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:87]
+ * #### Generated from [SolverProtocolModel.kt:82]
  */
 data class ModelEntry (
     val decl: org.ksmt.KAst,
@@ -726,7 +662,7 @@ data class ModelEntry (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:81]
+ * #### Generated from [SolverProtocolModel.kt:76]
  */
 data class ModelFuncInterpEntry (
     val hasVars: Boolean,
@@ -795,7 +731,7 @@ data class ModelFuncInterpEntry (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:99]
+ * #### Generated from [SolverProtocolModel.kt:94]
  */
 data class ModelResult (
     val declarations: List<org.ksmt.KAst>,
@@ -864,7 +800,7 @@ data class ModelResult (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:94]
+ * #### Generated from [SolverProtocolModel.kt:89]
  */
 data class ModelUninterpretedSortUniverse (
     val sort: org.ksmt.KAst,
@@ -927,7 +863,7 @@ data class ModelUninterpretedSortUniverse (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:56]
+ * #### Generated from [SolverProtocolModel.kt:51]
  */
 data class PopParams (
     val levels: UInt
@@ -984,7 +920,7 @@ data class PopParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:77]
+ * #### Generated from [SolverProtocolModel.kt:72]
  */
 data class ReasonUnknownResult (
     val reasonUnknown: String
@@ -1127,7 +1063,7 @@ enum class SolverType {
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:73]
+ * #### Generated from [SolverProtocolModel.kt:68]
  */
 data class UnsatCoreResult (
     val core: List<org.ksmt.KAst>
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt
index 585c03a5e..526c2af47 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt
@@ -1,6 +1,5 @@
 package org.ksmt.solver.async
 
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
@@ -15,7 +14,7 @@ interface KAsyncSolver<Config : KSolverConfiguration> : KSolver<Config> {
 
     suspend fun assertAsync(expr: KExpr<KBoolSort>)
 
-    suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>)
+    suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>)
 
     suspend fun pushAsync()
 
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt
index fdc2410d2..54a137274 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt
@@ -11,7 +11,6 @@ import kotlinx.coroutines.joinAll
 import kotlinx.coroutines.launch
 import kotlinx.coroutines.newSingleThreadContext
 import kotlinx.coroutines.runBlocking
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
@@ -107,8 +106,8 @@ class KPortfolioSolver(
         assertAsync(expr)
     }
 
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) = runBlocking {
-        assertAndTrackAsync(expr, trackVar)
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) = runBlocking {
+        assertAndTrackAsync(expr)
     }
 
     override fun push() = runBlocking {
@@ -154,10 +153,9 @@ class KPortfolioSolver(
         assertAsync(expr)
     }
 
-    override suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        solverOperation {
-            assertAndTrackAsync(expr, trackVar)
-        }
+    override suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>) = solverOperation {
+        assertAndTrackAsync(expr)
+    }
 
     override suspend fun pushAsync() = solverOperation {
         pushAsync()
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt
index f0ab06390..ed82d43f8 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt
@@ -4,7 +4,6 @@ import com.jetbrains.rd.util.AtomicReference
 import com.jetbrains.rd.util.threading.SpinWait
 import kotlinx.coroutines.sync.Mutex
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.runner.generated.ConfigurationBuilder
 import org.ksmt.runner.generated.models.SolverConfigurationParam
@@ -102,31 +101,28 @@ class KSolverRunner<Config : KSolverConfiguration>(
         }
     }
 
-    override suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        assertAndTrack(expr, trackVar) { e, track ->
-            ensureInitializedAndExecuteAsync(onException = {}) {
-                assertAndTrackAsync(e, track)
-            }
+    override suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>) = assertAndTrack(expr) { e ->
+        ensureInitializedAndExecuteAsync(onException = {}) {
+            assertAndTrackAsync(e)
         }
+    }
 
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        assertAndTrack(expr, trackVar) { e, track ->
-            ensureInitializedAndExecuteSync(onException = {}) {
-                assertAndTrackSync(e, track)
-            }
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) = assertAndTrack(expr) { e ->
+        ensureInitializedAndExecuteSync(onException = {}) {
+            assertAndTrackSync(e)
         }
+    }
 
     private inline fun assertAndTrack(
         expr: KExpr<KBoolSort>,
-        trackVar: KConstDecl<KBoolSort>,
-        execute: (KExpr<KBoolSort>, KConstDecl<KBoolSort>) -> Unit
+        execute: (KExpr<KBoolSort>) -> Unit
     ) {
-        ctx.ensureContextMatch(expr, trackVar)
+        ctx.ensureContextMatch(expr)
 
         try {
-            execute(expr, trackVar)
+            execute(expr)
         } finally {
-            solverState.assertAndTrack(expr, trackVar)
+            solverState.assertAndTrack(expr)
         }
     }
 
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt
index 82d3a346b..a4668486a 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt
@@ -11,12 +11,10 @@ import com.jetbrains.rd.util.threading.SynchronousScheduler
 import kotlinx.coroutines.TimeoutCancellationException
 import kotlinx.coroutines.withTimeout
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KUninterpretedSortValue
 import org.ksmt.runner.core.KsmtWorkerSession
-import org.ksmt.runner.generated.models.AssertAndTrackParams
 import org.ksmt.runner.generated.models.AssertParams
 import org.ksmt.runner.generated.models.CheckParams
 import org.ksmt.runner.generated.models.CheckResult
@@ -94,27 +92,21 @@ class KSolverRunnerExecutor(
         query(AssertParams(expr))
     }
 
-    fun assertAndTrackSync(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        assertAndTrack(expr, trackVar) { params ->
-            queryWithTimeoutAndExceptionHandlingSync {
-                assertAndTrack.querySync(params)
-            }
+    fun assertAndTrackSync(expr: KExpr<KBoolSort>) = assertAndTrack(expr) { params ->
+        queryWithTimeoutAndExceptionHandlingSync {
+            assertAndTrack.querySync(params)
         }
+    }
 
-    suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        assertAndTrack(expr, trackVar) { params ->
-            queryWithTimeoutAndExceptionHandlingAsync {
-                assertAndTrack.queryAsync(params)
-            }
+    suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>) = assertAndTrack(expr) { params ->
+        queryWithTimeoutAndExceptionHandlingAsync {
+            assertAndTrack.queryAsync(params)
         }
+    }
 
-    private inline fun assertAndTrack(
-        expr: KExpr<KBoolSort>,
-        trackVar: KConstDecl<KBoolSort>,
-        query: (AssertAndTrackParams) -> Unit
-    ) {
+    private inline fun assertAndTrack(expr: KExpr<KBoolSort>, query: (AssertParams) -> Unit) {
         ensureActive()
-        query(AssertAndTrackParams(expr, trackVar))
+        query(AssertParams(expr))
     }
 
     fun pushSync() = push {
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt
index 22226265d..aa132cabf 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt
@@ -1,6 +1,5 @@
 package org.ksmt.solver.runner
 
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.runner.generated.models.SolverConfigurationParam
 import org.ksmt.sort.KBoolSort
@@ -21,10 +20,7 @@ import java.util.concurrent.ConcurrentLinkedQueue
 class KSolverState {
     private sealed interface AssertFrame
     private data class ExprAssertFrame(val expr: KExpr<KBoolSort>) : AssertFrame
-    private data class AssertAndTrackFrame(
-        val expr: KExpr<KBoolSort>,
-        val trackVar: KConstDecl<KBoolSort>
-    ) : AssertFrame
+    private data class AssertAndTrackFrame(val expr: KExpr<KBoolSort>) : AssertFrame
 
     private val configuration = ConcurrentLinkedQueue<SolverConfigurationParam>()
 
@@ -47,8 +43,8 @@ class KSolverState {
         assertFrames.last.add(ExprAssertFrame(expr))
     }
 
-    fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) {
-        assertFrames.last.add(AssertAndTrackFrame(expr, trackVar))
+    fun assertAndTrack(expr: KExpr<KBoolSort>) {
+        assertFrames.last.add(AssertAndTrackFrame(expr))
     }
 
     fun push() {
@@ -65,14 +61,14 @@ class KSolverState {
         configureSolver = { executor.configureAsync(it) },
         pushScope = { executor.pushAsync() },
         assertExpr = { executor.assertAsync(it) },
-        assertExprAndTrack = { expr, trackVar -> executor.assertAndTrackAsync(expr, trackVar) }
+        assertExprAndTrack = { expr -> executor.assertAndTrackAsync(expr) }
     )
 
     fun applySync(executor: KSolverRunnerExecutor) = replayState(
         configureSolver = { executor.configureSync(it) },
         pushScope = { executor.pushSync() },
         assertExpr = { executor.assertSync(it) },
-        assertExprAndTrack = { expr, trackVar -> executor.assertAndTrackSync(expr, trackVar) }
+        assertExprAndTrack = { expr -> executor.assertAndTrackSync(expr) }
     )
 
     /**
@@ -83,7 +79,7 @@ class KSolverState {
         configureSolver: (List<SolverConfigurationParam>) -> Unit,
         pushScope: () -> Unit,
         assertExpr: (KExpr<KBoolSort>) -> Unit,
-        assertExprAndTrack: (KExpr<KBoolSort>, KConstDecl<KBoolSort>) -> Unit
+        assertExprAndTrack: (KExpr<KBoolSort>) -> Unit
     ) {
         if (configuration.isNotEmpty()) {
             configureSolver(configuration.toList())
@@ -100,7 +96,7 @@ class KSolverState {
             for (assertion in frame) {
                 when (assertion) {
                     is ExprAssertFrame -> assertExpr(assertion.expr)
-                    is AssertAndTrackFrame -> assertExprAndTrack(assertion.expr, assertion.trackVar)
+                    is AssertAndTrackFrame -> assertExprAndTrack(assertion.expr)
                 }
             }
         }
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt
index afa654c3e..273bde0eb 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt
@@ -2,7 +2,6 @@ package org.ksmt.solver.runner
 
 import com.jetbrains.rd.framework.IProtocol
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.runner.core.ChildProcessBase
 import org.ksmt.runner.core.KsmtWorkerArgs
@@ -88,7 +87,7 @@ class KSolverWorkerProcess : ChildProcessBase<SolverProtocolModel>() {
         }
         assertAndTrack.measureExecutionForTermination { params ->
             @Suppress("UNCHECKED_CAST")
-            solver.assertAndTrack(params.expression as KExpr<KBoolSort>, params.trackVar as KConstDecl<KBoolSort>)
+            solver.assertAndTrack(params.expression as KExpr<KBoolSort>)
         }
         push.measureExecutionForTermination {
             solver.push()
diff --git a/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt b/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt
index b03fa96c9..0d80adc6a 100644
--- a/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt
+++ b/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt
@@ -48,11 +48,6 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
         field("expression", kastType)
     }
 
-    private val assertAndTrackParams = structdef {
-        field("expression", kastType)
-        field("trackVar", kastType)
-    }
-
     private val popParams = structdef {
         field("levels", PredefinedType.uint)
     }
@@ -119,7 +114,7 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
             async
             documentation = "Assert expression"
         }
-        call("assertAndTrack", assertAndTrackParams, PredefinedType.void).apply {
+        call("assertAndTrack", assertParams, PredefinedType.void).apply {
             async
             documentation = "Assert and track expression"
         }
diff --git a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt
index 34a8b2838..c514dc32f 100644
--- a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt
+++ b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt
@@ -1,7 +1,6 @@
 package org.ksmt.solver.runner
 
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
@@ -54,7 +53,7 @@ class CustomSolverTest {
         override fun assert(expr: KExpr<KBoolSort>) {
         }
 
-        override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) {
+        override fun assertAndTrack(expr: KExpr<KBoolSort>) {
         }
 
         override fun push() {
diff --git a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt
index 64de3bf82..98df1dc57 100644
--- a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt
+++ b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt
@@ -58,7 +58,7 @@ class PortfolioSolverTest {
         val e3 = !c
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.checkWithAssumptions(listOf(e3))
 
         assertEquals(KSolverStatus.UNSAT, status)
@@ -66,7 +66,7 @@ class PortfolioSolverTest {
         val core = solver.unsatCore()
 
         assertEquals(2, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
         assertTrue(e3 in core)
     }
 
@@ -79,7 +79,7 @@ class PortfolioSolverTest {
         val e2 = !(a and b)
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.check()
 
         assertEquals(KSolverStatus.UNSAT, status)
@@ -87,7 +87,7 @@ class PortfolioSolverTest {
         val core = solver.unsatCore()
 
         assertEquals(1, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
     }
 
     @Test
@@ -96,7 +96,7 @@ class PortfolioSolverTest {
 
         solver.assert(a)
         solver.push()
-        val track = solver.assertAndTrack(!a)
+        solver.assertAndTrack(!a)
         var status = solver.check()
 
         assertEquals(KSolverStatus.UNSAT, status)
@@ -104,7 +104,7 @@ class PortfolioSolverTest {
         val core = solver.unsatCore()
 
         assertEquals(1, core.size)
-        assertTrue(track in core)
+        assertTrue(!a in core)
 
         solver.pop()
         status = solver.check()
diff --git a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt
index 966159423..168b5e8b5 100644
--- a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt
+++ b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt
@@ -62,12 +62,12 @@ class SolverRunnerTest {
         val e3 = !c
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.checkWithAssumptions(listOf(e3))
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(2, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
         assertTrue(e3 in core)
     }
 
@@ -80,12 +80,12 @@ class SolverRunnerTest {
         val e2 = !(a and b)
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
     }
 
     @Test
@@ -93,12 +93,12 @@ class SolverRunnerTest {
         val a = boolSort.mkConst("a")
         solver.assert(a)
         solver.push()
-        val track = solver.assertAndTrack(!a)
+        solver.assertAndTrack(!a)
         var status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(track in core)
+        assertTrue(!a in core)
         solver.pop()
         status = solver.check()
         assertEquals(KSolverStatus.SAT, status)
diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/CheckWithAssumptionsTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/CheckWithAssumptionsTest.kt
new file mode 100644
index 000000000..881a0248c
--- /dev/null
+++ b/ksmt-test/src/test/kotlin/org/ksmt/test/CheckWithAssumptionsTest.kt
@@ -0,0 +1,79 @@
+package org.ksmt.test
+
+import org.ksmt.KContext
+import org.ksmt.solver.KSolver
+import org.ksmt.solver.KSolverStatus
+import org.ksmt.solver.bitwuzla.KBitwuzlaSolver
+import org.ksmt.solver.cvc5.KCvc5Solver
+import org.ksmt.solver.yices.KYicesSolver
+import org.ksmt.solver.z3.KZ3Solver
+import org.ksmt.utils.getValue
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertTrue
+
+class CheckWithAssumptionsTest {
+
+    @Test
+    fun testComplexAssumptionZ3() = testComplexAssumption { KZ3Solver(it) }
+
+    @Test
+    fun testComplexAssumptionBitwuzla() = testComplexAssumption { KBitwuzlaSolver(it) }
+
+    @Test
+    fun testComplexAssumptionYices() = testComplexAssumption { KYicesSolver(it) }
+
+    @Test
+    fun testComplexAssumptionCvc() = testComplexAssumption { KCvc5Solver(it) }
+
+    @Test
+    fun testUnsatCoreGenerationZ3() = testUnsatCoreGeneration { KZ3Solver(it) }
+
+    @Test
+    fun testUnsatCoreGenerationBitwuzla() = testUnsatCoreGeneration { KBitwuzlaSolver(it) }
+
+    @Test
+    fun testUnsatCoreGenerationYices() = testUnsatCoreGeneration { KYicesSolver(it) }
+
+    @Test
+    fun testUnsatCoreGenerationCvc() = testUnsatCoreGeneration { KCvc5Solver(it) }
+
+    private fun testComplexAssumption(mkSolver: (KContext) -> KSolver<*>) = with(KContext()) {
+        mkSolver(this).use { solver ->
+            val a by bv32Sort
+            val b by bv32Sort
+
+            solver.assert(a eq mkBv(0))
+            solver.assert(b eq mkBv(0))
+
+            val expr = mkBvUnsignedGreaterExpr(a, b)
+            val status = solver.checkWithAssumptions(listOf(expr))
+
+            assertEquals(KSolverStatus.UNSAT, status)
+        }
+    }
+
+    private fun testUnsatCoreGeneration(mkSolver: (KContext) -> KSolver<*>) = with(KContext()) {
+        mkSolver(this).use { solver ->
+            val a by boolSort
+            val b by boolSort
+            val c by boolSort
+
+            val e1 = (a and b) or c
+            val e2 = !(a and b)
+            val e3 = !c
+
+            solver.assert(e1)
+            solver.assertAndTrack(e2)
+
+            val status = solver.checkWithAssumptions(listOf(e3))
+            assertEquals(KSolverStatus.UNSAT, status)
+
+            val core = solver.unsatCore()
+            assertEquals(2, core.size)
+
+            assertTrue(e2 in core)
+            assertTrue(e3 in core)
+        }
+    }
+}
diff --git a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt
index 364ef6010..7ab561d80 100644
--- a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt
+++ b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt
@@ -4,8 +4,9 @@ import com.sri.yices.Config
 import com.sri.yices.Context
 import com.sri.yices.Status
 import com.sri.yices.YicesException
+import it.unimi.dsi.fastutil.ints.IntArrayList
+import it.unimi.dsi.fastutil.ints.IntOpenHashSet
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
@@ -33,9 +34,11 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
         KYicesExprConverter(ctx, yicesCtx)
     }
 
+    private var lastAssumptions: TrackedAssumptions? = null
     private var lastCheckStatus = KSolverStatus.UNKNOWN
+    private var lastReasonOfUnknown: String? = null
 
-    private var currentLevelTrackedAssertions = mutableListOf<YicesTerm>()
+    private var currentLevelTrackedAssertions = mutableListOf<Pair<KExpr<KBoolSort>, YicesTerm>>()
     private val trackedAssertions = mutableListOf(currentLevelTrackedAssertions)
 
     private val timer = Timer()
@@ -55,16 +58,16 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
         nativeContext.assertFormula(yicesExpr)
     }
 
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) = yicesTry {
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) = yicesTry {
         ctx.ensureContextMatch(expr)
 
-        val trackVarExpr = ctx.mkConstApp(trackVar)
+        val trackVarExpr = ctx.mkFreshConst("track", ctx.boolSort)
         val trackedExpr = with(ctx) { !trackVarExpr or expr }
 
         assert(trackedExpr)
 
         val yicesTrackVar = with(exprInternalizer) { trackVarExpr.internalize() }
-        currentLevelTrackedAssertions += yicesTrackVar
+        currentLevelTrackedAssertions += expr to yicesTrackVar
     }
 
     override fun push(): Unit = yicesTry {
@@ -89,12 +92,12 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
         currentLevelTrackedAssertions = trackedAssertions.last()
     }
 
-    override fun check(timeout: Duration): KSolverStatus {
+    override fun check(timeout: Duration): KSolverStatus = yicesTryCheck {
         if (trackedAssertions.any { it.isNotEmpty() }) {
             return checkWithAssumptions(emptyList(), timeout)
         }
 
-        return withTimer(timeout) {
+        checkWithTimer(timeout) {
             nativeContext.check()
         }.processCheckResult()
     }
@@ -102,17 +105,25 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
     override fun checkWithAssumptions(
         assumptions: List<KExpr<KBoolSort>>,
         timeout: Duration
-    ): KSolverStatus {
+    ): KSolverStatus = yicesTryCheck {
         ctx.ensureContextMatch(assumptions)
 
-        val yicesAssumptions = mutableListOf<YicesTerm>()
-        trackedAssertions.flatMapTo(yicesAssumptions) { it }
+        val yicesAssumptions = TrackedAssumptions().also { lastAssumptions = it }
+
+        trackedAssertions.forEach { frame ->
+            frame.forEach { assertion ->
+                yicesAssumptions.assumeTrackedAssertion(assertion)
+            }
+        }
+
         with(exprInternalizer) {
-            assumptions.mapTo(yicesAssumptions) { it.internalize() }
+            assumptions.forEach { assumedExpr ->
+                yicesAssumptions.assumeAssumption(assumedExpr, assumedExpr.internalize())
+            }
         }
 
-        return withTimer(timeout) {
-            nativeContext.checkWithAssumptions(yicesAssumptions.toIntArray())
+        checkWithTimer(timeout) {
+            nativeContext.checkWithAssumptions(yicesAssumptions.assumedTerms())
         }.processCheckResult()
     }
 
@@ -130,9 +141,7 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
             "Unsat cores are only available after UNSAT checks"
         }
 
-        val yicesCore = nativeContext.unsatCore
-
-        with(exprConverter) { yicesCore.map { it.convert(ctx.boolSort) } }
+        lastAssumptions?.resolveUnsatCore(nativeContext.unsatCore) ?: emptyList()
     }
 
     override fun reasonOfUnknown(): String {
@@ -141,14 +150,14 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
         }
 
         // There is no way to retrieve reason of unknown from Yices in general case.
-        return "unknown"
+        return lastReasonOfUnknown ?: "unknown"
     }
 
     override fun interrupt() = yicesTry {
         nativeContext.stopSearch()
     }
 
-    private inline fun <T> withTimer(timeout: Duration, body: () -> T): T {
+    private inline fun <T> checkWithTimer(timeout: Duration, body: () -> T): T {
         val task = StopSearchTask()
 
         if (timeout.isFinite()) {
@@ -157,8 +166,6 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
 
         return try {
             body()
-        } catch (ex: YicesException) {
-            throw KSolverException(ex)
         } finally {
             task.cancel()
         }
@@ -170,6 +177,20 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
         throw KSolverException(ex)
     }
 
+    private inline fun yicesTryCheck(body: () -> KSolverStatus): KSolverStatus = try {
+        invalidateSolverState()
+        body()
+    } catch (ex: YicesException) {
+        lastReasonOfUnknown = ex.message
+        KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
+    }
+
+    private fun invalidateSolverState() {
+        lastCheckStatus = KSolverStatus.UNKNOWN
+        lastReasonOfUnknown = null
+        lastAssumptions = null
+    }
+
     private fun Status.processCheckResult() = when (this) {
         Status.SAT -> KSolverStatus.SAT
         Status.UNSAT -> KSolverStatus.UNSAT
@@ -187,4 +208,27 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
             nativeContext.stopSearch()
         }
     }
+
+    private class TrackedAssumptions {
+        private val assumedExprs = arrayListOf<Pair<KExpr<KBoolSort>, YicesTerm>>()
+        private val assumedTerms = IntArrayList()
+
+        fun assumeTrackedAssertion(trackedAssertion: Pair<KExpr<KBoolSort>, YicesTerm>) {
+            assumedExprs.add(trackedAssertion)
+            assumedTerms.add(trackedAssertion.second)
+        }
+
+        fun assumeAssumption(expr: KExpr<KBoolSort>, term: YicesTerm) =
+            assumeTrackedAssertion(expr to term)
+
+        fun assumedTerms(): YicesTermArray {
+            assumedTerms.trim() // Elements length now equal to size
+            return assumedTerms.elements()
+        }
+
+        fun resolveUnsatCore(yicesUnsatCore: YicesTermArray): List<KExpr<KBoolSort>> {
+            val unsatCoreTerms = IntOpenHashSet(yicesUnsatCore)
+            return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } }
+        }
+    }
 }
diff --git a/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt b/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt
index 9a8b114a8..e52717dc0 100644
--- a/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt
+++ b/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt
@@ -41,12 +41,12 @@ class SolverTest {
         val e3 = !c
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.checkWithAssumptions(listOf(e3))
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(2, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
         assertTrue(e3 in core)
     }
 
@@ -60,12 +60,12 @@ class SolverTest {
         val e2 = !(a and b)
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
     }
 
     @Test
@@ -80,17 +80,17 @@ class SolverTest {
 
         solver.push()
 
-        val track1 = solver.assertAndTrack(!a)
+        solver.assertAndTrack(!a)
 
         solver.push()
 
-        val track2 = solver.assertAndTrack(!b)
+        solver.assertAndTrack(!b)
 
         var status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         var core = solver.unsatCore()
         assertEquals(2, core.size)
-        assertTrue(track1 in core && track2 in core)
+        assertTrue(!a in core && !b in core)
 
         solver.pop()
 
@@ -100,7 +100,7 @@ class SolverTest {
         assertEquals(KSolverStatus.UNSAT, status)
         core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(track1 in core)
+        assertTrue(!a in core)
 
         solver.pop()
 
diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt
index 6e933da5e..062a453ed 100644
--- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt
+++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt
@@ -7,8 +7,8 @@ import com.microsoft.z3.solverAssert
 import com.microsoft.z3.solverAssertAndTrack
 import com.microsoft.z3.solverCheckAssumptions
 import com.microsoft.z3.solverGetUnsatCore
+import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap
 import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.solver.KSolver
@@ -26,6 +26,7 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
     private val z3Ctx = KZ3Context(ctx)
     private val solver = createSolver()
     private var lastCheckStatus = KSolverStatus.UNKNOWN
+    private var lastReasonOfUnknown: String? = null
     private var currentScope: UInt = 0u
 
     @Suppress("LeakingThis")
@@ -77,16 +78,21 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
         z3Ctx.assertPendingAxioms(solver)
     }
 
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) = z3Try {
-        ctx.ensureContextMatch(expr, trackVar)
+    private val trackedAssertions = Long2ObjectOpenHashMap<KExpr<KBoolSort>>()
 
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) = z3Try {
+        ctx.ensureContextMatch(expr)
+
+        val trackExpr = ctx.mkFreshConst("track", ctx.boolSort)
         val z3Expr = with(exprInternalizer) { expr.internalizeExpr() }
-        val z3TrackVar = with(exprInternalizer) { trackVar.apply().internalizeExpr() }
+        val z3TrackVar = with(exprInternalizer) { trackExpr.internalizeExpr() }
+
+        trackedAssertions.put(z3TrackVar, expr)
 
         solver.solverAssertAndTrack(z3Expr, z3TrackVar)
     }
 
-    override fun check(timeout: Duration): KSolverStatus = z3Try {
+    override fun check(timeout: Duration): KSolverStatus = z3TryCheck {
         solver.updateTimeout(timeout)
         solver.check().processCheckResult()
     }
@@ -94,7 +100,7 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
     override fun checkWithAssumptions(
         assumptions: List<KExpr<KBoolSort>>,
         timeout: Duration
-    ): KSolverStatus = z3Try {
+    ): KSolverStatus = z3TryCheck {
         ctx.ensureContextMatch(assumptions)
 
         val z3Assumptions = with(exprInternalizer) {
@@ -115,20 +121,19 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
         KZ3Model(model, ctx, z3Ctx, exprInternalizer)
     }
 
-    // TODO add mapping back from tracked variable into initial value
     override fun unsatCore(): List<KExpr<KBoolSort>> = z3Try {
         require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" }
 
         val unsatCore = solver.solverGetUnsatCore()
 
         with(exprConverter) {
-            unsatCore.map { it.convertExpr() }
+            unsatCore.map { trackedAssertions.get(it) ?: it.convertExpr() }
         }
     }
 
     override fun reasonOfUnknown(): String = z3Try {
         require(lastCheckStatus == KSolverStatus.UNKNOWN) { "Unknown reason is only available after UNKNOWN checks" }
-        solver.reasonUnknown
+        lastReasonOfUnknown ?: solver.reasonUnknown
     }
 
     override fun interrupt() = z3Try {
@@ -165,6 +170,19 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
         throw KSolverException(ex)
     }
 
+    private fun invalidateSolverState() {
+        lastReasonOfUnknown = null
+        lastCheckStatus = KSolverStatus.UNKNOWN
+    }
+
+    private inline fun z3TryCheck(body: () -> KSolverStatus): KSolverStatus = try {
+        invalidateSolverState()
+        body()
+    } catch (ex: Z3Exception) {
+        lastReasonOfUnknown = ex.message
+        KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
+    }
+
     companion object {
         init {
             System.setProperty("z3.skipLibraryLoad", "true")
diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt
index c309169f6..274fb3bcc 100644
--- a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt
+++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt
@@ -23,12 +23,12 @@ class IncrementalApiTest {
         val e3 = !c
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.checkWithAssumptions(listOf(e3))
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(2, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
         assertTrue(e3 in core)
     }
 
@@ -41,12 +41,12 @@ class IncrementalApiTest {
         val e2 = !(a and b)
 
         solver.assert(e1)
-        val e2Track = solver.assertAndTrack(e2)
+        solver.assertAndTrack(e2)
         val status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(e2Track in core)
+        assertTrue(e2 in core)
     }
 
     @Test
@@ -54,12 +54,12 @@ class IncrementalApiTest {
         val a = boolSort.mkConst("a")
         solver.assert(a)
         solver.push()
-        val track = solver.assertAndTrack(!a)
+        solver.assertAndTrack(!a)
         var status = solver.check()
         assertEquals(KSolverStatus.UNSAT, status)
         val core = solver.unsatCore()
         assertEquals(1, core.size)
-        assertTrue(track in core)
+        assertTrue(!a in core)
         solver.pop()
         status = solver.check()
         assertEquals(KSolverStatus.SAT, status)