diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md
new file mode 100644
index 000000000..70dbb9c4d
--- /dev/null
+++ b/usvm-ts/UNKNOWN_CALL_MODELS.md
@@ -0,0 +1,242 @@
+# TypeScript unknown-call models
+
+This document describes the semantic-model path used when the normal TypeScript interpreter cannot execute a call.
+
+## Mental model
+
+There are only three stages:
+
+1. The regular interpreter and existing compatibility approximations try to execute the call.
+2. If execution cannot continue, `TsUnknownCallModelCatalog` selects one enabled semantic model by its target.
+3. If no model handles the call or a model leaves a residual state, the configured fallback is applied.
+
+```text
+normal execution
+      |
+      | cannot execute
+      v
+enabled model with matching target? -- no --> fallback
+      |
+     yes
+      v
+model accepts these inputs? -------- no --> fallback
+      |
+     yes
+      v
+model successors + optional residual ----> residual uses fallback
+```
+
+The catalog contains model objects directly. There are no implementation-kind values, backend registrations, or
+separate descriptor and implementation IDs.
+
+## Configuration
+
+Unknown-call behavior is configured directly in `TsOptions`:
+
+```kotlin
+TsOptions(
+    enabledUnknownCallModelIds = setOf("ts.array.shift"),
+    unknownCallFallback = TsResidualCallPolicy.STOP_PATH,
+)
+```
+
+### `enabledUnknownCallModelIds`
+
+This is the only model-selection setting.
+
+| Value | Meaning |
+| --- | --- |
+| `null` | Enable every built-in model. This is the default. |
+| `emptySet()` | Disable every built-in model. |
+| `setOf("id", ...)` | Enable exactly the listed built-in model IDs. |
+
+Unknown IDs are rejected when the machine creates its immutable per-run catalog. The input set is copied at that
+point, so later mutations cannot change an active run.
+
+Use the model's `id`, for example `ts.array.shift`. A target method name, class name, source filename, or fingerprint is
+not a model ID.
+
+The built-in catalog currently contains one model:
+
+| ID | Implementation | Accepted calls |
+| --- | --- | --- |
+| `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array. |
+
+An `any`/unknown receiver, a fake-value wrapper, and a non-array receiver do not become applicable merely because the
+method is named `shift`; they use fallback. A definitely-array receiver with an unresolved element sort remains
+applicable and uses the fake-value representation described below.
+
+### `unknownCallFallback`
+
+The fallback is applied when:
+
+- no enabled model target matches the call;
+- the selected model returns `null` because it cannot safely handle the concrete inputs;
+- a model returns a satisfiable `residualGuard`.
+
+The available policies are:
+
+| Policy | Behavior |
+| --- | --- |
+| `STOP_PATH` | Prune the unsupported state. This is the default. |
+| `FRESH_SYMBOLIC_RETURN` | Continue with a fresh symbolic result and ignore unknown side effects and exceptions. |
+
+`FRESH_SYMBOLIC_RETURN` is deliberately imprecise. Use it only when opaque continuation is preferable to pruning.
+
+## Model identity and target
+
+Every model implements `TsUnknownCallModel`:
+
+```kotlin
+interface TsUnknownCallModel {
+    val id: String
+    val target: TsUnknownCallTarget
+
+    fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution?
+}
+```
+
+### Choosing an ID
+
+Use a stable semantic name:
+
+```text
+<ecosystem>.<owner-or-type>.<operation>[.<semantic-variant>]
+```
+
+Examples:
+
+- `ts.array.shift`
+- `ts.array.pop`
+- `node.buffer.copy`
+
+The ID is used for configuration, observer events, and catalog fingerprints. Do not include:
+
+- an implementation mechanism such as `intrinsic`;
+- a hash;
+- a version number;
+- a supported-domain label.
+
+Keep the same ID if an equivalent model is later reimplemented by another mechanism.
+
+### Choosing a target
+
+`TsUnknownCallTarget` matches stable call metadata declaratively:
+
+```kotlin
+TsUnknownCallTarget(
+    methodName = "shift",
+    failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION,
+)
+```
+
+Only `methodName` is required. Add `enclosingClassName` or `failureReason` when the method name alone is too broad.
+The catalog rejects overlapping enabled targets before execution, so catalog order is never a priority rule.
+
+The target identifies a call family. State-dependent checks, such as the receiver's symbolic runtime type, belong in
+`apply`.
+
+The built-in array target intentionally combines the method name with `PARTIAL_APPROXIMATION` instead of a class name.
+That failure reason is emitted only after the regular approximation path has classified the receiver as an
+`EtsArrayType`. Calls on `any`/unknown receivers reach another failure reason and cannot match this target. The model
+still validates the resolved receiver and array shape before changing memory.
+
+## Applicability and residual states
+
+There is no separate `EXACT` or `PARTIAL` flag.
+
+- `apply(...) == null` means the model rejects the complete call. The dispatcher uses fallback.
+- `residualGuard == null` means the returned execution completely handles the accepted state.
+- A non-null `residualGuard` sends precisely that symbolic subdomain to fallback.
+
+For example, a model may handle an array receiver under `isArray` and leave `!isArray` as residual:
+
+```kotlin
+TsUnknownCallModelExecution(
+    successors = listOf(
+        TsUnknownCallModelSuccessor(
+            guard = isArray,
+            completion = completion,
+        ),
+    ),
+    residualGuard = ctx.mkNot(isArray),
+)
+```
+
+Model authors are responsible for making successor guards and the residual guard disjoint and exhaustive. This
+property belongs in focused model tests; the dispatcher does not invoke the solver a second time merely to validate a
+model on every call.
+
+## When to write an intrinsic
+
+An intrinsic directly builds guarded successors and symbolic-memory operations in Kotlin. Use it only for an operation
+that TypeScript cannot express without losing symbolic efficiency or correctness.
+
+`Array.shift` is the built-in example because shifting a symbolic array is naturally represented by symbolic-memory
+`memcpy` operations. A resolved element sort uses one array region. A symbolic array with an unresolved element sort
+uses the boolean, number, and address regions that back a fake value; its removed element is materialized before
+forking so the exactly-one type constraint and updated solver models are inherited by every successor.
+
+Good intrinsic candidates include:
+
+- bulk symbolic-memory copy or fill;
+- symbolic collection primitives;
+- solver operations unavailable in the modeled language;
+- type-system operations that cannot be represented faithfully by ordinary code.
+
+Do not write an intrinsic merely because a library method is stateful.
+
+## Source-model migration
+
+A source model uses the same `TsUnknownCallModel` object and the same ID, target, successor, and residual contract.
+The source-model work in PR #380 should extend a successor completion with the EtsIR entry point and resolved inputs,
+make the model's EtsIR files visible in the analysis scene, and enter that method through the regular interpreter.
+Receiver binding, arguments, returns, exceptions, heap changes, aliases, and nested calls then use normal interpreter
+semantics. They must not be reimplemented in a source-specific dispatcher or backend registry.
+
+The model checks its supported domain before entering EtsIR. An unsupported call returns `null`; a guarded supported
+subdomain uses the complementary residual guard and the same configured fallback. Recursive redirection is prevented
+by tracking the active model ID in execution state, not by creating a second catalog.
+
+`Array.pop` is the source-model example. Its TypeScript body uses indexing and `length`; it must not call `pop` again.
+The existing `Array.shift` intrinsic remains the example for engine-only symbolic-memory `memcpy`.
+
+## Dynamic receivers
+
+A method name does not prove the receiver type. In particular, `value.shift()` may call a user-defined property rather
+than `Array.prototype.shift`.
+
+Use this decision rule:
+
+| Receiver knowledge | Action |
+| --- | --- |
+| Definitely the modeled built-in receiver type | Apply the model. |
+| Definitely another type | Return `null`; use fallback. |
+| Possibly the modeled type, with a trustworthy built-in target | Use a type guard and residual complement. |
+| `any`/unknown without proof of the built-in target | Return `null`; use fallback. |
+
+Never choose `typeStreamOf(receiver).firstOrNull()` as proof. It returns one possible type, not necessarily the only
+possible type. Use a statically proven type, `singleOrNull()` where uniqueness is guaranteed, or an explicit symbolic
+type guard.
+
+## Fingerprints
+
+The catalog sorts enabled models by ID and hashes their length-prefixed IDs. Therefore model registration order does
+not affect the fingerprint and ambiguous concatenations cannot collide merely because of ID boundaries.
+
+The fingerprint identifies the frozen enabled model set for one run. It is not a version and must not be used as a
+manually maintained configuration value. Experiment metadata records the tool revision separately. If model source
+can change independently of that revision, the runner also records a content hash for the external source or generated
+artifact; that content identity is experiment metadata, not another model ID, version, or compatibility setting. Keep
+the catalog fingerprint based only on enabled model IDs rather than adding implementation-specific fingerprint fields
+to the common model contract.
+
+## Observation
+
+Every applied model or fallback produces `TsUnknownCallEvent` through `TsInterpreterObserver.onUnknownCall`.
+
+- `ModelApplied(modelId)` identifies the semantic model.
+- `ResidualFallback(policy)` records the effective fallback.
+- `event.outcome` is derived from the decision and is not stored as a second independent value.
+
+Observer failures are logged and cannot alter symbolic exploration.
diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt
index af7236837..7ab3d97d9 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt
@@ -8,6 +8,7 @@ import org.usvm.UExpr
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.TsState
 import org.usvm.machine.types.mkFakeValue
 
 fun mockMethodCall(
@@ -15,28 +16,38 @@ fun mockMethodCall(
     method: EtsMethodSignature,
     resultType: EtsType = method.returnType,
 ) {
+    val result = makeFreshUnknownCallResult(scope, resultType)
+
     scope.doWithState {
-        val result: UExpr<*>
-        if (resultType is EtsVoidType) {
-            result = ctx.mkUndefinedValue()
-        } else {
-            val sort = ctx.typeToSort(resultType)
-            result = when (sort) {
-                is UAddressSort -> makeSymbolicRefUntyped()
-
-                is TsUnresolvedSort -> scope.calcOnState {
-                    mkFakeValue(
-                        scope = scope,
-                        boolValue = makeSymbolicPrimitive(ctx.boolSort),
-                        fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
-                        refValue = makeSymbolicRefUntyped(),
-                    )
-                }
-
-                else -> makeSymbolicPrimitive(sort)
-            }
-        }
-
-        methodResult = TsMethodResult.Success.MockedCall(result, method)
+        setMockMethodCallResult(method, result)
+    }
+}
+
+/** Stores a prepared opaque result on this state without applying callee effects or exceptions. */
+internal fun TsState.setMockMethodCallResult(
+    method: EtsMethodSignature,
+    result: UExpr<*>,
+) {
+    methodResult = TsMethodResult.Success.MockedCall(result, method)
+}
+
+/** Creates a fresh opaque result through [scope], keeping solver models consistent with new constraints. */
+internal fun makeFreshUnknownCallResult(
+    scope: TsStepScope,
+    resultType: EtsType,
+): UExpr<*> = scope.calcOnState {
+    if (resultType is EtsVoidType) return@calcOnState ctx.mkUndefinedValue()
+
+    when (val sort = ctx.typeToSort(resultType)) {
+        is UAddressSort -> makeSymbolicRefUntyped()
+
+        is TsUnresolvedSort -> mkFakeValue(
+            scope,
+            boolValue = makeSymbolicPrimitive(ctx.boolSort),
+            fpValue = makeSymbolicPrimitive(ctx.fp64Sort),
+            refValue = makeSymbolicRefUntyped(),
+        )
+
+        else -> makeSymbolicPrimitive(sort)
     }
 }
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 9ae27cb06..0248715fa 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -9,8 +9,8 @@ import org.jacodb.ets.model.EtsBooleanLiteralType
 import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsGenericType
-import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsLexicalEnvType
+import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberLiteralType
@@ -34,6 +34,7 @@ import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.UIteExpr
 import org.usvm.USort
 import org.usvm.api.allocateConcreteRef
 import org.usvm.api.allocateStaticRef
@@ -183,6 +184,12 @@ class TsContext(
     fun UConcreteHeapRef.getFakeType(scope: TsStepScope): EtsFakeType =
         scope.calcOnState { getFakeType(memory) }
 
+    /**
+     * Returns whether this expression is the storage identity of a synthetic fake-value wrapper.
+     *
+     * A positive result says nothing about the wrapper's active runtime kind. In particular, the expression must not
+     * be used as the represented object reference; inspect [EtsFakeType.refTypeExpr] and extract the reference payload.
+     */
     @OptIn(ExperimentalContracts::class)
     fun UExpr<*>.isFakeObject(): Boolean {
         contract {
@@ -192,6 +199,13 @@ class TsContext(
         return sort == addressSort && this is UConcreteHeapRef && address > MAGIC_OFFSET
     }
 
+    /** Returns whether this expression contains a fake-value wrapper as itself or as a conditional branch. */
+    fun UExpr<*>.containsFakeObject(): Boolean = when {
+        isFakeObject() -> true
+        this is UIteExpr<*> -> trueBranch.containsFakeObject() || falseBranch.containsFakeObject()
+        else -> false
+    }
+
     fun UExpr<*>.toFakeObject(scope: TsStepScope): UConcreteHeapRef {
         if (isFakeObject()) {
             return this
@@ -238,6 +252,12 @@ class TsContext(
         }
     }
 
+    /**
+     * Returns the reference payload of a fake-value wrapper without adding a reference-kind constraint.
+     *
+     * Use this only when [EtsFakeType.refTypeExpr] is already known or the caller guards the result equivalently.
+     * Otherwise use [unwrapRefWithPathConstraint].
+     */
     fun UHeapRef.unwrapRef(scope: TsStepScope): UHeapRef {
         if (isFakeObject()) {
             return extractRef(scope)
@@ -245,6 +265,9 @@ class TsContext(
         return this
     }
 
+    /**
+     * Extracts the reference payload from a fake-value wrapper and constrains that wrapper to the reference kind.
+     */
     fun UHeapRef.unwrapRefWithPathConstraint(scope: TsStepScope): UHeapRef {
         if (isFakeObject()) {
             scope.assert(getFakeType(scope).refTypeExpr)
@@ -285,6 +308,12 @@ class TsContext(
         return memory.read(lValue)
     }
 
+    /**
+     * Reads the reference payload without constraining [EtsFakeType.refTypeExpr].
+     *
+     * This operation alone does not prove that the wrapped value is a reference. The caller must either assert the
+     * discriminator through a live [TsStepScope] or use the payload only under an equivalent guard.
+     */
     fun UConcreteHeapRef.extractRef(memory: UReadOnlyMemory<*>): UHeapRef {
         check(isFakeObject())
         val lValue = getIntermediateRefLValue(address)
@@ -299,6 +328,7 @@ class TsContext(
         return scope.calcOnState { extractFp(memory) }
     }
 
+    /** Reads the reference payload through [scope] without adding a reference-kind constraint. */
     fun UConcreteHeapRef.extractRef(scope: TsStepScope): UHeapRef {
         return scope.calcOnState { extractRef(memory) }
     }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt
index df1ad1961..6b6c45168 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt
@@ -13,7 +13,7 @@ import org.usvm.statistics.UInterpreterObserver
 
 @Suppress("unused")
 interface TsInterpreterObserver : UInterpreterObserver {
-    /** Called after the profile dispatcher selects an outcome for an unknown call. */
+    /** Called after the dispatcher selects a model or fallback decision for an unknown call. */
     fun onUnknownCall(event: TsUnknownCallEvent) {
         // default empty implementation
     }
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 3d6b394f3..15e480447 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -9,10 +9,10 @@ import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
 import org.usvm.api.targets.TsTarget
-import org.usvm.machine.call.TsNoUnknownCallModels
-import org.usvm.machine.call.TsProfileUnknownCallDispatcher
+import org.usvm.machine.call.TsBuiltInUnknownCallModels
+import org.usvm.machine.call.TsModelUnknownCallDispatcher
 import org.usvm.machine.call.TsUnknownCallDispatcher
-import org.usvm.machine.call.TsUnknownCallModelProvider
+import org.usvm.machine.call.TsUnknownCallModelCatalog
 import org.usvm.machine.interpreter.TsInterpreter
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
@@ -45,15 +45,25 @@ class TsMachine(
     private val machineObserver: UMachineObserver<TsState>? = null,
     observer: TsInterpreterObserver? = null,
     unknownCallDispatcher: TsUnknownCallDispatcher? = null,
-    unknownCallModelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels,
+    unknownCallModels: TsUnknownCallModelCatalog? = null,
 ) : UMachine<TsState>() {
+    private val resolvedUnknownCallModels = when {
+        unknownCallDispatcher != null -> null
+        unknownCallModels != null -> unknownCallModels
+        else -> TsBuiltInUnknownCallModels.catalog(tsOptions.enabledUnknownCallModelIds)
+    }
+
+    /** Fingerprint of the model catalog used by this machine, or `null` for a custom dispatcher. */
+    val unknownCallModelCatalogFingerprint: String?
+        get() = resolvedUnknownCallModels?.fingerprint
+
     private val graph = TsGraph(scene)
     private val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, graph.hierarchy)
     private val components = TsComponents(typeSystem, options)
     private val ctx = TsContext(scene, components)
-    private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsProfileUnknownCallDispatcher(
-        profile = tsOptions.unknownCallProfile,
-        modelProvider = unknownCallModelProvider,
+    private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher(
+        models = requireNotNull(resolvedUnknownCallModels),
+        fallback = tsOptions.unknownCallFallback,
         observer = observer,
     )
     private val interpreter = TsInterpreter(
@@ -62,6 +72,7 @@ class TsMachine(
         options = tsOptions,
         observer = observer,
         unknownCallDispatcher = resolvedUnknownCallDispatcher,
+        throwExceptionOnStepFailure = options.throwExceptionOnStepFailure,
     )
     private val cfgStatistics = CfgStatisticsImpl(graph)
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt
index 09c3e6659..c3213f3a8 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt
@@ -1,11 +1,12 @@
 package org.usvm.machine
 
-import org.usvm.machine.call.TsUnknownCallProfile
-import org.usvm.machine.call.TsUnknownCallProfiles
+import org.usvm.machine.call.TsResidualCallPolicy
 
 data class TsOptions(
     val interproceduralAnalysis: Boolean = true,
     val enableVisualization: Boolean = false,
     val maxArraySize: Int = 1_000,
-    val unknownCallProfile: TsUnknownCallProfile = TsUnknownCallProfiles.MODELS_THEN_STOP,
+    /** `null` enables every built-in model; an empty set disables all models. */
+    val enabledUnknownCallModelIds: Set<String>? = null,
+    val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH,
 )
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt
new file mode 100644
index 000000000..51fd7c34e
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltInUnknownCallModels.kt
@@ -0,0 +1,13 @@
+package org.usvm.machine.call
+
+import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel
+
+/** The intentionally small built-in semantic-model catalog. */
+object TsBuiltInUnknownCallModels {
+    const val ARRAY_SHIFT_MODEL_ID: String = TsArrayShiftIntrinsicModel.MODEL_ID
+
+    fun catalog(enabledModelIds: Set<String>? = null) = TsUnknownCallModelCatalog(
+        models = listOf(TsArrayShiftIntrinsicModel),
+        enabledModelIds = enabledModelIds,
+    )
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt
index bb99b6ec9..48bffe05a 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCall.kt
@@ -60,6 +60,7 @@ enum class TsUnknownCallFailureReason {
     METHOD_BODY_UNAVAILABLE,
     INTERPROCEDURAL_ANALYSIS_DISABLED,
     LOGGING_CALL,
+    PARTIAL_APPROXIMATION,
 }
 
 /** Handles TypeScript calls that could not be executed by the regular call pipeline. */
@@ -67,6 +68,9 @@ fun interface TsUnknownCallDispatcher {
     fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome
 }
 
+/** Marks dispatchers that replace migrated compatibility approximations with semantic models. */
+interface TsUnknownCallModelDispatcher : TsUnknownCallDispatcher
+
 /** Preserves the pruning and opaque-return behavior that existed before the common dispatch boundary. */
 object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
     override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome {
@@ -109,6 +113,10 @@ object TsCompatibilityUnknownCallDispatcher : TsUnknownCallDispatcher {
                 scope.assert(falseExpr)
                 return TsUnknownCallOutcome.PATH_STOPPED
             }
+
+            TsUnknownCallFailureReason.PARTIAL_APPROXIMATION -> {
+                error("Migrated approximations must not be sent to the compatibility dispatcher")
+            }
         }
     }
 }
@@ -152,10 +160,10 @@ internal fun TsUnknownCallDispatcher.dispatch(
     failureReason: TsUnknownCallFailureReason,
     resolvedReceiver: UExpr<*>,
 ) = dispatch(
-    scope = scope,
-    call = call.call,
-    callSite = call.returnSite,
-    failureReason = failureReason,
+    scope,
+    call.call,
+    call.returnSite,
+    failureReason,
     resolvedReceiver = resolvedReceiver,
     resolvedArguments = call.args,
 )
@@ -166,11 +174,11 @@ internal fun TsUnknownCallDispatcher.dispatch(
     failureReason: TsUnknownCallFailureReason,
     callee: EtsMethodSignature,
 ) = dispatch(
-    scope = scope,
-    call = call.call,
-    callSite = call.returnSite,
-    failureReason = failureReason,
-    callee = callee,
+    scope,
+    call.call,
+    call.returnSite,
+    failureReason,
+    callee,
     resolvedReceiver = call.resolvedReceiver,
     resolvedArguments = call.args.takeLast(call.call.args.size),
 )
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt
new file mode 100644
index 000000000..240f4f003
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModel.kt
@@ -0,0 +1,107 @@
+package org.usvm.machine.call
+
+import org.jacodb.ets.model.EtsType
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.machine.state.TsState
+import org.usvm.machine.types.TsUnresolvedValue
+
+/** Declaratively identifies the calls handled by one semantic model. */
+data class TsUnknownCallTarget(
+    val methodName: String,
+    val enclosingClassName: String? = null,
+    val failureReason: TsUnknownCallFailureReason? = null,
+) {
+    init {
+        require(methodName.isNotBlank()) { "Semantic model target method name must not be blank" }
+        require(enclosingClassName == null || enclosingClassName.isNotBlank()) {
+            "Semantic model target class name must not be blank"
+        }
+    }
+
+    internal fun matches(call: TsUnknownCall): Boolean =
+        call.callee.name == methodName &&
+            (enclosingClassName == null || call.callee.enclosingClass.name == enclosingClassName) &&
+            (failureReason == null || call.failureReason == failureReason)
+
+    internal fun overlaps(other: TsUnknownCallTarget): Boolean {
+        val classNamesOverlap = enclosingClassName == null ||
+            other.enclosingClassName == null ||
+            enclosingClassName == other.enclosingClassName
+        val failureReasonsOverlap = failureReason == null ||
+            other.failureReason == null ||
+            failureReason == other.failureReason
+
+        return methodName == other.methodName && classNamesOverlap && failureReasonsOverlap
+    }
+}
+
+/**
+ * A semantic model selected by a stable [id] and a declarative [target].
+ *
+ * Returning `null` from [apply] means that the call is outside the model's supported input domain. The dispatcher
+ * then applies the configured fallback. A non-null execution may additionally contain a guarded residual domain.
+ */
+interface TsUnknownCallModel {
+    val id: String
+    val target: TsUnknownCallTarget
+
+    fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution?
+}
+
+/** Describes how a guarded model successor completes the original call. */
+sealed interface TsUnknownCallModelCompletion {
+    /** Produces a normal result on the selected successor state. */
+    class Normal(
+        val result: TsState.() -> UExpr<*>,
+    ) : TsUnknownCallModelCompletion
+
+    /** Produces a normal fake-wrapped result for a value whose runtime kind is unresolved. */
+    class Unresolved(
+        val value: TsUnresolvedValue,
+    ) : TsUnknownCallModelCompletion
+
+    /** Produces an exceptional result and its TypeScript type on the selected successor state. */
+    class Exceptional(
+        val exception: TsState.() -> Pair<UExpr<*>, EtsType>,
+    ) : TsUnknownCallModelCompletion
+}
+
+/** One guarded model successor. */
+class TsUnknownCallModelSuccessor(
+    val guard: UBoolExpr,
+    val completion: TsUnknownCallModelCompletion,
+    val applyStateChanges: TsState.() -> Unit = {},
+)
+
+/**
+ * A semantic-model execution plan.
+ *
+ * [residualGuard] is the input domain not covered by the model. `null` means that the model completely handles every
+ * state accepted by [TsUnknownCallModel.apply].
+ */
+class TsUnknownCallModelExecution(
+    successors: List<TsUnknownCallModelSuccessor>,
+    val residualGuard: UBoolExpr? = null,
+) {
+    val successors: List<TsUnknownCallModelSuccessor> = successors.toList()
+
+    init {
+        require(this.successors.isNotEmpty()) { "A semantic model must declare at least one guarded successor" }
+    }
+}
+
+/** The result of model lookup for one call. */
+sealed interface TsUnknownCallModelApplication {
+    class Applied(
+        val modelId: String,
+        val execution: TsUnknownCallModelExecution,
+    ) : TsUnknownCallModelApplication {
+        init {
+            require(modelId.isNotBlank()) { "Applied model ID must not be blank" }
+        }
+    }
+
+    /** No enabled model accepted the call. */
+    data object NotApplicable : TsUnknownCallModelApplication
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt
new file mode 100644
index 000000000..dd74e9343
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalog.kt
@@ -0,0 +1,92 @@
+package org.usvm.machine.call
+
+import org.usvm.machine.state.TsState
+import java.nio.ByteBuffer
+import java.nio.charset.StandardCharsets
+import java.security.MessageDigest
+
+private const val BYTE_MASK = 0xff
+
+/** An immutable deterministic set of semantic models used by one machine run. */
+class TsUnknownCallModelCatalog(
+    models: Collection<TsUnknownCallModel>,
+    enabledModelIds: Set<String>? = null,
+) {
+    private val models: List<TsUnknownCallModel>
+
+    val modelIds: List<String>
+        get() = models.map(TsUnknownCallModel::id)
+
+    val fingerprint: String
+
+    init {
+        val allModels = models.sortedBy(TsUnknownCallModel::id)
+        val duplicateIds = allModels
+            .groupingBy(TsUnknownCallModel::id)
+            .eachCount()
+            .filterValues { count -> count > 1 }
+            .keys
+            .sorted()
+
+        require(allModels.none { model -> model.id.isBlank() }) { "Semantic model ID must not be blank" }
+        require(duplicateIds.isEmpty()) { "Duplicate semantic model IDs: ${duplicateIds.joinToString()}" }
+
+        val selectedIds = enabledModelIds?.toSet()
+        val knownIds = allModels.mapTo(mutableSetOf(), TsUnknownCallModel::id)
+        val unknownIds = selectedIds.orEmpty().subtract(knownIds).sorted()
+
+        require(unknownIds.isEmpty()) { "Unknown semantic model IDs: ${unknownIds.joinToString()}" }
+
+        this.models = when (selectedIds) {
+            null -> allModels
+            else -> allModels.filter { model -> model.id in selectedIds }
+        }
+
+        validateUnambiguousTargets(this.models)
+        fingerprint = computeFingerprint(this.models)
+    }
+
+    internal fun select(call: TsUnknownCall): TsUnknownCallModel? =
+        models.singleOrNull { model -> model.target.matches(call) }
+
+    fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelApplication {
+        val model = select(call) ?: return TsUnknownCallModelApplication.NotApplicable
+        val execution = model.apply(state, call) ?: return TsUnknownCallModelApplication.NotApplicable
+
+        return TsUnknownCallModelApplication.Applied(
+            modelId = model.id,
+            execution = execution,
+        )
+    }
+}
+
+private fun validateUnambiguousTargets(models: List<TsUnknownCallModel>) {
+    models.forEachIndexed { index, model ->
+        val conflictingModel = models.drop(index + 1).firstOrNull { other ->
+            model.target.overlaps(other.target)
+        } ?: return@forEachIndexed
+
+        error(
+            "Ambiguous semantic model targets: " +
+                listOf(model.id, conflictingModel.id).sorted().joinToString()
+        )
+    }
+}
+
+private fun computeFingerprint(models: List<TsUnknownCallModel>): String {
+    val digest = MessageDigest.getInstance("SHA-256")
+
+    models.forEach { model ->
+        digest.updateLengthPrefixed(model.id)
+    }
+
+    return digest.digest().joinToString(separator = "") { byte ->
+        "%02x".format(byte.toInt() and BYTE_MASK)
+    }
+}
+
+private fun MessageDigest.updateLengthPrefixed(value: String) {
+    val bytes = value.toByteArray(StandardCharsets.UTF_8)
+    update(ByteBuffer.allocate(Int.SIZE_BYTES).putInt(bytes.size).array())
+    update(bytes)
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt
new file mode 100644
index 000000000..5a524e6de
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt
@@ -0,0 +1,188 @@
+package org.usvm.machine.call
+
+import org.usvm.UExpr
+import org.usvm.api.makeFreshUnknownCallResult
+import org.usvm.api.mockMethodCall
+import org.usvm.api.setMockMethodCallResult
+import org.usvm.machine.TsInterpreterObserver
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.TsState
+import org.usvm.machine.state.newStmt
+import org.usvm.machine.types.mkFakeValue
+
+/** The externally observable effect of an unknown-call decision. */
+enum class TsUnknownCallOutcome {
+    MODEL_APPLIED,
+    FRESH_SYMBOLIC_RETURN,
+    PATH_STOPPED,
+}
+
+/** Selects what happens when no semantic model handles an unknown call. */
+enum class TsResidualCallPolicy {
+    STOP_PATH,
+    FRESH_SYMBOLIC_RETURN,
+}
+
+/** Selects a semantic model and sends unsupported states to one configured fallback. */
+class TsModelUnknownCallDispatcher(
+    private val models: TsUnknownCallModelCatalog,
+    private val fallback: TsResidualCallPolicy,
+    private val observer: TsInterpreterObserver? = null,
+) : TsUnknownCallModelDispatcher {
+    override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome {
+        val application = scope.calcOnState {
+            this@TsModelUnknownCallDispatcher.models.apply(this, call)
+        }
+
+        return when (application) {
+            is TsUnknownCallModelApplication.Applied -> applyModel(scope, call, application)
+            TsUnknownCallModelApplication.NotApplicable -> applyFallback(scope, call)
+        }
+    }
+
+    private fun applyFallback(
+        scope: TsStepScope,
+        call: TsUnknownCall,
+    ): TsUnknownCallOutcome {
+        val decision = TsUnknownCallDecision.ResidualFallback(fallback)
+
+        when (fallback) {
+            TsResidualCallPolicy.STOP_PATH -> {
+                val falseExpr = scope.calcOnState { ctx.falseExpr }
+                scope.assert(falseExpr)
+            }
+
+            TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> {
+                mockMethodCall(scope, call.callee, call.resultType)
+                scope.doWithState { newStmt(call.callSite) }
+            }
+        }
+
+        observer?.onUnknownCallSafely(event(call, decision))
+        return decision.outcome
+    }
+
+    private fun applyModel(
+        scope: TsStepScope,
+        call: TsUnknownCall,
+        application: TsUnknownCallModelApplication.Applied,
+    ): TsUnknownCallOutcome {
+        val residualGuard = application.execution.residualGuard
+        // Creating an unresolved value may add fake-value constraints. Do it before forking so the residual clone
+        // inherits both the constraints and their solver models.
+        val freshResidualResult = if (
+            residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN
+        ) {
+            makeFreshUnknownCallResult(scope, call.resultType)
+        } else {
+            null
+        }
+        val stoppedResidualIsSatisfiable = residualGuard != null &&
+            fallback == TsResidualCallPolicy.STOP_PATH &&
+            scope.checkSat(residualGuard) != null
+
+        var modelApplied = false
+        var modelEventReported = false
+        var freshResidualApplied = false
+        // Materializing an unresolved result adds its exactly-one constraint. Do it before forking so every
+        // successor that uses the wrapper inherits both the constraint and the refreshed solver models.
+        val preparedUnresolvedResults = application.execution.successors.map { successor ->
+            val completion = successor.completion as? TsUnknownCallModelCompletion.Unresolved
+                ?: return@map null
+
+            scope.calcOnState {
+                mkFakeValue(scope = scope, value = completion.value)
+            }
+        }
+        val guardedStateChanges = application.execution.successors.mapIndexed { index, successor ->
+            successor.guard to modelStateChange(
+                call = call,
+                modelId = application.modelId,
+                successor = successor,
+                preparedUnresolvedResult = preparedUnresolvedResults[index],
+                onApplied = {
+                    modelApplied = true
+                    if (modelEventReported) {
+                        false
+                    } else {
+                        modelEventReported = true
+                        true
+                    }
+                },
+            )
+        }.toMutableList()
+
+        if (residualGuard != null && fallback == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) {
+            guardedStateChanges += residualGuard to {
+                setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult))
+                newStmt(call.callSite)
+                freshResidualApplied = true
+
+                val decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN)
+                val fallbackEvent = event(call, decision)
+                observer?.onUnknownCallSafely(fallbackEvent)
+            }
+        }
+
+        scope.forkMulti(guardedStateChanges)
+
+        if (stoppedResidualIsSatisfiable) {
+            val decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH)
+            val fallbackEvent = event(call, decision)
+            observer?.onUnknownCallSafely(fallbackEvent)
+        }
+
+        return when {
+            modelApplied -> TsUnknownCallOutcome.MODEL_APPLIED
+            freshResidualApplied -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN
+            stoppedResidualIsSatisfiable -> TsUnknownCallOutcome.PATH_STOPPED
+            else -> error("Semantic model ${application.modelId} produced no satisfiable successor or residual state")
+        }
+    }
+
+    private fun modelStateChange(
+        call: TsUnknownCall,
+        modelId: String,
+        successor: TsUnknownCallModelSuccessor,
+        preparedUnresolvedResult: UExpr<*>?,
+        onApplied: () -> Boolean,
+    ): TsState.() -> Unit = {
+        successor.applyStateChanges(this)
+
+        when (val completion = successor.completion) {
+            is TsUnknownCallModelCompletion.Normal -> {
+                val result = completion.result(this)
+                methodResult = TsMethodResult.Success.MockedCall(result, call.callee)
+                newStmt(call.callSite)
+            }
+
+            is TsUnknownCallModelCompletion.Unresolved -> {
+                val result = requireNotNull(preparedUnresolvedResult) {
+                    "Unresolved semantic-model result was not materialized"
+                }
+                methodResult = TsMethodResult.Success.MockedCall(result, call.callee)
+                newStmt(call.callSite)
+            }
+
+            is TsUnknownCallModelCompletion.Exceptional -> {
+                val (exception, type) = completion.exception(this)
+                methodResult = TsMethodResult.TsException(exception, type)
+            }
+        }
+
+        if (onApplied()) {
+            observer?.onUnknownCallSafely(event(call, TsUnknownCallDecision.ModelApplied(modelId)))
+        }
+    }
+
+    private fun event(
+        call: TsUnknownCall,
+        decision: TsUnknownCallDecision,
+    ) = TsUnknownCallEvent(
+        callSite = call.callSite,
+        callee = call.callee,
+        failureReason = call.failureReason,
+        decision = decision,
+    )
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt
index 7adf43527..2ae84bffd 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallObservation.kt
@@ -7,12 +7,6 @@ import org.usvm.machine.TsInterpreterObserver
 
 private val logger = KotlinLogging.logger {}
 
-/** Explains why a call reached the residual fallback instead of a semantic model. */
-enum class TsUnknownCallResidualReason {
-    MODEL_LOOKUP_DISABLED,
-    MODEL_NOT_APPLICABLE,
-}
-
 /** Describes the model or fallback action selected for one unknown call. */
 sealed interface TsUnknownCallDecision {
     data class ModelApplied(
@@ -25,19 +19,28 @@ sealed interface TsUnknownCallDecision {
 
     data class ResidualFallback(
         val policy: TsResidualCallPolicy,
-        val reason: TsUnknownCallResidualReason,
     ) : TsUnknownCallDecision
 }
 
+val TsUnknownCallDecision.outcome: TsUnknownCallOutcome
+    get() = when (this) {
+        is TsUnknownCallDecision.ModelApplied -> TsUnknownCallOutcome.MODEL_APPLIED
+        is TsUnknownCallDecision.ResidualFallback -> when (policy) {
+            TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED
+            TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN
+        }
+    }
+
 /** A structured decision reported for one unknown call. */
 data class TsUnknownCallEvent(
     val callSite: EtsStmt,
     val callee: EtsMethodSignature,
     val failureReason: TsUnknownCallFailureReason,
-    val profile: TsUnknownCallProfile,
-    val outcome: TsUnknownCallOutcome,
     val decision: TsUnknownCallDecision,
-)
+) {
+    val outcome: TsUnknownCallOutcome
+        get() = decision.outcome
+}
 
 internal fun TsInterpreterObserver.onUnknownCallSafely(event: TsUnknownCallEvent) {
     runCatching { onUnknownCall(event) }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt
deleted file mode 100644
index 66e4eeb1f..000000000
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallProfile.kt
+++ /dev/null
@@ -1,167 +0,0 @@
-package org.usvm.machine.call
-
-import org.jacodb.ets.model.EtsClassSignature
-import org.usvm.api.mockMethodCall
-import org.usvm.machine.TsInterpreterObserver
-import org.usvm.machine.interpreter.TsStepScope
-import org.usvm.machine.state.newStmt
-
-/** The externally observable decision made for a call that could not be executed normally. */
-enum class TsUnknownCallOutcome {
-    MODEL_APPLIED,
-    FRESH_SYMBOLIC_RETURN,
-    PATH_STOPPED,
-}
-
-/** Controls whether the dispatcher asks the configured model provider to handle a call. */
-enum class TsUnknownCallModelLookup {
-    DISABLED,
-    ENABLED,
-}
-
-/**
- * Selects what happens when model lookup is disabled or no model applies.
- *
- * [FRESH_SYMBOLIC_RETURN] creates a new symbolic value of the call expression's result type and advances past the
- * call. It deliberately ignores all callee side effects and exceptions, so it is an opaque continuation rather than
- * a semantic model of the callee.
- */
-enum class TsResidualCallPolicy {
-    STOP_PATH,
-    FRESH_SYMBOLIC_RETURN,
-}
-
-/** Independently configures model lookup and the fallback for residual calls. */
-data class TsUnknownCallProfile(
-    val modelLookup: TsUnknownCallModelLookup,
-    val residualPolicy: TsResidualCallPolicy,
-    val residualOverrides: Map<EtsClassSignature, TsResidualCallPolicy> = emptyMap(),
-) {
-    internal fun residualPolicyFor(call: TsUnknownCall): TsResidualCallPolicy =
-        residualOverrides[call.callee.enclosingClass] ?: residualPolicy
-}
-
-/** Ready-to-use profiles for the four supported model/fallback combinations. */
-object TsUnknownCallProfiles {
-    val STOP_ALL = TsUnknownCallProfile(
-        modelLookup = TsUnknownCallModelLookup.DISABLED,
-        residualPolicy = TsResidualCallPolicy.STOP_PATH,
-    )
-    val FRESH_SYMBOLIC_FOR_ALL = TsUnknownCallProfile(
-        modelLookup = TsUnknownCallModelLookup.DISABLED,
-        residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
-    )
-    val MODELS_THEN_STOP = TsUnknownCallProfile(
-        modelLookup = TsUnknownCallModelLookup.ENABLED,
-        residualPolicy = TsResidualCallPolicy.STOP_PATH,
-    )
-    val MODELS_THEN_FRESH_SYMBOLIC = TsUnknownCallProfile(
-        modelLookup = TsUnknownCallModelLookup.ENABLED,
-        residualPolicy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
-    )
-}
-
-/** The result of asking a model provider to handle one unknown call. */
-sealed interface TsUnknownCallModelApplication {
-    /** Identifies the semantic model that produced the successor states. */
-    data class Applied(
-        val modelId: String,
-    ) : TsUnknownCallModelApplication {
-        init {
-            require(modelId.isNotBlank()) { "Applied model ID must not be blank" }
-        }
-    }
-
-    /** Indicates that the provider has no semantic model for this call. */
-    data object NotApplicable : TsUnknownCallModelApplication
-}
-
-/**
- * Applies semantic models without exposing their lookup or registry implementation to the dispatcher.
- *
- * A provider returning [TsUnknownCallModelApplication.Applied] must update the supplied scope with the model's
- * successor states. The deterministic registry and concrete model implementations are introduced separately.
- */
-fun interface TsUnknownCallModelProvider {
-    fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication
-}
-
-/** Empty provider used until an explicit model registry is configured. */
-object TsNoUnknownCallModels : TsUnknownCallModelProvider {
-    override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication =
-        TsUnknownCallModelApplication.NotApplicable
-}
-
-/** Applies the selected model/fallback profile to every residual call. */
-class TsProfileUnknownCallDispatcher(
-    private val profile: TsUnknownCallProfile,
-    private val modelProvider: TsUnknownCallModelProvider,
-    private val observer: TsInterpreterObserver? = null,
-) : TsUnknownCallDispatcher {
-    override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome {
-        val residualReason = when (profile.modelLookup) {
-            TsUnknownCallModelLookup.DISABLED -> {
-                TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED
-            }
-
-            TsUnknownCallModelLookup.ENABLED -> {
-                when (val application = modelProvider.apply(scope, call)) {
-                    is TsUnknownCallModelApplication.Applied -> {
-                        val event = event(
-                            call = call,
-                            outcome = TsUnknownCallOutcome.MODEL_APPLIED,
-                            decision = TsUnknownCallDecision.ModelApplied(modelId = application.modelId),
-                        )
-                        observer?.onUnknownCallSafely(event)
-                        return TsUnknownCallOutcome.MODEL_APPLIED
-                    }
-
-                    TsUnknownCallModelApplication.NotApplicable -> {
-                        TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE
-                    }
-                }
-            }
-        }
-
-        val residualPolicy = profile.residualPolicyFor(call)
-        val outcome = when (residualPolicy) {
-            TsResidualCallPolicy.STOP_PATH -> TsUnknownCallOutcome.PATH_STOPPED
-            TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN
-        }
-        val event = event(
-            call = call,
-            outcome = outcome,
-            decision = TsUnknownCallDecision.ResidualFallback(
-                policy = residualPolicy,
-                reason = residualReason,
-            ),
-        )
-        when (residualPolicy) {
-            TsResidualCallPolicy.STOP_PATH -> {
-                val falseExpr = scope.calcOnState { ctx.falseExpr }
-                scope.assert(falseExpr)
-            }
-
-            TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> {
-                mockMethodCall(scope, call.callee, call.resultType)
-                scope.doWithState { newStmt(call.callSite) }
-            }
-        }
-
-        observer?.onUnknownCallSafely(event)
-        return outcome
-    }
-
-    private fun event(
-        call: TsUnknownCall,
-        outcome: TsUnknownCallOutcome,
-        decision: TsUnknownCallDecision,
-    ) = TsUnknownCallEvent(
-        callSite = call.callSite,
-        callee = call.callee,
-        failureReason = call.failureReason,
-        profile = profile.copy(residualOverrides = profile.residualOverrides.toMap()),
-        outcome = outcome,
-        decision = decision,
-    )
-}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt
new file mode 100644
index 000000000..5c8608af1
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt
@@ -0,0 +1,253 @@
+package org.usvm.machine.call.intrinsic
+
+import io.ksmt.utils.asExpr
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsUnknownType
+import org.usvm.UAddressSort
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.USort
+import org.usvm.api.memcpy
+import org.usvm.api.typeStreamOf
+import org.usvm.collection.array.UArrayIndexLValue
+import org.usvm.machine.TsSizeSort
+import org.usvm.machine.call.TsUnknownCall
+import org.usvm.machine.call.TsUnknownCallFailureReason
+import org.usvm.machine.call.TsUnknownCallModel
+import org.usvm.machine.call.TsUnknownCallModelCompletion
+import org.usvm.machine.call.TsUnknownCallModelExecution
+import org.usvm.machine.call.TsUnknownCallModelSuccessor
+import org.usvm.machine.call.TsUnknownCallTarget
+import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.expr.readSymbolicUnresolvedArrayElement
+import org.usvm.machine.state.TsState
+import org.usvm.machine.types.findMaterializedFakeValue
+import org.usvm.sizeSort
+import org.usvm.types.singleOrNull
+import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
+
+/** Engine intrinsic for `Array.shift`, whose bulk move is implemented by symbolic-memory `memcpy`. */
+internal object TsArrayShiftIntrinsicModel : TsUnknownCallModel {
+    const val MODEL_ID: String = "ts.array.shift"
+
+    override val id: String = MODEL_ID
+    override val target = TsUnknownCallTarget(
+        methodName = "shift",
+        failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION,
+    )
+
+    override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? = with(state.ctx) {
+        val input = resolveInput(state, call) ?: return@with null
+        val lengthLValue = mkArrayLengthLValue(input.array, input.arrayType)
+        val length = state.memory.read(lengthLValue)
+        val zero = mkBv(0)
+        val one = mkBv(1)
+        val emptyGuard = mkEq(length, zero)
+        val nonEmptyGuard = mkNot(emptyGuard)
+        val newLength = mkBvSubExpr(length, one)
+        val firstElementCompletion = state.firstElementCompletion(input, zero)
+
+        val emptySuccessor = TsUnknownCallModelSuccessor(
+            guard = emptyGuard,
+            completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() },
+        )
+        val nonEmptySuccessor = TsUnknownCallModelSuccessor(
+            guard = nonEmptyGuard,
+            completion = firstElementCompletion,
+            applyStateChanges = {
+                shiftElements(input, fromSrc = one, fromDst = zero, length = newLength)
+                memory.write(lengthLValue, newLength, guard = trueExpr)
+            },
+        )
+
+        TsUnknownCallModelExecution(successors = listOf(emptySuccessor, nonEmptySuccessor))
+    }
+
+    private fun resolveInput(state: TsState, call: TsUnknownCall): ArrayShiftInput? = with(state.ctx) {
+        if (call.arguments.isNotEmpty()) {
+            return@with null
+        }
+
+        val receiver = call.receiver ?: return@with null
+        val receiverValue = receiver.resolved ?: return@with null
+        if (receiverValue.sort != addressSort || receiverValue.containsFakeObject()) {
+            return@with null
+        }
+
+        val array = receiverValue.asExpr(addressSort)
+        val arrayType = (receiver.source.type as? EtsArrayType)
+            ?: (state.memory.typeStreamOf(array).singleOrNull() as? EtsArrayType)
+            ?: return@with null
+        if (arrayType.dimensions != 1) {
+            return@with null
+        }
+
+        val elementSort = typeToSort(arrayType.elementType)
+        ArrayShiftInput(array, arrayType, elementSort)
+    }
+
+    private fun TsState.firstElementCompletion(
+        input: ArrayShiftInput,
+        index: UExpr<TsSizeSort>,
+    ): TsUnknownCallModelCompletion = with(ctx) {
+        if (input.elementSort !is TsUnresolvedSort) {
+            val firstElementLValue = mkArrayIndexLValue(
+                sort = input.elementSort,
+                ref = input.array,
+                index = index,
+                type = input.arrayType,
+            )
+            val firstElement = memory.read(firstElementLValue)
+
+            return@with TsUnknownCallModelCompletion.Normal { firstElement }
+        }
+
+        if (input.array is UConcreteHeapRef) {
+            val firstElementLValue = mkArrayIndexLValue(
+                sort = addressSort,
+                ref = input.array,
+                index = index,
+                type = input.arrayType,
+            )
+            val firstElement = memory.read(firstElementLValue)
+
+            return@with TsUnknownCallModelCompletion.Normal {
+                check(firstElement.isFakeObject()) {
+                    "Expected fake object in concrete array with unresolved element type, got: $firstElement"
+                }
+                firstElement
+            }
+        }
+
+        val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+        val firstElementLValue = mkArrayIndexLValue(addressSort, input.array, index, unknownArrayType)
+        val materializedFirstElement = findMaterializedFakeValue(firstElementLValue)
+        if (materializedFirstElement != null) {
+            return@with TsUnknownCallModelCompletion.Normal { materializedFirstElement }
+        }
+
+        val firstElement = readSymbolicUnresolvedArrayElement(input.array, index)
+        TsUnknownCallModelCompletion.Unresolved(firstElement)
+    }
+
+    private fun TsState.shiftElements(
+        input: ArrayShiftInput,
+        fromSrc: UExpr<TsSizeSort>,
+        fromDst: UExpr<TsSizeSort>,
+        length: UExpr<TsSizeSort>,
+    ) = with(ctx) {
+        if (input.elementSort !is TsUnresolvedSort) {
+            copyArrayRegion(
+                input = input,
+                arrayType = input.arrayType,
+                elementSort = input.elementSort,
+                fromSrc = fromSrc,
+                fromDst = fromDst,
+                length = length,
+            )
+            return@with
+        }
+
+        if (input.array is UConcreteHeapRef) {
+            copyArrayRegion(
+                input = input,
+                arrayType = input.arrayType,
+                elementSort = addressSort,
+                fromSrc = fromSrc,
+                fromDst = fromDst,
+                length = length,
+            )
+            shiftMaterializedFakeValues(input)
+            return@with
+        }
+
+        copyArrayRegion(
+            input = input,
+            arrayType = EtsArrayType(EtsBooleanType, dimensions = 1),
+            elementSort = boolSort,
+            fromSrc = fromSrc,
+            fromDst = fromDst,
+            length = length,
+        )
+        copyArrayRegion(
+            input = input,
+            arrayType = EtsArrayType(EtsNumberType, dimensions = 1),
+            elementSort = fp64Sort,
+            fromSrc = fromSrc,
+            fromDst = fromDst,
+            length = length,
+        )
+        copyArrayRegion(
+            input = input,
+            arrayType = EtsArrayType(EtsUnknownType, dimensions = 1),
+            elementSort = addressSort,
+            fromSrc = fromSrc,
+            fromDst = fromDst,
+            length = length,
+        )
+        shiftMaterializedFakeValues(input)
+    }
+
+    private fun TsState.copyArrayRegion(
+        input: ArrayShiftInput,
+        arrayType: EtsArrayType,
+        elementSort: USort,
+        fromSrc: UExpr<TsSizeSort>,
+        fromDst: UExpr<TsSizeSort>,
+        length: UExpr<TsSizeSort>,
+    ) {
+        memory.memcpy(
+            srcRef = input.array,
+            dstRef = input.array,
+            type = ctx.arrayDescriptorOf(arrayType),
+            elementSort = elementSort,
+            fromSrc = fromSrc,
+            fromDst = fromDst,
+            length = length,
+        )
+    }
+
+    private fun TsState.shiftMaterializedFakeValues(input: ArrayShiftInput) = with(ctx) {
+        val arrayDescriptor = if (input.array is UConcreteHeapRef) {
+            arrayDescriptorOf(input.arrayType)
+        } else {
+            arrayDescriptorOf(EtsArrayType(EtsUnknownType, dimensions = 1))
+        }
+        val zero = mkBv(0)
+        val one = mkBv(1)
+        val shiftedValues = lValuesToAllocatedFakeObjects.mapNotNull { (lValue, fakeValue) ->
+            if (
+                lValue !is UArrayIndexLValue<*, *, *> ||
+                lValue.ref != input.array ||
+                lValue.arrayType != arrayDescriptor
+            ) {
+                return@mapNotNull null
+            }
+
+            val sourceIndex = lValue.index.asExpr(sizeSort)
+            if (sourceIndex == zero) {
+                return@mapNotNull null
+            }
+
+            val destinationIndex = mkBvSubExpr(sourceIndex, one)
+            val destinationLValue = UArrayIndexLValue(
+                addressSort,
+                input.array,
+                destinationIndex,
+                arrayDescriptor,
+            )
+            destinationLValue to fakeValue
+        }
+
+        lValuesToAllocatedFakeObjects += shiftedValues
+    }
+
+    private class ArrayShiftInput(
+        val array: UExpr<UAddressSort>,
+        val arrayType: EtsArrayType,
+        val elementSort: USort,
+    )
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
index 0060b4762..c48b2c552 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt
@@ -19,13 +19,17 @@ import org.usvm.api.memcpy
 import org.usvm.api.typeStreamOf
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.TsSizeSort
+import org.usvm.machine.call.TsUnknownCallFailureReason
+import org.usvm.machine.call.TsUnknownCallModelDispatcher
+import org.usvm.machine.call.dispatch
 import org.usvm.machine.expr.TsExprApproximationResult.Companion.from
 import org.usvm.machine.interpreter.PromiseState
 import org.usvm.machine.interpreter.markResolved
 import org.usvm.machine.interpreter.setResolvedValue
+import org.usvm.machine.state.lastStmt
 import org.usvm.sizeSort
 import org.usvm.types.first
-import org.usvm.types.firstOrNull
+import org.usvm.types.singleOrNull
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.resolveEtsMethods
@@ -89,7 +93,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
 
     val instanceType = if (instance.sort == addressSort && isAllocatedConcreteHeapRef(instance)) {
         scope.calcOnState {
-            memory.typeStreamOf(instance.asExpr(addressSort)).firstOrNull() ?: expr.instance.type
+            memory.typeStreamOf(instance.asExpr(addressSort)).singleOrNull() ?: expr.instance.type
         }
     } else {
         expr.instance.type
@@ -122,7 +126,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
 
         // Handle `Array.shift() method calls
         if (expr.callee.name == "shift") {
-            return from(handleArrayShift(expr, instanceType, elementSort))
+            return handleArrayShiftCall(expr, instanceType, elementSort, instance)
         }
 
         // Handle `Array.join() method calls
