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 b7767ed426..69da1df9d2 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
@@ -149,19 +149,29 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
             MachineResult(
                 states = entryObserver.reachedStates,
                 stopReason = outcome.stopReason,
+                unsupportedPaths = outcome.unsupportedPaths,
             )
         }
         val states = analysis.states
         if (states.isEmpty()) {
             val status = when (analysis.stopReason) {
-                TsAnalysisStopReason.EXHAUSTED -> CallsSymbolicStatus.UNREACHED
+                TsAnalysisStopReason.EXHAUSTED -> {
+                    if (analysis.unsupportedPaths.isEmpty()) {
+                        CallsSymbolicStatus.UNREACHED
+                    } else {
+                        CallsSymbolicStatus.UNSUPPORTED
+                    }
+                }
                 // The machine options above disable every stop condition except the per-target timeout.
-                TsAnalysisStopReason.STOPPED -> CallsSymbolicStatus.TIMEOUT
+                TsAnalysisStopReason.STOPPED -> {
+                    CallsSymbolicStatus.TIMEOUT
+                }
             }
 
             return result(
                 status = status,
                 startedAt = startedAt,
+                diagnostic = analysis.unsupportedPaths.joinToString().ifEmpty { null },
             )
         }
 
@@ -284,6 +294,7 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine {
     private data class MachineResult(
         val states: List<TsState>,
         val stopReason: TsAnalysisStopReason,
+        val unsupportedPaths: List<String>,
     )
 }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
index e58f45f474..a394c69d8f 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanLiteralType
 import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsLexicalEnvType
@@ -17,6 +18,7 @@ import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberLiteralType
 import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsParameterRef
+import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringLiteralType
@@ -66,6 +68,9 @@ class TsContext(
 
     val unresolvedSort: TsUnresolvedSort = TsUnresolvedSort(this)
 
+    /** Array storage for UTF-16 code units; ordinary TypeScript arrays never use this region. */
+    internal val stringBackingArrayDescriptor: EtsType = EtsRawType(kind = "usvm.ts.string.backing")
+
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
@@ -87,6 +92,18 @@ class TsContext(
     // String constant caching at context level
     private val stringConstants: MutableMap<String, UConcreteHeapRef> = mutableMapOf()
 
+    private val classConstructorRefs: MutableMap<EtsClassSignature, UConcreteHeapRef> = mutableMapOf()
+    private val constructorSignatures: MutableMap<UConcreteHeapRef, EtsClassSignature> = mutableMapOf()
+
+    fun classConstructorRef(signature: EtsClassSignature): UConcreteHeapRef =
+        classConstructorRefs.getOrPut(signature) {
+            allocateStaticRef().also { constructorSignatures[it] = signature }
+        }
+
+    fun classConstructorSignature(ref: UConcreteHeapRef): EtsClassSignature? = constructorSignatures[ref]
+
+    fun classConstructorRefs(): Collection<UConcreteHeapRef> = classConstructorRefs.values
+
     /**
      * Reverse mapping from heap references to their original string constant values.
      * This is used during test resolution to retrieve the actual string content when
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index 5c5d344b3b..da08c28390 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -1,9 +1,22 @@
 package org.usvm.machine
 
 import mu.KotlinLogging
+import org.jacodb.ets.model.EtsAliasType
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsClass
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsClassValueType
+import org.jacodb.ets.model.EtsFileSignature
+import org.jacodb.ets.model.EtsGenericType
+import org.jacodb.ets.model.EtsIntersectionType
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsTupleType
+import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnclearRefType
+import org.jacodb.ets.model.EtsUnionType
 import org.usvm.CoverageZone
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
@@ -49,6 +62,8 @@ enum class TsAnalysisStopReason {
 data class TsAnalysisResult(
     val states: List<TsState>,
     val stopReason: TsAnalysisStopReason,
+    /** Reasons for satisfiable paths excluded by an explicit engine model bound. */
+    val unsupportedPaths: List<String>,
 )
 
 class TsMachine(
@@ -101,6 +116,7 @@ class TsMachine(
     )
     private val cfgStatistics = CfgStatisticsImpl(graph)
 
+    /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */
     fun analyze(
         methods: List<EtsMethod>,
         targets: List<TsTarget> = emptyList(),
@@ -110,12 +126,15 @@ class TsMachine(
         methods: List<EtsMethod>,
         targets: List<TsTarget> = emptyList(),
     ): TsAnalysisResult {
-        val initialStates = mutableMapOf<EtsMethod, TsState>()
-        methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) }
+        val (initialStates, unsupportedPaths) = createInitialStates(methods, targets)
+
+        if (initialStates.isEmpty()) {
+            return TsAnalysisResult(emptyList(), TsAnalysisStopReason.EXHAUSTED, unsupportedPaths.toList())
+        }
 
         val methodsToTrackCoverage =
             when (options.coverageZone) {
-                CoverageZone.METHOD, CoverageZone.TRANSITIVE -> methods.toHashSet()
+                CoverageZone.METHOD, CoverageZone.TRANSITIVE -> initialStates.keys.toHashSet()
                 CoverageZone.CLASS -> TODO("Unsupported yet")
             }
 
@@ -154,7 +173,6 @@ class TsMachine(
 
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
-
         if (tsOptions.enableVisualization) {
             observers += TsStateVisualizer()
         }
@@ -192,7 +210,7 @@ class TsMachine(
         if (logger.isInfoEnabled) {
             observers.add(
                 StatisticsByMethodPrinter(
-                    getMethods = { methods },
+                    getMethods = { initialStates.keys.toList() },
                     print = logger::info,
                     getMethodSignature = { it.humanReadableSignature },
                     coverageStatistics = coverageStatistics,
@@ -202,10 +220,25 @@ class TsMachine(
             )
         }
 
+        val supportedObserver = CompositeUMachineObserver(observers)
+        val outcomeObserver = object : UMachineObserver<TsState> by supportedObserver {
+            override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
+                val unsupportedReason = state.unsupportedReason
+                if (unsupportedReason != null) {
+                    if (stateReachable) {
+                        unsupportedPaths += unsupportedReason
+                    }
+                    return
+                }
+
+                supportedObserver.onStateTerminated(state, stateReachable)
+            }
+        }
+
         run(
             interpreter,
             pathSelector,
-            observer = CompositeUMachineObserver(observers),
+            observer = outcomeObserver,
             isStateTerminated = { state -> state.callStack.isEmpty() },
             stopStrategy = stopStrategy
         )
@@ -216,10 +249,172 @@ class TsMachine(
             TsAnalysisStopReason.STOPPED
         }
 
-        return TsAnalysisResult(states = statesCollector.collectedStates, stopReason = stopReason)
+        return TsAnalysisResult(
+            states = statesCollector.collectedStates,
+            stopReason = stopReason,
+            unsupportedPaths = unsupportedPaths.toList(),
+        )
+    }
+
+    private fun createInitialStates(
+        methods: List<EtsMethod>,
+        targets: List<TsTarget>,
+    ): Pair<Map<EtsMethod, TsState>, MutableSet<String>> {
+        val initialStates = mutableMapOf<EtsMethod, TsState>()
+        val unsupportedPaths = mutableSetOf<String>()
+        val classesBySignature = analysisScene.projectAndSdkClasses.associateBy { it.signature }
+
+        methods.forEach { method ->
+            val genericParameters = method.typeParameters.filterIsInstance<EtsGenericType>().associateBy { it.typeName }
+            val unsupportedParameter = method.parameters.firstNotNullOfOrNull { parameter ->
+                val gap = parameter.type.constructorInputGap(genericParameters, classesBySignature)
+                gap?.let { parameter to it }
+            }
+            if (unsupportedParameter != null) {
+                val (parameter, gap) = unsupportedParameter
+                unsupportedPaths += "${gap.description} '${parameter.name}' " +
+                    "in ${method.humanReadableSignature} is not modeled"
+            } else {
+                initialStates[method] = interpreter.getInitialState(method, targets)
+            }
+        }
+
+        return initialStates to unsupportedPaths
     }
 
     override fun close() {
         components.close()
     }
 }
+
+private enum class ConstructorInputGap(val description: String) {
+    CONSTRUCTOR_VALUE("Constructor-typed parameter"),
+    UNRESOLVED_INHERITED_GENERIC("Unresolved inherited generic field in parameter"),
+}
+
+private fun EtsType.constructorInputGap(
+    genericParameters: Map<String, EtsGenericType>,
+    classesBySignature: Map<EtsClassSignature, EtsClass>,
+    visitedGenerics: Set<String> = emptySet(),
+    visitedClasses: Set<EtsClassSignature> = emptySet(),
+): ConstructorInputGap? = when (this) {
+    is EtsClassValueType -> ConstructorInputGap.CONSTRUCTOR_VALUE
+    is EtsUnionType -> types.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsIntersectionType -> types.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsTupleType -> types.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsArrayType -> elementType.constructorInputGap(
+        genericParameters,
+        classesBySignature,
+        visitedGenerics,
+        visitedClasses,
+    )
+    is EtsClassType -> constructorInputGapInClass(
+        genericParameters,
+        classesBySignature,
+        visitedGenerics,
+        visitedClasses,
+    )
+    is EtsUnclearRefType -> typeParameters.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    is EtsAliasType -> originalType.constructorInputGap(
+        genericParameters,
+        classesBySignature,
+        visitedGenerics,
+        visitedClasses,
+    )
+    is EtsGenericType -> {
+        if (typeName in visitedGenerics) {
+            null
+        } else {
+            val declaration = genericParameters[typeName]
+            listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType)
+                .firstNotNullOfOrNull {
+                    it.constructorInputGap(
+                        genericParameters,
+                        classesBySignature,
+                        visitedGenerics + typeName,
+                        visitedClasses,
+                    )
+                }
+        }
+    }
+    else -> null
+}
+
+private fun EtsClassType.constructorInputGapInClass(
+    genericParameters: Map<String, EtsGenericType>,
+    classesBySignature: Map<EtsClassSignature, EtsClass>,
+    visitedGenerics: Set<String>,
+    visitedClasses: Set<EtsClassSignature>,
+): ConstructorInputGap? {
+    val typeArgumentGap = typeParameters.firstNotNullOfOrNull {
+        it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses)
+    }
+    if (typeArgumentGap != null) {
+        return typeArgumentGap
+    }
+
+    if (signature in visitedClasses) {
+        return null
+    }
+
+    val clazz = classesBySignature[signature] ?: return null
+    val nextVisitedClasses = visitedClasses + signature
+    val fieldGap = clazz.fields.firstNotNullOfOrNull { field ->
+        if (field.modifiers.isStatic) return@firstNotNullOfOrNull null
+
+        field.type.constructorInputGap(
+            genericParameters,
+            classesBySignature,
+            visitedGenerics,
+            nextVisitedClasses,
+        )
+    }
+    if (fieldGap != null) {
+        return fieldGap
+    }
+
+    val superClass = clazz.superClass ?: return null
+    val superClasses = if (superClass.file == EtsFileSignature.UNKNOWN) {
+        classesBySignature.values.filter { it.name == superClass.name }
+    } else {
+        listOfNotNull(classesBySignature[superClass])
+    }
+
+    return superClasses.firstNotNullOfOrNull { parent ->
+        val parentGap = EtsClassType(parent.signature).constructorInputGap(
+            genericParameters,
+            classesBySignature,
+            visitedGenerics,
+            nextVisitedClasses,
+        )
+        if (parentGap != null) return@firstNotNullOfOrNull parentGap
+
+        // The frontend omits extends type arguments, so an inherited T may contain a constructor.
+        val parentGenerics = parent.typeParameters.filterIsInstance<EtsGenericType>()
+            .mapTo(mutableSetOf()) { it.typeName }
+        val unresolvedGenericField = parent.fields.any { field ->
+            !field.modifiers.isStatic && field.type.containsGeneric(parentGenerics)
+        }
+        if (unresolvedGenericField) ConstructorInputGap.UNRESOLVED_INHERITED_GENERIC else null
+    }
+}
+
+private fun EtsType.containsGeneric(names: Set<String>): Boolean = when (this) {
+    is EtsGenericType -> typeName in names
+    is EtsUnionType -> types.any { it.containsGeneric(names) }
+    is EtsIntersectionType -> types.any { it.containsGeneric(names) }
+    is EtsTupleType -> types.any { it.containsGeneric(names) }
+    is EtsArrayType -> elementType.containsGeneric(names)
+    is EtsClassType -> typeParameters.any { it.containsGeneric(names) }
+    is EtsUnclearRefType -> typeParameters.any { it.containsGeneric(names) }
+    is EtsAliasType -> originalType.containsGeneric(names)
+    else -> false
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt
new file mode 100644
index 0000000000..9a6d36d630
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt
@@ -0,0 +1,17 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsFileSignature
+
+private val runtimeFile = EtsFileSignature(
+    projectName = "usvm.ts.runtime",
+    fileName = "TypeError",
+)
+private val typeErrorSignature = EtsClassSignature(
+    name = "TypeError",
+    file = runtimeFile,
+)
+
+/** Type identity of terminal JavaScript TypeError exceptions produced by the interpreter. */
+internal val TS_TYPE_ERROR_TYPE = EtsClassType(typeErrorSignature)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
index 86444e1054..61fa030a29 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt
@@ -6,14 +6,19 @@ import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsStringType
+import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnknownType
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsSizeSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.sizeSort
 import org.usvm.util.arrayStorageType
 import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.mkFieldLValue
+import org.usvm.util.mkStringBackingLengthLValue
 
 // Handles reading the `length` property.
 fun TsContext.readLengthProperty(
@@ -34,31 +39,39 @@ fun TsContext.readLengthProperty(
         }
 
         is EtsStringType -> {
-            // Strings are treated as arrays of characters (represented as strings).
-            EtsArrayType(EtsStringType, dimensions = 1)
+            val charsRef = scope.calcOnState {
+                val valueLValue = mkFieldLValue(addressSort, instance, field = "value")
+                memory.read(valueLValue)
+            }
+
+            return readArrayLength(
+                scope = scope,
+                lengthLValue = mkStringBackingLengthLValue(charsRef),
+                maxArraySize = maxArraySize,
+            )
         }
 
         else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type")
     }
 
     // Read the length of the array.
-    return readArrayLength(scope, instance, arrayType, maxArraySize)
+    return readArrayLength(
+        scope = scope,
+        lengthLValue = mkArrayLengthLValue(instance, arrayType),
+        maxArraySize = maxArraySize,
+    )
 }
 
 // Reads the length of the array and returns it as a fp64 expression.
 fun TsContext.readArrayLength(
     scope: TsStepScope,
-    array: UHeapRef,
-    arrayType: EtsArrayType,
+    lengthLValue: UArrayLengthLValue<EtsType, TsSizeSort>,
     maxArraySize: Int,
 ): UExpr<KFp64Sort>? {
-    checkNotFake(array)
+    checkNotFake(lengthLValue.ref)
 
     // Read the length of the array.
-    val length = scope.calcOnState {
-        val lengthLValue = mkArrayLengthLValue(array, arrayType)
-        memory.read(lengthLValue)
-    }
+    val length = scope.calcOnState { memory.read(lengthLValue) }
 
     // Check that the length is within the allowed bounds.
     ensureLengthBounds(scope, length, maxArraySize) ?: return null
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 66184e3d19..9f94f38c80 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -18,7 +18,10 @@ import org.jacodb.ets.model.EtsBitXorExpr
 import org.jacodb.ets.model.EtsBooleanConstant
 import org.jacodb.ets.model.EtsCastExpr
 import org.jacodb.ets.model.EtsCaughtExceptionRef
+import org.jacodb.ets.model.EtsClassCategory
 import org.jacodb.ets.model.EtsClassSignature
+import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsClassValueRef
 import org.jacodb.ets.model.EtsClosureFieldRef
 import org.jacodb.ets.model.EtsConstant
 import org.jacodb.ets.model.EtsDeleteExpr
@@ -89,9 +92,11 @@ import org.usvm.api.allocateConcreteRef
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.initializeArrayLength
 import org.usvm.api.makeSymbolicPrimitive
+import org.usvm.api.typeStreamOf
 import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.machine.TS_TYPE_ERROR_TYPE
 import org.usvm.machine.TsConcreteMethodCallStmt
 import org.usvm.machine.TsContext
 import org.usvm.machine.TsOptions
@@ -114,6 +119,7 @@ import org.usvm.machine.state.newStmt
 import org.usvm.machine.types.EtsNominalType
 import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.sizeSort
+import org.usvm.types.TypesResult
 import org.usvm.util.EtsHierarchy
 import org.usvm.util.SymbolResolutionResult
 import org.usvm.util.isResolved
@@ -208,6 +214,8 @@ class TsExprResolver(
         return simpleValueResolver.visit(value)
     }
 
+    override fun visit(value: EtsClassValueRef): UExpr<out USort> = ctx.classConstructorRef(value.signature)
+
     override fun visit(value: EtsParameterRef): UExpr<out USort>? {
         return simpleValueResolver.visit(value)
     }
@@ -326,6 +334,11 @@ class TsExprResolver(
 
     override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) {
         val resolvedExpr = resolve(expr.arg) ?: return@with null
+        if (resolvedExpr is UConcreteHeapRef && classConstructorSignature(resolvedExpr) != null) {
+            // TypeScript assertions do not change the identity of a constructor at runtime.
+            return@with resolvedExpr
+        }
+
         return when (resolvedExpr.sort) {
             fp64Sort -> {
                 logger.error("Unsupported cast from fp ${expr.arg} to ${expr.type}")
@@ -375,47 +388,49 @@ class TsExprResolver(
             return mkStringConstant("boolean", scope)
         }
         if (arg.sort == addressSort) {
-            val ref = arg.asExpr(addressSort)
-            return mkIte(
-                condition = mkHeapRefEq(ref, mkTsNullValue()),
-                trueBranch = mkStringConstant("object", scope),
-                falseBranch = mkIte(
-                    condition = mkHeapRefEq(ref, mkUndefinedValue()),
-                    trueBranch = mkStringConstant("undefined", scope),
-                    falseBranch = mkIte(
-                        condition = scope.calcOnState {
-                            val unwrappedRef = ref.unwrapRefWithPathConstraint(scope)
-
-                            // TODO: adhoc: "expand" ITE
-                            if (unwrappedRef is UIteExpr<*>) {
-                                val trueBranch = unwrappedRef.trueBranch
-                                val falseBranch = unwrappedRef.falseBranch
-                                if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) {
-                                    val unwrappedTrueExpr =
-                                        trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
-                                    val unwrappedFalseExpr =
-                                        falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
-                                    return@calcOnState mkIte(
-                                        condition = unwrappedRef.condition,
-                                        trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType),
-                                        falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType),
-                                    )
-                                }
-                            }
-
-                            memory.types.evalTypeEquals(unwrappedRef, EtsStringType)
-                        },
-                        trueBranch = mkStringConstant("string", scope),
-                        falseBranch = mkStringConstant("object", scope),
-                    )
-                )
-            )
+            return resolveReferenceTypeof(arg.asExpr(addressSort))
         }
 
         logger.error { "visit(${expr::class.simpleName}) is not implemented yet" }
         error("Not supported $expr")
     }
 
+    private fun resolveReferenceTypeof(ref: UHeapRef): UExpr<out USort> = with(ctx) {
+        val functionValue = mkStringConstant("function", scope)
+        if (ref is UConcreteHeapRef && classConstructorSignature(ref) != null) return functionValue
+
+        val objectValue = mkStringConstant("object", scope)
+        val stringValue = mkStringConstant("string", scope)
+        val undefinedValue = mkStringConstant("undefined", scope)
+
+        val isClassConstructor = classConstructorRefs()
+            .map { constructorRef -> mkHeapRefEq(ref, constructorRef) }
+            .let { matches -> if (matches.isEmpty()) falseExpr else mkOr(matches) }
+        val isString = scope.calcOnState {
+            val unwrappedRef = ref.unwrapRefWithPathConstraint(scope)
+            val ite = unwrappedRef as? UIteExpr<*>
+
+            // TODO: adhoc: "expand" ITE
+            if (ite != null && (ite.trueBranch.isFakeObject() || ite.falseBranch.isFakeObject())) {
+                val unwrappedTrueExpr = ite.trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
+                val unwrappedFalseExpr = ite.falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope)
+                mkIte(
+                    condition = ite.condition,
+                    trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType),
+                    falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType),
+                )
+            } else {
+                memory.types.evalTypeEquals(unwrappedRef, EtsStringType)
+            }
+        }
+        val isUndefined = mkHeapRefEq(ref, mkUndefinedValue())
+        val isNull = mkHeapRefEq(ref, mkTsNullValue())
+        val objectOrString = mkIte(isString, stringValue, objectValue)
+        val objectOrFunction = mkIte(isClassConstructor, functionValue, objectOrString)
+        val notNull = mkIte(isUndefined, undefinedValue, objectOrFunction)
+        mkIte(isNull, objectValue, notNull)
+    }
+
     override fun visit(expr: EtsDeleteExpr): UExpr<out USort>? = with(ctx) {
         logger.warn {
             "delete operator is not fully supported, the result may not be accurate"
@@ -888,12 +903,125 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsInstanceOfExpr): UExpr<out USort>? = with(ctx) {
-        val arg = resolve(expr.arg)?.asExpr(addressSort) ?: return null
-        val checkType = expr.checkType as? EtsRefType ?: return falseExpr
+        val arg = resolve(expr.arg) ?: return null
+        val checkValue = expr.checkValue
 
-        scope.calcOnState {
-            memory.types.evalIsSubtype(arg, EtsNominalType(checkType))
+        val checkType = if (checkValue == null) {
+            // Legacy EtsIR contains only a static target. New frontend IR always evaluates the RHS.
+            expr.checkType as? EtsRefType
+                ?: return falseExpr
+        } else {
+            resolveInstanceofConstructor(checkValue) ?: return null
+        }
+
+        if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr
+        if (arg is UConcreteHeapRef && classConstructorSignature(arg) != null) {
+            if (checkType is EtsClassType && scene.projectClasses.any { it.signature == checkType.signature }) {
+                return falseExpr
+            }
+
+            throw UnsupportedOperationException(
+                "instanceof on a class constructor against an SDK or unknown class is not modeled"
+            )
+        }
+
+        if (arg.isFakeObject()) {
+            val fakeType = arg.getFakeType(scope)
+            val refValue = arg.extractRef(scope)
+            val isInstance = scope.calcOnState {
+                memory.types.evalIsSubtype(refValue, EtsNominalType(checkType))
+            }
+
+            return mkAnd(
+                fakeType.refTypeExpr,
+                mkHeapRefEq(refValue, mkTsNullValue()).not(),
+                mkHeapRefEq(refValue, mkUndefinedValue()).not(),
+                isInstance,
+            )
+        }
+
+        val objectRef = arg.asExpr(addressSort)
+        if (isAllocatedConcreteHeapRef(objectRef) && checkType is EtsClassType) {
+            val objectTypes = scope.calcOnState { memory.typeStreamOf(objectRef).take(2) }
+            val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull() as? EtsClassType
+            if (objectType != null) {
+                val objectClass = hierarchy.classesForType(objectType).singleOrNull()
+                    ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType")
+                val constructorClass = hierarchy.classesForType(checkType).singleOrNull()
+                    ?: throw UnsupportedOperationException("Unknown instanceof constructor class: $checkType")
+                return mkBool(constructorClass in hierarchy.getAncestors(objectClass))
+            }
         }
+
+        scope.calcOnState { memory.types.evalIsSubtype(objectRef, EtsNominalType(checkType)) }
+    }
+
+    private fun resolveInstanceofConstructor(checkValue: EtsEntity): EtsClassType? = with(ctx) {
+        val constructor = resolve(checkValue) ?: return null
+        if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwInstanceofTypeError()
+        if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwInstanceofTypeError()
+
+        if (constructor.sort != addressSort || constructor.isFakeObject()) {
+            throw UnsupportedOperationException("Unresolved instanceof RHS callability is not modeled")
+        }
+
+        val constructorRef = constructor as? UConcreteHeapRef
+            ?: throw UnsupportedOperationException("Symbolic instanceof constructor identity is not modeled")
+        if (getStringConstantValue(constructorRef) != null) return throwInstanceofTypeError()
+
+        val signature = classConstructorSignature(constructorRef)
+            ?: return resolveNonConstructorInstanceofRight(constructorRef)
+        val clazz = scene.projectAndSdkClasses.singleOrNull { it.signature == signature }
+            ?: throw UnsupportedOperationException("Unknown instanceof class: $signature")
+        val hasPotentialCustomHasInstance = hierarchy.getAncestors(clazz).any { ancestor ->
+            ancestor.methods.any { method ->
+                method.modifiers.isStatic && (method.name == "%computed" || method.name == "Symbol.hasInstance")
+            } || ancestor.fields.any { field ->
+                field.modifiers.isStatic && (field.name == "%computed" || field.name == "Symbol.hasInstance")
+            }
+        }
+        if (hasPotentialCustomHasInstance) {
+            throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature")
+        }
+
+        EtsClassType(signature)
+    }
+
+    private fun resolveNonConstructorInstanceofRight(ref: UConcreteHeapRef): Nothing? = with(ctx) {
+        val objectTypes = if (isAllocatedConcreteHeapRef(ref)) {
+            scope.calcOnState { memory.typeStreamOf(ref).take(n = 2) }
+        } else {
+            null
+        }
+        val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull()
+        if (objectType == EtsStringType) return throwInstanceofTypeError()
+
+        val objectClass = (objectType as? EtsClassType)?.let { type ->
+            scene.projectClasses.singleOrNull { it.signature == type.signature }
+        }
+        if (objectClass != null) {
+            // Computed members may include Symbol.hasInstance, so their instances need a separate model.
+            val ordinaryObject = objectClass.category == EtsClassCategory.CLASS ||
+                objectClass.category == EtsClassCategory.OBJECT
+            val hasComputedMember = hierarchy.getAncestors(objectClass).any { ancestor ->
+                ancestor.methods.any { it.name == "%computed" || it.name == "Symbol.hasInstance" } ||
+                    ancestor.fields.any { it.name == "%computed" || it.name == "Symbol.hasInstance" }
+            }
+            val isFunction = scope.calcOnState { associatedFunction[ref] != null }
+
+            if (ordinaryObject && !hasComputedMember && !isFunction) return throwInstanceofTypeError()
+        }
+
+        throw UnsupportedOperationException("Unknown instanceof constructor value: $ref")
+    }
+
+    private fun throwInstanceofTypeError(): Nothing? {
+        scope.doWithState {
+            val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE)
+            methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE)
+        }
+
+        return null
     }
 
     // endregion
