From a8301e2eb1063c81a973a01f1fe865489f5b5ca0 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 11 Jul 2025 16:28:16 +0300
Subject: [PATCH 01/40] Make instance in VirtualMethodCall non-null

---
 usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt        | 2 +-
 .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt
index 428ce13155..0f74291f75 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt
@@ -21,7 +21,7 @@ sealed interface TsMethodCall : EtsStmt {
 
 class TsVirtualMethodCallStmt(
     val callee: EtsMethodSignature,
-    override val instance: UExpr<*>?,
+    override val instance: UExpr<*>,
     override val args: List<UExpr<*>>,
     override val returnSite: EtsStmt,
 ) : TsMethodCall {
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 b89d9156d6..be9dcee863 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
@@ -156,7 +156,7 @@ class TsInterpreter(
 
         // NOTE: USE '.callee' INSTEAD OF '.method' !!!
 
-        val instance = requireNotNull(stmt.instance) { "Virtual code invocation with null as an instance" }
+        val instance = stmt.instance
 
         val unwrappedInstance = if (instance.isFakeObject()) {
             // TODO support primitives calls

From 67a24bf66fd86eb013d9b3176466e28f3d12de15 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 11 Jul 2025 17:38:04 +0300
Subject: [PATCH 02/40] Extract approximations

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 116 +++++++++++-------
 .../org/usvm/machine/state/TsMethodResult.kt  |  17 ++-
 2 files changed, 79 insertions(+), 54 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index b778671c2d..76e0449909 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -1176,61 +1176,89 @@ class TsExprResolver(
         }
     }
 
-    override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
-        val instanceRefResolved = resolve(value.instance) ?: return null
-        if (instanceRefResolved.sort != addressSort) {
-            logger.error("InstanceFieldRef access on not address sort: $instanceRefResolved")
-            scope.assert(falseExpr)
-            return null
+    private fun handleArrayLength(
+        value: EtsInstanceFieldRef,
+        instance: UHeapRef,
+    ): UExpr<*> = with(ctx) {
+        val arrayType = value.instance.type as EtsArrayType
+        val length = scope.calcOnState {
+            val lengthLValue = mkArrayLengthLValue(instance, arrayType)
+            memory.read(lengthLValue)
         }
-        val instanceRef = instanceRefResolved.asExpr(addressSort)
 
-        checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
+        scope.doWithState {
+            pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0))
+        }
 
-        // TODO It is a hack for array's length
-        if (value.field.name == "length") {
-            if (value.instance.type is EtsArrayType) {
-                val arrayType = value.instance.type as EtsArrayType
-                val lengthLValue = mkArrayLengthLValue(instanceRef, arrayType)
-                val length = scope.calcOnState { memory.read(lengthLValue) }
-                scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
+        return mkBvToFpExpr(
+            fp64Sort,
+            fpRoundingModeSortDefaultValue(),
+            length.asExpr(sizeSort),
+            signed = true,
+        )
+    }
 
-                return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), length.asExpr(sizeSort), signed = true)
-            }
+    private fun handleFakeLength(
+        value: EtsInstanceFieldRef,
+        instance: UConcreteHeapRef,
+    ): UExpr<*> = with(ctx) {
+        val fakeType = instance.getFakeType(scope)
 
-            // TODO: handle "length" property for arrays inside fake objects
-            if (instanceRef.isFakeObject()) {
-                val fakeType = instanceRef.getFakeType(scope)
+        // If we want to get length from a fake object, we assume that it is an array.
+        scope.doWithState {
+            pathConstraints += fakeType.refTypeExpr
+        }
 
-                // If we want to get length from a fake object, we assume that it is an array.
-                scope.doWithState { pathConstraints += fakeType.refTypeExpr }
+        val ref = instance.unwrapRef(scope)
 
-                val refLValue = getIntermediateRefLValue(instanceRef.address)
-                val obj = scope.calcOnState { memory.read(refLValue) }
+        val arrayType = when (val type = value.instance.type) {
+            is EtsArrayType -> type
 
-                val type = value.instance.type
-                val arrayType = type as? EtsArrayType ?: run {
-                    check(type is EtsAnyType || type is EtsUnknownType) {
-                        "Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got $type"
-                    }
+            is EtsAnyType, is EtsUnknownType -> {
+                // If the type is not an array, we assume it is a fake object with
+                // a length property that behaves like an array.
+                EtsArrayType(EtsUnknownType, dimensions = 1)
+            }
 
-                    // We don't know the type of the array, since it is a fake object
-                    // If we'd know the type, we would have used it instead of creating a fake object
-                    EtsArrayType(EtsUnknownType, dimensions = 1)
-                }
-                val lengthLValue = mkArrayLengthLValue(obj, arrayType)
-                val length = scope.calcOnState { memory.read(lengthLValue) }
+            else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got $type")
+        }
+        val length = scope.calcOnState {
+            val lengthLValue = mkArrayLengthLValue(ref, arrayType)
+            memory.read(lengthLValue)
+        }
 
-                scope.doWithState { pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) }
+        scope.doWithState {
+            pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0))
+        }
 
-                return mkBvToFpExpr(
-                    fp64Sort,
-                    fpRoundingModeSortDefaultValue(),
-                    length.asExpr(sizeSort),
-                    signed = true
-                )
+        return mkBvToFpExpr(
+            fp64Sort,
+            fpRoundingModeSortDefaultValue(),
+            length.asExpr(sizeSort),
+            signed = true
+        )
+    }
 
-            }
+    override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
+        val instanceResolved = resolve(value.instance) ?: return null
+        if (instanceResolved.sort != addressSort) {
+            logger.error { "Instance of field ref should be a reference, but got $instanceResolved" }
+            scope.assert(falseExpr)
+            return null
+        }
+        val instanceRef = instanceResolved.asExpr(addressSort)
+
+        checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
+
+        // Handle array length
+        if (value.field.name == "length" && value.instance.type is EtsArrayType) {
+            return handleArrayLength(value, instanceRef)
+        }
+
+        // Handle length property for fake objects
+        // TODO: handle "length" property for arrays inside fake objects
+        if (value.field.name == "length" && instanceRef.isFakeObject()) {
+            return handleFakeLength(value, instanceRef)
         }
 
         return handleFieldRef(value.instance, instanceRef, value.field, hierarchy)
