diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt
index f206c24bf6..72c857e79c 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt
@@ -2,6 +2,7 @@ package org.usvm.ts.calls
 
 import kotlinx.serialization.Serializable
 import kotlinx.serialization.decodeFromString
+import org.usvm.SolverType
 import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
@@ -37,6 +38,7 @@ internal data class CallsCoverageCellIdentity(
     val nativeFrontendRevision: String,
     val sourceManifest: String,
     val sourceIdentity: CallsCoverageSourceIdentity,
+    val solver: String,
     val projectIndex: Int,
     val functionIndex: Int,
     val profile: CallsExperimentProfile,
@@ -96,6 +98,11 @@ internal fun runCoverageUniverse(
         projectIndex = projectIndex,
         functionIndex = functionIndex,
     )
+    validateCoverageManifestBuild(
+        manifest = source.manifest,
+        runtimeToolRevision = runtimeToolRevision,
+        runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
+    )
     val output = Path.of(arguments.next()).toAbsolutePath().normalize()
     require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { "ETS_FRONTEND_SCRIPT must be unset" }
 
@@ -199,6 +206,11 @@ private fun parseCoverageCellRequest(
     val projectIndex = arguments.next().toInt()
     val functionIndex = arguments.next().toInt()
     val source = CallsCoverageSource.load(manifestPath, projectIndex = projectIndex, functionIndex = functionIndex)
+    validateCoverageManifestBuild(
+        manifest = source.manifest,
+        runtimeToolRevision = runtimeToolRevision,
+        runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
+    )
     val profile = CallsExperimentProfile.valueOf(arguments.next())
     val seed = arguments.next().toLong()
     val output = Path.of(arguments.next()).toAbsolutePath().normalize()
@@ -229,11 +241,12 @@ private fun parseCoverageCellRequest(
 
 
     val identity = CallsCoverageCellIdentity(
-        schemaVersion = 2,
+        schemaVersion = 3,
         toolRevision = runtimeToolRevision,
         nativeFrontendRevision = runtimeNativeFrontendRevision,
         sourceManifest = source.manifestPath.toString(),
         sourceIdentity = source.identity,
+        solver = source.manifest.solver,
         projectIndex = projectIndex,
         functionIndex = functionIndex,
         profile = profile,
@@ -271,6 +284,7 @@ private fun loadOrRunCoverageSearch(
             seed = identity.seed,
             budget = identity.budgetMillis.milliseconds,
             solverQueryLimit = identity.solverLimitMillis.milliseconds,
+            solverType = SolverType.valueOf(identity.solver),
             candidateCap = identity.candidateCap,
             onCandidate = { candidate -> appendDurably(candidatePath, encode(candidate)) },
         )
@@ -347,6 +361,19 @@ private fun coverageCheckpoints(
     }
 }
 
+private fun validateCoverageManifestBuild(
+    manifest: CallsExperimentManifest,
+    runtimeToolRevision: String,
+    runtimeNativeFrontendRevision: String,
+) {
+    require(manifest.toolRevision == runtimeToolRevision) {
+        "Coverage manifest tool revision differs from the running build"
+    }
+    require(manifest.nativeFrontendRevision == runtimeNativeFrontendRevision) {
+        "Coverage manifest frontend revision differs from the running build"
+    }
+}
+
 private inline fun <reified T> readLines(path: Path): List<T> = if (Files.exists(path)) {
     Files.readAllLines(path).filter(String::isNotBlank).map { line ->
         CallsExperimentJson.json.decodeFromString<T>(line)
diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt
index 2fcec4d4f6..1be8e31024 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt
@@ -79,6 +79,7 @@ internal data class CallsCoverageSearchRequest(
     val seed: Long,
     val budget: Duration,
     val solverQueryLimit: Duration,
+    val solverType: SolverType = SolverType.YICES,
     val candidateCap: Int,
     val onCandidate: (CallsCoverageCandidate) -> Unit = {},
 ) {
@@ -203,7 +204,7 @@ internal class CurrentTsCallsCoverageEngine(
             randomSeed = request.seed,
             timeout = request.budget,
             solverTimeout = request.solverQueryLimit,
-            solverType = SolverType.Z3,
+            solverType = request.solverType,
             stopOnCoverage = CALLS_STOP_ON_COVERAGE,
             stopOnTargetsReached = false,
             throwExceptionOnStepFailure = true,
diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt
index c73673579a..5a8bc4c4d2 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt
@@ -5,6 +5,7 @@ import kotlinx.serialization.Serializable
 import kotlinx.serialization.decodeFromString
 import kotlinx.serialization.json.Json
 import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
 import org.usvm.machine.call.TsResidualCallPolicy
 import org.usvm.machine.call.TsUnknownCallEvent
@@ -77,7 +78,7 @@ internal data class CallsExperimentManifest(
         require(seeds.isNotEmpty() && seeds.distinct().size == seeds.size) { "Seeds must be non-empty and unique" }
         require(perTargetBudgetMillis > 0) { "Per-target budget must be positive" }
         require(projects.isNotEmpty()) { "At least one project is required" }
-        require(solver == "Z3") { "The frozen calls experiment requires the Z3 solver" }
+        require(solver == "YICES" || solver == "Z3") { "Unsupported calls experiment solver: $solver" }
         require(searchPolicy == CALLS_PATH_SELECTION_STRATEGY.name) {
             "The frozen calls experiment requires ${CALLS_PATH_SELECTION_STRATEGY.name} search"
         }
@@ -135,6 +136,7 @@ internal data class CallsSymbolicSearchRequest(
     val expectedNativeFrontendRevision: String,
     val seed: Long,
     val budget: Duration,
+    val solverType: SolverType = SolverType.YICES,
     val unknownCallEventSink: ((TsUnknownCallEvent) -> Unit)? = null,
     val runtimeLimitationEventSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)? = null,
 )
@@ -421,6 +423,7 @@ internal class CallsExperimentRunner(
             expectedNativeFrontendRevision = manifest.nativeFrontendRevision,
             seed = seed,
             budget = manifest.perTargetBudgetMillis.milliseconds,
+            solverType = SolverType.valueOf(manifest.solver),
         )
         val eventWrites = CallsEventWriteTracker()
         val unknownCallSink = callsUnknownCallEventSink(
diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt
index 4e5a6d8ab9..ada0139f1d 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt
@@ -6,7 +6,6 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsReturnStmt
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStmt
-import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.machine.TsAnalysisStopReason
@@ -176,7 +175,7 @@ internal class CurrentTsCallsSymbolicEngine(
             stateCollectionStrategy = StateCollectionStrategy.REACHED_TARGET,
             randomSeed = request.seed,
             timeout = request.budget,
-            solverType = SolverType.Z3,
+            solverType = request.solverType,
             stopOnCoverage = CALLS_STOP_ON_COVERAGE,
             stopOnTargetsReached = false,
             throwExceptionOnStepFailure = true,
diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt
index 426a85e9ba..f8cddffa5c 100644
--- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt
+++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt
@@ -1,6 +1,7 @@
 package org.usvm.ts.calls
 
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.ts.pbt.model.ArrayDomain
 import org.usvm.ts.pbt.model.BooleanDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
@@ -69,6 +70,31 @@ class CallsCoverageExperimentTest {
         assertTrue(universe.probeElapsedMillis >= 0)
     }
 
+    @Test
+    fun `coverage search honors either explicitly configured solver`() {
+        val fixture = fixture(
+            source = """
+                export function classify(flag: boolean): number {
+                  if (flag) return 1;
+                  return 2;
+                }
+            """.trimIndent(),
+            exportName = "classify",
+            inputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)),
+        )
+        for (solverType in listOf(SolverType.YICES, SolverType.Z3)) {
+            val emitted = mutableListOf<CallsCoverageCandidate>()
+
+            val search = CurrentTsCallsCoverageEngine(testSourceEngine()).search(
+                request = coverageRequest(fixture, onCandidate = emitted::add, solverType = solverType),
+            )
+
+            assertEquals(CallsCoverageSearchStatus.EXHAUSTED, search.status, search.toString())
+            assertEquals(2, search.candidates.size)
+            assertEquals(search.candidates, emitted)
+        }
+    }
+
     @Test
     fun `coverage universe has a denominator without invoking the entry function`() {
         val fixture = fixture(
@@ -273,6 +299,7 @@ class CallsCoverageExperimentTest {
     private fun coverageRequest(
         fixture: CoverageFixture,
         onCandidate: (CallsCoverageCandidate) -> Unit,
+        solverType: SolverType = SolverType.YICES,
     ) = CallsCoverageSearchRequest(
         sourceRoot = fixture.sourceRoot,
         project = fixture.project,
@@ -283,6 +310,7 @@ class CallsCoverageExperimentTest {
         seed = 17,
         budget = 10.seconds,
         solverQueryLimit = 2.seconds,
+        solverType = solverType,
         candidateCap = 8,
         onCandidate = onCandidate,
     )
diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt
index 5788f8e414..d590706752 100644
--- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt
+++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt
@@ -2,6 +2,7 @@ package org.usvm.ts.calls
 
 import kotlinx.serialization.decodeFromString
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.ts.pbt.model.BooleanDomain
 import org.usvm.ts.pbt.model.NumberDomain
 import org.usvm.ts.pbt.model.PropertyInput
@@ -32,6 +33,102 @@ class CallsCoverageSourceTest {
         )
         assertEquals(emptySearch, result.search)
         assertEquals(fixture.source.identity, result.identity.sourceIdentity)
+        assertEquals(3, result.identity.schemaVersion)
+        assertEquals("YICES", result.identity.solver)
+    }
+
+    @Test
+    fun `coverage cell forwards the explicit manifest solver to search`() {
+        val fixture = fixture(solver = "Z3")
+        val solvers = mutableListOf<SolverType>()
+
+        fixture.runCell(searchFunction = { request ->
+            solvers += request.solverType
+            emptySearch
+        })
+
+        val result = CallsExperimentJson.json.decodeFromString<CallsCoverageCellResult>(
+            Files.readString(fixture.output.resolve("result.json")),
+        )
+        assertEquals(listOf(SolverType.Z3), solvers)
+        assertEquals("Z3", result.identity.solver)
+    }
+
+    @Test
+    fun `resumed search rejects a persisted identity from a different solver`() {
+        val fixture = fixture()
+        fixture.persistSearch(solver = "Z3")
+
+        val failure = assertFailsWith<IllegalArgumentException> { fixture.runCell() }
+
+        assertEquals("Cell identity changed", failure.message)
+        fixture.assertNoReplayOrCompletion()
+    }
+
+    @Test
+    fun `resumed search rejects the prior cell schema`() {
+        val fixture = fixture()
+        fixture.persistSearch(schemaVersion = 2)
+
+        val failure = assertFailsWith<IllegalArgumentException> { fixture.runCell() }
+
+        assertEquals("Cell identity changed", failure.message)
+        fixture.assertNoReplayOrCompletion()
+    }
+
+    @Test
+    fun `build mismatch rejects search and universe collection before callbacks`() {
+        val fixture = fixture()
+        var searched = false
+        var probed = false
+        val otherRevision = "2222222222222222222222222222222222222222"
+
+        val searchFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runCell(runtimeToolRevision = otherRevision, searchFunction = {
+                searched = true
+                emptySearch
+            })
+        }
+        val universeFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runUniverse(runtimeToolRevision = otherRevision, probeFunction = {
+                probed = true
+                sampleUniverse
+            })
+        }
+
+        assertEquals("Coverage manifest tool revision differs from the running build", searchFailure.message)
+        assertEquals(searchFailure.message, universeFailure.message)
+        assertFalse(searched)
+        assertFalse(probed)
+        assertFalse(Files.exists(fixture.output.resolve("identity.json")))
+        assertFalse(Files.exists(directory.resolve("universe-output/universe.json")))
+    }
+
+    @Test
+    fun `frontend mismatch rejects search and universe collection before callbacks`() {
+        val fixture = fixture()
+        var searched = false
+        var probed = false
+
+        val searchFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runCell(runtimeNativeFrontendRevision = "bundled:other", searchFunction = {
+                searched = true
+                emptySearch
+            })
+        }
+        val universeFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runUniverse(runtimeNativeFrontendRevision = "bundled:other", probeFunction = {
+                probed = true
+                sampleUniverse
+            })
+        }
+
+        assertEquals("Coverage manifest frontend revision differs from the running build", searchFailure.message)
+        assertEquals(searchFailure.message, universeFailure.message)
+        assertFalse(searched)
+        assertFalse(probed)
+        assertFalse(Files.exists(fixture.output.resolve("identity.json")))
+        assertFalse(Files.exists(directory.resolve("universe-output/universe.json")))
     }
 
     @Test
@@ -189,7 +286,7 @@ class CallsCoverageSourceTest {
         assertFalse(Files.exists(directory.resolve("universe-output/universe.json")))
     }
 
-    private fun fixture(): Fixture {
+    private fun fixture(solver: String = "YICES"): Fixture {
         val sourceRoot = Files.createDirectory(directory.resolve("source"))
         val sourceFile = sourceRoot.resolve("Fixture.ts")
         Files.writeString(sourceFile, "export function first(flag: boolean): boolean { return flag; }")
@@ -218,7 +315,7 @@ class CallsCoverageSourceTest {
             experimentId = "coverage-identity",
             toolRevision = TOOL_REVISION,
             nativeFrontendRevision = FRONTEND_REVISION,
-            solver = "Z3",
+            solver = solver,
             searchPolicy = CALLS_PATH_SELECTION_STRATEGY.name,
             modelSet = CallsModelSetIdentity(ids = emptySet(), toolRevision = TOOL_REVISION),
             seeds = listOf(17L),
@@ -255,25 +352,30 @@ class CallsCoverageSourceTest {
             Files.writeString(universePath, CallsExperimentJson.json.encodeToUtf8SafeString(record))
         }
 
-        fun runUniverse(probeFunction: (CallsCoverageSource) -> CallsCoverageUniverse): Path {
+        fun runUniverse(
+            runtimeToolRevision: String = TOOL_REVISION,
+            runtimeNativeFrontendRevision: String = FRONTEND_REVISION,
+            probeFunction: (CallsCoverageSource) -> CallsCoverageUniverse,
+        ): Path {
             val output = manifestPath.resolveSibling("universe-output")
             runCoverageUniverse(
                 args = listOf(manifestPath.toString(), "0", "0", output.toString()),
-                runtimeToolRevision = TOOL_REVISION,
-                runtimeNativeFrontendRevision = FRONTEND_REVISION,
+                runtimeToolRevision = runtimeToolRevision,
+                runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
                 probeFunction = probeFunction,
             )
 
             return output
         }
 
-        fun persistSearch() {
+        fun persistSearch(schemaVersion: Int = 3, solver: String = source.manifest.solver) {
             val identity = CallsCoverageCellIdentity(
-                schemaVersion = 2,
+                schemaVersion = schemaVersion,
                 toolRevision = TOOL_REVISION,
                 nativeFrontendRevision = FRONTEND_REVISION,
                 sourceManifest = manifestPath.toRealPath().toString(),
                 sourceIdentity = source.identity,
+                solver = solver,
                 projectIndex = 0,
                 functionIndex = 0,
                 profile = CallsExperimentProfile.EMPTY_STOP,
@@ -295,6 +397,8 @@ class CallsCoverageSourceTest {
         }
 
         fun runCell(
+            runtimeToolRevision: String = TOOL_REVISION,
+            runtimeNativeFrontendRevision: String = FRONTEND_REVISION,
             searchFunction: (CallsCoverageSearchRequest) -> CallsCoverageSearchResult = {
                 error("Must resume persisted search")
             },
@@ -312,8 +416,8 @@ class CallsCoverageSourceTest {
                     "8",
                     universePath.toString(),
                 ),
-                runtimeToolRevision = TOOL_REVISION,
-                runtimeNativeFrontendRevision = FRONTEND_REVISION,
+                runtimeToolRevision = runtimeToolRevision,
+                runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
                 searchFunction = searchFunction,
             )
         }
diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt
index 08a1a5d754..371417f10e 100644
--- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt
+++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsExperimentTest.kt
@@ -6,6 +6,7 @@ import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.machine.call.TsResidualCallPolicy
 import org.usvm.machine.call.TsUnknownCallDecision
 import org.usvm.machine.call.TsUnknownCallEvent
@@ -23,6 +24,28 @@ import kotlin.test.assertNull
 import kotlin.test.assertTrue
 
 class CallsExperimentTest {
+    @Test
+    fun `runner forwards an explicitly configured solver`(@TempDir directory: Path) {
+        val solvers = mutableListOf<SolverType>()
+        val engine = CallsSymbolicEngine { request ->
+            solvers += request.solverType
+            result(status = CallsSymbolicStatus.UNREACHED)
+        }
+        val z3Manifest = manifest(sourceRoot = ".", seeds = listOf(17L)).copy(solver = "Z3")
+
+        CallsExperimentRunner(
+            symbolicEngine = engine,
+            targetReplayer = CallsTargetReplayer { _, _, _, _, _ -> error("No witness to replay") },
+            runtimeToolRevision = FIXTURE_TOOL_REVISION,
+        ).run(
+            manifest = z3Manifest,
+            manifestDirectory = directory,
+            rawOutput = directory.resolve("results.jsonl"),
+        )
+
+        assertEquals(setOf(SolverType.Z3), solvers.toSet())
+    }
+
     @Test
     fun `runner persists call events before search returns without counting them as results`(@TempDir directory: Path) {
         val source = Path.of(checkNotNull(javaClass.getResource("/calls/SourceTargetReplayFixture.ts")).toURI())
@@ -513,7 +536,7 @@ class CallsExperimentTest {
         experimentId = "fixture",
         toolRevision = FIXTURE_TOOL_REVISION,
         nativeFrontendRevision = "frontend-revision",
-        solver = "Z3",
+        solver = "YICES",
         searchPolicy = CALLS_PATH_SELECTION_STRATEGY.name,
         modelSet = CallsModelSetIdentity(
             ids = setOf("ts.array.pop", "ts.array.shift"),
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt
index 0db12fc868..10bf82289f 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt
@@ -3,6 +3,7 @@ package org.usvm.ts.pbt.usvm
 import io.ksmt.utils.asExpr
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsType
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.api.targets.TsTarget
@@ -30,7 +31,7 @@ import org.usvm.ts.pbt.model.PropertyId
 /** Searches mapped TypeScript predicates for concrete property violations with USVM. */
 class UsvmPropertySearcher(
     private val scene: EtsScene,
-    machineOptions: UMachineOptions = UMachineOptions(),
+    machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES),
     private val tsOptions: TsOptions = TsOptions(),
     projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(),
 ) {
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt
index 31bf803489..8c2ca6d260 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmCollectionDomainProjectorTest.kt
@@ -9,6 +9,7 @@ import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.BeforeAll
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UConcreteHeapRef
 import org.usvm.UMachineOptions
@@ -187,7 +188,10 @@ class UsvmCollectionDomainProjectorTest {
     ) {
         TsMachine(
             scene = scene,
-            options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL),
+            options = UMachineOptions(
+                solverType = SolverType.YICES,
+                stateCollectionStrategy = StateCollectionStrategy.ALL
+            ),
             tsOptions = TsOptions(),
         ).use { machine ->
             machine.analyze(
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt
index c9a988ef7b..5f2df3b3d8 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmInitialStateConfigurationTest.kt
@@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.machine.TsMachine
@@ -30,7 +31,8 @@ class UsvmInitialStateConfigurationTest {
         val method = scene.projectClasses
             .flatMap { etsClass -> etsClass.methods }
             .single { candidate -> candidate.name == "isPositive" }
-        val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL)
+        val options =
+            UMachineOptions(solverType = SolverType.YICES, stateCollectionStrategy = StateCollectionStrategy.ALL)
 
         val states = TsMachine(
             scene = scene,
@@ -85,7 +87,8 @@ class UsvmInitialStateConfigurationTest {
         )
         val mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent))
         val predicate = requireNotNull(mapper.map(manifest).predicate.exactTargetOrNull())
-        val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL)
+        val options =
+            UMachineOptions(solverType = SolverType.YICES, stateCollectionStrategy = StateCollectionStrategy.ALL)
 
         val analysis = TsMachine(
             scene = scene,
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt
index ffd0fe5a0c..ba5c59748b 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcherTest.kt
@@ -5,6 +5,7 @@ import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.BeforeAll
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.machine.TsOptions
 import org.usvm.ts.pbt.backend.ProjectionCapability
@@ -327,7 +328,7 @@ class UsvmPropertySearcherTest {
         val manifest = manifest(predicateExport = "validProperty")
         val zeroTimeoutSearcher = UsvmPropertySearcher(
             scene = scene,
-            machineOptions = UMachineOptions(timeout = Duration.ZERO),
+            machineOptions = UMachineOptions(solverType = SolverType.YICES, timeout = Duration.ZERO),
         )
 
         val result = zeroTimeoutSearcher.search(
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt
index 65f8fc7e55..9e05b77b05 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmScalarDomainProjectorTest.kt
@@ -6,6 +6,7 @@ import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.BeforeAll
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapRef
@@ -206,7 +207,10 @@ class UsvmScalarDomainProjectorTest {
     ): Boolean = runCatching {
         TsMachine(
             scene = scene,
-            options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL),
+            options = UMachineOptions(
+                solverType = SolverType.YICES,
+                stateCollectionStrategy = StateCollectionStrategy.ALL
+            ),
             tsOptions = TsOptions(),
         ).use { machine ->
             machine.analyze(
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index b5d2eb38a2..079d72f26e 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStmt
 import org.usvm.CoverageZone
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
@@ -72,7 +73,7 @@ data class TsMachineAnalysisResult(
 
 class TsMachine(
     scene: EtsScene,
-    override val options: UMachineOptions,
+    override val options: UMachineOptions = UMachineOptions(solverType = SolverType.YICES),
     private val tsOptions: TsOptions,
     private val machineObserver: UMachineObserver<TsState>? = null,
     observer: TsInterpreterObserver? = null,
diff --git a/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt b/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt
index 6193e96512..745c79b020 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/checkers/ReachabilityChecker.kt
@@ -3,6 +3,7 @@ package org.usvm.checkers
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.targets.ReachabilityObserver
 import org.usvm.api.targets.TsReachabilityTarget
@@ -20,6 +21,7 @@ class ReachabilityChecker {
         EtsScene(listOf(file))
     }
     val options = UMachineOptions(
+        solverType = SolverType.YICES,
         stopOnTargetsReached = true,
         pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
         timeout = 15000000.seconds
diff --git a/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt b/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt
index b874547060..336867f2f2 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/checkers/UnreachableCodeDetector.kt
@@ -8,6 +8,7 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.TestInstance
 import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.checkers.UnreachableCodeDetector
 import org.usvm.machine.TsMachine
@@ -26,7 +27,7 @@ class UnreachableCodeDetectorTest {
         )
         EtsScene(listOf(file))
     }
-    val options = UMachineOptions()
+    val options = UMachineOptions(solverType = SolverType.YICES)
     val tsOptions = TsOptions(interproceduralAnalysis = false)
 
     @Test
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt
index e67df781a5..ace942d088 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/StringEngineTest.kt
@@ -6,6 +6,7 @@ import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
@@ -48,7 +49,8 @@ class StringEngineTest : TsMethodTestRunner() {
     fun `shared allocation and bounded decoding preserve a solver selected surrogate`() {
         val method = getMethod(methodName = "inputRoundtrip", className = "SymbolicStringEngine")
         lateinit var input: UConcreteHeapRef
-        val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL)
+        val options =
+            UMachineOptions(solverType = SolverType.YICES, stateCollectionStrategy = StateCollectionStrategy.ALL)
 
         TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine ->
             val states = machine.analyze(
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineCompletionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineCompletionTest.kt
index 416e1910ae..5ccb6df57a 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineCompletionTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineCompletionTest.kt
@@ -2,18 +2,48 @@ package org.usvm.machine
 
 import org.jacodb.ets.model.EtsScene
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.util.TsMethodTestRunner
 import kotlin.test.assertEquals
+import kotlin.test.assertSame
+import kotlin.test.assertTrue
 import kotlin.time.Duration
 
 class TsMachineCompletionTest : TsMethodTestRunner() {
     override val scene: EtsScene = loadScene("/samples/lang/StaticOverloads.ts")
 
+    @Test
+    fun `TypeScript defaults to Yices without replacing an explicitly selected solver`() {
+        val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads")
+
+        TsMachine(scene = scene, tsOptions = TsOptions()).use { machine ->
+            assertEquals(SolverType.YICES, machine.options.solverType)
+        }
+
+        for (solverType in listOf(SolverType.YICES, SolverType.Z3)) {
+            val options = UMachineOptions(
+                solverType = solverType,
+                stopOnCoverage = 0,
+                timeout = Duration.INFINITE,
+            )
+
+            TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine ->
+                val outcome = machine.analyzeWithOutcome(methods = listOf(method))
+
+                assertSame(options, machine.options)
+                assertEquals(solverType, machine.options.solverType)
+                assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+                assertTrue(outcome.states.isNotEmpty())
+            }
+        }
+    }
+
     @Test
     fun `analysis distinguishes path exhaustion from strategy stop`() {
         val method = getMethod(methodName = "callOverloaded", className = "StaticOverloads")
         val exhaustedOptions = UMachineOptions(
+            solverType = SolverType.YICES,
             stopOnCoverage = 0,
             timeout = Duration.INFINITE,
         )
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt
index c58e180e51..fa09cad3fc 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSharedAnalysisTest.kt
@@ -32,7 +32,7 @@ class TsSharedAnalysisTest {
         stateCollectionStrategy = StateCollectionStrategy.ALL,
         stopOnCoverage = 0,
         timeout = Duration.INFINITE,
-        solverType = SolverType.Z3,
+        solverType = SolverType.YICES,
     )
     private val tsOptions = TsOptions(
         unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()),
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt
index e06ee3b519..aab11c09ca 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt
@@ -7,6 +7,7 @@ import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.TsTest
 import org.usvm.api.TsTestValue
@@ -63,7 +64,11 @@ class ErrorModelBackingBoundaryTest : TsMethodTestRunner() {
     // It does not claim support for adding arbitrary own properties through the TypeScript interpreter.
     private fun checkStorageIsolation(key: ErrorStorageField, sourceName: String) {
         val method = getMethod(methodName = "allocatedError", className = "ErrorModelBackingBoundary")
-        TsMachine(scene = scene, options = UMachineOptions(), tsOptions = TsOptions()).use { machine ->
+        TsMachine(
+            scene = scene,
+            options = UMachineOptions(solverType = SolverType.YICES),
+            tsOptions = TsOptions()
+        ).use { machine ->
             val state = machine.analyze(listOf(method)).single()
             val result = assertIs<TsMethodResult.Success>(state.methodResult)
             val reference = result.value.asExpr(state.ctx.addressSort)
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt
index a0896e7fc3..140475c707 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt
@@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsMethodSignature
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsUnknownType
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
@@ -341,7 +342,7 @@ class TsUnknownCallModelCatalogTest {
         val error = assertFailsWith<IllegalArgumentException> {
             TsMachine(
                 scene = EtsScene(projectFiles = listOf(applicationFile)),
-                options = UMachineOptions(),
+                options = UMachineOptions(solverType = SolverType.YICES),
                 tsOptions = TsOptions(),
                 unknownCallModels = catalog,
             )
@@ -361,7 +362,7 @@ class TsUnknownCallModelCatalogTest {
         val error = assertFailsWith<IllegalArgumentException> {
             TsMachine(
                 scene = EtsScene(projectFiles = emptyList(), sdkFiles = listOf(sdkFile)),
-                options = UMachineOptions(),
+                options = UMachineOptions(solverType = SolverType.YICES),
                 tsOptions = TsOptions(),
                 unknownCallModels = catalog,
             ).close()
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt
index 8244fa9351..e05c0f4975 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/RuntimeLimitationBoundariesTest.kt
@@ -4,6 +4,7 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.TsTestValue
 import org.usvm.machine.TsAnalysisStopReason
@@ -36,7 +37,11 @@ class RuntimeLimitationBoundariesTest : TsMethodTestRunner() {
 
         TsMachine(
             scene = scene,
-            options = UMachineOptions(throwExceptionOnStepFailure = true, stepsFromLastCovered = 128L),
+            options = UMachineOptions(
+                solverType = SolverType.YICES,
+                throwExceptionOnStepFailure = true,
+                stepsFromLastCovered = 128L
+            ),
             tsOptions = TsOptions(),
             observer = observer,
         ).use { machine ->
@@ -59,7 +64,11 @@ class RuntimeLimitationBoundariesTest : TsMethodTestRunner() {
 
         TsMachine(
             scene = scene,
-            options = UMachineOptions(throwExceptionOnStepFailure = true, stepsFromLastCovered = 128L),
+            options = UMachineOptions(
+                solverType = SolverType.YICES,
+                throwExceptionOnStepFailure = true,
+                stepsFromLastCovered = 128L
+            ),
             tsOptions = TsOptions(),
             observer = observer,
         ).use { machine ->
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt
index 869554eb16..4fc9bbacfa 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt
@@ -3,6 +3,7 @@ package org.usvm.samples.arrays
 import org.jacodb.ets.model.EtsScene
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.TsTestValue
 import org.usvm.machine.TsInterpreterObserver
@@ -153,7 +154,7 @@ class AllocatedArrays : TsMethodTestRunner() {
         val observer = RecordingObserver()
         val states = TsMachine(
             scene = scene,
-            options = UMachineOptions(),
+            options = UMachineOptions(solverType = SolverType.YICES),
             tsOptions = TsOptions(),
             observer = observer,
         ).use { machine ->
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/NamedFunctionImports.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/NamedFunctionImports.kt
index 670a6ea47e..8a471013d0 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/NamedFunctionImports.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/NamedFunctionImports.kt
@@ -3,6 +3,7 @@ package org.usvm.samples.lang
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.loadEtsProjectAutoConvert
 import org.junit.jupiter.api.Test
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.TsTestValue
 import org.usvm.machine.TsAnalysisStopReason
@@ -46,7 +47,11 @@ class NamedFunctionImports : TsMethodTestRunner() {
     fun `namespace direct and optional calls explicitly report their unrepresented receiver`() {
         listOf("namespaceDirectCall", "namespaceOptionalCall").forEach { methodName ->
             val method = getMethod(methodName = methodName)
-            val outcome = TsMachine(scene = scene, options = UMachineOptions(), tsOptions = TsOptions()).use { machine ->
+            val outcome = TsMachine(
+                scene = scene,
+                options = UMachineOptions(solverType = SolverType.YICES),
+                tsOptions = TsOptions(),
+            ).use { machine ->
                 machine.analyzeWithOutcome(methods = listOf(method))
             }
 
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/DeleteProperty.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/DeleteProperty.kt
index f9cf673eb9..e7538eade8 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/DeleteProperty.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/DeleteProperty.kt
@@ -2,6 +2,7 @@ package org.usvm.samples.operators
 
 import org.jacodb.ets.model.EtsScene
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.api.TsTestValue
@@ -43,6 +44,7 @@ class DeleteProperty : TsMethodTestRunner() {
     fun `delete example exhausts paths without interpreter failure`() {
         val method = getMethod("readAfterDelete")
         val options = UMachineOptions(
+            solverType = SolverType.YICES,
             stopOnCoverage = 0,
             timeout = Duration.INFINITE,
             throwExceptionOnStepFailure = true,
@@ -134,6 +136,7 @@ class DeleteProperty : TsMethodTestRunner() {
         )
 
         val options = UMachineOptions(
+            solverType = SolverType.YICES,
             stateCollectionStrategy = StateCollectionStrategy.ALL,
             stopOnCoverage = 0,
             timeout = Duration.INFINITE,
@@ -259,6 +262,7 @@ class DeleteProperty : TsMethodTestRunner() {
     fun `type assertion losing a property reference reports unsupported`() {
         val method = getMethod("deleteCastedField")
         val options = UMachineOptions(
+            solverType = SolverType.YICES,
             stateCollectionStrategy = StateCollectionStrategy.ALL,
             stopOnCoverage = 0,
             timeout = Duration.INFINITE,
@@ -279,7 +283,11 @@ class DeleteProperty : TsMethodTestRunner() {
             "deleteInput", "untouchedInput", "deleteInputAlias", "restoreInput", "conditionalDeleteInput",
             "deleteValueExpression", "deleteAssignmentExpression", "deleteCastedValue",
         )
-        val options = UMachineOptions(stateCollectionStrategy = StateCollectionStrategy.ALL, stopOnCoverage = 0)
+        val options = UMachineOptions(
+            solverType = SolverType.YICES,
+            stateCollectionStrategy = StateCollectionStrategy.ALL,
+            stopOnCoverage = 0,
+        )
         val tests = names.associateWith { name -> runner(getMethod(name), options) }
 
         fun serialize(value: TsTestValue): String = when (value) {
@@ -323,6 +331,7 @@ class DeleteProperty : TsMethodTestRunner() {
     fun `deleting an own property with a prototype fallback reports unsupported outcome`() {
         val method = getMethod("deleteOwnToString")
         val options = UMachineOptions(
+            solverType = SolverType.YICES,
             stateCollectionStrategy = StateCollectionStrategy.ALL,
             stopOnCoverage = 0,
             timeout = Duration.INFINITE,
@@ -340,6 +349,7 @@ class DeleteProperty : TsMethodTestRunner() {
     @Test
     fun `deleting prototype methods reports unsupported while own field remains supported`() {
         val options = UMachineOptions(
+            solverType = SolverType.YICES,
             stateCollectionStrategy = StateCollectionStrategy.ALL,
             stopOnCoverage = 0,
             timeout = Duration.INFINITE,
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt
index f5f7639590..76d3dcd6de 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt
@@ -3,6 +3,7 @@ package org.usvm.samples.types
 import org.jacodb.ets.model.EtsScene
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.api.TsTestValue
@@ -651,6 +652,7 @@ class RuntimeInstanceofTest : TsMethodTestRunner() {
     }
 
     private val machineOptions = UMachineOptions(
+        solverType = SolverType.YICES,
         stateCollectionStrategy = StateCollectionStrategy.ALL,
         stopOnCoverage = 0,
         timeout = 30.seconds,
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt
index 11d96bf15a..d85e220e69 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeNewTest.kt
@@ -3,6 +3,7 @@ package org.usvm.samples.types
 import org.jacodb.ets.model.EtsScene
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.api.TsTestValue
@@ -509,6 +510,7 @@ class RuntimeNewTest : TsMethodTestRunner() {
     }
 
     private val machineOptions = UMachineOptions(
+        solverType = SolverType.YICES,
         stateCollectionStrategy = StateCollectionStrategy.ALL,
         stopOnCoverage = 0,
         timeout = 30.seconds,