@@ -1311,6 +1439,8 @@ class TsSimpleValueResolver(
         return resolveLocal(value)
     }
 
+    override fun visit(value: EtsClassValueRef): UExpr<out USort> = ctx.classConstructorRef(value.signature)
+
     override fun visit(value: EtsConstant): UExpr<out USort> = with(ctx) {
         logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
         error("Not supported $value")
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
index f5ea96ef7a..b15e04d2b1 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
@@ -82,6 +82,7 @@ import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
+import org.usvm.util.mkStringBackingLengthLValue
 import org.usvm.util.resolveEtsMethods
 import org.usvm.util.type
 import org.usvm.utils.ensureSat
@@ -150,6 +151,18 @@ class TsInterpreter(
                     }
                 }
             }
+        } catch (e: UnsupportedOperationException) {
+            if (throwExceptionOnStepFailure) {
+                throw e
+            }
+
+            val reason = e.message?.takeIf(String::isNotBlank) ?: "Unsupported TypeScript operation"
+            state.terminateAsUnsupported(reason)
+
+            return StepResult(
+                forkedStates = scope.stepResult().forkedStates,
+                originalStateAlive = true,
+            )
         } catch (e: Exception) {
             if (throwExceptionOnStepFailure) {
                 throw e
@@ -743,6 +756,7 @@ class TsInterpreter(
             ctx = ctx,
             ownership = MutabilityOwnership(),
             entrypoint = method,
+            maxStringLength = options.maxArraySize,
             targets = UTargetsSet.from(targets),
         )
 
@@ -811,6 +825,20 @@ class TsInterpreter(
                 state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
 
                 state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType)
+
+                // String constants store UTF-16 code units in their `value` array.
+                // Give symbolic inputs the same backing representation and bound its length.
+                val charsType = EtsArrayType(EtsNumberType, dimensions = 1)
+                val valueLValue = mkFieldLValue(addressSort, ref, field = "value")
+                val charsRef = state.memory.read(valueLValue).asExpr(addressSort)
+                state.pathConstraints += mkNot(mkHeapRefEq(charsRef, mkUndefinedValue()))
+                state.pathConstraints += state.memory.types.evalTypeEquals(charsRef, charsType)
+
+                val lengthLValue = mkStringBackingLengthLValue(charsRef)
+                val length = state.memory.read(lengthLValue).asExpr(sizeSort)
+                state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0))
+                state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize))
+                state.boundedStringBackingRefs += ref
             }
 
             val parameterSort = typeToSort(parameterType)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
index 9e4e1db477..03f28f177a 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
@@ -4,23 +4,159 @@ import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
 import io.ksmt.utils.cast
 import mu.KotlinLogging
+import org.jacodb.ets.model.EtsStringType
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.UIteExpr
 import org.usvm.USort
+import org.usvm.api.evalTypeEquals
+import org.usvm.isFalse
+import org.usvm.isTrue
 import org.usvm.machine.TsContext
