diff --git a/README.md b/README.md
index d74fb022c..5ca25c1e3 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.25)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.26)
 [![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.25")
+implementation("io.ksmt:ksmt-core:0.5.26")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.25")
+implementation("io.ksmt:ksmt-z3:0.5.26")
 ```
 
 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 2a5b6b211..a031bda9d 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.25"
+version = "0.5.26"
 
 repositories {
     mavenCentral()
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 81d46341f..a31b3ef91 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.25")    
+    implementation("io.ksmt:ksmt-core:0.5.26")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.25")
+    implementation("io.ksmt:ksmt-z3:0.5.26")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.25")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.26")
 }
 ```
 
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index 625c84973..8489355d6 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.25")
+    implementation("io.ksmt:ksmt-core:0.5.26")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.25")
+    implementation("io.ksmt:ksmt-z3:0.5.26")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.25")
+    implementation("io.ksmt:ksmt-runner:0.5.26")
 }
 
 java {
diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt
index a40ee8a60..3b6edfc6e 100644
--- a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt
+++ b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt
@@ -2,7 +2,13 @@ package io.ksmt.solver.bitwuzla
 
 import io.ksmt.solver.KSolverConfiguration
 import io.ksmt.solver.KSolverUniversalConfigurationBuilder
+import io.ksmt.solver.KSolverUnsupportedFeatureException
 import io.ksmt.solver.KSolverUnsupportedParameterException
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
 import org.ksmt.solver.bitwuzla.bindings.Bitwuzla
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption
 import org.ksmt.solver.bitwuzla.bindings.Native
@@ -42,11 +48,23 @@ class KBitwuzlaSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuz
     override fun setBitwuzlaOption(option: BitwuzlaOption, value: String) {
         Native.bitwuzlaSetOptionStr(bitwuzla, option, value)
     }
+
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        if (theories.isNullOrEmpty()) return
+
+        if (setOf(LIA, LRA, NIA, NRA).intersect(theories).isNotEmpty()) {
+            throw KSolverUnsupportedFeatureException("Unsupported theories $theories")
+        }
+    }
 }
 
 class KBitwuzlaSolverUniversalConfiguration(
     private val builder: KSolverUniversalConfigurationBuilder
 ) : KBitwuzlaSolverConfiguration {
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        builder.buildOptimizeForTheories(theories, quantifiersAllowed)
+    }
+
     override fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) {
         builder.buildIntParameter(option.name, value)
     }
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverConfiguration.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverConfiguration.kt
index cb087e124..00f5d76a5 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverConfiguration.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverConfiguration.kt
@@ -1,8 +1,23 @@
 package io.ksmt.solver
 