@@ -159,6 +163,28 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
     return TsExprApproximationResult.NoApproximation
 }
 
+private fun TsExprResolver.handleArrayShiftCall(
+    expr: EtsInstanceCallExpr,
+    instanceType: EtsArrayType,
+    elementSort: USort,
+    resolvedReceiver: UExpr<*>,
+): TsExprApproximationResult {
+    val dispatcher = unknownCallDispatcher
+    if (dispatcher !is TsUnknownCallModelDispatcher) {
+        return from(handleArrayShift(expr, instanceType, elementSort))
+    }
+
+    dispatcher.dispatch(
+        scope,
+        expr,
+        scope.calcOnState { lastStmt },
+        failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION,
+        resolvedReceiver = resolvedReceiver,
+    )
+
+    return TsExprApproximationResult.ResolveFailure
+}
+
 private fun TsExprResolver.handleValueOf(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
     if (expr.args.isNotEmpty()) {
         logger.warn { "valueOf() should have no arguments, but got ${expr.args.size}" }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt
index 684c8902d..3b097ad1a 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt
@@ -15,6 +15,9 @@ import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.TsContext
 import org.usvm.machine.TsSizeSort
 import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsState
+import org.usvm.machine.types.TsUnresolvedValue
+import org.usvm.machine.types.findMaterializedFakeValue
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.sizeSort
 import org.usvm.types.first
@@ -127,28 +130,49 @@ fun TsContext.readArray(
     // that can hold boolean, number, and reference values.
     // We read all three types from the array and combine them into a fake object.
     return scope.calcOnState {
-        val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1)
-        val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType)
-        val bool = memory.read(boolLValue)
-
-        val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
-        val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType)
-        val fp = memory.read(fpLValue)
-
         val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
         val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType)