@@ -1250,7 +1278,7 @@ class TsExprResolver(
                 scope.doWithState {
                     // TODO: Handle static initializer result
                     val result = methodResult
-                    if (result is TsMethodResult.Success && result.methodSignature() == initializer.signature) {
+                    if (result is TsMethodResult.Success && result.methodSignature == initializer.signature) {
                         methodResult = TsMethodResult.NoCall
                     }
                 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt
index 1bd8f7acb3..4b1a88312b 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt
@@ -5,7 +5,6 @@ import org.jacodb.ets.model.EtsMethodSignature
 import org.jacodb.ets.model.EtsType
 import org.usvm.UExpr
 import org.usvm.UHeapRef
-import org.usvm.USort
 
 /**
  * Represents a result of a method invocation.
@@ -16,25 +15,23 @@ sealed interface TsMethodResult {
      */
     object NoCall : TsMethodResult
 
-    sealed class Success(val value: UExpr<out USort>) : TsMethodResult {
-        abstract fun methodSignature(): EtsMethodSignature
+    sealed class Success(val value: UExpr<*>) : TsMethodResult {
+        abstract val methodSignature: EtsMethodSignature
 
         /**
          * A [method] successfully returned a [value].
          */
         class RegularCall(
             val method: EtsMethod,
-            value: UExpr<out USort>,
+            value: UExpr<*>,
         ) : Success(value) {
-            override fun methodSignature(): EtsMethodSignature = method.signature
+            override val methodSignature: EtsMethodSignature get() = method.signature
         }
 
         class MockedCall(
-            val methodSignature: EtsMethodSignature,
-            value: UExpr<out USort>,
-        ) : Success(value) {
-            override fun methodSignature(): EtsMethodSignature = methodSignature
-        }
+            override val methodSignature: EtsMethodSignature,
+            value: UExpr<*>,
+        ) : Success(value)
     }
 
     /**

From aac5a5fc9810f32c5403b013606b561656233319 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 14 Jul 2025 15:06:13 +0300
Subject: [PATCH 03/40] Make call instance non-nullable

---
 usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt
index 0f74291f75..49616f7db8 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMethodCall.kt
@@ -7,7 +7,7 @@ import org.jacodb.ets.model.EtsStmtLocation
 import org.usvm.UExpr
 
 sealed interface TsMethodCall : EtsStmt {
-    val instance: UExpr<*>?
+    val instance: UExpr<*>
     val args: List<UExpr<*>>
     val returnSite: EtsStmt
 
@@ -38,7 +38,7 @@ class TsVirtualMethodCallStmt(
 //  and not wrapped in array (if calling a vararg method)
 class TsConcreteMethodCallStmt(
     val callee: EtsMethod,
-    override val instance: UExpr<*>?,
+    override val instance: UExpr<*>,
     override val args: List<UExpr<*>>,
     override val returnSite: EtsStmt,
 ) : TsMethodCall {

From 21d96d573a221988ffe2918f654a63932568e097 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 14 Jul 2025 15:06:26 +0300
Subject: [PATCH 04/40] Reogranize

---
 .../usvm/machine/interpreter/TsInterpreter.kt | 80 ++++++++++---------
 1 file changed, 41 insertions(+), 39 deletions(-)

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 be9dcee863..59dacf119a 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
@@ -230,10 +230,7 @@ class TsInterpreter(
         val possibleTypesSet = possibleTypes.types.toSet()
 
         if (possibleTypesSet.singleOrNull() == EtsAnyType) {
-            mockMethodCall(scope, stmt.callee)
-            scope.calcOnState {
-                newStmt(stmt.returnSite)
-            }
+            mockMethodCall(scope, stmt.callee, stmt.returnSite)
             return
         }
 
@@ -297,17 +294,16 @@ class TsInterpreter(
             }
             constraint to block
         }
+
         if (conditionsWithBlocks.isEmpty()) {
             logger.warn {
                 "No suitable methods found for call: ${stmt.callee} with instance: $unwrappedInstance"
             }
-            mockMethodCall(scope, stmt.callee)
-            scope.doWithState {
-                newStmt(stmt.returnSite)
-            }
-        } else {
-            scope.forkMulti(conditionsWithBlocks)
+            mockMethodCall(scope, stmt.callee, stmt.returnSite)
+            return
         }
+
+        scope.forkMulti(conditionsWithBlocks)
     }
 
     private fun visitConcreteMethodCall(scope: TsStepScope, stmt: TsConcreteMethodCallStmt) {
@@ -317,10 +313,7 @@ class TsInterpreter(
         // TODO: observer
 
         if (stmt.callee.signature.enclosingClass.name == "Log") {
-            mockMethodCall(scope, stmt.callee.signature)
-            scope.doWithState {
-                newStmt(stmt.returnSite)
-            }
+            mockMethodCall(scope, stmt.callee.signature, stmt.returnSite)
             return
         }
 
@@ -329,10 +322,7 @@ class TsInterpreter(
             // logger.warn { "No entry point for method: ${stmt.callee}, mocking the call" }
             // If the method doesn't have entry points,
             // we go through it, we just mock the call
-            mockMethodCall(scope, stmt.callee.signature)
-            scope.doWithState {
-                newStmt(stmt.returnSite)
-            }
+            mockMethodCall(scope, stmt.callee.signature, stmt.returnSite)
             return
         }
 
@@ -405,7 +395,7 @@ class TsInterpreter(
                 "Expected $numFormal arguments, got ${args.size}"
             }
 
-            args += stmt.instance!!
+            args += stmt.instance
 
             // TODO: re-check push sorts for arguments
             pushSortsForActualArguments(args)
@@ -471,13 +461,14 @@ class TsInterpreter(
     private fun visitAssignStmt(scope: TsStepScope, stmt: EtsAssignStmt) = with(ctx) {
         val exprResolver = exprResolverWithScope(scope)
 
-        stmt.callExpr?.let {
+        val callExpr = stmt.callExpr
+        if (callExpr != null) {
             val methodResult = scope.calcOnState { methodResult }
 
             when (methodResult) {
                 is TsMethodResult.NoCall -> observer?.onCallWithUnresolvedArguments(
                     exprResolver.simpleValueResolver,
-                    it,
+                    callExpr,
                     scope
                 )
 
@@ -490,16 +481,18 @@ class TsInterpreter(
                 is TsMethodResult.TsException -> error("Exceptions must be processed earlier")
             }
 
-            if (it is EtsPtrCallExpr) {
-                mockMethodCall(scope, it.callee)
+            if (callExpr is EtsPtrCallExpr) {
+                mockMethodCall(scope, callExpr.callee, stmt)
                 return
             }
 
             if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
-                mockMethodCall(scope, it.callee)
+                mockMethodCall(scope, callExpr.callee, stmt)
                 return
             }
-        } ?: observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
+        } else {
+            observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
+        }
 
         val expr = exprResolver.resolve(stmt.rhv) ?: return
 
@@ -698,7 +691,7 @@ class TsInterpreter(
         }
 
         if (stmt.expr is EtsPtrCallExpr) {
-            mockMethodCall(scope, stmt.expr.callee)
+            mockMethodCall(scope, stmt.expr.callee, stmt)
             return
         }
 
@@ -711,7 +704,7 @@ class TsInterpreter(
         }
 
         // intraprocedural analysis
-        mockMethodCall(scope, stmt.expr.callee)
+        mockMethodCall(scope, stmt.expr.callee, stmt)
     }
 
     private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) {
@@ -841,25 +834,34 @@ class TsInterpreter(
         state
     }
 
-    private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) {
+    private fun mockMethodCall(
+        scope: TsStepScope,
+        method: EtsMethodSignature,
+        returnSite: EtsStmt,
+    ) {
         scope.doWithState {
+            newStmt(returnSite)
+
             if (method.returnType is EtsVoidType) {
-                methodResult = TsMethodResult.Success.MockedCall(method, ctx.mkUndefinedValue())
+                val result = ctx.mkUndefinedValue()
+                methodResult = TsMethodResult.Success.MockedCall(method, result)
                 return@doWithState
             }
 
             val resultSort = ctx.typeToSort(method.returnType)
-            val resultValue = when (resultSort) {
-                is UAddressSort -> makeSymbolicRefUntyped()
-
-                is TsUnresolvedSort -> ctx.mkFakeValue(
-                    scope,
-                    makeSymbolicPrimitive(ctx.boolSort),
-                    makeSymbolicPrimitive(ctx.fp64Sort),
-                    makeSymbolicRefUntyped()
-                )
+            val resultValue = scope.calcOnState {
+                when (resultSort) {
+                    is UAddressSort -> makeSymbolicRefUntyped()
+
+                    is TsUnresolvedSort -> ctx.mkFakeValue(
+                        scope,
+                        makeSymbolicPrimitive(ctx.boolSort),
+                        makeSymbolicPrimitive(ctx.fp64Sort),
+                        makeSymbolicRefUntyped()
+                    )
 
-                else -> makeSymbolicPrimitive(resultSort)
+                    else -> makeSymbolicPrimitive(resultSort)
+                }
             }
             methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
         }

From ff172a80baa78c4201030d0c0f42626fc3210b25 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 14 Jul 2025 15:06:33 +0300
Subject: [PATCH 05/40] Add test for PtrCall

---
 .../test/kotlin/org/usvm/samples/PtrCall.kt   | 24 +++++++++++++++++++
 usvm-ts/src/test/resources/samples/PtrCall.ts |  9 +++++++
 2 files changed, 33 insertions(+)
 create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt
 create mode 100644 usvm-ts/src/test/resources/samples/PtrCall.ts

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt
new file mode 100644
index 0000000000..427b317b75
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt
@@ -0,0 +1,24 @@
+package org.usvm.samples
+
+import org.jacodb.ets.model.EtsScene
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import kotlin.test.Test
+
+class PtrCall : TsMethodTestRunner() {
+
+    private val className = this::class.simpleName!!
+
+    override val scene: EtsScene = loadSampleScene(className)
+
+    @Test
+    fun `test call lambda`() {
+        val method = getMethod(className, "callLambda")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number == 42.0 },
+            )
+        )
+    }
+}
diff --git a/usvm-ts/src/test/resources/samples/PtrCall.ts b/usvm-ts/src/test/resources/samples/PtrCall.ts
new file mode 100644
index 0000000000..9e5f32a528
--- /dev/null
+++ b/usvm-ts/src/test/resources/samples/PtrCall.ts
@@ -0,0 +1,9 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
+class PtrCall {
+    callLambda(): number {
+        const f = () => 42;
+        return f();
+    }
+}

From a86a2f96db462e827f416a7508741d59754f5e8c Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 14 Jul 2025 15:30:21 +0300
Subject: [PATCH 06/40] Make Success sealed interface

---
 .../org/usvm/machine/interpreter/TsInterpreter.kt   |  7 ++++---
 .../kotlin/org/usvm/machine/state/TsMethodResult.kt | 13 +++++++------
 .../kotlin/org/usvm/machine/state/TsStateUtils.kt   |  2 +-
 3 files changed, 12 insertions(+), 10 deletions(-)

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 59dacf119a..1ce390af01 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
@@ -179,7 +179,7 @@ class TsInterpreter(
                     if (stmt.callee.name == CONSTRUCTOR_NAME) {
                         // Approximate unresolved constructor:
                         scope.doWithState {
-                            methodResult = TsMethodResult.Success.MockedCall(stmt.callee, unwrappedInstance)
+                            methodResult = TsMethodResult.Success.MockedCall(unwrappedInstance, stmt.callee)
                             newStmt(stmt.returnSite)
                         }
                         return
@@ -860,10 +860,11 @@ class TsInterpreter(
                         makeSymbolicRefUntyped()
                     )
 
-                    else -> makeSymbolicPrimitive(resultSort)
+                    else -> makeSymbolicPrimitive(sort)
                 }
             }
-            methodResult = TsMethodResult.Success.MockedCall(method, resultValue)
+
+            methodResult = TsMethodResult.Success.MockedCall(result, method)
         }
     }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt
index 4b1a88312b..27a33458b2 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsMethodResult.kt
@@ -15,23 +15,24 @@ sealed interface TsMethodResult {
      */
     object NoCall : TsMethodResult
 
-    sealed class Success(val value: UExpr<*>) : TsMethodResult {
-        abstract val methodSignature: EtsMethodSignature
+    sealed interface Success : TsMethodResult {
+        val value: UExpr<*>
+        val methodSignature: EtsMethodSignature
 
         /**
          * A [method] successfully returned a [value].
          */
         class RegularCall(
+            override val value: UExpr<*>,
             val method: EtsMethod,
-            value: UExpr<*>,
-        ) : Success(value) {
+        ) : Success {
             override val methodSignature: EtsMethodSignature get() = method.signature
         }
 
         class MockedCall(
+            override val value: UExpr<*>,
             override val methodSignature: EtsMethodSignature,
-            value: UExpr<*>,
-        ) : Success(value)
+        ) : Success
     }
 
     /**
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt
index e706047b5f..b464c1f8f4 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt
@@ -20,7 +20,7 @@ fun TsState.returnValue(valueToReturn: UExpr<out USort>) {
         popLocalToSortStack()
     }
 
-    methodResult = TsMethodResult.Success.RegularCall(returnFromMethod, valueToReturn)
+    methodResult = TsMethodResult.Success.RegularCall(valueToReturn, returnFromMethod)
 
     if (returnSite != null) {
         newStmt(returnSite)

From 6b37769f793bad9b62d8e43fef736fc31fbb4d62 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 14 Jul 2025 15:30:33 +0300
Subject: [PATCH 07/40] Reorganize mock

---
 .../org/usvm/machine/interpreter/TsInterpreter.kt   | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

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 1ce390af01..267b1acc01 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
@@ -842,15 +842,12 @@ class TsInterpreter(
         scope.doWithState {
             newStmt(returnSite)
 
+            val result: UExpr<*>
             if (method.returnType is EtsVoidType) {
-                val result = ctx.mkUndefinedValue()
-                methodResult = TsMethodResult.Success.MockedCall(method, result)
-                return@doWithState
-            }
-
-            val resultSort = ctx.typeToSort(method.returnType)
-            val resultValue = scope.calcOnState {
-                when (resultSort) {
+                result = ctx.mkUndefinedValue()
+            } else {
+                val sort = ctx.typeToSort(method.returnType)
+                result = when (sort) {
                     is UAddressSort -> makeSymbolicRefUntyped()
 
                     is TsUnresolvedSort -> ctx.mkFakeValue(

From 809040af89a026025914a7855ddb181a1877fad2 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 14 Jul 2025 17:04:02 +0300
Subject: [PATCH 08/40] Support CallPtr

---
 .../src/main/kotlin/org/usvm/api/TsMock.kt    | 38 +++++++++++
 .../org/usvm/machine/expr/TsExprResolver.kt   | 51 ++++++++++++++-
 .../usvm/machine/interpreter/TsInterpreter.kt | 65 +++++--------------
 .../kotlin/org/usvm/machine/state/TsState.kt  | 18 +++++
 .../org/usvm/machine/state/TsStateUtils.kt    |  3 +-
 5 files changed, 121 insertions(+), 54 deletions(-)
 create mode 100644 usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt

diff --git a/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt
new file mode 100644
index 0000000000..adcff2dd7d
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt
@@ -0,0 +1,38 @@
+package org.usvm.api
+
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsVoidType
+import org.usvm.UAddressSort
+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.types.mkFakeValue
+
+fun mockMethodCall(
+    scope: TsStepScope,
+    method: EtsMethodSignature,
+) {
+    scope.doWithState {
+        val result: UExpr<*>
+        if (method.returnType is EtsVoidType) {
+            result = ctx.mkUndefinedValue()
+        } else {
+            val sort = ctx.typeToSort(method.returnType)
+            result = when (sort) {
+                is UAddressSort -> makeSymbolicRefUntyped()
+
+                is TsUnresolvedSort -> ctx.mkFakeValue(
+                    scope,
+                    makeSymbolicPrimitive(ctx.boolSort),
+                    makeSymbolicPrimitive(ctx.fp64Sort),
+                    makeSymbolicRefUntyped()
+                )
+
+                else -> makeSymbolicPrimitive(sort)
+            }
+        }
+
+        methodResult = TsMethodResult.Success.MockedCall(result, method)
+    }
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 76e0449909..cb4fbe353c 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -79,6 +79,7 @@ import org.jacodb.ets.model.EtsUnsignedRightShiftExpr
 import org.jacodb.ets.model.EtsValue
 import org.jacodb.ets.model.EtsVoidExpr
 import org.jacodb.ets.model.EtsYieldExpr
+import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX
 import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.UNKNOWN_CLASS_NAME
@@ -94,6 +95,7 @@ import org.usvm.USort
 import org.usvm.api.allocateConcreteRef
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.initializeArrayLength
+import org.usvm.api.mockMethodCall
 import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
@@ -966,9 +968,39 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? {
-        // TODO: IMPORTANT do not forget to fill sorts of arguments map
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        return when (val result = scope.calcOnState { methodResult }) {
+            is TsMethodResult.Success -> {
+                scope.doWithState { methodResult = TsMethodResult.NoCall }
+                result.value
+            }
+
+            is TsMethodResult.TsException -> {
+                error("Exception should be handled earlier")
+            }
+
+            is TsMethodResult.NoCall -> {
+                val ptr = resolve(expr.ptr) ?: return null
+
+                if (isAllocatedConcreteHeapRef(ptr)) {
+                    val callee = scope.calcOnState {
+                        associatedMethods[ptr] ?: error("No associated methods for ptr: $ptr")
+                    }
+
+                    val resolvedArgs = expr.args.map { resolve(it) ?: return null }
+                    val concreteCall = TsConcreteMethodCallStmt(
+                        callee = callee,
+                        instance = ptr,
+                        args = resolvedArgs,
+                        returnSite = scope.calcOnState { lastStmt },
+                    )
+                    scope.doWithState { newStmt(concreteCall) }
+                } else {
+                    mockMethodCall(scope, expr.callee)
+                }
+
+                null
+            }
+        }
     }
 
     // endregion
@@ -1472,6 +1504,19 @@ class TsSimpleValueResolver(
             return ctx.mkFpInf(false, ctx.fp64Sort)
         }
 
+        if (local.name.startsWith(ANONYMOUS_METHOD_PREFIX)) {
+            val sig = EtsMethodSignature(
+                enclosingClass = EtsClassSignature.UNKNOWN,
+                name = local.name,
+                parameters = emptyList(),
+                returnType = EtsUnknownType,
+            )
+            val methods = ctx.resolveEtsMethods(sig)
+            val method = methods.single()
+            val ref = scope.calcOnState { getMethodRef(method) }
+            return ref
+        }
+
         val currentMethod = scope.calcOnState { lastEnteredMethod }
         if (local !in currentMethod.getDeclaredLocals()) {
             if (local.type is EtsFunctionType) {
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 267b1acc01..c0a1ce11be 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
@@ -13,7 +13,6 @@ import org.jacodb.ets.model.EtsIfStmt
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
-import org.jacodb.ets.model.EtsMethodSignature
 import org.jacodb.ets.model.EtsNopStmt
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
@@ -31,20 +30,17 @@ import org.jacodb.ets.model.EtsUndefinedType
 import org.jacodb.ets.model.EtsUnionType
 import org.jacodb.ets.model.EtsUnknownType
 import org.jacodb.ets.model.EtsValue
-import org.jacodb.ets.model.EtsVoidType
 import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.callExpr
 import org.jacodb.ets.utils.getDeclaredLocals
 import org.usvm.StepResult
 import org.usvm.StepScope
-import org.usvm.UAddressSort
 import org.usvm.UExpr
 import org.usvm.UInterpreter
 import org.usvm.UIteExpr
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.initializeArray
-import org.usvm.api.makeSymbolicPrimitive
-import org.usvm.api.makeSymbolicRefUntyped
+import org.usvm.api.mockMethodCall
 import org.usvm.api.targets.TsTarget
 import org.usvm.api.typeStreamOf
 import org.usvm.collections.immutable.internal.MutabilityOwnership
@@ -67,7 +63,6 @@ import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.parametersWithThisCount
 import org.usvm.machine.state.returnValue
 import org.usvm.machine.types.EtsAuxiliaryType
-import org.usvm.machine.types.mkFakeValue
 import org.usvm.machine.types.toAuxiliaryType
 import org.usvm.sizeSort
 import org.usvm.targets.UTargetsSet
@@ -230,7 +225,8 @@ class TsInterpreter(
         val possibleTypesSet = possibleTypes.types.toSet()
 
         if (possibleTypesSet.singleOrNull() == EtsAnyType) {
-            mockMethodCall(scope, stmt.callee, stmt.returnSite)
+            mockMethodCall(scope, stmt.callee)
+            scope.doWithState { newStmt(stmt.returnSite) }
             return
         }
 
@@ -299,7 +295,8 @@ class TsInterpreter(
             logger.warn {
                 "No suitable methods found for call: ${stmt.callee} with instance: $unwrappedInstance"
             }
-            mockMethodCall(scope, stmt.callee, stmt.returnSite)
+            mockMethodCall(scope, stmt.callee)
+            scope.doWithState { newStmt(stmt.returnSite) }
             return
         }
 
@@ -313,7 +310,8 @@ class TsInterpreter(
         // TODO: observer
 
         if (stmt.callee.signature.enclosingClass.name == "Log") {
-            mockMethodCall(scope, stmt.callee.signature, stmt.returnSite)
+            mockMethodCall(scope, stmt.callee.signature)
+            scope.doWithState { newStmt(stmt.returnSite) }
             return
         }
 
@@ -322,7 +320,8 @@ class TsInterpreter(
             // logger.warn { "No entry point for method: ${stmt.callee}, mocking the call" }
             // If the method doesn't have entry points,
             // we go through it, we just mock the call
-            mockMethodCall(scope, stmt.callee.signature, stmt.returnSite)
+            mockMethodCall(scope, stmt.callee.signature)
+            scope.doWithState { newStmt(stmt.returnSite) }
             return
         }
 
@@ -481,13 +480,9 @@ class TsInterpreter(
                 is TsMethodResult.TsException -> error("Exceptions must be processed earlier")
             }
 
-            if (callExpr is EtsPtrCallExpr) {
-                mockMethodCall(scope, callExpr.callee, stmt)
-                return
-            }
-
             if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
-                mockMethodCall(scope, callExpr.callee, stmt)
+                mockMethodCall(scope, callExpr.callee)
+                scope.doWithState { newStmt(stmt) }
                 return
             }
         } else {
@@ -683,15 +678,16 @@ class TsInterpreter(
 
     private fun visitCallStmt(scope: TsStepScope, stmt: EtsCallStmt) {
         if (scope.calcOnState { methodResult } is TsMethodResult.Success) {
+            val nextStmt = stmt.nextStmt ?: return
             scope.doWithState {
                 methodResult = TsMethodResult.NoCall
-                newStmt(stmt.nextStmt!!)
+                newStmt(nextStmt)
             }
             return
         }
 
         if (stmt.expr is EtsPtrCallExpr) {
-            mockMethodCall(scope, stmt.expr.callee, stmt)
+            mockMethodCall(scope, stmt.expr.callee)
             return
         }
 
@@ -704,7 +700,7 @@ class TsInterpreter(
         }
 
         // intraprocedural analysis
-        mockMethodCall(scope, stmt.expr.callee, stmt)
+        mockMethodCall(scope, stmt.expr.callee)
     }
 
     private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) {
@@ -834,37 +830,6 @@ class TsInterpreter(
         state
     }
 
-    private fun mockMethodCall(
-        scope: TsStepScope,
-        method: EtsMethodSignature,
-        returnSite: EtsStmt,
-    ) {
-        scope.doWithState {
-            newStmt(returnSite)
-
-            val result: UExpr<*>
-            if (method.returnType is EtsVoidType) {
-                result = ctx.mkUndefinedValue()
-            } else {
-                val sort = ctx.typeToSort(method.returnType)
-                result = when (sort) {
-                    is UAddressSort -> makeSymbolicRefUntyped()
-
-                    is TsUnresolvedSort -> ctx.mkFakeValue(
-                        scope,
-                        makeSymbolicPrimitive(ctx.boolSort),
-                        makeSymbolicPrimitive(ctx.fp64Sort),
-                        makeSymbolicRefUntyped()
-                    )
-
-                    else -> makeSymbolicPrimitive(sort)
-                }
-            }
-
-            methodResult = TsMethodResult.Success.MockedCall(result, method)
-        }
-    }
-
     // TODO: expand with interpreter implementation
     private val EtsStmt.nextStmt: EtsStmt?
         get() = graph.successors(this).firstOrNull()
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index 87649e8366..2a239d88c9 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsType
+import org.jacodb.ets.model.EtsUnknownType
 import org.jacodb.ets.model.EtsValue
 import org.usvm.PathNode
 import org.usvm.UCallStack
@@ -57,6 +58,9 @@ class TsState(
     var discoveredCallees: UPersistentHashMap<Pair<EtsStmt, Int>, EtsBlockCfg> = persistentHashMapOf(),
     var promiseStates: UPersistentHashMap<UConcreteHeapRef, PromiseState> = persistentHashMapOf(),
     var promiseExecutors: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
+    // TODO: use normal naming
+    var method2ref: UPersistentHashMap<EtsMethod, UConcreteHeapRef> = persistentHashMapOf(),
+    var associatedMethods: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,
@@ -158,6 +162,18 @@ class TsState(
         promiseExecutors = promiseExecutors.put(promise, method, ownership)
     }
 
+    fun getMethodRef(
+        method: EtsMethod,
+    ): UConcreteHeapRef {
+        val (updated, result) = method2ref.getOrPut(method, ownership) {
+            // TODO: what type should we use here?
+            memory.allocConcrete(EtsUnknownType)
+        }
+        associatedMethods = associatedMethods.put(result, method, ownership)
+        method2ref = updated
+        return result
+    }
+
     override fun clone(newConstraints: UPathConstraints<EtsType>?): TsState {
         val newThisOwnership = MutabilityOwnership()
         val cloneOwnership = MutabilityOwnership()
@@ -187,6 +203,8 @@ class TsState(
             discoveredCallees = discoveredCallees,
             promiseStates = promiseStates,
             promiseExecutors = promiseExecutors,
+            method2ref = method2ref,
+            associatedMethods = associatedMethods,
         )
     }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt
index b464c1f8f4..2a639ca915 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStateUtils.kt
@@ -6,7 +6,8 @@ import org.jacodb.ets.utils.getDeclaredLocals
 import org.usvm.UExpr
 import org.usvm.USort
 
-val TsState.lastStmt get() = pathNode.statement
+val TsState.lastStmt: EtsStmt
+    get() = currentStatement
 
 fun TsState.newStmt(stmt: EtsStmt) {
     pathNode += stmt

From e232fe7679722ced9d7b3c326ddaa7e2974dc6f3 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 14 Jul 2025 17:05:33 +0300
Subject: [PATCH 09/40] Move

---
 .../src/test/kotlin/org/usvm/samples/Call.kt  | 11 +++++++++
 .../test/kotlin/org/usvm/samples/PtrCall.kt   | 24 -------------------
 usvm-ts/src/test/resources/samples/Call.ts    |  5 ++++
 usvm-ts/src/test/resources/samples/PtrCall.ts |  9 -------
 4 files changed, 16 insertions(+), 33 deletions(-)
 delete mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt
 delete mode 100644 usvm-ts/src/test/resources/samples/PtrCall.ts

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
index 4a0854c08d..95c0658a1b 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -288,6 +288,17 @@ class Call : TsMethodTestRunner() {
             { r -> r.number == 20.0 },
         )
     }
+
+    @Test
+    fun `test call local lambda`() {
+        val method = getMethod(className, "callLocalLambda")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number == 42.0 },
+            )
+        )
+    }
 }
 
 fun fib(n: Double): Double {
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt
deleted file mode 100644
index 427b317b75..0000000000
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/PtrCall.kt
+++ /dev/null
@@ -1,24 +0,0 @@
-package org.usvm.samples
-
-import org.jacodb.ets.model.EtsScene
-import org.usvm.api.TsTestValue
-import org.usvm.util.TsMethodTestRunner
-import kotlin.test.Test
-
-class PtrCall : TsMethodTestRunner() {
-
-    private val className = this::class.simpleName!!
-
-    override val scene: EtsScene = loadSampleScene(className)
-
-    @Test
-    fun `test call lambda`() {
-        val method = getMethod(className, "callLambda")
-        discoverProperties<TsTestValue.TsNumber>(
-            method = method,
-            invariants = arrayOf(
-                { r -> r.number == 42.0 },
-            )
-        )
-    }
-}
diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts
index 218800ff1d..3e40fa2f33 100644
--- a/usvm-ts/src/test/resources/samples/Call.ts
+++ b/usvm-ts/src/test/resources/samples/Call.ts
@@ -164,6 +164,11 @@ class Call {
         let x: A = makeA();
         return x.foo(); // 20 (!!!) from B::foo
     }
+
+    callLocalLambda(): number {
+        const f = () => 42;
+        return f();
+    }
 }
 
 class A {
diff --git a/usvm-ts/src/test/resources/samples/PtrCall.ts b/usvm-ts/src/test/resources/samples/PtrCall.ts
deleted file mode 100644
index 9e5f32a528..0000000000
--- a/usvm-ts/src/test/resources/samples/PtrCall.ts
+++ /dev/null
@@ -1,9 +0,0 @@
-// @ts-nocheck
-// noinspection JSUnusedGlobalSymbols
-
-class PtrCall {
-    callLambda(): number {
-        const f = () => 42;
-        return f();
-    }
-}

From 20053f217922f9755d758406a6979a26e1aeba1a Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 17 Jul 2025 14:19:29 +0300
Subject: [PATCH 10/40] Use local jacodb

---
 settings.gradle.kts                               | 15 +++++++++++++--
 .../usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt    |  9 +++++++++
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/settings.gradle.kts b/settings.gradle.kts
index b6b98f4490..78be2d60d8 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -12,7 +12,7 @@ pluginManagement {
 
 plugins {
     // https://plugins.gradle.org/plugin/com.gradle.develocity
-    id("com.gradle.develocity") version("4.0.2")
+    id("com.gradle.develocity") version "4.0.2"
 }
 
 develocity {
@@ -55,4 +55,15 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons"
 // Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink.
 // As a workaround, we convert it to a real absolute path.
 // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756
-// includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath())
+includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath()) {
+    dependencySubstitution {
+        all {
+            val requested = requested
+            if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") {
+                val targetProject = ":${requested.module}"
+                useTarget(project(targetProject))
+                logger.info("Substituting ${requested.group}:${requested.module} with $targetProject")
+            }
+        }
+    }
+}
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
index c62b006dcb..dc91d56c9f 100644
--- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
+++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
@@ -25,6 +25,7 @@ import org.jacodb.ets.dto.EnumValueTypeDto
 import org.jacodb.ets.dto.FunctionTypeDto
 import org.jacodb.ets.dto.GenericTypeDto
 import org.jacodb.ets.dto.IntersectionTypeDto
+import org.jacodb.ets.dto.LexicalEnvTypeDto
 import org.jacodb.ets.dto.LiteralTypeDto
 import org.jacodb.ets.dto.LocalSignatureDto
 import org.jacodb.ets.dto.NeverTypeDto
@@ -48,6 +49,7 @@ import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsFunctionType
 import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsIntersectionType
+import org.jacodb.ets.model.EtsLexicalEnvType
 import org.jacodb.ets.model.EtsLiteralType
 import org.jacodb.ets.model.EtsNeverType
 import org.jacodb.ets.model.EtsNullType
@@ -104,6 +106,13 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
         )
     }
 
+    override fun visit(type: EtsLexicalEnvType): TypeDto {
+        return LexicalEnvTypeDto(
+            method = type.nestedMethod.toDto(),
+            closures = type.closures.map { it.toDto() },
+        )
+    }
+
     override fun visit(type: EtsEnumValueType): TypeDto {
         return EnumValueTypeDto(
             signature = type.signature.toDto(),

From e8024b3e60c806340b7406654115c0645005fed1 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 17 Jul 2025 16:57:52 +0300
Subject: [PATCH 11/40] Support closures

---
 .../dataflow/ts/infer/dto/EtsTypeToDto.kt     |   1 +
 .../dataflow/ts/infer/dto/EtsValueToDto.kt    |  27 ++++
 .../org/usvm/machine/expr/TsExprResolver.kt   | 122 ++++++++++++++----
 .../kotlin/org/usvm/machine/state/TsState.kt  |   9 ++
 .../src/test/kotlin/org/usvm/samples/Call.kt  |  28 ++++
 usvm-ts/src/test/resources/samples/Call.ts    |  16 +++
 6 files changed, 178 insertions(+), 25 deletions(-)

diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
index dc91d56c9f..737e34dab3 100644
--- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
+++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt
@@ -107,6 +107,7 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
     }
 
     override fun visit(type: EtsLexicalEnvType): TypeDto {
+        @Suppress("DEPRECATION")
         return LexicalEnvTypeDto(
             method = type.nestedMethod.toDto(),
             closures = type.closures.map { it.toDto() },
diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt
index f52eb1575f..2a788b0605 100644
--- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt
+++ b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsValueToDto.kt
@@ -17,7 +17,10 @@
 package org.usvm.dataflow.ts.infer.dto
 
 import org.jacodb.ets.dto.ArrayRefDto
+import org.jacodb.ets.dto.CaughtExceptionRefDto
+import org.jacodb.ets.dto.ClosureFieldRefDto
 import org.jacodb.ets.dto.ConstantDto
+import org.jacodb.ets.dto.GlobalRefDto
 import org.jacodb.ets.dto.InstanceFieldRefDto
 import org.jacodb.ets.dto.LocalDto
 import org.jacodb.ets.dto.ParameterRefDto
@@ -26,7 +29,10 @@ import org.jacodb.ets.dto.ThisRefDto
 import org.jacodb.ets.dto.ValueDto
 import org.jacodb.ets.model.EtsArrayAccess
 import org.jacodb.ets.model.EtsBooleanConstant
+import org.jacodb.ets.model.EtsCaughtExceptionRef
+import org.jacodb.ets.model.EtsClosureFieldRef
 import org.jacodb.ets.model.EtsConstant
+import org.jacodb.ets.model.EtsGlobalRef
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsNullConstant
@@ -112,4 +118,25 @@ private object EtsValueToDto : EtsValue.Visitor<ValueDto> {
             field = value.field.toDto(),
         )
     }
+
+    override fun visit(value: EtsCaughtExceptionRef): ValueDto {
+        return CaughtExceptionRefDto(
+            type = value.type.toDto(),
+        )
+    }
+
+    override fun visit(value: EtsGlobalRef): ValueDto {
+        return GlobalRefDto(
+            name = value.name,
+            ref = value.ref?.toDto(),
+        )
+    }
+
+    override fun visit(value: EtsClosureFieldRef): ValueDto {
+        return ClosureFieldRefDto(
+            base = value.base.toDto(),
+            fieldName = value.fieldName,
+            type = value.type.toDto(),
+        )
+    }
 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index cb4fbe353c..a3e6b17579 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -2,6 +2,7 @@ package org.usvm.machine.expr
 
 import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
+import io.ksmt.utils.cast
 import mu.KotlinLogging
 import org.jacodb.ets.model.EtsAddExpr
 import org.jacodb.ets.model.EtsAndExpr
@@ -17,8 +18,10 @@ import org.jacodb.ets.model.EtsBitXorExpr
 import org.jacodb.ets.model.EtsBooleanConstant
 import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsCastExpr
+import org.jacodb.ets.model.EtsCaughtExceptionRef
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsClassType
+import org.jacodb.ets.model.EtsClosureFieldRef
 import org.jacodb.ets.model.EtsConstant
 import org.jacodb.ets.model.EtsDeleteExpr
 import org.jacodb.ets.model.EtsDivExpr
@@ -28,6 +31,7 @@ import org.jacodb.ets.model.EtsExpExpr
 import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsFileSignature
 import org.jacodb.ets.model.EtsFunctionType
+import org.jacodb.ets.model.EtsGlobalRef
 import org.jacodb.ets.model.EtsGtEqExpr
 import org.jacodb.ets.model.EtsGtExpr
 import org.jacodb.ets.model.EtsInExpr
@@ -35,6 +39,7 @@ import org.jacodb.ets.model.EtsInstanceCallExpr
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsInstanceOfExpr
 import org.jacodb.ets.model.EtsLeftShiftExpr
+import org.jacodb.ets.model.EtsLexicalEnvType
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsLtEqExpr
 import org.jacodb.ets.model.EtsLtExpr
@@ -121,7 +126,6 @@ import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.types.EtsAuxiliaryType
 import org.usvm.machine.types.mkFakeValue
-import org.usvm.memory.ULValue
 import org.usvm.sizeSort
 import org.usvm.util.EtsHierarchy
 import org.usvm.util.EtsPropertyResolution
@@ -1330,6 +1334,32 @@ class TsExprResolver(
         return handleFieldRef(instance = null, instanceRef, value.field, hierarchy)
     }
 
+    override fun visit(value: EtsCaughtExceptionRef): UExpr<out USort>? {
+        logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
+        error("Not supported $value")
+    }
+
+    override fun visit(value: EtsGlobalRef): UExpr<out USort>? {
+        logger.warn { "visit(${value::class.simpleName}) is not implemented yet" }
+        error("Not supported $value")
+    }
+
+    override fun visit(value: EtsClosureFieldRef): UExpr<out USort>? = with(ctx) {
+        val obj = resolve(value.base) ?: return null
+        check(isAllocatedConcreteHeapRef(obj)) {
+            "Closure object should be a concrete heap reference, but got $obj"
+        }
+
+        val sort = typeToSort(value.type)
+        if (sort is TsUnresolvedSort) {
+            val lValue = mkFieldLValue(addressSort, obj, value.fieldName)
+            scope.calcOnState { memory.read(lValue) }
+        } else {
+            val lValue = mkFieldLValue(sort, obj, value.fieldName)
+            scope.calcOnState { memory.read(lValue) }
+        }
+    }
+
     // endregion
 
     // region OTHER
@@ -1415,7 +1445,7 @@ class TsSimpleValueResolver(
     private val localToIdx: (EtsMethod, EtsValue) -> Int?,
 ) : EtsValue.Visitor<UExpr<out USort>?> {
 
-    private fun resolveLocal(local: EtsValue): ULValue<*, USort> {
+    private fun resolveLocal(local: EtsValue): UExpr<*> {
         val currentMethod = scope.calcOnState { lastEnteredMethod }
         val entrypoint = scope.calcOnState { entrypoint }
 
@@ -1427,17 +1457,40 @@ class TsSimpleValueResolver(
         if (localIdx == null) {
             require(local is EtsLocal)
 
+            // Handle closures
+            if (local.name.startsWith("%closures")) {
+                val existingClosures = scope.calcOnState { closures[local.name] }
+                if (existingClosures != null) {
+                    return existingClosures
+                }
+                val type = local.type
+                check(type is EtsLexicalEnvType)
+                val obj = scope.calcOnState { memory.allocConcrete(type) }
+                for (captured in type.closures) {
+                    val resolvedCaptured = resolveLocal(captured)
+                    val lValue = mkFieldLValue(resolvedCaptured.sort, obj, captured.name)
+                    scope.doWithState {
+                        memory.write(lValue, resolvedCaptured.cast(), guard = ctx.trueExpr)
+                    }
+                }
+                scope.doWithState {
+                    setClosureObject(local.name, obj)
+                }
+                return obj
+            }
+
             val globalObject = scope.calcOnState { globalObject }
 
             val localName = local.name
             // Check whether this local was already created or not
             if (localName in scope.calcOnState { addedArtificialLocals }) {
                 val sort = ctx.typeToSort(local.type)
-                if (sort is TsUnresolvedSort) {
-                    return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+                val lValue = if (sort is TsUnresolvedSort) {
+                    mkFieldLValue(ctx.addressSort, globalObject, local.name)
                 } else {
-                    return mkFieldLValue(sort, globalObject, local.name)
+                    mkFieldLValue(sort, globalObject, local.name)
                 }
+                return scope.calcOnState { memory.read(lValue) }
             }
 
             logger.warn { "Cannot resolve local $local, creating a field of the global object" }
@@ -1447,12 +1500,13 @@ class TsSimpleValueResolver(
             }
 
             val sort = ctx.typeToSort(local.type)
-            if (sort is TsUnresolvedSort) {
+            val lValue = if (sort is TsUnresolvedSort) {
                 globalObject.createFakeField(localName, scope)
-                return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+                mkFieldLValue(ctx.addressSort, globalObject, local.name)
             } else {
-                return mkFieldLValue(sort, globalObject, local.name)
+                mkFieldLValue(sort, globalObject, local.name)
             }
+            return scope.calcOnState { memory.read(lValue) }
         }
 
         val sort = scope.calcOnState {
@@ -1463,33 +1517,42 @@ class TsSimpleValueResolver(
         // If we are not in the entrypoint, all correct values are already resolved and we can just return
         // a registerStackLValue for the local
         if (currentMethod != entrypoint) {
-            return mkRegisterStackLValue(sort, localIdx)
+            val lValue = mkRegisterStackLValue(sort, localIdx)
+            return scope.calcOnState { memory.read(lValue) }
         }
 
         // arguments and this for the first stack frame
         return when (sort) {
-            is UBoolSort -> mkRegisterStackLValue(sort, localIdx)
-            is KFp64Sort -> mkRegisterStackLValue(sort, localIdx)
-            is UAddressSort -> mkRegisterStackLValue(sort, localIdx)
+            is UBoolSort -> {
+                val lValue = mkRegisterStackLValue(sort, localIdx)
+                scope.calcOnState { memory.read(lValue) }
+            }
+
+            is KFp64Sort -> {
+                val lValue = mkRegisterStackLValue(sort, localIdx)
+                scope.calcOnState { memory.read(lValue) }
+            }
+
+            is UAddressSort -> {
+                val lValue = mkRegisterStackLValue(sort, localIdx)
+                scope.calcOnState { memory.read(lValue) }
+            }
+
             is TsUnresolvedSort -> {
                 check(local is EtsThis || local is EtsParameterRef) {
                     "Only This and ParameterRef are expected here"
                 }
 
-                val lValue = mkRegisterStackLValue(ctx.addressSort, localIdx)
-
                 val boolRValue = ctx.mkRegisterReading(localIdx, ctx.boolSort)
                 val fpRValue = ctx.mkRegisterReading(localIdx, ctx.fp64Sort)
                 val refRValue = ctx.mkRegisterReading(localIdx, ctx.addressSort)
 
                 val fakeObject = ctx.mkFakeValue(scope, boolRValue, fpRValue, refRValue)
+                val lValue = mkRegisterStackLValue(ctx.addressSort, localIdx)
                 scope.calcOnState {
-                    with(ctx) {
-                        memory.write(lValue, fakeObject.asExpr(addressSort), guard = trueExpr)
-                    }
+                    memory.write(lValue, fakeObject.asExpr(ctx.addressSort), guard = ctx.trueExpr)
                 }
-
-                lValue
+                fakeObject
             }
 
             else -> error("Unsupported sort $sort")
@@ -1525,18 +1588,15 @@ class TsSimpleValueResolver(
             }
         }
 
-        val lValue = resolveLocal(local)
-        return scope.calcOnState { memory.read(lValue) }
+        return resolveLocal(local)
     }
 
     override fun visit(value: EtsParameterRef): UExpr<out USort> {
-        val lValue = resolveLocal(value)
-        return scope.calcOnState { memory.read(lValue) }
+        return resolveLocal(value)
     }
 
     override fun visit(value: EtsThis): UExpr<out USort> {
-        val lValue = resolveLocal(value)
-        return scope.calcOnState { memory.read(lValue) }
+        return resolveLocal(value)
     }
 
     override fun visit(value: EtsConstant): UExpr<out USort> = with(ctx) {
@@ -1575,4 +1635,16 @@ class TsSimpleValueResolver(
     override fun visit(value: EtsStaticFieldRef): UExpr<out USort> = with(ctx) {
         error("Should not be called")
     }
+
+    override fun visit(value: EtsCaughtExceptionRef): UExpr<out USort>? {
+        error("Should not be called")
+    }
+
+    override fun visit(value: EtsGlobalRef): UExpr<out USort>? {
+        error("Should not be called")
+    }
+
+    override fun visit(value: EtsClosureFieldRef): UExpr<out USort>? {
+        error("Should not be called")
+    }
 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index 2a239d88c9..e871377941 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -61,6 +61,7 @@ class TsState(
     // TODO: use normal naming
     var method2ref: UPersistentHashMap<EtsMethod, UConcreteHeapRef> = persistentHashMapOf(),
     var associatedMethods: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
+    var closures: UPersistentHashMap<String, UConcreteHeapRef> = persistentHashMapOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,
@@ -174,6 +175,13 @@ class TsState(
         return result
     }
 
+    fun setClosureObject(
+        name: String,
+        closure: UConcreteHeapRef,
+    ) {
+        closures = closures.put(name, closure, ownership)
+    }
+
     override fun clone(newConstraints: UPathConstraints<EtsType>?): TsState {
         val newThisOwnership = MutabilityOwnership()
         val cloneOwnership = MutabilityOwnership()
@@ -205,6 +213,7 @@ class TsState(
             promiseExecutors = promiseExecutors,
             method2ref = method2ref,
             associatedMethods = associatedMethods,
+            closures = closures,
         )
     }
 
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
index 95c0658a1b..1d3974e770 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -299,6 +299,34 @@ class Call : TsMethodTestRunner() {
             )
         )
     }
+
+    @Test
+    fun `test call local closure capturing local`() {
+        val method = getMethod(className, "callLocalClosureCapturingLocal")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number == 42.0 },
+            )
+        )
+    }
+
+    @Test
+    fun `test call local closure capturing arguments`() {
+        val method = getMethod(className, "callLocalClosureCapturingArguments")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r ->
+                (a.value && b.value) && r.number == 1.0
+            },
+            { a, b, r ->
+                !(a.value && b.value) && r.number == 2.0
+            },
+            invariants = arrayOf(
+                { _, _, r -> r.number in listOf(1.0, 2.0) },
+            )
+        )
+    }
 }
 
 fun fib(n: Double): Double {
diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts
index 3e40fa2f33..7d3f59b20c 100644
--- a/usvm-ts/src/test/resources/samples/Call.ts
+++ b/usvm-ts/src/test/resources/samples/Call.ts
@@ -169,6 +169,22 @@ class Call {
         const f = () => 42;
         return f();
     }
+
+    callLocalClosureCapturingLocal(): number {
+        const x = 42;
+        const f = () => x;
+        return f();
+    }
+
+    callLocalClosureCapturingArguments(a: boolean, b: boolean): number {
+        const f = () => a && b;
+        const res = f();
+        if (res) {
+            return 1;
+        } else {
+            return 2;
+        }
+    }
 }
 
 class A {

From 32b79f6b9d0430862b71acf162e8a63487bb97e3 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 17 Jul 2025 17:17:32 +0300
Subject: [PATCH 12/40] Fix local jacodb

---
 .github/workflows/ci.yml | 38 ++++++++++++++++++++++++++++++++++++++
 settings.gradle.kts      |  6 +++++-
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3d5026c497..bc2c5758f7 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -18,6 +18,13 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
+      - name: Checkout local jacodb
+        uses: actions/checkout@v4
+        with:
+          repository: UnitTestBot/jacodb
+          ref: lipen/grpc
+          path: jacodb
+
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -45,6 +52,13 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
+      - name: Checkout local jacodb
+        uses: actions/checkout@v4
+        with:
+          repository: UnitTestBot/jacodb
+          ref: lipen/grpc
+          path: jacodb
+
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -74,6 +88,13 @@ jobs:
           # 'usvm-python/cpythonadapter/cpython' is a submodule
           submodules: true
 
+      - name: Checkout local jacodb
+        uses: actions/checkout@v4
+        with:
+          repository: UnitTestBot/jacodb
+          ref: lipen/grpc
+          path: jacodb
+
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -107,6 +128,13 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
+      - name: Checkout local jacodb
+        uses: actions/checkout@v4
+        with:
+          repository: UnitTestBot/jacodb
+          ref: lipen/grpc
+          path: jacodb
+
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -168,6 +196,13 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
+      - name: Checkout local jacodb
+        uses: actions/checkout@v4
+        with:
+          repository: UnitTestBot/jacodb
+          ref: lipen/grpc
+          path: jacodb
+
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -177,6 +212,9 @@ jobs:
       - name: Setup Gradle
         uses: gradle/actions/setup-gradle@v4
 
+      - name: Show project list
+        run: ./gradlew projects
+
       - name: Validate Project List
         run: ./gradlew validateProjectList
 
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 78be2d60d8..1dc120c720 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -55,7 +55,11 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons"
 // Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink.
 // As a workaround, we convert it to a real absolute path.
 // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756
-includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath()) {
+
+val jacodbPath = file("jacodb").takeIf { it.exists() }
+    ?: file("../jacodb").takeIf { it.exists() }
+    ?: error("Local JacoDB directory not found")
+includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) {
     dependencySubstitution {
         all {
             val requested = requested

From 76d04a413993e3e915db592fca9976bfbe8172cf Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 17 Jul 2025 17:18:54 +0300
Subject: [PATCH 13/40] Fix local jacodb branch

---
 .github/workflows/ci.yml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index bc2c5758f7..2300693524 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -22,7 +22,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           repository: UnitTestBot/jacodb
-          ref: lipen/grpc
+          ref: lipen/lexical-env-type
           path: jacodb
 
       - name: Setup Java JDK
@@ -56,7 +56,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           repository: UnitTestBot/jacodb
-          ref: lipen/grpc
+          ref: lipen/lexical-env-type
           path: jacodb
 
       - name: Setup Java JDK
@@ -92,7 +92,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           repository: UnitTestBot/jacodb
-          ref: lipen/grpc
+          ref: lipen/lexical-env-type
           path: jacodb
 
       - name: Setup Java JDK
@@ -132,7 +132,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           repository: UnitTestBot/jacodb
-          ref: lipen/grpc
+          ref: lipen/lexical-env-type
           path: jacodb
 
       - name: Setup Java JDK
@@ -200,7 +200,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           repository: UnitTestBot/jacodb
-          ref: lipen/grpc
+          ref: lipen/lexical-env-type
           path: jacodb
 
       - name: Setup Java JDK

From 2c2920ed266456a0aec09b261e5e6463faa3218f Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 17 Jul 2025 17:24:34 +0300
Subject: [PATCH 14/40] Bump ArkAnalyzer to neo/2025-07-16

---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 2300693524..3d5f07e2cc 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -158,7 +158,7 @@ jobs:
           DEST_DIR="arkanalyzer"
           MAX_RETRIES=10
           RETRY_DELAY=3  # Delay between retries in seconds  
-          BRANCH="neo/2025-06-24"
+          BRANCH="neo/2025-07-16"
 
           for ((i=1; i<=MAX_RETRIES; i++)); do
               git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

From a22f190994b13e7f716417faa4790a7888fc3423 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 17 Jul 2025 18:31:42 +0300
Subject: [PATCH 15/40] Add more tests for nested lambdas and closures

---
 .../src/test/kotlin/org/usvm/samples/Call.kt  | 59 +++++++++++++++++--
 usvm-ts/src/test/resources/samples/Call.ts    | 46 ++++++++++++++-
 2 files changed, 96 insertions(+), 9 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
index 1d3974e770..b579832987 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -290,8 +290,8 @@ class Call : TsMethodTestRunner() {
     }
 
     @Test
-    fun `test call local lambda`() {
-        val method = getMethod(className, "callLocalLambda")
+    fun `test call lambda`() {
+        val method = getMethod(className, "callLambda")
         discoverProperties<TsTestValue.TsNumber>(
             method = method,
             invariants = arrayOf(
@@ -301,8 +301,8 @@ class Call : TsMethodTestRunner() {
     }
 
     @Test
-    fun `test call local closure capturing local`() {
-        val method = getMethod(className, "callLocalClosureCapturingLocal")
+    fun `test call closure capturing local`() {
+        val method = getMethod(className, "callClosureCapturingLocal")
         discoverProperties<TsTestValue.TsNumber>(
             method = method,
             invariants = arrayOf(
@@ -312,8 +312,8 @@ class Call : TsMethodTestRunner() {
     }
 
     @Test
-    fun `test call local closure capturing arguments`() {
-        val method = getMethod(className, "callLocalClosureCapturingArguments")
+    fun `test call closure capturing arguments`() {
+        val method = getMethod(className, "callClosureCapturingArguments")
         discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
             method = method,
             { a, b, r ->
@@ -327,6 +327,53 @@ class Call : TsMethodTestRunner() {
             )
         )
     }
+
+    @Test
+    fun `test call nested lambda`() {
+        val method = getMethod(className, "callNestedLambda")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number == 42.0 },
+            )
+        )
+    }
+
+    @Test
+    fun `test call nested closure capturing outer local`() {
+        val method = getMethod(className, "callNestedClosureCapturingOuterLocal")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number == 42.0 },
+            )
+        )
+    }
+
+    @Test
+    fun `test call nested closure capturing inner local`() {
+        val method = getMethod(className, "callNestedClosureCapturingInnerLocal")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number == 42.0 },
+            )
+        )
+    }
+
+    @Test
+    fun `test call nested closure capturing local and argument`() {
+        val method = getMethod(className, "callNestedClosureCapturingLocalAndArgument")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, r -> a.value && r.number == 1.0 },
+            { a, r -> !a.value && r.number == 2.0 },
+            invariants = arrayOf(
+                { _, r -> r.number in listOf(1.0, 2.0) }
+            )
+        )
+    }
+
 }
 
 fun fib(n: Double): Double {
diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts
index 7d3f59b20c..49dff6b087 100644
--- a/usvm-ts/src/test/resources/samples/Call.ts
+++ b/usvm-ts/src/test/resources/samples/Call.ts
@@ -165,18 +165,18 @@ class Call {
         return x.foo(); // 20 (!!!) from B::foo
     }
 
-    callLocalLambda(): number {
+    callLambda(): number {
         const f = () => 42;
         return f();
     }
 
-    callLocalClosureCapturingLocal(): number {
+    callClosureCapturingLocal(): number {
         const x = 42;
         const f = () => x;
         return f();
     }
 
-    callLocalClosureCapturingArguments(a: boolean, b: boolean): number {
+    callClosureCapturingArguments(a: boolean, b: boolean): number {
         const f = () => a && b;
         const res = f();
         if (res) {
@@ -185,6 +185,46 @@ class Call {
             return 2;
         }
     }
+
+    callNestedLambda(): number {
+        const f = () => {
+            const g = () => 42;
+            return g();
+        };
+        return f();
+    }
+
+    callNestedClosureCapturingOuterLocal(): number {
+        const x = 42;
+        const f = () => {
+            const g = () => x;
+            return g();
+        };
+        return f();
+    }
+
+    callNestedClosureCapturingInnerLocal(): number {
+        const f = () => {
+            const x = 42;
+            const g = () => x;
+            return g();
+        };
+        return f();
+    }
+
+    callNestedClosureCapturingLocalAndArgument(a: boolean): number {
+        const b = true;
+        const f = () => {
+            const g = () => a && b;
+            return g();
+        };
+        const res = f();
+        if (res) {
+            return 1;
+        } else {
+            return 2;
+        }
+    }
 }
 
 class A {

From 18dc0ae4295e4e59a3153591cda34cb2ce90560f Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Thu, 17 Jul 2025 19:11:20 +0300
Subject: [PATCH 16/40] Add tests (disabled) for closures capturing mutable
 locals

---
 .../src/test/kotlin/org/usvm/samples/Call.kt  | 30 +++++++++++++++++++
 usvm-ts/src/test/kotlin/org/usvm/util/Util.kt | 10 +++++++
 usvm-ts/src/test/resources/samples/Call.ts    | 20 +++++++++++++
 3 files changed, 60 insertions(+)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
index b579832987..c833ef1701 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -5,6 +5,7 @@ import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
 import org.usvm.api.TsTestValue
 import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.eq
 
 class Call : TsMethodTestRunner() {
 
@@ -374,6 +375,35 @@ class Call : TsMethodTestRunner() {
         )
     }
 
+    @Disabled("Capturing mutable locals is not properly supported in ArkIR")
+    // Note: This test is disabled because ArkIR cannot properly represent the mutation
+    // of a captured mutable local (`let` or `var`) inside a closure.
+    // Due to this, `x += 100` instruction has no effect, and the result is 145 (120+20) instead of 225 (120+125).
+    // A possible solution would be to represent LHS in `x += 100` with `ClosureFieldRef` instead of `Local`.
+    @Test
+    fun `test call closure capturing mutable local`() {
+        val method = getMethod(className, "callClosureCapturingMutableLocal")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number eq 245 },
+            )
+        )
+    }
+
+    @Disabled("Capturing mutable locals is not properly supported in ArkIR")
+    // Note: See above.
+    // This test incorrectly produces 20 instead of 120.
+    @Test
+    fun `test call closure mutating captured local`() {
+        val method = getMethod(className, "callClosureMutatingCapturedLocal")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            invariants = arrayOf(
+                { r -> r.number eq 120 },
+            )
+        )
+    }
 }
 
 fun fib(n: Double): Double {
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt
index 0bb0ca1e10..056dae2934 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt
@@ -1,3 +1,13 @@
 package org.usvm.util
 
+import kotlin.math.abs
+
 fun Boolean.toDouble() = if (this) 1.0 else 0.0
+
+infix fun Double.eq(other: Int): Boolean {
+    return this eq other.toDouble()
+}
+
+infix fun Double.eq(other: Double): Boolean {
+    return abs(this - other) < 1e-9
+}
diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts
index 49dff6b087..653387e3f2 100644
--- a/usvm-ts/src/test/resources/samples/Call.ts
+++ b/usvm-ts/src/test/resources/samples/Call.ts
@@ -225,6 +225,26 @@ class Call {
             return 2;
         }
     }
+
+    callClosureCapturingMutableLocal(): number {
+        let x = 42;
+        const f = () => {
+            x += 100;
+            return x + 5;
+        };
+        x = 20;
+        return f() + x; // (20+100+5) + (20+100) = 245
+    }
+
+    callClosureMutatingCapturedLocal(): number {
+        let x = 42;
+        const f= () => {
+            x += 100;
+        };
+        x = 20;
+        f();
+        return x; // 120
+    }
 }
 
 class A {

From 0df24bd2ac31e879b4588ec6e6f304ff3b33b1ac Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 13:52:01 +0300
Subject: [PATCH 17/40] Move fib

---
 usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
index c833ef1701..cacf823550 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -404,13 +404,13 @@ class Call : TsMethodTestRunner() {
             )
         )
     }
-}
 
-fun fib(n: Double): Double {
-    if (n.isNaN()) return 0.0
-    if (n < 0) return -1.0
-    if (n > 10) return -100.0
-    if (n == 0.0) return 1.0
-    if (n == 1.0) return 1.0
-    return fib(n - 1.0) + fib(n - 2.0)
+    private fun fib(n: Double): Double {
+        if (n.isNaN()) return 0.0
+        if (n < 0) return -1.0
+        if (n > 10) return -100.0
+        if (n == 0.0) return 1.0
+        if (n == 1.0) return 1.0
+        return fib(n - 1.0) + fib(n - 2.0)
+    }
 }

From fe52769a55a72189fce496da5707940f0d28c5d0 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 14:18:14 +0300
Subject: [PATCH 18/40] Rename stored associations in state

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 10 +++---
 .../kotlin/org/usvm/machine/state/TsState.kt  | 34 +++++++++----------
 2 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index a3e6b17579..d4aded6985 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -398,7 +398,7 @@ class TsExprResolver(
         }
 
         val promiseState = scope.calcOnState {
-            promiseStates[promise] ?: PromiseState.PENDING
+            promiseState[promise] ?: PromiseState.PENDING
         }
 
         val isResolved = scope.calcOnState { isResolved(promise) }
@@ -408,7 +408,7 @@ class TsExprResolver(
                 "Promise state should be PENDING, but it is $promiseState for $promise"
             }
             val executor = scope.calcOnState {
-                promiseExecutors[promise]
+                promiseExecutor[promise]
                     ?: error("Await expression should have a promise executor, but it is not set for $promise")
             }
             check(executor.cfg.stmts.isNotEmpty())
@@ -987,7 +987,7 @@ class TsExprResolver(
 
                 if (isAllocatedConcreteHeapRef(ptr)) {
                     val callee = scope.calcOnState {
-                        associatedMethods[ptr] ?: error("No associated methods for ptr: $ptr")
+                        associatedMethod[ptr] ?: error("No associated methods for ptr: $ptr")
                     }
 
                     val resolvedArgs = expr.args.map { resolve(it) ?: return null }
@@ -1459,7 +1459,7 @@ class TsSimpleValueResolver(
 
             // Handle closures
             if (local.name.startsWith("%closures")) {
-                val existingClosures = scope.calcOnState { closures[local.name] }
+                val existingClosures = scope.calcOnState { closureObject[local.name] }
                 if (existingClosures != null) {
                     return existingClosures
                 }
@@ -1576,7 +1576,7 @@ class TsSimpleValueResolver(
             )
             val methods = ctx.resolveEtsMethods(sig)
             val method = methods.single()
-            val ref = scope.calcOnState { getMethodRef(method) }
+            val ref = scope.calcOnState { getAssociatedMethod(method) }
             return ref
         }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index e871377941..819f13f5f6 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -56,12 +56,12 @@ class TsState(
     val addedArtificialLocals: MutableSet<String> = hashSetOf(),
     val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
     var discoveredCallees: UPersistentHashMap<Pair<EtsStmt, Int>, EtsBlockCfg> = persistentHashMapOf(),
-    var promiseStates: UPersistentHashMap<UConcreteHeapRef, PromiseState> = persistentHashMapOf(),
-    var promiseExecutors: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
+    var promiseState: UPersistentHashMap<UConcreteHeapRef, PromiseState> = persistentHashMapOf(),
+    var promiseExecutor: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
     // TODO: use normal naming
-    var method2ref: UPersistentHashMap<EtsMethod, UConcreteHeapRef> = persistentHashMapOf(),
-    var associatedMethods: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
-    var closures: UPersistentHashMap<String, UConcreteHeapRef> = persistentHashMapOf(),
+    var methodToRef: UPersistentHashMap<EtsMethod, UConcreteHeapRef> = persistentHashMapOf(),
+    var associatedMethod: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
+    var closureObject: UPersistentHashMap<String, UConcreteHeapRef> = persistentHashMapOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,
@@ -153,25 +153,25 @@ class TsState(
         promise: UConcreteHeapRef,
         state: PromiseState,
     ) {
-        promiseStates = promiseStates.put(promise, state, ownership)
+        promiseState = promiseState.put(promise, state, ownership)
     }
 
     fun setPromiseExecutor(
         promise: UConcreteHeapRef,
         method: EtsMethod,
     ) {
-        promiseExecutors = promiseExecutors.put(promise, method, ownership)
+        promiseExecutor = promiseExecutor.put(promise, method, ownership)
     }
 
-    fun getMethodRef(
+    fun getAssociatedMethod(
         method: EtsMethod,
     ): UConcreteHeapRef {
-        val (updated, result) = method2ref.getOrPut(method, ownership) {
+        val (updated, result) = methodToRef.getOrPut(method, ownership) {
             // TODO: what type should we use here?
             memory.allocConcrete(EtsUnknownType)
         }
-        associatedMethods = associatedMethods.put(result, method, ownership)
-        method2ref = updated
+        associatedMethod = associatedMethod.put(result, method, ownership)
+        methodToRef = updated
         return result
     }
 
@@ -179,7 +179,7 @@ class TsState(
         name: String,
         closure: UConcreteHeapRef,
     ) {
-        closures = closures.put(name, closure, ownership)
+        closureObject = closureObject.put(name, closure, ownership)
     }
 
     override fun clone(newConstraints: UPathConstraints<EtsType>?): TsState {
@@ -209,11 +209,11 @@ class TsState(
             addedArtificialLocals = addedArtificialLocals,
             lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(),
             discoveredCallees = discoveredCallees,
-            promiseStates = promiseStates,
-            promiseExecutors = promiseExecutors,
-            method2ref = method2ref,
-            associatedMethods = associatedMethods,
-            closures = closures,
+            promiseState = promiseState,
+            promiseExecutor = promiseExecutor,
+            methodToRef = methodToRef,
+            associatedMethod = associatedMethod,
+            closureObject = closureObject,
         )
     }
 

From 3375b4d5cab0e37d7489e22587e48a632492fc6a Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 14:46:30 +0300
Subject: [PATCH 19/40] Refactoring

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 154 +++++++++---------
 .../usvm/machine/interpreter/TsInterpreter.kt |   8 +-
 .../kotlin/org/usvm/util/EtsFieldResolver.kt  |  20 +--
 3 files changed, 92 insertions(+), 90 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index d4aded6985..c58f0980a2 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -128,7 +128,7 @@ import org.usvm.machine.types.EtsAuxiliaryType
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.sizeSort
 import org.usvm.util.EtsHierarchy
-import org.usvm.util.EtsPropertyResolution
+import org.usvm.util.TsResolutionResult
 import org.usvm.util.createFakeField
 import org.usvm.util.isResolved
 import org.usvm.util.mkArrayIndexLValue
@@ -818,21 +818,44 @@ class TsExprResolver(
         }
     }
 
+    private fun handleR(): UExpr<*>? = with(ctx) {
+        val mockSymbol = scope.calcOnState {
+            memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership)
+        }
+        scope.assert(mkNot(mkEq(mockSymbol, mkTsNullValue())))
+        mockSymbol
+    }
+
+    private fun handleNumberConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
+        check(expr.args.size == 1) {
+            "Number() should have exactly one argument, but got ${expr.args.size}"
+        }
+        val arg = resolve(expr.args.single()) ?: return null
+        return mkNumericExpr(arg, scope)
+    }
+
+    private fun handleBooleanConverter(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
+        check(expr.args.size == 1) {
+            "Boolean() should have exactly one argument, but got ${expr.args.size}"
+        }
+        val arg = resolve(expr.args.single()) ?: return null
+        return mkTruthyExpr(arg, scope)
+    }
+
     override fun visit(expr: EtsStaticCallExpr): UExpr<*>? = with(ctx) {
+        // Mock `$r` calls
+        if (expr.callee.name == "\$r") {
+            return handleR()
+        }
+
+        // Handle `Number(...)` calls
         if (expr.callee.name == "Number") {
-            check(expr.args.size == 1) {
-                "Number() should have exactly one argument, but got ${expr.args.size}"
-            }
-            val arg = resolve(expr.args.single()) ?: return null
-            return mkNumericExpr(arg, scope)
+            return handleNumberConverter(expr)
         }
 
+        // Handle `Boolean(...)` calls
         if (expr.callee.name == "Boolean") {
-            check(expr.args.size == 1) {
-                "Boolean() should have exactly one argument, but got ${expr.args.size}"
-            }
-            val arg = resolve(expr.args.single()) ?: return null
-            return mkTruthyExpr(arg, scope)
+            return handleBooleanConverter(expr)
         }
 
         if (expr.callee.name in listOf("resolve", "reject")) {
@@ -867,16 +890,6 @@ class TsExprResolver(
             return mkUndefinedValue()
         }
 
-        if (expr.callee.name == "\$r") {
-            return scope.calcOnState {
-                val mockSymbol = memory.mocker.createMockSymbol(trackedLiteral = null, addressSort, ownership)
-
-                scope.assert(mkEq(mockSymbol, ctx.mkTsNullValue()).not())
-
-                mockSymbol
-            }
-        }
-
         return when (val result = scope.calcOnState { methodResult }) {
             is TsMethodResult.Success -> {
                 scope.doWithState { methodResult = TsMethodResult.NoCall }
@@ -888,58 +901,47 @@ class TsExprResolver(
             }
 
             is TsMethodResult.NoCall -> {
-                val resolutionResult = resolveStaticMethod(expr.callee)
-
-                if (resolutionResult is EtsPropertyResolution.Empty) {
-                    logger.error { "Could not resolve static call: ${expr.callee}" }
-                    scope.assert(falseExpr)
-                    return null
-                }
-
-                // static virtual call
-                if (resolutionResult is EtsPropertyResolution.Ambiguous) {
-                    val resolvedArgs = expr.args.map { resolve(it) ?: return null }
-
-                    val staticProperties = resolutionResult.properties.take(
-                        Constants.STATIC_METHODS_FORK_LIMIT
-                    )
-
-                    val staticInstances = scope.calcOnState {
-                        staticProperties.map { getStaticInstance(it.enclosingClass!!) }
+                when (val resolved = resolveStaticMethod(expr.callee)) {
+                    TsResolutionResult.Empty -> {
+                        logger.error { "Could not resolve static call: ${expr.callee}" }
+                        scope.assert(falseExpr)
                     }
 
-                    val concreteCalls = staticProperties.mapIndexed { index, value ->
-                        TsConcreteMethodCallStmt(
-                            callee = value,
-                            instance = staticInstances[index],
-                            args = resolvedArgs,
-                            returnSite = scope.calcOnState { lastStmt }
-                        )
+                    // Static virtual call
+                    is TsResolutionResult.Ambiguous -> {
+                        val resolvedArgs = expr.args.map { resolve(it) ?: return null }
+                        val staticProperties = resolved.properties.take(Constants.STATIC_METHODS_FORK_LIMIT)
+                        val staticInstances = scope.calcOnState {
+                            staticProperties.map { getStaticInstance(it.enclosingClass!!) }
+                        }
+                        val concreteCalls = staticProperties.mapIndexed { index, value ->
+                            TsConcreteMethodCallStmt(
+                                callee = value,
+                                instance = staticInstances[index],
+                                args = resolvedArgs,
+                                returnSite = scope.calcOnState { lastStmt }
+                            )
+                        }
+                        val blocks: List<Pair<UBoolExpr, TsState.() -> Unit>> = concreteCalls.map { stmt ->
+                            mkTrue() to { newStmt(stmt) }
+                        }
+                        scope.forkMulti(blocks)
                     }
 
-                    val blocks = concreteCalls.map {
-                        ctx.mkTrue() to { state: TsState -> state.newStmt(it) }
+                    is TsResolutionResult.Unique -> {
+                        val instance = scope.calcOnState {
+                            getStaticInstance(resolved.property.enclosingClass!!)
+                        }
+                        val args = expr.args.map { resolve(it) ?: return null }
+                        val concreteCall = TsConcreteMethodCallStmt(
+                            callee = resolved.property,
+                            instance = instance,
+                            args = args,
+                            returnSite = scope.calcOnState { lastStmt },
+                        )
+                        scope.doWithState { newStmt(concreteCall) }
                     }
-
-                    scope.forkMulti(blocks)
-
-                    return null
                 }
-
-                require(resolutionResult is EtsPropertyResolution.Unique)
-
-                val instance = scope.calcOnState { getStaticInstance(resolutionResult.property.enclosingClass!!) }
-
-                val resolvedArgs = expr.args.map { resolve(it) ?: return null }
-
-                val concreteCall = TsConcreteMethodCallStmt(
-                    callee = resolutionResult.property,
-                    instance = instance,
-                    args = resolvedArgs,
-                    returnSite = scope.calcOnState { lastStmt },
-                )
-                scope.doWithState { newStmt(concreteCall) }
-
                 null
             }
         }
@@ -947,20 +949,20 @@ class TsExprResolver(
 
     private fun resolveStaticMethod(
         method: EtsMethodSignature,
-    ): EtsPropertyResolution<EtsMethod> {
+    ): TsResolutionResult<EtsMethod> {
         // Perfect signature:
         if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
             val classes = hierarchy.classesForType(EtsClassType(method.enclosingClass))
             if (classes.size > 1) {
                 val methods = classes.map { it.methods.single { it.name == method.name } }
-                return EtsPropertyResolution.create(methods)
+                return TsResolutionResult.create(methods)
             }
 
-            if (classes.isEmpty()) return EtsPropertyResolution.Empty
+            if (classes.isEmpty()) return TsResolutionResult.Empty
 
             val clazz = classes.single()
             val methods = clazz.methods.filter { it.name == method.name }
-            return EtsPropertyResolution.create(methods)
+            return TsResolutionResult.create(methods)
         }
 
         // Unknown signature:
@@ -968,7 +970,7 @@ class TsExprResolver(
             .flatMap { it.methods }
             .filter { it.name == method.name }
 
-        return EtsPropertyResolution.create(methods)
+        return TsResolutionResult.create(methods)
     }
 
     override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? {
@@ -1138,7 +1140,7 @@ class TsExprResolver(
         val etsField = resolveEtsField(instance, field, hierarchy)
 
         val sort = when (etsField) {
-            is EtsPropertyResolution.Empty -> {
+            is TsResolutionResult.Empty -> {
                 if (field.name !in listOf("i", "LogLevel")) {
                     logger.warn { "Field $field not found, creating fake field" }
                 }
@@ -1150,8 +1152,8 @@ class TsExprResolver(
                 addressSort
             }
 
-            is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type)
-            is EtsPropertyResolution.Ambiguous -> unresolvedSort
+            is TsResolutionResult.Unique -> typeToSort(etsField.property.type)
+            is TsResolutionResult.Ambiguous -> unresolvedSort
         }
 
         scope.doWithState {
@@ -1184,7 +1186,7 @@ class TsExprResolver(
                 }
 
                 // TODO ambiguous enum fields resolution
-                if (etsField is EtsPropertyResolution.Unique) {
+                if (etsField is TsResolutionResult.Unique) {
                     val fieldType = etsField.property.type
                     if (fieldType is EtsRawType && fieldType.kind == "EnumValueType") {
                         val fakeType = fakeRef.getFakeType(scope)
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 c0a1ce11be..3be32412d4 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
@@ -68,7 +68,7 @@ import org.usvm.sizeSort
 import org.usvm.targets.UTargetsSet
 import org.usvm.types.TypesResult
 import org.usvm.types.single
-import org.usvm.util.EtsPropertyResolution
+import org.usvm.util.TsResolutionResult
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
@@ -585,9 +585,9 @@ class TsInterpreter(
 
                     // If there is no such field, we create a fake field for the expr
                     val sort = when (etsField) {
-                        is EtsPropertyResolution.Empty -> unresolvedSort
-                        is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type)
-                        is EtsPropertyResolution.Ambiguous -> unresolvedSort
+                        is TsResolutionResult.Empty -> unresolvedSort
+                        is TsResolutionResult.Unique -> typeToSort(etsField.property.type)
+                        is TsResolutionResult.Ambiguous -> unresolvedSort
                     }
 
                     if (sort == unresolvedSort) {
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
index 695e79e21c..5188459900 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
@@ -16,7 +16,7 @@ fun TsContext.resolveEtsField(
     instance: EtsLocal?,
     field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
-): EtsPropertyResolution<EtsField> {
+): TsResolutionResult<EtsField> {
     // Perfect signature:
     if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) {
         val classes = hierarchy.classesForType(EtsClassType(field.enclosingClass))
@@ -29,7 +29,7 @@ fun TsContext.resolveEtsField(
         val clazz = classes.single()
         val fields = clazz.getAllFields(hierarchy).filter { it.name == field.name }
         if (fields.size == 1) {
-            return EtsPropertyResolution.create(fields.single())
+            return TsResolutionResult.create(fields.single())
         }
     }
 
@@ -39,12 +39,12 @@ fun TsContext.resolveEtsField(
         when (instanceType) {
             is EtsClassType -> {
                 val field = tryGetSingleField(scene, instanceType.signature.name, field.name, hierarchy)
-                if (field != null) return EtsPropertyResolution.create(field)
+                if (field != null) return TsResolutionResult.create(field)
             }
 
             is EtsUnclearRefType -> {
                 val field = tryGetSingleField(scene, instanceType.typeName, field.name, hierarchy)
-                if (field != null) return EtsPropertyResolution.create(field)
+                if (field != null) return TsResolutionResult.create(field)
             }
         }
     }
@@ -53,7 +53,7 @@ fun TsContext.resolveEtsField(
         cls.getAllFields(hierarchy).filter { it.name == field.name }
     }
 
-    return EtsPropertyResolution.create(fields)
+    return TsResolutionResult.create(fields)
 }
 
 private fun tryGetSingleField(
@@ -116,15 +116,15 @@ fun EtsClass.getAllProperties(hierarchy: EtsHierarchy): Pair<Set<EtsFieldName>,
     return allFields to allMethods
 }
 
-sealed class EtsPropertyResolution<out T> {
-    data class Unique<T>(val property: T) : EtsPropertyResolution<T>()
-    data class Ambiguous<T>(val properties: List<T>) : EtsPropertyResolution<T>()
-    data object Empty : EtsPropertyResolution<Nothing>()
+sealed class TsResolutionResult<out T> {
+    data class Unique<T>(val property: T) : TsResolutionResult<T>()
+    data class Ambiguous<T>(val properties: List<T>) : TsResolutionResult<T>()
+    data object Empty : TsResolutionResult<Nothing>()
 
     companion object {
         fun <T> create(property: T) = Unique(property)
 
-        fun <T> create(properties: List<T>): EtsPropertyResolution<T> {
+        fun <T> create(properties: List<T>): TsResolutionResult<T> {
             return when {
                 properties.isEmpty() -> Empty
                 properties.size == 1 -> Unique(properties.single())

From 89d0102f37358b2c23c3d3eccc38aa86a2941911 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 14:59:03 +0300
Subject: [PATCH 20/40] Comment

---
 usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index c58f0980a2..32bd0cce35 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -1316,6 +1316,8 @@ class TsExprResolver(
                 scope.doWithState {
                     // TODO: Handle static initializer result
                     val result = methodResult
+                    // TODO: Why this signature check is needed?
+                    // TODO: Why we need to reset methodResult here? Double-check that it is even set anywhere.
                     if (result is TsMethodResult.Success && result.methodSignature == initializer.signature) {
                         methodResult = TsMethodResult.NoCall
                     }

From ab4b9a134fe14dbe9daacdbf4bad47c52526ddb4 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 14:59:10 +0300
Subject: [PATCH 21/40] Cleanup

---
 usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index 819f13f5f6..4950f153a8 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -136,8 +136,7 @@ class TsState(
     ) {
         pushLocalToSortStack()
         arguments.forEachIndexed { index, arg ->
-            val idx = index
-            saveSortForLocal(idx, arg.sort)
+            saveSortForLocal(index, arg.sort)
         }
     }
 

From f9d4e6ec277d8c4c31cc192f7317f4e39c5b48fb Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 15:02:44 +0300
Subject: [PATCH 22/40] TODO

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 67 ++++++++++---------
 1 file changed, 36 insertions(+), 31 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 32bd0cce35..b9258f11ca 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -858,37 +858,42 @@ class TsExprResolver(
             return handleBooleanConverter(expr)
         }
 
-        if (expr.callee.name in listOf("resolve", "reject")) {
-            val promise = resolve(
-                EtsThis(
-                    EtsClassType(
-                        EtsClassSignature(
-                            "Promise",
-                            EtsFileSignature("typescript", "lib.es5.d.ts")
-                        )
-                    )
-                )
-            )?.asExpr(addressSort) ?: return null
-            check(isAllocatedConcreteHeapRef(promise)) {
-                "Promise instance should be allocated, but it is not: $promise"
-            }
-            val newState = when (expr.callee.name) {
-                "resolve" -> PromiseState.FULFILLED
-                "reject" -> PromiseState.REJECTED
-                else -> error("Unexpected: $expr")
-            }
-            check(expr.args.size == 1) {
-                "${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}"
-            }
-            val value = resolve(expr.args.single()) ?: return null
-            val fakeValue = value.toFakeObject(scope)
-            scope.doWithState {
-                markResolved(promise.asExpr(addressSort))
-                setPromiseState(promise, newState)
-                setResolvedValue(promise.asExpr(addressSort), fakeValue)
-            }
-            return mkUndefinedValue()
-        }
+        // TODO: this should be handled in visit(AwaitExpr)
+        // Note: in the new IR, calls to "resolve" and "reject" methods were fixed to be PtrCall, so we
+        //  cannot handle them here. Instead, we should rely on the common handling of PtrCall, that is,
+        //  allocate new refs and associate them with SYNTHETIC "resolve" and "reject" methods.
+        //
+        // if (expr.callee.name in listOf("resolve", "reject")) {
+        //     val promise = resolve(
+        //         EtsThis(
+        //             EtsClassType(
+        //                 EtsClassSignature(
+        //                     "Promise",
+        //                     EtsFileSignature("typescript", "lib.es5.d.ts")
+        //                 )
+        //             )
+        //         )
+        //     )?.asExpr(addressSort) ?: return null
+        //     check(isAllocatedConcreteHeapRef(promise)) {
+        //         "Promise instance should be allocated, but it is not: $promise"
+        //     }
+        //     val newState = when (expr.callee.name) {
+        //         "resolve" -> PromiseState.FULFILLED
+        //         "reject" -> PromiseState.REJECTED
+        //         else -> error("Unexpected: $expr")
+        //     }
+        //     check(expr.args.size == 1) {
+        //         "${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}"
+        //     }
+        //     val value = resolve(expr.args.single()) ?: return null
+        //     val fakeValue = value.toFakeObject(scope)
+        //     scope.doWithState {
+        //         markResolved(promise.asExpr(addressSort))
+        //         setPromiseState(promise, newState)
+        //         setResolvedValue(promise.asExpr(addressSort), fakeValue)
+        //     }
+        //     return mkUndefinedValue()
+        // }
 
         return when (val result = scope.calcOnState { methodResult }) {
             is TsMethodResult.Success -> {

From 485f00e6a74a08dcf28b067801c253a694999a56 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 15:09:37 +0300
Subject: [PATCH 23/40] Note

---
 .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt   | 2 ++
 1 file changed, 2 insertions(+)

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 3be32412d4..3ab20def7e 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
@@ -678,6 +678,8 @@ class TsInterpreter(
 
     private fun visitCallStmt(scope: TsStepScope, stmt: EtsCallStmt) {
         if (scope.calcOnState { methodResult } is TsMethodResult.Success) {
+            // TODO: seems like USVM will never finish going back to this state even when there is no next stmt,
+            //  since the state is not dead, and the method result is not reset...
             val nextStmt = stmt.nextStmt ?: return
             scope.doWithState {
                 methodResult = TsMethodResult.NoCall

From 657a9300a632e21eb91f768759e071f7828326e7 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 16:21:31 +0300
Subject: [PATCH 24/40] Disable long test for now

---
 usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt
index df730b468c..6244a87621 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt
@@ -1,6 +1,7 @@
 package org.usvm.samples.operators
 
 import org.jacodb.ets.model.EtsScene
+import org.junit.jupiter.api.Disabled
 import org.usvm.api.TsTestValue
 import org.usvm.util.TsMethodTestRunner
 import org.usvm.util.toDouble
@@ -49,6 +50,7 @@ class Division : TsMethodTestRunner() {
         )
     }
 
+    @Disabled("Long running test")
     @Test
     fun testUnknownDivision() {
         val method = getMethod(className, "unknownDivision")

From 0b3aaa553960b234afa1a7afc441a32918060ad4 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 16:22:53 +0300
Subject: [PATCH 25/40] Store 'this' in register 0, and arguments in 1..n

---
 .../org/usvm/machine/expr/TsExprResolver.kt   |  2 +-
 .../usvm/machine/interpreter/TsInterpreter.kt | 23 +++++++++++--------
 .../kotlin/org/usvm/machine/state/TsState.kt  | 11 +++++----
 .../kotlin/org/usvm/util/TsTestResolver.kt    |  3 ++-
 4 files changed, 22 insertions(+), 17 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index b9258f11ca..8d6b46364c 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -420,7 +420,7 @@ class TsExprResolver(
                 check(executor.parameters.size <= 2) {
                     "Executor should have at most 2 parameters (resolve and reject), but it has ${executor.parameters.size} for $executor"
                 }
-                val args = executor.parameters.map { mkUndefinedValue() } + promise
+                val args = listOf(promise) + executor.parameters.map { mkUndefinedValue() }
                 // pushSortsForArguments(instance = null, args = emptyList(), localToIdx)
                 pushSortsForActualArguments(args)
                 memory.stack.push(args.toTypedArray(), executor.localsCount)
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 3ab20def7e..1b1d1010cd 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
@@ -332,6 +332,8 @@ class TsInterpreter(
             val numActual = stmt.args.size
             val numFormal = stmt.callee.parameters.size
 
+            args += stmt.instance
+
             // vararg call:
             // function f(x: any, ...args: any[]) {}
             //   f(1, 2, 3) -> f(1, [2, 3])
@@ -390,12 +392,10 @@ class TsInterpreter(
                 }
             }
 
-            check(args.size == numFormal) {
-                "Expected $numFormal arguments, got ${args.size}"
+            check(args.size - 1 == numFormal) {
+                "Expected $numFormal arguments, got ${args.size - 1} (not counting 'this')"
             }
 
-            args += stmt.instance
-
             // TODO: re-check push sorts for arguments
             pushSortsForActualArguments(args)
             callStack.push(stmt.callee, stmt.returnSite)
@@ -741,11 +741,11 @@ class TsInterpreter(
                 map[local.name]
             }
 
-            // Note: 'this' has index 'n'
-            is EtsThis -> method.parameters.size
+            // Note: 'this' has index 0
+            is EtsThis -> 0
 
-            // Note: arguments have indices from 0 to (n-1)
-            is EtsParameterRef -> local.index
+            // Note: arguments have indices from 1 to n
+            is EtsParameterRef -> local.index + 1
 
             else -> error("Unexpected local: $local")
         }
@@ -765,6 +765,7 @@ class TsInterpreter(
         // TODO check for statics
         val thisIdx = mapLocalToIdx(method, EtsThis(method.enclosingClass!!.type))
             ?: error("Cannot find index for 'this' in method: $method")
+        check(thisIdx == 0)
         val thisInstanceRef = mkRegisterStackLValue(addressSort, thisIdx)
         val thisRef = state.memory.read(thisInstanceRef).asExpr(addressSort)
 
@@ -775,14 +776,16 @@ class TsInterpreter(
         state.pathConstraints += state.memory.types.evalTypeEquals(thisRef, method.enclosingClass!!.type)
 
         method.parameters.forEachIndexed { i, param ->
+            val idx = i + 1 // +1 because 0 is reserved for `this`
+
             val ref by lazy {
-                val lValue = mkRegisterStackLValue(addressSort, i)
+                val lValue = mkRegisterStackLValue(addressSort, idx)
                 state.memory.read(lValue).asExpr(addressSort)
             }
 
             val parameterType = param.type
             if (parameterType is EtsRefType) {
-                val argLValue = mkRegisterStackLValue(addressSort, i)
+                val argLValue = mkRegisterStackLValue(addressSort, idx)
                 val ref = state.memory.read(argLValue).asExpr(addressSort)
                 if (parameterType is EtsArrayType) {
                     state.pathConstraints += state.memory.types.evalTypeEquals(ref, parameterType)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index 4950f153a8..88683d43a9 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -125,18 +125,19 @@ class TsState(
 
         // Note: first, push an empty map, then fill the arguments, and then the instance (this)
         pushLocalToSortStack()
-        argSorts.forEachIndexed { index, sort ->
-            saveSortForLocal(index, sort)
+        instanceSort?.let { saveSortForLocal(0, it) }
+        argSorts.forEachIndexed { i, sort ->
+            val idx = i + 1 // + 1 because 0 is reserved for `this`
+            saveSortForLocal(idx, sort)
         }
-        instanceSort?.let { saveSortForLocal(args.size, it) }
     }
 
     fun pushSortsForActualArguments(
         arguments: List<UExpr<*>>,
     ) {
         pushLocalToSortStack()
-        arguments.forEachIndexed { index, arg ->
-            saveSortForLocal(index, arg.sort)
+        arguments.forEachIndexed { idx, arg ->
+            saveSortForLocal(idx, arg.sort)
         }
     }
 
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
index 31d2cfdfa8..c6e7c5da2c 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -314,7 +314,8 @@ open class TsTestStateResolver(
     }
 
     fun resolveParameters(): List<TsTestValue> = with(ctx) {
-        method.parameters.mapIndexed { idx, param ->
+        method.parameters.mapIndexed { i, param ->
+            val idx = i + 1 // +1 because the register 0 is reserved for `this`
             val sort = typeToSort(param.type)
 
             if (sort is TsUnresolvedSort) {

From a5f1833aec770603f42080b55ab1f27686241e22 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 16:23:41 +0300
Subject: [PATCH 26/40] Cleanup

---
 usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt
index 618e8d2a5c..0c7ce64126 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt
@@ -7,11 +7,6 @@ import kotlin.test.Test
 
 class Async : TsMethodTestRunner() {
 
-    companion object {
-        private const val SDK_TYPESCRIPT_PATH = "/sdk/typescript"
-        private const val SDK_OHOS_PATH = "/sdk/ohos"
-    }
-
     private val className = this::class.simpleName!!
 
     override val scene: EtsScene = loadSampleScene(className)

From 3e879f46fdb56a4a819d5dd47b6da21302b8a621 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 16:28:33 +0300
Subject: [PATCH 27/40] Rename and refine async tests

---
 .../src/test/kotlin/org/usvm/samples/Async.kt   | 14 +++++++-------
 usvm-ts/src/test/resources/samples/Async.ts     | 17 ++++++-----------
 2 files changed, 13 insertions(+), 18 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt
index 0c7ce64126..c51dbb8ca6 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Async.kt
@@ -3,6 +3,7 @@ package org.usvm.samples
 import org.jacodb.ets.model.EtsScene
 import org.usvm.api.TsTestValue
 import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.eq
 import kotlin.test.Test
 
 class Async : TsMethodTestRunner() {
@@ -12,20 +13,19 @@ class Async : TsMethodTestRunner() {
     override val scene: EtsScene = loadSampleScene(className)
 
     @Test
-    fun `create and await promise`() {
-        val method = getMethod(className, "createAndAwaitPromise")
+    fun `await resolving promise`() {
+        val method = getMethod(className, "awaitResolvingPromise")
         discoverProperties<TsTestValue.TsNumber>(
             method = method,
-            { r -> r.number == 1.0 },
             invariants = arrayOf(
-                { r -> r.number != -1.0 },
+                { r -> r.number eq 42 },
             )
         )
     }
 
     @Test
-    fun `create and await rejecting promise`() {
-        val method = getMethod(className, "createAndAwaitRejectingPromise")
+    fun `await rejecting promise`() {
+        val method = getMethod(className, "awaitRejectingPromise")
         discoverProperties<TsTestValue>(
             method = method,
             { r -> r is TsTestValue.TsException },
@@ -38,7 +38,7 @@ class Async : TsMethodTestRunner() {
         discoverProperties<TsTestValue.TsNumber>(
             method = method,
             invariants = arrayOf(
-                { r -> r.number == 50.0 },
+                { r -> r.number eq 42 },
             )
         )
     }
diff --git a/usvm-ts/src/test/resources/samples/Async.ts b/usvm-ts/src/test/resources/samples/Async.ts
index 8f2d67c70c..ac3a966384 100644
--- a/usvm-ts/src/test/resources/samples/Async.ts
+++ b/usvm-ts/src/test/resources/samples/Async.ts
@@ -2,19 +2,14 @@
 // noinspection JSUnusedGlobalSymbols
 
 class Async {
-    createAndAwaitPromise(): number {
+    awaitResolvingPromise(): number {
         const promise = new Promise((resolve) => {
             resolve(42);
         });
-        const resolved = await promise;
-        if (resolved == 42) {
-            return 1;
-        } else {
-            return -1; // unreachable
-        }
+        return await promise; // 42
     }
 
-    createAndAwaitRejectingPromise(): number {
+    awaitRejectingPromise() {
         const promise = new Promise((resolve, reject) => {
             reject(new Error("An error occurred"));
         });
@@ -22,11 +17,11 @@ class Async {
     }
 
     awaitResolvedPromise(): number {
-        const promise = Promise.resolve(50);
-        return await promise; // 50
+        const promise = Promise.resolve(42);
+        return await promise; // 42
     }
 
-    awaitRejectedPromise(): number {
+    awaitRejectedPromise() {
         const promise = Promise.reject(new Error("An error occurred"));
         await promise; // exception
     }

From ee06f23cf95d49af8ee8d0dc52e114a2e09b3424 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 18:32:17 +0300
Subject: [PATCH 28/40] Add support for ptr-call-based resolve/reject

---
 usvm-core/src/main/kotlin/org/usvm/Context.kt |   2 +-
 .../main/kotlin/org/usvm/machine/TsContext.kt |  19 ++-
 .../org/usvm/machine/expr/TsExprResolver.kt   | 135 ++++++++++--------
 .../usvm/machine/interpreter/TsFunction.kt    |   9 ++
 .../usvm/machine/interpreter/TsInterpreter.kt |  11 +-
 .../kotlin/org/usvm/machine/state/TsState.kt  |  24 ++--
 6 files changed, 122 insertions(+), 78 deletions(-)
 create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt

diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt
index 47d688b98a..8ddaa88a80 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Context.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt
@@ -94,7 +94,7 @@ open class UContext<USizeSort : USort>(
     val addressSort: UAddressSort = mkUninterpretedSort("Address")
     val nullRef: UNullRef = UNullRef(this)
 
-    fun mkNullRef(): USymbolicHeapRef {
+    open fun mkNullRef(): USymbolicHeapRef {
         return nullRef
     }
 
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 f2844f33ee..b80d18a45f 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -25,7 +25,9 @@ import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.UNullRef
 import org.usvm.USort
+import org.usvm.USymbolicHeapRef
 import org.usvm.api.allocateConcreteRef
 import org.usvm.api.initializeArray
 import org.usvm.api.typeStreamOf
@@ -58,11 +60,16 @@ class TsContext(
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
+    @Deprecated("Use mkUndefinedValue() or mkTsNullValue() instead")
+    override fun mkNullRef(): USymbolicHeapRef {
+        error("Use mkUndefinedValue() or mkTsNullValue() instead of mkNullRef() in TS context")
+    }
+
     /**
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.
      */
-    private val undefinedValue: UHeapRef = mkNullRef()
+    private val undefinedValue: UHeapRef = nullRef
     fun mkUndefinedValue(): UHeapRef = undefinedValue
 
     private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
@@ -181,7 +188,7 @@ class TsContext(
     }
 
     fun createFakeObjectRef(): UConcreteHeapRef {
-        val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET
+        val address = addressCounter.freshAllocatedAddress() + MAGIC_OFFSET
         return mkConcreteHeapRef(address)
     }
 
@@ -263,6 +270,14 @@ class TsContext(
             ref
         }
     }
+
+    // This is a special function that resolves promises in the interpreter.
+    // It is not a real function in the code, but we need it to handle promise resolution.
+    val resolveFunctionRef: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
+
+    // This is a special function that rejects promises in the interpreter.
+    // It is not a real function in the code, but we need it to handle promise rejection.
+    val rejectFunctionRef: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
 }
 
 class Constants {
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 8d6b46364c..6558405b09 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -29,7 +29,6 @@ import org.jacodb.ets.model.EtsEntity
 import org.jacodb.ets.model.EtsEqExpr
 import org.jacodb.ets.model.EtsExpExpr
 import org.jacodb.ets.model.EtsFieldSignature
-import org.jacodb.ets.model.EtsFileSignature
 import org.jacodb.ets.model.EtsFunctionType
 import org.jacodb.ets.model.EtsGlobalRef
 import org.jacodb.ets.model.EtsGtEqExpr
@@ -104,6 +103,7 @@ import org.usvm.api.mockMethodCall
 import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.isStaticHeapRef
 import org.usvm.machine.Constants
 import org.usvm.machine.TsConcreteMethodCallStmt
 import org.usvm.machine.TsContext
@@ -412,16 +412,38 @@ class TsExprResolver(
                     ?: error("Await expression should have a promise executor, but it is not set for $promise")
             }
             check(executor.cfg.stmts.isNotEmpty())
-            scope.doWithState {
-                // Note: arguments for 'executor' are:
-                //   - `resolve`, if present in parameters
-                //   - `reject`, if present in parameters
-                //   - `promise` == "this", should be the last
-                check(executor.parameters.size <= 2) {
-                    "Executor should have at most 2 parameters (resolve and reject), but it has ${executor.parameters.size} for $executor"
+
+            val args: MutableList<UExpr<*>> = mutableListOf()
+
+            // 'this':
+            // args += mkUndefinedValue()
+            args += mkConcreteHeapRef(addressCounter.freshStaticAddress())
+
+            val params = executor.parameters.toMutableList()
+            if (params.isNotEmpty() && params[0].type is EtsLexicalEnvType) {
+                params.removeFirst()
+                // TODO: handle closures
+                args += mkUndefinedValue()
+            }
+            if (params.isNotEmpty()) {
+                args += resolveFunctionRef
+                scope.doWithState {
+                    setBoundThis(resolveFunctionRef, promise)
                 }
-                val args = listOf(promise) + executor.parameters.map { mkUndefinedValue() }
-                // pushSortsForArguments(instance = null, args = emptyList(), localToIdx)
+                if (params.size >= 2) {
+                    args += rejectFunctionRef
+                    scope.doWithState {
+                        setBoundThis(rejectFunctionRef, promise)
+                    }
+                    if (params.size >= 3) {
+                        error(
+                            "Promise executor should have at most 3 parameters" +
+                                " (closures, resolve, reject), but got ${params.size}"
+                        )
+                    }
+                }
+            }
+            scope.doWithState {
                 pushSortsForActualArguments(args)
                 memory.stack.push(args.toTypedArray(), executor.localsCount)
                 registerCallee(currentStatement, executor.cfg)
@@ -858,43 +880,6 @@ class TsExprResolver(
             return handleBooleanConverter(expr)
         }
 
-        // TODO: this should be handled in visit(AwaitExpr)
-        // Note: in the new IR, calls to "resolve" and "reject" methods were fixed to be PtrCall, so we
-        //  cannot handle them here. Instead, we should rely on the common handling of PtrCall, that is,
-        //  allocate new refs and associate them with SYNTHETIC "resolve" and "reject" methods.
-        //
-        // if (expr.callee.name in listOf("resolve", "reject")) {
-        //     val promise = resolve(
-        //         EtsThis(
-        //             EtsClassType(
-        //                 EtsClassSignature(
-        //                     "Promise",
-        //                     EtsFileSignature("typescript", "lib.es5.d.ts")
-        //                 )
-        //             )
-        //         )
-        //     )?.asExpr(addressSort) ?: return null
-        //     check(isAllocatedConcreteHeapRef(promise)) {
-        //         "Promise instance should be allocated, but it is not: $promise"
-        //     }
-        //     val newState = when (expr.callee.name) {
-        //         "resolve" -> PromiseState.FULFILLED
-        //         "reject" -> PromiseState.REJECTED
-        //         else -> error("Unexpected: $expr")
-        //     }
-        //     check(expr.args.size == 1) {
-        //         "${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}"
-        //     }
-        //     val value = resolve(expr.args.single()) ?: return null
-        //     val fakeValue = value.toFakeObject(scope)
-        //     scope.doWithState {
-        //         markResolved(promise.asExpr(addressSort))
-        //         setPromiseState(promise, newState)
-        //         setResolvedValue(promise.asExpr(addressSort), fakeValue)
-        //     }
-        //     return mkUndefinedValue()
-        // }
-
         return when (val result = scope.calcOnState { methodResult }) {
             is TsMethodResult.Success -> {
                 scope.doWithState { methodResult = TsMethodResult.NoCall }
@@ -978,8 +963,8 @@ class TsExprResolver(
         return TsResolutionResult.create(methods)
     }
 
-    override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? {
-        return when (val result = scope.calcOnState { methodResult }) {
+    override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? = with(ctx) {
+        when (val result = scope.calcOnState { methodResult }) {
             is TsMethodResult.Success -> {
                 scope.doWithState { methodResult = TsMethodResult.NoCall }
                 result.value
@@ -992,15 +977,46 @@ class TsExprResolver(
             is TsMethodResult.NoCall -> {
                 val ptr = resolve(expr.ptr) ?: return null
 
-                if (isAllocatedConcreteHeapRef(ptr)) {
-                    val callee = scope.calcOnState {
-                        associatedMethod[ptr] ?: error("No associated methods for ptr: $ptr")
+                if (isStaticHeapRef(ptr)) {
+                    // Handle 'resolve' and 'reject' function call
+                    if (ptr === resolveFunctionRef || ptr === rejectFunctionRef) {
+                        val promise = scope.calcOnState {
+                            boundThis[ptr] ?: error("No bound 'this' for ptr: $ptr")
+                        }
+                        check(isAllocatedConcreteHeapRef(promise)) {
+                            "Promise instance should be allocated, but it is not: $promise"
+                        }
+                        val newState = when (ptr) {
+                            resolveFunctionRef -> PromiseState.FULFILLED
+                            rejectFunctionRef -> PromiseState.REJECTED
+                            else -> error("Unexpected ptr: $ptr")
+                        }
+                        check(expr.args.size == 1) {
+                            "${
+                                when (ptr) {
+                                    resolveFunctionRef -> "resolve"
+                                    rejectFunctionRef -> "reject"
+                                    else -> error("Unexpected ptr: $ptr")
+                                }
+                            }() should have exactly one argument, but got ${expr.args.size}"
+                        }
+                        val value = resolve(expr.args.single()) ?: return null
+                        val fakeValue = value.toFakeObject(scope)
+                        scope.doWithState {
+                            markResolved(promise.asExpr(addressSort))
+                            setPromiseState(promise, newState)
+                            setResolvedValue(promise.asExpr(addressSort), fakeValue)
+                        }
+                        return mkUndefinedValue()
                     }
 
+                    val callee = scope.calcOnState {
+                        associatedFunction[ptr] ?: error("No associated methods for ptr: $ptr")
+                    }
                     val resolvedArgs = expr.args.map { resolve(it) ?: return null }
                     val concreteCall = TsConcreteMethodCallStmt(
-                        callee = callee,
-                        instance = ptr,
+                        callee = callee.method,
+                        instance = callee.thisInstance ?: ctx.mkUndefinedValue(),
                         args = resolvedArgs,
                         returnSite = scope.calcOnState { lastStmt },
                     )
@@ -1355,7 +1371,7 @@ class TsExprResolver(
 
     override fun visit(value: EtsClosureFieldRef): UExpr<out USort>? = with(ctx) {
         val obj = resolve(value.base) ?: return null
-        check(isAllocatedConcreteHeapRef(obj)) {
+        check(isStaticHeapRef(obj)) {
             "Closure object should be a concrete heap reference, but got $obj"
         }
 
@@ -1454,7 +1470,7 @@ class TsSimpleValueResolver(
     private val localToIdx: (EtsMethod, EtsValue) -> Int?,
 ) : EtsValue.Visitor<UExpr<out USort>?> {
 
-    private fun resolveLocal(local: EtsValue): UExpr<*> {
+    private fun resolveLocal(local: EtsValue): UExpr<*> = with(ctx) {
         val currentMethod = scope.calcOnState { lastEnteredMethod }
         val entrypoint = scope.calcOnState { entrypoint }
 
@@ -1474,7 +1490,8 @@ class TsSimpleValueResolver(
                 }
                 val type = local.type
                 check(type is EtsLexicalEnvType)
-                val obj = scope.calcOnState { memory.allocConcrete(type) }
+                // val obj = scope.calcOnState { memory.allocConcrete(type) }
+                val obj = mkConcreteHeapRef(addressCounter.freshStaticAddress())
                 for (captured in type.closures) {
                     val resolvedCaptured = resolveLocal(captured)
                     val lValue = mkFieldLValue(resolvedCaptured.sort, obj, captured.name)
@@ -1531,7 +1548,7 @@ class TsSimpleValueResolver(
         }
 
         // arguments and this for the first stack frame
-        return when (sort) {
+        when (sort) {
             is UBoolSort -> {
                 val lValue = mkRegisterStackLValue(sort, localIdx)
                 scope.calcOnState { memory.read(lValue) }
@@ -1585,7 +1602,7 @@ class TsSimpleValueResolver(
             )
             val methods = ctx.resolveEtsMethods(sig)
             val method = methods.single()
-            val ref = scope.calcOnState { getAssociatedMethod(method) }
+            val ref = scope.calcOnState { getMethodRef(method) }
             return ref
         }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt
new file mode 100644
index 0000000000..928ffccbfa
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsFunction.kt
@@ -0,0 +1,9 @@
+package org.usvm.machine.interpreter
+
+import org.jacodb.ets.model.EtsMethod
+import org.usvm.UHeapRef
+
+class TsFunction(
+    val method: EtsMethod,
+    val thisInstance: UHeapRef?,
+)
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 1b1d1010cd..5e1d7a2dcc 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
@@ -678,21 +678,16 @@ class TsInterpreter(
 
     private fun visitCallStmt(scope: TsStepScope, stmt: EtsCallStmt) {
         if (scope.calcOnState { methodResult } is TsMethodResult.Success) {
-            // TODO: seems like USVM will never finish going back to this state even when there is no next stmt,
-            //  since the state is not dead, and the method result is not reset...
-            val nextStmt = stmt.nextStmt ?: return
             scope.doWithState {
                 methodResult = TsMethodResult.NoCall
+            }
+            val nextStmt = stmt.nextStmt ?: return
+            scope.doWithState {
                 newStmt(nextStmt)
             }
             return
         }
 
-        if (stmt.expr is EtsPtrCallExpr) {
-            mockMethodCall(scope, stmt.expr.callee)
-            return
-        }
-
         if (tsOptions.interproceduralAnalysis) {
             val exprResolver = exprResolverWithScope(scope)
             exprResolver.resolve(stmt.expr) ?: return
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index 88683d43a9..e105560fbb 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -8,12 +8,12 @@ import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsType
-import org.jacodb.ets.model.EtsUnknownType
 import org.jacodb.ets.model.EtsValue
 import org.usvm.PathNode
 import org.usvm.UCallStack
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.UState
 import org.usvm.api.targets.TsTarget
@@ -24,6 +24,7 @@ import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.constraints.UPathConstraints
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.PromiseState
+import org.usvm.machine.interpreter.TsFunction
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemory
 import org.usvm.model.UModelBase
@@ -58,10 +59,10 @@ class TsState(
     var discoveredCallees: UPersistentHashMap<Pair<EtsStmt, Int>, EtsBlockCfg> = persistentHashMapOf(),
     var promiseState: UPersistentHashMap<UConcreteHeapRef, PromiseState> = persistentHashMapOf(),
     var promiseExecutor: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
-    // TODO: use normal naming
     var methodToRef: UPersistentHashMap<EtsMethod, UConcreteHeapRef> = persistentHashMapOf(),
-    var associatedMethod: UPersistentHashMap<UConcreteHeapRef, EtsMethod> = persistentHashMapOf(),
+    var associatedFunction: UPersistentHashMap<UConcreteHeapRef, TsFunction> = persistentHashMapOf(),
     var closureObject: UPersistentHashMap<String, UConcreteHeapRef> = persistentHashMapOf(),
+    var boundThis: UPersistentHashMap<UConcreteHeapRef, UHeapRef> = persistentHashMapOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,
@@ -163,14 +164,14 @@ class TsState(
         promiseExecutor = promiseExecutor.put(promise, method, ownership)
     }
 
-    fun getAssociatedMethod(
+    fun getMethodRef(
         method: EtsMethod,
+        thisInstance: UHeapRef? = null,
     ): UConcreteHeapRef {
         val (updated, result) = methodToRef.getOrPut(method, ownership) {
-            // TODO: what type should we use here?
-            memory.allocConcrete(EtsUnknownType)
+            ctx.mkConcreteHeapRef(ctx.addressCounter.freshStaticAddress())
         }
-        associatedMethod = associatedMethod.put(result, method, ownership)
+        associatedFunction = associatedFunction.put(result, TsFunction(method, thisInstance), ownership)
         methodToRef = updated
         return result
     }
@@ -182,6 +183,13 @@ class TsState(
         closureObject = closureObject.put(name, closure, ownership)
     }
 
+    fun setBoundThis(
+        instance: UConcreteHeapRef,
+        thisRef: UHeapRef,
+    ) {
+        boundThis = boundThis.put(instance, thisRef, ownership)
+    }
+
     override fun clone(newConstraints: UPathConstraints<EtsType>?): TsState {
         val newThisOwnership = MutabilityOwnership()
         val cloneOwnership = MutabilityOwnership()
@@ -212,7 +220,7 @@ class TsState(
             promiseState = promiseState,
             promiseExecutor = promiseExecutor,
             methodToRef = methodToRef,
-            associatedMethod = associatedMethod,
+            associatedFunction = associatedFunction,
             closureObject = closureObject,
         )
     }

From 3f6b551fb088b624a94adaae71bb4d5891f0c5f0 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 18:32:54 +0300
Subject: [PATCH 29/40] Bump ArkAnalyzer to branch 'neo/2025-07-18'

---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3d5f07e2cc..96d24f6b8a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -158,7 +158,7 @@ jobs:
           DEST_DIR="arkanalyzer"
           MAX_RETRIES=10
           RETRY_DELAY=3  # Delay between retries in seconds  
-          BRANCH="neo/2025-07-16"
+          BRANCH="neo/2025-07-18"
 
           for ((i=1; i<=MAX_RETRIES; i++)); do
               git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

From 8f0ff6d9d18ca1676c44d23e2a03056703f8278d Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 18:42:48 +0300
Subject: [PATCH 30/40] Nothing

---
 usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 b80d18a45f..514f23225b 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -61,7 +61,7 @@ class TsContext(
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
     @Deprecated("Use mkUndefinedValue() or mkTsNullValue() instead")
-    override fun mkNullRef(): USymbolicHeapRef {
+    override fun mkNullRef(): Nothing {
         error("Use mkUndefinedValue() or mkTsNullValue() instead of mkNullRef() in TS context")
     }
 

From 1fadffedf8b33aa2acd437b337adf93eac21fe13 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Fri, 18 Jul 2025 18:43:10 +0300
Subject: [PATCH 31/40] Format

---
 usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt           | 2 --
 .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt   | 1 -
 2 files changed, 3 deletions(-)

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 514f23225b..add8864924 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -25,9 +25,7 @@ import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.UHeapRef
-import org.usvm.UNullRef
 import org.usvm.USort
-import org.usvm.USymbolicHeapRef
 import org.usvm.api.allocateConcreteRef
 import org.usvm.api.initializeArray
 import org.usvm.api.typeStreamOf
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 5e1d7a2dcc..463aa09664 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
@@ -17,7 +17,6 @@ import org.jacodb.ets.model.EtsNopStmt
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
 import org.jacodb.ets.model.EtsParameterRef
-import org.jacodb.ets.model.EtsPtrCallExpr
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsReturnStmt
 import org.jacodb.ets.model.EtsStaticFieldRef

From 190d1f6a3c3a6af26e20dd162de73577f79fe41f Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 4 Aug 2025 18:34:48 +0300
Subject: [PATCH 32/40] Use allocated ref for closures

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt  | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 6558405b09..f8e7804ede 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -1371,7 +1371,7 @@ class TsExprResolver(
 
     override fun visit(value: EtsClosureFieldRef): UExpr<out USort>? = with(ctx) {
         val obj = resolve(value.base) ?: return null
-        check(isStaticHeapRef(obj)) {
+        check(isAllocatedConcreteHeapRef(obj)) {
             "Closure object should be a concrete heap reference, but got $obj"
         }
 
@@ -1490,8 +1490,7 @@ class TsSimpleValueResolver(
                 }
                 val type = local.type
                 check(type is EtsLexicalEnvType)
-                // val obj = scope.calcOnState { memory.allocConcrete(type) }
-                val obj = mkConcreteHeapRef(addressCounter.freshStaticAddress())
+                val obj = allocateConcreteRef()
                 for (captured in type.closures) {
                     val resolvedCaptured = resolveLocal(captured)
                     val lValue = mkFieldLValue(resolvedCaptured.sort, obj, captured.name)

From c4690211cd5db380e088b0063087028498a4459d Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 16:10:24 +0300
Subject: [PATCH 33/40] Use allocated ref, improve comment

---
 usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt     | 8 ++++----
 .../main/kotlin/org/usvm/machine/expr/TsExprResolver.kt   | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

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 add8864924..9a1d5917d0 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -269,13 +269,13 @@ class TsContext(
         }
     }
 
-    // This is a special function that resolves promises in the interpreter.
+    // This is an identifier for a special function representing the 'resolve' function used in promises.
     // It is not a real function in the code, but we need it to handle promise resolution.
-    val resolveFunctionRef: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
+    val resolveFunctionRef: UConcreteHeapRef = allocateConcreteRef()
 
-    // This is a special function that rejects promises in the interpreter.
+    // This is an identifier for a special function representing the 'reject' function used in promises.
     // It is not a real function in the code, but we need it to handle promise rejection.
-    val rejectFunctionRef: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
+    val rejectFunctionRef: UConcreteHeapRef = allocateConcreteRef()
 }
 
 class Constants {
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index f8e7804ede..c37f493599 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -977,7 +977,7 @@ class TsExprResolver(
             is TsMethodResult.NoCall -> {
                 val ptr = resolve(expr.ptr) ?: return null
 
-                if (isStaticHeapRef(ptr)) {
+                if (isAllocatedConcreteHeapRef(ptr)) {
                     // Handle 'resolve' and 'reject' function call
                     if (ptr === resolveFunctionRef || ptr === rejectFunctionRef) {
                         val promise = scope.calcOnState {

From f8772bc10d4af37b43cef7f89e9379b5b7223103 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 16:35:30 +0300
Subject: [PATCH 34/40] Pass undefined as 'this' in executor

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt  | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index c37f493599..43e4d40814 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -415,9 +415,8 @@ class TsExprResolver(
 
             val args: MutableList<UExpr<*>> = mutableListOf()
 
-            // 'this':
-            // args += mkUndefinedValue()
-            args += mkConcreteHeapRef(addressCounter.freshStaticAddress())
+            // Executor lambda does not have 'this', so we fill it with 'undefined':
+            args += mkUndefinedValue()
 
             val params = executor.parameters.toMutableList()
             if (params.isNotEmpty() && params[0].type is EtsLexicalEnvType) {

From e51e8a292649fab1e40a303297a37ee9c6f82cc7 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 16:42:44 +0300
Subject: [PATCH 35/40] Cleanup imports

---
 usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 1 -
 1 file changed, 1 deletion(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 43e4d40814..d8fd19c26b 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -103,7 +103,6 @@ import org.usvm.api.mockMethodCall
 import org.usvm.dataflow.ts.infer.tryGetKnownType
 import org.usvm.dataflow.ts.util.type
 import org.usvm.isAllocatedConcreteHeapRef
-import org.usvm.isStaticHeapRef
 import org.usvm.machine.Constants
 import org.usvm.machine.TsConcreteMethodCallStmt
 import org.usvm.machine.TsContext

From 0462c439533cc1a87cefa2f7f45cc85ffdc435ab Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 16:49:19 +0300
Subject: [PATCH 36/40] Use allocated ref for lambdas

---
 usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
index e105560fbb..1de4a84b83 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -16,6 +16,7 @@ import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.UState
+import org.usvm.api.allocateConcreteRef
 import org.usvm.api.targets.TsTarget
 import org.usvm.collections.immutable.getOrPut
 import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
@@ -168,9 +169,7 @@ class TsState(
         method: EtsMethod,
         thisInstance: UHeapRef? = null,
     ): UConcreteHeapRef {
-        val (updated, result) = methodToRef.getOrPut(method, ownership) {
-            ctx.mkConcreteHeapRef(ctx.addressCounter.freshStaticAddress())
-        }
+        val (updated, result) = methodToRef.getOrPut(method, ownership) { ctx.allocateConcreteRef() }
         associatedFunction = associatedFunction.put(result, TsFunction(method, thisInstance), ownership)
         methodToRef = updated
         return result

From 062a850c3b1e40d5a86efd7124989fa22a5a270b Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 17:09:23 +0300
Subject: [PATCH 37/40] Use non-local jacodb

---
 buildSrc/src/main/kotlin/Dependencies.kt |  2 +-
 settings.gradle.kts                      | 31 ++++++++++++------------
 2 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index fc2953acb4..822ef6b1e1 100644
--- a/buildSrc/src/main/kotlin/Dependencies.kt
+++ b/buildSrc/src/main/kotlin/Dependencies.kt
@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "081adc271e"
+    const val jacodb = "e8347c557c"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 1dc120c720..6af778f65f 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -55,19 +55,18 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons"
 // Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink.
 // As a workaround, we convert it to a real absolute path.
 // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756
-
-val jacodbPath = file("jacodb").takeIf { it.exists() }
-    ?: file("../jacodb").takeIf { it.exists() }
-    ?: error("Local JacoDB directory not found")
-includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) {
-    dependencySubstitution {
-        all {
-            val requested = requested
-            if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") {
-                val targetProject = ":${requested.module}"
-                useTarget(project(targetProject))
-                logger.info("Substituting ${requested.group}:${requested.module} with $targetProject")
-            }
-        }
-    }
-}
+// val jacodbPath = file("jacodb").takeIf { it.exists() }
+//     ?: file("../jacodb").takeIf { it.exists() }
+//     ?: error("Local JacoDB directory not found")
+// includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) {
+//     dependencySubstitution {
+//         all {
+//             val requested = requested
+//             if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") {
+//                 val targetProject = ":${requested.module}"
+//                 useTarget(project(targetProject))
+//                 logger.info("Substituting ${requested.group}:${requested.module} with $targetProject")
+//             }
+//         }
+//     }
+// }

From f906c3e35301888bdf9436bb0207ba3679ce0e89 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 17:09:34 +0300
Subject: [PATCH 38/40] Extract processing functions

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 116 ++++++++++--------
 1 file changed, 64 insertions(+), 52 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index d8fd19c26b..5e9c023951 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -878,66 +878,38 @@ class TsExprResolver(
             return handleBooleanConverter(expr)
         }
 
-        return when (val result = scope.calcOnState { methodResult }) {
-            is TsMethodResult.Success -> {
-                scope.doWithState { methodResult = TsMethodResult.NoCall }
-                result.value
-            }
+        val result = scope.calcOnState { methodResult }
 
-            is TsMethodResult.TsException -> {
-                error("Exception should be handled earlier")
-            }
+        if (result is TsMethodResult.Success) {
+            scope.doWithState { methodResult = TsMethodResult.NoCall }
+            return result.value
+        }
 
-            is TsMethodResult.NoCall -> {
-                when (val resolved = resolveStaticMethod(expr.callee)) {
-                    TsResolutionResult.Empty -> {
-                        logger.error { "Could not resolve static call: ${expr.callee}" }
-                        scope.assert(falseExpr)
-                    }
+        if (result is TsMethodResult.TsException) {
+            error("Exception should be handled earlier")
+        }
 
-                    // Static virtual call
-                    is TsResolutionResult.Ambiguous -> {
-                        val resolvedArgs = expr.args.map { resolve(it) ?: return null }
-                        val staticProperties = resolved.properties.take(Constants.STATIC_METHODS_FORK_LIMIT)
-                        val staticInstances = scope.calcOnState {
-                            staticProperties.map { getStaticInstance(it.enclosingClass!!) }
-                        }
-                        val concreteCalls = staticProperties.mapIndexed { index, value ->
-                            TsConcreteMethodCallStmt(
-                                callee = value,
-                                instance = staticInstances[index],
-                                args = resolvedArgs,
-                                returnSite = scope.calcOnState { lastStmt }
-                            )
-                        }
-                        val blocks: List<Pair<UBoolExpr, TsState.() -> Unit>> = concreteCalls.map { stmt ->
-                            mkTrue() to { newStmt(stmt) }
-                        }
-                        scope.forkMulti(blocks)
-                    }
+        check(result is TsMethodResult.NoCall)
 
-                    is TsResolutionResult.Unique -> {
-                        val instance = scope.calcOnState {
-                            getStaticInstance(resolved.property.enclosingClass!!)
-                        }
-                        val args = expr.args.map { resolve(it) ?: return null }
-                        val concreteCall = TsConcreteMethodCallStmt(
-                            callee = resolved.property,
-                            instance = instance,
-                            args = args,
-                            returnSite = scope.calcOnState { lastStmt },
-                        )
-                        scope.doWithState { newStmt(concreteCall) }
-                    }
-                }
-                null
+        when (val resolved = resolveStaticMethod(expr.callee)) {
+            is TsResolutionResult.Empty -> {
+                logger.error { "Could not resolve static call: ${expr.callee}" }
+                scope.assert(falseExpr)
+            }
+
+            is TsResolutionResult.Ambiguous -> {
+                processAmbiguousStaticMethod(resolved, expr)
+            }
+
+            is TsResolutionResult.Unique -> {
+                processUniqueStaticMethod(resolved, expr)
             }
         }
+
+        null
     }
 
-    private fun resolveStaticMethod(
-        method: EtsMethodSignature,
-    ): TsResolutionResult<EtsMethod> {
+    private fun resolveStaticMethod(method: EtsMethodSignature): TsResolutionResult<EtsMethod> {
         // Perfect signature:
         if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
             val classes = hierarchy.classesForType(EtsClassType(method.enclosingClass))
@@ -961,6 +933,46 @@ class TsExprResolver(
         return TsResolutionResult.create(methods)
     }
 
+    private fun processAmbiguousStaticMethod(
+        resolved: TsResolutionResult.Ambiguous<EtsMethod>,
+        expr: EtsStaticCallExpr,
+    ) = with(ctx) {
+        val resolvedArgs = expr.args.map { resolve(it) ?: return }
+        val staticProperties = resolved.properties.take(Constants.STATIC_METHODS_FORK_LIMIT)
+        val staticInstances = scope.calcOnState {
+            staticProperties.map { getStaticInstance(it.enclosingClass!!) }
+        }
+        val concreteCalls = staticProperties.mapIndexed { index, value ->
+            TsConcreteMethodCallStmt(
+                callee = value,
+                instance = staticInstances[index],
+                args = resolvedArgs,
+                returnSite = scope.calcOnState { lastStmt }
+            )
+        }
+        val blocks: List<Pair<UBoolExpr, TsState.() -> Unit>> = concreteCalls.map { stmt ->
+            mkTrue() to { newStmt(stmt) }
+        }
+        scope.forkMulti(blocks)
+    }
+
+    private fun processUniqueStaticMethod(
+        resolved: TsResolutionResult.Unique<EtsMethod>,
+        expr: EtsStaticCallExpr,
+    ) = with(ctx) {
+        val instance = scope.calcOnState {
+            getStaticInstance(resolved.property.enclosingClass!!)
+        }
+        val args = expr.args.map { resolve(it) ?: return }
+        val concreteCall = TsConcreteMethodCallStmt(
+            callee = resolved.property,
+            instance = instance,
+            args = args,
+            returnSite = scope.calcOnState { lastStmt },
+        )
+        scope.doWithState { newStmt(concreteCall) }
+    }
+
     override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? = with(ctx) {
         when (val result = scope.calcOnState { methodResult }) {
             is TsMethodResult.Success -> {

From cf978baf7a87175b0a17f78df0cad30aa2874a10 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 17:10:08 +0300
Subject: [PATCH 39/40] Remove with(ctx)

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 5e9c023951..b7bb27937f 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -936,7 +936,7 @@ class TsExprResolver(
     private fun processAmbiguousStaticMethod(
         resolved: TsResolutionResult.Ambiguous<EtsMethod>,
         expr: EtsStaticCallExpr,
-    ) = with(ctx) {
+    ) {
         val resolvedArgs = expr.args.map { resolve(it) ?: return }
         val staticProperties = resolved.properties.take(Constants.STATIC_METHODS_FORK_LIMIT)
         val staticInstances = scope.calcOnState {
@@ -951,7 +951,7 @@ class TsExprResolver(
             )
         }
         val blocks: List<Pair<UBoolExpr, TsState.() -> Unit>> = concreteCalls.map { stmt ->
-            mkTrue() to { newStmt(stmt) }
+            ctx.mkTrue() to { newStmt(stmt) }
         }
         scope.forkMulti(blocks)
     }
@@ -959,7 +959,7 @@ class TsExprResolver(
     private fun processUniqueStaticMethod(
         resolved: TsResolutionResult.Unique<EtsMethod>,
         expr: EtsStaticCallExpr,
-    ) = with(ctx) {
+    ) {
         val instance = scope.calcOnState {
             getStaticInstance(resolved.property.enclosingClass!!)
         }

From affb666e0e587e650cc2d863e564957c8f1c0c52 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 5 Aug 2025 17:20:31 +0300
Subject: [PATCH 40/40] Bump jacodb, remove local jacodb setup on CI

---
 .github/workflows/ci.yml                 | 35 ------------------------
 buildSrc/src/main/kotlin/Dependencies.kt |  2 +-
 2 files changed, 1 insertion(+), 36 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 96d24f6b8a..a82636cfac 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -18,13 +18,6 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
-      - name: Checkout local jacodb
-        uses: actions/checkout@v4
-        with:
-          repository: UnitTestBot/jacodb
-          ref: lipen/lexical-env-type
-          path: jacodb
-
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -52,13 +45,6 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
-      - name: Checkout local jacodb
-        uses: actions/checkout@v4
-        with:
-          repository: UnitTestBot/jacodb
-          ref: lipen/lexical-env-type
-          path: jacodb
-
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -88,13 +74,6 @@ jobs:
           # 'usvm-python/cpythonadapter/cpython' is a submodule
           submodules: true
 
-      - name: Checkout local jacodb
-        uses: actions/checkout@v4
-        with:
-          repository: UnitTestBot/jacodb
-          ref: lipen/lexical-env-type
-          path: jacodb
-
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -128,13 +107,6 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
-      - name: Checkout local jacodb
-        uses: actions/checkout@v4
-        with:
-          repository: UnitTestBot/jacodb
-          ref: lipen/lexical-env-type
-          path: jacodb
-
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
@@ -196,13 +168,6 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
-      - name: Checkout local jacodb
-        uses: actions/checkout@v4
-        with:
-          repository: UnitTestBot/jacodb
-          ref: lipen/lexical-env-type
-          path: jacodb
-
       - name: Setup Java JDK
         uses: actions/setup-java@v4
         with:
diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index 822ef6b1e1..1e312d34fe 100644
--- a/buildSrc/src/main/kotlin/Dependencies.kt
+++ b/buildSrc/src/main/kotlin/Dependencies.kt
@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "e8347c557c"
+    const val jacodb = "5acbadfed0"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"