+@Suppress("OVERLOADS_INTERFACE", "INAPPLICABLE_JVM_NAME")
 interface KSolverConfiguration {
     fun setBoolParameter(param: String, value: Boolean)
     fun setIntParameter(param: String, value: Int)
     fun setStringParameter(param: String, value: String)
     fun setDoubleParameter(param: String, value: Double)
+
+    /**
+     * Specialize the solver to work with the provided theories.
+     *
+     * [theories] a set of theories.
+     * If the provided theories are null, the solver is specialized to work with all supported theories.
+     * If the provided theory set is empty, the solver is configured to work only with propositional formulas.
+     *
+     * [quantifiersAllowed] allows or disallows formulas with quantifiers.
+     * If quantifiers are not allowed, the solver is specialized to work with Quantifier Free formulas.
+     * * */
+    @JvmOverloads
+    @JvmName("optimizeForTheories")
+    fun optimizeForTheories(theories: Set<KTheory>? = null, quantifiersAllowed: Boolean = false)
 }
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverUniversalConfigurationBuilder.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverUniversalConfigurationBuilder.kt
index ba3640157..db8c69c03 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverUniversalConfigurationBuilder.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverUniversalConfigurationBuilder.kt
@@ -5,4 +5,5 @@ interface KSolverUniversalConfigurationBuilder {
     fun buildIntParameter(param: String, value: Int)
     fun buildStringParameter(param: String, value: String)
     fun buildDoubleParameter(param: String, value: Double)
+    fun buildOptimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean)
 }
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt
new file mode 100644
index 000000000..bee24e454
--- /dev/null
+++ b/ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt
@@ -0,0 +1,79 @@
+package io.ksmt.solver
+
+import io.ksmt.solver.KTheory.Array
+import io.ksmt.solver.KTheory.BV
+import io.ksmt.solver.KTheory.FP
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.UF
+
+/**
+ * SMT theory
+ * */
+enum class KTheory {
+    UF, BV, FP, Array,
+    LIA, NIA, LRA, NRA
+}
+
+@Suppress("ComplexMethod", "ComplexCondition")
+fun Set<KTheory>?.smtLib2String(quantifiersAllowed: Boolean = false): String = buildString {
+    val theories = this@smtLib2String
+
+    if (!quantifiersAllowed) {
+        append("QF_")
+    }
+
+    if (theories == null) {
+        append("ALL")
+        return@buildString
+    }
+
+    if (theories.isEmpty()) {
+        append("SAT")
+        return@buildString
+    }
+
+    if (Array in theories) {
+        if (theories.size == 1) {
+            append("AX")
+            return@buildString
+        }
+        append("A")
+    }
+
+    if (UF in theories) {
+        append("UF")
+    }
+
+    if (BV in theories) {
+        append("BV")
+    }
+
+    if (FP in theories) {
+        append("FP")
+    }
+
+    if (LIA in theories || NIA in theories || LRA in theories || NRA in theories) {
+        val hasNonLinear = NIA in theories || NRA in theories
+        val hasReal = LRA in theories || NRA in theories
+        val hasInt = LIA in theories || NIA in theories
+
+        if (hasNonLinear) {
+            append("N")
+        } else {
+            append("L")
+        }
+
+        if (hasInt) {
+            append("I")
+        }
+
+        if (hasReal) {
+            append("R")
+        }
+
+        append("A")
+    }
+}
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt
new file mode 100644
index 000000000..eeb205f10
--- /dev/null
+++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt
@@ -0,0 +1,133 @@
+package io.ksmt.utils
+
+import io.ksmt.KContext
+import io.ksmt.expr.KDivArithExpr
+import io.ksmt.expr.KExistentialQuantifier
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KFunctionApp
+import io.ksmt.expr.KMulArithExpr
+import io.ksmt.expr.KPowerArithExpr
+import io.ksmt.expr.KUniversalQuantifier
+import io.ksmt.expr.transformer.KNonRecursiveTransformer
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.Array
+import io.ksmt.solver.KTheory.BV
+import io.ksmt.solver.KTheory.FP
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.UF
+import io.ksmt.sort.KArithSort
+import io.ksmt.sort.KArray2Sort
+import io.ksmt.sort.KArray3Sort
+import io.ksmt.sort.KArrayNSort
+import io.ksmt.sort.KArraySort
+import io.ksmt.sort.KBoolSort
+import io.ksmt.sort.KBvSort
+import io.ksmt.sort.KFpRoundingModeSort
+import io.ksmt.sort.KFpSort
+import io.ksmt.sort.KIntSort
+import io.ksmt.sort.KRealSort
+import io.ksmt.sort.KSort
+import io.ksmt.sort.KSortVisitor
+import io.ksmt.sort.KUninterpretedSort
+
+class KExprTheoryRequirement(ctx: KContext) : KNonRecursiveTransformer(ctx) {
+    val usedTheories = hashSetOf<KTheory>()
+
+    var hasQuantifiers: Boolean = false
+        private set
+
+    private val sortRequirementCollector = Sort2TheoryRequirement()
+
+    override fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T> {
+        expr.sort.accept(sortRequirementCollector)
+        return super.transformExpr(expr)
+    }
+
+    override fun <T : KSort> transform(expr: KFunctionApp<T>): KExpr<T> {
+        if (expr.args.isNotEmpty()) {
+            usedTheories += UF
+        }
+        return super.transform(expr)
+    }
+
+    override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> {
+        hasQuantifiers = true
+        return super.transform(expr)
+    }
+
+    override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> {
+        hasQuantifiers = true
+        return super.transform(expr)
+    }
+
+    override fun <T : KArithSort> transform(expr: KMulArithExpr<T>): KExpr<T> {
+        usedTheories += if (expr.sort is KIntSort) NIA else NRA
+        return super.transform(expr)
+    }
+
+    override fun <T : KArithSort> transform(expr: KDivArithExpr<T>): KExpr<T> {
+        usedTheories += if (expr.sort is KIntSort) NIA else NRA
+        return super.transform(expr)
+    }
+
+    override fun <T : KArithSort> transform(expr: KPowerArithExpr<T>): KExpr<T> {
+        usedTheories += if (expr.sort is KIntSort) NIA else NRA
+        return super.transform(expr)
+    }
+
+    private inner class Sort2TheoryRequirement : KSortVisitor<Unit> {
+        override fun visit(sort: KBoolSort) {
+        }
+
+        override fun visit(sort: KIntSort) {
+            usedTheories += LIA
+        }
+
+        override fun visit(sort: KRealSort) {
+            usedTheories += LRA
+        }
+
+        override fun <S : KBvSort> visit(sort: S) {
+            usedTheories += BV
+        }
+
+        override fun <S : KFpSort> visit(sort: S) {
+            usedTheories += FP
+        }
+
+        override fun <D : KSort, R : KSort> visit(sort: KArraySort<D, R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun <D0 : KSort, D1 : KSort, R : KSort> visit(sort: KArray2Sort<D0, D1, R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> visit(sort: KArray3Sort<D0, D1, D2, R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun <R : KSort> visit(sort: KArrayNSort<R>) {
+            usedTheories += Array
+            sort.range.accept(this)
+            sort.domainSorts.forEach { it.accept(this) }
+        }
+
+        override fun visit(sort: KFpRoundingModeSort) {
+            usedTheories += FP
+        }
+
+        override fun visit(sort: KUninterpretedSort) {
+            usedTheories += UF
+        }
+    }
+}
diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt
index ac7d8dace..10d3b4f01 100644
--- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt
+++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt
@@ -3,7 +3,6 @@ package io.ksmt.solver.cvc5
 import io.github.cvc5.CVC5ApiException
 import io.github.cvc5.Result
 import io.github.cvc5.Solver
-import io.github.cvc5.TermManager
 import io.ksmt.KContext
 import io.ksmt.expr.KExpr
 import io.ksmt.solver.KModel
@@ -18,9 +17,13 @@ import kotlin.time.DurationUnit
 
 open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfiguration> {
     private val termManager = KCvc5TermManager()
-    private val solver = termManager.builder { Solver(this) }
     private val cvc5Ctx = KCvc5Context(termManager, ctx)
 
+    private var solverLazyConfiguration: KCvc5SolverLazyConfiguration? = null
+    private var solverInitialized: Boolean = false
+    private val solver by lazy { initSolver() }
+    fun nativeSolver(): Solver = solver
+
     private val exprInternalizer by lazy { createExprInternalizer(cvc5Ctx) }
 
     private val currentScope: UInt
@@ -36,21 +39,37 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
     private var cvc5CurrentLevelTrackedAssertions = KCvc5TermMap<KExpr<KBoolSort>>()
     private val cvc5TrackedAssertions = mutableListOf(cvc5CurrentLevelTrackedAssertions)
 
-    init {
+    private fun initSolver(): Solver = cvc5Try {
+        val solver = termManager.builder { Solver(this) }
+
+        solverInitialized = true
+        solverLazyConfiguration?.configure(solver)
+        solverLazyConfiguration = null
+
         solver.setOption("produce-models", "true")
         solver.setOption("produce-unsat-cores", "true")
+
         /**
          * Allow floating-point sorts of all sizes, rather than
          * only Float32 (8/24) or Float64 (11/53) (experimental in cvc5 1.0.2)
          */
         solver.setOption("fp-exp", "true")
+
+        return solver
     }
 
     open fun createExprInternalizer(cvc5Ctx: KCvc5Context): KCvc5ExprInternalizer =
         KCvc5ExprInternalizer(cvc5Ctx, solver)
 
     override fun configure(configurator: KCvc5SolverConfiguration.() -> Unit) {
-        KCvc5SolverConfigurationImpl(solver).configurator()
+        if (!solverInitialized) {
+            val config = solverLazyConfiguration
+                ?: KCvc5SolverLazyConfiguration().also { solverLazyConfiguration = it }
+
+            config.configurator()
+        } else {
+            KCvc5SolverOptionsConfiguration(solver).configurator()
+        }
     }
 
     override fun assert(expr: KExpr<KBoolSort>) = cvc5Try {
diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SolverConfiguration.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SolverConfiguration.kt
index 7ef58b0cd..48c841d92 100644
--- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SolverConfiguration.kt
+++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SolverConfiguration.kt
@@ -2,8 +2,11 @@ package io.ksmt.solver.cvc5
 
 import io.github.cvc5.Solver
 import io.ksmt.solver.KSolverConfiguration
+import io.ksmt.solver.KSolverException
 import io.ksmt.solver.KSolverUniversalConfigurationBuilder
 import io.ksmt.solver.KSolverUnsupportedParameterException
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.smtLib2String
 
 interface KCvc5SolverConfiguration : KSolverConfiguration {
     fun setCvc5Option(option: String, value: String)
@@ -35,19 +38,49 @@ interface KCvc5SolverConfiguration : KSolverConfiguration {
     }
 }
 
-class KCvc5SolverConfigurationImpl(val solver: Solver) : KCvc5SolverConfiguration {
+class KCvc5SolverLazyConfiguration : KCvc5SolverConfiguration {
+    private var logicConfiguration: String? = null
+    private val options = mutableMapOf<String, String>()
+
+    override fun setCvc5Option(option: String, value: String) {
+        options[option] = value
+    }
+
+    override fun setCvc5Logic(value: String) {
+        logicConfiguration = value
+    }
+
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        logicConfiguration = theories.smtLib2String(quantifiersAllowed)
+    }
+
+    fun configure(solver: Solver) {
+        logicConfiguration?.let { solver.setLogic(it) }
+        options.forEach { (option, value) -> solver.setOption(option, value) }
+    }
+}
+
+class KCvc5SolverOptionsConfiguration(val solver: Solver) : KCvc5SolverConfiguration {
     override fun setCvc5Option(option: String, value: String) {
         solver.setOption(option, value)
     }
 
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        throw KSolverException("Solver logic already configured")
+    }
+
     override fun setCvc5Logic(value: String) {
-        solver.setLogic(value)
+        throw KSolverException("Solver logic already configured")
     }
 }
 
 class KCvc5SolverUniversalConfiguration(
     private val builder: KSolverUniversalConfigurationBuilder
 ) : KCvc5SolverConfiguration {
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        builder.buildOptimizeForTheories(theories, quantifiersAllowed)
+    }
+
     override fun setCvc5Option(option: String, value: String) {
         builder.buildStringParameter(option, value)
     }
diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/LogicTest.kt b/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/LogicTest.kt
new file mode 100644
index 000000000..dbc977c82
--- /dev/null
+++ b/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/LogicTest.kt
@@ -0,0 +1,49 @@
+package io.ksmt.solver.cvc5
+
+import io.ksmt.KContext
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.smtLib2String
+import kotlin.test.Test
+import kotlin.test.assertEquals
+
+class LogicTest {
+    private val ctx = KContext()
+    private val solver = KCvc5Solver(ctx)
+
+    @Test
+    fun testSetAllLogic() {
+        solver.configure {
+            optimizeForTheories(theories = null, quantifiersAllowed = false)
+        }
+
+        assertEquals("QF_ALL", solver.nativeSolver().getLogic())
+    }
+
+    @Test
+    fun testSetPropLogic() {
+        solver.configure {
+            optimizeForTheories(theories = emptySet(), quantifiersAllowed = false)
+        }
+
+        assertEquals("QF_SAT", solver.nativeSolver().getLogic())
+    }
+
+    @Test
+    fun testSetSpecificLogic() {
+        solver.configure {
+            optimizeForTheories(theories = setOf(KTheory.BV, KTheory.UF, KTheory.Array), quantifiersAllowed = false)
+        }
+
+        assertEquals("QF_AUFBV", solver.nativeSolver().getLogic())
+    }
+
+    @Test
+    fun testSetSupportedLogic() {
+        solver.configure {
+            optimizeForTheories(theories = KTheory.values().toSet(), quantifiersAllowed = false)
+        }
+
+        val expected = KTheory.values().toSet().smtLib2String(quantifiersAllowed = false)
+        assertEquals(expected, solver.nativeSolver().getLogic())
+    }
+}
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 89b598d49..11f470fcd 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
@@ -20,7 +20,7 @@ import kotlin.jvm.JvmStatic
 class SolverProtocolModel private constructor(
     private val _initSolver: RdCall<CreateSolverParams, Unit>,
     private val _deleteSolver: RdCall<Unit, Unit>,
-    private val _configure: RdCall<List<SolverConfigurationParam>, Unit>,
+    private val _configure: RdCall<SolverConfiguration, Unit>,
     private val _assert: RdCall<AssertParams, Unit>,
     private val _bulkAssert: RdCall<BulkAssertParams, Unit>,
     private val _assertAndTrack: RdCall<AssertParams, Unit>,
@@ -41,6 +41,8 @@ class SolverProtocolModel private constructor(
         override fun registerSerializersCore(serializers: ISerializers)  {
             serializers.register(CreateSolverParams)
             serializers.register(SolverConfigurationParam)
+            serializers.register(SolverConfigurationTheories)
+            serializers.register(SolverConfiguration)
             serializers.register(AssertParams)
             serializers.register(BulkAssertParams)
             serializers.register(PopParams)
@@ -78,9 +80,8 @@ class SolverProtocolModel private constructor(
             }
         }
         
-        private val __SolverConfigurationParamListSerializer = SolverConfigurationParam.list()
         
-        const val serializationHash = 6588187342629653927L
+        const val serializationHash = 2069028780388633863L
         
     }
     override val serializersOwner: ISerializersOwner get() = SolverProtocolModel
@@ -101,7 +102,7 @@ class SolverProtocolModel private constructor(
     /**
      * Configure solver with parameters
      */
-    val configure: RdCall<List<SolverConfigurationParam>, Unit> get() = _configure
+    val configure: RdCall<SolverConfiguration, Unit> get() = _configure
     
     /**
      * Assert expression
@@ -205,7 +206,7 @@ class SolverProtocolModel private constructor(
     ) : this(
         RdCall<CreateSolverParams, Unit>(CreateSolverParams, FrameworkMarshallers.Void),
         RdCall<Unit, Unit>(FrameworkMarshallers.Void, FrameworkMarshallers.Void),
-        RdCall<List<SolverConfigurationParam>, Unit>(__SolverConfigurationParamListSerializer, FrameworkMarshallers.Void),
+        RdCall<SolverConfiguration, Unit>(SolverConfiguration, FrameworkMarshallers.Void),
         RdCall<AssertParams, Unit>(AssertParams, FrameworkMarshallers.Void),
         RdCall<BulkAssertParams, Unit>(BulkAssertParams, FrameworkMarshallers.Void),
         RdCall<AssertParams, Unit>(AssertParams, FrameworkMarshallers.Void),
@@ -271,7 +272,7 @@ val IProtocol.solverProtocolModel get() = getOrCreateExtension(SolverProtocolMod
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:47]
+ * #### Generated from [SolverProtocolModel.kt:57]
  */
 data class AssertParams (
     val expression: io.ksmt.KAst
@@ -328,7 +329,7 @@ data class AssertParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:51]
+ * #### Generated from [SolverProtocolModel.kt:61]
  */
 data class BulkAssertParams (
     val expressions: List<io.ksmt.KAst>
@@ -385,7 +386,7 @@ data class BulkAssertParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:59]
+ * #### Generated from [SolverProtocolModel.kt:69]
  */
 data class CheckParams (
     val timeout: Long
@@ -442,7 +443,7 @@ data class CheckParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:63]
+ * #### Generated from [SolverProtocolModel.kt:73]
  */
 data class CheckResult (
     val status: io.ksmt.solver.KSolverStatus
@@ -499,7 +500,7 @@ data class CheckResult (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:67]
+ * #### Generated from [SolverProtocolModel.kt:77]
  */
 data class CheckWithAssumptionsParams (
     val assumptions: List<io.ksmt.KAst>,
@@ -667,7 +668,7 @@ data class CreateSolverParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:86]
+ * #### Generated from [SolverProtocolModel.kt:96]
  */
 data class ModelEntry (
     val decl: io.ksmt.KAst,
@@ -742,7 +743,7 @@ data class ModelEntry (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:80]
+ * #### Generated from [SolverProtocolModel.kt:90]
  */
 data class ModelFuncInterpEntry (
     val hasVars: Boolean,
@@ -811,7 +812,7 @@ data class ModelFuncInterpEntry (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:98]
+ * #### Generated from [SolverProtocolModel.kt:108]
  */
 data class ModelResult (
     val declarations: List<io.ksmt.KAst>,
@@ -880,7 +881,7 @@ data class ModelResult (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:93]
+ * #### Generated from [SolverProtocolModel.kt:103]
  */
 data class ModelUninterpretedSortUniverse (
     val sort: io.ksmt.KAst,
@@ -943,7 +944,7 @@ data class ModelUninterpretedSortUniverse (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:55]
+ * #### Generated from [SolverProtocolModel.kt:65]
  */
 data class PopParams (
     val levels: UInt
@@ -1000,7 +1001,7 @@ data class PopParams (
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:76]
+ * #### Generated from [SolverProtocolModel.kt:86]
  */
 data class ReasonUnknownResult (
     val reasonUnknown: String
@@ -1056,6 +1057,69 @@ data class ReasonUnknownResult (
 }
 
 
+/**
+ * #### Generated from [SolverProtocolModel.kt:52]
+ */
+data class SolverConfiguration (
+    val params: List<SolverConfigurationParam>,
+    val theories: SolverConfigurationTheories?
+) : IPrintable {
+    //companion
+    
+    companion object : IMarshaller<SolverConfiguration> {
+        override val _type: KClass<SolverConfiguration> = SolverConfiguration::class
+        
+        @Suppress("UNCHECKED_CAST")
+        override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): SolverConfiguration  {
+            val params = buffer.readList { SolverConfigurationParam.read(ctx, buffer) }
+            val theories = buffer.readNullable { SolverConfigurationTheories.read(ctx, buffer) }
+            return SolverConfiguration(params, theories)
+        }
+        
+        override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: SolverConfiguration)  {
+            buffer.writeList(value.params) { v -> SolverConfigurationParam.write(ctx, buffer, v) }
+            buffer.writeNullable(value.theories) { SolverConfigurationTheories.write(ctx, buffer, it) }
+        }
+        
+        
+    }
+    //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 SolverConfiguration
+        
+        if (params != other.params) return false
+        if (theories != other.theories) return false
+        
+        return true
+    }
+    //hash code trait
+    override fun hashCode(): Int  {
+        var __r = 0
+        __r = __r*31 + params.hashCode()
+        __r = __r*31 + if (theories != null) theories.hashCode() else 0
+        return __r
+    }
+    //pretty print
+    override fun print(printer: PrettyPrinter)  {
+        printer.println("SolverConfiguration (")
+        printer.indent {
+            print("params = "); params.print(printer); println()
+            print("theories = "); theories.print(printer); println()
+        }
+        printer.print(")")
+    }
+    //deepClone
+    //contexts
+}
+
+
 /**
  * #### Generated from [SolverProtocolModel.kt:36]
  */
@@ -1125,6 +1189,69 @@ data class SolverConfigurationParam (
 }
 
 
+/**
+ * #### Generated from [SolverProtocolModel.kt:47]
+ */
+data class SolverConfigurationTheories (
+    val quantifiersAllowed: Boolean,
+    val theories: List<String>?
+) : IPrintable {
+    //companion
+    
+    companion object : IMarshaller<SolverConfigurationTheories> {
+        override val _type: KClass<SolverConfigurationTheories> = SolverConfigurationTheories::class
+        
+        @Suppress("UNCHECKED_CAST")
+        override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): SolverConfigurationTheories  {
+            val quantifiersAllowed = buffer.readBool()
+            val theories = buffer.readNullable { buffer.readList { buffer.readString() } }
+            return SolverConfigurationTheories(quantifiersAllowed, theories)
+        }
+        
+        override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: SolverConfigurationTheories)  {
+            buffer.writeBool(value.quantifiersAllowed)
+            buffer.writeNullable(value.theories) { buffer.writeList(it) { v -> buffer.writeString(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 SolverConfigurationTheories
+        
+        if (quantifiersAllowed != other.quantifiersAllowed) return false
+        if (theories != other.theories) return false
+        
+        return true
+    }
+    //hash code trait
+    override fun hashCode(): Int  {
+        var __r = 0
+        __r = __r*31 + quantifiersAllowed.hashCode()
+        __r = __r*31 + if (theories != null) theories.hashCode() else 0
+        return __r
+    }
+    //pretty print
+    override fun print(printer: PrettyPrinter)  {
+        printer.println("SolverConfigurationTheories (")
+        printer.indent {
+            print("quantifiersAllowed = "); quantifiersAllowed.print(printer); println()
+            print("theories = "); theories.print(printer); println()
+        }
+        printer.print(")")
+    }
+    //deepClone
+    //contexts
+}
+
+
 /**
  * #### Generated from [SolverProtocolModel.kt:21]
  */
@@ -1143,7 +1270,7 @@ enum class SolverType {
 
 
 /**
- * #### Generated from [SolverProtocolModel.kt:72]
+ * #### Generated from [SolverProtocolModel.kt:82]
  */
 data class UnsatCoreResult (
     val core: List<io.ksmt.KAst>
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 e77ee03f7..a469bc412 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
@@ -2,11 +2,10 @@ package io.ksmt.solver.runner
 
 import com.jetbrains.rd.util.AtomicReference
 import com.jetbrains.rd.util.threading.SpinWait
-import kotlinx.coroutines.sync.Mutex
 import io.ksmt.KContext
 import io.ksmt.expr.KExpr
 import io.ksmt.runner.generated.ConfigurationBuilder
-import io.ksmt.runner.generated.models.SolverConfigurationParam
+import io.ksmt.runner.generated.models.SolverConfiguration
 import io.ksmt.runner.generated.models.SolverType
 import io.ksmt.solver.KModel
 import io.ksmt.solver.KSolverConfiguration
@@ -15,6 +14,7 @@ import io.ksmt.solver.KSolverStatus
 import io.ksmt.solver.async.KAsyncSolver
 import io.ksmt.solver.runner.KSolverRunnerManager.CustomSolverInfo
 import io.ksmt.sort.KBoolSort
+import kotlinx.coroutines.sync.Mutex
 import java.util.concurrent.atomic.AtomicBoolean
 import kotlin.time.Duration
 
@@ -61,11 +61,14 @@ class KSolverRunner<Config : KSolverConfiguration>(
 
     private inline fun configure(
         configurator: Config.() -> Unit,
-        execute: (List<SolverConfigurationParam>) -> Unit
+        execute: (SolverConfiguration) -> Unit
     ) {
         val universalConfigurator = KSolverRunnerUniversalConfigurator()
         configurationBuilder(universalConfigurator).configurator()
-        val config = universalConfigurator.config
+        val config = SolverConfiguration(
+            params = universalConfigurator.config,
+            theories = universalConfigurator.theories
+        )
 
         try {
             execute(config)
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 328cc9cbf..343f74712 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
@@ -8,8 +8,6 @@ import com.jetbrains.rd.util.TimeoutException
 import com.jetbrains.rd.util.lifetime.Lifetime
 import com.jetbrains.rd.util.reactive.RdFault
 import com.jetbrains.rd.util.threading.SynchronousScheduler
-import kotlinx.coroutines.TimeoutCancellationException
-import kotlinx.coroutines.withTimeout
 import io.ksmt.KContext
 import io.ksmt.decl.KDecl
 import io.ksmt.expr.KExpr
@@ -22,55 +20,57 @@ import io.ksmt.runner.generated.models.CheckResult
 import io.ksmt.runner.generated.models.CheckWithAssumptionsParams
 import io.ksmt.runner.generated.models.ContextSimplificationMode
 import io.ksmt.runner.generated.models.CreateSolverParams
-import io.ksmt.runner.generated.models.ModelResult
 import io.ksmt.runner.generated.models.ModelEntry
 import io.ksmt.runner.generated.models.ModelFuncInterpEntry
+import io.ksmt.runner.generated.models.ModelResult
 import io.ksmt.runner.generated.models.PopParams
 import io.ksmt.runner.generated.models.ReasonUnknownResult
-import io.ksmt.runner.generated.models.SolverConfigurationParam
+import io.ksmt.runner.generated.models.SolverConfiguration
 import io.ksmt.runner.generated.models.SolverProtocolModel
 import io.ksmt.runner.generated.models.SolverType
 import io.ksmt.runner.generated.models.UnsatCoreResult
+import io.ksmt.solver.KModel
+import io.ksmt.solver.KSolverException
+import io.ksmt.solver.KSolverStatus
+import io.ksmt.solver.KSolverUnsupportedFeatureException
+import io.ksmt.solver.KSolverUnsupportedParameterException
 import io.ksmt.solver.model.KFuncInterp
 import io.ksmt.solver.model.KFuncInterpEntry
 import io.ksmt.solver.model.KFuncInterpEntryVarsFree
 import io.ksmt.solver.model.KFuncInterpEntryWithVars
 import io.ksmt.solver.model.KFuncInterpVarsFree
 import io.ksmt.solver.model.KFuncInterpWithVars
-import io.ksmt.solver.KModel
-import io.ksmt.solver.KSolverException
-import io.ksmt.solver.KSolverStatus
-import io.ksmt.solver.KSolverUnsupportedFeatureException
-import io.ksmt.solver.KSolverUnsupportedParameterException
 import io.ksmt.solver.model.KModelImpl
 import io.ksmt.solver.runner.KSolverRunnerManager.CustomSolverInfo
 import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KUninterpretedSort
+import io.ksmt.utils.uncheckedCast
+import kotlinx.coroutines.TimeoutCancellationException
+import kotlinx.coroutines.withTimeout
 import java.util.concurrent.CompletableFuture
 import java.util.concurrent.TimeUnit
-import io.ksmt.utils.uncheckedCast
 import kotlin.time.Duration
 
 class KSolverRunnerExecutor(
     private val hardTimeout: Duration,
     private val worker: KsmtWorkerSession<SolverProtocolModel>,
 ) {
-    fun configureSync(config: List<SolverConfigurationParam>) = configure(config) { cfg ->
+    fun configureSync(config: SolverConfiguration) = configure(config) { cfg ->
         queryWithTimeoutAndExceptionHandlingSync {
             configure.querySync(cfg)
         }
     }
 
-    suspend fun configureAsync(config: List<SolverConfigurationParam>) = configure(config) { cfg ->
+    suspend fun configureAsync(config: SolverConfiguration) = configure(config) { cfg ->
         queryWithTimeoutAndExceptionHandlingAsync {
             configure.queryAsync(cfg)
         }
     }
 
     private inline fun configure(
-        config: List<SolverConfigurationParam>,
-        query: (List<SolverConfigurationParam>) -> Unit
+        config: SolverConfiguration,
+        query: (SolverConfiguration) -> Unit
     ) {
         ensureActive()
         query(config)
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerUniversalConfigurator.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerUniversalConfigurator.kt
index d18b0837b..196ae467c 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerUniversalConfigurator.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerUniversalConfigurator.kt
@@ -2,11 +2,18 @@ package io.ksmt.solver.runner
 
 import io.ksmt.runner.generated.models.ConfigurationParamKind
 import io.ksmt.runner.generated.models.SolverConfigurationParam
+import io.ksmt.runner.generated.models.SolverConfigurationTheories
 import io.ksmt.solver.KSolverConfiguration
 import io.ksmt.solver.KSolverUniversalConfigurationBuilder
+import io.ksmt.solver.KTheory
 
 class KSolverRunnerUniversalConfigurator : KSolverUniversalConfigurationBuilder {
     val config = mutableListOf<SolverConfigurationParam>()
+    var theories: SolverConfigurationTheories? = null
+
+    override fun buildOptimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        this.theories = SolverConfigurationTheories(quantifiersAllowed, theories?.map { it.name })
+    }
 
     override fun buildBoolParameter(param: String, value: Boolean) {
         config += SolverConfigurationParam(ConfigurationParamKind.Bool, param, "$value")
@@ -25,6 +32,11 @@ class KSolverRunnerUniversalConfigurator : KSolverUniversalConfigurationBuilder
     }
 }
 
+fun KSolverConfiguration.setUniversalOptimizeForTheories(theoriesConfig: SolverConfigurationTheories) {
+    val theories = theoriesConfig.theories?.mapTo(hashSetOf()) { KTheory.valueOf(it) }
+    optimizeForTheories(theories, theoriesConfig.quantifiersAllowed)
+}
+
 fun KSolverConfiguration.addUniversalParam(param: SolverConfigurationParam): Unit = with(param) {
     when (kind) {
         ConfigurationParamKind.String -> setStringParameter(name, value)
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 23ad6262a..b90a4b442 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
@@ -1,7 +1,7 @@
 package io.ksmt.solver.runner
 
 import io.ksmt.expr.KExpr
-import io.ksmt.runner.generated.models.SolverConfigurationParam
+import io.ksmt.runner.generated.models.SolverConfiguration
 import io.ksmt.sort.KBoolSort
 import java.util.concurrent.ConcurrentLinkedDeque
 import java.util.concurrent.ConcurrentLinkedQueue
@@ -23,7 +23,7 @@ class KSolverState {
         val tracked: ConcurrentLinkedQueue<KExpr<KBoolSort>> = ConcurrentLinkedQueue(),
     )
 
-    private val configuration = ConcurrentLinkedQueue<SolverConfigurationParam>()
+    private val configuration = ConcurrentLinkedQueue<SolverConfiguration>()
 
     /**
      * Asserted expressions.
@@ -36,8 +36,8 @@ class KSolverState {
         assertFrames.addLast(AssertionFrame())
     }
 
-    fun configure(config: List<SolverConfigurationParam>) {
-        configuration.addAll(config)
+    fun configure(config: SolverConfiguration) {
+        configuration.add(config)
     }
 
     fun assert(expr: KExpr<KBoolSort>) {
@@ -77,13 +77,13 @@ class KSolverState {
      * all solver state modification operations.
      * */
     private inline fun replayState(
-        configureSolver: (List<SolverConfigurationParam>) -> Unit,
+        configureSolver: (SolverConfiguration) -> Unit,
         pushScope: () -> Unit,
         assertExprs: (List<KExpr<KBoolSort>>) -> Unit,
         assertExprsAndTrack: (List<KExpr<KBoolSort>>) -> Unit
     ) {
         if (configuration.isNotEmpty()) {
-            configureSolver(configuration.toList())
+            configuration.forEach { configureSolver(it) }
         }
 
         var firstFrame = true
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 48ff7c29b..94b8da3ab 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
@@ -79,7 +79,8 @@ class KSolverWorkerProcess : ChildProcessBase<SolverProtocolModel>() {
         }
         configure.measureExecutionForTermination { config ->
             solver.configure {
-                config.forEach { addUniversalParam(it) }
+                config.theories?.let { setUniversalOptimizeForTheories(it) }
+                config.params.forEach { addUniversalParam(it) }
             }
         }
         assert.measureExecutionForTermination { params ->
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 f6c1dfa79..a0681d5ef 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
@@ -44,6 +44,16 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
         field("value", PredefinedType.string)
     }
 
+    private val solverConfigurationTheories = structdef {
+        field("quantifiersAllowed", PredefinedType.bool)
+        field("theories", immutableList(PredefinedType.string).nullable)
+    }
+
+    private val solverConfiguration = structdef {
+        field("params", immutableList(solverConfigurationParam))
+        field("theories", solverConfigurationTheories.nullable)
+    }
+
     private val assertParams = structdef {
         field("expression", kastType)
     }
@@ -110,7 +120,7 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
             async
             documentation = "Delete solver"
         }
-        call("configure", immutableList(solverConfigurationParam), PredefinedType.void).apply {
+        call("configure", solverConfiguration, PredefinedType.void).apply {
             async
             documentation = "Configure solver with parameters"
         }
diff --git a/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/CustomSolverTest.kt b/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/CustomSolverTest.kt
index da20ec611..4a05d845b 100644
--- a/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/CustomSolverTest.kt
+++ b/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/CustomSolverTest.kt
@@ -7,6 +7,7 @@ import io.ksmt.solver.KSolver
 import io.ksmt.solver.KSolverConfiguration
 import io.ksmt.solver.KSolverStatus
 import io.ksmt.solver.KSolverUniversalConfigurationBuilder
+import io.ksmt.solver.KTheory
 import io.ksmt.solver.model.KModelImpl
 import io.ksmt.sort.KBoolSort
 import kotlin.test.Test
@@ -72,6 +73,10 @@ class CustomSolverTest {
     class CustomSolverConfigBuilder(
         val builder: KSolverUniversalConfigurationBuilder
     ) : CustomSolverConfig {
+        override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+            error("Solver stub is not configurable")
+        }
+
         override fun setBoolParameter(param: String, value: Boolean) {
             error("Solver stub is not configurable")
         }
diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt
index d08ecd5c5..93975799c 100644
--- a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt
+++ b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt
@@ -49,6 +49,7 @@ import io.ksmt.test.TestRunner
 import io.ksmt.test.TestWorker
 import io.ksmt.test.TestWorkerProcess
 import io.ksmt.utils.FpUtils.isZero
+import io.ksmt.utils.KExprTheoryRequirement
 import java.nio.file.Path
 import java.nio.file.Paths
 import kotlin.io.path.Path
@@ -110,7 +111,15 @@ abstract class BenchmarksBasedTest {
                 val assertions = worker.parseFile(samplePath)
                 val ksmtAssertions = worker.convertAssertions(assertions)
 
+                val theoryRequirement = KExprTheoryRequirement(ctx).also { req ->
+                    ksmtAssertions.forEach { req.apply(it) }
+                }
+
                 val model = solverProvider(ctx).use { testSolver ->
+                    testSolver.configure {
+                        optimizeForTheories(theoryRequirement.usedTheories, theoryRequirement.hasQuantifiers)
+                    }
+
                     ksmtAssertions.forEach { testSolver.assertAsync(it) }
 
                     val status = testSolver.checkAsync(SOLVER_CHECK_SAT_TIMEOUT)
@@ -184,7 +193,15 @@ abstract class BenchmarksBasedTest {
 
                 val ksmtAssertions = worker.convertAssertions(assertions)
 
+                val theoryRequirement = KExprTheoryRequirement(ctx).also { req ->
+                    ksmtAssertions.forEach { req.apply(it) }
+                }
+
                 val actualStatus = solverProvider(ctx).use { ksmtSolver ->
+                    ksmtSolver.configure {
+                        optimizeForTheories(theoryRequirement.usedTheories, theoryRequirement.hasQuantifiers)
+                    }
+
                     ksmtAssertions.forEach { ksmtSolver.assertAsync(it) }
 
                     // use greater timeout to reduce false-positive unknowns
diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt
index 7c164abc9..7e08e45a1 100644
--- a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt
+++ b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt
@@ -36,16 +36,7 @@ class Cvc5BenchmarksBasedTest : BenchmarksBasedTest() {
         @JvmStatic
         fun cvc5TestData() = testData()
 
-        /**
-         * Resource limit to prevent solver from consuming huge amounts of native memory.
-         * The value is measured in some abstract resource usage units and chosen to maintain
-         * a balance between resource usage and the number of unknown check-sat results.
-         * */
-        const val RESOURCE_LIMIT = 4000
-
         fun KSolverRunnerManager.createCvc5TestSolver(ctx: KContext) =
-            createSolver(ctx, KCvc5Solver::class).apply {
-                configure { setCvc5Option("rlimit", "$RESOURCE_LIMIT") }
-            }
+            createSolver(ctx, KCvc5Solver::class)
     }
 }
diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolver.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolver.kt
index 51eeb7b04..b3d07b9d9 100644
--- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolver.kt
+++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolver.kt
@@ -28,6 +28,8 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
         }
     }
 
+    fun nativeSolver(): Context = nativeContext
+
     private val exprInternalizer: KYicesExprInternalizer by lazy {
         KYicesExprInternalizer(yicesCtx)
     }
@@ -50,7 +52,9 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
             "Solver instance has already been created"
         }
 
-        KYicesSolverConfigurationImpl(config).configurator()
+        yicesTry {
+            KYicesSolverConfigurationImpl(config).configurator()
+        }
     }
 
     override fun assert(expr: KExpr<KBoolSort>) = yicesTry {
diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt
index f97b72673..669a56a4b 100644
--- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt
+++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt
@@ -3,7 +3,15 @@ package io.ksmt.solver.yices
 import com.sri.yices.Config
 import io.ksmt.solver.KSolverConfiguration
 import io.ksmt.solver.KSolverUniversalConfigurationBuilder
+import io.ksmt.solver.KSolverUnsupportedFeatureException
 import io.ksmt.solver.KSolverUnsupportedParameterException
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.FP
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.smtLib2String
 
 interface KYicesSolverConfiguration : KSolverConfiguration {
     fun setYicesOption(option: String, value: String)
@@ -26,6 +34,22 @@ interface KYicesSolverConfiguration : KSolverConfiguration {
 }
 
 class KYicesSolverConfigurationImpl(private val config: Config) : KYicesSolverConfiguration {
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        if (theories.isNullOrEmpty()) return
+
+        if (FP in theories) {
+            throw KSolverUnsupportedFeatureException("Unsupported theory $FP")
+        }
+
+        // Yices requires MCSAT for the arithmetic theories
+        if (setOf(LIA, LRA, NIA, NRA).intersect(theories).isNotEmpty()) {
+            return
+        }
+
+        val theoryStr = theories.smtLib2String(quantifiersAllowed)
+        config.defaultConfigForLogic(theoryStr)
+    }
+
     override fun setYicesOption(option: String, value: String) {
         config.set(option, value)
     }
@@ -34,6 +58,10 @@ class KYicesSolverConfigurationImpl(private val config: Config) : KYicesSolverCo
 class KYicesSolverUniversalConfiguration(
     private val builder: KSolverUniversalConfigurationBuilder
 ) : KYicesSolverConfiguration {
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        builder.buildOptimizeForTheories(theories, quantifiersAllowed)
+    }
+
     override fun setYicesOption(option: String, value: String) {
         builder.buildStringParameter(option, value)
     }
diff --git a/ksmt-yices/ksmt-yices-core/src/test/kotlin/io/ksmt/solver/yices/LogicTest.kt b/ksmt-yices/ksmt-yices-core/src/test/kotlin/io/ksmt/solver/yices/LogicTest.kt
new file mode 100644
index 000000000..a1e59be5b
--- /dev/null
+++ b/ksmt-yices/ksmt-yices-core/src/test/kotlin/io/ksmt/solver/yices/LogicTest.kt
@@ -0,0 +1,54 @@
+package io.ksmt.solver.yices
+
+import io.ksmt.KContext
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.Array
+import io.ksmt.solver.KTheory.BV
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.UF
+import kotlin.test.Test
+import kotlin.test.assertNotNull
+
+class LogicTest {
+    private val ctx = KContext()
+    private val solver = KYicesSolver(ctx)
+
+    @Test
+    fun testSetAllLogic() {
+        solver.configure {
+            optimizeForTheories(theories = null, quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+
+    @Test
+    fun testSetPropLogic() {
+        solver.configure {
+            optimizeForTheories(theories = emptySet(), quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+
+    @Test
+    fun testSetSpecificLogic() {
+        solver.configure {
+            optimizeForTheories(theories = setOf(BV, UF, Array), quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+
+    @Test
+    fun testSetSpecificLogic2() {
+        solver.configure {
+            optimizeForTheories(theories = setOf(LIA, LRA, NIA, NRA, UF, Array), quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+}
diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt
index 76933ce3f..9faecab6e 100644
--- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt
+++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt
@@ -25,7 +25,11 @@ import kotlin.time.DurationUnit
 
 open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration> {
     private val z3Ctx = KZ3Context(ctx)
-    private val solver = createSolver()
+
+    private var lazyConfiguration: KZ3SolverLazyConfiguration? = null
+    private var solverInitialized: Boolean = false
+    private val solver by lazy { createSolver() }
+    fun nativeSolver(): Solver = solver
 
     private var lastCheckStatus = KSolverStatus.UNKNOWN
     private var lastReasonOfUnknown: String? = null
@@ -48,12 +52,36 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
 
     open fun createExprConverter(z3Ctx: KZ3Context) = KZ3ExprConverter(ctx, z3Ctx)
 
-    private fun createSolver(): Solver = z3Ctx.nativeContext.mkSolver()
+    private fun createSolver(): Solver {
+        solverInitialized = true
+        val config = lazyConfiguration
+        lazyConfiguration = null
+
+        val logic = config?.logicConfiguration
+
+        val solver = if (logic != null) {
+            z3Ctx.nativeContext.mkSolver(logic)
+        } else {
+            z3Ctx.nativeContext.mkSolver()
+        }
+
+        config?.params?.let { solver.setParameters(it) }
+
+        return solver
+    }
 
     override fun configure(configurator: KZ3SolverConfiguration.() -> Unit) {
-        val params = z3Ctx.nativeContext.mkParams()
-        KZ3SolverConfigurationImpl(params).configurator()
-        solver.setParameters(params)
+        if (!solverInitialized) {
+            val config = lazyConfiguration
+                ?: KZ3SolverLazyConfiguration(z3Ctx.nativeContext.mkParams())
+                    .also { lazyConfiguration = it }
+
+            config.configurator()
+        } else {
+            val config = KZ3SolverParamsConfiguration(z3Ctx.nativeContext.mkParams())
+            config.configurator()
+            solver.setParameters(config.params)
+        }
     }
 
     override fun push() {
diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SolverConfiguration.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SolverConfiguration.kt
index 92c2c559a..e6c0ef809 100644
--- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SolverConfiguration.kt
+++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SolverConfiguration.kt
@@ -2,7 +2,18 @@ package io.ksmt.solver.z3
 
 import com.microsoft.z3.Params
 import io.ksmt.solver.KSolverConfiguration
+import io.ksmt.solver.KSolverException
 import io.ksmt.solver.KSolverUniversalConfigurationBuilder
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.Array
+import io.ksmt.solver.KTheory.BV
+import io.ksmt.solver.KTheory.FP
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.UF
+import io.ksmt.solver.smtLib2String
 
 interface KZ3SolverConfiguration : KSolverConfiguration {
     fun setZ3Option(option: String, value: Boolean)
@@ -27,7 +38,7 @@ interface KZ3SolverConfiguration : KSolverConfiguration {
     }
 }
 
-class KZ3SolverConfigurationImpl(private val params: Params) : KZ3SolverConfiguration {
+sealed class KZ3SolverConfigurationImpl(val params: Params) : KZ3SolverConfiguration {
     override fun setZ3Option(option: String, value: Boolean) {
         params.add(option, value)
     }
@@ -45,9 +56,97 @@ class KZ3SolverConfigurationImpl(private val params: Params) : KZ3SolverConfigur
     }
 }
 
+class KZ3SolverLazyConfiguration(params: Params) : KZ3SolverConfigurationImpl(params) {
+    var logicConfiguration: String? = null
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        if (theories.isNullOrEmpty() || !supportedLogicCombination(theories, quantifiersAllowed)) {
+            logicConfiguration = null
+            return
+        }
+
+        logicConfiguration = theories.smtLib2String(quantifiersAllowed)
+    }
+
+    /**
+     * Z3 provide special solver only for the following theory combinations
+     * */
+    private fun supportedLogicCombination(theories: Set<KTheory>, quantifiersAllowed: Boolean): Boolean =
+        if (quantifiersAllowed) {
+            theories in supportedTheoriesWithQuantifiers
+        } else {
+            theories in supportedQuantifierFreeTheories
+        }
+
+    companion object {
+        private fun l(vararg theories: KTheory) = theories.toSet()
+
+        private val supportedTheoriesWithQuantifiers = setOf(
+            l(Array, BV),
+            l(Array, LIA),
+            l(Array, UF, BV),
+            l(Array, UF, LIA),
+            l(Array, UF, LIA, LRA),
+            l(Array, UF, NIA),
+            l(Array, UF, NIA, NRA),
+            l(BV),
+            l(FP),
+            l(LIA),
+            l(LRA),
+            l(NIA),
+            l(NRA),
+            l(UF),
+            l(UF, BV),
+            l(UF, LIA),
+            l(UF, LRA),
+            l(UF, NIA),
+            l(UF, NIA, NRA),
+            l(UF, NRA),
+        )
+
+        private val supportedQuantifierFreeTheories = setOf(
+            l(Array),
+            l(Array, BV),
+            l(Array, LIA),
+            l(Array, NIA),
+            l(Array, UF, BV),
+            l(Array, UF, LIA),
+            l(Array, UF, LIA, LRA),
+            l(Array, UF, NIA),
+            l(Array, UF, NIA, NRA),
+            l(BV),
+            l(BV, FP),
+            l(FP),
+            l(FP, LRA),
+            l(LIA),
+            l(LIA, LRA),
+            l(LRA),
+            l(NIA),
+            l(NIA, NRA),
+            l(NRA),
+            l(UF),
+            l(UF, BV),
+            l(UF, LIA),
+            l(UF, LRA),
+            l(UF, NIA),
+            l(UF, NIA, NRA),
+            l(UF, NRA),
+        )
+    }
+}
+
+class KZ3SolverParamsConfiguration(params: Params) : KZ3SolverConfigurationImpl(params) {
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        throw KSolverException("Solver logic already configured")
+    }
+}
+
 class KZ3SolverUniversalConfiguration(
     private val builder: KSolverUniversalConfigurationBuilder
 ) : KZ3SolverConfiguration {
+    override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
+        builder.buildOptimizeForTheories(theories, quantifiersAllowed)
+    }
+
     override fun setZ3Option(option: String, value: Boolean) {
         builder.buildBoolParameter(option, value)
     }
diff --git a/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/LogicTest.kt b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/LogicTest.kt
new file mode 100644
index 000000000..40ce3b63d
--- /dev/null
+++ b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/LogicTest.kt
@@ -0,0 +1,63 @@
+package io.ksmt.solver.z3
+
+import io.ksmt.KContext
+import io.ksmt.solver.KTheory
+import io.ksmt.solver.KTheory.Array
+import io.ksmt.solver.KTheory.BV
+import io.ksmt.solver.KTheory.LIA
+import io.ksmt.solver.KTheory.LRA
+import io.ksmt.solver.KTheory.NIA
+import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.UF
+import kotlin.test.Test
+import kotlin.test.assertNotNull
+
+class LogicTest {
+    private val ctx = KContext()
+    private val solver = KZ3Solver(ctx)
+
+    @Test
+    fun testSetAllLogic() {
+        solver.configure {
+            optimizeForTheories(theories = null, quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+
+    @Test
+    fun testSetPropLogic() {
+        solver.configure {
+            optimizeForTheories(theories = emptySet(), quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+
+    @Test
+    fun testSetSpecificLogic() {
+        solver.configure {
+            optimizeForTheories(theories = setOf(BV, UF, Array), quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+
+    @Test
+    fun testSetSpecificLogic2() {
+        solver.configure {
+            optimizeForTheories(theories = setOf(LIA, LRA, NIA, NRA, UF, Array), quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+
+    @Test
+    fun testSetSupportedLogic() {
+        solver.configure {
+            optimizeForTheories(theories = KTheory.values().toSet(), quantifiersAllowed = false)
+        }
+
+        assertNotNull(solver.nativeSolver())
+    }
+}