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 d91a348784..98d913d88a 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
@@ -58,21 +58,76 @@ internal fun runCoverageCell(
     runtimeNativeFrontendRevision: String = CallsBuildIdentity.nativeFrontendRevision,
     searchFunction: (CallsCoverageSearchRequest) -> CallsCoverageSearchResult = CurrentTsCallsCoverageEngine()::search,
 ) {
-    require(args.size == 9) { "coverage-cell requires 9 arguments" }
-    val projectIndex = args[1].toInt()
-    val functionIndex = args[2].toInt()
-    val source = CallsCoverageSource.load(Path.of(args[0]), projectIndex, functionIndex)
-    val manifestPath = source.manifestPath
-    val manifest = source.manifest
-    val profile = CallsExperimentProfile.valueOf(args[3])
-    val seed = args[4].toLong()
-    val output = Path.of(args[5]).toAbsolutePath().normalize()
-    val budgetMillis = args[6].toLong()
-    val solverLimitMillis = args[7].toLong()
-    val candidateCap = args[8].toInt()
-    val project = source.project
-    val function = source.function
-    require(seed in manifest.seeds) { "Seed is outside the frozen source manifest" }
+    val request = parseCoverageCellRequest(
+        args = args,
+        runtimeToolRevision = runtimeToolRevision,
+        runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
+    )
+    val source = request.source
+    val identity = request.identity
+    val output = request.output
+    require(Regex("[0-9a-f]{40}").matches(identity.toolRevision)) { "Coverage build must be clean" }
+
+    Files.createDirectories(output)
+    val identityPath = output.resolve("identity.json")
+    val expectedIdentity = encode(identity)
+    if (Files.exists(identityPath)) {
+        require(Files.readString(identityPath).trim() == expectedIdentity) { "Cell identity changed" }
+    } else {
+        require(Files.list(output).use { entries -> entries.findAny().isEmpty }) { "Output directory is not empty" }
+        atomicWrite(identityPath, expectedIdentity)
+    }
+    require(!Files.exists(output.resolve("result.json"))) { "Cell already completed" }
+
+    val search = loadOrRunCoverageSearch(
+        source = source,
+        identity = identity,
+        output = output,
+        searchFunction = searchFunction,
+    )
+    val events = replayCoverageCandidates(source = source, search = search, output = output)
+
+    source.verifyUnchanged()
+    val result = CallsCoverageCellResult(
+        identity = identity,
+        search = search,
+        replayErrors = events.count { it.error != null },
+        completionMismatches = events.indices.count { index ->
+            events[index].replay?.completion != null &&
+                events[index].replay?.completion != search.candidates[index].completion
+        },
+        checkpoints = coverageCheckpoints(search = search, events = events, budgetMillis = identity.budgetMillis),
+    )
+    atomicWrite(output.resolve("result.json"), encode(result))
+    System.out.appendLine(encode(result))
+}
+
+private data class CoverageCellRequest(
+    val source: CallsCoverageSource,
+    val identity: CallsCoverageCellIdentity,
+    val output: Path,
+)
+
+private fun parseCoverageCellRequest(
+    args: List<String>,
+    runtimeToolRevision: String,
+    runtimeNativeFrontendRevision: String,
+): CoverageCellRequest {
+    require(args.size == COVERAGE_CELL_ARGUMENT_COUNT) {
+        "coverage-cell requires $COVERAGE_CELL_ARGUMENT_COUNT arguments"
+    }
+    val arguments = args.iterator()
+    val manifestPath = Path.of(arguments.next())
+    val projectIndex = arguments.next().toInt()
+    val functionIndex = arguments.next().toInt()
+    val source = CallsCoverageSource.load(manifestPath, projectIndex = projectIndex, functionIndex = functionIndex)
+    val profile = CallsExperimentProfile.valueOf(arguments.next())
+    val seed = arguments.next().toLong()
+    val output = Path.of(arguments.next()).toAbsolutePath().normalize()
+    val budgetMillis = arguments.next().toLong()
+    val solverLimitMillis = arguments.next().toLong()
+    val candidateCap = arguments.next().toInt()
+    require(seed in source.manifest.seeds) { "Seed is outside the frozen source manifest" }
     require(budgetMillis > 0 && solverLimitMillis in 1..budgetMillis && candidateCap > 0)
     require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { "ETS_FRONTEND_SCRIPT must be unset" }
 
@@ -80,7 +135,7 @@ internal fun runCoverageCell(
         schemaVersion = 2,
         toolRevision = runtimeToolRevision,
         nativeFrontendRevision = runtimeNativeFrontendRevision,
-        sourceManifest = manifestPath.toString(),
+        sourceManifest = source.manifestPath.toString(),
         sourceIdentity = source.identity,
         projectIndex = projectIndex,
         functionIndex = functionIndex,
@@ -90,37 +145,35 @@ internal fun runCoverageCell(
         solverLimitMillis = solverLimitMillis,
         candidateCap = candidateCap,
     )
-    require(Regex("[0-9a-f]{40}").matches(identity.toolRevision)) { "Coverage build must be clean" }
 
-    Files.createDirectories(output)
-    val identityPath = output.resolve("identity.json")
-    val expectedIdentity = encode(identity)
-    if (Files.exists(identityPath)) {
-        require(Files.readString(identityPath).trim() == expectedIdentity) { "Cell identity changed" }
-    } else {
-        require(Files.list(output).use { entries -> entries.findAny().isEmpty }) { "Output directory is not empty" }
-        atomicWrite(identityPath, expectedIdentity)
-    }
-    require(!Files.exists(output.resolve("result.json"))) { "Cell already completed" }
+    return CoverageCellRequest(source = source, identity = identity, output = output)
+}
 
+private fun loadOrRunCoverageSearch(
+    source: CallsCoverageSource,
+    identity: CallsCoverageCellIdentity,
+    output: Path,
+    searchFunction: (CallsCoverageSearchRequest) -> CallsCoverageSearchResult,
+): CallsCoverageSearchResult {
     val candidatePath = output.resolve("candidates.jsonl")
     val searchPath = output.resolve("search.json")
-    val search = if (Files.exists(searchPath)) {
+
+    return if (Files.exists(searchPath)) {
         CallsExperimentJson.json.decodeFromString<CallsCoverageSearchResult>(Files.readString(searchPath))
     } else {
         require(!Files.exists(candidatePath)) { "Interrupted search requires investigation before restart" }
         source.verifyUnchanged()
         val request = CallsCoverageSearchRequest(
             sourceRoot = source.sourceRoot,
-            project = project,
-            function = function,
-            profile = profile,
-            frozenModelIds = manifest.modelSet.ids,
+            project = source.project,
+            function = source.function,
+            profile = identity.profile,
+            frozenModelIds = source.manifest.modelSet.ids,
             expectedNativeFrontendRevision = identity.nativeFrontendRevision,
-            seed = seed,
-            budget = budgetMillis.milliseconds,
-            solverQueryLimit = solverLimitMillis.milliseconds,
-            candidateCap = candidateCap,
+            seed = identity.seed,
+            budget = identity.budgetMillis.milliseconds,
+            solverQueryLimit = identity.solverLimitMillis.milliseconds,
+            candidateCap = identity.candidateCap,
             onCandidate = { candidate -> appendDurably(candidatePath, encode(candidate)) },
         )
         val result = searchFunction(request)
@@ -130,7 +183,13 @@ internal fun runCoverageCell(
         atomicWrite(searchPath, encode(result))
         result
     }
+}
 
+private fun replayCoverageCandidates(
+    source: CallsCoverageSource,
+    search: CallsCoverageSearchResult,
+    output: Path,
+): List<CallsCoverageReplayEvent> {
     val replayPath = output.resolve("replays.jsonl")
     val events = readLines<CallsCoverageReplayEvent>(replayPath).toMutableList()
     require(events.map(CallsCoverageReplayEvent::index) == events.indices.toList()) {
@@ -140,7 +199,7 @@ internal fun runCoverageCell(
     if (search.candidates.isNotEmpty()) {
         OriginalTypeScriptCoverageReplayer(
             sourceRoot = source.sourceRoot,
-            function = function,
+            function = source.function,
         ).use { replayer ->
             search.candidates.indices.drop(events.size).forEach { index ->
                 val candidate = search.candidates[index]
@@ -160,32 +219,26 @@ internal fun runCoverageCell(
         }
     }
 
-    source.verifyUnchanged()
-    val checkpoints = listOf(30_000L, 60_000L, 120_000L).filter { it <= budgetMillis }.map { checkpoint ->
-        val indices = search.candidates.indices.filter { index ->
-            search.candidates[index].emittedAtMillis <= checkpoint
-        }
-        val replayed = indices.mapNotNull { index -> events[index].replay }
-        CallsCoverageCheckpoint(
-            searchBudgetMillis = checkpoint,
-            emittedCandidates = indices.size,
-            replayedCandidates = replayed.size,
-            coveredStatements = replayed.flatMap { it.coveredStatementKeys }.toSet().size,
-            coveredIfArms = replayed.flatMap { it.coveredIfArmKeys }.toSet().size,
-        )
+    return events
+}
+
+private fun coverageCheckpoints(
+    search: CallsCoverageSearchResult,
+    events: List<CallsCoverageReplayEvent>,
+    budgetMillis: Long,
+): List<CallsCoverageCheckpoint> = COVERAGE_CHECKPOINT_MILLIS.filter { it <= budgetMillis }.map { checkpoint ->
+    val indices = search.candidates.indices.filter { index ->
+        search.candidates[index].emittedAtMillis <= checkpoint
     }
-    val result = CallsCoverageCellResult(
-        identity = identity,
-        search = search,
-        replayErrors = events.count { it.error != null },
-        completionMismatches = events.indices.count { index ->
-            events[index].replay?.completion != null &&
-                events[index].replay?.completion != search.candidates[index].completion
-        },
-        checkpoints = checkpoints,
+    val replayed = indices.mapNotNull { index -> events[index].replay }
+
+    CallsCoverageCheckpoint(
+        searchBudgetMillis = checkpoint,
+        emittedCandidates = indices.size,
+        replayedCandidates = replayed.size,
+        coveredStatements = replayed.flatMap { it.coveredStatementKeys }.toSet().size,
+        coveredIfArms = replayed.flatMap { it.coveredIfArmKeys }.toSet().size,
     )
-    atomicWrite(output.resolve("result.json"), encode(result))
-    println(encode(result))
 }
 
 private inline fun <reified T> readLines(path: Path): List<T> = if (Files.exists(path)) {
@@ -200,7 +253,12 @@ private inline fun <reified T> encode(value: T): String = CallsExperimentJson.js
 
 private fun appendDurably(path: Path, line: String) {
     val bytes = ByteBuffer.wrap((line + "\n").toByteArray(Charsets.UTF_8))
-    FileChannel.open(path, StandardOpenOption.CREATE, StandardOpenOption.WRITE, StandardOpenOption.APPEND).use { channel ->
+    FileChannel.open(
+        path,
+        StandardOpenOption.CREATE,
+        StandardOpenOption.WRITE,
+        StandardOpenOption.APPEND,
+    ).use { channel ->
         while (bytes.hasRemaining()) channel.write(bytes)
         channel.force(true)
     }
@@ -213,4 +271,13 @@ private fun atomicWrite(path: Path, contents: String) {
     Files.move(temporary, path, StandardCopyOption.ATOMIC_MOVE)
 }
 
+private const val COVERAGE_CELL_ARGUMENT_COUNT = 9
 private const val REPLAY_TIMEOUT_MILLIS = 20_000L
+private const val FIRST_CHECKPOINT_MILLIS = 30_000L
+private const val SECOND_CHECKPOINT_MILLIS = 60_000L
+private const val THIRD_CHECKPOINT_MILLIS = 120_000L
+private val COVERAGE_CHECKPOINT_MILLIS = listOf(
+    FIRST_CHECKPOINT_MILLIS,
+    SECOND_CHECKPOINT_MILLIS,
+    THIRD_CHECKPOINT_MILLIS,
+)
diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt
index be888d1564..eec5990326 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt
@@ -10,11 +10,11 @@ import org.usvm.ts.pbt.backend.SourceFileCoverage
 import org.usvm.ts.pbt.fastcheck.FastCheckBackend
 import org.usvm.ts.pbt.fastcheck.FastCheckRuntime
 import org.usvm.ts.pbt.fastcheck.TypeScriptSourceInspector
-import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.BooleanDomain
-import org.usvm.ts.pbt.model.PropertyInput
+import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyId
+import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.TypeScriptEntryPoint
 import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.file.Files
@@ -54,38 +54,45 @@ internal class OriginalTypeScriptCoverageReplayer(
     private val backend: FastCheckBackend
 
     init {
-        try {
-            require(function.entryPoint.executionKind == org.usvm.ts.pbt.model.ExecutionKind.SYNC) {
-                "Coverage replay requires a synchronous entry point"
-            }
-            val source = this.sourceRoot.resolve(function.sourceFile).normalize()
-            require(source.startsWith(this.sourceRoot) && Files.isRegularFile(source)) {
-                "Coverage entry source is outside its frozen root"
-            }
-            val closure = TypeScriptSourceInspector.localSourceClosure(sourceRoot = this.sourceRoot, source = source)
-            require(closure.reasonCode == null) { closure.diagnostic ?: "Unsupported local source closure" }
-            allowedFiles = closure.files.toSet()
-
-            Files.createDirectory(overlayRoot)
-            Files.newDirectoryStream(this.sourceRoot).use { entries ->
-                entries.forEach { entry ->
-                    Files.createSymbolicLink(overlayRoot.resolve(entry.fileName), entry.toAbsolutePath())
-                }
-            }
-            Files.writeString(
-                overlayRoot.resolve(wrapperName),
-                coverageWrapper(
-                    sourceFile = function.sourceFile,
-                    exportName = function.entryPoint.exportName,
-                    observationPath = observationPath,
-                    dropSentinel = usesSentinel,
-                ),
-            )
-            backend = FastCheckBackend(sourceRoots = listOf(overlayRoot, this.sourceRoot))
-        } catch (error: Throwable) {
+        val setup = runCatching { prepareReplay() }.getOrElse { error ->
             deleteWorkspace()
             throw error
         }
+        allowedFiles = setup.allowedFiles
+        backend = setup.backend
+    }
+
+    private fun prepareReplay(): CoverageReplaySetup {
+        require(function.entryPoint.executionKind == org.usvm.ts.pbt.model.ExecutionKind.SYNC) {
+            "Coverage replay requires a synchronous entry point"
+        }
+        val source = sourceRoot.resolve(function.sourceFile).normalize()
+        require(source.startsWith(sourceRoot) && Files.isRegularFile(source)) {
+            "Coverage entry source is outside its frozen root"
+        }
+        val closure = TypeScriptSourceInspector.localSourceClosure(sourceRoot = sourceRoot, source = source)
+        require(closure.reasonCode == null) { closure.diagnostic ?: "Unsupported local source closure" }
+
+        Files.createDirectory(overlayRoot)
+        Files.newDirectoryStream(sourceRoot).use { entries ->
+            entries.forEach { entry ->
+                Files.createSymbolicLink(overlayRoot.resolve(entry.fileName), entry.toAbsolutePath())
+            }
+        }
+        Files.writeString(
+            overlayRoot.resolve(wrapperName),
+            coverageWrapper(
+                sourceFile = function.sourceFile,
+                exportName = function.entryPoint.exportName,
+                observationPath = observationPath,
+                dropSentinel = usesSentinel,
+            ),
+        )
+
+        return CoverageReplaySetup(
+            allowedFiles = closure.files.toSet(),
+            backend = FastCheckBackend(sourceRoots = listOf(overlayRoot, sourceRoot)),
+        )
     }
 
     fun replay(inputs: List<JsConcreteValue>, timeoutMillis: Long): CallsCoverageReplayResult {
@@ -170,6 +177,11 @@ internal class OriginalTypeScriptCoverageReplayer(
     }
 }
 
+private data class CoverageReplaySetup(
+    val allowedFiles: Set<String>,
+    val backend: FastCheckBackend,
+)
+
 private fun collectHits(
     relative: String,
     file: SourceFileCoverage,
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 d47c253cc9..aaf6981225 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
@@ -136,17 +136,7 @@ internal class CurrentTsCallsCoverageEngine(
         } else {
             TsUnknownCallModelSelection.Only(emptySet())
         }
-        val machineOptions = UMachineOptions(
-            pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY),
-            stateCollectionStrategy = StateCollectionStrategy.COVERED_NEW,
-            randomSeed = request.seed,
-            timeout = request.budget,
-            solverTimeout = request.solverQueryLimit,
-            solverType = SolverType.Z3,
-            stopOnCoverage = CALLS_STOP_ON_COVERAGE,
-            stopOnTargetsReached = false,
-            throwExceptionOnStepFailure = true,
-        )
+        val machineOptions = coverageMachineOptions(request)
         val machineResult = runCatching {
             TsMachine(
                 scene = preparation.scene,
@@ -187,6 +177,19 @@ internal class CurrentTsCallsCoverageEngine(
             diagnostic = machineResult.exceptionOrNull()?.let { error -> error.message ?: error::class.java.name },
         )
     }
+
+    private fun coverageMachineOptions(request: CallsCoverageSearchRequest): UMachineOptions =
+        UMachineOptions(
+            pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY),
+            stateCollectionStrategy = StateCollectionStrategy.COVERED_NEW,
+            randomSeed = request.seed,
+            timeout = request.budget,
+            solverTimeout = request.solverQueryLimit,
+            solverType = SolverType.Z3,
+            stopOnCoverage = CALLS_STOP_ON_COVERAGE,
+            stopOnTargetsReached = false,
+            throwExceptionOnStepFailure = true,
+        )
 }
 
 private class CompletedCoverageCandidateObserver(
@@ -216,8 +219,12 @@ private class CompletedCoverageCandidateObserver(
                 if (result.method != method) return
                 CallsCoverageCompletion.RETURNED
             }
-            is TsMethodResult.TsException -> CallsCoverageCompletion.THREW
-            else -> return
+            is TsMethodResult.TsException -> {
+                CallsCoverageCompletion.THREW
+            }
+            else -> {
+                return
+            }
         }
         val pathStatements = state.pathNode.allStatements.filterTo(hashSetOf()) { statement ->
             statement in entryStatements
diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSource.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSource.kt
index 7f9ba56ecb..9dff8e1998 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSource.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSource.kt
@@ -34,6 +34,8 @@ internal class CallsCoverageSource private constructor(
     }
 
     companion object {
+        private const val UNSIGNED_BYTE_MASK = 0xff
+
         fun load(manifestPath: Path, projectIndex: Int, functionIndex: Int): CallsCoverageSource {
             val realManifestPath = manifestPath.toRealPath()
             val manifestBytes = Files.readAllBytes(realManifestPath)
@@ -59,6 +61,6 @@ internal class CallsCoverageSource private constructor(
         }
 
         private fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256").digest(bytes)
-            .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and 0xff) }
+            .joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and UNSIGNED_BYTE_MASK) }
     }
 }
diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt
index 936aa91c2d..868987148f 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt
@@ -101,7 +101,7 @@ private fun TsState.materializeCallsConstant(value: JsConcreteValue): UExpr<*> =
         is JsConcreteValue.String -> mkInitializedStringConstant(value.value)
         JsConcreteValue.Null -> mkTsNullValue()
         JsConcreteValue.Undefined -> mkUndefinedValue()
-        is JsConcreteValue.Array -> error("Array constants are not primitive domains")
+        is JsConcreteValue.Array, is JsConcreteValue.Object -> error("Structured constants are not primitive domains")
     }
 }
 
@@ -161,7 +161,9 @@ private fun PropertyDomain.callsRuntimeType(): EtsType = when (this) {
             is JsConcreteValue.String -> EtsStringType
             JsConcreteValue.Null -> EtsNullType
             JsConcreteValue.Undefined -> EtsUndefinedType
-            is JsConcreteValue.Array -> error("Array constants are not primitive domains")
+            is JsConcreteValue.Array, is JsConcreteValue.Object -> error(
+                "Structured constants are not primitive domains",
+            )
         }
     }
     else -> {
diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt
index 749f1be17a..2bb749d0b2 100644
--- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt
+++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt
@@ -19,7 +19,7 @@ import org.usvm.util.mkRegisterStackLValue
 
 internal fun PropertyDomain.isSupportedCallsSymbolicDomain(): Boolean = when (this) {
     BooleanDomain, is IntegerDomain, is NumberDomain, is StringDomain -> true
-    is ConstantDomain -> value !is JsConcreteValue.Array
+    is ConstantDomain -> value !is JsConcreteValue.Array && value !is JsConcreteValue.Object
     is OptionalDomain -> value.isSupportedCallsSymbolicDomain() &&
         (nil == JsConcreteValue.Null || nil == JsConcreteValue.Undefined)
     is ArrayDomain -> element.isSupportedCallsSymbolicDomain()
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 4d919a200b..ceae9dffce 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
@@ -237,7 +237,11 @@ internal class CurrentTsCallsSymbolicEngine(
                 diagnostic = buildList {
                     addAll(analysis.unsupportedPaths)
                     if (interpreterObserver.runtimeLimitations.isNotEmpty()) {
-                        add(interpreterObserver.runtimeLimitations.joinToString(prefix = "Runtime feature limitations: "))
+                        add(
+                            interpreterObserver.runtimeLimitations.joinToString(
+                                prefix = "Runtime feature limitations: ",
+                            ),
+                        )
                     }
                 }.joinToString().ifEmpty { null },
             )
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 724e81eb38..4b178bdf0f 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,10 +1,10 @@
 package org.usvm.ts.calls
 
 import org.junit.jupiter.api.io.TempDir
-import org.usvm.ts.pbt.model.BooleanDomain
 import org.usvm.ts.pbt.model.ArrayDomain
-import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.BooleanDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.NumberDomain
 import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.StringDomain
 import org.usvm.ts.pbt.model.TypeScriptEntryPoint
@@ -84,10 +84,12 @@ class CallsCoverageExperimentTest {
         val fixture = fixture(
             source = "export function replace(values: number[]): number { values[0] = 2; return values[0]; }",
             exportName = "replace",
-            inputs = listOf(PropertyInput(
-                name = "values",
-                domain = ArrayDomain(element = NumberDomain(), minLength = 1, maxLength = 1),
-            )),
+            inputs = listOf(
+                PropertyInput(
+                    name = "values",
+                    domain = ArrayDomain(element = NumberDomain(), minLength = 1, maxLength = 1),
+                ),
+            ),
         )
         val inputs = listOf(JsConcreteValue.Array(listOf(JsConcreteValue.number(1.0))))
 
@@ -118,10 +120,12 @@ class CallsCoverageExperimentTest {
                 }
             """.trimIndent(),
             exportName = "replace",
-            inputs = listOf(PropertyInput(
-                name = "values",
-                domain = ArrayDomain(element = NumberDomain(), minLength = 1, maxLength = 1),
-            )),
+            inputs = listOf(
+                PropertyInput(
+                    name = "values",
+                    domain = ArrayDomain(element = NumberDomain(), minLength = 1, maxLength = 1),
+                ),
+            ),
         )
         val inputs = listOf(JsConcreteValue.Array(listOf(JsConcreteValue.number(1.0))))
 
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 f04103e0af..4fb5cb5f1b 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
@@ -40,13 +40,11 @@ class CallsCoverageSourceTest {
         val original = fixture.source.manifest
         val project = fixture.source.project
         val function = fixture.source.function
+        val changedExport = function.copy(entryPoint = function.entryPoint.copy(exportName = "second"))
+        val changedInputs = function.copy(inputs = listOf(PropertyInput(name = "flag", domain = NumberDomain())))
         val mutations = listOf(
-            original.copy(projects = listOf(project.copy(functions = listOf(
-                function.copy(entryPoint = function.entryPoint.copy(exportName = "second")),
-            )))),
-            original.copy(projects = listOf(project.copy(functions = listOf(
-                function.copy(inputs = listOf(PropertyInput(name = "flag", domain = NumberDomain()))),
-            )))),
+            original.copy(projects = listOf(project.copy(functions = listOf(changedExport)))),
+            original.copy(projects = listOf(project.copy(functions = listOf(changedInputs)))),
             original.copy(modelSet = original.modelSet.copy(ids = setOf("ts.array.includes"))),
         )
 
@@ -68,7 +66,9 @@ class CallsCoverageSourceTest {
         runCallsGit(fixture.source.sourceRoot, "add", "Fixture.ts")
         runCallsGit(fixture.source.sourceRoot, "commit", "-m", "Change source")
         val newRevision = runCallsGit(fixture.source.sourceRoot, "rev-parse", "HEAD").trim()
-        val changed = fixture.source.manifest.copy(projects = listOf(fixture.source.project.copy(revision = newRevision)))
+        val changed = fixture.source.manifest.copy(
+            projects = listOf(fixture.source.project.copy(revision = newRevision)),
+        )
         Files.writeString(fixture.manifestPath, CallsExperimentJson.encodeManifest(changed))
 
         val failure = assertFailsWith<IllegalArgumentException> { fixture.runCell() }
@@ -119,7 +119,9 @@ class CallsCoverageSourceTest {
     fun `manifest edit between search and replay is detected by the frozen source guard`() {
         val fixture = fixture()
         fixture.persistSearch()
-        val changed = fixture.source.manifest.copy(modelSet = fixture.source.manifest.modelSet.copy(ids = setOf("other")))
+        val changed = fixture.source.manifest.copy(
+            modelSet = fixture.source.manifest.modelSet.copy(ids = setOf("other")),
+        )
         Files.writeString(fixture.manifestPath, CallsExperimentJson.encodeManifest(changed))
 
         val failure = assertFailsWith<IllegalArgumentException> { fixture.source.verifyUnchanged() }
@@ -193,15 +195,33 @@ class CallsCoverageSourceTest {
                 solverLimitMillis = 1_000L,
                 candidateCap = 8,
             )
-            Files.writeString(output.resolve("identity.json"), CallsExperimentJson.json.encodeToUtf8SafeString(identity))
-            Files.writeString(output.resolve("search.json"), CallsExperimentJson.json.encodeToUtf8SafeString(emptySearch))
+            Files.writeString(
+                output.resolve("identity.json"),
+                CallsExperimentJson.json.encodeToUtf8SafeString(identity),
+            )
+            Files.writeString(
+                output.resolve("search.json"),
+                CallsExperimentJson.json.encodeToUtf8SafeString(emptySearch),
+            )
         }
 
         fun runCell(
-            searchFunction: (CallsCoverageSearchRequest) -> CallsCoverageSearchResult = { error("Must resume persisted search") },
+            searchFunction: (CallsCoverageSearchRequest) -> CallsCoverageSearchResult = {
+                error("Must resume persisted search")
+            },
         ) {
             runCoverageCell(
-                args = listOf(manifestPath.toString(), "0", "0", "EMPTY_STOP", "17", output.toString(), "30000", "1000", "8"),
+                args = listOf(
+                    manifestPath.toString(),
+                    "0",
+                    "0",
+                    "EMPTY_STOP",
+                    "17",
+                    output.toString(),
+                    "30000",
+                    "1000",
+                    "8",
+                ),
                 runtimeToolRevision = TOOL_REVISION,
                 runtimeNativeFrontendRevision = FRONTEND_REVISION,
                 searchFunction = searchFunction,
diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt
index 7d8482e484..c99529c8fa 100644
--- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt
+++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsLocalSourceClosureTest.kt
@@ -207,5 +207,4 @@ internal class CallsLocalSourceClosureTest : CurrentTsCallsSymbolicEngineTestSup
         returnExpression = "helper(value)",
         dependencies = mapOf("helper.ts" to dependency),
     )
-
 }
diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt
index d8add601ba..97d0e87356 100644
--- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt
+++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt
@@ -1,9 +1,12 @@
 package org.usvm.ts.calls
 
 import org.usvm.ts.pbt.model.ArrayDomain
+import org.usvm.ts.pbt.model.ConstantDomain
+import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.JsNumber
 import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.PropertyInput
 import kotlin.test.Test
 import kotlin.test.assertEquals
@@ -12,6 +15,47 @@ import kotlin.test.assertNotNull
 import kotlin.test.assertTrue
 
 internal class CurrentTsCallsInputDomainsTest : CurrentTsCallsSymbolicEngineTestSupport() {
+    @Test
+    fun `object input domains are rejected before symbolic materialization`() {
+        val fixture = fixture(
+            source = """
+                export function objectInput(value: any): boolean {
+                  if (typeof value === "object") {
+                    return true;
+                  }
+                  return false;
+                }
+            """.trimIndent(),
+            exportName = "objectInput",
+            inputs = listOf(
+                PropertyInput(
+                    name = "value",
+                    domain = ObjectDomain(fields = mapOf("count" to IntegerDomain(min = 0, max = 1))),
+                ),
+            ),
+            targetStatement = "return true;",
+        )
+
+        val preflight = fixture.preflight()
+        val result = fixture.search(modelIds = emptySet())
+
+        assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, preflight.status, preflight.toString())
+        assertEquals(CallsSymbolicPreflightReasonCode.INPUT_DOMAIN_UNSUPPORTED, preflight.reasonCode)
+        assertEquals(CallsSymbolicStatus.UNSUPPORTED, result.status, result.toString())
+    }
+
+    @Test
+    fun `structured constants remain outside primitive symbolic domains`() {
+        val constant = ConstantDomain(value = JsConcreteValue.Object(fields = emptyMap()))
+        val inputs = listOf(PropertyInput(name = "value", domain = constant))
+
+        val diagnostic = callsSymbolicInputPreflight(inputs)
+
+        assertTrue(!constant.isSupportedCallsSymbolicDomain())
+        assertNotNull(diagnostic)
+        assertTrue(diagnostic.contains("value"))
+    }
+
     @Test
     fun `singleton zero input domain preserves a negative zero witness`() {
         val fixture = fixture(
diff --git a/usvm-ts-fast-check/fast-check-adapter/package.json b/usvm-ts-fast-check/fast-check-adapter/package.json
index f27cceecb5..6764b2e13b 100644
--- a/usvm-ts-fast-check/fast-check-adapter/package.json
+++ b/usvm-ts-fast-check/fast-check-adapter/package.json
@@ -9,7 +9,7 @@
     "build": "tsc --project tsconfig.json",
     "pretest": "npm run build",
     "test": "npm run test:compiled",
-    "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js"
+    "test:compiled": "node --test dist/test/coverage-branches.test.js dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/observe-object.test.js dist/test/process-group-shutdown.test.js dist/test/process-supervisor.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/source-replay.test.js dist/test/source-captures.test.js dist/test/local-source-closure.test.js"
   },
   "dependencies": {
     "@jridgewell/trace-mapping": "0.3.31",
diff --git a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts
index 37be28fd61..fba52cc37a 100644
--- a/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/src/diagnostics.ts
@@ -39,10 +39,12 @@ export const adapterDiagnostic = {
   domainNumberEmpty: invalidRequest('domain.number.empty'),
   domainIntegerBounds: invalidRequest('domain.integer.bounds'),
   domainLengthInvalid: invalidRequest('domain.length.invalid'),
+  domainObjectFieldsInvalid: invalidRequest('domain.object.fields'),
   jsValueInvalid: invalidRequest('js-value.invalid'),
   jsValueBooleanInvalid: invalidRequest('js-value.boolean.invalid'),
   jsValueStringInvalid: invalidRequest('js-value.string.invalid'),
   jsValueArrayInvalid: invalidRequest('js-value.array.invalid'),
+  jsValueObjectInvalid: invalidRequest('js-value.object.invalid'),
   jsValueKindUnknown: invalidRequest('js-value.kind.unknown'),
   jsValueTypeUnsupported: invalidRequest('js-value.type.unsupported'),
   jsNumberInvalid: invalidRequest('js-number.invalid'),
diff --git a/usvm-ts-fast-check/fast-check-adapter/src/js-value.ts b/usvm-ts-fast-check/fast-check-adapter/src/js-value.ts
index f7578c744e..4df60f1990 100644
--- a/usvm-ts-fast-check/fast-check-adapter/src/js-value.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/src/js-value.ts
@@ -1,3 +1,4 @@
+import { types } from 'node:util';
 import {
   adapterDiagnostic,
   type AdapterDiagnosticDescriptor,
@@ -10,7 +11,8 @@ export type JsConcreteValue =
   | boolean
   | string
   | number
-  | JsConcreteValue[];
+  | JsConcreteValue[]
+  | { [key: string]: JsConcreteValue };
 
 export type TaggedJsNumber =
   | { value: 'finite'; bits: string }
@@ -24,7 +26,8 @@ export type TaggedJsValue =
   | { kind: 'boolean'; value: boolean }
   | { kind: 'string'; value: string }
   | ({ kind: 'number' } & TaggedJsNumber)
-  | { kind: 'array'; elements: TaggedJsValue[] };
+  | { kind: 'array'; elements: TaggedJsValue[] }
+  | { kind: 'object'; fields: Record<string, TaggedJsValue> };
 
 export interface ProtocolDiagnostic {
   kind: AdapterDiagnosticKind;
@@ -92,6 +95,20 @@ export function decodeJsValue(value: unknown, path = 'value'): JsConcreteValue {
       return value.elements.map((element: unknown, index: number) =>
         decodeJsValue(element, `${path}.elements[${index}]`));
 
+    case 'object': {
+      const fields = value.fields;
+      if (fields === null || typeof fields !== 'object' || Array.isArray(fields)) {
+        throw protocolError(adapterDiagnostic.jsValueObjectInvalid, 'Object value must contain fields', path);
+      }
+
+      const entries = Object.entries(fields).map(([name, field]) => {
+        requireSafeObjectKey(name, `${path}.fields.${name}`);
+        return [name, decodeJsValue(field, `${path}.fields.${name}`)] as const;
+      });
+
+      return Object.fromEntries(entries);
+    }
+
     default:
       throw protocolError(
         adapterDiagnostic.jsValueKindUnknown,
@@ -102,20 +119,66 @@ export function decodeJsValue(value: unknown, path = 'value'): JsConcreteValue {
 }
 
 export function encodeJsValue(value: unknown): TaggedJsValue {
+  return encodeValue(value, new WeakSet());
+}
+
+function encodeValue(value: unknown, seen: WeakSet<object>): TaggedJsValue {
   if (value === undefined) return { kind: 'undefined' };
   if (value === null) return { kind: 'null' };
   if (typeof value === 'boolean') return { kind: 'boolean', value };
   if (typeof value === 'string') return { kind: 'string', value };
   if (typeof value === 'number') return { kind: 'number', ...encodeJsNumber(value) };
-  if (Array.isArray(value)) return { kind: 'array', elements: value.map(encodeJsValue) };
 
-  throw protocolError(
+  if (typeof value !== 'object' || types.isProxy(value) || seen.has(value)) {
+    throw unsupportedValue();
+  }
+  seen.add(value);
+  const isArray = Array.isArray(value);
+  const expectedPrototype = isArray ? Array.prototype : Object.prototype;
+  if (Object.getPrototypeOf(value) !== expectedPrototype || Object.getOwnPropertySymbols(value).length > 0) {
+    throw unsupportedValue();
+  }
+
+  if (isArray) {
+    const elements: TaggedJsValue[] = [];
+    for (let index = 0; index < value.length; index += 1) {
+      elements.push(encodeValue(ownDataValue(value, String(index)), seen));
+    }
+    if (Object.getOwnPropertyNames(value).length !== value.length + 1) throw unsupportedValue();
+
+    return { kind: 'array', elements };
+  }
+
+  const entries = Object.getOwnPropertyNames(value).map((name) => {
+    requireSafeObjectKey(name, `value.fields.${name}`);
+
+    return [name, encodeValue(ownDataValue(value, name), seen)] as const;
+  });
+
+  return { kind: 'object', fields: Object.fromEntries(entries) };
+}
+
+function ownDataValue(value: object, name: string): unknown {
+  const descriptor = Object.getOwnPropertyDescriptor(value, name);
+  if (descriptor === undefined || !descriptor.enumerable || !('value' in descriptor)) throw unsupportedValue();
+
+  return descriptor.value;
+}
+
+function unsupportedValue(): ProtocolError {
+  return protocolError(
     adapterDiagnostic.jsValueTypeUnsupported,
-    `Unsupported JavaScript value type: ${typeof value}`,
+    'Only primitive values, dense arrays, and plain own-data objects without aliases are supported',
     'value',
   );
 }
 
+function requireSafeObjectKey(name: string, path: string): void {
+  if (['__proto__', 'constructor', 'prototype'].includes(name)) {
+    throw protocolError(adapterDiagnostic.jsValueObjectInvalid, 'Unsupported object property name', path);
+  }
+}
+
 export function decodeJsNumber(taggedNumber: unknown, path = 'number'): number {
   requireObject(
     taggedNumber,
diff --git a/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts b/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts
index 2e7d7cea65..e6bac1b8c8 100644
--- a/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/src/observe-property.ts
@@ -262,7 +262,8 @@ function captureValue(
   }
 
   if (types.isProxy(value)) return { status: 'unsupported', reason: 'proxy' };
-  if (!Array.isArray(value)) return { status: 'unsupported', reason: 'unsupported-type' };
+  if (typeof value !== 'object' || value === null) return { status: 'unsupported', reason: 'unsupported-type' };
+  if (!Array.isArray(value)) return captureObject(value, maxArrayElements, seen, depth, budget);
   if (depth >= 4) return { status: 'unsupported', reason: 'depth-limit' };
   if (Object.getPrototypeOf(value) !== Array.prototype) return { status: 'unsupported', reason: 'array-prototype' };
   if (seen.has(value)) return { status: 'unsupported', reason: 'alias-or-cycle' };
@@ -290,11 +291,54 @@ function captureValue(
   // Inspect names only after the bounded value walk, rather than allocating every descriptor up front.
   const hasExtraProperty = Object.getOwnPropertyNames(value)
     .some((key) => key !== 'length' && !/^(0|[1-9]\d*)$/.test(key));
-  if (hasExtraProperty) return { status: 'unsupported', reason: 'array-extra-property' };
+  if (hasExtraProperty || Object.getOwnPropertySymbols(value).length > 0) {
+    return { status: 'unsupported', reason: 'array-extra-property' };
+  }
 
   return { status: 'captured', value: { kind: 'array', elements } };
 }
 
+function captureObject(
+  value: object,
+  maxArrayElements: number,
+  seen: WeakSet<object>,
+  depth: number,
+  budget: CaptureBudget,
+): CaptureResult {
+  if (depth >= 4) return { status: 'unsupported', reason: 'depth-limit' };
+  if (Object.getPrototypeOf(value) !== Object.prototype) return { status: 'unsupported', reason: 'object-prototype' };
+  if (seen.has(value)) return { status: 'unsupported', reason: 'alias-or-cycle' };
+
+  budget.remaining -= '{"kind":"object","fields":{}}'.length;
+  if (budget.remaining < 0) return { status: 'truncated', reason: 'byte-budget' };
+
+  seen.add(value);
+  const entries: Array<readonly [string, TaggedJsValue]> = [];
+  for (const name in value) {
+    const descriptor = Object.getOwnPropertyDescriptor(value, name);
+    if (descriptor === undefined) continue;
+    if (entries.length >= 32) return { status: 'unsupported', reason: 'object-field-limit' };
+    if (['__proto__', 'constructor', 'prototype'].includes(name)) {
+      return { status: 'unsupported', reason: 'object-property-name' };
+    }
+    if (!('value' in descriptor)) return { status: 'unsupported', reason: 'accessor' };
+
+    budget.remaining -= entries.length === 0 ? 1 : 2; // Colon and, after the first field, comma.
+    if (!reserveJsonString(name, budget)) return { status: 'truncated', reason: 'byte-budget' };
+    const captured = captureValue(descriptor.value, maxArrayElements, seen, depth + 1, budget);
+    if (captured.status !== 'captured') return captured;
+
+    entries.push([name, captured.value]);
+  }
+
+  // Reject properties the wire format cannot preserve, after the bounded value walk.
+  const hasHiddenProperties = Object.getOwnPropertyNames(value).length !== entries.length
+    || Object.getOwnPropertySymbols(value).length > 0;
+  if (hasHiddenProperties) return { status: 'unsupported', reason: 'object-hidden-property' };
+
+  return { status: 'captured', value: { kind: 'object', fields: Object.fromEntries(entries) } };
+}
+
 function reserveJsonString(value: string, budget: CaptureBudget): boolean {
   // Count the actual JSON UTF-8 cost without allocating its escaped representation.
   // Stop at the first excess: a large string or nested array never requires a full serialization.
diff --git a/usvm-ts-fast-check/fast-check-adapter/src/project-domain.ts b/usvm-ts-fast-check/fast-check-adapter/src/project-domain.ts
index 5be1ed72c8..f0cc7c1f91 100644
--- a/usvm-ts-fast-check/fast-check-adapter/src/project-domain.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/src/project-domain.ts
@@ -48,7 +48,7 @@ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary<Js
     case 'constant': {
       const value = decodeJsValue(domain.value, `${path}.value`);
 
-      if (Array.isArray(value)) {
+      if (value !== null && typeof value === 'object') {
         throw protocolError(
           adapterDiagnostic.domainConstantUnsupported,
           'Constant domains support JavaScript primitives only',
@@ -90,6 +90,14 @@ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary<Js
         maxLength: domain.maxLength,
       });
 
+    case 'object': {
+      const fields = requireObjectFields(domain.fields, path);
+      const arbitraries = Object.fromEntries(Object.entries(fields).map(([name, field]) =>
+        [name, projectDomain(field, `${path}.fields.${name}`)]));
+
+      return fc.record(arbitraries, { noNullPrototype: true });
+    }
+
     default:
       throw protocolError(
         adapterDiagnostic.domainKindUnknown,
@@ -99,6 +107,21 @@ export function projectDomain(domain: unknown, path = 'domain'): fc.Arbitrary<Js
   }
 }
 
+function requireObjectFields(fields: unknown, path: string): Record<string, unknown> {
+  const isRecord = fields !== null && typeof fields === 'object' && !Array.isArray(fields);
+  if (!isRecord) {
+    throw protocolError(adapterDiagnostic.domainObjectFieldsInvalid, 'Invalid object fields', `${path}.fields`);
+  }
+  const names = Object.keys(fields);
+  const invalidNames = names.length > 32
+    || names.some((name) => ['__proto__', 'constructor', 'prototype'].includes(name));
+  if (invalidNames) {
+    throw protocolError(adapterDiagnostic.domainObjectFieldsInvalid, 'Invalid object fields', `${path}.fields`);
+  }
+
+  return fields as Record<string, unknown>;
+}
+
 export function projectionCapability(domain: unknown, path = 'domain'): ProjectionCapability {
   try {
     projectDomain(domain, path);
diff --git a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts
index e37d2a5202..1e118f9d6c 100644
--- a/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/test/execute-property.test.ts
@@ -850,6 +850,32 @@ test('reports the original nested array when the predicate mutates its invocatio
   });
 });
 
+test('reports and replays the original plain object after nested mutation', async () => {
+  await withPropertyModule(async (sourceRoot) => {
+    const originalValue = { nested: { score: 1 } };
+    const request = executionRequest(sourceRoot, 'mutatesNestedObject', {
+      inputDomain: { kind: 'object', fields: {
+        nested: { kind: 'object', fields: { score: { kind: 'integer', min: 1, max: 1 } } },
+      } },
+    });
+    request.examples = [[encodeJsValue(originalValue)]];
+    enableObservation(request);
+
+    const response = await executeProperty(request);
+    const replay = await executeProperty({
+      ...request,
+      replayPath: response.result.replayPath ?? undefined,
+      seed: response.result.seed,
+    });
+
+    assert.equal(response.result.status, 'failure');
+    assert.deepEqual(response.result.counterexample, [encodeJsValue(originalValue)]);
+    assert.deepEqual(response.result.observations?.invocations[0]?.input,
+      { status: 'captured', value: encodeJsValue([originalValue]) });
+    assert.deepEqual(replay.result.counterexample, response.result.counterexample);
+  });
+});
+
 test('reports and replays the original array when the predicate creates a cycle', async () => {
   await withPropertyModule(async (sourceRoot) => {
     const originalValue = [1];
@@ -1026,6 +1052,12 @@ export function mutatesNestedArrayToObject(value: unknown[][]): boolean {
   return false;
 }
 
+export function mutatesNestedObject(value: { nested: { score: number } }): boolean {
+  value.nested.score = 2;
+
+  return false;
+}
+
 export function mutatesArrayToCycle(value: unknown[]): boolean {
   value[0] = value;
 
diff --git a/usvm-ts-fast-check/fast-check-adapter/test/js-value.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/js-value.test.ts
index 2cf1b03299..8676c44e2a 100644
--- a/usvm-ts-fast-check/fast-check-adapter/test/js-value.test.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/test/js-value.test.ts
@@ -43,6 +43,14 @@ test('tagged JavaScript primitives round trip without losing semantics', () => {
         && value[0] === undefined
         && Object.is(value[1], -0),
     },
+    {
+      tagged: {
+        kind: 'object',
+        fields: { score: { kind: 'number', value: 'finite', bits: '8000000000000000' } },
+      },
+      matches: (value) => value !== null && typeof value === 'object'
+        && !Array.isArray(value) && Object.is(value.score, -0),
+    },
   ];
 
   for (const { tagged, matches } of cases) {
@@ -80,3 +88,30 @@ test('finite tags reject nonfinite bit patterns at the tagged input boundary', (
 test('unknown tagged value kinds are rejected explicitly', () => {
   assert.throws(() => decodeJsValue({ kind: 'symbol' }), /js-value\.kind\.unknown/);
 });
+
+
+test('object transport refuses hooks and lossy property layouts', () => {
+  let calls = 0;
+  const accessor = Object.defineProperty({}, 'x', {
+    enumerable: true, get: () => { calls += 1; throw new Error('getter'); },
+  });
+  const nestedAccessor = Object.defineProperty([1], '0', {
+    enumerable: true, get: () => { calls += 1; throw new Error('getter'); },
+  });
+  const proxy = new Proxy({}, {
+    ownKeys: () => { calls += 1; throw new Error('proxy'); },
+  });
+  const shared = { x: 1 };
+  const invalid = [accessor, { array: nestedAccessor }, proxy, { a: shared, b: shared },
+    Object.defineProperty({}, 'hidden', { value: 1 }), { [Symbol('x')]: 1 }, Object.create(null)];
+
+  for (const value of invalid) assert.throws(() => encodeJsValue(value), /js-value\.type\.unsupported/);
+  assert.equal(calls, 0);
+});
+
+test('object transport rejects unsafe keys on decode without affecting Object prototype', () => {
+  const fields = Object.fromEntries([['__proto__', { kind: 'boolean', value: true }]]);
+
+  assert.throws(() => decodeJsValue({ kind: 'object', fields }), /js-value\.object\.invalid/);
+  assert.equal(Object.getPrototypeOf({}), Object.prototype);
+});
diff --git a/usvm-ts-fast-check/fast-check-adapter/test/observe-object.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/observe-object.test.ts
new file mode 100644
index 0000000000..47f53c6069
--- /dev/null
+++ b/usvm-ts-fast-check/fast-check-adapter/test/observe-object.test.ts
@@ -0,0 +1,109 @@
+import assert from 'node:assert/strict';
+import test from 'node:test';
+import { encodeJsValue } from '../src/js-value.js';
+import { ObservationRecorder, type ObservationRequest } from '../src/observe-property.js';
+import { stringifyProtocolJson } from '../src/protocol-json.js';
+
+const request: ObservationRequest = {
+  points: [], sources: [], maxInvocations: 1, maxPointsPerInvocation: 1,
+  maxArrayElements: 32, maxBytes: 4096,
+};
+
+function capture(value: unknown, limits = request) {
+  const recorder = new ObservationRecorder('objects', limits);
+
+  const returned = recorder.run([value], 'unknown', () => value);
+
+  assert.equal(returned, value);
+  assert.ok(Buffer.byteLength(stringifyProtocolJson(recorder.result), 'utf8') <= limits.maxBytes);
+
+  return recorder.result.invocations[0]?.input;
+}
+
+test('object observations preserve nested special values before mutation', () => {
+  const value = { x: -0, nested: { values: [Number.NaN, undefined, '\ud800'] } };
+  const expected = encodeJsValue([value]);
+
+  const observed = capture(value);
+  value.nested.values[0] = 42;
+
+  assert.deepEqual(observed, { status: 'captured', value: expected });
+});
+
+test('object observations refuse accessors and proxies without running their hooks', () => {
+  let hookCalls = 0;
+  const accessor = Object.defineProperty({}, 'x', {
+    enumerable: true, get: () => { hookCalls += 1; throw new Error('getter'); },
+  });
+  const proxy = new Proxy({}, {
+    ownKeys: () => { hookCalls += 1; throw new Error('proxy'); },
+    getPrototypeOf: () => { hookCalls += 1; throw new Error('proxy'); },
+  });
+
+  assert.deepEqual(capture(accessor), { status: 'unsupported', reason: 'accessor' });
+  assert.deepEqual(capture(proxy), { status: 'unsupported', reason: 'proxy' });
+  assert.equal(hookCalls, 0);
+});
+
+test('object observations reject lossy keys, prototypes, aliases, and cycles', () => {
+  const shared = { x: 1 };
+  const cycle: { self?: unknown } = {};
+  cycle.self = cycle;
+  const hidden = Object.defineProperty({}, 'x', { value: 1 });
+  const symbol = { [Symbol('x')]: 1 };
+  const unsafe = Object.fromEntries([['__proto__', 1]]);
+  const cases: Array<[unknown, string]> = [
+    [{ a: shared, b: shared }, 'alias-or-cycle'],
+    [cycle, 'alias-or-cycle'],
+    [hidden, 'object-hidden-property'],
+    [symbol, 'object-hidden-property'],
+    [unsafe, 'object-property-name'],
+    [Object.create(null), 'object-prototype'],
+    [new (class C { x = 1; })(), 'object-prototype'],
+  ];
+
+  for (const [value, reason] of cases) {
+    assert.deepEqual(capture(value), { status: 'unsupported', reason });
+  }
+});
+
+test('object capture accounts for escaped field names and stops before later values', () => {
+  const limits = { ...request, maxBytes: 1024 };
+  const oversizedName = Object.fromEntries([['\u0000'.repeat(1000), 1]]);
+  let getterCalls = 0;
+  const oversizedValue = Object.defineProperty({ first: ['x'.repeat(262_144)] }, 'later', {
+    enumerable: true, get: () => { getterCalls += 1; throw new Error('getter'); },
+  });
+
+  for (const value of [oversizedName, oversizedValue]) {
+    assert.deepEqual(capture(value, limits), { status: 'truncated', reason: 'byte-budget' });
+  }
+  assert.equal(getterCalls, 0);
+});
+
+test('object observations enforce field count and mixed collection depth', () => {
+  const manyFields = Object.fromEntries(Array.from({ length: 33 }, (_, index) => [`x${index}`, 1]));
+  const deepValue = { a: [{ b: { c: 1 } }] };
+
+  assert.deepEqual(capture(manyFields), { status: 'unsupported', reason: 'object-field-limit' });
+  assert.deepEqual(capture(deepValue), { status: 'unsupported', reason: 'depth-limit' });
+});
+
+test('object observation serialization ignores inherited toJSON', () => {
+  const original = Object.getOwnPropertyDescriptor(Object.prototype, 'toJSON');
+  let calls = 0;
+  try {
+    Object.defineProperty(Object.prototype, 'toJSON', {
+      configurable: true,
+      value: () => { calls += 1; throw new Error('toJSON'); },
+    });
+
+    const observed = capture({ x: { y: -0 } });
+
+    assert.equal(observed?.status, 'captured');
+    assert.equal(calls, 0);
+  } finally {
+    if (original === undefined) delete (Object.prototype as { toJSON?: unknown }).toJSON;
+    else Object.defineProperty(Object.prototype, 'toJSON', original);
+  }
+});
diff --git a/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts
index 992f9c4d2d..865a373e63 100644
--- a/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/test/project-domain.test.ts
@@ -96,6 +96,17 @@ interface ProjectionCase {
 }
 
 const projectionCases: ProjectionCase[] = [
+  {
+    name: 'plain object',
+    domain: { kind: 'object', fields: { score: { kind: 'integer', min: 0, max: 3 }, enabled: { kind: 'boolean' } } },
+    matches: (value) => {
+      if (value === null || typeof value !== 'object' || Array.isArray(value)) return false;
+      const fields = value as Record<string, unknown>;
+      return Object.getPrototypeOf(value) === Object.prototype
+        && typeof fields.enabled === 'boolean' && typeof fields.score === 'number'
+        && fields.score >= 0 && fields.score <= 3;
+    },
+  },
   {
     name: 'boolean',
     domain: { kind: 'boolean' },
@@ -161,15 +172,15 @@ test('fast-check capability is exact for supported recursive domains', () => {
 });
 
 test('unknown domain kinds are rejected and reported as unsupported', () => {
-  assert.throws(() => projectDomain({ kind: 'object' }), /domain\.kind\.unknown/);
+  assert.throws(() => projectDomain({ kind: 'symbol' }), /domain\.kind\.unknown/);
 
   assert.deepEqual(
-    projectionCapability({ kind: 'object' }, 'inputs[0].domain'),
+    projectionCapability({ kind: 'symbol' }, 'inputs[0].domain'),
     {
       level: 'unsupported',
       diagnostics: [{
         code: 'domain.kind.unknown',
-        message: 'Unknown property domain kind: object',
+        message: 'Unknown property domain kind: symbol',
         path: 'inputs[0].domain',
       }],
     },
@@ -211,3 +222,17 @@ function taggedNumber(value: number): { value: 'finite'; bits: string } {
 
   return { value: 'finite', bits: view.getBigUint64(0, false).toString(16).padStart(16, '0') };
 }
+
+
+test('plain object domains reject unsafe keys and oversized shapes', () => {
+  const invalidFields = [
+    Object.fromEntries([['__proto__', { kind: 'boolean' }]]),
+    Object.fromEntries(Array.from({ length: 33 }, (_, index) => [`x${index}`, { kind: 'boolean' }])),
+  ];
+
+  for (const fields of invalidFields) {
+    assert.throws(() => projectDomain({ kind: 'object', fields }), /domain\.object\.fields/);
+  }
+  assert.throws(() => projectDomain({ kind: 'constant', value: { kind: 'object', fields: {} } }),
+    /domain\.constant\.unsupported/);
+});
diff --git a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt
index be529c822b..17978ced59 100644
--- a/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt
+++ b/usvm-ts-fast-check/src/test/kotlin/org/usvm/ts/pbt/usvm/PropertyExecutionConformanceTest.kt
@@ -18,6 +18,7 @@ import org.usvm.ts.pbt.mapping.PropertyEtsMapper
 import org.usvm.ts.pbt.model.ArrayDomain
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyId
 import org.usvm.ts.pbt.model.PropertyInput
@@ -143,6 +144,38 @@ class PropertyExecutionConformanceTest {
         assertEquals(symbolicInputs, replay.counterexample)
     }
 
+    @Test
+    fun `plain object symbolic candidates replay with their entry values`() {
+        val domain = ObjectDomain(mapOf("count" to IntegerDomain(min = 0, max = 2)))
+        val property = property(predicateExport = "mutatesObjectAndFails", domain = domain)
+        val manifest = property.toManifest()
+
+        val search = searcher.search(manifest, mapper.map(manifest), exactCapability)
+        val inputs = assertNotNull(search.inputs, search.toString())
+        val replay = backend.run(
+            property = property,
+            configuration = configuration.copy(examples = listOf(inputs)),
+        )
+
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, search.status, search.toString())
+        assertEquals(listOf(JsConcreteValue.Object(mapOf("count" to JsConcreteValue.number(2.0)))), inputs)
+        assertEquals(PropertyFailureKind.PROPERTY, replay.failure?.kind)
+        assertEquals(inputs, replay.counterexample)
+    }
+
+    @Test
+    fun `plain object class annotations have the same runtime identity in both backends`() {
+        val domain = ObjectDomain(mapOf("count" to IntegerDomain(min = 0, max = 2)))
+        val property = property(predicateExport = "plainAnnotatedObject", domain = domain)
+        val manifest = property.toManifest()
+
+        val search = searcher.search(manifest, mapper.map(manifest), exactCapability)
+        val concrete = backend.run(property, configuration)
+
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, search.status, search.toString())
+        assertEquals(PropertyRunStatus.SUCCESS, concrete.status)
+    }
+
     private fun concreteOutcome(
         property: PropertyDefinition,
         expectedBackendError: BackendErrorExpectation?,
diff --git a/usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts b/usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts
index 3ce5d3016d..0b663e437d 100644
--- a/usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts
+++ b/usvm-ts-fast-check/src/test/resources/properties/contract/PropertyExecutionContract.ts
@@ -160,3 +160,19 @@ export function mutatesAndFails(value: number[]): boolean {
 
     return false;
 }
+
+
+class AnnotatedRecord {
+    count: number = 0;
+    absent: () => number = () => 10;
+}
+
+export function mutatesObjectAndFails(value: { count: number }): boolean {
+    const before = value.count;
+    value.count += 1;
+    return before !== 2;
+}
+
+export function plainAnnotatedObject(value: AnnotatedRecord): boolean {
+    return !(value instanceof AnnotatedRecord) && value.absent === undefined;
+}
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt
index 1d3257e617..834f33602e 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/PbtDiagnosticCode.kt
@@ -53,6 +53,7 @@ internal object PbtDiagnosticCode {
     const val INPUT_NAME_DUPLICATE = "input.name.duplicate"
     const val INPUT_NAME_INVALID = "input.name.invalid"
     const val DOMAIN_ARRAY_LENGTH = "domain.array.length"
+    const val DOMAIN_OBJECT_FIELDS = "domain.object.fields"
     const val DOMAIN_CONSTANT_UNSUPPORTED = "domain.constant.unsupported"
     const val DOMAIN_INTEGER_BOUNDS = "domain.integer.bounds"
     const val DOMAIN_NUMBER_BOUND_NAN = "domain.number.bound.nan"
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt
index d442482b83..09a9b01049 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/JsConcreteValue.kt
@@ -98,7 +98,7 @@ data class JsNumber(
     }
 }
 
-/** Lossless transport value for JavaScript primitives and recursively nested arrays. */
+/** Lossless transport value for JavaScript primitives, arrays, and plain objects. */
 @Serializable(with = JsConcreteValueSerializer::class)
 sealed interface JsConcreteValue {
     /** JavaScript `undefined`. */
@@ -121,6 +121,9 @@ sealed interface JsConcreteValue {
     /** Ordered recursively tagged elements of one concrete JavaScript array. */
     data class Array(val elements: List<JsConcreteValue>) : JsConcreteValue
 
+    /** Own data properties of a plain JavaScript object. */
+    data class Object(val fields: Map<KotlinString, JsConcreteValue>) : JsConcreteValue
+
     companion object {
         /** Creates a lossless tagged value from any ECMAScript binary64 number. */
         fun number(value: Double): Number = Number(JsNumber.fromDouble(value))
@@ -172,6 +175,17 @@ object JsConcreteValueSerializer : KSerializer<JsConcreteValue> {
                         put("kind", "array")
                         put("elements", jsonElements)
                     }
+
+                    is JsConcreteValue.Object -> {
+                        val fields = buildJsonObject {
+                            value.fields.forEach { (name, fieldValue) ->
+                                put(name, jsonEncoder.json.encodeToJsonElement(JsConcreteValueSerializer, fieldValue))
+                            }
+                        }
+
+                        put("kind", "object")
+                        put("fields", fields)
+                    }
                 }
             },
         )
@@ -214,6 +228,11 @@ object JsConcreteValueSerializer : KSerializer<JsConcreteValue> {
                 deserializeArray(jsonDecoder, value)
             }
 
+            "object" -> {
+                value.requireExactKeys("kind", "fields")
+                deserializeObject(jsonDecoder, value)
+            }
+
             else -> {
                 throw SerializationException("Unknown JavaScript value kind: $kind")
             }
@@ -270,6 +289,16 @@ private fun deserializeArray(jsonDecoder: JsonDecoder, value: JsonObject): JsCon
     return JsConcreteValue.Array(elements)
 }
 
+private fun deserializeObject(jsonDecoder: JsonDecoder, value: JsonObject): JsConcreteValue.Object {
+    val jsonFields = value["fields"] as? JsonObject
+        ?: throw SerializationException("Object JsConcreteValue requires fields")
+    val fields = jsonFields.mapValues { (_, fieldValue) ->
+        jsonDecoder.json.decodeFromJsonElement(JsConcreteValueSerializer, fieldValue)
+    }
+
+    return JsConcreteValue.Object(fields)
+}
+
 private val JsNumberKind.serialName: String
     get() = when (this) {
         JsNumberKind.FINITE -> "finite"
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt
index 08f630936a..3f18a4c3b5 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/model/PropertyDomain.kt
@@ -71,6 +71,11 @@ data class ArrayDomain(
     val maxLength: Int = DEFAULT_MAX_ARRAY_LENGTH,
 ) : PropertyDomain
 
+/** Plain JavaScript object with an exact, fixed set of own data properties. */
+@Serializable
+@SerialName("object")
+data class ObjectDomain(val fields: Map<String, PropertyDomain>) : PropertyDomain
+
 /** Returns whether [value] belongs to this domain, including recursive tuple and array constraints. */
 operator fun PropertyDomain.contains(value: JsConcreteValue): Boolean = when (this) {
     BooleanDomain -> value is JsConcreteValue.Boolean
@@ -90,6 +95,12 @@ operator fun PropertyDomain.contains(value: JsConcreteValue): Boolean = when (th
             value.elements.size in minLength..maxLength &&
             value.elements.all { elementValue -> elementValue in element }
     }
+
+    is ObjectDomain -> {
+        value is JsConcreteValue.Object &&
+            value.fields.keys == fields.keys &&
+            fields.all { (name, domain) -> value.fields.getValue(name) in domain }
+    }
 }
 
 private fun JsConcreteValue.Number.isIntegerIn(domain: IntegerDomain): Boolean {
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/PlainObjectInputShapes.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/PlainObjectInputShapes.kt
new file mode 100644
index 0000000000..461885bfbd
--- /dev/null
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/PlainObjectInputShapes.kt
@@ -0,0 +1,75 @@
+package org.usvm.ts.pbt.usvm
+
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassCategory
+import org.jacodb.ets.model.EtsClassImpl
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsFieldImpl
+import org.jacodb.ets.model.EtsFieldSignature
+import org.jacodb.ets.model.EtsFile
+import org.jacodb.ets.model.EtsFileSignature
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsType
+import org.usvm.ts.pbt.model.ObjectDomain
+import org.usvm.ts.pbt.model.PropertyDomain
+
+/** Runtime shapes of the own data properties emitted by the concrete input generator. */
+class PlainObjectInputShapes(sourceScene: EtsScene, domains: List<PropertyDomain>) {
+    private val shapes = linkedMapOf<ObjectDomain, EtsClassType>()
+    private val classes = mutableListOf<EtsClass>()
+    private val occupiedNames = sourceScene.projectAndSdkClasses.mapTo(mutableSetOf()) { it.name }
+    private val fileSignature: EtsFileSignature
+    val scene: EtsScene
+
+    init {
+        val occupiedFiles = (sourceScene.projectFiles + sourceScene.sdkFiles).mapTo(mutableSetOf()) { it.signature }
+        sourceScene.projectAndSdkClasses.mapTo(occupiedFiles) { it.signature.file }
+        fileSignature = generateSequence(0) { it + 1 }
+            .map { index -> EtsFileSignature(projectName = "usvm-property-inputs", fileName = "shapes-$index.ts") }
+            .first { it !in occupiedFiles }
+        domains.forEach(::register)
+
+        scene = if (classes.isEmpty()) {
+            sourceScene
+        } else {
+            val file = EtsFile(signature = fileSignature, classes = classes, namespaces = emptyList())
+            EtsScene(
+                projectFiles = sourceScene.projectFiles + file,
+                sdkFiles = sourceScene.sdkFiles,
+                projectName = sourceScene.projectName,
+            )
+        }
+    }
+
+    fun typeOf(domain: ObjectDomain): EtsClassType = shapes.getValue(domain)
+
+    /** Runtime storage type derived from the generated value, without granting source-class ancestry. */
+    fun runtimeTypeOf(domain: PropertyDomain): EtsType = domain.symbolicInputRuntimeType(::typeOf)
+
+    private fun register(domain: PropertyDomain): EtsType = domain.symbolicInputRuntimeType(::registerObject)
+
+    private fun registerObject(domain: ObjectDomain): EtsClassType {
+        shapes[domain]?.let { return it }
+
+        val name = generateSequence(shapes.size) { it + 1 }
+            .map { index -> "__usvm_property_input_$index" }
+            .first { it !in occupiedNames }
+        occupiedNames += name
+        val signature = EtsClassSignature(name = name, file = fileSignature)
+        val type = EtsClassType(signature)
+        shapes[domain] = type
+        val fields = domain.fields.map { (fieldName, fieldDomain) ->
+            EtsFieldImpl(EtsFieldSignature(enclosingClass = signature, name = fieldName, type = register(fieldDomain)))
+        }
+
+        // A source annotation supplies field layout, never methods or nominal ancestry.
+        classes += EtsClassImpl(
+            signature = signature,
+            fields = fields,
+            methods = emptyList(),
+            category = EtsClassCategory.OBJECT,
+        )
+        return type
+    }
+}
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/SymbolicInputRuntimeType.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/SymbolicInputRuntimeType.kt
new file mode 100644
index 0000000000..9b1c26604f
--- /dev/null
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/SymbolicInputRuntimeType.kt
@@ -0,0 +1,68 @@
+package org.usvm.ts.pbt.usvm
+
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsNullType
+import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsStringType
+import org.jacodb.ets.model.EtsTupleType
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUndefinedType
+import org.jacodb.ets.model.EtsUnionType
+import org.usvm.ts.pbt.model.ArrayDomain
+import org.usvm.ts.pbt.model.BooleanDomain
+import org.usvm.ts.pbt.model.ConstantDomain
+import org.usvm.ts.pbt.model.IntegerDomain
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
+import org.usvm.ts.pbt.model.OptionalDomain
+import org.usvm.ts.pbt.model.PropertyDomain
+import org.usvm.ts.pbt.model.StringDomain
+import org.usvm.ts.pbt.model.TupleDomain
+
+internal fun PropertyDomain.symbolicInputRuntimeType(
+    objectType: (ObjectDomain) -> EtsClassType,
+): EtsType = when (this) {
+    BooleanDomain -> {
+        EtsBooleanType
+    }
+    is IntegerDomain, is NumberDomain -> {
+        EtsNumberType
+    }
+    is StringDomain -> {
+        EtsStringType
+    }
+    is ArrayDomain -> {
+        val nestedType = element.symbolicInputRuntimeType(objectType)
+        if (nestedType is EtsArrayType) {
+            nestedType.copy(dimensions = nestedType.dimensions + 1)
+        } else {
+            EtsArrayType(elementType = nestedType, dimensions = 1)
+        }
+    }
+    is TupleDomain -> {
+        EtsTupleType(types = elements.map { it.symbolicInputRuntimeType(objectType) })
+    }
+    is OptionalDomain -> {
+        val nestedType = value.symbolicInputRuntimeType(objectType)
+        val nilType = ConstantDomain(nil).symbolicInputRuntimeType(objectType)
+        EtsUnionType(types = listOf(nestedType, nilType))
+    }
+    is ObjectDomain -> {
+        objectType(this)
+    }
+    is ConstantDomain -> {
+        when (value) {
+            is JsConcreteValue.Boolean -> EtsBooleanType
+            is JsConcreteValue.Number -> EtsNumberType
+            is JsConcreteValue.String -> EtsStringType
+            JsConcreteValue.Null -> EtsNullType
+            JsConcreteValue.Undefined -> EtsUndefinedType
+            is JsConcreteValue.Array, is JsConcreteValue.Object -> {
+                error("Structured constants are not primitive domains")
+            }
+        }
+    }
+}
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt
index fb6d335cc8..48caffa173 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmCandidateInputResolver.kt
@@ -21,6 +21,7 @@ import org.usvm.ts.pbt.model.ConstantDomain
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.OptionalDomain
 import org.usvm.ts.pbt.model.PropertyDomain
 import org.usvm.ts.pbt.model.PropertyInput
@@ -29,9 +30,10 @@ import org.usvm.ts.pbt.model.TupleDomain
 import org.usvm.util.componentType
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.mkFieldLValue
 import org.usvm.util.resolveStringValue
 
-internal class UsvmCandidateInputResolver {
+internal class UsvmCandidateInputResolver(private val objectShapes: PlainObjectInputShapes? = null) {
     fun resolve(
         state: TsState,
         declaredInputs: List<PropertyInput>,
@@ -78,9 +80,29 @@ internal class UsvmCandidateInputResolver {
             is OptionalDomain -> resolveOptional(state, domain, etsType, value)
             is TupleDomain -> resolveTuple(state, domain, etsType, value)
             is ArrayDomain -> resolveArray(state, domain, etsType as EtsArrayType, value)
+            is ObjectDomain -> resolveObject(state, domain, value)
         }
     }
 
+    private fun resolveObject(
+        state: TsState,
+        domain: ObjectDomain,
+        value: UExpr<out USort>,
+    ): JsConcreteValue.Object = with(state.ctx) {
+        val shapes = requireNotNull(objectShapes) { "Object projection metadata is missing from the input snapshot" }
+        val reference = value.asExpr(addressSort)
+        val fields = domain.fields.mapValues { (name, fieldDomain) ->
+            val fieldType = shapes.runtimeTypeOf(fieldDomain)
+            val declaredSort = typeToSort(fieldType)
+            val storageSort = if (declaredSort is TsUnresolvedSort) addressSort else declaredSort
+            val fieldValue = state.memory.read(mkFieldLValue(storageSort, reference, name))
+
+            resolveValue(state, fieldDomain, fieldType, fieldValue)
+        }
+
+        JsConcreteValue.Object(fields)
+    }
+
     private fun resolveFakeValue(
         state: TsState,
         domain: PropertyDomain,
@@ -118,7 +140,7 @@ internal class UsvmCandidateInputResolver {
         }
 
         val nestedType = (etsType as org.jacodb.ets.model.EtsUnionType).types.first { type ->
-            UsvmProjectionCapabilityResolver().domainCompatibilityForProjector(domain.value, type)
+            UsvmProjectionCapabilityResolver(state.ctx.scene).domainCompatibilityForProjector(domain.value, type)
         }
 
         resolveValue(state, domain.value, nestedType, value)
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt
index 92d0c0c8fb..fd168e327b 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmDomainProjector.kt
@@ -29,6 +29,7 @@ import org.usvm.ts.pbt.model.ConstantDomain
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.OptionalDomain
 import org.usvm.ts.pbt.model.PropertyDomain
 import org.usvm.ts.pbt.model.PropertyInput
@@ -37,6 +38,7 @@ import org.usvm.ts.pbt.model.TupleDomain
 import org.usvm.util.componentType
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
 import org.usvm.util.mkSymbolicString
 
@@ -50,11 +52,16 @@ data class UsvmProjectedInput(
 data class UsvmDeclaredDomainProjection(
     val inputs: List<UsvmProjectedInput>,
     val initialState: TsState,
+    val objectShapes: PlainObjectInputShapes? = null,
 )
 
-/** Materializes declared property domains in a real USVM TypeScript initial state. */
+/**
+ * Materializes declared property domains in a real USVM TypeScript initial state.
+ * Object inputs require [objectShapes] whose scene was used to construct the machine.
+ */
 class UsvmDomainProjector(
     private val options: UsvmProjectionOptions = UsvmProjectionOptions(),
+    private val objectShapes: PlainObjectInputShapes? = null,
 ) {
     fun configure(
         state: TsState,
@@ -67,13 +74,14 @@ class UsvmDomainProjector(
         }
 
         val pairedInputs = inputs.zip(bindings)
+        val capabilityResolver = UsvmProjectionCapabilityResolver(state.ctx.scene)
         pairedInputs.forEachIndexed { index, (input, binding) ->
             require(input.name == binding.propertyInputName) {
                 "Property input ${input.name} does not match EtsIR binding ${binding.propertyInputName}"
             }
 
             val path = "inputs[$index].domain"
-            val capability = UsvmProjectionCapabilityResolver().domainCapabilityForProjector(
+            val capability = capabilityResolver.domainCapabilityForProjector(
                 domain = input.domain,
                 etsType = binding.parameter.type,
                 path = path,
@@ -117,10 +125,13 @@ class UsvmDomainProjector(
         return UsvmDeclaredDomainProjection(
             inputs = projectedInputs,
             initialState = state.clone(),
+            objectShapes = objectShapes,
         )
     }
 
     private inner class Materializer(private val state: TsState) {
+        private val capabilityResolver = UsvmProjectionCapabilityResolver(state.ctx.scene)
+
         fun materialize(domain: PropertyDomain, etsType: EtsType): UExpr<out USort> = when (domain) {
             BooleanDomain -> state.makeSymbolicPrimitive(state.ctx.boolSort)
             is IntegerDomain -> materializeInteger(domain)
@@ -130,6 +141,23 @@ class UsvmDomainProjector(
             is OptionalDomain -> materializeOptional(domain, etsType)
             is TupleDomain -> materializeTuple(domain, etsType)
             is ArrayDomain -> materializeArray(domain, etsType as EtsArrayType)
+            is ObjectDomain -> materializeObject(domain)
+        }
+
+        private fun materializeObject(domain: ObjectDomain): UConcreteHeapRef = with(state.ctx) {
+            val shapes = requireNotNull(objectShapes) {
+                "Object shapes must be added to the machine scene before configuring inputs"
+            }
+            val reference = state.memory.allocConcrete(shapes.typeOf(domain))
+            domain.fields.forEach { (name, fieldDomain) ->
+                val fieldType = shapes.runtimeTypeOf(fieldDomain)
+                val value = materialize(fieldDomain, fieldType)
+                val sort = value.sort
+
+                state.memory.write(mkFieldLValue(sort, reference, name), value.asExpr(sort), guard = trueExpr)
+            }
+
+            reference
         }
 
         private fun materializeInteger(domain: IntegerDomain): UExpr<KFp64Sort> = with(state.ctx) {
@@ -185,7 +213,9 @@ class UsvmDomainProjector(
                 is JsConcreteValue.String -> state.mkInitializedStringConstant(value.value)
                 JsConcreteValue.Null -> mkTsNullValue()
                 JsConcreteValue.Undefined -> mkUndefinedValue()
-                is JsConcreteValue.Array -> error("Array constants are not valid property-domain primitives")
+                is JsConcreteValue.Array, is JsConcreteValue.Object -> {
+                    error("Object constants are not valid property-domain primitives")
+                }
             }
         }
 
@@ -195,7 +225,7 @@ class UsvmDomainProjector(
         ): UExpr<out USort> = with(state.ctx) {
             val unionType = etsType as EtsUnionType
             val nestedType = unionType.types.first { type ->
-                UsvmProjectionCapabilityResolver().domainCompatibilityForProjector(domain.value, type)
+                capabilityResolver.domainCompatibilityForProjector(domain.value, type)
             }
             val nestedValue = materialize(domain.value, nestedType)
             val nilValue = materializeConstant(domain.nil)
@@ -237,7 +267,7 @@ class UsvmDomainProjector(
         ): UConcreteHeapRef = with(state.ctx) {
             val elementTypes = when (etsType) {
                 is EtsTupleType -> etsType.types
-                is EtsArrayType -> List(domain.elements.size) { etsType.elementType }
+                is EtsArrayType -> List(domain.elements.size) { etsType.componentType }
                 else -> error("Unsupported tuple EtsIR type $etsType")
             }
             val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt
index b3ac7bba19..4664380a34 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityResolver.kt
@@ -1,17 +1,23 @@
 package org.usvm.ts.pbt.usvm
 
+import org.jacodb.ets.model.EtsAliasType
+import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanLiteralType
 import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberLiteralType
 import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringLiteralType
 import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsTupleType
 import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnclearRefType
 import org.jacodb.ets.model.EtsUndefinedType
 import org.jacodb.ets.model.EtsUnionType
+import org.jacodb.ets.model.EtsUnknownType
 import org.usvm.ts.pbt.PbtDiagnosticCode
 import org.usvm.ts.pbt.backend.CapabilityDiagnostic
 import org.usvm.ts.pbt.backend.ProjectionCapability
@@ -30,14 +36,19 @@ import org.usvm.ts.pbt.model.ExecutionKind
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.OptionalDomain
 import org.usvm.ts.pbt.model.PropertyDomain
 import org.usvm.ts.pbt.model.StringDomain
 import org.usvm.ts.pbt.model.TupleDomain
+import org.usvm.util.EtsHierarchy
 import org.usvm.util.componentType
+import org.usvm.util.declaredInstanceProperty
 
 /** Calculates USVM fidelity without constructing or mutating a symbolic state. */
-class UsvmProjectionCapabilityResolver {
+class UsvmProjectionCapabilityResolver(scene: EtsScene? = null) {
+    private val hierarchy = scene?.let(::EtsHierarchy)
+
     fun resolve(
         manifest: PropertyManifest,
         mapping: PropertyEtsMappingArtifact,
@@ -179,6 +190,9 @@ class UsvmProjectionCapabilityResolver {
         path: String,
         options: UsvmProjectionOptions,
     ): ProjectionCapability {
+        if (domain is ObjectDomain) {
+            return objectCapability(domain, etsType, path, options)
+        }
         if (!domainCompatibilityForProjector(domain, etsType)) {
             return unsupported(
                 code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED,
@@ -209,6 +223,119 @@ class UsvmProjectionCapabilityResolver {
 
             is TupleDomain -> tupleCapability(domain, etsType, path, options)
             is ArrayDomain -> arrayCapability(domain, etsType, path, options)
+            is ObjectDomain -> error("Object domains are validated before scalar compatibility")
+        }
+    }
+
+    private fun objectCapability(
+        domain: ObjectDomain,
+        etsType: EtsType,
+        path: String,
+        options: UsvmProjectionOptions,
+    ): ProjectionCapability {
+        if (etsType is EtsAliasType) {
+            return objectCapability(domain, etsType.originalType, path, options)
+        }
+        if (etsType is EtsUnionType) {
+            val alternatives = etsType.types.map { member -> objectCapability(domain, member, path, options) }
+            return alternatives.firstOrNull { it.level == ProjectionLevel.EXACT }
+                ?: aggregateProjectionCapabilities(alternatives)
+        }
+
+        if (etsType == EtsAnyType || etsType == EtsUnknownType) {
+            return untypedDomainCapability(domain, path, options)
+        }
+
+        val acceptsObject = etsType is EtsClassType || etsType is EtsUnclearRefType
+        if (!acceptsObject) {
+            return unsupported(
+                code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED,
+                message = "Object domain requires an object declaration, got $etsType",
+                path = path,
+            )
+        }
+        val metadata = hierarchy ?: return unsupported(
+            code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED,
+            message = "Object projection requires the source scene to resolve field declarations",
+            path = path,
+        )
+        val fieldCapabilities = domain.fields.map { (name, fieldDomain) ->
+            val fieldPath = "$path.fields.$name"
+            val declaration = declaredInstanceProperty(etsType, name, metadata)
+            if (declaration == null) {
+                unsupported(
+                    code = PbtDiagnosticCode.USVM_DOMAIN_TYPE_UNSUPPORTED,
+                    message = "Cannot resolve compatible declarations for object field $name in $etsType",
+                    path = fieldPath,
+                )
+            } else {
+                val declaredTypes = (declaration.type as? EtsUnionType)?.types ?: listOf(declaration.type)
+                val fieldType = if (declaration.optional && fieldDomain is OptionalDomain) {
+                    EtsUnionType(types = (declaredTypes + EtsUndefinedType).distinct())
+                } else {
+                    declaration.type
+                }
+                objectFieldCapability(fieldDomain, fieldType, fieldPath, options)
+            }
+        }
+
+        return aggregateProjectionCapabilities(fieldCapabilities)
+    }
+
+    private fun objectFieldCapability(
+        domain: PropertyDomain,
+        etsType: EtsType,
+        path: String,
+        options: UsvmProjectionOptions,
+    ): ProjectionCapability {
+        if (etsType is EtsAliasType) {
+            return objectFieldCapability(domain, etsType.originalType, path, options)
+        }
+        if (etsType is EtsUnionType && domain !is OptionalDomain) {
+            val alternatives = etsType.types.map { member -> objectFieldCapability(domain, member, path, options) }
+            return alternatives.firstOrNull { it.level == ProjectionLevel.EXACT }
+                ?: aggregateProjectionCapabilities(alternatives)
+        }
+        if (etsType == EtsAnyType || etsType == EtsUnknownType) {
+            return untypedDomainCapability(domain, path, options)
+        }
+
+        return domainCapabilityForProjector(domain, etsType, path, options)
+    }
+
+    /** An untyped declaration adds no type restriction; domain bounds still apply to every supplied value. */
+    private fun untypedDomainCapability(
+        domain: PropertyDomain,
+        path: String,
+        options: UsvmProjectionOptions,
+    ): ProjectionCapability = when (domain) {
+        is ObjectDomain -> {
+            val capabilities = domain.fields.map { (name, field) ->
+                untypedDomainCapability(field, "$path.fields.$name", options)
+            }
+            aggregateProjectionCapabilities(capabilities)
+        }
+        is OptionalDomain -> untypedDomainCapability(domain.value, "$path.value", options)
+        is ArrayDomain -> {
+            if (domain.maxLength > options.maxSymbolicCollectionLength) {
+                collectionTooLarge(domain.maxLength, options, path)
+            } else {
+                untypedDomainCapability(domain.element, "$path.element", options)
+            }
+        }
+        is TupleDomain -> {
+            if (domain.elements.size > options.maxSymbolicCollectionLength) {
+                collectionTooLarge(domain.elements.size, options, path)
+            } else {
+                val capabilities = domain.elements.mapIndexed { index, element ->
+                    untypedDomainCapability(element, "$path.elements[$index]", options)
+                }
+                aggregateProjectionCapabilities(capabilities)
+            }
+        }
+        else -> {
+            val storageType = domain.symbolicInputRuntimeType { error("Object domain was handled recursively") }
+            domainCapabilityForProjector(domain, storageType, path, options)
         }
     }
 
@@ -268,6 +395,16 @@ class UsvmProjectionCapabilityResolver {
         is IntegerDomain, is NumberDomain -> etsType == EtsNumberType || etsType is EtsNumberLiteralType
         is StringDomain -> etsType == EtsStringType || etsType is EtsStringLiteralType
         is ConstantDomain -> isConstantCompatible(domain.value, etsType)
+        is ObjectDomain -> objectCapability(
+            domain = domain,
+            etsType = etsType,
+            path = "domain",
+            // This query selects a representation; domain bounds are checked separately with caller options.
+            options = UsvmProjectionOptions(
+                maxSymbolicCollectionLength = Int.MAX_VALUE,
+                maxSymbolicStringLength = Int.MAX_VALUE,
+            ),
+        ).level != ProjectionLevel.UNSUPPORTED
         is OptionalDomain -> isOptionalCompatible(domain, etsType)
         is TupleDomain -> when (etsType) {
             is EtsTupleType -> {
@@ -296,7 +433,7 @@ class UsvmProjectionCapabilityResolver {
         is JsConcreteValue.String -> etsType == EtsStringType || etsType is EtsStringLiteralType
         JsConcreteValue.Null -> etsType == EtsNullType
         JsConcreteValue.Undefined -> etsType == EtsUndefinedType
-        is JsConcreteValue.Array -> false
+        is JsConcreteValue.Array, is JsConcreteValue.Object -> false
     }
 
     private fun isOptionalCompatible(domain: OptionalDomain, etsType: EtsType): Boolean {
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 90a6c8c2ba..0db12fc868 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
@@ -39,9 +39,7 @@ class UsvmPropertySearcher(
         maxSymbolicCollectionLength = minOf(projectionOptions.maxSymbolicCollectionLength, tsOptions.maxArraySize),
         maxSymbolicStringLength = minOf(projectionOptions.maxSymbolicStringLength, tsOptions.maxArraySize),
     )
-    private val capabilityResolver = UsvmProjectionCapabilityResolver()
-    private val domainProjector = UsvmDomainProjector(this.projectionOptions)
-    private val inputResolver = UsvmCandidateInputResolver()
+    private val capabilityResolver = UsvmProjectionCapabilityResolver(scene)
 
     fun search(
         manifest: PropertyManifest,
@@ -92,9 +90,11 @@ class UsvmPropertySearcher(
         lateinit var projection: UsvmDeclaredDomainProjection
         val target = UsvmViolationTsTarget()
         val observer = UsvmViolationObserver(target)
+        val objectShapes = PlainObjectInputShapes(scene, manifest.inputs.map { it.domain })
+        val domainProjector = UsvmDomainProjector(projectionOptions, objectShapes)
 
         return TsMachine(
-            scene = scene,
+            scene = objectShapes.scene,
             options = machineOptions,
             tsOptions = tsOptions,
             machineObserver = observer,
@@ -328,7 +328,7 @@ class UsvmPropertySearcher(
     ): UsvmPropertySearchResult {
         val violationTarget = classifyViolation(violationState)
         val inputs = runCatching {
-            inputResolver.resolve(violationState, manifest.inputs, projection)
+            UsvmCandidateInputResolver(projection.objectShapes).resolve(violationState, manifest.inputs, projection)
         }.getOrElse { failure ->
             val diagnostic = CapabilityDiagnostic(
                 code = PbtDiagnosticCode.USVM_INPUT_RESOLUTION_FAILED,
diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt
index e1efb37001..3e096447c0 100644
--- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt
+++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/validation/PropertyValidation.kt
@@ -11,6 +11,7 @@ import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.JsNumber
 import org.usvm.ts.pbt.model.JsNumberKind
 import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.OptionalDomain
 import org.usvm.ts.pbt.model.PropertyAssertion
 import org.usvm.ts.pbt.model.PropertyDefinition
@@ -248,7 +249,8 @@ private fun validateDomain(
         }
 
         is ConstantDomain -> {
-            if (domain.value is JsConcreteValue.Array) {
+            val isObjectConstant = domain.value is JsConcreteValue.Array || domain.value is JsConcreteValue.Object
+            if (isObjectConstant) {
                 diagnostics += diagnostic(
                     code = PbtDiagnosticCode.DOMAIN_CONSTANT_UNSUPPORTED,
                     message = "Constant domains support JavaScript primitives only",
@@ -293,6 +295,21 @@ private fun validateDomain(
             )
             validateDomain(domain.element, "$path.element", diagnostics)
         }
+
+        is ObjectDomain -> {
+            val invalidFields = domain.fields.size > MAX_OBJECT_FIELDS ||
+                domain.fields.keys.any { it in UNSAFE_OBJECT_KEYS }
+            if (invalidFields) {
+                diagnostics += diagnostic(
+                    code = PbtDiagnosticCode.DOMAIN_OBJECT_FIELDS,
+                    message = "Object domain has too many fields or an unsafe property name",
+                    path = path,
+                )
+            }
+            domain.fields.forEach { (name, fieldDomain) ->
+                validateDomain(fieldDomain, "$path.fields.$name", diagnostics)
+            }
+        }
     }
 }
 
@@ -354,6 +371,11 @@ private fun validateJsConcreteValue(
             validateJsConcreteValue(element, "$path.elements[$index]", diagnostics)
         }
     }
+    if (value is JsConcreteValue.Object) {
+        value.fields.forEach { (name, fieldValue) ->
+            validateJsConcreteValue(fieldValue, "$path.fields.$name", diagnostics)
+        }
+    }
 }
 
 private fun validateJsNumber(
@@ -466,3 +488,6 @@ private const val MAX_DIRECT_ARRAY_LENGTH = 32
 // ECMAScript permits these otherwise invisible Unicode characters after the first identifier character.
 private const val ZERO_WIDTH_NON_JOINER_CODE_POINT = 0x200C
 private const val ZERO_WIDTH_JOINER_CODE_POINT = 0x200D
+
+private const val MAX_OBJECT_FIELDS = 32
+private val UNSAFE_OBJECT_KEYS = setOf("__proto__", "constructor", "prototype")
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt
index d858c0a71c..a0058e9f35 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/JsConcreteValueTest.kt
@@ -56,6 +56,19 @@ class JsConcreteValueTest {
         assertEquals(value, PropertyManifestJson.json.decodeFromString<JsConcreteValue>(encoded))
     }
 
+    @Test
+    fun `plain objects keep nested tagged values through JSON`() {
+        val fields = mapOf(
+            "score" to JsConcreteValue.number(-0.0),
+            "nested" to JsConcreteValue.Object(mapOf("enabled" to JsConcreteValue.Boolean(true))),
+        )
+        val value = JsConcreteValue.Object(fields = fields)
+
+        val encoded = PropertyManifestJson.json.encodeToString<JsConcreteValue>(value)
+
+        assertEquals(value, PropertyManifestJson.json.decodeFromString<JsConcreteValue>(encoded))
+    }
+
     @Test
     fun `string tags require string values`() {
         assertFailsWith<SerializationException> {
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/PropertyDomainTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/PropertyDomainTest.kt
index 114a3c77ea..5afa81257b 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/PropertyDomainTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/model/PropertyDomainTest.kt
@@ -5,6 +5,20 @@ import kotlin.test.assertFalse
 import kotlin.test.assertTrue
 
 class PropertyDomainTest {
+    @Test
+    fun `object membership requires every declared field and no extras`() {
+        val domain = ObjectDomain(mapOf("score" to NumberDomain(), "enabled" to BooleanDomain))
+        val fields = mapOf(
+            "score" to JsConcreteValue.number(2.0),
+            "enabled" to JsConcreteValue.Boolean(true),
+        )
+        val valid = JsConcreteValue.Object(fields = fields)
+
+        assertTrue(valid in domain)
+        assertFalse(JsConcreteValue.Object(valid.fields - "enabled") in domain)
+        assertFalse(JsConcreteValue.Object(valid.fields + ("extra" to JsConcreteValue.Null)) in domain)
+    }
+
     @Test
     fun `integer membership matches values produced by fast-check integer`() {
         val domain = IntegerDomain(min = -1, max = 1)
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmObjectDomainProjectionTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmObjectDomainProjectionTest.kt
new file mode 100644
index 0000000000..3e9236fee1
--- /dev/null
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmObjectDomainProjectionTest.kt
@@ -0,0 +1,174 @@
+package org.usvm.ts.pbt.usvm
+
+import org.jacodb.ets.model.EtsScene
+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.ts.pbt.backend.ProjectionCapability
+import org.usvm.ts.pbt.backend.ProjectionLevel
+import org.usvm.ts.pbt.manifest.PropertyManifest
+import org.usvm.ts.pbt.mapping.PropertyEtsMapper
+import org.usvm.ts.pbt.model.ArrayDomain
+import org.usvm.ts.pbt.model.IntegerDomain
+import org.usvm.ts.pbt.model.JsConcreteValue
+import org.usvm.ts.pbt.model.ObjectDomain
+import org.usvm.ts.pbt.model.OptionalDomain
+import org.usvm.ts.pbt.model.PropertyDomain
+import org.usvm.ts.pbt.model.PropertyInput
+import org.usvm.ts.pbt.model.TypeScriptEntryPoint
+import org.usvm.ts.pbt.testResourcePath
+import kotlin.test.assertEquals
+import kotlin.test.assertNull
+import kotlin.test.assertTrue
+
+class UsvmObjectDomainProjectionTest {
+    @Test
+    fun `object candidates preserve entry fields through mutation and preconditions`() {
+        val domain = ObjectDomain(mapOf("count" to IntegerDomain(min = -2, max = 2)))
+
+        val result = search("objectMutation", domain, precondition = "positiveObject")
+
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status, result.toString())
+        assertEquals(listOf(objectValue("count")), result.inputs)
+    }
+
+    @Test
+    fun `class annotations do not grant prototype identity or missing fields`() {
+        val domain = ObjectDomain(mapOf("value" to IntegerDomain(min = 2, max = 2)))
+
+        val identity = search("plainClassIdentity", domain)
+        val absent = search("absentClassField", domain)
+
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, identity.status, identity.toString())
+        assertEquals(UsvmPropertySearchStatus.NO_VIOLATION_REACHED, absent.status, absent.toString())
+    }
+
+    @Test
+    fun `nearest inherited field declarations retain structural inputs`() {
+        val domain = ObjectDomain(mapOf("value" to IntegerDomain(min = 0, max = 2)))
+
+        val result = search("inheritedField", domain)
+
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status, result.toString())
+        assertEquals(listOf(objectValue("value")), result.inputs)
+    }
+
+    @Test
+    fun `nested array objects recover their values from the initial snapshot`() {
+        val element = ObjectDomain(mapOf("count" to IntegerDomain(min = 0, max = 2)))
+        val domain = ObjectDomain(mapOf("entries" to ArrayDomain(element, minLength = 1, maxLength = 1)))
+
+        val result = search("nestedObjects", domain)
+
+        val expected = JsConcreteValue.Object(mapOf("entries" to JsConcreteValue.Array(listOf(objectValue("count")))))
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status, result.toString())
+        assertEquals(listOf(expected), result.inputs)
+    }
+
+    @Test
+    fun `optional objects and optional fields preserve their selected kind`() {
+        val count = IntegerDomain(min = 0, max = 2)
+        val optionalObject = OptionalDomain(ObjectDomain(mapOf("count" to count)))
+        val optionalField = ObjectDomain(mapOf("count" to OptionalDomain(count)))
+
+        val objectResult = search("optionalObject", optionalObject)
+        val fieldResult = search("optionalField", optionalField)
+
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, objectResult.status, objectResult.toString())
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, fieldResult.status, fieldResult.toString())
+        assertEquals(listOf(objectValue("count")), objectResult.inputs)
+        assertEquals(listOf(objectValue("count")), fieldResult.inputs)
+    }
+
+    @Test
+    fun `an any annotation does not discard a declared object domain`() {
+        val domain = ObjectDomain(mapOf("count" to IntegerDomain(min = 0, max = 2)))
+
+        val result = search("untypedObject", domain)
+
+        assertEquals(UsvmPropertySearchStatus.VIOLATION_REACHED, result.status, result.toString())
+        assertEquals(listOf(objectValue("count")), result.inputs)
+    }
+
+    @Test
+    fun `incompatible supplied fields retain a precise capability diagnostic`() {
+        val domain = ObjectDomain(mapOf("count" to IntegerDomain(min = 0, max = 2)))
+
+        val result = search("acceptsBooleanField", domain)
+
+        assertEquals(UsvmPropertySearchStatus.UNSUPPORTED, result.status)
+        assertNull(result.inputs)
+        assertTrue(result.diagnostics.any { it.path == "inputs[0].domain.fields.count" }, result.toString())
+    }
+
+    @Test
+    fun `optional object type matching preserves the configured collection bound`() {
+        val fields = mapOf("entries" to ArrayDomain(IntegerDomain(), maxLength = 11))
+        val domain = OptionalDomain(value = ObjectDomain(fields = fields))
+        val manifest = PropertyManifest(
+            propertyId = "objects.optional-capacity",
+            inputs = listOf(PropertyInput(name = "value", domain = domain)),
+            predicate = TypeScriptEntryPoint(module = MODULE, exportName = "optionalCollection"),
+        )
+        val mapping = mapper.map(manifest)
+        val resolver = UsvmProjectionCapabilityResolver(scene)
+        val concrete = ProjectionCapability(level = ProjectionLevel.EXACT)
+
+        val admitted = resolver.resolve(
+            manifest = manifest,
+            mapping = mapping,
+            concreteCapability = concrete,
+            options = UsvmProjectionOptions(maxSymbolicCollectionLength = 12),
+        )
+        val bounded = resolver.resolve(
+            manifest = manifest,
+            mapping = mapping,
+            concreteCapability = concrete,
+            options = UsvmProjectionOptions(maxSymbolicCollectionLength = 10),
+        )
+
+        assertEquals(ProjectionLevel.EXACT, admitted.symbolic.level)
+        assertEquals(ProjectionLevel.UNSUPPORTED, bounded.symbolic.level)
+        assertEquals("inputs[0].domain.value.fields.entries", bounded.symbolic.diagnostics.single().path)
+    }
+
+    private fun objectValue(name: String) = JsConcreteValue.Object(mapOf(name to JsConcreteValue.number(2.0)))
+
+    private fun search(
+        predicate: String,
+        domain: PropertyDomain,
+        precondition: String? = null,
+    ): UsvmPropertySearchResult {
+        val manifest = PropertyManifest(
+            propertyId = "objects.$predicate",
+            inputs = listOf(PropertyInput(name = "value", domain = domain)),
+            predicate = TypeScriptEntryPoint(module = MODULE, exportName = predicate),
+            precondition = precondition?.let { TypeScriptEntryPoint(module = MODULE, exportName = it) },
+        )
+
+        return searcher.search(
+            manifest = manifest,
+            mapping = mapper.map(manifest),
+            concreteCapability = ProjectionCapability(level = ProjectionLevel.EXACT),
+        )
+    }
+
+    companion object {
+        private const val MODULE = "UsvmObjectProjectionFixture.ts"
+        private lateinit var mapper: PropertyEtsMapper
+        private lateinit var scene: EtsScene
+        private lateinit var searcher: UsvmPropertySearcher
+
+        @JvmStatic
+        @BeforeAll
+        fun loadFixture() {
+            val source = testResourcePath("/usvm/$MODULE")
+            val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)
+            scene = EtsScene(listOf(file))
+
+            mapper = PropertyEtsMapper(scene = scene, sourceRoots = listOf(source.parent))
+            searcher = UsvmPropertySearcher(scene)
+        }
+    }
+}
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt
index 8e1bdd2900..0c41d6d2b1 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/usvm/UsvmProjectionCapabilityTest.kt
@@ -19,6 +19,7 @@ import org.usvm.ts.pbt.model.ExecutionKind
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.OptionalDomain
 import org.usvm.ts.pbt.model.PropertyInput
 import org.usvm.ts.pbt.model.StringDomain
@@ -52,6 +53,18 @@ class UsvmProjectionCapabilityTest {
         }
     }
 
+    @Test
+    fun `object domains have exact symbolic projection with their own runtime identity`() {
+        val capability = resolve(
+            domain = ObjectDomain(mapOf("value" to NumberDomain())),
+            exportName = "acceptsObject",
+        )
+
+        assertEquals(ProjectionLevel.EXACT, capability.symbolic.level)
+        assertEquals(PropertyCapabilityLevel.EXACT, capability.property)
+        assertEquals(emptyList(), capability.symbolic.diagnostics)
+    }
+
     @Test
     fun `recursive domains inherit the least capable nested projection`() {
         val optional = resolve(
@@ -227,7 +240,7 @@ class UsvmProjectionCapabilityTest {
 
     companion object {
         private lateinit var mapper: PropertyEtsMapper
-        private val resolver = UsvmProjectionCapabilityResolver()
+        private lateinit var resolver: UsvmProjectionCapabilityResolver
 
         @JvmStatic
         @BeforeAll
@@ -235,8 +248,10 @@ class UsvmProjectionCapabilityTest {
             val source = testResourcePath("/usvm/UsvmCapabilityFixture.ts")
             val file = loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)
 
+            val scene = EtsScene(listOf(file))
+            resolver = UsvmProjectionCapabilityResolver(scene)
             mapper = PropertyEtsMapper(
-                scene = EtsScene(listOf(file)),
+                scene = scene,
                 sourceRoots = listOf(source.parent),
             )
         }
diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt
index a847e1cdb0..41ff6f7104 100644
--- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt
+++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/validation/PropertyValidationTest.kt
@@ -1,12 +1,14 @@
 package org.usvm.ts.pbt.validation
 
 import org.junit.jupiter.api.Test
+import org.usvm.ts.pbt.model.BooleanDomain
 import org.usvm.ts.pbt.model.ConstantDomain
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.JsNumber
 import org.usvm.ts.pbt.model.JsNumberKind
 import org.usvm.ts.pbt.model.NumberDomain
+import org.usvm.ts.pbt.model.ObjectDomain
 import org.usvm.ts.pbt.model.OptionalDomain
 import org.usvm.ts.pbt.model.PropertyDefinition
 import org.usvm.ts.pbt.model.PropertyDomain
@@ -74,6 +76,29 @@ class PropertyValidationTest {
         )
     }
 
+    @Test
+    fun `object domains reject unsafe keys and oversized shapes`() {
+        val domains = listOf(
+            ObjectDomain(mapOf("__proto__" to BooleanDomain)),
+            ObjectDomain((0..32).associate { index -> "field$index" to BooleanDomain }),
+        )
+
+        domains.forEach { domain ->
+            val diagnostics = validatePropertyDefinition(validDefinition(domain)).diagnostics
+
+            assertEquals(listOf("domain.object.fields"), diagnostics.map { it.code })
+        }
+    }
+
+    @Test
+    fun `constant domains reject object values`() {
+        val definition = validDefinition(ConstantDomain(JsConcreteValue.Object(emptyMap())))
+
+        val diagnostics = validatePropertyDefinition(definition).diagnostics
+
+        assertEquals(listOf("domain.constant.unsupported"), diagnostics.map { it.code })
+    }
+
     @Test
     fun `invalid number encodings are diagnosed without comparing the bounds`() {
         val invalidMinimum = JsNumber(JsNumberKind.FINITE, bits = "invalid")
diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts
index ec6edb1925..fdb0ee84f6 100644
--- a/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts
+++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmCapabilityFixture.ts
@@ -57,3 +57,7 @@ function throwingHelper(_value: number): boolean {
 export function returnsNumber(value: number): number {
   return value;
 }
+
+export function acceptsObject(input: { value: number }): boolean {
+    return input.value > 0;
+}
diff --git a/usvm-ts-pbt/src/test/resources/usvm/UsvmObjectProjectionFixture.ts b/usvm-ts-pbt/src/test/resources/usvm/UsvmObjectProjectionFixture.ts
new file mode 100644
index 0000000000..16b9070e99
--- /dev/null
+++ b/usvm-ts-pbt/src/test/resources/usvm/UsvmObjectProjectionFixture.ts
@@ -0,0 +1,64 @@
+class AnnotatedValue {
+    value: number = 0;
+    ignored: () => number = () => 10;
+}
+
+class ParentValue {
+    value: number = 0;
+}
+
+class ChildValue extends ParentValue {
+    value: number = 0;
+}
+
+export function objectMutation(value: { count: number }): boolean {
+    const before = value.count;
+    value.count += 1;
+    return before !== 2;
+}
+
+export function plainClassIdentity(value: AnnotatedValue): boolean {
+    return !(value instanceof AnnotatedValue);
+}
+
+export function absentClassField(value: AnnotatedValue): boolean {
+    return value.ignored === undefined;
+}
+
+export function inheritedField(value: ChildValue): boolean {
+    return value.value !== 2;
+}
+
+export function nestedObjects(value: { entries: { count: number }[] }): boolean {
+    const before = value.entries[0].count;
+    value.entries[0].count = 9;
+    return before !== 2;
+}
+
+export function optionalObject(value: { count: number } | undefined): boolean {
+    if (value === undefined) return true;
+    const before = value.count;
+    value.count = 9;
+    return before !== 2;
+}
+
+export function optionalField(value: { count?: number }): boolean {
+    if (value.count === undefined) return true;
+    return value.count !== 2;
+}
+
+export function untypedObject(value: any): boolean {
+    return value.count !== 2;
+}
+
+export function positiveObject(value: { count: number }): boolean {
+    return value.count > 0;
+}
+
+export function acceptsBooleanField(value: { count: boolean }): boolean {
+    return value.count;
+}
+
+export function optionalCollection(value: { entries: number[] } | undefined): boolean {
+    return value === undefined || value.entries.length >= 0;
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt
index 7d19c3bc17..c08b86af09 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt
@@ -1,9 +1,7 @@
 package org.usvm.machine.expr
 
 import org.jacodb.ets.model.EtsArrayType
-import org.jacodb.ets.model.EtsClassCategory
 import org.jacodb.ets.model.EtsClassType
-import org.jacodb.ets.model.EtsFieldImpl
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnclearRefType
@@ -24,6 +22,8 @@ import org.usvm.machine.types.extractValue
 import org.usvm.machine.types.iteUnresolvedValue
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.util.EtsHierarchy
+import org.usvm.util.InputPropertyDeclaration
+import org.usvm.util.declaredInstanceProperty
 import org.usvm.util.getAllMethods
 import org.usvm.util.mkFieldLValue
 
@@ -44,39 +44,11 @@ private fun <S : USort> propertyLValue(sort: S, ref: UHeapRef, name: String, slo
 internal fun TsContext.initialPropertyPresenceLValue(ref: UHeapRef, name: String): UFieldLValue<*, UBoolSort> =
     propertyLValue(boolSort, ref, name, PropertySlot.INITIAL_PRESENCE, written = false)
 
-internal data class InputPropertyDeclaration(val type: EtsType, val optional: Boolean)
-
-/** Resolve receiver-local metadata; independent declarations must agree on type and optionality. */
 internal fun declaredInputProperty(
     local: EtsLocal?,
     name: String,
     hierarchy: EtsHierarchy,
-): InputPropertyDeclaration? {
-    val type = local?.type
-    if (type !is EtsClassType && type !is EtsUnclearRefType) return null
-
-    val declarations = hierarchy.classesForType(type).map { receiver ->
-        val fieldOwners = hierarchy.getAncestors(receiver).filter { owner ->
-            owner.fields.any { !it.isStatic && it.name == name }
-        }
-        // A class field defines the value even when an implemented interface has a weaker contract.
-        val classOwners = fieldOwners.filter { it.category != EtsClassCategory.INTERFACE }
-        val owners = classOwners.ifEmpty { fieldOwners }
-
-        // A redeclaration shadows the ancestor's type and optional flag.
-        val nearestOwners = owners.filter { owner ->
-            owners.none { descendant -> owner != descendant && owner in hierarchy.getAncestors(descendant) }
-        }
-        nearestOwners.flatMap { owner -> owner.fields.filter { !it.isStatic && it.name == name } }
-            .map { field ->
-                InputPropertyDeclaration(field.type, optional = (field as? EtsFieldImpl)?.isOptional == true)
-            }
-            .distinct()
-            .singleOrNull()
-    }
-    // An unresolved receiver may denote several classes. Keep metadata only when every candidate agrees.
-    return declarations.distinct().singleOrNull()
-}
+): InputPropertyDeclaration? = declaredInstanceProperty(local?.type, name, hierarchy)
 
 internal fun TsContext.trackInputProperty(
     scope: TsStepScope,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
index b6b34f38b0..7593ac8c2a 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt
@@ -43,6 +43,7 @@ import org.usvm.machine.types.mkFakeValue
 import org.usvm.machine.types.requiresConstructorWitness
 import org.usvm.machine.types.toAuxiliaryType
 import org.usvm.util.EtsHierarchy
+import org.usvm.util.InputPropertyDeclaration
 import org.usvm.util.TsResolutionResult
 import org.usvm.util.arrayStorageType
 import org.usvm.util.createFakeField
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/InputPropertyDeclaration.kt b/usvm-ts/src/main/kotlin/org/usvm/util/InputPropertyDeclaration.kt
new file mode 100644
index 0000000000..07dbcd5890
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/InputPropertyDeclaration.kt
@@ -0,0 +1,41 @@
+package org.usvm.util
+
+import org.jacodb.ets.model.EtsClassCategory
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsFieldImpl
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnclearRefType
+
+/** Resolved own or inherited data-field metadata for a declared receiver type. */
+data class InputPropertyDeclaration(val type: EtsType, val optional: Boolean)
+
+/** Resolve receiver-local metadata; independent declarations must agree on type and optionality. */
+fun declaredInstanceProperty(
+    type: EtsType?,
+    name: String,
+    hierarchy: EtsHierarchy,
+): InputPropertyDeclaration? {
+    if (type !is EtsClassType && type !is EtsUnclearRefType) return null
+
+    val declarations = hierarchy.classesForType(type).map { receiver ->
+        val fieldOwners = hierarchy.getAncestors(receiver).filter { owner ->
+            owner.fields.any { !it.isStatic && it.name == name }
+        }
+        // A class field defines the value even when an implemented interface has a weaker contract.
+        val classOwners = fieldOwners.filter { it.category != EtsClassCategory.INTERFACE }
+        val owners = classOwners.ifEmpty { fieldOwners }
+
+        // A redeclaration shadows the ancestor's type and optional flag.
+        val nearestOwners = owners.filter { owner ->
+            owners.none { descendant -> owner != descendant && owner in hierarchy.getAncestors(descendant) }
+        }
+        nearestOwners.flatMap { owner -> owner.fields.filter { !it.isStatic && it.name == name } }
+            .map { field ->
+                InputPropertyDeclaration(field.type, optional = (field as? EtsFieldImpl)?.isOptional == true)
+            }
+            .distinct()
+            .singleOrNull()
+    }
+    // An unresolved receiver may denote several classes. Keep metadata only when every candidate agrees.
+    return declarations.distinct().singleOrNull()
+}