-        val ref = memory.read(refLValue)
+        val materializedValue = findMaterializedFakeValue(refLValue)
+        if (materializedValue != null) {
+            return@calcOnState materializedValue
+        }
+
+        val value = readSymbolicUnresolvedArrayElement(array, index)
 
-        // If the read reference is already a fake object, we can return it directly.
-        // Otherwise, we need to create a new fake object and write it back to the memory.
+        // Reuse an existing fake object or materialize a flat wrapper for all three payloads.
         // TODO: Think about the type constraint to get a consistent array resolution later
-        if (ref.isFakeObject()) {
-            ref
+        if (value.refValue.isFakeObject()) {
+            value.refValue
         } else {
-            val fakeObj = mkFakeValue(scope, bool, fp, ref)
+            val fakeObj = mkFakeValue(scope = scope, value = value)
             lValuesToAllocatedFakeObjects += refLValue to fakeObj
             memory.write(refLValue, fakeObj, guard = trueExpr)
             fakeObj
         }
     }
 }
+
+internal fun TsState.readSymbolicUnresolvedArrayElement(
+    array: UHeapRef,
+    index: UExpr<TsSizeSort>,
+): TsUnresolvedValue = with(ctx) {
+    check(array !is UConcreteHeapRef) { "A concrete unresolved array stores fake-value wrappers directly" }
+
+    val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1)
+    val boolLValue = mkArrayIndexLValue(boolSort, array, index, boolArrayType)
+    val boolValue = memory.read(boolLValue)
+
+    val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
+    val fpLValue = mkArrayIndexLValue(fp64Sort, array, index, numberArrayType)
+    val fpValue = memory.read(fpLValue)
+
+    val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+    val refLValue = mkArrayIndexLValue(addressSort, array, index, unknownArrayType)
+    val refValue = memory.read(refLValue)
+
+    TsUnresolvedValue(
+        boolValue = boolValue,
+        fpValue = fpValue,
+        refValue = refValue,
+    )
+}
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 0bf9f180b..cc8e915f6 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
@@ -96,6 +96,7 @@ class TsInterpreter(
     private val options: TsOptions,
     private val observer: TsInterpreterObserver? = null,
     private val unknownCallDispatcher: TsUnknownCallDispatcher,
+    private val throwExceptionOnStepFailure: Boolean = false,
 ) : UInterpreter<TsState>() {
 
     private val forkBlackList: UForkBlackList<TsState, EtsStmt> = UForkBlackList.createDefault()
@@ -146,6 +147,10 @@ class TsInterpreter(
                 }
             }
         } catch (e: Exception) {
+            if (throwExceptionOnStepFailure) {
+                throw e
+            }
+
             logger.error {
                 "Exception: $e\n${e.stackTrace.take(5).joinToString("\n") { "    $it" }}"
             }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt
index 151b5d911..a4b7c4e88 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsFakeType.kt
@@ -6,6 +6,22 @@ import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.machine.TsContext
 
+/**
+ * Type metadata for a synthetic wrapper representing a TypeScript value whose runtime kind is not known.
+ *
+ * The wrapper is identified by a special concrete heap reference, but that reference is only the wrapper's storage
+ * identity. It is not the object reference represented by the value. The possible boolean, number, and reference
+ * payloads are stored separately in the wrapper's intermediate fields.
+ *
+ * [boolTypeExpr], [fpTypeExpr], and [refTypeExpr] are symbolic discriminators. Exactly one of them must be true for
+ * every feasible state. Consumers should therefore keep the wrapper intact until the runtime kind is proven. In
+ * particular, using the reference payload requires constraining [refTypeExpr] and then extracting that payload;
+ * treating the wrapper reference itself as the payload or narrowing solely from a static TypeScript type is unsound.
+ *
+ * If narrowing establishes that the represented value is a particular object, the corresponding discriminator
+ * constraints must also be propagated to previously materialized fake values that may refer to the same object.
+ * Constraining only the extracted address breaks alias consistency.
+ */
 class EtsFakeType(
     val boolTypeExpr: UBoolExpr,
     val fpTypeExpr: UBoolExpr,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt
index 2dcd2bfb8..3c75494d9 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt
@@ -15,6 +15,24 @@ import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsState
 import org.usvm.memory.ULValue
 
+internal fun TsState.findMaterializedFakeValue(lValue: ULValue<*, *>): UConcreteHeapRef? =
+    lValuesToAllocatedFakeObjects.lastOrNull { (recordedLValue) -> recordedLValue == lValue }?.second
+
+/**
+ * Creates a fresh synthetic wrapper for a TypeScript value with a not necessarily known runtime kind.
+ *
+ * Non-null arguments initialize the corresponding boolean, number, and reference payload fields. When exactly one
+ * payload is supplied, the wrapper is constrained to that runtime kind. When multiple payloads are supplied, all
+ * three kind discriminators remain symbolic and [EtsFakeType.mkExactlyOneTypeConstraint] selects exactly one active
+ * representation. Callers that model a completely unknown value should therefore supply all three payloads.
+ *
+ * The returned concrete heap reference identifies the wrapper, not its reference payload. Consumers must preserve
+ * the wrapper or explicitly constrain the appropriate discriminator before extracting a payload.
+ *
+ * [scope] may be `null` only while constructing the initial state, before solver models exist. During symbolic
+ * execution a live scope is required so that adding the exactly-one constraint also checks satisfiability and updates
+ * the state's models.
+ */
 fun TsState.mkFakeValue(
     scope: TsStepScope?, // pass `null` only in the initial state, where `scope` is not available!
     boolValue: UBoolExpr? = null,
@@ -69,6 +87,16 @@ fun TsState.mkFakeValue(
     fakeValueRef
 }
 
+fun TsState.mkFakeValue(
+    scope: TsStepScope?,
+    value: TsUnresolvedValue,
+): UConcreteHeapRef = mkFakeValue(
+    scope = scope,
+    boolValue = value.boolValue,
+    fpValue = value.fpValue,
+    refValue = value.refValue,
+)
+
 fun <T : USort> TsState.extractValue(
     value: UExpr<out USort>,
     sort: T,
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt
new file mode 100644
index 000000000..7d7f7bb65
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsUnresolvedValue.kt
@@ -0,0 +1,13 @@
+package org.usvm.machine.types
+
+import io.ksmt.sort.KFp64Sort
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+
+/** The three backing payloads of a TypeScript value whose active runtime kind is not resolved yet. */
+data class TsUnresolvedValue(
+    val boolValue: UBoolExpr,
+    val fpValue: UExpr<KFp64Sort>,
+    val refValue: UHeapRef,
+)
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt
new file mode 100644
index 000000000..7b8bdd69a
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftIntrinsicModelTest.kt
@@ -0,0 +1,345 @@
+package org.usvm.machine.call
+
+import org.jacodb.ets.model.EtsArrayType
+import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsInstanceCallExpr
+import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.model.EtsUnknownType
+import org.jacodb.ets.utils.EtsIrProvider
+import org.jacodb.ets.utils.callExpr
+import org.jacodb.ets.utils.loadEtsFileAutoConvert
+import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
+import org.usvm.StateCollectionStrategy
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTestValue
+import org.usvm.api.makeSymbolicRefUntyped
+import org.usvm.machine.TsInterpreterObserver
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.state.TsState
+import org.usvm.util.TsTestResolver
+import org.usvm.util.getResourcePath
+import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+import kotlin.test.assertNotNull
+import kotlin.test.assertNull
+import kotlin.test.assertTrue
+import kotlin.time.Duration
+
+class TsArrayShiftIntrinsicModelTest {
+    private val sourceFile = loadEtsFileAutoConvert(
+        getResourcePath("/models/ArrayShiftIntrinsic.ts"),
+        provider = EtsIrProvider.TS_FRONTEND,
+    )
+    private val scene = EtsScene(listOf(sourceFile))
+
+    @Test
+    fun `empty array shift returns undefined through intrinsic model`() {
+        val result = analyze(methodName = "emptyArray")
+
+        assertIs<TsTestValue.TsUndefined>(result.values.single())
+        assertEquals(listOf("ts.array.shift"), result.modelIds)
+        assertTrue(assertNotNull(result.catalogFingerprint).matches(Regex("[0-9a-f]{64}")))
+    }
+
+    @Test
+    fun `non empty array shift returns first element moves tail and shrinks array`() {
+        val result = analyze(methodName = "nonEmptyArray")
+
+        assertEquals(32.0, assertIs<TsTestValue.TsNumber>(result.values.single()).number)
+        assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome })
+    }
+
+    @Test
+    fun `reference array preserves removed element alias and moves tail`() {
+        val result = analyze(methodName = "aliasedElement")
+
+        assertEquals(42.0, assertIs<TsTestValue.TsNumber>(result.values.single()).number)
+    }
+
+    @Test
+    fun `symbolic primitive array remains in the supported domain`() {
+        val result = analyze(methodName = "symbolicNumberArray")
+
+        assertTrue(result.values.isNotEmpty())
+        assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome })
+    }
+
+    @Test
+    fun `empty and non empty guards are complementary`() {
+        val state = analyzeStates(methodName = "unknownValue").single()
+        val symbolicArray = state.makeSymbolicRefUntyped()
+
+        val application = TsArrayShiftIntrinsicModel.apply(state, arrayShiftCall(symbolicArray))
+        val execution = assertNotNull(application)
+        val (emptyArray, nonEmptyArray) = execution.successors
+
+        assertEquals(2, execution.successors.size)
+        assertEquals(state.ctx.mkNot(emptyArray.guard), nonEmptyArray.guard)
+        assertNull(execution.residualGuard)
+    }
+
+    @Test
+    fun `symbolic unknown array preserves removed element and moves all value regions`() {
+        val result = analyze(methodName = "symbolicUnknownArray")
+        val reachesExpectedResult = result.values.any { value ->
+            (value as? TsTestValue.TsNumber)?.number == 47.0
+        }
+
+        assertTrue(reachesExpectedResult)
+        assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome })
+    }
+
+    @Test
+    fun `symbolic unknown array copies boolean number and address regions`() {
+        val state = analyzeStates(methodName = "unknownValue").single()
+        val symbolicArray = state.makeSymbolicRefUntyped()
+
+        with(state.ctx) {
+            val zero = mkBv(0)
+            val one = mkBv(1)
+            val boolValue = trueExpr
+            val fpValue = mkFp64(17.0)
+            val refValue = state.makeSymbolicRefUntyped()
+
+            val boolArrayType = EtsArrayType(EtsBooleanType, dimensions = 1)
+            val numberArrayType = EtsArrayType(EtsNumberType, dimensions = 1)
+            val unknownArrayType = EtsArrayType(EtsUnknownType, dimensions = 1)
+
+            val lengthLValue = mkArrayLengthLValue(symbolicArray, unknownArrayType)
+            state.memory.write(lengthLValue, mkBv(2), guard = trueExpr)
+            state.memory.write(
+                mkArrayIndexLValue(boolSort, symbolicArray, one, boolArrayType),
+                boolValue,
+                guard = trueExpr,
+            )
+            state.memory.write(
+                mkArrayIndexLValue(fp64Sort, symbolicArray, one, numberArrayType),
+                fpValue,
+                guard = trueExpr,
+            )
+            state.memory.write(
+                mkArrayIndexLValue(addressSort, symbolicArray, one, unknownArrayType),
+                refValue,
+                guard = trueExpr,
+            )
+
+            val execution = assertNotNull(
+                TsArrayShiftIntrinsicModel.apply(
+                    state,
+                    arrayShiftCall(symbolicArray, methodName = "symbolicUnknownArray"),
+                )
+            )
+            val nonEmptySuccessor = execution.successors.last()
+            assertIs<TsUnknownCallModelCompletion.Unresolved>(nonEmptySuccessor.completion)
+
+            nonEmptySuccessor.applyStateChanges(state)
+
+            val shiftedBoolValue = state.memory.read(
+                mkArrayIndexLValue(boolSort, symbolicArray, zero, boolArrayType)
+            )
+            val shiftedFpValue = state.memory.read(
+                mkArrayIndexLValue(fp64Sort, symbolicArray, zero, numberArrayType)
+            )
+            val shiftedRefValue = state.memory.read(
+                mkArrayIndexLValue(addressSort, symbolicArray, zero, unknownArrayType)
+            )
+
+            assertEquals(boolValue, shiftedBoolValue)
+            assertEquals(fpValue, shiftedFpValue)
+            assertEquals(refValue, shiftedRefValue)
+            assertEquals(one, state.memory.read(lengthLValue))
+        }
+    }
+
+    @Test
+    fun `concrete unknown array shifts fake wrapped values`() {
+        val result = analyze(methodName = "mixedUnknownArray")
+
+        assertEquals(49.0, assertIs<TsTestValue.TsNumber>(result.values.single()).number)
+        assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome })
+    }
+
+    @Test
+    fun `empty concrete unknown array returns undefined`() {
+        val result = analyze(methodName = "emptyUnknownArray")
+
+        assertIs<TsTestValue.TsUndefined>(result.values.single())
+        assertEquals(listOf(TsUnknownCallOutcome.MODEL_APPLIED), result.events.map { it.outcome })
+    }
+
+    @Test
+    fun `array shift with arguments uses residual fallback`() {
+        assertUsesResidualFallback(methodName = "shiftWithArguments")
+    }
+
+    @Test
+    fun `fake wrapper receiver is not accepted as an array`() {
+        val state = analyzeStates(methodName = "unknownValue").single()
+        val fakeReceiver = makeFakeReceiver(state)
+
+        val execution = TsArrayShiftIntrinsicModel.apply(state, arrayShiftCall(fakeReceiver))
+
+        assertNull(execution)
+    }
+
+    @Test
+    fun `conditional receiver containing fake wrapper is not accepted as an array`() {
+        val state = analyzeStates(methodName = "unknownValue").single()
+        val fakeReceiver = makeFakeReceiver(state)
+        val fakeType = with(state.ctx) { fakeReceiver.getFakeType(state.memory) }
+        val conditionalReceiver = state.ctx.mkIte(
+            condition = fakeType.boolTypeExpr,
+            trueBranch = fakeReceiver,
+            falseBranch = state.makeSymbolicRefUntyped(),
+        )
+
+        val execution = TsArrayShiftIntrinsicModel.apply(state, arrayShiftCall(conditionalReceiver))
+
+        assertNull(execution)
+    }
+
+    @Test
+    fun `empty enabled set sends shift to configured fallback`() {
+        val disabledResult = analyze(
+            methodName = "nonEmptyArray",
+            tsOptions = TsOptions(
+                enabledUnknownCallModelIds = emptySet(),
+                unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+            ),
+        )
+
+        assertEquals(listOf(TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN), disabledResult.events.map { it.outcome })
+    }
+
+    @Test
+    fun `compatibility dispatcher keeps the legacy shift approximation`() {
+        val result = analyze(
+            methodName = "nonEmptyArray",
+            dispatcher = TsCompatibilityUnknownCallDispatcher,
+        )
+
+        assertEquals(32.0, assertIs<TsTestValue.TsNumber>(result.values.single()).number)
+        assertTrue(result.events.isEmpty())
+        assertNull(result.catalogFingerprint)
+    }
+
+    private fun analyze(
+        methodName: String,
+        tsOptions: TsOptions = TsOptions(),
+        dispatcher: TsUnknownCallDispatcher? = null,
+    ): AnalysisResult {
+        val method = method(methodName)
+        val observer = RecordingUnknownCallObserver()
+
+        return TsMachine(
+            scene = scene,
+            options = machineOptions,
+            tsOptions = tsOptions,
+            observer = observer,
+            unknownCallDispatcher = dispatcher,
+        ).use { machine ->
+            val states = machine.analyze(listOf(method))
+            val values = states.map { state -> TsTestResolver().resolve(method, state).returnValue }
+
+            AnalysisResult(
+                values = values,
+                events = observer.events.toList(),
+                catalogFingerprint = machine.unknownCallModelCatalogFingerprint,
+            )
+        }
+    }
+
+    private fun assertUsesResidualFallback(methodName: String) {
+        val result = analyze(methodName)
+
+        assertTrue(result.values.isEmpty())
+        assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.single().outcome)
+    }
+
+    private fun makeFakeReceiver(state: TsState): UConcreteHeapRef {
+        val result = assertIs<TsMethodResult.Success>(state.methodResult).value
+        val fakeReceiver = assertIs<UConcreteHeapRef>(result)
+
+        assertTrue(with(state.ctx) { fakeReceiver.isFakeObject() })
+        return fakeReceiver
+    }
+
+    private fun arrayShiftCall(
+        resolvedReceiver: UExpr<*>,
+        methodName: String = "nonEmptyArray",
+    ): TsUnknownCall {
+        val callSite = method(methodName).cfg.stmts.single { stmt ->
+            stmt.callExpr?.callee?.name == "shift"
+        }
+        val sourceCall = assertIs<EtsInstanceCallExpr>(assertNotNull(callSite.callExpr))
+
+        return TsUnknownCall(
+            callee = sourceCall.callee,
+            receiver = TsUnknownCallValue(source = sourceCall.instance, resolved = resolvedReceiver),
+            arguments = emptyList(),
+            resultType = sourceCall.type,
+            callSite = callSite,
+            failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION,
+        )
+    }
+
+    private fun analyzeStates(methodName: String): List<TsState> {
+        val method = method(methodName)
+
+        return TsMachine(
+            scene = scene,
+            options = machineOptions,
+            tsOptions = TsOptions(),
+        ).use { machine ->
+            machine.analyze(listOf(method))
+        }
+    }
+
+    private fun method(name: String): EtsMethod = scene.projectClasses
+        .single { it.name == "ArrayShiftIntrinsic" }
+        .methods
+        .single { it.name == name }
+
+    private class RecordingUnknownCallObserver : TsInterpreterObserver {
+        val events = mutableListOf<TsUnknownCallEvent>()
+
+        override fun onUnknownCall(event: TsUnknownCallEvent) {
+            events += event
+        }
+    }
+
+    private data class AnalysisResult(
+        val values: List<TsTestValue>,
+        val events: List<TsUnknownCallEvent>,
+        val catalogFingerprint: String?,
+    ) {
+        val modelIds: List<String>
+            get() = events.mapNotNull { event ->
+                (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId
+            }
+    }
+
+    private companion object {
+        val machineOptions = UMachineOptions(
+            pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+            stateCollectionStrategy = StateCollectionStrategy.ALL,
+            exceptionsPropagation = true,
+            timeout = Duration.INFINITE,
+            stepsFromLastCovered = 3_500L,
+            solverType = SolverType.YICES,
+            solverTimeout = Duration.INFINITE,
+            typeOperationsTimeout = Duration.INFINITE,
+        )
+    }
+}
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 5233e5280..81ae7a03b 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
@@ -1,6 +1,7 @@
 package org.usvm.machine.call
 
 import io.ksmt.utils.asExpr