+import org.usvm.machine.TsSizeSort
 import org.usvm.machine.expr.mkNumericExpr
 import org.usvm.machine.expr.mkTruthyExpr
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.types.ExprWithTypeConstraint
 import org.usvm.machine.types.iteWriteIntoFakeObject
 import org.usvm.util.boolToFp
+import org.usvm.util.mkFieldLValue
+import org.usvm.util.mkStringBackingElementLValue
+import org.usvm.util.mkStringBackingLengthLValue
 
 private val logger = KotlinLogging.logger {}
 
+/** Strings are primitive values even though the TS heap stores their UTF-16 contents behind references. */
+private fun TsContext.stringValueEquals(
+    lhs: UHeapRef,
+    rhs: UHeapRef,
+    sameReference: UBoolExpr,
+    activeGuard: UBoolExpr,
+    scope: TsStepScope,
+): UBoolExpr? {
+    val lhsConstant = (lhs as? UConcreteHeapRef)?.let(::getStringConstantValue)
+    val rhsConstant = (rhs as? UConcreteHeapRef)?.let(::getStringConstantValue)
+    if (lhsConstant != null && rhsConstant != null) {
+        return if (lhsConstant == rhsConstant) trueExpr else falseExpr
+    }
+
+    val (lhsIsString, rhsIsString) = scope.calcOnState {
+        memory.types.evalTypeEquals(lhs, EtsStringType) to memory.types.evalTypeEquals(rhs, EtsStringType)
+    }
+    if (lhsIsString.isFalse || rhsIsString.isFalse) return falseExpr
+
+    val bothStrings = mkAnd(lhsIsString, rhsIsString)
+    val missingBacking = scope.calcOnState {
+        (lhsConstant == null && lhs !in boundedStringBackingRefs) ||
+            (rhsConstant == null && rhs !in boundedStringBackingRefs)
+    }
+    // An alias of a known literal has that literal's value without reading a symbolic backing array.
+    val knownLiteralAlias = if (lhsConstant != null || rhsConstant != null) sameReference else falseExpr
+    val notBothStrings = mkNot(bothStrings)
+    val lhsNullish = mkOr(mkHeapRefEq(lhs, mkTsNullValue()), mkHeapRefEq(lhs, mkUndefinedValue()))
+    val rhsNullish = mkOr(mkHeapRefEq(rhs, mkTsNullValue()), mkHeapRefEq(rhs, mkUndefinedValue()))
+    if (missingBacking) {
+        val supportedWithoutBacking = mkOr(
+            mkNot(activeGuard),
+            knownLiteralAlias,
+            lhsNullish,
+            rhsNullish,
+            notBothStrings,
+        )
+        scope.fork(supportedWithoutBacking, blockOnFalseState = {
+            terminateAsUnsupported(reason = "String equality needs a modeled string backing for dynamic references")
+        }) ?: return null
+        return falseExpr
+    }
+
+    val comparison = scope.calcOnState {
+        val lhsChars = memory.read(mkFieldLValue(addressSort, lhs, field = "value"))
+        val rhsChars = memory.read(mkFieldLValue(addressSort, rhs, field = "value"))
+        val lhsLength = memory.read(mkStringBackingLengthLValue(lhsChars))
+        val rhsLength = memory.read(mkStringBackingLengthLValue(rhsChars))
+
+        StringComparisonData(
+            lhsChars = lhsChars,
+            rhsChars = rhsChars,
+            lhsLength = lhsLength,
+            rhsLength = rhsLength,
+            maxLength = maxStringLength,
+        )
+    }
+
+    val zero = mkBv(0)
+    val maximum = mkBv(comparison.maxLength)
+    val boundedLengths = mkAnd(
+        if (lhsConstant == null) {
+            mkAnd(
+                mkBvSignedGreaterOrEqualExpr(comparison.lhsLength, zero),
+                mkBvSignedLessOrEqualExpr(comparison.lhsLength, maximum),
+            )
+        } else {
+            trueExpr
+        },
+        if (rhsConstant == null) {
+            mkAnd(
+                mkBvSignedGreaterOrEqualExpr(comparison.rhsLength, zero),
+                mkBvSignedLessOrEqualExpr(comparison.rhsLength, maximum),
+            )
+        } else {
+            trueExpr
+        },
+    )
+    val supported = mkOr(
+        mkNot(activeGuard),
+        knownLiteralAlias,
+        lhsNullish,
+        rhsNullish,
+        notBothStrings,
+        boundedLengths,
+    )
+    scope.fork(supported, blockOnFalseState = {
+        terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..$maxStringLength")
+    }) ?: return null
+
+    // Known literals supply a tighter comparison bound; all other string lengths are constrained above.
+    val comparisonLength = lhsConstant?.length ?: rhsConstant?.length ?: comparison.maxLength
+    val equalCharacters = (0 until comparisonLength).map { index ->
+        val position = mkBv(index)
+        val lhsCharacter = scope.calcOnState {
+            memory.read(mkStringBackingElementLValue(comparison.lhsChars, position))
+        }
+        val rhsCharacter = scope.calcOnState {
+            memory.read(mkStringBackingElementLValue(comparison.rhsChars, position))
+        }
+        mkImplies(mkBvSignedLessExpr(position, comparison.lhsLength), mkEq(lhsCharacter, rhsCharacter))
+    }
+
+    return mkAnd(lhsIsString, rhsIsString, mkEq(comparison.lhsLength, comparison.rhsLength), mkAnd(equalCharacters))
+}
+
+private data class StringComparisonData(
+    val lhsChars: UHeapRef,
+    val rhsChars: UHeapRef,
+    val lhsLength: UExpr<TsSizeSort>,
+    val rhsLength: UExpr<TsSizeSort>,
+    val maxLength: Int,
+)
+
+private fun TsContext.referenceOrStringValueEquals(
+    lhs: UHeapRef,
+    rhs: UHeapRef,
+    scope: TsStepScope,
+    activeGuard: UBoolExpr = trueExpr,
+): UBoolExpr? {
+    val sameReference = mkHeapRefEq(lhs, rhs)
+    if (sameReference.isTrue) return trueExpr
+
+    val equalStringValues = stringValueEquals(lhs, rhs, sameReference, activeGuard, scope) ?: return null
+    return mkOr(sameReference, equalStringValues)
+}
+
 sealed interface TsBinaryOperator {
 
     fun TsContext.onBool(
@@ -41,12 +177,26 @@ sealed interface TsBinaryOperator {
         scope: TsStepScope,
     ): UExpr<*>?
 
+    fun TsContext.onRefWithGuard(
+        lhs: UHeapRef,
+        rhs: UHeapRef,
+        scope: TsStepScope,
+        activeGuard: UBoolExpr,
+    ): UExpr<*>? = onRef(lhs, rhs, scope)
+
     fun TsContext.resolveFakeObject(
         lhs: UExpr<*>,
         rhs: UExpr<*>,
         scope: TsStepScope,
     ): UExpr<*>?
 
+    fun TsContext.resolveFakeObjectWithGuard(
+        lhs: UExpr<*>,
+        rhs: UExpr<*>,
+        scope: TsStepScope,
+        activeGuard: UBoolExpr,
+    ): UExpr<*>? = resolveFakeObject(lhs, rhs, scope)
+
     fun TsContext.internalResolve(
         lhs: UExpr<*>,
         rhs: UExpr<*>,
@@ -57,10 +207,13 @@ sealed interface TsBinaryOperator {
         lhs: UExpr<*>,
         rhs: UExpr<*>,
         scope: TsStepScope,
+        activeGuard: UBoolExpr = trueExpr,
     ): UExpr<*>? {
         if (lhs is UIteExpr<*>) {
-            val trueBranch = resolve(lhs.trueBranch, rhs, scope) ?: return null
-            val falseBranch = resolve(lhs.falseBranch, rhs, scope) ?: return null
+            val trueBranchGuard = mkAnd(activeGuard, lhs.condition)
+            val falseBranchGuard = mkAnd(activeGuard, mkNot(lhs.condition))
+            val trueBranch = resolve(lhs.trueBranch, rhs, scope, trueBranchGuard) ?: return null
+            val falseBranch = resolve(lhs.falseBranch, rhs, scope, falseBranchGuard) ?: return null
             return lhs.ctx.mkIte(
                 lhs.condition,
                 trueBranch.asExpr(falseBranch.sort),
@@ -69,8 +222,10 @@ sealed interface TsBinaryOperator {
         }
 
         if (rhs is UIteExpr<*>) {
-            val trueBranch = resolve(lhs, rhs.trueBranch, scope) ?: return null
-            val falseBranch = resolve(lhs, rhs.falseBranch, scope) ?: return null
+            val trueBranchGuard = mkAnd(activeGuard, rhs.condition)
+            val falseBranchGuard = mkAnd(activeGuard, mkNot(rhs.condition))
+            val trueBranch = resolve(lhs, rhs.trueBranch, scope, trueBranchGuard) ?: return null
+            val falseBranch = resolve(lhs, rhs.falseBranch, scope, falseBranchGuard) ?: return null
             return lhs.ctx.mkIte(
                 rhs.condition,
                 trueBranch.asExpr(falseBranch.sort),
@@ -82,7 +237,7 @@ sealed interface TsBinaryOperator {
         val rhsValue = rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs
 
         if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) {
-            return resolveFakeObject(lhsValue, rhsValue, scope)
+            return resolveFakeObjectWithGuard(lhsValue, rhsValue, scope, activeGuard)
         }
 
         val lhsSort = lhsValue.sort
@@ -90,7 +245,12 @@ sealed interface TsBinaryOperator {
             return when (lhsSort) {
                 boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope)
                 fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope)
-                addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope)
+                addressSort -> onRefWithGuard(
+                    lhsValue.asExpr(addressSort),
+                    rhsValue.asExpr(addressSort),
+                    scope,
+                    activeGuard,
+                )
                 else -> TODO("Unsupported sort $lhsSort")
             }
         }
@@ -98,11 +258,13 @@ sealed interface TsBinaryOperator {
         return internalResolve(lhsValue, rhsValue, scope)
     }
 
+    @Suppress("LongMethod")
     fun <R : USort> TsContext.commonResolveFakeObject(
         lhs: UExpr<*>,
         rhs: UExpr<*>,
         scope: TsStepScope,
         resultSort: R,
+        activeGuard: UBoolExpr = trueExpr,
         reduce: (List<ExprWithTypeConstraint<R>>) -> UExpr<R>,
     ): UExpr<R>? {
         check(lhs.isFakeObject() || rhs.isFakeObject())
@@ -180,9 +342,10 @@ sealed interface TsBinaryOperator {
                 )
 
                 // fake(ref) + fake(ref)
-                val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null
+                val refRefGuard = mkAnd(activeGuard, lhsType.refTypeExpr, rhsType.refTypeExpr)
+                val refRefExpr = onRefWithGuard(lhsRef, rhsRef, scope, refRefGuard)?.asExpr(resultSort) ?: return null
                 conjuncts += ExprWithTypeConstraint(
-                    constraint = mkAnd(lhsType.refTypeExpr, rhsType.refTypeExpr),
+                    constraint = refRefGuard,
                     expr = refRefExpr
                 )
             }
@@ -259,7 +422,12 @@ sealed interface TsBinaryOperator {
                         )
 
                         // fake(ref) + ref
-                        val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null
+                        val refRefExpr = onRefWithGuard(
+                            lhsRef,
+                            rhsRef,
+                            scope,
+                            mkAnd(activeGuard, lhsType.refTypeExpr),
+                        )?.asExpr(resultSort) ?: return null
                         conjuncts += ExprWithTypeConstraint(
                             constraint = lhsType.refTypeExpr,
                             expr = refRefExpr
@@ -344,7 +512,12 @@ sealed interface TsBinaryOperator {
                         )
 
                         // ref + fake(ref)
-                        val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null
+                        val refRefExpr = onRefWithGuard(
+                            lhsRef,
+                            rhsRef,
+                            scope,
+                            mkAnd(activeGuard, rhsType.refTypeExpr),
+                        )?.asExpr(resultSort) ?: return null
                         conjuncts += ExprWithTypeConstraint(
                             constraint = rhsType.refTypeExpr,
                             expr = refRefExpr
@@ -383,16 +556,24 @@ sealed interface TsBinaryOperator {
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UBoolExpr {
+        ): UBoolExpr? = onRefWithGuard(lhs, rhs, scope, trueExpr)
+
+        override fun TsContext.onRefWithGuard(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UBoolExpr? {
             // Note: in JavaScript, `null == undefined`
             val lhsIsNull = mkEq(lhs, mkTsNullValue())
             val rhsIsNull = mkEq(rhs, mkTsNullValue())
             val lhsIsUndefined = mkEq(lhs, mkUndefinedValue())
             val rhsIsUndefined = mkEq(rhs, mkUndefinedValue())
+            val referenceEquality = referenceOrStringValueEquals(lhs, rhs, scope, activeGuard) ?: return null
             return mkOr(
                 mkAnd(lhsIsUndefined, rhsIsNull),
                 mkAnd(lhsIsNull, rhsIsUndefined),
-                mkHeapRefEq(lhs, rhs)
+                referenceEquality,
             )
         }
 
@@ -400,21 +581,28 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UBoolExpr {
+        ): UBoolExpr? = resolveFakeObjectWithGuard(lhs, rhs, scope, trueExpr)
+
+        override fun TsContext.resolveFakeObjectWithGuard(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UBoolExpr? {
             return commonResolveFakeObject(
                 lhs,
                 rhs,
                 scope,
-                boolSort
+                boolSort,
+                activeGuard,
             ) { conjuncts -> mkAnd(conjuncts.map { (condition, value) -> mkImplies(condition, value) }) }
-                ?: error("Should not be null")
         }
 
         override fun TsContext.internalResolve(
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UBoolExpr {
+        ): UBoolExpr? {
             check(!lhs.isFakeObject() && !rhs.isFakeObject())
 
             // bool == bool
@@ -508,29 +696,47 @@ sealed interface TsBinaryOperator {
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<*>? {
             return with(Eq) {
-                onRef(lhs, rhs, scope).not()
+                onRef(lhs, rhs, scope)?.not()
             }
         }
 
+        override fun TsContext.onRefWithGuard(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UExpr<*>? = with(Eq) {
+            onRefWithGuard(lhs, rhs, scope, activeGuard)?.not()
+        }
+
         override fun TsContext.resolveFakeObject(
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<*>? {
             return with(Eq) {
-                resolveFakeObject(lhs, rhs, scope).not()
+                resolveFakeObject(lhs, rhs, scope)?.not()
             }
         }
 
+        override fun TsContext.resolveFakeObjectWithGuard(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UExpr<*>? = with(Eq) {
+            resolveFakeObjectWithGuard(lhs, rhs, scope, activeGuard)?.not()
+        }
+
         override fun TsContext.internalResolve(
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<*>? {
             return with(Eq) {
-                internalResolve(lhs, rhs, scope).not()
+                internalResolve(lhs, rhs, scope)?.not()
             }
         }
     }
@@ -556,15 +762,27 @@ sealed interface TsBinaryOperator {
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UBoolExpr {
-            return mkHeapRefEq(lhs, rhs)
-        }
+        ): UBoolExpr? = onRefWithGuard(lhs, rhs, scope, trueExpr)
+
+        override fun TsContext.onRefWithGuard(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UBoolExpr? = referenceOrStringValueEquals(lhs, rhs, scope, activeGuard)
 
         override fun TsContext.resolveFakeObject(
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UBoolExpr {
+        ): UBoolExpr? = resolveFakeObjectWithGuard(lhs, rhs, scope, trueExpr)
+
+        override fun TsContext.resolveFakeObjectWithGuard(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UBoolExpr? {
             check(lhs.isFakeObject() || rhs.isFakeObject())
 
             var lhsValue: UExpr<*> = lhs
@@ -643,14 +861,17 @@ sealed interface TsBinaryOperator {
             if (lhsValue.sort == addressSort && rhsValue.sort == addressSort) {
                 val left = lhsValue.asExpr(addressSort)
                 val right = rhsValue.asExpr(addressSort)
+                val lhsRefGuard = if (lhs.isFakeObject()) lhs.getFakeType(scope).refTypeExpr else trueExpr
+                val rhsRefGuard = if (rhs.isFakeObject()) rhs.getFakeType(scope).refTypeExpr else trueExpr
+                val refComparisonGuard = mkAnd(activeGuard, typeConstraint, lhsRefGuard, rhsRefGuard)
                 return mkAnd(
                     typeConstraint,
-                    mkHeapRefEq(left, right)
+                    onRefWithGuard(left, right, scope, refComparisonGuard) ?: return null
                 )
             }
 
             val looseEqualityConstraint = with(Eq) {
-                resolve(lhsValue, rhsValue, scope)?.asExpr(boolSort) ?: error("Should not be encountered")
+                resolve(lhsValue, rhsValue, scope, activeGuard)?.asExpr(boolSort) ?: return null
             }
 
             return mkAnd(typeConstraint, looseEqualityConstraint)
@@ -693,22 +914,40 @@ sealed interface TsBinaryOperator {
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UBoolExpr {
+        ): UBoolExpr? {
             return with(StrictEq) {
-                onRef(lhs, rhs, scope).not()
+                onRef(lhs, rhs, scope)?.not()
             }
         }
 
+        override fun TsContext.onRefWithGuard(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UBoolExpr? = with(StrictEq) {
+            onRefWithGuard(lhs, rhs, scope, activeGuard)?.not()
+        }
+
         override fun TsContext.resolveFakeObject(
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UBoolExpr {
+        ): UBoolExpr? {
             return with(StrictEq) {
-                resolveFakeObject(lhs, rhs, scope).not()
+                resolveFakeObject(lhs, rhs, scope)?.not()
             }
         }
 
+        override fun TsContext.resolveFakeObjectWithGuard(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+            activeGuard: UBoolExpr,
+        ): UBoolExpr? = with(StrictEq) {
+            resolveFakeObjectWithGuard(lhs, rhs, scope, activeGuard)?.not()
+        }
+
         override fun TsContext.internalResolve(
             lhs: UExpr<*>,
             rhs: UExpr<*>,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index 019257dd38..4dd9f42851 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -1,6 +1,5 @@
 package org.usvm.machine.state
 
-import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBlockCfg
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsFile
@@ -48,6 +47,7 @@ class TsState(
     ctx: TsContext,
     ownership: MutabilityOwnership,
     override val entrypoint: EtsMethod,
+    val maxStringLength: Int,
     callStack: UCallStack<EtsMethod, EtsStmt> = UCallStack(),
     pathConstraints: UPathConstraints<EtsType> = UPathConstraints(ctx, ownership),
     memory: UMemory<EtsType, EtsMethod> = UMemory(ctx, ownership, pathConstraints.typeConstraints),
@@ -81,6 +81,13 @@ class TsState(
      * for identical string values.
      */
     var stringConstantAllocatedRefs: UPersistentHashMap<String, UConcreteHeapRef> = persistentHashMapOf(),
+    /**
+     * References whose string backing and length bound have been modeled.
+     * A new symbolic string producer must register its reference here after creating the backing model.
+     * String literals are recognized separately through [TsContext.getStringConstantValue].
+     */
+    var boundedStringBackingRefs: Set<UHeapRef> = emptySet(),
+    var unsupportedReason: String? = null,
     private val activeUnknownCallModels: MutableList<Pair<String, Int>> = mutableListOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
@@ -93,6 +100,14 @@ class TsState(
     forkPoints = forkPoints,
     targets = targets,
 ) {
+    /** Terminates a satisfiable path that the TypeScript model cannot execute soundly. */
+    fun terminateAsUnsupported(reason: String) {
+        require(reason.isNotBlank())
+
+        unsupportedReason = reason
+        while (callStack.isNotEmpty()) callStack.pop()
+    }
+
     fun getSortForLocal(idx: Int): USort? {
         val localToSort = localToSortStack.last()
         return localToSort[idx]
@@ -254,20 +269,17 @@ class TsState(
             memory.types.allocate(ref.address, EtsStringType)
 
             // Initialize char array
-            val valueType = EtsArrayType(EtsNumberType, dimensions = 1)
-            val descriptor = ctx.arrayDescriptorOf(valueType)
-
-            val charArray = memory.allocConcrete(valueType.elementType)
+            val charArray = memory.allocConcrete(EtsNumberType)
             memory.initializeArray(
                 arrayHeapRef = charArray,
-                type = descriptor,
+                type = stringBackingArrayDescriptor,
                 sort = bv16Sort,
                 sizeSort = sizeSort,
                 contents = value.asSequence().map { mkBv(it.code, bv16Sort) },
             )
 
             // Write char array to `ref.value`
-            val valueLValue = mkFieldLValue(addressSort, ref, "value")
+            val valueLValue = mkFieldLValue(addressSort, ref, field = "value")
             memory.write(valueLValue, charArray, guard = trueExpr)
 
             ref
@@ -289,6 +301,7 @@ class TsState(
             ctx = ctx,
             ownership = cloneOwnership,
             entrypoint = entrypoint,
+            maxStringLength = maxStringLength,
             callStack = callStack.clone(),
             pathConstraints = clonedConstraints,
             memory = memory.clone(clonedConstraints.typeConstraints, newThisOwnership, cloneOwnership),
@@ -310,6 +323,8 @@ class TsState(
             dfltObject = dfltObject,
             dfltObjectFieldSorts = dfltObjectFieldSorts,
             stringConstantAllocatedRefs = stringConstantAllocatedRefs,
+            boundedStringBackingRefs = boundedStringBackingRefs,
+            unsupportedReason = unsupportedReason,
             activeUnknownCallModels = activeUnknownCallModels.toMutableList(),
         )
     }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt
index 8b319bd539..a4e8104319 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt
@@ -1,5 +1,6 @@
 package org.usvm.util
 
+import io.ksmt.sort.KBv16Sort
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsField
 import org.jacodb.ets.model.EtsFieldSignature
@@ -76,6 +77,19 @@ fun mkArrayLengthLValue(
     return UArrayLengthLValue(ref, descriptor, sizeSort)
 }
 
+internal fun mkStringBackingLengthLValue(
+    ref: UHeapRef,
+): UArrayLengthLValue<EtsType, TsSizeSort> = with(ref.tctx) {
+    UArrayLengthLValue(ref, stringBackingArrayDescriptor, sizeSort)
+}
+
+internal fun mkStringBackingElementLValue(
+    ref: UHeapRef,
+    index: UExpr<TsSizeSort>,
+): UArrayIndexLValue<EtsType, KBv16Sort, TsSizeSort> = with(ref.tctx) {
+    UArrayIndexLValue(bv16Sort, ref, index, stringBackingArrayDescriptor)
+}
+
 fun <Sort : USort> mkRegisterStackLValue(
     sort: Sort,
     idx: Int,
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt
new file mode 100644
index 0000000000..6b65a64be0
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt
@@ -0,0 +1,331 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.StateCollectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.TsUnsupportedWitnessException
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import org.usvm.util.jsString
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+import kotlin.test.assertTrue
+import kotlin.time.Duration
+
+class TsStringEqualityTest : TsMethodTestRunner() {
+    @TempDir
+    lateinit var directory: Path
+
+    private val source = getResourcePath("/models/StringEquality.ts")
+    override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)))
+    private val analysisOptions = UMachineOptions(
+        pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+        solverType = SolverType.YICES,
+        solverTimeout = Duration.INFINITE,
+        typeOperationsTimeout = Duration.INFINITE,
+        throwExceptionOnStepFailure = true,
+    )
+
+    @Test
+    fun `string equality and inequality produce replayable witnesses`() {
+        val expected = mapOf<String, (List<String>) -> Int>(
+            "equalsA" to { args -> if (args[0] == "a") 1 else 2 },
+            "notEqualsA" to { args -> if (args[0] != "a") 1 else 2 },
+            "equalsEmpty" to { args -> if (args[0].isEmpty()) 1 else 2 },
+            "equalsUnicode" to { args -> if (args[0] == "\uD83D\uDE00") 1 else 2 },
+            "equalsOther" to { args -> if (args[0] == args[1]) 1 else 2 },
+            "equalsAtLengthOne" to { args ->
+                if (args[0].length != 1 || args[1].length != 1) 3 else if (args[0] == args[1]) 1 else 2
+            },
+            "looselyEqualsOther" to { args -> if (args[0] == args[1]) 1 else 2 },
+            "looselyNotEqualsOther" to { args -> if (args[0] != args[1]) 1 else 2 },
+        )
+
+        val twoParameterMethods = setOf(
+            "equalsOther",
+            "equalsAtLengthOne",
+            "looselyEqualsOther",
+            "looselyNotEqualsOther",
+        )
+
+        expected.forEach { (name, expectedResult) ->
+            val method = getMethod(methodName = name, className = "StringEquality")
+
+            if (name in twoParameterMethods) {
+                val results = if (name == "equalsAtLengthOne") listOf(1, 2, 3) else listOf(1, 2)
+                discoverProperties<TsTestValue.TsString, TsTestValue.TsString, TsTestValue.TsNumber>(
+                    method = method,
+                    *results.map { expectedNumber ->
+                        {
+                                left: TsTestValue.TsString,
+                                right: TsTestValue.TsString,
+                                result: TsTestValue.TsNumber,
+                            ->
+                            result.number == expectedNumber.toDouble() &&
+                                result.number == expectedResult(listOf(left.value, right.value)).toDouble()
+                        }
+                    }.toTypedArray(),
+                    invariants = arrayOf({ left, right, result ->
+                        result.number == expectedResult(listOf(left.value, right.value)).toDouble()
+                    }),
+                )
+            } else {
+                discoverProperties<TsTestValue.TsString, TsTestValue.TsNumber>(
+                    method = method,
+                    { input, result -> result.number == 1.0 && expectedResult(listOf(input.value)) == 1 },
+                    { input, result -> result.number == 2.0 && expectedResult(listOf(input.value)) == 2 },
+                    invariants = arrayOf({ input, result ->
+                        result.number == expectedResult(listOf(input.value)).toDouble()
+                    }),
+                )
+            }
+        }
+
+        val tests = expected.mapValues { (name, _) -> analyze(name) }
+
+        tests.forEach { (name, generated) ->
+            val expectedResults = if (name == "equalsAtLengthOne") setOf(1, 2, 3) else setOf(1, 2)
+            assertEquals(expectedResults, generated.map { resultNumber(it) }.toSet(), name)
+            generated.forEach { test ->
+                val inputs = test.before.parameters.map { assertIs<TsTestValue.TsString>(it).value }
+                assertEquals(expected.getValue(name)(inputs), resultNumber(test), "$name: $test")
+            }
+        }
+
+        replay(tests)
+    }
+
+    @Test
+    fun `null and undefined strict and loose equality remain distinct`() {
+        discoverProperties<TsTestValue.TsNumber>(
+            method = getMethod(methodName = "nullAndUndefined", className = "StringEquality"),
+            { result -> result.number == 2.0 },
+            invariants = arrayOf({ result -> result.number == 2.0 }),
+        )
+
+        val tests = mapOf("nullAndUndefined" to analyze("nullAndUndefined"))
+
+        assertEquals(setOf(2), tests.getValue("nullAndUndefined").map(::resultNumber).toSet())
+
+        replay(tests)
+    }
+
+    @Test
+    fun `default string bound can compare two symbolic inputs`() {
+        discoverProperties<TsTestValue.TsString, TsTestValue.TsString, TsTestValue.TsNumber>(
+            method = getMethod(methodName = "equalsOther", className = "StringEquality"),
+            { left, right, result -> left.value == right.value && result.number == 1.0 },
+            { left, right, result -> left.value != right.value && result.number == 2.0 },
+        )
+
+        val tests = analyze("equalsOther", maxStringLength = 1_000)
+
+        assertEquals(setOf(1, 2), tests.map(::resultNumber).toSet())
+
+        replay(mapOf("equalsOther" to tests))
+    }
+
+    @Test
+    fun `any and unknown string alternatives are explicit unsupported paths`() {
+        val generated = listOf("equalsAnyStrings", "equalsUnknownStrings").associateWith { name ->
+            val method = scene.projectClasses.single { it.name == "StringEquality" }
+                .methods
+                .single { it.name == name }
+            val analysis = TsMachine(
+                scene,
+                options = analysisOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL),
+                tsOptions = TsOptions(maxArraySize = 4),
+            ).use { machine ->
+                machine.analyzeWithOutcome(listOf(method))
+            }
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name)
+            assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }, name)
+            val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) }
+            assertTrue(tests.isNotEmpty(), name)
+            assertTrue(tests.all { resultNumber(it) == 3 }, "$name: $tests")
+
+            tests
+        }
+
+        replayDynamic(generated)
+        replayLongMismatch()
+
+        val method = scene.projectClasses.single { it.name == "StringEquality" }
+            .methods
+            .single { it.name == "equalsAnyStrings" }
+        val ordinaryStates = TsMachine(
+            scene,
+            options = analysisOptions,
+            tsOptions = TsOptions(maxArraySize = 4),
+        ).use { machine ->
+            machine.analyze(listOf(method))
+        }
+        val ordinaryTests = ordinaryStates.map { state -> TsTestResolver().resolve(method, state) }
+        assertTrue(ordinaryTests.none { resultNumber(it) in setOf(1, 2) })
+    }
+
+    @Test
+    fun `two unmodeled string references do not yield equality witnesses`() {
+        val method = scene.projectClasses.single { it.name == "StringEquality" }
+            .methods
+            .single { it.name == "looselyEqualsDynamicStrings" }
+        val analysis = TsMachine(
+            scene,
+            options = analysisOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL),
+            tsOptions = TsOptions(maxArraySize = 4),
+        ).use { machine ->
+            machine.analyzeWithOutcome(listOf(method))
+        }
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason)
+        assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it })
+        val unsupportedWitnesses = mutableListOf<TsUnsupportedWitnessException>()
+        val tests = analysis.states.mapNotNull { state ->
+            try {
+                TsTestResolver().resolve(method, state)
+            } catch (failure: TsUnsupportedWitnessException) {
+                unsupportedWitnesses += failure
+                null
+            }
+        }
+
+        assertTrue(unsupportedWitnesses.isNotEmpty(), "Expected an unbacked string witness")
+        assertTrue(unsupportedWitnesses.all { "missing backing array" in it.message.orEmpty() })
+        assertTrue(tests.none { resultNumber(it) in setOf(1, 2) }, "$tests")
+    }
+
+    @Test
+    fun `unsupported fork does not consume covered-new slot or stop before supported result`() {
+        val method = scene.projectClasses.single { it.name == "StringEquality" }
+            .methods
+            .single { it.name == "equalsAnyDirect" }
+        val analysis = TsMachine(
+            scene,
+            options = analysisOptions.copy(collectedStatesLimit = 1),
+            tsOptions = TsOptions(maxArraySize = 4),
+        ).use { machine ->
+            machine.analyzeWithOutcome(listOf(method))
+        }
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason)
+        assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it })
+        val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) }
+        val supported = tests.filter { test ->
+            test.before.parameters[0] !is TsTestValue.TsString && resultNumber(test) == 2
+        }
+        assertTrue(supported.isNotEmpty(), "$tests")
+
+        replayDynamic(mapOf("equalsAnyDirect" to supported))
+    }
+
+    private fun analyze(name: String, maxStringLength: Int = 4): List<TsTest> {
+        val method = scene.projectClasses.single { it.name == "StringEquality" }
+            .methods
+            .single { it.name == name }
+        val analysis = TsMachine(
+            scene,
+            options = analysisOptions,
+            tsOptions = TsOptions(maxArraySize = maxStringLength),
+        ).use { machine ->
+            machine.analyzeWithOutcome(listOf(method))
+        }
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name)
+        assertTrue(analysis.states.isNotEmpty(), name)
+        assertTrue(analysis.states.all { it.methodResult is TsMethodResult.Success }, name)
+
+        return analysis.states.map { state -> TsTestResolver().resolve(method, state) }
+    }
+
+    private fun resultNumber(test: TsTest): Int =
+        assertIs<TsTestValue.TsNumber>(test.returnValue).number.toInt()
+
+    private fun replay(tests: Map<String, List<TsTest>>) {
+        val script = buildString {
+            appendLine(source.readText())
+            tests.forEach { (name, generated) ->
+                generated.forEachIndexed { index, test ->
+                    val args = test.before.parameters.joinToString { value ->
+                        jsString(assertIs<TsTestValue.TsString>(value).value)
+                    }
+                    val expected = resultNumber(test)
+
+                    appendLine("if (new StringEquality().$name($args) !== $expected) {")
+                    appendLine("  throw Error('$name witness $index');")
+                    appendLine("}")
+                }
+            }
+        }
+
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "string-equality",
+            timeoutMessage = "Node replay timed out",
+        )
+    }
+
+    private fun replayDynamic(tests: Map<String, List<TsTest>>) {
+        val script = buildString {
+            appendLine(source.readText())
+            tests.forEach { (name, generated) ->
+                generated.forEachIndexed { index, test ->
+                    val left = jsDynamic(test.before.parameters[0])
+                    val right = jsString(assertIs<TsTestValue.TsString>(test.before.parameters[1]).value)
+
+                    appendLine("if (new StringEquality().$name($left, $right) !== ${resultNumber(test)}) {")
+                    appendLine("  throw Error('$name witness $index');")
+                    appendLine("}")
+                }
+            }
+        }
+
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "dynamic-string-equality",
+            timeoutMessage = "Node replay timed out",
+        )
+    }
+
+    private fun jsDynamic(value: TsTestValue): String = when (value) {
+        is TsTestValue.TsBoolean -> value.value.toString()
+        is TsTestValue.TsNumber -> value.number.toString()
+        TsTestValue.TsNull -> "null"
+        TsTestValue.TsUndefined -> "undefined"
+        is TsTestValue.TsClass -> "{}"
+        is TsTestValue.TsArray<*> -> "[]"
+        else -> error("Unexpected string alternative: $value")
+    }
+
+    private fun replayLongMismatch() {
+        val script = buildString {
+            appendLine(source.readText())
+            appendLine("const left = 'a'.repeat(4) + 'x';")
+            appendLine("const right = 'a'.repeat(4) + 'y';")
+            appendLine("if (new StringEquality().equalsAnyStrings(left, right) !== 2) throw Error('long any');")
+            appendLine("if (new StringEquality().equalsUnknownStrings(left, right) !== 2) throw Error('long unknown');")
+        }
+
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "long-string-equality",
+            timeoutMessage = "Node replay timed out",
+        )
+    }
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt
new file mode 100644
index 0000000000..f214fb0e7d
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt
@@ -0,0 +1,268 @@
+package org.usvm.machine
+
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsTestResolver
+import org.usvm.util.TsUnsupportedWitnessException
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import org.usvm.util.jsString
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+import kotlin.test.assertTrue
+import kotlin.time.Duration
+
+private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000
+
+class TsSymbolicStringInputTest {
+    @TempDir
+    lateinit var directory: Path
+
+    private val machineOptions = UMachineOptions(
+        pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+        solverType = SolverType.YICES,
+        solverTimeout = Duration.INFINITE,
+        typeOperationsTimeout = Duration.INFINITE,
+    )
+
+    @Test
+    fun `symbolic string witnesses replay including empty and nonempty values`() {
+        val source = getResourcePath("/models/SymbolicStringInput.ts")
+        val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)))
+        val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods
+            .filter { it.name in setOf("identity", "lengthOne", "literal", "literalLength") }
+            .associateBy { it.name }
+        val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine ->
+            methods.mapValues { (_, method) ->
+                machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) }
+            }
+        }
+
+        val identityTests = tests.getValue("identity")
+        assertTrue(identityTests.isNotEmpty())
+        identityTests.forEach { test ->
+            val input = assertIs<TsTestValue.TsString>(test.before.parameters.single()).value
+            val result = assertIs<TsTestValue.TsString>(test.returnValue).value
+            assertEquals(input, result, message = test.toString())
+        }
+
+        val lengthTests = tests.getValue("lengthOne")
+        assertEquals(
+            setOf(0.0, 1.0),
+            lengthTests.map { test ->
+                assertIs<TsTestValue.TsNumber>(test.returnValue).number
+            }.toSet()
+        )
+        assertTrue(
+            lengthTests.any { test ->
+                assertIs<TsTestValue.TsString>(test.before.parameters.single()).value.isEmpty()
+            }
+        )
+        assertTrue(
+            lengthTests.any { test ->
+                assertIs<TsTestValue.TsString>(test.before.parameters.single()).value.isNotEmpty()
+            }
+        )
+
+        val literalTests = tests.getValue("literal")
+        assertTrue(literalTests.isNotEmpty())
+        literalTests.forEach { test ->
+            assertEquals("A\u0000\u03a9\uD83D\uDE00", assertIs<TsTestValue.TsString>(test.returnValue).value)
+        }
+
+        val literalLengthTests = tests.getValue("literalLength")
+        assertTrue(literalLengthTests.isNotEmpty())
+        literalLengthTests.forEach { test ->
+            assertEquals(5.0, assertIs<TsTestValue.TsNumber>(test.returnValue).number)
+        }
+
+        val script = buildString {
+            appendLine(source.readText())
+            tests.forEach { (name, generated) ->
+                generated.forEachIndexed { index, test ->
+                    val args = test.before.parameters.joinToString { value ->
+                        jsString(assertIs<TsTestValue.TsString>(value).value)
+                    }
+                    val expected = when (val result = test.returnValue) {
+                        is TsTestValue.TsString -> jsString(result.value)
+                        is TsTestValue.TsNumber -> result.number.toString()
+                        else -> error("Unexpected result for $name: $result")
+                    }
+
+                    appendLine("if (new SymbolicStringInput().$name($args) !== $expected) {")
+                    appendLine("  throw Error('$name witness $index');")
+                    appendLine("}")
+                }
+            }
+        }
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "basic-strings",
+            timeoutMessage = "basic-strings replay timed out",
+            failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT),
+        )
+    }
+
+    @Test
+    fun `string backing cannot alias an input number array`() {
+        val source = getResourcePath("/models/SymbolicStringInput.ts")
+        val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)))
+        val method = scene.projectClasses.single { it.name == "SymbolicStringInput" }
+            .methods
+            .single { it.name == "independentArrayLength" }
+
+        val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine ->
+            machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) }
+        }
+
+        assertTrue(tests.isNotEmpty())
+        assertEquals(
+            setOf(0.0, 2.0),
+            tests.map { test ->
+                assertIs<TsTestValue.TsNumber>(test.returnValue).number
+            }.toSet()
+        )
+
+        val script = buildString {
+            appendLine(source.readText())
+            tests.forEachIndexed { index, test ->
+                val input = assertIs<TsTestValue.TsString>(test.before.parameters[0]).value
+                val array = assertIs<TsTestValue.TsArray<*>>(test.before.parameters[1])
+                val elements = array.values.joinToString { value ->
+                    assertIs<TsTestValue.TsNumber>(value).number.toString()
+                }
+                val expected = assertIs<TsTestValue.TsNumber>(test.returnValue).number
+                val encodedInput = jsString(input)
+
+                appendLine(
+                    "if (new SymbolicStringInput().independentArrayLength($encodedInput, [$elements]) !== $expected) {"
+                )
+                appendLine("  throw Error('array alias witness $index');")
+                appendLine("}")
+            }
+        }
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "array-isolation",
+            timeoutMessage = "array-isolation replay timed out",
+            failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT),
+        )
+    }
+
+    @Test
+    fun `configured string bound is shared with concrete test extraction`() {
+        val source = getResourcePath("/models/SymbolicStringInput.ts")
+        val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)))
+        val method = scene.projectClasses.single { it.name == "SymbolicStringInput" }
+            .methods
+            .single { it.name == "lengthIs10001" }
+        val maxStringLength = 10_001
+
+        val tests = TsMachine(
+            scene,
+            options = machineOptions,
+            tsOptions = TsOptions(maxArraySize = maxStringLength),
+        ).use { machine ->
+            machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) }
+        }
+
+        assertEquals(
+            setOf(0.0, 1.0),
+            tests.map { test ->
+                assertIs<TsTestValue.TsNumber>(test.returnValue).number
+            }.toSet()
+        )
+        val longWitness = tests.single { test ->
+            assertIs<TsTestValue.TsNumber>(test.returnValue).number == 1.0
+        }
+        assertEquals(
+            maxStringLength,
+            assertIs<TsTestValue.TsString>(longWitness.before.parameters.single()).value.length
+        )
+
+        val script = buildString {
+            appendLine(source.readText())
+            tests.forEachIndexed { index, test ->
+                val input = assertIs<TsTestValue.TsString>(test.before.parameters.single()).value
+                val expected = assertIs<TsTestValue.TsNumber>(test.returnValue).number
+
+                appendLine("if (new SymbolicStringInput().lengthIs10001(${jsString(input)}) !== $expected) {")
+                appendLine("  throw Error('string bound witness $index');")
+                appendLine("}")
+            }
+        }
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "string-bound",
+            timeoutMessage = "string-bound replay timed out",
+            failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT),
+        )
+    }
+
+    @Test
+    fun `string inferred from any without backing cannot become an empty witness`() {
+        val source = getResourcePath("/models/SymbolicStringInput.ts")
+        val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND)))
+        val method = scene.projectClasses.single { it.name == "SymbolicStringInput" }
+            .methods
+            .single { it.name == "anyStringLength" }
+
+        val states = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine ->
+            machine.analyze(listOf(method))
+        }
+
+        assertTrue(states.isNotEmpty())
+        val resolutions = states.map { state -> runCatching { TsTestResolver().resolve(method, state) } }
+        val unsupported = resolutions.mapNotNull { it.exceptionOrNull() }
+        assertTrue(
+            unsupported.isNotEmpty(),
+            "Expected an unbacked symbolic string: $resolutions",
+        )
+        unsupported.forEach { failure ->
+            assertIs<TsUnsupportedWitnessException>(failure)
+            assertTrue("missing backing array" in failure.message.orEmpty(), failure.toString())
+        }
+
+        val supported = resolutions.mapNotNull { it.getOrNull() }
+        assertTrue(supported.isNotEmpty())
+        val script = buildString {
+            appendLine(source.readText())
+            appendLine("if (new SymbolicStringInput().anyStringLength(\"\") !== 2) throw Error('empty string');")
+            appendLine("if (new SymbolicStringInput().anyStringLength(\"x\") !== 1) throw Error('one-char string');")
+            supported.forEachIndexed { index, test ->
+                val input = when (val value = test.before.parameters.single()) {
+                    TsTestValue.TsUndefined -> "undefined"
+                    TsTestValue.TsNull -> "null"
+                    is TsTestValue.TsBoolean -> value.value.toString()
+                    is TsTestValue.TsNumber -> value.number.toString()
+                    is TsTestValue.TsString -> jsString(value.value)
+                    else -> error("Unexpected input for anyStringLength: $value")
+                }
+                val expected = assertIs<TsTestValue.TsNumber>(test.returnValue).number
+
+                appendLine("if (new SymbolicStringInput().anyStringLength($input) !== $expected) {")
+                appendLine("  throw Error('any string witness $index');")
+                appendLine("}")
+            }
+        }
+
+        assertNodeReplay(
+            source = script,
+            directory = directory,
+            name = "any-string",
+            timeoutMessage = "any-string replay timed out",
+        )
+    }
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt
index 2a844e606d..793a1d98ff 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt
@@ -14,9 +14,9 @@ import org.usvm.api.TsTestValue
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.jsString
 import java.nio.file.Path
