diff --git a/README.md b/README.md
index 2fc051b9b..db5a1d4db 100644
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.9)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.10)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.9")
+implementation("io.ksmt:ksmt-core:0.5.10")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.9")
+implementation("io.ksmt:ksmt-z3:0.5.10")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 
diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
index fca1322f7..ea4191eeb 100644
--- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
+++ b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.9"
+version = "0.5.10"
 
 repositories {
     mavenCentral()
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 5a93254f3..0319e4d2d 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.9")    
+    implementation("io.ksmt:ksmt-core:0.5.10")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.9")
+    implementation("io.ksmt:ksmt-z3:0.5.10")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.9")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.10")
 }
 ```
 
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index 88bfe3edd..68c07f90e 100644
--- a/examples/build.gradle.kts
+++ b/examples/build.gradle.kts
@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.9")
+    implementation("io.ksmt:ksmt-core:0.5.10")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.9")
+    implementation("io.ksmt:ksmt-z3:0.5.10")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.9")
+    implementation("io.ksmt:ksmt-runner:0.5.10")
 }
 
 java {
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
index 7933c0f45..81b012048 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
@@ -78,6 +78,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
 
         // Simplify argument and retry expr simplification
         if (simplifiedArgument == null) {
+            markExpressionAsNotTransformed()
             expr.transformAfter(argument)
             return expr
         }
@@ -92,6 +93,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
         expr.processNextArgument()
 
         // Repeat simplification with next argument
+        markExpressionAsNotTransformed()
         retryExprTransformation(expr)
 
         return expr
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
index 288280cee..00abc2a83 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
@@ -27,7 +27,7 @@ import java.util.IdentityHashMap
  * a [transformExprAfterTransformed] method.
  * */
 abstract class KNonRecursiveTransformerBase: KTransformer {
-    private val transformed = IdentityHashMap<KExpr<*>, KExpr<*>>()
+    private var transformed = IdentityHashMap<KExpr<*>, KExpr<*>>()
     private val exprStack = ArrayList<KExpr<*>>()
     private var exprWasTransformed = false
 
@@ -41,7 +41,7 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
             while (exprStack.size > initialStackSize) {
                 val e = exprStack.removeLast()
 
-                val cachedExpr = transformedExpr(expr)
+                val cachedExpr = transformedExpr(e)
                 if (cachedExpr != null) {
                     continue
                 }
@@ -63,6 +63,14 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
         return transformedExpr(expr) ?: error("expr was not properly transformed: $expr")
     }
 
+    /**
+     * Reset transformer expression cache.
+     * */
+    fun resetCache() {
+        check(exprStack.isEmpty()) { "Can not reset cache during expression transformation" }
+        transformed = IdentityHashMap()
+    }
+
     /**
      * Disable [KTransformer] transformApp implementation since it is incorrect
      * for non-recursive usage.
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt
index 4e453bfc3..70a462833 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt
@@ -22,7 +22,7 @@ import java.util.IdentityHashMap
  * a [visitExprAfterVisited] method.
  * */
 abstract class KNonRecursiveVisitorBase<V : Any> : KVisitor<KExprVisitResult<V>> {
-    private val visitResults = IdentityHashMap<KExpr<*>, V>()
+    private var visitResults = IdentityHashMap<KExpr<*>, V>()
     private val exprStack = ArrayList<KExpr<*>>()
 
     private var lastVisitedExpr: KExpr<*>? = null
@@ -100,6 +100,14 @@ abstract class KNonRecursiveVisitorBase<V : Any> : KVisitor<KExprVisitResult<V>>
         return expr
     }
 
+    /**
+     * Reset visitor expression cache.
+     * */
+    fun resetCache() {
+        check(exprStack.isEmpty()) { "Can not reset cache during expression visit" }
+        visitResults = IdentityHashMap()
+    }
+
     /**
      * Disable [KVisitor] visitApp implementation since it is incorrect
      * for non-recursive usage.
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt
index 21a641d68..1efda992f 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt
@@ -20,6 +20,15 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
     @JvmName("assertExpr")
     fun assert(expr: KExpr<KBoolSort>)
 
+
+    /**
+     * Assert multiple expressions into solver.
+     *
+     * @see check
+     * */
+    @JvmName("assertExprs")
+    fun assert(exprs: List<KExpr<KBoolSort>>) = exprs.forEach { assert(it) }
+
     /**
      * Assert an expression into solver and track it in unsat cores.
      *
@@ -28,6 +37,14 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
      * */
     fun assertAndTrack(expr: KExpr<KBoolSort>)
 
+    /**
+     * Assert multiple expressions into solver and track them in unsat cores.
+     *
+     * @see checkWithAssumptions
+     * @see unsatCore
+     * */
+    fun assertAndTrack(exprs: List<KExpr<KBoolSort>>) = exprs.forEach { assertAndTrack(it) }
+
     /**
      * Create a backtracking point for assertion stack.
      *
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
index 3e06be7f2..89b598d49 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
@@ -22,7 +22,9 @@ 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 _bulkAssert: RdCall<BulkAssertParams, Unit>,
     private val _assertAndTrack: RdCall<AssertParams, Unit>,
+    private val _bulkAssertAndTrack: RdCall<BulkAssertParams, Unit>,
     private val _push: RdCall<Unit, Unit>,
     private val _pop: RdCall<PopParams, Unit>,
     private val _check: RdCall<CheckParams, CheckResult>,
@@ -40,6 +42,7 @@ class SolverProtocolModel private constructor(
             serializers.register(CreateSolverParams)
             serializers.register(SolverConfigurationParam)
             serializers.register(AssertParams)
+            serializers.register(BulkAssertParams)
             serializers.register(PopParams)
             serializers.register(CheckParams)
             serializers.register(CheckResult)
@@ -77,7 +80,7 @@ class SolverProtocolModel private constructor(
         
         private val __SolverConfigurationParamListSerializer = SolverConfigurationParam.list()
         
-        const val serializationHash = 9141130720080102681L
+        const val serializationHash = 6588187342629653927L
         
     }
     override val serializersOwner: ISerializersOwner get() = SolverProtocolModel
@@ -105,11 +108,21 @@ class SolverProtocolModel private constructor(
      */
     val assert: RdCall<AssertParams, Unit> get() = _assert
     
+    /**
+     * Assert multiple expressions
+     */
+    val bulkAssert: RdCall<BulkAssertParams, Unit> get() = _bulkAssert
+    
     /**
      * Assert and track expression
      */
     val assertAndTrack: RdCall<AssertParams, Unit> get() = _assertAndTrack
     
+    /**
+     * Assert and track multiple expressions
+     */
+    val bulkAssertAndTrack: RdCall<BulkAssertParams, Unit> get() = _bulkAssertAndTrack
+    
     /**
      * Solver push
      */
@@ -156,7 +169,9 @@ class SolverProtocolModel private constructor(
         _deleteSolver.async = true
         _configure.async = true
         _assert.async = true
+        _bulkAssert.async = true
         _assertAndTrack.async = true
+        _bulkAssertAndTrack.async = true
         _push.async = true
         _pop.async = true
         _check.async = true
@@ -172,7 +187,9 @@ class SolverProtocolModel private constructor(
         bindableChildren.add("deleteSolver" to _deleteSolver)
         bindableChildren.add("configure" to _configure)
         bindableChildren.add("assert" to _assert)
+        bindableChildren.add("bulkAssert" to _bulkAssert)
         bindableChildren.add("assertAndTrack" to _assertAndTrack)
+        bindableChildren.add("bulkAssertAndTrack" to _bulkAssertAndTrack)
         bindableChildren.add("push" to _push)
         bindableChildren.add("pop" to _pop)
         bindableChildren.add("check" to _check)
@@ -190,7 +207,9 @@ 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<BulkAssertParams, Unit>(BulkAssertParams, FrameworkMarshallers.Void),
         RdCall<AssertParams, Unit>(AssertParams, FrameworkMarshallers.Void),
+        RdCall<BulkAssertParams, Unit>(BulkAssertParams, FrameworkMarshallers.Void),
         RdCall<Unit, Unit>(FrameworkMarshallers.Void, FrameworkMarshallers.Void),
         RdCall<PopParams, Unit>(PopParams, FrameworkMarshallers.Void),
         RdCall<CheckParams, CheckResult>(CheckParams, CheckResult),
@@ -211,7 +230,9 @@ class SolverProtocolModel private constructor(
             print("deleteSolver = "); _deleteSolver.print(printer); println()
             print("configure = "); _configure.print(printer); println()
             print("assert = "); _assert.print(printer); println()
+            print("bulkAssert = "); _bulkAssert.print(printer); println()
             print("assertAndTrack = "); _assertAndTrack.print(printer); println()
+            print("bulkAssertAndTrack = "); _bulkAssertAndTrack.print(printer); println()
             print("push = "); _push.print(printer); println()
             print("pop = "); _pop.print(printer); println()
             print("check = "); _check.print(printer); println()
@@ -230,7 +251,9 @@ class SolverProtocolModel private constructor(
             _deleteSolver.deepClonePolymorphic(),
             _configure.deepClonePolymorphic(),
             _assert.deepClonePolymorphic(),
+            _bulkAssert.deepClonePolymorphic(),
             _assertAndTrack.deepClonePolymorphic(),
+            _bulkAssertAndTrack.deepClonePolymorphic(),
             _push.deepClonePolymorphic(),
             _pop.deepClonePolymorphic(),
             _check.deepClonePolymorphic(),
@@ -305,7 +328,64 @@ data class AssertParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:55]
+ * #### Generated from [SolverProtocolModel.kt:51]
+ */
+data class BulkAssertParams (
+    val expressions: List<io.ksmt.KAst>
+) : IPrintable {
+    //companion
+    
+    companion object : IMarshaller<BulkAssertParams> {
+        override val _type: KClass<BulkAssertParams> = BulkAssertParams::class
+        
+        @Suppress("UNCHECKED_CAST")
+        override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): BulkAssertParams  {
+            val expressions = buffer.readList { (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller<io.ksmt.KAst>).read(ctx, buffer) }
+            return BulkAssertParams(expressions)
+        }
+        
+        override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: BulkAssertParams)  {
+            buffer.writeList(value.expressions) { v -> (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller<io.ksmt.KAst>).write(ctx,buffer, v) }
+        }
+        
+        
+    }
+    //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 BulkAssertParams
+        
+        if (expressions != other.expressions) return false
+        
+        return true
+    }
+    //hash code trait
+    override fun hashCode(): Int  {
+        var __r = 0
+        __r = __r*31 + expressions.hashCode()
+        return __r
+    }
+    //pretty print
+    override fun print(printer: PrettyPrinter)  {
+        printer.println("BulkAssertParams (")
+        printer.indent {
+            print("expressions = "); expressions.print(printer); println()
+        }
+        printer.print(")")
+    }
+    //deepClone
+    //contexts
+}
+
+
+/**
+ * #### Generated from [SolverProtocolModel.kt:59]
  */
 data class CheckParams (
     val timeout: Long
@@ -362,7 +442,7 @@ data class CheckParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:59]
+ * #### Generated from [SolverProtocolModel.kt:63]
  */
 data class CheckResult (
     val status: io.ksmt.solver.KSolverStatus
@@ -419,7 +499,7 @@ data class CheckResult (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:63]
+ * #### Generated from [SolverProtocolModel.kt:67]
  */
 data class CheckWithAssumptionsParams (
     val assumptions: List<io.ksmt.KAst>,
@@ -587,7 +667,7 @@ data class CreateSolverParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:82]
+ * #### Generated from [SolverProtocolModel.kt:86]
  */
 data class ModelEntry (
     val decl: io.ksmt.KAst,
@@ -662,7 +742,7 @@ data class ModelEntry (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:76]
+ * #### Generated from [SolverProtocolModel.kt:80]
  */
 data class ModelFuncInterpEntry (
     val hasVars: Boolean,
@@ -731,7 +811,7 @@ data class ModelFuncInterpEntry (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:94]
+ * #### Generated from [SolverProtocolModel.kt:98]
  */
 data class ModelResult (
     val declarations: List<io.ksmt.KAst>,
@@ -800,7 +880,7 @@ data class ModelResult (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:89]
+ * #### Generated from [SolverProtocolModel.kt:93]
  */
 data class ModelUninterpretedSortUniverse (
     val sort: io.ksmt.KAst,
@@ -863,7 +943,7 @@ data class ModelUninterpretedSortUniverse (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:51]
+ * #### Generated from [SolverProtocolModel.kt:55]
  */
 data class PopParams (
     val levels: UInt
@@ -920,7 +1000,7 @@ data class PopParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:72]
+ * #### Generated from [SolverProtocolModel.kt:76]
  */
 data class ReasonUnknownResult (
     val reasonUnknown: String
@@ -1063,7 +1143,7 @@ enum class SolverType {
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:68]
+ * #### Generated from [SolverProtocolModel.kt:72]
  */
 data class UnsatCoreResult (
     val core: List<io.ksmt.KAst>
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt
index 6728916ef..7287091de 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt
@@ -14,8 +14,12 @@ interface KAsyncSolver<Config : KSolverConfiguration> : KSolver<Config> {
 
     suspend fun assertAsync(expr: KExpr<KBoolSort>)
 
+    suspend fun assertAsync(exprs: List<KExpr<KBoolSort>>) = exprs.forEach { assertAsync(it) }
+
     suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>)
 
+    suspend fun assertAndTrackAsync(exprs: List<KExpr<KBoolSort>>) = exprs.forEach { assertAndTrackAsync(it) }
+
     suspend fun pushAsync()
 
     suspend fun popAsync(n: UInt)
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt
index 7b3c8810e..161a5b1ef 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt
@@ -106,10 +106,18 @@ class KPortfolioSolver(
         assertAsync(expr)
     }
 
+    override fun assert(exprs: List<KExpr<KBoolSort>>) = runBlocking {
+        assertAsync(exprs)
+    }
+
     override fun assertAndTrack(expr: KExpr<KBoolSort>) = runBlocking {
         assertAndTrackAsync(expr)
     }
 
+    override fun assertAndTrack(exprs: List<KExpr<KBoolSort>>) = runBlocking {
+        assertAndTrackAsync(exprs)
+    }
+
     override fun push() = runBlocking {
         pushAsync()
     }
@@ -153,10 +161,18 @@ class KPortfolioSolver(
         assertAsync(expr)
     }
 
+    override suspend fun assertAsync(exprs: List<KExpr<KBoolSort>>) = solverOperation {
+        assertAsync(exprs)
+    }
+
     override suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>) = solverOperation {
         assertAndTrackAsync(expr)
     }
 
+    override suspend fun assertAndTrackAsync(exprs: List<KExpr<KBoolSort>>) = solverOperation {
+        assertAndTrackAsync(exprs)
+    }
+
     override suspend fun pushAsync() = solverOperation {
         pushAsync()
     }
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt
index 418a47505..e77ee03f7 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt
@@ -101,18 +101,47 @@ class KSolverRunner<Config : KSolverConfiguration>(
         }
     }
 
-    override suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>) = assertAndTrack(expr) { e ->
-        ensureInitializedAndExecuteAsync(onException = {}) {
-            assertAndTrackAsync(e)
+    override suspend fun assertAsync(exprs: List<KExpr<KBoolSort>>) =
+        bulkAssert(exprs) { e ->
+            ensureInitializedAndExecuteAsync(onException = {}) {
+                bulkAssertAsync(e)
+            }
         }
-    }
 
-    override fun assertAndTrack(expr: KExpr<KBoolSort>) = assertAndTrack(expr) { e ->
-        ensureInitializedAndExecuteSync(onException = {}) {
-            assertAndTrackSync(e)
+    override fun assert(exprs: List<KExpr<KBoolSort>>) =
+        bulkAssert(exprs) { e ->
+            ensureInitializedAndExecuteSync(onException = {}) {
+                bulkAssertSync(e)
+            }
+        }
+
+    private inline fun bulkAssert(
+        exprs: List<KExpr<KBoolSort>>,
+        execute: (List<KExpr<KBoolSort>>) -> Unit
+    ) {
+        ctx.ensureContextMatch(exprs)
+
+        try {
+            execute(exprs)
+        } finally {
+            exprs.forEach { solverState.assert(it) }
         }
     }
 
+    override suspend fun assertAndTrackAsync(expr: KExpr<KBoolSort>) =
+        assertAndTrack(expr) { e ->
+            ensureInitializedAndExecuteAsync(onException = {}) {
+                assertAndTrackAsync(e)
+            }
+        }
+
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) =
+        assertAndTrack(expr) { e ->
+            ensureInitializedAndExecuteSync(onException = {}) {
+                assertAndTrackSync(e)
+            }
+        }
+
     private inline fun assertAndTrack(
         expr: KExpr<KBoolSort>,
         execute: (KExpr<KBoolSort>) -> Unit
@@ -126,6 +155,33 @@ class KSolverRunner<Config : KSolverConfiguration>(
         }
     }
 
+    override suspend fun assertAndTrackAsync(exprs: List<KExpr<KBoolSort>>) =
+        bulkAssertAndTrack(exprs) { e ->
+            ensureInitializedAndExecuteAsync(onException = {}) {
+                bulkAssertAndTrackAsync(e)
+            }
+        }
+
+    override fun assertAndTrack(exprs: List<KExpr<KBoolSort>>) =
+        bulkAssertAndTrack(exprs) { e ->
+            ensureInitializedAndExecuteSync(onException = {}) {
+                bulkAssertAndTrackSync(e)
+            }
+        }
+
+    private inline fun bulkAssertAndTrack(
+        exprs: List<KExpr<KBoolSort>>,
+        execute: (List<KExpr<KBoolSort>>) -> Unit
+    ) {
+        ctx.ensureContextMatch(exprs)
+
+        try {
+            execute(exprs)
+        } finally {
+            exprs.forEach { solverState.assertAndTrack(it) }
+        }
+    }
+
     override suspend fun pushAsync() = push {
         executeIfInitialized(onException = {}) {
             pushAsync()
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt
index d24eb5383..328cc9cbf 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt
@@ -16,6 +16,7 @@ import io.ksmt.expr.KExpr
 import io.ksmt.expr.KUninterpretedSortValue
 import io.ksmt.runner.core.KsmtWorkerSession
 import io.ksmt.runner.generated.models.AssertParams
+import io.ksmt.runner.generated.models.BulkAssertParams
 import io.ksmt.runner.generated.models.CheckParams
 import io.ksmt.runner.generated.models.CheckResult
 import io.ksmt.runner.generated.models.CheckWithAssumptionsParams
@@ -92,6 +93,25 @@ class KSolverRunnerExecutor(
         query(AssertParams(expr))
     }
 
+    fun bulkAssertSync(exprs: List<KExpr<KBoolSort>>) = bulkAssert(exprs) { params ->
+        queryWithTimeoutAndExceptionHandlingSync {
+            bulkAssert.querySync(params)
+        }
+    }
+
+    suspend fun bulkAssertAsync(exprs: List<KExpr<KBoolSort>>) = bulkAssert(exprs) { params ->
+        queryWithTimeoutAndExceptionHandlingAsync {
+            bulkAssert.queryAsync(params)
+        }
+    }
+
+    private inline fun bulkAssert(exprs: List<KExpr<KBoolSort>>, query: (BulkAssertParams) -> Unit) {
+        if (exprs.isEmpty()) return
+
+        ensureActive()
+        query(BulkAssertParams(exprs))
+    }
+
     fun assertAndTrackSync(expr: KExpr<KBoolSort>) = assertAndTrack(expr) { params ->
         queryWithTimeoutAndExceptionHandlingSync {
             assertAndTrack.querySync(params)
@@ -109,6 +129,25 @@ class KSolverRunnerExecutor(
         query(AssertParams(expr))
     }
 
+    fun bulkAssertAndTrackSync(exprs: List<KExpr<KBoolSort>>) = bulkAssertAndTrack(exprs) { params ->
+        queryWithTimeoutAndExceptionHandlingSync {
+            bulkAssertAndTrack.querySync(params)
+        }
+    }
+
+    suspend fun bulkAssertAndTrackAsync(exprs: List<KExpr<KBoolSort>>) = bulkAssertAndTrack(exprs) { params ->
+        queryWithTimeoutAndExceptionHandlingAsync {
+            bulkAssertAndTrack.queryAsync(params)
+        }
+    }
+
+    private inline fun bulkAssertAndTrack(exprs: List<KExpr<KBoolSort>>, query: (BulkAssertParams) -> Unit) {
+        if (exprs.isEmpty()) return
+
+        ensureActive()
+        query(BulkAssertParams(exprs))
+    }
+
     fun pushSync() = push {
         queryWithTimeoutAndExceptionHandlingSync {
             push.querySync(Unit)
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt
index 5afa0d518..23ad6262a 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt
@@ -18,21 +18,22 @@ import java.util.concurrent.ConcurrentLinkedQueue
  * We don't consider last check-sat result as a solver state.
  * */
 class KSolverState {
-    private sealed interface AssertFrame
-    private data class ExprAssertFrame(val expr: KExpr<KBoolSort>) : AssertFrame
-    private data class AssertAndTrackFrame(val expr: KExpr<KBoolSort>) : AssertFrame
+    private class AssertionFrame(
+        val asserted: ConcurrentLinkedQueue<KExpr<KBoolSort>> = ConcurrentLinkedQueue(),
+        val tracked: ConcurrentLinkedQueue<KExpr<KBoolSort>> = ConcurrentLinkedQueue(),
+    )
 
     private val configuration = ConcurrentLinkedQueue<SolverConfigurationParam>()
 
     /**
      * Asserted expressions.
-     * Each nested queue contains expressions of the
+     * Each nested assertion frame contains expressions of the
      * corresponding assertion level.
      * */
-    private val assertFrames = ConcurrentLinkedDeque<ConcurrentLinkedQueue<AssertFrame>>()
+    private val assertFrames = ConcurrentLinkedDeque<AssertionFrame>()
 
     init {
-        assertFrames.addLast(ConcurrentLinkedQueue())
+        assertFrames.addLast(AssertionFrame())
     }
 
     fun configure(config: List<SolverConfigurationParam>) {
@@ -40,15 +41,15 @@ class KSolverState {
     }
 
     fun assert(expr: KExpr<KBoolSort>) {
-        assertFrames.last.add(ExprAssertFrame(expr))
+        assertFrames.last.asserted.add(expr)
     }
 
     fun assertAndTrack(expr: KExpr<KBoolSort>) {
-        assertFrames.last.add(AssertAndTrackFrame(expr))
+        assertFrames.last.tracked.add(expr)
     }
 
     fun push() {
-        assertFrames.addLast(ConcurrentLinkedQueue())
+        assertFrames.addLast(AssertionFrame())
     }
 
     fun pop(n: UInt) {
@@ -60,15 +61,15 @@ class KSolverState {
     suspend fun applyAsync(executor: KSolverRunnerExecutor) = replayState(
         configureSolver = { executor.configureAsync(it) },
         pushScope = { executor.pushAsync() },
-        assertExpr = { executor.assertAsync(it) },
-        assertExprAndTrack = { expr -> executor.assertAndTrackAsync(expr) }
+        assertExprs = { executor.bulkAssertAsync(it) },
+        assertExprsAndTrack = { expr -> executor.bulkAssertAndTrackAsync(expr) }
     )
 
     fun applySync(executor: KSolverRunnerExecutor) = replayState(
         configureSolver = { executor.configureSync(it) },
         pushScope = { executor.pushSync() },
-        assertExpr = { executor.assertSync(it) },
-        assertExprAndTrack = { expr -> executor.assertAndTrackSync(expr) }
+        assertExprs = { executor.bulkAssertSync(it) },
+        assertExprsAndTrack = { expr -> executor.bulkAssertAndTrackSync(expr) }
     )
 
     /**
@@ -78,8 +79,8 @@ class KSolverState {
     private inline fun replayState(
         configureSolver: (List<SolverConfigurationParam>) -> Unit,
         pushScope: () -> Unit,
-        assertExpr: (KExpr<KBoolSort>) -> Unit,
-        assertExprAndTrack: (KExpr<KBoolSort>) -> Unit
+        assertExprs: (List<KExpr<KBoolSort>>) -> Unit,
+        assertExprsAndTrack: (List<KExpr<KBoolSort>>) -> Unit
     ) {
         if (configuration.isNotEmpty()) {
             configureSolver(configuration.toList())
@@ -93,12 +94,8 @@ class KSolverState {
             }
             firstFrame = false
 
-            for (assertion in frame) {
-                when (assertion) {
-                    is ExprAssertFrame -> assertExpr(assertion.expr)
-                    is AssertAndTrackFrame -> assertExprAndTrack(assertion.expr)
-                }
-            }
+            assertExprs(frame.asserted.toList())
+            assertExprsAndTrack(frame.tracked.toList())
         }
     }
 }
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt
index b5f6125eb..2506d578a 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt
@@ -85,10 +85,18 @@ class KSolverWorkerProcess : ChildProcessBase<SolverProtocolModel>() {
             @Suppress("UNCHECKED_CAST")
             solver.assert(params.expression as KExpr<KBoolSort>)
         }
+        bulkAssert.measureExecutionForTermination { params ->
+            @Suppress("UNCHECKED_CAST")
+            solver.assert(params.expressions as List<KExpr<KBoolSort>>)
+        }
         assertAndTrack.measureExecutionForTermination { params ->
             @Suppress("UNCHECKED_CAST")
             solver.assertAndTrack(params.expression as KExpr<KBoolSort>)
         }
+        bulkAssertAndTrack.measureExecutionForTermination { params ->
+            @Suppress("UNCHECKED_CAST")
+            solver.assertAndTrack(params.expressions as List<KExpr<KBoolSort>>)
+        }
         push.measureExecutionForTermination {
             solver.push()
         }
diff --git a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt
index d434b1fdc..f6c1dfa79 100644
--- a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt
+++ b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt
@@ -48,6 +48,10 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
         field("expression", kastType)
     }
 
+    private val bulkAssertParams = structdef {
+        field("expressions", immutableList(kastType))
+    }
+
     private val popParams = structdef {
         field("levels", PredefinedType.uint)
     }
@@ -114,10 +118,18 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
             async
             documentation = "Assert expression"
         }
+        call("bulkAssert", bulkAssertParams, PredefinedType.void).apply {
+            async
+            documentation = "Assert multiple expressions"
+        }
         call("assertAndTrack", assertParams, PredefinedType.void).apply {
             async
             documentation = "Assert and track expression"
         }
+        call("bulkAssertAndTrack", bulkAssertParams, PredefinedType.void).apply {
+            async
+            documentation = "Assert and track multiple expressions"
+        }
         call("push", PredefinedType.void, PredefinedType.void).apply {
             async
             documentation = "Solver push"
diff --git a/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt b/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt
index f7c7625d1..92083faf8 100644
--- a/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt
+++ b/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt
@@ -153,6 +153,29 @@ class SolverRunnerTest {
         assertEquals(model1, model3)
     }
 
+    @Test
+    fun testBulkAssert(): Unit = with(context) {
+        val a = boolSort.mkConst("a")
+        val b = boolSort.mkConst("b")
+        val c = boolSort.mkConst("c")
+
+        val e1 = (a and b) or c
+        val e2 = !(a and b)
+        val e3 = !c
+
+        solver.push()
+        solver.assert(listOf(e1, e2, e3))
+        assertEquals(KSolverStatus.UNSAT, solver.check())
+        solver.pop()
+
+        solver.push()
+        solver.assertAndTrack(listOf(e1, e2, e3))
+        assertEquals(KSolverStatus.UNSAT, solver.check())
+
+        val core = solver.unsatCore()
+        assertTrue(core.isNotEmpty())
+    }
+
     @Test
     fun testSolverInstanceCreation(): Unit = with(context){
         SolverType.Z3.createInstance(this)