+import io.mockk.mockk
 import org.jacodb.ets.model.EtsFile
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
@@ -9,6 +10,8 @@ import org.jacodb.ets.model.EtsPtrCallExpr
 import org.jacodb.ets.model.EtsReturnStmt
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStmt
+import org.jacodb.ets.model.EtsStringType
+import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsVoidType
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.callExpr
@@ -18,17 +21,18 @@ import org.usvm.PathSelectionStrategy
 import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
 import org.usvm.UMachineOptions
-import org.usvm.api.mockMethodCall
 import org.usvm.api.targets.ReachabilityObserver
 import org.usvm.api.targets.TsReachabilityTarget
+import org.usvm.isTrue
 import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
-import org.usvm.machine.state.newStmt
+import org.usvm.solver.USatResult
 import org.usvm.util.getResourcePath
 import kotlin.test.assertEquals
 import kotlin.test.assertFailsWith
@@ -47,31 +51,25 @@ class TsUnknownCallDispatcherTest {
     private val fullScene = EtsScene(listOf(sourceFile))
 
     @Test
-    fun `every profile decision is reported through the interpreter observer`() {
+    fun `every model or fallback decision is reported through the interpreter observer`() {
         val cases = listOf(
             ObservationCase(
-                profile = TsUnknownCallProfiles.MODELS_THEN_STOP,
-                modelProvider = TsNoUnknownCallModels,
+                fallback = TsResidualCallPolicy.STOP_PATH,
+                models = noModels,
                 outcome = TsUnknownCallOutcome.PATH_STOPPED,
-                decision = TsUnknownCallDecision.ResidualFallback(
-                    policy = TsResidualCallPolicy.STOP_PATH,
-                    reason = TsUnknownCallResidualReason.MODEL_NOT_APPLICABLE,
-                ),
+                decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.STOP_PATH),
                 finalStateCount = 0,
             ),
             ObservationCase(
-                profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL,
-                modelProvider = TsNoUnknownCallModels,
+                fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+                models = noModels,
                 outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN,
-                decision = TsUnknownCallDecision.ResidualFallback(
-                    policy = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
-                    reason = TsUnknownCallResidualReason.MODEL_LOOKUP_DISABLED,
-                ),
+                decision = TsUnknownCallDecision.ResidualFallback(TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN),
                 finalStateCount = 1,
             ),
             ObservationCase(
-                profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC,
-                modelProvider = ApplyingModelProvider,
+                fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+                models = catalog(ApplyingModel),
                 outcome = TsUnknownCallOutcome.MODEL_APPLIED,
                 decision = TsUnknownCallDecision.ModelApplied(modelId = "applying-model"),
                 finalStateCount = 1,
@@ -82,17 +80,16 @@ class TsUnknownCallDispatcherTest {
             val observer = RecordingUnknownCallObserver()
             val states = analyzeAllStates(
                 methodName = "declaredMethodWithoutBodyContinues",
-                profile = case.profile,
-                modelProvider = case.modelProvider,
+                fallback = case.fallback,
+                models = case.models,
                 observer = observer,
             )
 
-            assertEquals(case.finalStateCount, states.size, case.profile.toString())
+            assertEquals(case.finalStateCount, states.size, case.fallback.toString())
             val event = observer.events.single()
             assertEquals("declaredMethodWithoutBodyContinues", event.callSite.location.method.name)
             assertEquals("external", event.callee.name)
             assertEquals(TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, event.failureReason)
-            assertEquals(case.profile, event.profile)
             assertEquals(case.outcome, event.outcome)
             assertEquals(case.decision, event.decision)
         }
@@ -103,8 +100,7 @@ class TsUnknownCallDispatcherTest {
         val observer = RecordingUnknownCallObserver()
         val states = analyzeAllStates(
             methodName = "modeledUnknownCallForks",
-            profile = TsUnknownCallProfiles.MODELS_THEN_STOP,
-            modelProvider = ForkingModelProvider,
+            models = catalog(ForkingModel),
             observer = observer,
         )
 
@@ -117,13 +113,13 @@ class TsUnknownCallDispatcherTest {
     fun `throwing observer cannot change fresh or modeled exploration`() {
         val cases = listOf(
             ObservationFailureCase(
-                profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL,
-                modelProvider = TsNoUnknownCallModels,
+                fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+                models = noModels,
                 expectedFinalStateCount = 1,
             ),
             ObservationFailureCase(
-                profile = TsUnknownCallProfiles.MODELS_THEN_STOP,
-                modelProvider = ForkingModelProvider,
+                fallback = TsResidualCallPolicy.STOP_PATH,
+                models = catalog(ForkingModel),
                 expectedFinalStateCount = 2,
                 methodName = "modeledUnknownCallForks",
             ),
@@ -132,19 +128,22 @@ class TsUnknownCallDispatcherTest {
         cases.forEach { case ->
             val states = analyzeAllStates(
                 methodName = case.methodName,
-                profile = case.profile,
-                modelProvider = case.modelProvider,
+                fallback = case.fallback,
+                models = case.models,
                 observer = ThrowingUnknownCallObserver,
             )
 
-            assertEquals(case.expectedFinalStateCount, states.size, case.profile.toString())
+            assertEquals(case.expectedFinalStateCount, states.size, case.fallback.toString())
         }
     }
 
     @Test
     fun `applied model decisions require non blank identifiers`() {
         assertFailsWith<IllegalArgumentException> {
-            TsUnknownCallModelApplication.Applied(modelId = " ")
+            TsUnknownCallModelApplication.Applied(
+                modelId = " ",
+                execution = completeExecution(),
+            )
         }
         assertFailsWith<IllegalArgumentException> {
             TsUnknownCallDecision.ModelApplied(modelId = "")
@@ -152,93 +151,102 @@ class TsUnknownCallDispatcherTest {
     }
 
     @Test
-    fun `profiles select model lookup independently from residual fallback`() {
-        val cases = listOf(
-            ProfileCase(
-                profile = TsUnknownCallProfiles.STOP_ALL,
-                withoutModel = ProfileResult(
-                    reachesReturn = false,
-                    outcome = TsUnknownCallOutcome.PATH_STOPPED,
-                ),
-                withModel = ProfileResult(
-                    reachesReturn = false,
-                    outcome = TsUnknownCallOutcome.PATH_STOPPED,
-                ),
-            ),
-            ProfileCase(
-                profile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL,
-                withoutModel = ProfileResult(
-                    reachesReturn = true,
-                    outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN,
-                ),
-                withModel = ProfileResult(
-                    reachesReturn = true,
-                    outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN,
-                ),
-            ),
-            ProfileCase(
-                profile = TsUnknownCallProfiles.MODELS_THEN_STOP,
-                withoutModel = ProfileResult(
-                    reachesReturn = false,
-                    outcome = TsUnknownCallOutcome.PATH_STOPPED,
-                ),
-                withModel = ProfileResult(
-                    reachesReturn = true,
-                    outcome = TsUnknownCallOutcome.MODEL_APPLIED,
-                ),
-            ),
-            ProfileCase(
-                profile = TsUnknownCallProfiles.MODELS_THEN_FRESH_SYMBOLIC,
-                withoutModel = ProfileResult(
-                    reachesReturn = true,
-                    outcome = TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN,
-                ),
-                withModel = ProfileResult(
-                    reachesReturn = true,
-                    outcome = TsUnknownCallOutcome.MODEL_APPLIED,
-                ),
-            ),
+    fun `model execution plans require at least one successor`() {
+        val error = assertFailsWith<IllegalArgumentException> {
+            TsUnknownCallModelExecution(
+                successors = emptyList(),
+                residualGuard = mockk(),
+            )
+        }
+
+        assertEquals("A semantic model must declare at least one guarded successor", error.message)
+    }
+
+    @Test
+    fun `fresh fallback preserves all fake value representations`() {
+        assertFreshResultPreservesAllFakeRepresentations(
+            fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
         )
+    }
 
-        cases.forEach { case ->
-            assertEquals(case.withoutModel, runProfile(case.profile, TsNoUnknownCallModels), case.profile.toString())
-            assertEquals(case.withModel, runProfile(case.profile, ApplyingModelProvider), case.profile.toString())
-        }
+    @Test
+    fun `partial residual fallback preserves all fake value representations`() {
+        assertFreshResultPreservesAllFakeRepresentations(
+            fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+            models = catalog(UnsupportedPartialModel),
+        )
+    }
+
+    @Test
+    fun `partial model sends only residual domain to fresh fallback`() {
+        val observer = RecordingUnknownCallObserver()
+        val states = analyzeAllStates(
+            methodName = "modeledUnknownCallForks",
+            fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
+            models = catalog(SupportedTrueResidualFalseModel),
+            observer = observer,
+        )
+
+        assertEquals(2, states.size)
+        assertEquals(
+            listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.FRESH_SYMBOLIC_RETURN),
+            observer.events.map { it.outcome },
+        )
     }
 
     @Test
-    fun `TsOptions profile configures the machine dispatcher`() {
-        assertEquals(TsUnknownCallProfiles.MODELS_THEN_STOP, TsOptions().unknownCallProfile)
-        assertTrue(TsOptions().unknownCallProfile.residualOverrides.isEmpty())
+    fun `partial model sends residual domain to stop fallback`() {
+        val observer = RecordingUnknownCallObserver()
+        val states = analyzeAllStates(
+            methodName = "modeledUnknownCallForks",
+            models = catalog(SupportedTrueResidualFalseModel),
+            observer = observer,
+        )
 
-        assertFalse(reachesReturn("declaredMethodWithoutBodyContinues"))
-        assertTrue(
-            reachesReturn(
-                "declaredMethodWithoutBodyContinues",
-                tsOptions = TsOptions(unknownCallProfile = TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL),
-            )
+        assertEquals(1, states.size)
+        assertEquals(
+            listOf(TsUnknownCallOutcome.MODEL_APPLIED, TsUnknownCallOutcome.PATH_STOPPED),
+            observer.events.map { it.outcome },
         )
     }
 
     @Test
-    fun `explicit family override replaces the profile residual fallback`() {
-        val family = method(fullScene, "declaredMethodWithoutBodyContinues")
+    fun `exceptional model successor preserves exception state`() {
+        val states = analyzeAllStates(
+            methodName = "modeledUnknownCallThrows",
+            models = catalog(ExceptionalModel),
+        )
+
+        assertIs<TsMethodResult.TsException>(states.single().methodResult)
+    }
+
+    @Test
+    fun `stateful model can return an existing reference alias`() {
+        val states = analyzeAllStates(
+            methodName = "modeledUnknownCallReturnsAlias",
+            models = catalog(StatefulAliasModel),
+        )
+        val aliasReturn = method(fullScene, "modeledUnknownCallReturnsAlias")
             .cfg
             .stmts
-            .mapNotNull { it.callExpr }
-            .single { it.callee.name == "external" }
-            .callee
-            .enclosingClass
-        val profile = TsUnknownCallProfiles.STOP_ALL.copy(
-            residualOverrides = mapOf(
-                family to TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
-            )
-        )
+            .filterIsInstance<EtsReturnStmt>()
+            .first()
+
+        val state = states.single()
+        assertTrue(aliasReturn in state.pathNode.allStatements)
+        assertTrue(STATE_CHANGE_MARKER in state.addedArtificialLocals)
+    }
+
+    @Test
+    fun `TsOptions configures one fallback without profiles`() {
+        assertEquals(TsResidualCallPolicy.STOP_PATH, TsOptions().unknownCallFallback)
+        assertNull(TsOptions().enabledUnknownCallModelIds)
 
+        assertFalse(reachesReturn("declaredMethodWithoutBodyContinues"))
         assertTrue(
             reachesReturn(
                 "declaredMethodWithoutBodyContinues",
-                tsOptions = TsOptions(unknownCallProfile = profile),
+                tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN),
             )
         )
     }
@@ -246,9 +254,9 @@ class TsUnknownCallDispatcherTest {
     @Test
     fun `fresh symbolic return uses the source call result type`() {
         val dispatcher = RecordingResultSortDispatcher(
-            TsProfileUnknownCallDispatcher(
-                TsUnknownCallProfiles.FRESH_SYMBOLIC_FOR_ALL,
-                TsNoUnknownCallModels,
+            TsModelUnknownCallDispatcher(
+                models = noModels,
+                fallback = TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN,
             )
         )
 
@@ -354,7 +362,7 @@ class TsUnknownCallDispatcherTest {
     }
 
     @Test
-    fun `descriptor keeps typed call data without eagerly resolving arguments`() {
+    fun `unknown call keeps typed data without eagerly resolving arguments`() {
         val dispatcher = RecordingUnknownCallDispatcher()
         val scene = sceneWithout("ExternalStatic")
 
@@ -369,7 +377,7 @@ class TsUnknownCallDispatcherTest {
     }
 
     @Test
-    fun `descriptor preserves source and resolved values available at dispatch`() {
+    fun `unknown call preserves source and resolved values available at dispatch`() {
         val dispatcher = RecordingUnknownCallDispatcher()
 
         assertFalse(reachesReturn("nonReferenceInstanceCallPrunes", dispatcher = dispatcher))
@@ -410,7 +418,7 @@ class TsUnknownCallDispatcherTest {
     }
 
     @Test
-    fun `pointer descriptor pairs its source with the resolved function pointer`() {
+    fun `pointer call pairs its source with the resolved function pointer`() {
         val dispatcher = RecordingUnknownCallDispatcher()
         val pointerCall = method(fullScene, "associatedLoggingPointerContinues", className = "Log")
             .cfg
@@ -434,7 +442,7 @@ class TsUnknownCallDispatcherTest {
     }
 
     @Test
-    fun `descriptor result type comes from the source overload`() {
+    fun `unknown call result type comes from the source overload`() {
         val dispatcher = RecordingUnknownCallDispatcher()
 
         assertTrue(reachesReturn("overloadedDeclaredMethodWithoutBodyContinues", dispatcher = dispatcher))
@@ -452,17 +460,17 @@ class TsUnknownCallDispatcherTest {
         scene: EtsScene = fullScene,
         tsOptions: TsOptions = TsOptions(),
         dispatcher: TsUnknownCallDispatcher? = null,
-        modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels,
+        models: TsUnknownCallModelCatalog = noModels,
         className: String = "CallFallbackBaseline",
     ): Boolean = returnStatement(scene, methodName, className) in
-        reachedStatements(methodName, scene, tsOptions, dispatcher, modelProvider, className)
+        reachedStatements(methodName, scene, tsOptions, dispatcher, models, className)
 
     private fun reachedStatements(
         methodName: String,
         scene: EtsScene,
         tsOptions: TsOptions,
         dispatcher: TsUnknownCallDispatcher?,
-        modelProvider: TsUnknownCallModelProvider,
+        models: TsUnknownCallModelCatalog,
         className: String,
     ): Set<EtsStmt> {
         val method = method(scene, methodName, className)
@@ -476,7 +484,7 @@ class TsUnknownCallDispatcherTest {
             tsOptions = tsOptions,
             machineObserver = ReachabilityObserver(),
             unknownCallDispatcher = dispatcher,
-            unknownCallModelProvider = modelProvider,
+            unknownCallModels = models,
         ).use { machine ->
             machine.analyze(listOf(method), listOf(initialTarget))
                 .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements }
@@ -508,22 +516,60 @@ class TsUnknownCallDispatcherTest {
 
     private fun analyzeAllStates(
         methodName: String,
-        profile: TsUnknownCallProfile,
-        modelProvider: TsUnknownCallModelProvider = TsNoUnknownCallModels,
+        fallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH,
+        models: TsUnknownCallModelCatalog = noModels,
         observer: TsInterpreterObserver? = null,
     ): List<TsState> {
         val method = method(fullScene, methodName)
         return TsMachine(
             scene = fullScene,
             options = allStatesMachineOptions,
-            tsOptions = TsOptions(unknownCallProfile = profile),
+            tsOptions = TsOptions(unknownCallFallback = fallback),
             observer = observer,
-            unknownCallModelProvider = modelProvider,
+            unknownCallModels = models,
         ).use { machine ->
             machine.analyze(listOf(method))
         }
     }
 
+    private fun assertFreshResultPreservesAllFakeRepresentations(
+        fallback: TsResidualCallPolicy,
+        models: TsUnknownCallModelCatalog = noModels,
+    ) {
+        val method = method(fullScene, "freshUnknownCallResult")
+        TsMachine(
+            scene = fullScene,
+            options = allStatesMachineOptions,
+            tsOptions = TsOptions(unknownCallFallback = fallback),
+            unknownCallModels = models,
+        ).use { machine ->
+            val state = machine.analyze(listOf(method)).single()
+            val result = assertIs<TsMethodResult.Success>(state.methodResult).value
+            val fakeValue = assertIs<UConcreteHeapRef>(result)
+            val fakeType = with(state.ctx) {
+                assertTrue(fakeValue.isFakeObject())
+                fakeValue.getFakeType(state.memory)
+            }
+            val discriminators = mapOf(
+                "boolean" to fakeType.boolTypeExpr,
+                "number" to fakeType.fpTypeExpr,
+                "reference" to fakeType.refTypeExpr,
+            )
+
+            discriminators.forEach { (kind, discriminator) ->
+                val constraints = state.pathConstraints.clone()
+                constraints += discriminator
+                val solverResult = state.ctx.solver<EtsType>().check(constraints)
+
+                assertIs<USatResult<*>>(solverResult, "Fresh fake result lost its $kind representation")
+            }
+
+            val exactlyOneType = fakeType.mkExactlyOneTypeConstraint(state.ctx)
+            assertTrue(state.models.isNotEmpty())
+            assertTrue(state.models.all { model -> model.eval(exactlyOneType).isTrue })
+        }
+    }
+
     private class RecordingUnknownCallDispatcher : TsUnknownCallDispatcher {
         val calls = mutableListOf<TsUnknownCall>()
         val receiverIsAssociatedFunction = mutableListOf<Boolean?>()
@@ -538,27 +584,6 @@ class TsUnknownCallDispatcherTest {
         }
     }
 
-    private fun runProfile(
-        profile: TsUnknownCallProfile,
-        modelProvider: TsUnknownCallModelProvider,
-    ): ProfileResult {
-        val dispatcher = RecordingOutcomeDispatcher(TsProfileUnknownCallDispatcher(profile, modelProvider))
-        val reachesReturn = reachesReturn(
-            "declaredMethodWithoutBodyContinues",
-            dispatcher = dispatcher,
-        )
-        return ProfileResult(reachesReturn, dispatcher.outcomes.single())
-    }
-
-    private class RecordingOutcomeDispatcher(
-        private val delegate: TsUnknownCallDispatcher,
-    ) : TsUnknownCallDispatcher {
-        val outcomes = mutableListOf<TsUnknownCallOutcome>()
-
-        override fun dispatch(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallOutcome =
-            delegate.dispatch(scope, call).also(outcomes::add)
-    }
-
     private class RecordingResultSortDispatcher(
         private val delegate: TsUnknownCallDispatcher,
     ) : TsUnknownCallDispatcher {
@@ -576,31 +601,101 @@ class TsUnknownCallDispatcherTest {
         }
     }
 
-    private object ApplyingModelProvider : TsUnknownCallModelProvider {
-        override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication {
-            mockMethodCall(scope, call.callee, call.resultType)
-            scope.doWithState { newStmt(call.callSite) }
-            return TsUnknownCallModelApplication.Applied(modelId = "applying-model")
+    private object ApplyingModel : TestModel(id = "applying-model", methodName = "external") {
+        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution {
+            val successor = TsUnknownCallModelSuccessor(
+                guard = state.ctx.trueExpr,
+                completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() },
+            )
+
+            return TsUnknownCallModelExecution(successors = listOf(successor))
         }
     }
 
-    private object ForkingModelProvider : TsUnknownCallModelProvider {
-        override fun apply(scope: TsStepScope, call: TsUnknownCall): TsUnknownCallModelApplication {
+    private object ForkingModel : TestModel(id = "forking-model", methodName = "convert") {
+        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution {
             val result = requireNotNull(call.arguments.single().resolved)
-            val condition = scope.calcOnState { result.asExpr(ctx.boolSort) }
-            val completeCall: TsState.() -> Unit = {
-                methodResult = TsMethodResult.Success.MockedCall(result, call.callee)
-                newStmt(call.callSite)
-            }
-            scope.fork(
-                condition = condition,
-                blockOnTrueState = completeCall,
-                blockOnFalseState = completeCall,
+            val condition = result.asExpr(state.ctx.boolSort)
+            val completion = TsUnknownCallModelCompletion.Normal { result }
+
+            return TsUnknownCallModelExecution(
+                successors = listOf(
+                    TsUnknownCallModelSuccessor(
+                        guard = condition,
+                        completion = completion,
+                    ),
+                    TsUnknownCallModelSuccessor(
+                        guard = state.ctx.mkNot(condition),
+                        completion = completion,
+                    ),
+                ),
+            )
+        }
+    }
+
+    private object SupportedTrueResidualFalseModel : TestModel(id = "partial-model", methodName = "convert") {
+        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution {
+            val result = requireNotNull(call.arguments.single().resolved)
+            val condition = result.asExpr(state.ctx.boolSort)
+            val successor = TsUnknownCallModelSuccessor(
+                guard = condition,
+                completion = TsUnknownCallModelCompletion.Normal { result },
+            )
+
+            return TsUnknownCallModelExecution(
+                successors = listOf(successor),
+                residualGuard = state.ctx.mkNot(condition),
             )
-            return TsUnknownCallModelApplication.Applied(modelId = "forking-model")
         }
     }
 
+    private object ExceptionalModel : TestModel(id = "exceptional-model", methodName = "fail") {
+        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution {
+            val successor = TsUnknownCallModelSuccessor(
+                guard = state.ctx.trueExpr,
+                completion = TsUnknownCallModelCompletion.Exceptional {
+                    ctx.mkUndefinedValue() to EtsStringType
+                },
+            )
+
+            return TsUnknownCallModelExecution(successors = listOf(successor))
+        }
+    }
+
+    private object UnsupportedPartialModel : TestModel(id = "unsupported-partial-model", methodName = "value") {
+        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution {
+            val successor = TsUnknownCallModelSuccessor(
+                guard = state.ctx.falseExpr,
+                completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() },
+            )
+
+            return TsUnknownCallModelExecution(
+                successors = listOf(successor),
+                residualGuard = state.ctx.trueExpr,
+            )
+        }
+    }
+
+    private object StatefulAliasModel : TestModel(id = "stateful-alias-model", methodName = "identity") {
+        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution {
+            val argument = requireNotNull(call.arguments.single().resolved)
+            val successor = TsUnknownCallModelSuccessor(
+                guard = state.ctx.trueExpr,
+                completion = TsUnknownCallModelCompletion.Normal { argument },
+                applyStateChanges = { addedArtificialLocals += STATE_CHANGE_MARKER },
+            )
+
+            return TsUnknownCallModelExecution(successors = listOf(successor))
+        }
+    }
+
+    private abstract class TestModel(
+        override val id: String,
+        methodName: String,
+    ) : TsUnknownCallModel {
+        override val target = TsUnknownCallTarget(methodName = methodName)
+    }
+
     private class RecordingUnknownCallObserver : TsInterpreterObserver {
         val events = mutableListOf<TsUnknownCallEvent>()
 
@@ -615,28 +710,17 @@ class TsUnknownCallDispatcherTest {
         }
     }
 
-    private data class ProfileCase(
-        val profile: TsUnknownCallProfile,
-        val withoutModel: ProfileResult,
-        val withModel: ProfileResult,
-    )
-
-    private data class ProfileResult(
-        val reachesReturn: Boolean,
-        val outcome: TsUnknownCallOutcome,
-    )
-
     private data class ObservationCase(
-        val profile: TsUnknownCallProfile,
-        val modelProvider: TsUnknownCallModelProvider,
+        val fallback: TsResidualCallPolicy,
+        val models: TsUnknownCallModelCatalog,
         val outcome: TsUnknownCallOutcome,
         val decision: TsUnknownCallDecision,
         val finalStateCount: Int,
     )
 
     private data class ObservationFailureCase(
-        val profile: TsUnknownCallProfile,
-        val modelProvider: TsUnknownCallModelProvider,
+        val fallback: TsResidualCallPolicy,
+        val models: TsUnknownCallModelCatalog,
         val expectedFinalStateCount: Int,
         val methodName: String = "declaredMethodWithoutBodyContinues",
     )
@@ -658,6 +742,23 @@ class TsUnknownCallDispatcherTest {
     }
 
     private companion object {
+        const val STATE_CHANGE_MARKER = "semantic-model-state-change"
+
+        val noModels = TsUnknownCallModelCatalog(emptyList())
+
+        fun catalog(vararg models: TsUnknownCallModel): TsUnknownCallModelCatalog =
+            TsUnknownCallModelCatalog(models.toList())
+
+        fun completeExecution(): TsUnknownCallModelExecution =
+            TsUnknownCallModelExecution(
+                successors = listOf(
+                    TsUnknownCallModelSuccessor(
+                        guard = mockk(),
+                        completion = TsUnknownCallModelCompletion.Normal { mockk<UExpr<*>>() },
+                    ),
+                ),
+            )
+
         val machineOptions = UMachineOptions(
             pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
             exceptionsPropagation = true,
diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt
new file mode 100644
index 000000000..cde61a23c
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt
@@ -0,0 +1,118 @@
+package org.usvm.machine.call
+
+import org.usvm.machine.state.TsState
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertFailsWith
+import kotlin.test.assertNotEquals
+import kotlin.test.assertTrue
+
+class TsUnknownCallModelCatalogTest {
+    @Test
+    fun `model IDs and target names must be non blank`() {
+        assertFailsWith<IllegalArgumentException> {
+            TsUnknownCallModelCatalog(listOf(model(id = " ")))
+        }
+        assertFailsWith<IllegalArgumentException> {
+            TsUnknownCallTarget(methodName = " ")
+        }
+        assertFailsWith<IllegalArgumentException> {
+            TsUnknownCallTarget(methodName = "method", enclosingClassName = " ")
+        }
+    }
+
+    @Test
+    fun `duplicate IDs are rejected`() {
+        val error = assertFailsWith<IllegalArgumentException> {
+            TsUnknownCallModelCatalog(
+                models = listOf(
+                    model(id = "duplicate", methodName = "first"),
+                    model(id = "duplicate", methodName = "second"),
+                )
+            )
+        }
+
+        assertEquals("Duplicate semantic model IDs: duplicate", error.message)
+    }
+
+    @Test
+    fun `overlapping declarative targets are rejected before execution`() {
+        val error = assertFailsWith<IllegalStateException> {
+            TsUnknownCallModelCatalog(
+                models = listOf(
+                    model(id = "z-model", methodName = "target"),
+                    model(
+                        id = "a-model",
+                        methodName = "target",
+                        failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE,
+                    ),
+                )
+            )
+        }
+
+        assertEquals("Ambiguous semantic model targets: a-model, z-model", error.message)
+    }
+
+    @Test
+    fun `unknown enabled IDs are rejected`() {
+        val error = assertFailsWith<IllegalArgumentException> {
+            TsUnknownCallModelCatalog(
+                models = listOf(model(id = "known")),
+                enabledModelIds = setOf("missing"),
+            )
+        }
+
+        assertEquals("Unknown semantic model IDs: missing", error.message)
+    }
+
+    @Test
+    fun `selection and fingerprint do not depend on model order`() {
+        val forward = listOf(
+            model(id = "a", methodName = "first"),
+            model(id = "b", methodName = "second"),
+        )
+
+        val first = TsUnknownCallModelCatalog(forward)
+        val second = TsUnknownCallModelCatalog(forward.reversed())
+
+        assertEquals(listOf("a", "b"), first.modelIds)
+        assertEquals(first.modelIds, second.modelIds)
+        assertEquals(first.fingerprint, second.fingerprint)
+    }
+
+    @Test
+    fun `enabled subset is detached and changes fingerprint`() {
+        val mutableIds = mutableSetOf("a")
+        val models = listOf(
+            model(id = "a", methodName = "first"),
+            model(id = "b", methodName = "second"),
+        )
+        val onlyA = TsUnknownCallModelCatalog(models, enabledModelIds = mutableIds)
+        mutableIds += "b"
+        val both = TsUnknownCallModelCatalog(models)
+
+        assertEquals(listOf("a"), onlyA.modelIds)
+        assertNotEquals(onlyA.fingerprint, both.fingerprint)
+        assertTrue(onlyA.fingerprint.matches(Regex("[0-9a-f]{64}")))
+    }
+
+    private fun model(
+        id: String,
+        methodName: String = "target-$id",
+        failureReason: TsUnknownCallFailureReason? = null,
+    ): TsUnknownCallModel = FakeModel(
+        id = id,
+        target = TsUnknownCallTarget(
+            methodName = methodName,
+            failureReason = failureReason,
+        ),
+    )
+
+    private class FakeModel(
+        override val id: String,
+        override val target: TsUnknownCallTarget,
+    ) : TsUnknownCallModel {
+        override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution =
+            error("Fake model must not execute in catalog metadata tests")
+    }
+}
diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts
index c78d4027f..7b80de0eb 100644
--- a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts
+++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts
@@ -18,6 +18,15 @@ declare class ExternalBoolean {
     static convert(value: boolean): boolean;
 }
 
+declare class ExternalAny {
+    static value(): any;
+}
+
+declare class ExternalModeledCall {
+    static identity(value: ExternalReceiver): ExternalReceiver;
+    static fail(): number;
+}
+
 class KnownReceiver {
     known(): number {
         return 1;
@@ -68,6 +77,21 @@ class CallFallbackBaseline {
         return ExternalBoolean.convert(value);
     }
 
+    modeledUnknownCallReturnsAlias(receiver: ExternalReceiver): number {
+        if (ExternalModeledCall.identity(receiver) === receiver) {
+            return 122;
+        }
+        return 0;
+    }
+
+    modeledUnknownCallThrows(): number {
+        return ExternalModeledCall.fail();
+    }
+
+    freshUnknownCallResult(): any {
+        return ExternalAny.value();
+    }
+
     anyReceiverWithKnownMethodContinues(receiver: any): number {
         receiver.known();
         return 102;
diff --git a/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts
new file mode 100644
index 000000000..52f114978
--- /dev/null
+++ b/usvm-ts/src/test/resources/models/ArrayShiftIntrinsic.ts
@@ -0,0 +1,74 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
+class ArrayElement {}
+
+export class ArrayShiftIntrinsic {
+    unknownValue(value: any): any {
+        return value;
+    }
+
+    emptyArray(): number | undefined {
+        const values: number[] = [];
+        return values.shift();
+    }
+
+    nonEmptyArray(): number {
+        const values = [10, 20, 30];
+        return values.shift()! + values[0] + values.length;
+    }
+
+    aliasedElement(): number {
+        const first = new ArrayElement();
+        const second = new ArrayElement();
+        const values: ArrayElement[] = [first, second];
+        if (values.shift() === first && values[0] === second && values.length === 1) {
+            return 42;
+        }
+
+        return 0;
+    }
+
+    symbolicNumberArray(values: number[]): number {
+        values.shift();
+        return 46;
+    }
+
+    symbolicUnknownArray(values: any[]): number {
+        if (values.length < 2) {
+            return 0;
+        }
+
+        const oldLength = values.length;
+        const firstType = typeof values[0];
+        const secondType = typeof values[1];
+        const removedType = typeof values.shift();
+        if (removedType === firstType && typeof values[0] === secondType && values.length === oldLength - 1) {
+            return 47;
+        }
+
+        return 1;
+    }
+
+    mixedUnknownArray(): number {
+        const element = new ArrayElement();
+        const values: any[] = [10, true, element];
+        const removed = values.shift();
+        if (removed === 10 && values[0] === true && values[1] === element && values.length === 2) {
+            return 49;
+        }
+
+        return 0;
+    }
+
+    emptyUnknownArray(): any {
+        const values: any[] = [];
+        return values.shift();
+    }
+
+    shiftWithArguments(): number {
+        const values = [1];
+        values.shift(0);
+        return 48;
+    }
+}