-import java.util.concurrent.TimeUnit
-import kotlin.io.path.readText
 import kotlin.io.path.writeText
 import kotlin.test.assertEquals
 import kotlin.test.assertIs
@@ -64,7 +64,12 @@ class TsArrayShiftReplayTest {
                         appendLine("}")
                     }
                 }
-                assertReplay(script, index)
+                assertNodeReplay(
+                    source = script,
+                    directory = directory,
+                    name = "replay$index",
+                    timeoutMessage = "Replay timed out",
+                )
             }
         }
     }
@@ -436,29 +441,6 @@ class TsArrayShiftReplayTest {
         else -> error("Unsupported replay value: $value")
     }
 
-    private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString(
-        separator = "",
-        prefix = "\"",
-        postfix = "\"",
-    )
-
-    private fun assertReplay(source: String, index: Int) {
-        val script = directory.resolve("replay$index.ts")
-        val output = directory.resolve("replay$index.out")
-        script.writeText(source)
-        val process = ProcessBuilder("node", "--experimental-strip-types", script.toString())
-            .redirectErrorStream(true)
-            .redirectOutput(output.toFile())
-            .start()
-
-        try {
-            assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Replay timed out")
-            assertEquals(0, process.exitValue(), "${output.readText()}\n$source")
-        } finally {
-            if (process.isAlive) process.destroyForcibly()
-        }
-    }
-
     private data class ReplayCase(
         val name: String,
         val parameters: String,
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt
index a38ba9b3fe..72293e5b07 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt
@@ -15,11 +15,11 @@ import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
 import org.usvm.util.getResourcePath
+import org.usvm.util.jsString
 import java.nio.file.Path
-import java.util.concurrent.TimeUnit
 import kotlin.io.path.readText
-import kotlin.io.path.writeText
 import kotlin.test.assertEquals
 import kotlin.test.assertIs
 import kotlin.test.assertTrue
@@ -81,7 +81,12 @@ class TsInstanceCallReceiverTest {
                         appendLine("}")
                     }
                 }
-                assertReplay(replay, case.method)
+                assertNodeReplay(
+                    source = replay,
+                    directory = directory,
+                    name = case.method,
+                    timeoutMessage = "Receiver replay timed out",
+                )
             }
         }
     }
@@ -98,29 +103,6 @@ class TsInstanceCallReceiverTest {
         else -> error("Unsupported receiver input: $value")
     }
 
-    private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString(
-        separator = "",
-        prefix = "\"",
-        postfix = "\"",
-    )
-
-    private fun assertReplay(source: String, name: String) {
-        val script = directory.resolve("$name.ts")
-        val output = directory.resolve("$name.out")
-        script.writeText(source)
-        val process = ProcessBuilder("node", "--experimental-strip-types", script.toString())
-            .redirectErrorStream(true)
-            .redirectOutput(output.toFile())
-            .start()
-
-        try {
-            assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Receiver replay timed out")
-            assertEquals(0, process.exitValue(), "${output.readText()}\n$source")
-        } finally {
-            if (process.isAlive) process.destroyForcibly()
-        }
-    }
-
     private data class Case(
         val method: String,
         val results: Set<Double>,
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt
index 4abb82bb0b..083104b732 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt
@@ -28,6 +28,7 @@ import org.usvm.UMachineOptions
 import org.usvm.api.targets.ReachabilityObserver
 import org.usvm.api.targets.TsReachabilityTarget
 import org.usvm.isTrue
+import org.usvm.machine.TsAnalysisStopReason
 import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
@@ -52,6 +53,38 @@ class TsUnknownCallDispatcherTest {
     )
     private val fullScene = EtsScene(listOf(sourceFile))
 
+    @Test
+    fun `unsupported model exception is reported without a successful state`() {
+        val method = method(fullScene, "declaredMethodWithoutBodyContinues")
+        val dispatcher = TsUnknownCallDispatcher { _, _ ->
+            throw UnsupportedOperationException("The call model is not implemented")
+        }
+
+        val outcome = TsMachine(
+            scene = fullScene,
+            options = allStatesMachineOptions,
+            tsOptions = TsOptions(),
+            unknownCallDispatcher = dispatcher,
+        ).use { machine ->
+            machine.analyzeWithOutcome(methods = listOf(method))
+        }
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.states.isEmpty())
+        assertEquals(listOf("The call model is not implemented"), outcome.unsupportedPaths)
+
+        assertFailsWith<UnsupportedOperationException> {
+            TsMachine(
+                scene = fullScene,
+                options = allStatesMachineOptions.copy(throwExceptionOnStepFailure = true),
+                tsOptions = TsOptions(),
+                unknownCallDispatcher = dispatcher,
+            ).use { machine ->
+                machine.analyzeWithOutcome(methods = listOf(method))
+            }
+        }
+    }
+
     @Test
     fun `every model or fallback decision is reported through the interpreter observer`() {
         val cases = listOf(
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt
new file mode 100644
index 0000000000..b02a29d870
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt
@@ -0,0 +1,583 @@
+package org.usvm.samples.types
+
+import org.jacodb.ets.model.EtsScene
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.StateCollectionStrategy
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTestValue
+import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.machine.TsAnalysisStopReason
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+import kotlin.test.assertTrue
+import kotlin.time.Duration.Companion.seconds
+
+class RuntimeInstanceofTest : TsMethodTestRunner() {
+    @TempDir
+    lateinit var directory: Path
+
+    private val tsPath = "/samples/types/RuntimeInstanceof.ts"
+
+    override val scene: EtsScene = loadScene(tsPath)
+
+    @Test
+    fun `dynamic constructor value selects both outcomes`() {
+        val method = getMethod(methodName = "dynamicConstructor", className = "RuntimeInstanceof")
+
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { input, result -> input.value && result.number == 1.0 },
+            { input, result -> !input.value && result.number == 0.0 },
+            invariants = arrayOf({ input, result -> result.number == (if (input.value) 1.0 else 0.0) }),
+        )
+
+        val outcome = analyze("dynamicConstructor")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}")
+        val cases = outcome.states.map { state ->
+            assertIs<TsMethodResult.Success>(state.methodResult)
+            val test = TsTestResolver().resolve(method, state)
+            val input = assertIs<TsTestValue.TsBoolean>(test.before.parameters.single()).value
+            val actual = assertIs<TsTestValue.TsNumber>(test.returnValue).number
+            assertEquals(if (input) 1.0 else 0.0, actual)
+            input to actual
+        }
+        assertEquals(setOf(false, true), cases.map { it.first }.toSet())
+
+        replay(cases.map { (input, actual) ->
+            "if (new RuntimeInstanceof().dynamicConstructor($input) !== ${actual.toInt()}) throw Error('dynamic $input');"
+        })
+    }
+
+    @Test
+    fun `returned class value keeps constructor identity`() {
+        val method = getMethod(methodName = "returnedConstructor", className = "RuntimeInstanceof")
+
+        discoverConstant("returnedConstructor", expected = 1.0)
+
+        val outcome = analyze("returnedConstructor")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}")
+        assertTrue(outcome.states.isNotEmpty())
+        outcome.states.forEach { state ->
+            assertIs<TsMethodResult.Success>(state.methodResult)
+            val test = TsTestResolver().resolve(method, state)
+            assertEquals(1.0, assertIs<TsTestValue.TsNumber>(test.returnValue).number)
+        }
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().returnedConstructor() !== 1) throw Error('returned constructor');"
+        ))
+    }
+
+    @Test
+    fun `typeof recognizes constructor values stored in a local`() {
+        val method = getMethod(methodName = "aliasedClassTypeof", className = "RuntimeInstanceof")
+
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { input, result -> input.value && result.number == 1.0 },
+            { input, result -> !input.value && result.number == 1.0 },
+            invariants = arrayOf({ _, result -> result.number == 1.0 }),
+        )
+
+        val outcome = analyze("aliasedClassTypeof")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}")
+        val inputs = outcome.states.map { state ->
+            assertIs<TsMethodResult.Success>(state.methodResult)
+            val test = TsTestResolver().resolve(method, state)
+            assertEquals(1.0, assertIs<TsTestValue.TsNumber>(test.returnValue).number)
+            assertIs<TsTestValue.TsBoolean>(test.before.parameters.single()).value
+        }
+        assertEquals(setOf(false, true), inputs.toSet())
+
+        replay(inputs.map { input ->
+            "if (new RuntimeInstanceof().aliasedClassTypeof($input) !== 1) throw Error('typeof $input');"
+        })
+    }
+
+    @Test
+    fun `direct and inherited checks use declared class identity`() {
+        val expected = mapOf(
+            "directConstructor" to 1.0,
+            "castConstructor" to 1.0,
+            "nonNullConstructor" to 1.0,
+            "anyConstructor" to 1.0,
+            "unknownConstructor" to 1.0,
+            "objectConstructor" to 1.0,
+            "unrelatedConstructor" to 0.0,
+            "classTypeof" to 1.0,
+            "primitiveLeft" to 0.0,
+        )
+
+        expected.forEach { (methodName, expectedResult) ->
+            val method = getMethod(methodName = methodName, className = "RuntimeInstanceof")
+
+            discoverConstant(methodName, expected = expectedResult)
+
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}")
+            assertTrue(outcome.states.isNotEmpty(), "$methodName: ${outcome.unsupportedPaths}")
+            outcome.states.forEach { state ->
+                assertIs<TsMethodResult.Success>(state.methodResult, methodName)
+                val test = TsTestResolver().resolve(method, state)
+                assertEquals(expectedResult, assertIs<TsTestValue.TsNumber>(test.returnValue).number, methodName)
+            }
+        }
+
+        replay(expected.map { (methodName, expectedResult) ->
+            "if (new RuntimeInstanceof().$methodName() !== ${expectedResult.toInt()}) throw Error('$methodName');"
+        })
+    }
+
+    @Test
+    fun `nullish left operands are not class instances`() {
+        val methods = listOf("undefinedLeft", "nullLeft")
+
+        methods.forEach { methodName ->
+            val method = getMethod(methodName = methodName, className = "RuntimeInstanceof")
+
+            discoverConstant(methodName, expected = 0.0)
+
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}")
+            assertTrue(outcome.states.isNotEmpty(), methodName)
+            outcome.states.forEach { state ->
+                assertIs<TsMethodResult.Success>(state.methodResult)
+                val test = TsTestResolver().resolve(method, state)
+                assertEquals(0.0, assertIs<TsTestValue.TsNumber>(test.returnValue).number, methodName)
+            }
+        }
+
+        replay(methods.map { methodName ->
+            "if (new RuntimeInstanceof().$methodName() !== 0) throw Error('$methodName');"
+        })
+    }
+
+    @Test
+    fun `any receiver can contain an instance of the checked class`() {
+        val method = getMethod(methodName = "anyLeft", className = "RuntimeInstanceof")
+
+        discoverProperties<TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { _, result -> result.number == 0.0 },
+            { _, result -> result.number == 1.0 },
+            invariants = arrayOf({ _, result -> result.number == 0.0 || result.number == 1.0 }),
+        )
+
+        val outcome = analyze("anyLeft")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}")
+        val cases = outcome.states.map { state ->
+            assertIs<TsMethodResult.Success>(state.methodResult)
+            val test = TsTestResolver().resolve(method, state)
+            val input = test.before.parameters.single()
+            val actual = assertIs<TsTestValue.TsNumber>(test.returnValue).number
+            input to actual
+        }
+        assertEquals(setOf(0.0, 1.0), cases.map { it.second }.toSet(), "$cases")
+
+        val generatedAssertions = cases.mapIndexed { index, (input, actual) ->
+            val argument = when (input) {
+                is TsTestValue.TsClass -> "new ${input.name}()"
+                is TsTestValue.TsBoolean -> input.value.toString()
+                is TsTestValue.TsNumber -> input.number.toString()
+                TsTestValue.TsNull -> "null"
+                TsTestValue.TsUndefined -> "undefined"
+                else -> error("Cannot replay generated instanceof input: $input")
+            }
+
+            "if (new RuntimeInstanceof().anyLeft($argument) !== ${actual.toInt()}) " +
+                "throw Error('generated instanceof case $index');"
+        }
+        replay(generatedAssertions + listOf(
+            "if (new RuntimeInstanceof().anyLeft(new InstanceA()) !== 1) throw Error('A instance');",
+            "if (new RuntimeInstanceof().anyLeft(new InstanceB()) !== 0) throw Error('B instance');",
+            "if (new RuntimeInstanceof().anyLeft(42) !== 0) throw Error('primitive');",
+        ))
+    }
+
+    @Test
+    fun `class constructor values are not instances of project classes`() {
+        val methods = listOf("constructorLeft", "constructorAliasLeft", "anyConstructorLeft")
+
+        methods.forEach { methodName ->
+            val method = getMethod(methodName = methodName, className = "RuntimeInstanceof")
+            if (methodName == "constructorAliasLeft") {
+                discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+                    method = method,
+                    { input, result -> input.value && result.number == 0.0 },
+                    { input, result -> !input.value && result.number == 0.0 },
+                    invariants = arrayOf({ _, result -> result.number == 0.0 }),
+                )
+            } else {
+                discoverConstant(methodName, expected = 0.0)
+            }
+
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}")
+            assertTrue(outcome.states.isNotEmpty(), methodName)
+
+            val tests = outcome.states.map { state ->
+                assertIs<TsMethodResult.Success>(state.methodResult, methodName)
+                val test = TsTestResolver().resolve(method, state)
+                assertEquals(0.0, assertIs<TsTestValue.TsNumber>(test.returnValue).number, methodName)
+                test
+            }
+
+            if (methodName == "constructorAliasLeft") {
+                val inputs = tests.map { test ->
+                    assertIs<TsTestValue.TsBoolean>(test.before.parameters.single()).value
+                }
+                assertEquals(setOf(false, true), inputs.toSet())
+            }
+        }
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().constructorLeft() !== 0) throw Error('direct ctor LHS');",
+            "if (new RuntimeInstanceof().constructorAliasLeft(true) !== 0) throw Error('A ctor LHS');",
+            "if (new RuntimeInstanceof().constructorAliasLeft(false) !== 0) throw Error('B ctor LHS');",
+            "if (new RuntimeInstanceof().anyConstructorLeft() !== 0) throw Error('any ctor LHS');",
+        ))
+    }
+
+    @Test
+    fun `subclass instance belongs to declared parent constructor`() {
+        val method = getMethod(methodName = "inheritedConstructor", className = "RuntimeInstanceof")
+
+        discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
+            method = method,
+            { _, result -> result.number == 1.0 },
+            invariants = arrayOf({ _, result -> result.number == 1.0 }),
+        )
+
+        val outcome = analyze("inheritedConstructor")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}")
+        assertTrue(outcome.states.isNotEmpty())
+        outcome.states.forEach { state ->
+            assertIs<TsMethodResult.Success>(state.methodResult)
+            val test = TsTestResolver().resolve(method, state)
+            assertEquals(1.0, assertIs<TsTestValue.TsNumber>(test.returnValue).number)
+        }
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().inheritedConstructor(new InstanceChild()) !== 1) throw Error('parent');"
+        ))
+    }
+
+    @Test
+    fun `non callable RHS throws a TypeError object`() {
+        val methods = listOf(
+            "nonCallableRight",
+            "booleanRight",
+            "stringRight",
+            "nullRight",
+            "undefinedRight",
+            "objectRight",
+            "classInstanceRight",
+        )
+
+        methods.forEach { methodName ->
+            val method = getMethod(methodName = methodName, className = "RuntimeInstanceof")
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}")
+            assertTrue(outcome.states.isNotEmpty(), methodName)
+            outcome.states.forEach { state ->
+                val exception = assertIs<TsMethodResult.TsException>(state.methodResult)
+                assertEquals("TypeError", exception.type.typeName)
+                assertTrue(isAllocatedConcreteHeapRef(exception.value))
+
+                val test = TsTestResolver().resolve(method, state)
+                val objectException = assertIs<TsTestValue.TsException.ObjectException>(test.returnValue)
+                assertEquals("TypeError", assertIs<TsTestValue.TsClass>(objectException.value).name)
+            }
+        }
+
+        replay(methods.map { methodName ->
+            "let caught$methodName = false; try { new RuntimeInstanceof().$methodName(); } " +
+                "catch (error) { caught$methodName = error instanceof TypeError; } " +
+                "if (!caught$methodName) throw Error('$methodName TypeError');"
+        })
+    }
+
+    @Test
+    fun `custom hasInstance is explicitly unsupported`() {
+        val custom = analyze("customHasInstance")
+        val inherited = analyze("inheritedHasInstance")
+        val customField = analyze(methodName = "customHasInstanceField")
+        val inheritedField = analyze(methodName = "inheritedHasInstanceField")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, custom.stopReason)
+        assertTrue(custom.states.isEmpty())
+        assertTrue(custom.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${custom.unsupportedPaths}")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, inherited.stopReason)
+        assertTrue(inherited.states.isEmpty())
+        assertTrue(inherited.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inherited.unsupportedPaths}")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, customField.stopReason)
+        assertTrue(customField.states.isEmpty())
+        assertTrue(customField.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${customField.unsupportedPaths}")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, inheritedField.stopReason)
+        assertTrue(inheritedField.states.isEmpty())
+        assertTrue(inheritedField.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inheritedField.unsupportedPaths}")
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().customHasInstance() !== false) throw Error('custom hasInstance');",
+            "if (new RuntimeInstanceof().inheritedHasInstance(new InstanceHasInstanceChild()) !== false) " +
+                "throw Error('inherited hasInstance');",
+            "if (new RuntimeInstanceof().customHasInstanceField() !== false) " +
+                "throw Error('field hasInstance');",
+            "if (new RuntimeInstanceof().inheritedHasInstanceField(new InstanceHasInstanceFieldChild()) !== false) " +
+                "throw Error('inherited field hasInstance');",
+        ))
+    }
+
+    @Test
+    fun `symbolic RHS stays explicitly unsupported until callability is modeled`() {
+        val outcome = analyze("unresolvedRight")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.states.isEmpty())
+        assertTrue(outcome.unsupportedPaths.any { "Unresolved instanceof RHS callability" in it },
+            "${outcome.unsupportedPaths}")
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().unresolvedRight(InstanceA) !== true) throw Error('callable RHS');",
+            "let threwTypeError = false; try { new RuntimeInstanceof().unresolvedRight(42); } " +
+                "catch (error) { threwTypeError = error instanceof TypeError; } " +
+                "if (!threwTypeError) throw Error('non-callable RHS');",
+        ))
+    }
+
+    @Test
+    fun `constructor typed input has an explicit unsupported outcome`() {
+        val outcome = analyze("constructorParameter")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.states.isEmpty())
+        assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it },
+            "${outcome.unsupportedPaths}")
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().constructorParameter(InstanceA) !== true) throw Error('A input');",
+            "if (new RuntimeInstanceof().constructorParameter(InstanceB) !== false) throw Error('B input');",
+        ))
+    }
+
+    @Test
+    fun `constructor containing input types have explicit unsupported outcomes`() {
+        val methods = listOf(
+            "constructorUnionParameter",
+            "nullableConstructorParameter",
+            "constructorAliasParameter",
+            "constructorIntersectionParameter",
+            "genericConstructorParameter",
+        )
+
+        methods.forEach { methodName ->
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}")
+            assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it },
+                "$methodName: ${outcome.unsupportedPaths}")
+        }
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().constructorUnionParameter(InstanceA) !== true) throw Error('union A');",
+            "if (new RuntimeInstanceof().constructorUnionParameter(InstanceB) !== true) throw Error('union B');",
+            "if (new RuntimeInstanceof().nullableConstructorParameter(null) !== true) throw Error('nullable null');",
+            "if (new RuntimeInstanceof().nullableConstructorParameter(InstanceA) !== true) throw Error('nullable A');",
+            "if (new RuntimeInstanceof().constructorAliasParameter(InstanceA) !== true) throw Error('alias');",
+            "if (new RuntimeInstanceof().constructorIntersectionParameter(InstanceA) !== true) throw Error('intersection');",
+            "if (new RuntimeInstanceof().genericConstructorParameter(InstanceA) !== true) throw Error('generic');",
+        ))
+    }
+
+    @Test
+    fun `constructor arrays have an explicit unsupported outcome`() {
+        val methods = listOf("constructorArrayParameter", "constructorNestedArrayParameter")
+
+        methods.forEach { methodName ->
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}")
+            assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it },
+                "$methodName: ${outcome.unsupportedPaths}")
+        }
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().constructorArrayParameter([InstanceA]) !== true) throw Error('array');",
+            "if (new RuntimeInstanceof().constructorNestedArrayParameter([[InstanceA]]) !== true) " +
+                "throw Error('nested array');",
+        ))
+    }
+
+    @Test
+    fun `constructor tuple has an explicit unsupported outcome`() {
+        val outcome = analyze("constructorTupleParameter")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.states.isEmpty())
+        assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it },
+            "${outcome.unsupportedPaths}")
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().constructorTupleParameter([InstanceA]) !== true) throw Error('tuple');"
+        ))
+    }
+
+    @Test
+    fun `constructor value in class type argument has an explicit unsupported outcome`() {
+        val outcome = analyze("constructorBoxParameter")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.states.isEmpty(), "${outcome.states}")
+        assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it },
+            "${outcome.unsupportedPaths}")
+
+        replay(listOf(
+            "const box = new InstanceConstructorBox(); box.value = InstanceA; " +
+                "if (new RuntimeInstanceof().constructorBoxParameter(box) !== true) throw Error('box');",
+        ))
+    }
+
+    @Test
+    fun `constructor values in object fields have explicit unsupported outcomes`() {
+        val methods = listOf(
+            "structuralConstructorParameter",
+            "recursiveConstructorParameter",
+            "inheritedConstructorParameter",
+        )
+
+        methods.forEach { methodName ->
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}")
+            assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it },
+                "$methodName: ${outcome.unsupportedPaths}")
+        }
+
+        replay(listOf(
+            "if (new RuntimeInstanceof().structuralConstructorParameter({ ctor: InstanceA }) !== true) " +
+                "throw Error('structural');",
+            "const holder = new InstanceRecursiveHolder(); holder.ctor = InstanceA; " +
+                "if (new RuntimeInstanceof().recursiveConstructorParameter(holder) !== true) throw Error('recursive');",
+            "const inherited = new InstanceInheritedHolder(); inherited.ctor = InstanceA; " +
+                "if (new RuntimeInstanceof().inheritedConstructorParameter(inherited) !== true) throw Error('inherited');",
+        ))
+    }
+
+    @Test
+    fun `inherited generic fields have explicit unsupported outcomes`() {
+        val methods = listOf("inheritedGenericConstructorParameter", "inheritedGenericNumberParameter")
+
+        methods.forEach { methodName ->
+            val outcome = analyze(methodName)
+
+            assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName)
+            assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}")
+            assertTrue(outcome.unsupportedPaths.any { "Unresolved inherited generic" in it },
+                "$methodName: ${outcome.unsupportedPaths}")
+        }
+
+        replay(listOf(
+            "const holder = new InstanceInheritedGenericConstructor(); holder.ctor = InstanceA; " +
+                "if (new RuntimeInstanceof().inheritedGenericConstructorParameter(holder) !== true) " +
+                "throw Error('inherited generic');",
+            "const numberHolder = new InstanceInheritedGenericNumber(); numberHolder.ctor = 1; " +
+                "if (new RuntimeInstanceof().inheritedGenericNumberParameter(numberHolder) !== true) " +
+                "throw Error('inherited generic number');",
+        ))
+    }
+
+    @Test
+    fun `concrete inherited number input is not excluded by the constructor guard`() {
+        val outcome = analyze("inheritedConcreteNumberParameter")
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}")
+        assertTrue(outcome.states.isNotEmpty())
+
+        replay(listOf(
+            "const holder = new InstanceInheritedConcreteNumber(); holder.value = 1; " +
+                "if (new RuntimeInstanceof().inheritedConcreteNumberParameter(holder) !== true) " +
+                "throw Error('inherited concrete number');",
+        ))
+    }
+
+    @Test
+    fun `unsupported constructor input does not hide another entrypoint`() {
+        val methods = listOf("constructorParameter", "directConstructor")
+            .map { getMethod(methodName = it, className = "RuntimeInstanceof") }
+        val outcome = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine ->
+            machine.analyzeWithOutcome(methods = methods)
+        }
+
+        assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason)
+        assertTrue(outcome.unsupportedPaths.any { "constructorParameter" in it }, "${outcome.unsupportedPaths}")
+        assertTrue(outcome.states.isNotEmpty())
+        outcome.states.forEach { state -> assertIs<TsMethodResult.Success>(state.methodResult) }
+    }
+
+    private fun discoverConstant(methodName: String, expected: Double) {
+        discoverProperties<TsTestValue.TsNumber>(
+            method = getMethod(methodName = methodName, className = "RuntimeInstanceof"),
+            { result -> result.number == expected },
+            invariants = arrayOf({ result -> result.number == expected }),
+        )
+    }
+
+    private fun analyze(methodName: String) = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine ->
+        machine.analyzeWithOutcome(methods = listOf(getMethod(methodName = methodName, className = "RuntimeInstanceof")))
+    }
+
+    private fun replay(assertions: List<String>) {
+        val source = buildString {
+            appendLine(getResourcePath(tsPath).readText())
+            assertions.forEach(::appendLine)
+        }
+
+        assertNodeReplay(
+            source = source,
+            directory = directory,
+            name = "runtime-instanceof",
+            timeoutMessage = "Node replay timed out",
+        )
+    }
+
+    private val machineOptions = UMachineOptions(
+        stateCollectionStrategy = StateCollectionStrategy.ALL,
+        stopOnCoverage = 0,
+        timeout = 30.seconds,
+    )
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/NodeReplay.kt b/usvm-ts/src/test/kotlin/org/usvm/util/NodeReplay.kt
new file mode 100644
index 0000000000..3c48906fa2
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/NodeReplay.kt
@@ -0,0 +1,40 @@
+package org.usvm.util
+
+import java.nio.file.Path
+import java.util.concurrent.TimeUnit
+import kotlin.io.path.readText
+import kotlin.io.path.writeText
+import kotlin.test.assertEquals
+import kotlin.test.assertTrue
+
+private const val NODE_REPLAY_TIMEOUT_SECONDS = 10L
+
+fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString(
+    separator = "",
+    prefix = "\"",
+    postfix = "\"",
+)
+
+fun assertNodeReplay(
+    source: String,
+    directory: Path,
+    name: String,
+    timeoutMessage: String,
+    failureContext: String = source,
+) {
+    val script = directory.resolve("$name.ts")
+    val output = directory.resolve("$name.out")
+    script.writeText(source)
+
+    val process = ProcessBuilder("node", "--experimental-strip-types", script.toString())
+        .redirectErrorStream(true)
+        .redirectOutput(output.toFile())
+        .start()
+
+    try {
+        assertTrue(process.waitFor(NODE_REPLAY_TIMEOUT_SECONDS, TimeUnit.SECONDS), timeoutMessage)
+        assertEquals(0, process.exitValue(), "${output.readText()}\n$failureContext")
+    } finally {
+        if (process.isAlive) process.destroyForcibly()
+    }
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
index 2f950432f0..ab0c7b129c 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -1,5 +1,6 @@
 package org.usvm.util
 
+import io.ksmt.expr.KBitVec16Value
 import io.ksmt.expr.KFpValue
 import io.ksmt.utils.asExpr
 import org.jacodb.ets.model.EtsArrayType
@@ -38,6 +39,7 @@ import org.usvm.collection.field.UFieldLValue
 import org.usvm.isAllocated
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.isTrue
+import org.usvm.machine.TS_TYPE_ERROR_TYPE
 import org.usvm.machine.TsContext
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.expr.extractDouble
@@ -54,6 +56,9 @@ import org.usvm.model.UModelBase
 import org.usvm.sizeSort
 import org.usvm.types.first
 
+/** A satisfying state lacks the modeled data needed to emit a concrete witness. */
+class TsUnsupportedWitnessException(message: String) : IllegalStateException(message)
+
 class TsTestResolver {
     private val resolvedLValuesToFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf()
 
@@ -63,8 +68,22 @@ class TsTestResolver {
 
         prepareForResolve(state)
 
-        val beforeMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects)
-        val afterMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects)
+        val beforeMemoryScope = MemoryScope(
+            this,
+            model,
+            memory,
+            method,
+            resolvedLValuesToFakeObjects,
+            state.maxStringLength
+        )
+        val afterMemoryScope = MemoryScope(
+            this,
+            model,
+            memory,
+            method,
+            resolvedLValuesToFakeObjects,
+            state.maxStringLength
+        )
 
         val result = when (val res = state.methodResult) {
             is TsMethodResult.NoCall -> {
@@ -125,6 +144,15 @@ class TsTestResolver {
             try {
                 // Dispatch based on the exception type, similar to string const resolution
                 when (res.type) {
+                    TS_TYPE_ERROR_TYPE -> {
+                        val concreteRef = evaluateInModel(res.value) as? UConcreteHeapRef
+                        check(concreteRef != null && isAllocatedConcreteHeapRef(concreteRef))
+
+                        TsTestValue.TsException.ObjectException(
+                            TsTestValue.TsClass(name = "TypeError", properties = emptyMap())
+                        )
+                    }
+
                     is EtsStringType -> {
                         val concreteRef = evaluateInModel(res.value) as? UConcreteHeapRef
                         if (concreteRef != null && isAllocatedConcreteHeapRef(concreteRef)) {
@@ -158,7 +186,8 @@ class TsTestResolver {
         finalStateMemory: UReadOnlyMemory<EtsType>,
         method: EtsMethod,
         resolvedLValuesToFakeObjects: List<Pair<ULValue<*, *>, UConcreteHeapRef>>,
-    ) : TsTestStateResolver(ctx, model, finalStateMemory, method, resolvedLValuesToFakeObjects) {
+        maxStringLength: Int,
+    ) : TsTestStateResolver(ctx, model, finalStateMemory, method, resolvedLValuesToFakeObjects, maxStringLength) {
         fun resolveState(): TsParametersState {
             val thisInstance = resolveThisInstance()
             val parameters = resolveParameters()
@@ -174,6 +203,7 @@ open class TsTestStateResolver(
     private val finalStateMemory: UReadOnlyMemory<EtsType>,
     val method: EtsMethod,
     val resolvedLValuesToFakeObjects: List<Pair<ULValue<*, *>, UConcreteHeapRef>>,
+    val maxStringLength: Int,
 ) {
     fun resolveLValue(
         lValue: ULValue<*, *>,
@@ -250,11 +280,7 @@ open class TsTestStateResolver(
             }
 
             is EtsStringType -> {
-                if (isAllocatedConcreteHeapRef(concreteRef)) {
-                    resolveAllocatedString(concreteRef)
-                } else {
-                    TsTestValue.TsString("String construction is not yet implemented")
-                }
+                resolveString(heapRef, concreteRef)
             }
 
             else -> error("Unexpected type: $type")
@@ -306,13 +332,36 @@ open class TsTestStateResolver(
         return TsTestValue.TsArray(values)
     }
 
-    private fun resolveAllocatedString(
-        ref: UConcreteHeapRef,
-    ): TsTestValue.TsString {
-        val value = ctx.getStringConstantValue(ref) ?: run {
-            error("String constant not found for ref: $ref")
+    private fun resolveString(
+        heapRef: UHeapRef,
+        concreteRef: UConcreteHeapRef,
+    ): TsTestValue.TsString = with(ctx) {
+        getStringConstantValue(concreteRef)?.let { return TsTestValue.TsString(it) }
+
+        // Symbolic strings have no mutable value field in the final state. Resolve
+        // their backing array from the model in both before and after snapshots.
+        val allocated = isAllocatedConcreteHeapRef(concreteRef)
+        val stringMemory = if (allocated) finalStateMemory else model
+        val stringRef = if (allocated) heapRef else concreteRef
+        val valueLValue = mkFieldLValue(addressSort, stringRef, field = "value")
+        val charsRef = evaluateInModel(stringMemory.read(valueLValue)) as UConcreteHeapRef
+        if (charsRef.address == 0) {
+            throw TsUnsupportedWitnessException("Symbolic string is missing backing array: $concreteRef")
         }
-        return TsTestValue.TsString(value)
+
+        val lengthLValue = mkStringBackingLengthLValue(charsRef)
+        val length = evaluateInModel(stringMemory.read(lengthLValue)).extractInt()
+        require(length in 0..maxStringLength) { "Unsupported symbolic string length: $length" }
+
+        val value = buildString(length) {
+            repeat(length) { index ->
+                val elementLValue = mkStringBackingElementLValue(charsRef, mkSizeExpr(index))
+                val element = evaluateInModel(stringMemory.read(elementLValue)) as KBitVec16Value
+                append(element.shortValue.toInt().toChar())
+            }
+        }
+
+        TsTestValue.TsString(value)
     }
 
     fun resolveThisInstance(): TsTestValue {
@@ -396,7 +445,7 @@ open class TsTestStateResolver(
             is EtsLiteralType -> TODO()
             EtsNullType -> TODO()
             EtsNeverType -> TODO()
-            EtsStringType -> TsTestValue.TsString("String construction is not yet implemented")
+            EtsStringType -> error("String values must be resolved from heap references")
             EtsVoidType -> TODO()
             else -> error("Unexpected type: $type")
         }
diff --git a/usvm-ts/src/test/resources/models/StringEquality.ts b/usvm-ts/src/test/resources/models/StringEquality.ts
new file mode 100644
index 0000000000..b861925d4f
--- /dev/null
+++ b/usvm-ts/src/test/resources/models/StringEquality.ts
@@ -0,0 +1,58 @@
+class StringEquality {
+    equalsA(value: string): number {
+        return value === "a" ? 1 : 2;
+    }
+
+    notEqualsA(value: string): number {
+        return value !== "a" ? 1 : 2;
+    }
+
+    equalsEmpty(value: string): number {
+        return value === "" ? 1 : 2;
+    }
+
+    equalsUnicode(value: string): number {
+        return value === "\uD83D\uDE00" ? 1 : 2;
+    }
+
+    equalsOther(left: string, right: string): number {
+        return left === right ? 1 : 2;
+    }
+
+    equalsAtLengthOne(left: string, right: string): number {
+        if (left.length !== 1 || right.length !== 1) return 3;
+
+        return left === right ? 1 : 2;
+    }
+
+    looselyEqualsOther(left: string, right: string): number {
+        return left == right ? 1 : 2;
+    }
+
+    looselyNotEqualsOther(left: string, right: string): number {
+        return left != right ? 1 : 2;
+    }
+
+    equalsAnyStrings(left: any, right: string): number {
+        if (typeof left !== "string") return 3;
+        return left === right ? 1 : 2;
+    }
+
+    equalsUnknownStrings(left: unknown, right: string): number {
+        if (typeof left !== "string") return 3;
+        return left === right ? 1 : 2;
+    }
+
+    equalsAnyDirect(left: any, right: string): number {
+        return left === right ? 1 : 2;
+    }
+
+    looselyEqualsDynamicStrings(left: any, right: any): number {
+        if (typeof left !== "string" || typeof right !== "string") return 3;
+        return left == right ? 1 : 2;
+    }
+
+    nullAndUndefined(): number {
+        return null === undefined ? 1 : null == undefined ? 2 : 3;
+    }
+}
diff --git a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts
new file mode 100644
index 0000000000..dc1d2b7710
--- /dev/null
+++ b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts
@@ -0,0 +1,36 @@
+class SymbolicStringInput {
+    identity(value: string): string {
+        return value;
+    }
+
+    lengthOne(value: string): number {
+        if (value.length === 0) return 0;
+
+        return value.length === 1 ? 1 : 0;
+    }
+
+    literal(): string {
+        return "A\u0000\u03a9\uD83D\uDE00";
+    }
+
+    literalLength(): number {
+        return "A\u0000\u03a9\uD83D\uDE00".length;
+    }
+
+    independentArrayLength(value: string, array: number[]): number {
+        if (value.length !== 1 || array.length !== 1) return 0;
+
+        array.length = 0;
+        return value.length === 0 ? 1 : 2;
+    }
+
+    lengthIs10001(value: string): number {
+        return value.length === 10001 ? 1 : 0;
+    }
+
+    anyStringLength(value: any): number {
+        if (typeof value !== "string") return 0;
+
+        return value.length === 1 ? 1 : 2;
+    }
+}
diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts
new file mode 100644
index 0000000000..aa1f335e6a
--- /dev/null
+++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts
@@ -0,0 +1,246 @@
+// @ts-nocheck
+
+class RuntimeInstanceof {
+    dynamicConstructor(useA: boolean): number {
+        const ctor = useA ? InstanceA : InstanceB;
+        return new InstanceA() instanceof ctor ? 1 : 0;
+    }
+
+    constructorValue(): typeof InstanceA {
+        return InstanceA;
+    }
+
+    returnedConstructor(): number {
+        const ctor = this.constructorValue();
+        return new InstanceA() instanceof ctor && typeof ctor === "function" ? 1 : 0;
+    }
+
+    directConstructor(): number {
+        return new InstanceA() instanceof InstanceA ? 1 : 0;
+    }
+
+    castConstructor(): number {
+        return new InstanceA() instanceof (InstanceA as typeof InstanceA) ? 1 : 0;
+    }
+
+    nonNullConstructor(): number {
+        return new InstanceA() instanceof InstanceA! ? 1 : 0;
+    }
+
+    anyConstructor(): number {
+        return new InstanceA() instanceof (InstanceA as any) ? 1 : 0;
+    }
+
+    unknownConstructor(): number {
+        return new InstanceA() instanceof (InstanceA as unknown as typeof InstanceA) ? 1 : 0;
+    }
+
+    objectConstructor(): number {
+        return new InstanceA() instanceof (InstanceA as object as typeof InstanceA) ? 1 : 0;
+    }
+
+    inheritedConstructor(instance: InstanceChild): number {
+        return instance instanceof InstanceParent ? 1 : 0;
+    }
+
+    unrelatedConstructor(): number {
+        return new InstanceA() instanceof InstanceB ? 1 : 0;
+    }
+
+    classTypeof(): number {
+        return typeof InstanceA === "function" ? 1 : 0;
+    }
+
+    aliasedClassTypeof(useA: boolean): number {
+        const ctor = useA ? InstanceA : InstanceB;
+        return typeof ctor === "function" ? 1 : 0;
+    }
+
+    primitiveLeft(): number {
+        return 42 instanceof InstanceA ? 1 : 0;
+    }
+
+    anyLeft(value: any): number {
+        return value instanceof InstanceA ? 1 : 0;
+    }
+
+    constructorLeft(): number {
+        return InstanceA instanceof InstanceA ? 1 : 0;
+    }
+
+    constructorAliasLeft(useA: boolean): number {
+        const ctor = useA ? InstanceA : InstanceB;
+        return ctor instanceof InstanceA ? 1 : 0;
+    }
+
+    anyConstructorLeft(): number {
+        const value: any = InstanceA;
+        return value instanceof InstanceA ? 1 : 0;
+    }
+
+    undefinedLeft(): number {
+        const value: any = undefined;
+        return value instanceof InstanceA ? 1 : 0;
+    }
+
+    nullLeft(): number {
+        const value: any = null;
+        return value instanceof InstanceA ? 1 : 0;
+    }
+
+    nonCallableRight(): boolean {
+        const ctor: any = 42;
+        return new InstanceA() instanceof ctor;
+    }
+
+    booleanRight(): boolean {
+        const ctor: any = true;
+        return new InstanceA() instanceof ctor;
+    }
+
+    stringRight(): boolean {
+        const ctor: any = "not a constructor";
+        return new InstanceA() instanceof ctor;
+    }
+
+    nullRight(): boolean {
+        const ctor: any = null;
+        return new InstanceA() instanceof ctor;
+    }
+
+    undefinedRight(): boolean {
+        const ctor: any = undefined;
+        return new InstanceA() instanceof ctor;
+    }
+
+    objectRight(): boolean {
+        const ctor: any = {};
+        return new InstanceA() instanceof ctor;
+    }
+
+    classInstanceRight(): boolean {
+        const ctor: any = new InstanceB();
+        return new InstanceA() instanceof ctor;
+    }
+
+    unresolvedRight(ctor: any): boolean {
+        return new InstanceA() instanceof ctor;
+    }
+
+    customHasInstance(): boolean {
+        return new InstanceCustom() instanceof InstanceCustom;
+    }
+
+    inheritedHasInstance(instance: InstanceHasInstanceChild): boolean {
+        return instance instanceof InstanceHasInstanceChild;
+    }
+
+    customHasInstanceField(): boolean {
+        return new InstanceCustomField() instanceof InstanceCustomField;
+    }
+
+    inheritedHasInstanceField(instance: InstanceHasInstanceFieldChild): boolean {
+        return instance instanceof InstanceHasInstanceFieldChild;
+    }
+
+    constructorParameter(ctor: typeof InstanceA): boolean {
+        return new InstanceA() instanceof ctor;
+    }
+
+    constructorUnionParameter(ctor: typeof InstanceA | typeof InstanceB): boolean {
+        return typeof ctor === "function";
+    }
+
+    nullableConstructorParameter(ctor: typeof InstanceA | null): boolean {
+        return ctor === null || typeof ctor === "function";
+    }
+
+    constructorAliasParameter(ctor: InstanceConstructorAlias): boolean {
+        return typeof ctor === "function";
+    }
+
+    constructorIntersectionParameter(ctor: typeof InstanceA & { marker?: number }): boolean {
+        return typeof ctor === "function";
+    }
+
+    genericConstructorParameter<T extends typeof InstanceA>(ctor: T): boolean {
+        return typeof ctor === "function";
+    }
+
+    constructorTupleParameter(ctors: [typeof InstanceA]): boolean {
+        return new InstanceA() instanceof ctors[0];
+    }
+
+    constructorArrayParameter(ctors: (typeof InstanceA)[]): boolean {
+        return ctors.length === 1 && new InstanceA() instanceof ctors[0];
+    }
+
+    constructorNestedArrayParameter(ctors: (typeof InstanceA)[][]): boolean {
+        return new InstanceA() instanceof ctors[0][0];
+    }
+
+    constructorBoxParameter(box: InstanceConstructorBox<typeof InstanceA>): boolean {
+        return typeof box.value === "function";
+    }
+
+    structuralConstructorParameter(holder: { ctor: typeof InstanceA }): boolean {
+        return typeof holder.ctor === "function";
+    }
+
+    recursiveConstructorParameter(holder: InstanceRecursiveHolder): boolean {
+        return typeof holder.ctor === "function";
+    }
+
+    inheritedConstructorParameter(holder: InstanceInheritedHolder): boolean {
+        return typeof holder.ctor === "function";
+    }
+
+    inheritedGenericConstructorParameter(holder: InstanceInheritedGenericConstructor): boolean {
+        return typeof holder.ctor === "function";
+    }
+
+    inheritedGenericNumberParameter(holder: InstanceInheritedGenericNumber): boolean {
+        return typeof holder.ctor === "number";
+    }
+
+    inheritedConcreteNumberParameter(holder: InstanceInheritedConcreteNumber): boolean {
+        return holder.value === 1;
+    }
+}
+
+type InstanceConstructorAlias = typeof InstanceA | typeof InstanceB;
+
+class InstanceA {}
+class InstanceB {}
+class InstanceConstructorBox<T> { value!: T; }
+class InstanceRecursiveHolder {
+    next?: InstanceRecursiveHolder;
+    ctor!: typeof InstanceA;
+}
+class InstanceConstructorBase { ctor!: typeof InstanceA; }
+class InstanceInheritedHolder extends InstanceConstructorBase {}
+class InstanceGenericConstructorBase<T> { ctor!: T; }
+class InstanceInheritedGenericConstructor extends InstanceGenericConstructorBase<typeof InstanceA> {}
+class InstanceInheritedGenericNumber extends InstanceGenericConstructorBase<number> {}
+class InstanceConcreteNumberBase { value!: number; }
+class InstanceInheritedConcreteNumber extends InstanceConcreteNumberBase {}
+class InstanceParent {}
+class InstanceChild extends InstanceParent { childMarker: number = 1; }
+class InstanceCustom {
+    static [Symbol.hasInstance](_value: unknown): boolean {
+        return false;
+    }
+}
+class InstanceHasInstanceParent {
+    static [Symbol.hasInstance](_value: unknown): boolean {
+        return false;
+    }
+}
+class InstanceHasInstanceChild extends InstanceHasInstanceParent { hasInstanceChildMarker: number = 1; }
+class InstanceCustomField {
+    static [Symbol.hasInstance] = (_value: unknown): boolean => false;
+}
+class InstanceHasInstanceFieldParent {
+    static [Symbol.hasInstance] = (_value: unknown): boolean => false;
+}
+class InstanceHasInstanceFieldChild extends InstanceHasInstanceFieldParent { hasInstanceFieldChildMarker: number = 1; }