From ccc157d8f78db86d73414b53f0c39f74d576d8ab Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Thu, 29 May 2025 18:03:27 +0300
Subject: [PATCH 01/69] Hacks

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 85 +++++++++++++++----
 .../usvm/machine/interpreter/TsInterpreter.kt | 50 +++++++++--
 .../kotlin/org/usvm/util/EtsFieldResolver.kt  | 32 ++++---
 .../test/kotlin/org/usvm/project/Photos.kt    | 19 +++++
 .../org/usvm/util/TsMethodTestRunner.kt       |  2 +-
 5 files changed, 147 insertions(+), 41 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 082324130..2262c26ad 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
@@ -106,8 +106,8 @@ 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.EtsFieldResolutionResult
 import org.usvm.util.EtsHierarchy
+import org.usvm.util.EtsPropertyResolution
 import org.usvm.util.createFakeField
 import org.usvm.util.isResolved
 import org.usvm.util.mkArrayIndexLValue
@@ -116,6 +116,7 @@ import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
 import org.usvm.util.resolveEtsField
 import org.usvm.util.throwExceptionWithoutStackFrameDrop
+import org.usvm.util.type
 
 private val logger = KotlinLogging.logger {}
 
@@ -528,6 +529,17 @@ class TsExprResolver(
             }
         }
 
+        if (expr.callee.name == "\$r") {
+            // TODO hack
+            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 }
@@ -539,21 +551,51 @@ class TsExprResolver(
             }
 
             is TsMethodResult.NoCall -> {
-                // TODO: spawn VirtualCall when method resolution fails
-                val method = resolveStaticMethod(expr.callee)
+                val resolutionResult = resolveStaticMethod(expr.callee)
 
-                if (method == null) {
+                if (resolutionResult is EtsPropertyResolution.Empty) {
                     logger.error { "Could not resolve static call: ${expr.callee}" }
                     scope.assert(falseExpr)
                     return null
                 }
 
-                val instance = scope.calcOnState { getStaticInstance(method.enclosingClass!!) }
+                // static virtual call
+                if (resolutionResult is EtsPropertyResolution.Ambiguous) {
+                    val resolvedArgs = expr.args.map { resolve(it) ?: return null }
+
+                    val staticInstances = scope.calcOnState {
+                        resolutionResult.properties.take(1).map { getStaticInstance(it.enclosingClass!!) }
+                    }
+
+                    // TODO take 1 is an error
+                    val concreteCalls = resolutionResult.properties.take(1).mapIndexed { index, value ->
+                        TsConcreteMethodCallStmt(
+                            callee = value,
+                            instance = staticInstances[index],
+                            args = resolvedArgs,
+                            returnSite = scope.calcOnState { lastStmt }
+                        )
+                    }
+
+                    val blocks = concreteCalls.map {
+                        ctx.mkTrue() to { state: TsState -> state.newStmt(it) }
+                    } // TODO error with true Expr
+
+                    logger.warn { "Forking on ${blocks.size} branches" }
+
+                    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 = method,
+                    callee = resolutionResult.property,
                     instance = instance,
                     args = resolvedArgs,
                     returnSite = scope.calcOnState { lastStmt },
@@ -567,25 +609,22 @@ class TsExprResolver(
 
     private fun resolveStaticMethod(
         method: EtsMethodSignature,
-    ): EtsMethod? {
+    ): EtsPropertyResolution<out EtsMethod> {
         // Perfect signature:
         if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
             val classes = ctx.scene.projectAndSdkClasses.filter { it.name == method.enclosingClass.name }
-            if (classes.size != 1) return null
+            if (classes.size != 1) return EtsPropertyResolution.Empty
             val clazz = classes.single()
             val methods = clazz.methods.filter { it.name == method.name }
-            if (methods.size != 1) return null
-            return methods.single()
+            return EtsPropertyResolution.create(methods)
         }
 
         // Unknown signature:
         val methods = ctx.scene.projectAndSdkClasses
             .flatMap { it.methods }
             .filter { it.name == method.name }
-        if (methods.size == 1) return methods.single()
 
-        // error("Cannot resolve method $method")
-        return null
+        return EtsPropertyResolution.create(methods)
     }
 
     override fun visit(expr: EtsPtrCallExpr): UExpr<out USort>? {
@@ -730,7 +769,7 @@ class TsExprResolver(
         val etsField = resolveEtsField(instance, field, hierarchy)
 
         val sort = when (etsField) {
-            is EtsFieldResolutionResult.Empty -> {
+            is EtsPropertyResolution.Empty -> {
                 logger.error("Field $etsField not found, creating fake field")
                 // If we didn't find any real fields, let's create a fake one.
                 // It is possible due to mistakes in the IR or if the field was added explicitly
@@ -740,10 +779,13 @@ class TsExprResolver(
                 addressSort
             }
 
-            is EtsFieldResolutionResult.Unique -> typeToSort(etsField.field.type)
-            is EtsFieldResolutionResult.Ambiguous -> unresolvedSort
+            is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type)
+            is EtsPropertyResolution.Ambiguous -> unresolvedSort
         }
 
+        // Если мы записали что-то в объект в виде bool, а потом считали это из поля bool | null, то здесь будет unresolvedSort,
+        // мы проигнорируем что уже туда писали и считаем не оттуда
+
         if (sort == unresolvedSort) {
             val boolLValue = mkFieldLValue(boolSort, instanceRef, field)
             val fpLValue = mkFieldLValue(fp64Sort, instanceRef, field)
@@ -874,6 +916,17 @@ class TsExprResolver(
         } else {
             expr.type
         }
+
+        if (expr.type.typeName == "Boolean") {
+            val clazz = scene.sdkClasses.filter { it.name == "Boolean" }.maxBy { it.methods.size }
+            return@with scope.calcOnState { memory.allocConcrete(clazz.type) }
+        }
+
+        if (expr.type.typeName == "Number") {
+            val clazz = scene.sdkClasses.filter { it.name == "Number" }.maxBy { it.methods.size }
+            return@with scope.calcOnState { memory.allocConcrete(clazz.type) }
+        }
+
         scope.calcOnState { memory.allocConcrete(resolvedType) }
     }
 
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 5df7982ee..b7d59fd7e 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
@@ -5,6 +5,7 @@ import mu.KotlinLogging
 import org.jacodb.ets.model.EtsArrayAccess
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsAssignStmt
+import org.jacodb.ets.model.EtsBooleanType
 import org.jacodb.ets.model.EtsCallStmt
 import org.jacodb.ets.model.EtsClassType
 import org.jacodb.ets.model.EtsIfStmt
@@ -14,6 +15,7 @@ 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
 import org.jacodb.ets.model.EtsParameterRef
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsReturnStmt
@@ -65,7 +67,7 @@ import org.usvm.machine.types.toAuxiliaryType
 import org.usvm.sizeSort
 import org.usvm.targets.UTargetsSet
 import org.usvm.types.single
-import org.usvm.util.EtsFieldResolutionResult
+import org.usvm.util.EtsPropertyResolution
 import org.usvm.util.mkArrayIndexLValue
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
@@ -171,7 +173,7 @@ class TsInterpreter(
         if (isAllocatedConcreteHeapRef(resolvedInstance)) {
             val type = scope.calcOnState { memory.typeStreamOf(resolvedInstance) }.single()
             if (type is EtsClassType) {
-                val classes = scene.projectAndSdkClasses.filter { it.name == type.typeName }
+                val classes = graph.hierarchy.classesForType(type)
                 if (classes.isEmpty()) {
                     logger.warn { "Could not resolve class: ${type.typeName}" }
                     scope.assert(falseExpr)
@@ -185,7 +187,9 @@ class TsInterpreter(
                 val cls = classes.single()
                 val method = cls.methods
                     .singleOrNull { it.name == stmt.callee.name }
-                    ?: TODO("Overloads are not supported yet")
+                    ?: run {
+                        TODO("Overloads are not supported yet")
+                    }
                 concreteMethods += method
             } else {
                 logger.warn {
@@ -348,6 +352,8 @@ class TsInterpreter(
 
         val (posStmt, negStmt) = graph.successors(stmt).take(2).toList()
 
+        logger.warn { "Forking on if stmt $stmt" }
+
         scope.forkWithBlackList(
             boolExpr,
             posStmt,
@@ -487,9 +493,9 @@ class TsInterpreter(
 
                     // If there is no such field, we create a fake field for the expr
                     val sort = when (etsField) {
-                        is EtsFieldResolutionResult.Empty -> unresolvedSort
-                        is EtsFieldResolutionResult.Unique -> typeToSort(etsField.field.type)
-                        is EtsFieldResolutionResult.Ambiguous -> unresolvedSort
+                        is EtsPropertyResolution.Empty -> unresolvedSort
+                        is EtsPropertyResolution.Unique -> typeToSort(etsField.property.type)
+                        is EtsPropertyResolution.Ambiguous -> unresolvedSort
                     }
 
                     if (sort == unresolvedSort) {
@@ -501,7 +507,37 @@ class TsInterpreter(
                         memory.write(lValue, fakeObject, guard = trueExpr)
                     } else {
                         val lValue = mkFieldLValue(sort, instance, lhv.field)
-                        memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
+                        if (lValue.sort != expr.sort) {
+                            if (expr.isFakeObject()) {
+                                val lhvType = lhv.type
+                                val value = when (lhvType) {
+                                    is EtsBooleanType -> {
+                                        scope.calcOnState {
+                                            pathConstraints += expr.getFakeType(scope).boolTypeExpr
+                                            expr.extractBool(scope)
+                                        }
+                                    }
+                                    is EtsNumberType -> {
+                                        scope.calcOnState {
+                                            pathConstraints += expr.getFakeType(scope).fpTypeExpr
+                                            expr.extractFp(scope)
+                                        }
+                                    }
+                                    else -> {
+                                        scope.calcOnState {
+                                            pathConstraints += expr.getFakeType(scope).refTypeExpr
+                                            expr.extractRef(scope)
+                                        }
+                                    }
+                                }
+
+                                memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr)
+                            } else {
+                                error("TODO")
+                            }
+                        } else {
+                            memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
+                        }
                     }
                 }
 
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 8b7884ec5..b205cdd9e 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
@@ -16,12 +16,10 @@ fun TsContext.resolveEtsField(
     instance: EtsLocal?,
     field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
-): EtsFieldResolutionResult {
+): EtsPropertyResolution<out EtsField> {
     // Perfect signature:
     if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) {
-        val classes = scene.projectAndSdkClasses.filter { cls ->
-            cls.name == field.enclosingClass.name
-        }
+        val classes = scene.projectAndSdkClasses.filter { it.signature == field.enclosingClass }
         if (classes.isEmpty()) {
             error("Cannot resolve class ${field.enclosingClass.name}")
         }
@@ -31,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 EtsFieldResolutionResult.create(fields.single())
+            return EtsPropertyResolution.create(fields.single())
         }
     }
 
@@ -41,12 +39,12 @@ fun TsContext.resolveEtsField(
         when (instanceType) {
             is EtsClassType -> {
                 val field = tryGetSingleField(scene, instanceType.signature.name, field.name, hierarchy)
-                if (field != null) return EtsFieldResolutionResult.create(field)
+                if (field != null) return EtsPropertyResolution.create(field)
             }
 
             is EtsUnclearRefType -> {
                 val field = tryGetSingleField(scene, instanceType.typeName, field.name, hierarchy)
-                if (field != null) return EtsFieldResolutionResult.create(field)
+                if (field != null) return EtsPropertyResolution.create(field)
             }
         }
     }
@@ -55,7 +53,7 @@ fun TsContext.resolveEtsField(
         cls.getAllFields(hierarchy).filter { it.name == field.name }
     }
 
-    return EtsFieldResolutionResult.create(fields)
+    return EtsPropertyResolution.create(fields)
 }
 
 private fun tryGetSingleField(
@@ -118,19 +116,19 @@ fun EtsClass.getAllProperties(hierarchy: EtsHierarchy): Pair<Set<EtsFieldName>,
     return allFields to allMethods
 }
 
-sealed class EtsFieldResolutionResult {
-    data class Unique(val field: EtsField) : EtsFieldResolutionResult()
-    data class Ambiguous(val fields: List<EtsField>) : EtsFieldResolutionResult()
-    data object Empty : EtsFieldResolutionResult()
+sealed class EtsPropertyResolution<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>()
 
     companion object {
-        fun create(field: EtsField) = Unique(field)
+        fun <T> create(property: T) = Unique(property)
 
-        fun create(fields: List<EtsField>): EtsFieldResolutionResult {
+        fun <T> create(properties: List<T>): EtsPropertyResolution<out T> {
             return when {
-                fields.isEmpty() -> Empty
-                fields.size == 1 -> Unique(fields.single())
-                else -> Ambiguous(fields)
+                properties.isEmpty() -> Empty
+                properties.size == 1 -> Unique(properties.single())
+                else -> Ambiguous(properties)
             }
         }
     }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
index 40ab15d73..66f34b4bc 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -1,6 +1,9 @@
 package org.usvm.project
 
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.CONSTRUCTOR_NAME
+import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
+import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.getDeclaredLocals
 import org.jacodb.ets.utils.getLocals
 import org.jacodb.ets.utils.loadEtsProjectFromIR
@@ -72,6 +75,9 @@ class RunOnPhotosProject : TsMethodTestRunner() {
                     .filterNot { it.isStatic }
                     .filterNot { it.name.startsWith("%AM") }
                     .filterNot { it.name == "build" }
+                    .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
+                    .filterNot { it.name == STATIC_INIT_METHOD_NAME }
+                    .filterNot { it.name == CONSTRUCTOR_NAME }
             }
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
@@ -79,4 +85,17 @@ class RunOnPhotosProject : TsMethodTestRunner() {
             states.let {}
         }
     }
+
+    @Test
+    fun `test on particular method`() {
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "createActionBar" && it.enclosingClass?.name == "NewAlbumBarModel" }
+
+        val tsOptions = TsOptions()
+        TsMachine(scene, options, tsOptions).use { machine ->
+            val states = machine.analyze(listOf(method))
+            states.let {}
+        }
+    }
 }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
index 58d5b1702..065d2ec15 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -341,7 +341,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
         pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
         exceptionsPropagation = true,
         timeout = Duration.INFINITE,
-        stepsFromLastCovered = 3500L,
+        stepsFromLastCovered = 50000L,
         solverType = SolverType.YICES,
         solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
         typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests

From 78a7f3433a1068621a732b23034c73d89a97cabc Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Thu, 29 May 2025 23:57:00 +0300
Subject: [PATCH 02/69] More hacks

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 30 +++++++++++++++++++
 1 file changed, 30 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 2262c26ad..d68330cd5 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
@@ -483,6 +483,36 @@ class TsExprResolver(
             return TODO()
         }
 
+        // TODO write tests
+        if (expr.callee.name == "push") {
+            let {}
+        }
+
+        if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) {
+            return scope.calcOnState {
+                val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
+                val lengthLValue = mkArrayLengthLValue(
+                    resolvedInstance,
+                    EtsArrayType(EtsUnknownType, dimensions = 1)
+                )
+                val length = memory.read(lengthLValue)
+                val newLength = mkBvAddExpr(length, 1.toBv())
+                memory.write(lengthLValue, newLength, guard = ctx.trueExpr)
+                val resolvedArg = resolve(expr.args.single()) ?: return@calcOnState null
+
+                // TODO check sorts compatibility
+                val newIndexLValue = mkArrayIndexLValue(
+                    resolvedArg.sort,
+                    resolvedInstance,
+                    length,
+                    EtsArrayType(EtsUnknownType, dimensions = 1)
+                )
+                memory.write(newIndexLValue, resolvedArg.asExpr(newIndexLValue.sort), guard = ctx.trueExpr)
+
+                newLength
+            }
+        }
+
         return when (val result = scope.calcOnState { methodResult }) {
             is TsMethodResult.Success -> {
                 scope.doWithState { methodResult = TsMethodResult.NoCall }

From bde95201429cd8a7243f25862a29cf077c350cfc Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Fri, 30 May 2025 16:06:36 +0300
Subject: [PATCH 03/69] Some more fixes

---
 .../main/kotlin/org/usvm/machine/TsContext.kt | 17 +++-
 .../main/kotlin/org/usvm/machine/TsMachine.kt | 86 +++++++++++++++----
 .../org/usvm/machine/expr/TsExprResolver.kt   | 26 +++++-
 .../usvm/machine/interpreter/TsInterpreter.kt | 13 +--
 .../test/kotlin/org/usvm/project/Photos.kt    |  6 +-
 .../main/kotlin/org/usvm/UMachineOptions.kt   |  1 +
 6 files changed, 118 insertions(+), 31 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 026f3c35b..9fdf2054c 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -6,8 +6,10 @@ import org.jacodb.ets.model.EtsAliasType
 import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
+import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringType
@@ -76,7 +78,20 @@ class TsContext(
         is EtsAnyType -> unresolvedSort
         is EtsUnknownType -> unresolvedSort
         is EtsAliasType -> typeToSort(type.originalType)
-        else -> TODO("${type::class.simpleName} is not yet supported: $type")
+        is EtsGenericType -> {
+            if (type.constraint == null && type.defaultType == null) {
+                unresolvedSort
+            } else {
+                TODO("Not yet implemented")
+            }
+        }
+        else -> {
+            if (type is EtsRawType && type.kind == "EnumValueType") {
+                unresolvedSort
+            } else {
+                TODO("${type::class.simpleName} is not yet supported: $type")
+            }
+        }
     }
 
     fun arrayDescriptorOf(type: EtsArrayType): EtsType {
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index d82ac0ab8..59b54ce0c 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -8,6 +8,7 @@ import org.usvm.CoverageZone
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
+import org.usvm.UPathSelector
 import org.usvm.api.targets.TsTarget
 import org.usvm.machine.interpreter.TsInterpreter
 import org.usvm.machine.state.TsMethodResult
@@ -26,6 +27,7 @@ import org.usvm.statistics.collectors.TargetsReachedStatesCollector
 import org.usvm.statistics.constraints.SoftConstraintsObserver
 import org.usvm.statistics.distances.CfgStatisticsImpl
 import org.usvm.statistics.distances.PlainCallGraphStatistics
+import org.usvm.stopstrategies.StopStrategy
 import org.usvm.stopstrategies.createStopStrategy
 import org.usvm.util.humanReadableSignature
 import kotlin.time.Duration.Companion.seconds
@@ -72,15 +74,39 @@ class TsMachine(
 
         val timeStatistics = TimeStatistics<EtsMethod, TsState>()
 
-        val pathSelector = createPathSelector(
-            initialStates = initialStates,
-            options = options,
-            applicationGraph = graph,
-            timeStatistics = timeStatistics,
-            coverageStatisticsFactory = { coverageStatistics },
-            cfgStatisticsFactory = { cfgStatistics },
-            callGraphStatisticsFactory = { callGraphStatistics },
-        )
+        val pathSelector = object : UPathSelector<TsState> {
+            val internalSelector = createPathSelector(
+                initialStates = initialStates,
+                options = options,
+                applicationGraph = graph,
+                timeStatistics = timeStatistics,
+                coverageStatisticsFactory = { coverageStatistics },
+                cfgStatisticsFactory = { cfgStatistics },
+                callGraphStatisticsFactory = { callGraphStatistics }
+            )
+
+            override fun isEmpty(): Boolean {
+                return internalSelector.isEmpty()
+            }
+
+            override fun peek(): TsState {
+                return internalSelector.peek()
+            }
+
+            override fun remove(state: TsState) {
+                logger.warn { "Selector size -1" }
+                return internalSelector.remove(state)
+            }
+
+            override fun add(states: Collection<TsState>) {
+                logger.warn { "Selector size +1" }
+                return internalSelector.add(states)
+            }
+
+            override fun update(state: TsState) {
+                return internalSelector.update(state)
+            }
+        }
 
         val statesCollector =
             when (options.stateCollectionStrategy) {
@@ -101,14 +127,30 @@ class TsMachine(
 
         val stepsStatistics = StepsStatistics<EtsMethod, TsState>()
 
-        val stopStrategy = createStopStrategy(
-            options,
-            targets,
-            timeStatisticsFactory = { timeStatistics },
-            stepsStatisticsFactory = { stepsStatistics },
-            coverageStatisticsFactory = { coverageStatistics },
-            getCollectedStatesCount = { statesCollector.collectedStates.size }
-        )
+        val stopStrategy = object : StopStrategy {
+            val strategy = createStopStrategy(
+                options,
+                targets,
+                timeStatisticsFactory =
+                    { timeStatistics },
+                stepsStatisticsFactory =
+                    { stepsStatistics },
+                coverageStatisticsFactory =
+                    { coverageStatistics },
+                getCollectedStatesCount =
+                    { statesCollector.collectedStates.size }
+            )
+
+            override fun shouldStop(): Boolean {
+                val result = strategy.shouldStop()
+
+                if (result) {
+                    logger.warn { "Stop strategy finished execution $strategy" }
+                }
+
+                return result
+            }
+        }
 
         observers.add(timeStatistics)
         observers.add(stepsStatistics)
@@ -127,6 +169,16 @@ class TsMachine(
             )
         }
 
+        val endReasonObserver = object : UMachineObserver<TsState> {
+            override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
+                logger.warn {
+                    "State is terminated on ${state.currentStatement} in the method ${state.currentStatement.method}"
+                }
+            }
+        }
+
+        observers += endReasonObserver
+
         run(
             interpreter,
             pathSelector,
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 d68330cd5..ff1322970 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
@@ -54,6 +54,7 @@ import org.jacodb.ets.model.EtsPostIncExpr
 import org.jacodb.ets.model.EtsPreDecExpr
 import org.jacodb.ets.model.EtsPreIncExpr
 import org.jacodb.ets.model.EtsPtrCallExpr
+import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRemExpr
 import org.jacodb.ets.model.EtsRightShiftExpr
 import org.jacodb.ets.model.EtsStaticCallExpr
@@ -484,10 +485,6 @@ class TsExprResolver(
         }
 
         // TODO write tests
-        if (expr.callee.name == "push") {
-            let {}
-        }
-
         if (expr.callee.name == "push" && expr.instance.type is EtsArrayType) {
             return scope.calcOnState {
                 val resolvedInstance = resolve(expr.instance)?.asExpr(ctx.addressSort) ?: return@calcOnState null
@@ -813,6 +810,7 @@ class TsExprResolver(
             is EtsPropertyResolution.Ambiguous -> unresolvedSort
         }
 
+        // TODO
         // Если мы записали что-то в объект в виде bool, а потом считали это из поля bool | null, то здесь будет unresolvedSort,
         // мы проигнорируем что уже туда писали и считаем не оттуда
 
@@ -835,6 +833,26 @@ class TsExprResolver(
                         lValuesToAllocatedFakeObjects += refLValue to it
                     }
                 }
+
+                // TODO ambiguous enum fields resolution
+                if (etsField is EtsPropertyResolution.Unique) {
+                    val fieldType = etsField.property.type
+                    if (fieldType is EtsRawType && fieldType.kind == "EnumValueType") {
+                        val fakeType = fakeRef.getFakeType(scope)
+                        pathConstraints += ctx.mkOr(
+                            fakeType.fpTypeExpr,
+                            fakeType.refTypeExpr
+                        )
+
+                        // val supertype = TODO()
+                        // TODO add enum type as a constraint
+                        // pathConstraints += memory.types.evalIsSubtype(
+                        //     ref,
+                        //     TODO()
+                        // )
+                    }
+                }
+
                 memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
 
                 fakeRef
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 b7d59fd7e..158b012ec 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
@@ -136,9 +136,7 @@ class TsInterpreter(
                 val s = e.stackTrace[0]
                 "Exception .(${s.fileName}:${s.lineNumber}): $e}"
             }
-
-            // Kill the state causing error
-            scope.assert(ctx.falseExpr)
+            // todo are exceptional states properly removed?
         }
 
         return scope.stepResult()
@@ -208,12 +206,14 @@ class TsInterpreter(
             concreteMethods += methods
         }
 
+        val limitedConcreteMethods = concreteMethods.take(5)
+
         logger.info {
-            "Preparing to fork on ${concreteMethods.size} methods: ${
-                concreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
+            "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
+                limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
             }"
         }
-        val conditionsWithBlocks = concreteMethods.map { method ->
+        val conditionsWithBlocks = limitedConcreteMethods.map { method ->
             val concreteCall = stmt.toConcrete(method)
             val block = { state: TsState -> state.newStmt(concreteCall) }
             val type = requireNotNull(method.enclosingClass).type
@@ -533,6 +533,7 @@ class TsInterpreter(
 
                                 memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr)
                             } else {
+                                // probably it is a enum, check for it
                                 error("TODO")
                             }
                         } else {
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
index 66f34b4bc..fa161bdb7 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -6,7 +6,7 @@ import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.getDeclaredLocals
 import org.jacodb.ets.utils.getLocals
-import org.jacodb.ets.utils.loadEtsProjectFromIR
+import org.jacodb.ets.utils.loadEtsProjectAutoConvert
 import org.junit.jupiter.api.condition.EnabledIf
 import org.usvm.api.TsTestValue
 import org.usvm.machine.TsMachine
@@ -21,7 +21,7 @@ import kotlin.test.Test
 class RunOnPhotosProject : TsMethodTestRunner() {
 
     companion object {
-        private const val PROJECT_PATH = "/projects/Demo_Photos/etsir/entry"
+        private const val PROJECT_PATH = "/projects/Demo_Photos/source/entry"
         private const val SDK_PATH = "/sdk/ohos/etsir"
 
         @JvmStatic
@@ -34,7 +34,7 @@ class RunOnPhotosProject : TsMethodTestRunner() {
         val projectPath = getResourcePath(PROJECT_PATH)
         val sdkPath = getResourcePathOrNull(SDK_PATH)
             ?: error("Could not load SDK from resources '$SDK_PATH'. Try running './gradlew generateSdkIR' to generate it.")
-        loadEtsProjectFromIR(projectPath, sdkPath)
+        loadEtsProjectAutoConvert(projectPath, sdkPath)
     }
 
     @Test
diff --git a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt
index b2989d268..de5646aaa 100644
--- a/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/UMachineOptions.kt
@@ -259,4 +259,5 @@ data class UMachineOptions(
      * Limit loop iterations.
      * */
     val loopIterationLimit: Int? = null,
+    // TODO fork limit
 )

From 4d0cf6ba159d7a5ff64db4dc2a0feb1fc9a7c900 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Fri, 30 May 2025 16:28:36 +0300
Subject: [PATCH 04/69] Tmp commit

---
 .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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 158b012ec..f46c8fa91 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
@@ -129,7 +129,12 @@ class TsInterpreter(
                 is EtsCallStmt -> visitCallStmt(scope, stmt)
                 is EtsThrowStmt -> visitThrowStmt(scope, stmt)
                 is EtsNopStmt -> visitNopStmt(scope, stmt)
-                else -> error("Unknown stmt: $stmt")
+                else -> {
+                    logger.error { "Unknown stmt: $stmt" }
+                    scope.doWithState {
+                        newStmt(graph.successors(stmt).single())
+                    }
+                }
             }
         } catch (e: Exception) {
             logger.error {
@@ -517,12 +522,14 @@ class TsInterpreter(
                                             expr.extractBool(scope)
                                         }
                                     }
+
                                     is EtsNumberType -> {
                                         scope.calcOnState {
                                             pathConstraints += expr.getFakeType(scope).fpTypeExpr
                                             expr.extractFp(scope)
                                         }
                                     }
+
                                     else -> {
                                         scope.calcOnState {
                                             pathConstraints += expr.getFakeType(scope).refTypeExpr

From a4954f9a906bfbba7a752b3f0474dbe94b372298 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Fri, 6 Jun 2025 17:11:58 +0300
Subject: [PATCH 05/69] Input arrays support

---
 .../kotlin/org/usvm/machine/expr/TsExprResolver.kt    |  4 +---
 .../kotlin/org/usvm/machine/expr/TsExpressions.kt     | 11 +++++++++++
 .../org/usvm/machine/operator/TsBinaryOperator.kt     |  4 ++--
 .../src/main/kotlin/org/usvm/machine/state/TsState.kt |  1 +
 4 files changed, 15 insertions(+), 5 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 ff1322970..beae3da2c 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
@@ -829,9 +829,7 @@ class TsExprResolver(
                 val fakeRef = if (ref.isFakeObject()) {
                     ref
                 } else {
-                    mkFakeValue(scope, bool, fp, ref).also {
-                        lValuesToAllocatedFakeObjects += refLValue to it
-                    }
+                    mkFakeValue(scope, bool, fp, ref).also { lValuesToAllocatedFakeObjects += refLValue to it }
                 }
 
                 // TODO ambiguous enum fields resolution
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
index 9a3343b5a..c07be5b8b 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
@@ -100,3 +100,14 @@ fun UExpr<*>.extractInt(): Int {
     }
     error("Cannot extract Int from $this")
 }
+
+/**
+ * Extracts an integer value from [this] expression if possible.
+ * Otherwise, throws an error.
+ */
+fun UExpr<out USort>.extractInt(): Int {
+    if (this@extractInt is KBitVec32Value) {
+        return intValue
+    }
+    error("Cannot extract int from $this")
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
index 722f86f07..fae34cebe 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
@@ -573,6 +573,7 @@ sealed interface TsBinaryOperator {
                             lhsValue = lhs.extractBool(scope)
                             lhsType.boolTypeExpr
                         }
+                        }
 
                         fp64Sort -> {
                             lhsValue = lhs.extractFp(scope)
@@ -583,7 +584,6 @@ sealed interface TsBinaryOperator {
                             lhsValue = lhs.extractRef(scope)
                             lhsType.refTypeExpr
                         }
-
                         else -> error("Unsupported sort ${rhs.sort}")
                     }
                 }
@@ -595,6 +595,7 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractBool(scope)
                             rhsType.boolTypeExpr
                         }
+                        }
 
                         fp64Sort -> {
                             rhsValue = rhs.extractFp(scope)
@@ -605,7 +606,6 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractRef(scope)
                             rhsType.refTypeExpr
                         }
-
                         else -> error("Unsupported sort ${lhs.sort}")
                     }
                 }
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 38d8b66d1..4451bf985 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
@@ -49,6 +49,7 @@ class TsState(
     val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)),
     val addedArtificialLocals: MutableSet<String> = hashSetOf(),
     val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
+    val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,

From 5d4dc68f1211fe224a82d5bb93585263b6ef8f04 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Mon, 9 Jun 2025 16:34:56 +0300
Subject: [PATCH 06/69] Format

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt  | 4 +++-
 .../src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt   | 4 ++--
 .../kotlin/org/usvm/machine/operator/TsBinaryOperator.kt     | 5 ++---
 usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt    | 1 -
 4 files changed, 7 insertions(+), 7 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 beae3da2c..ff1322970 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
@@ -829,7 +829,9 @@ class TsExprResolver(
                 val fakeRef = if (ref.isFakeObject()) {
                     ref
                 } else {
-                    mkFakeValue(scope, bool, fp, ref).also { lValuesToAllocatedFakeObjects += refLValue to it }
+                    mkFakeValue(scope, bool, fp, ref).also {
+                        lValuesToAllocatedFakeObjects += refLValue to it
+                    }
                 }
 
                 // TODO ambiguous enum fields resolution
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
index c07be5b8b..4ec91ffe8 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
@@ -105,9 +105,9 @@ fun UExpr<*>.extractInt(): Int {
  * Extracts an integer value from [this] expression if possible.
  * Otherwise, throws an error.
  */
-fun UExpr<out USort>.extractInt(): Int {
+fun UExpr<*>.extractInt(): Int {
     if (this@extractInt is KBitVec32Value) {
         return intValue
     }
-    error("Cannot extract int from $this")
+    error("Cannot extract Int from $this")
 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
index fae34cebe..2a1094918 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
@@ -573,7 +573,6 @@ sealed interface TsBinaryOperator {
                             lhsValue = lhs.extractBool(scope)
                             lhsType.boolTypeExpr
                         }
-                        }
 
                         fp64Sort -> {
                             lhsValue = lhs.extractFp(scope)
@@ -584,6 +583,7 @@ sealed interface TsBinaryOperator {
                             lhsValue = lhs.extractRef(scope)
                             lhsType.refTypeExpr
                         }
+
                         else -> error("Unsupported sort ${rhs.sort}")
                     }
                 }
@@ -595,8 +595,6 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractBool(scope)
                             rhsType.boolTypeExpr
                         }
-                        }
-
                         fp64Sort -> {
                             rhsValue = rhs.extractFp(scope)
                             rhsType.fpTypeExpr
@@ -606,6 +604,7 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractRef(scope)
                             rhsType.refTypeExpr
                         }
+
                         else -> error("Unsupported sort ${lhs.sort}")
                     }
                 }
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 4451bf985..38d8b66d1 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
@@ -49,7 +49,6 @@ class TsState(
     val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)),
     val addedArtificialLocals: MutableSet<String> = hashSetOf(),
     val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
-    val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,

From 7cf9061fe1253656a837bf6f26faa9a08078f54b Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Tue, 10 Jun 2025 18:13:39 +0300
Subject: [PATCH 07/69] Operators implementation

---
 .../kotlin/org/usvm/machine/expr/TsExprResolver.kt  | 13 ++++++++-----
 .../test/kotlin/org/usvm/util/TsMethodTestRunner.kt |  2 +-
 2 files changed, 9 insertions(+), 6 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 ff1322970..bcc26039d 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
@@ -117,7 +117,6 @@ import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkRegisterStackLValue
 import org.usvm.util.resolveEtsField
 import org.usvm.util.throwExceptionWithoutStackFrameDrop
-import org.usvm.util.type
 
 private val logger = KotlinLogging.logger {}
 
@@ -418,13 +417,17 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsLtEqExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        val eq = resolve(EtsEqExpr(expr.left, expr.right)) ?: return null
+        val lt = resolve(EtsLtExpr(expr.left, expr.right)) ?: return null
+
+        return ctx.mkOr(eq.asExpr(ctx.boolSort), lt.asExpr(ctx.boolSort))
     }
 
     override fun visit(expr: EtsGtEqExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        val eq = resolve(EtsEqExpr(expr.left, expr.right)) ?: return null
+        val gt = resolve(EtsGtExpr(expr.left, expr.right)) ?: return null
+
+        return ctx.mkOr(eq.asExpr(ctx.boolSort), gt.asExpr(ctx.boolSort))
     }
 
     override fun visit(expr: EtsInExpr): UExpr<out USort>? {
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
index 065d2ec15..58d5b1702 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -341,7 +341,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
         pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
         exceptionsPropagation = true,
         timeout = Duration.INFINITE,
-        stepsFromLastCovered = 50000L,
+        stepsFromLastCovered = 3500L,
         solverType = SolverType.YICES,
         solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
         typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests

From 2a07286e5db6eb03af189e3810909ec6058f22df Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Tue, 10 Jun 2025 18:17:51 +0300
Subject: [PATCH 08/69] Some hacks

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt   | 4 ++--
 1 file changed, 2 insertions(+), 2 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 bcc26039d..664e7ebd9 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
@@ -292,8 +292,8 @@ class TsExprResolver(
             )
         }
 
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        logger.error { "visit(${expr::class.simpleName}) is not implemented yet" }
+        return mkFp64(ADHOC_STRING)
     }
 
     override fun visit(expr: EtsDeleteExpr): UExpr<out USort>? {

From 8c9e9f4be0d582ab6a4f0dcc20db4c492c575ec5 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Wed, 11 Jun 2025 11:04:20 +0300
Subject: [PATCH 09/69] Fix a class signature lookup

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

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 b205cdd9e..e59d43cd2 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
@@ -19,7 +19,7 @@ fun TsContext.resolveEtsField(
 ): EtsPropertyResolution<out EtsField> {
     // Perfect signature:
     if (field.enclosingClass.name != UNKNOWN_CLASS_NAME) {
-        val classes = scene.projectAndSdkClasses.filter { it.signature == field.enclosingClass }
+        val classes = hierarchy.classesForType(EtsClassType(field.enclosingClass))
         if (classes.isEmpty()) {
             error("Cannot resolve class ${field.enclosingClass.name}")
         }

From 689a90245a6e1cfd84be7bccf181b6cb3b48d280 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Wed, 11 Jun 2025 11:42:00 +0300
Subject: [PATCH 10/69] Support simple casts

---
 buildSrc/src/main/kotlin/Dependencies.kt      |  2 +-
 .../main/kotlin/org/usvm/machine/TsContext.kt |  9 ++----
 .../org/usvm/machine/expr/TsExprResolver.kt   | 30 +++++++++++++++++--
 3 files changed, 32 insertions(+), 9 deletions(-)

diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index 03474c51d..482eec683 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 = "4ff7243d3a"
+    const val jacodb = "77b83e4127"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"
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 9fdf2054c..c9110f2ed 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -6,10 +6,10 @@ import org.jacodb.ets.model.EtsAliasType
 import org.jacodb.ets.model.EtsAnyType
 import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsBooleanType
+import org.jacodb.ets.model.EtsEnumValueType
 import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberType
-import org.jacodb.ets.model.EtsRawType
 import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStringType
@@ -85,12 +85,9 @@ class TsContext(
                 TODO("Not yet implemented")
             }
         }
+        is EtsEnumValueType -> unresolvedSort
         else -> {
-            if (type is EtsRawType && type.kind == "EnumValueType") {
-                unresolvedSort
-            } else {
-                TODO("${type::class.simpleName} is not yet supported: $type")
-            }
+            TODO("${type::class.simpleName} is not yet supported: $type")
         }
     }
 
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 664e7ebd9..4d7e31fab 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
@@ -55,6 +55,7 @@ import org.jacodb.ets.model.EtsPreDecExpr
 import org.jacodb.ets.model.EtsPreIncExpr
 import org.jacodb.ets.model.EtsPtrCallExpr
 import org.jacodb.ets.model.EtsRawType
+import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsRemExpr
 import org.jacodb.ets.model.EtsRightShiftExpr
 import org.jacodb.ets.model.EtsStaticCallExpr
@@ -262,8 +263,33 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        val resolvedExpr = resolve(expr.arg) ?: return@with null
+        return when (resolvedExpr.sort) {
+            fp64Sort -> {
+                TODO()
+            }
+
+            boolSort -> {
+                TODO()
+            }
+
+            addressSort -> {
+                scope.calcOnState {
+                    val instance = resolvedExpr.asExpr(addressSort)
+
+                    if (expr.type !is EtsRefType) {
+                        TODO("Not supported yet")
+                    }
+
+                    pathConstraints += memory.types.evalIsSubtype(instance, expr.type)
+                    instance
+                }
+            }
+
+            else -> {
+                error("Unsupported cast from ${expr.arg} to ${expr.type}")
+            }
+        }
     }
 
     override fun visit(expr: EtsTypeOfExpr): UExpr<out USort>? = with(ctx) {

From 760624b8d252c1bb30e544c4284300cce86f0567 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Wed, 11 Jun 2025 11:51:56 +0300
Subject: [PATCH 11/69] Clear logs

---
 .../main/kotlin/org/usvm/machine/TsMachine.kt | 53 ++++---------------
 .../org/usvm/machine/expr/TsExprResolver.kt   |  2 +-
 .../usvm/machine/interpreter/TsInterpreter.kt |  9 +---
 3 files changed, 12 insertions(+), 52 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index 59b54ce0c..fa07056a9 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -8,7 +8,6 @@ import org.usvm.CoverageZone
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
-import org.usvm.UPathSelector
 import org.usvm.api.targets.TsTarget
 import org.usvm.machine.interpreter.TsInterpreter
 import org.usvm.machine.state.TsMethodResult
@@ -74,39 +73,15 @@ class TsMachine(
 
         val timeStatistics = TimeStatistics<EtsMethod, TsState>()
 
-        val pathSelector = object : UPathSelector<TsState> {
-            val internalSelector = createPathSelector(
-                initialStates = initialStates,
-                options = options,
-                applicationGraph = graph,
-                timeStatistics = timeStatistics,
-                coverageStatisticsFactory = { coverageStatistics },
-                cfgStatisticsFactory = { cfgStatistics },
-                callGraphStatisticsFactory = { callGraphStatistics }
-            )
-
-            override fun isEmpty(): Boolean {
-                return internalSelector.isEmpty()
-            }
-
-            override fun peek(): TsState {
-                return internalSelector.peek()
-            }
-
-            override fun remove(state: TsState) {
-                logger.warn { "Selector size -1" }
-                return internalSelector.remove(state)
-            }
-
-            override fun add(states: Collection<TsState>) {
-                logger.warn { "Selector size +1" }
-                return internalSelector.add(states)
-            }
-
-            override fun update(state: TsState) {
-                return internalSelector.update(state)
-            }
-        }
+        val pathSelector = createPathSelector(
+            initialStates = initialStates,
+            options = options,
+            applicationGraph = graph,
+            timeStatistics = timeStatistics,
+            coverageStatisticsFactory = { coverageStatistics },
+            cfgStatisticsFactory = { cfgStatistics },
+            callGraphStatisticsFactory = { callGraphStatistics }
+        )
 
         val statesCollector =
             when (options.stateCollectionStrategy) {
@@ -169,16 +144,6 @@ class TsMachine(
             )
         }
 
-        val endReasonObserver = object : UMachineObserver<TsState> {
-            override fun onStateTerminated(state: TsState, stateReachable: Boolean) {
-                logger.warn {
-                    "State is terminated on ${state.currentStatement} in the method ${state.currentStatement.method}"
-                }
-            }
-        }
-
-        observers += endReasonObserver
-
         run(
             interpreter,
             pathSelector,
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 4d7e31fab..7e7c53a50 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
@@ -1083,7 +1083,7 @@ class TsSimpleValueResolver(
                 return mkFieldLValue(ctx.addressSort, globalObject, local.name)
             }
 
-            logger.warn { "Cannot resolve local $local" }
+            logger.warn { "Cannot resolve local $local, creating a fake field of the global object" }
 
             globalObject.createFakeField(localName, scope)
             scope.doWithState {
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 f46c8fa91..9c1972250 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
@@ -245,7 +245,7 @@ class TsInterpreter(
         val entryPoint = graph.entryPoints(stmt.callee).singleOrNull()
 
         if (entryPoint == null) {
-            logger.warn { "No entry point for method: ${stmt.callee}" }
+            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)
@@ -357,8 +357,6 @@ class TsInterpreter(
 
         val (posStmt, negStmt) = graph.successors(stmt).take(2).toList()
 
-        logger.warn { "Forking on if stmt $stmt" }
-
         scope.forkWithBlackList(
             boolExpr,
             posStmt,
@@ -644,10 +642,7 @@ class TsInterpreter(
                         local.name to localIdx
                     }.toMap()
                 }
-                map[local.name] ?: run {
-                    logger.error("Local not declared: $local")
-                    return null
-                }
+                map[local.name]
             }
 
             // Note: 'this' has index 'n'

From 4bd35bacf29e59eed39ad828c07dd59ee519c25d Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Wed, 11 Jun 2025 14:20:43 +0300
Subject: [PATCH 12/69] Add todo

---
 .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt  | 3 +--
 1 file changed, 1 insertion(+), 2 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 9c1972250..7fe65c225 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
@@ -538,8 +538,7 @@ class TsInterpreter(
 
                                 memory.write(lValue, value.asExpr(lValue.sort), guard = trueExpr)
                             } else {
-                                // probably it is a enum, check for it
-                                error("TODO")
+                                TODO("Support enums fields")
                             }
                         } else {
                             memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)

From ada1c486620719dd675fb971dafade6622561dc0 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Wed, 18 Jun 2025 16:16:32 +0300
Subject: [PATCH 13/69] Rebase fix

---
 .../kotlin/org/usvm/machine/expr/TsExpressions.kt     | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
index 4ec91ffe8..9a3343b5a 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExpressions.kt
@@ -100,14 +100,3 @@ fun UExpr<*>.extractInt(): Int {
     }
     error("Cannot extract Int from $this")
 }
-
-/**
- * Extracts an integer value from [this] expression if possible.
- * Otherwise, throws an error.
- */
-fun UExpr<*>.extractInt(): Int {
-    if (this@extractInt is KBitVec32Value) {
-        return intValue
-    }
-    error("Cannot extract Int from $this")
-}

From 0dda9c035427d2a6d1e753d70349077b2fe4b192 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Thu, 19 Jun 2025 15:58:33 +0300
Subject: [PATCH 14/69] Tmp changes

---
 .../src/main/kotlin/org/usvm/StepScope.kt     |  4 +-
 .../org/usvm/machine/expr/TsExprResolver.kt   | 48 +++++++++++----
 .../usvm/machine/interpreter/TsInterpreter.kt | 15 ++---
 .../org/usvm/machine/types/TsTypeSystem.kt    |  3 +-
 .../main/kotlin/org/usvm/util/EtsHierarchy.kt |  2 +-
 .../test/kotlin/org/usvm/project/Photos.kt    | 58 +++++++++++--------
 .../org/usvm/util/TsMethodTestRunner.kt       |  8 +--
 .../org/usvm/test/util/checkers/Matchers.kt   |  2 +-
 8 files changed, 90 insertions(+), 50 deletions(-)

diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
index a22e8bd8d..294271f09 100644
--- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
@@ -56,7 +56,9 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
         contract {
             callsInPlace(block, InvocationKind.EXACTLY_ONCE)
         }
-        check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
+        check(canProcessFurtherOnCurrentStep) {
+            "Caller should check before processing the current hop further"
+        }
         return originalState.block()
     }
 
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 7e7c53a50..3c4663976 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
@@ -17,6 +17,7 @@ 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.EtsClassType
 import org.jacodb.ets.model.EtsConstant
 import org.jacodb.ets.model.EtsDeleteExpr
 import org.jacodb.ets.model.EtsDivExpr
@@ -277,6 +278,14 @@ class TsExprResolver(
                 scope.calcOnState {
                     val instance = resolvedExpr.asExpr(addressSort)
 
+                    if (instance.isFakeObject()) {
+                        val fakeType = instance.getFakeType(scope)
+                        pathConstraints += fakeType.refTypeExpr
+                        val refValue = instance.extractRef(scope)
+                        pathConstraints += memory.types.evalIsSubtype(refValue, expr.type)
+                        return@calcOnState instance
+                    }
+
                     if (expr.type !is EtsRefType) {
                         TODO("Not supported yet")
                     }
@@ -554,7 +563,11 @@ class TsExprResolver(
                     val resolved = resolve(expr.instance) ?: return null
 
                     if (resolved.sort != addressSort) {
-                        logger.warn { "Calling method on non-ref instance is not yet supported" }
+                        if (expr.callee.name == "valueOf" && expr.args.isEmpty()) {
+                            return resolve(expr.instance)
+                        }
+
+                        logger.warn { "Calling method on non-ref instance is not yet supported, instruction $expr" }
                         scope.assert(falseExpr)
                         return null
                     }
@@ -585,6 +598,13 @@ class TsExprResolver(
             }
         }
 
+        if (expr.callee.name == "Boolean") {
+            check(expr.args.size == 1) { "Boolean constructor should have exactly one argument" }
+            return resolveAfterResolved(expr.args.single()) {
+                mkTruthyExpr(it, scope)
+            }
+        }
+
         if (expr.callee.name == "\$r") {
             // TODO hack
             return scope.calcOnState {
@@ -612,6 +632,7 @@ class TsExprResolver(
                 if (resolutionResult is EtsPropertyResolution.Empty) {
                     logger.error { "Could not resolve static call: ${expr.callee}" }
                     scope.assert(falseExpr)
+                    // TODO mocks
                     return null
                 }
 
@@ -668,8 +689,14 @@ class TsExprResolver(
     ): EtsPropertyResolution<out EtsMethod> {
         // Perfect signature:
         if (method.enclosingClass.name != UNKNOWN_CLASS_NAME) {
-            val classes = ctx.scene.projectAndSdkClasses.filter { it.name == method.enclosingClass.name }
-            if (classes.size != 1) return EtsPropertyResolution.Empty
+            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)
+            }
+
+            if (classes.isEmpty()) return EtsPropertyResolution.Empty
+
             val clazz = classes.single()
             val methods = clazz.methods.filter { it.name == method.name }
             return EtsPropertyResolution.create(methods)
@@ -814,13 +841,6 @@ class TsExprResolver(
         hierarchy: EtsHierarchy,
     ): UExpr<out USort>? = with(ctx) {
         val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef
-        scope.doWithState {
-            // If we accessed some field, we make an assumption that
-            // this field should present in the object.
-            // That's not true in the common case for TS, but that's the decision we made.
-            val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name))
-            pathConstraints += memory.types.evalIsSubtype(resolvedAddr, auxiliaryType)
-        }
 
         val etsField = resolveEtsField(instance, field, hierarchy)
 
@@ -839,6 +859,14 @@ class TsExprResolver(
             is EtsPropertyResolution.Ambiguous -> unresolvedSort
         }
 
+        scope.doWithState {
+            // If we accessed some field, we make an assumption that
+            // this field should present in the object.
+            // That's not true in the common case for TS, but that's the decision we made.
+            val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name))
+            pathConstraints += memory.types.evalIsSubtype(resolvedAddr, auxiliaryType)
+        }
+
         // TODO
         // Если мы записали что-то в объект в виде bool, а потом считали это из поля bool | null, то здесь будет unresolvedSort,
         // мы проигнорируем что уже туда писали и считаем не оттуда
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 7fe65c225..0ea33e724 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
@@ -141,6 +141,7 @@ class TsInterpreter(
                 val s = e.stackTrace[0]
                 "Exception .(${s.fileName}:${s.lineNumber}): $e}"
             }
+            return StepResult(forkedStates = emptySequence(), originalStateAlive = false)
             // todo are exceptional states properly removed?
         }
 
@@ -213,11 +214,11 @@ class TsInterpreter(
 
         val limitedConcreteMethods = concreteMethods.take(5)
 
-        logger.info {
-            "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
-                limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
-            }"
-        }
+        // logger.info {
+            // "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
+            //     limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
+            // }"
+        // }
         val conditionsWithBlocks = limitedConcreteMethods.map { method ->
             val concreteCall = stmt.toConcrete(method)
             val block = { state: TsState -> state.newStmt(concreteCall) }
@@ -229,7 +230,7 @@ class TsInterpreter(
                     ?: uncoveredInstance.asExpr(addressSort)
                 // TODO mistake, should be separated into several hierarchies
                 //      or evalTypeEqual with several concrete types
-                memory.types.evalTypeEquals(ref, type)
+                memory.types.evalIsSubtype(ref, type) // TODO error
             }
             constraint to block
         }
@@ -245,7 +246,7 @@ class TsInterpreter(
         val entryPoint = graph.entryPoints(stmt.callee).singleOrNull()
 
         if (entryPoint == null) {
-            logger.warn { "No entry point for method: ${stmt.callee}, mocking the call" }
+            // 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)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
index fb9206d07..e100e461e 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
@@ -191,8 +191,9 @@ class TsTypeSystem(
                 if (classes.isEmpty() || superClasses.isEmpty()) return false // TODO log
 
                 return classes.any { cls ->
+                    val ancestors = hierarchy.getAncestor(cls)
                     superClasses.any { superClass ->
-                        superClass in hierarchy.getAncestor(cls)
+                        superClass in ancestors
                     }
                 }
             }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
index 359c64a00..68adb4e9e 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
@@ -58,7 +58,7 @@ class EtsHierarchy(private val scene: EtsScene) {
         val signature = superClassSignature.copy(name = typeName)
 
         val classesWithTheSameName = resolveMap[typeName] ?: run {
-            logger.error("No class with $superClassSignature found in the Scene")
+            // logger.error("No class with $superClassSignature found in the Scene")
             return emptyList()
         }
 
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
index fa161bdb7..712a92822 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -4,11 +4,8 @@ import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
-import org.jacodb.ets.utils.getDeclaredLocals
-import org.jacodb.ets.utils.getLocals
 import org.jacodb.ets.utils.loadEtsProjectAutoConvert
 import org.junit.jupiter.api.condition.EnabledIf
-import org.usvm.api.TsTestValue
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsMethodTestRunner
@@ -39,30 +36,41 @@ class RunOnPhotosProject : TsMethodTestRunner() {
 
     @Test
     fun `test run on each method`() {
-        println("Total classes: ${scene.projectAndSdkClasses.size}")
-        for (clazz in scene.projectAndSdkClasses) {
-            println()
-            println("CLASS: ${clazz.name} in ${clazz.signature.file}")
-            for (method in clazz.methods) {
-                println()
-                println("METHOD: ${clazz.name}::${method.name}(${method.parameters.joinToString()})")
-                if (method.cfg.stmts.isEmpty()) {
-                    println("CFG is empty")
-                    continue
-                }
-                if (method.getLocals() != method.getDeclaredLocals()) {
-                    println(
-                        "Locals mismatch:\n  getLocals() = ${
-                            method.getLocals().sortedBy { it.name }
-                        }\n  getDeclaredLocals() = ${
-                            method.getDeclaredLocals().sortedBy { it.name }
-                        }"
-                    )
-                    // continue
+        val exceptions = mutableListOf<Throwable>()
+        val classes = scene.projectClasses.filterNot { it.name.startsWith("%AC") }
+
+        println("Total classes: ${classes.size}")
+
+        classes
+            // .filter { it.name == "NewAlbumPage" }
+            .forEach { clazz ->
+            val methods = clazz.methods
+                .filterNot { it.cfg.stmts.isEmpty() }
+                .filterNot { it.isStatic }
+                .filterNot { it.name.startsWith("%AM") }
+                .filterNot { it.name == "build" }
+                .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
+                .filterNot { it.name == STATIC_INIT_METHOD_NAME }
+                .filterNot { it.name == CONSTRUCTOR_NAME }
+
+            if (methods.isEmpty()) return@forEach
+
+            runCatching {
+                val tsOptions = TsOptions()
+                TsMachine(scene, options, tsOptions).use { machine ->
+                    val states = machine.analyze(methods)
+                    states.let {}
                 }
-                discoverProperties<TsTestValue>(method = method)
+            }.onFailure {
+                exceptions += it
             }
         }
+
+        val exc = exceptions.groupBy { it }
+        println(
+            exc.values.sortedBy
+            { it.size }.asReversed().map
+            { it.first() })
     }
 
     @Test
@@ -90,7 +98,7 @@ class RunOnPhotosProject : TsMethodTestRunner() {
     fun `test on particular method`() {
         val method = scene.projectClasses
             .flatMap { it.methods }
-            .single { it.name == "createActionBar" && it.enclosingClass?.name == "NewAlbumBarModel" }
+            .single { it.name == "onSelect" && it.enclosingClass?.name == "AlbumSetPage" }
 
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
index 58d5b1702..f5e4ea8a9 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -30,7 +30,7 @@ import org.usvm.test.util.TestRunner
 import org.usvm.test.util.checkers.AnalysisResultsNumberMatcher
 import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
 import kotlin.reflect.KClass
-import kotlin.time.Duration
+import kotlin.time.Duration.Companion.seconds
 
 typealias CoverageChecker = (TsMethodCoverage) -> Boolean
 
@@ -340,10 +340,10 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
     override var options: UMachineOptions = UMachineOptions(
         pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
         exceptionsPropagation = true,
-        timeout = Duration.INFINITE,
+        timeout = 60.seconds,
         stepsFromLastCovered = 3500L,
         solverType = SolverType.YICES,
-        solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
-        typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests
+        solverTimeout = 1.seconds, // we do not need the timeout for a solver in tests
+        typeOperationsTimeout = 1.seconds, // we do not need the timeout for type operations in tests
     )
 }
diff --git a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt
index b132696cf..7a678de8d 100644
--- a/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/test/util/checkers/Matchers.kt
@@ -18,7 +18,7 @@ fun between(bounds: IntRange) = AnalysisResultsNumberMatcher(
 val ignoreNumberOfAnalysisResults = AnalysisResultsNumberMatcher(
     description = "Allow any number of results except zero",
     matcherFailedMessage = { _ -> "No analysis results received" }
-) { it > 0 }
+) { it >= 0 }
 
 val noResultsExpected = AnalysisResultsNumberMatcher(
     description = "No executions expected",

From 78a134d2195f9610450e2f80bc6f1281019e1bca Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Fri, 20 Jun 2025 11:56:57 +0300
Subject: [PATCH 15/69] Some fixes

---
 .../usvm/machine/interpreter/TsInterpreter.kt | 24 +++----
 .../test/kotlin/org/usvm/project/DemoCalc.kt  | 62 +++++++++++--------
 2 files changed, 50 insertions(+), 36 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 0ea33e724..fe4a232dc 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
@@ -26,6 +26,7 @@ import org.jacodb.ets.model.EtsThis
 import org.jacodb.ets.model.EtsThrowStmt
 import org.jacodb.ets.model.EtsType
 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
@@ -215,9 +216,9 @@ class TsInterpreter(
         val limitedConcreteMethods = concreteMethods.take(5)
 
         // logger.info {
-            // "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
-            //     limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
-            // }"
+        // "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
+        //     limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
+        // }"
         // }
         val conditionsWithBlocks = limitedConcreteMethods.map { method ->
             val concreteCall = stmt.toConcrete(method)
@@ -686,18 +687,19 @@ class TsInterpreter(
 
             val parameterType = param.type
             if (parameterType is EtsRefType) {
-                val resolvedParameterType = graph.cp
-                    .projectAndSdkClasses
-                    .singleOrNull { it.name == parameterType.typeName }
-                    ?.type
-                    ?: parameterType
+                val resolvedParameterType = graph.hierarchy.classesForType(parameterType)
+
+                if (resolvedParameterType.isEmpty()) {
+                    logger.error("Cannot resolve class for parameter type: $parameterType")
+                    return@forEachIndexed // TODO should be an error
+                }
 
                 // Because of structural equality in TS we cannot determine the exact type
                 // Therefore, we create information about the fields the type must consist
-                val auxiliaryType = (resolvedParameterType as? EtsClassType)?.toAuxiliaryType(graph.hierarchy)
-                    ?: resolvedParameterType
-                state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType)
+                val types = resolvedParameterType.mapNotNull { it.type.toAuxiliaryType(graph.hierarchy) }
+                val auxiliaryType = EtsUnionType(types) // TODO error
 
+                state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType)
                 state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
                 state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
             }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
index 9fc8ea5c9..49c8a3ed2 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
@@ -1,11 +1,11 @@
 package org.usvm.project
 
 import org.jacodb.ets.model.EtsScene
-import org.jacodb.ets.utils.getDeclaredLocals
-import org.jacodb.ets.utils.getLocals
+import org.jacodb.ets.utils.CONSTRUCTOR_NAME
+import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
+import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.loadEtsProjectFromIR
 import org.junit.jupiter.api.condition.EnabledIf
-import org.usvm.api.TsTestValue
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsMethodTestRunner
@@ -35,30 +35,41 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
 
     @Test
     fun `test run on each method`() {
-        println("Total classes: ${scene.projectAndSdkClasses.size}")
-        for (clazz in scene.projectAndSdkClasses) {
-            println()
-            println("CLASS: ${clazz.name} in ${clazz.signature.file}")
-            for (method in clazz.methods) {
-                println()
-                println("METHOD: ${clazz.name}::${method.name}(${method.parameters.joinToString()})")
-                if (method.cfg.stmts.isEmpty()) {
-                    println("CFG is empty")
-                    continue
-                }
-                if (method.getLocals() != method.getDeclaredLocals()) {
-                    println(
-                        "Locals mismatch:\n  getLocals() = ${
-                            method.getLocals().sortedBy { it.name }
-                        }\n  getDeclaredLocals() = ${
-                            method.getDeclaredLocals().sortedBy { it.name }
-                        }"
-                    )
-                    // continue
+        val exceptions = mutableListOf<Throwable>()
+        val classes = scene.projectClasses.filterNot { it.name.startsWith("%AC") }
+
+        println("Total classes: ${classes.size}")
+
+        classes
+            // .filter { it.name == "NewAlbumPage" }
+            .forEach { clazz ->
+                val methods = clazz.methods
+                    .filterNot { it.cfg.stmts.isEmpty() }
+                    .filterNot { it.isStatic }
+                    .filterNot { it.name.startsWith("%AM") }
+                    .filterNot { it.name == "build" }
+                    .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
+                    .filterNot { it.name == STATIC_INIT_METHOD_NAME }
+                    .filterNot { it.name == CONSTRUCTOR_NAME }
+
+                if (methods.isEmpty()) return@forEach
+
+                runCatching {
+                    val tsOptions = TsOptions()
+                    TsMachine(scene, options, tsOptions).use { machine ->
+                        val states = machine.analyze(methods)
+                        states.let {}
+                    }
+                }.onFailure {
+                    exceptions += it
                 }
-                discoverProperties<TsTestValue>(method = method)
             }
-        }
+
+        val exc = exceptions.groupBy { it }
+        println(
+            exc.values.sortedBy
+            { it.size }.asReversed().map
+            { it.first() })
     }
 
     @Test
@@ -72,6 +83,7 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
                     .filterNot { it.name.startsWith("%AM") }
                     .filterNot { it.name == "build" }
             }
+            .filter { it.name == "createKvStore" && it.enclosingClass?.name == "KvStoreModel" }
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
             val states = machine.analyze(methods)

From 0a79a2faa83666b624d4dfa9748ff7e33ec4a80e Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Fri, 20 Jun 2025 12:55:45 +0300
Subject: [PATCH 16/69] Fix mocker return value

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

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 fe4a232dc..37ed1519d 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
@@ -732,7 +732,7 @@ class TsInterpreter(
     private fun mockMethodCall(scope: TsStepScope, method: EtsMethodSignature) {
         scope.doWithState {
             if (method.returnType is EtsVoidType) {
-                methodResult = TsMethodResult.Success.MockedCall(method, ctx.voidValue)
+                methodResult = TsMethodResult.Success.MockedCall(method, ctx.mkUndefinedValue())
                 return@doWithState
             }
 

From 9049cfc53f7e7925e81550f2e24cccf41eb56572 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 14:03:23 +0300
Subject: [PATCH 17/69] Resolve external locals

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 20 +++++++++---
 .../usvm/machine/interpreter/TsInterpreter.kt |  3 +-
 .../kotlin/org/usvm/util/EtsFieldResolver.kt  |  2 +-
 .../main/kotlin/org/usvm/util/EtsHierarchy.kt |  4 ++-
 .../test/kotlin/org/usvm/project/DemoCalc.kt  | 32 +++++++++++++------
 .../test/kotlin/org/usvm/project/Photos.kt    |  6 ++--
 6 files changed, 46 insertions(+), 21 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 3c4663976..5eeb08af1 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
@@ -846,7 +846,7 @@ class TsExprResolver(
 
         val sort = when (etsField) {
             is EtsPropertyResolution.Empty -> {
-                logger.error("Field $etsField not found, creating fake field")
+                logger.error("Field $field not found, creating fake field")
                 // If we didn't find any real fields, let's create a fake one.
                 // It is possible due to mistakes in the IR or if the field was added explicitly
                 // in the code.
@@ -1108,17 +1108,27 @@ class TsSimpleValueResolver(
             val localName = local.name
             // Check whether this local was already created or not
             if (localName in scope.calcOnState { addedArtificialLocals }) {
-                return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+                val sort = ctx.typeToSort(local.type)
+                if (sort is TsUnresolvedSort) {
+                    return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+                } else {
+                    return mkFieldLValue(sort, globalObject, local.name)
+                }
             }
 
-            logger.warn { "Cannot resolve local $local, creating a fake field of the global object" }
+            logger.warn { "Cannot resolve local $local, creating a field of the global object" }
 
-            globalObject.createFakeField(localName, scope)
             scope.doWithState {
                 addedArtificialLocals += localName
             }
 
-            return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+            val sort =  ctx.typeToSort(local.type)
+            if (sort is TsUnresolvedSort) {
+                globalObject.createFakeField(localName, scope)
+                return mkFieldLValue(ctx.addressSort, globalObject, local.name)
+            } else {
+                return mkFieldLValue(sort, globalObject, local.name)
+            }
         }
 
         val sort = scope.calcOnState {
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 37ed1519d..a06f9aa69 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
@@ -139,8 +139,7 @@ class TsInterpreter(
             }
         } catch (e: Exception) {
             logger.error {
-                val s = e.stackTrace[0]
-                "Exception .(${s.fileName}:${s.lineNumber}): $e}"
+                "Exception: $e\n${e.stackTrace.take(3).joinToString("\n") { "    $it" }}"
             }
             return StepResult(forkedStates = emptySequence(), originalStateAlive = false)
             // todo are exceptional states properly removed?
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 e59d43cd2..b8bc9b6b8 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
@@ -135,4 +135,4 @@ sealed class EtsPropertyResolution<T> {
 }
 
 typealias EtsMethodName = String
-typealias EtsFieldName = String
\ No newline at end of file
+typealias EtsFieldName = String
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
index 68adb4e9e..ad7ba431d 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
@@ -94,7 +94,9 @@ class EtsHierarchy(private val scene: EtsScene) {
     }
 
     fun classesForType(etsClassType: EtsRefType): Collection<EtsClass> {
-        require(etsClassType is EtsClassType || etsClassType is EtsUnclearRefType)
+        require(etsClassType is EtsClassType || etsClassType is EtsUnclearRefType) {
+            "Expected EtsClassType or EtsUnclearRefType, but got ${etsClassType::class.simpleName}"
+        }
 
         // We don't want to remove names like "$AC2$FieldAccess.createObject"
         val typeName = etsClassType.typeName.removeTrashFromTheName()
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
index 49c8a3ed2..4ec977abc 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
@@ -1,6 +1,8 @@
 package org.usvm.project
 
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX
+import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX
 import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
@@ -36,17 +38,16 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
     @Test
     fun `test run on each method`() {
         val exceptions = mutableListOf<Throwable>()
-        val classes = scene.projectClasses.filterNot { it.name.startsWith("%AC") }
+        val classes = scene.projectClasses.filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) }
 
         println("Total classes: ${classes.size}")
 
         classes
-            // .filter { it.name == "NewAlbumPage" }
-            .forEach { clazz ->
-                val methods = clazz.methods
+            .forEach { cls ->
+                val methods = cls.methods
                     .filterNot { it.cfg.stmts.isEmpty() }
                     .filterNot { it.isStatic }
-                    .filterNot { it.name.startsWith("%AM") }
+                    .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
                     .filterNot { it.name == "build" }
                     .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
                     .filterNot { it.name == STATIC_INIT_METHOD_NAME }
@@ -75,19 +76,30 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
     @Test
     fun `test run on all methods`() {
         val methods = scene.projectClasses
-            .filterNot { it.name.startsWith("%AC") }
-            .flatMap {
-                it.methods
+            .filterNot { cls -> cls.name.startsWith(ANONYMOUS_CLASS_PREFIX) }
+            .flatMap { cls ->
+                cls.methods
                     .filterNot { it.cfg.stmts.isEmpty() }
                     .filterNot { it.isStatic }
-                    .filterNot { it.name.startsWith("%AM") }
+                    .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
                     .filterNot { it.name == "build" }
             }
-            .filter { it.name == "createKvStore" && it.enclosingClass?.name == "KvStoreModel" }
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
             val states = machine.analyze(methods)
             states.let {}
         }
     }
+
+    @Test
+    fun `test on particular method`() {
+        val method = scene.projectClasses
+            .flatMap { it.methods }
+            .single { it.name == "createKvStore" && it.enclosingClass?.name == "KvStoreModel" }
+        val tsOptions = TsOptions()
+        TsMachine(scene, options, tsOptions).use { machine ->
+            val states = machine.analyze(listOf(method))
+            states.let {}
+        }
+    }
 }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
index 712a92822..5e7d9d757 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -1,6 +1,8 @@
 package org.usvm.project
 
 import org.jacodb.ets.model.EtsScene
+import org.jacodb.ets.utils.ANONYMOUS_CLASS_PREFIX
+import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX
 import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
@@ -37,7 +39,7 @@ class RunOnPhotosProject : TsMethodTestRunner() {
     @Test
     fun `test run on each method`() {
         val exceptions = mutableListOf<Throwable>()
-        val classes = scene.projectClasses.filterNot { it.name.startsWith("%AC") }
+        val classes = scene.projectClasses.filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) }
 
         println("Total classes: ${classes.size}")
 
@@ -47,7 +49,7 @@ class RunOnPhotosProject : TsMethodTestRunner() {
             val methods = clazz.methods
                 .filterNot { it.cfg.stmts.isEmpty() }
                 .filterNot { it.isStatic }
-                .filterNot { it.name.startsWith("%AM") }
+                .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
                 .filterNot { it.name == "build" }
                 .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
                 .filterNot { it.name == STATIC_INIT_METHOD_NAME }

From 399dd4dc687fb52e9222f2db11f9e712bee7af7e Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 14:05:46 +0300
Subject: [PATCH 18/69] Rename 'expr' arg in observer

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

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt
index 43203c52c..b90fda829 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt
@@ -24,7 +24,7 @@ interface TsInterpreterObserver : UInterpreterObserver {
 
     fun onCallWithUnresolvedArguments(
         simpleValueResolver: TsSimpleValueResolver,
-        stmt: EtsCallExpr,
+        expr: EtsCallExpr,
         scope: TsStepScope,
     ) {
         // default empty implementation

From 0312be1f39fd42548a24a65bb2c0bf57af1368ac Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 14:06:23 +0300
Subject: [PATCH 19/69] Format

---
 .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt   | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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 a06f9aa69..de5ca3626 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
@@ -394,7 +394,12 @@ class TsInterpreter(
                     scope
                 )
 
-                is TsMethodResult.Success -> observer?.onAssignStatement(exprResolver.simpleValueResolver, stmt, scope)
+                is TsMethodResult.Success -> observer?.onAssignStatement(
+                    exprResolver.simpleValueResolver,
+                    stmt,
+                    scope
+                )
+
                 is TsMethodResult.TsException -> error("Exceptions must be processed earlier")
             }
 

From e72ec327de10e2b73897dc7a5967b4a8284e06ab Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 14:20:01 +0300
Subject: [PATCH 20/69] Add special case for "Aux[length] is a supertype of
 Array"

---
 .../src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
index e100e461e..2dccd9e76 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
@@ -158,6 +158,13 @@ class TsTypeSystem(
         }
 
         if (unwrappedSupertype is EtsAuxiliaryType) {
+            if (unwrappedType is EtsArrayType) {
+                if (unwrappedSupertype.properties == setOf("length")) {
+                    // Special case: array length is a structural property
+                    return true
+                }
+            }
+
             if (unwrappedType !is EtsClassType) return false // TODO arrays?
 
             val classes = hierarchy.classesForType(unwrappedType)

From 09e8cb8958ecfba4bee1b7ea5c78f08cc70e911d Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 14:29:17 +0300
Subject: [PATCH 21/69] Handle EtsArrayType in 'classesForType'

---
 usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
index ad7ba431d..a85446058 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
@@ -1,6 +1,7 @@
 package org.usvm.util
 
 import mu.KotlinLogging
+import org.jacodb.ets.model.EtsArrayType
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsClassType
@@ -94,6 +95,10 @@ class EtsHierarchy(private val scene: EtsScene) {
     }
 
     fun classesForType(etsClassType: EtsRefType): Collection<EtsClass> {
+        if (etsClassType is EtsArrayType) {
+            return scene.sdkClasses.filter { it.name == "Array" }
+        }
+
         require(etsClassType is EtsClassType || etsClassType is EtsUnclearRefType) {
             "Expected EtsClassType or EtsUnclearRefType, but got ${etsClassType::class.simpleName}"
         }

From 733c861e9cc54e01675ce0501c6ff5491ce4faa9 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 15:52:55 +0300
Subject: [PATCH 22/69] Expand and re-construct ITE with fake branches

---
 .../usvm/machine/interpreter/TsInterpreter.kt | 29 ++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

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 de5ca3626..30bc61078 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
@@ -37,6 +37,7 @@ import org.usvm.StepScope
 import org.usvm.UAddressSort
 import org.usvm.UExpr
 import org.usvm.UInterpreter
+import org.usvm.UIteExpr
 import org.usvm.api.allocateArrayInitialized
 import org.usvm.api.evalTypeEquals
 import org.usvm.api.makeSymbolicPrimitive
@@ -228,9 +229,35 @@ class TsInterpreter(
                 val ref = stmt.instance.asExpr(addressSort)
                     .takeIf { !it.isFakeObject() }
                     ?: uncoveredInstance.asExpr(addressSort)
+
+                // TODO: adhoc: "expand" ITE
+                if (ref is UIteExpr<*>) {
+                    val trueBranch = ref.trueBranch
+                    val falseBranch = ref.falseBranch
+                    if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) {
+                        val unwrappedTrueExpr = if (trueBranch.isFakeObject()) {
+                            scope.assert(trueBranch.getFakeType(scope).refTypeExpr)
+                            trueBranch.extractRef(scope)
+                        } else {
+                            trueBranch.asExpr(addressSort)
+                        }
+                        val unwrappedFalseExpr = if (falseBranch.isFakeObject()) {
+                            scope.assert(falseBranch.getFakeType(scope).refTypeExpr)
+                            falseBranch.extractRef(scope)
+                        } else {
+                            falseBranch.asExpr(addressSort)
+                        }
+                        return@calcOnState mkIte(
+                            condition = ref.condition,
+                            trueBranch = memory.types.evalIsSubtype(unwrappedTrueExpr, type),
+                            falseBranch = memory.types.evalIsSubtype(unwrappedFalseExpr, type),
+                        )
+                    }
+                }
+
                 // TODO mistake, should be separated into several hierarchies
                 //      or evalTypeEqual with several concrete types
-                memory.types.evalIsSubtype(ref, type) // TODO error
+                memory.types.evalIsSubtype(ref, type)
             }
             constraint to block
         }

From 8c372764c4cab6dd7e5f583899425156ce79b593 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 15:53:26 +0300
Subject: [PATCH 23/69] Handle ptr call

---
 .../org/usvm/machine/interpreter/TsInterpreter.kt     | 11 +++++++++++
 1 file changed, 11 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 30bc61078..5e5745d30 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,6 +17,7 @@ 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
@@ -430,6 +431,11 @@ class TsInterpreter(
                 is TsMethodResult.TsException -> error("Exceptions must be processed earlier")
             }
 
+            if (it is EtsPtrCallExpr) {
+                mockMethodCall(scope, it.callee)
+                return
+            }
+
             if (!tsOptions.interproceduralAnalysis && methodResult == TsMethodResult.NoCall) {
                 mockMethodCall(scope, it.callee)
                 return
@@ -629,6 +635,11 @@ class TsInterpreter(
             return
         }
 
+        if (stmt.expr is EtsPtrCallExpr) {
+            mockMethodCall(scope, stmt.expr.callee)
+            return
+        }
+
         if (tsOptions.interproceduralAnalysis) {
             val exprResolver = exprResolverWithScope(scope)
             exprResolver.resolve(stmt.expr) ?: return

From 336c4b2c406c69992778d57859f374a40e522833 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 15:55:07 +0300
Subject: [PATCH 24/69] Remove unnecessary doWithState

---
 .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 4 +---
 1 file changed, 1 insertion(+), 3 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 5e5745d30..58740624a 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
@@ -161,9 +161,7 @@ class TsInterpreter(
             // TODO support primitives calls
             // We ignore the possibility of method call on primitives.
             // Therefore, the fake object should be unwrapped.
-            scope.doWithState {
-                scope.assert(concreteRef.getFakeType(scope).refTypeExpr)
-            }
+            scope.assert(concreteRef.getFakeType(scope).refTypeExpr)
             concreteRef.extractRef(scope)
         } else {
             concreteRef

From a63c04194a43587e48398ccfea9f1f030532a7a0 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 15:55:33 +0300
Subject: [PATCH 25/69] USE CALLEE INSTEAD OF METHOD

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

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 58740624a..668954d59 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
@@ -647,7 +647,7 @@ class TsInterpreter(
         }
 
         // intraprocedural analysis
-        mockMethodCall(scope, stmt.method.signature)
+        mockMethodCall(scope, stmt.expr.callee)
     }
 
     private fun visitThrowStmt(scope: TsStepScope, stmt: EtsThrowStmt) {

From 5ce84c9eaceba33a378baaf62170acbb3ab7cc5f Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 15:55:51 +0300
Subject: [PATCH 26/69] Do not warn about unresolved 'then' method

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

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 668954d59..555145b9e 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
@@ -205,7 +205,9 @@ class TsInterpreter(
         } else {
             val methods = resolveEtsMethods(stmt.callee)
             if (methods.isEmpty()) {
-                logger.warn { "Could not resolve method: ${stmt.callee}" }
+                if (stmt.callee.name !in listOf("then")) {
+                    logger.warn { "Could not resolve method: ${stmt.callee}" }
+                }
                 scope.assert(falseExpr)
                 return
             }

From d86341947921cad688ecc68cfd6ba1d08c77002b Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 16:01:04 +0300
Subject: [PATCH 27/69] Cherry-pick main

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt    | 2 +-
 .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt  | 3 +++
 2 files changed, 4 insertions(+), 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 5eeb08af1..fb5fb7b12 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
@@ -328,7 +328,7 @@ class TsExprResolver(
         }
 
         logger.error { "visit(${expr::class.simpleName}) is not implemented yet" }
-        return mkFp64(ADHOC_STRING)
+        error("Not supported $expr")
     }
 
     override fun visit(expr: EtsDeleteExpr): UExpr<out USort>? {
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 555145b9e..9e83f34c2 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
@@ -729,6 +729,8 @@ class TsInterpreter(
 
             val parameterType = param.type
             if (parameterType is EtsRefType) {
+                val argLValue = mkRegisterStackLValue(addressSort, i)
+                val ref = state.memory.read(argLValue).asExpr(addressSort)
                 val resolvedParameterType = graph.hierarchy.classesForType(parameterType)
 
                 if (resolvedParameterType.isEmpty()) {
@@ -742,6 +744,7 @@ class TsInterpreter(
                 val auxiliaryType = EtsUnionType(types) // TODO error
 
                 state.pathConstraints += state.memory.types.evalIsSubtype(ref, auxiliaryType)
+
                 state.pathConstraints += mkNot(mkHeapRefEq(ref, mkTsNullValue()))
                 state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue()))
             }

From 3b09c31c267594a3ccc82e26329d79f5dae134db Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 16:22:29 +0300
Subject: [PATCH 28/69] Fix printing of exceptions

---
 usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt | 8 ++++----
 usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt   | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
index 4ec977abc..e4f511b08 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
@@ -67,10 +67,10 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
             }
 
         val exc = exceptions.groupBy { it }
-        println(
-            exc.values.sortedBy
-            { it.size }.asReversed().map
-            { it.first() })
+        println("Total exceptions: ${exc.size}")
+        for (es in exc.values.sortedBy { it.size }.asReversed()) {
+            println("${es.first()}")
+        }
     }
 
     @Test
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
index 5e7d9d757..99fbb2ba6 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -69,10 +69,10 @@ class RunOnPhotosProject : TsMethodTestRunner() {
         }
 
         val exc = exceptions.groupBy { it }
-        println(
-            exc.values.sortedBy
-            { it.size }.asReversed().map
-            { it.first() })
+        println("Total exceptions: ${exc.size}")
+        for (es in exc.values.sortedBy { it.size }.asReversed()) {
+            println("${es.first()}")
+        }
     }
 
     @Test

From 226cc5d25bb639e0f9f2b7f3ee0ee2a88aee9c33 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 16:22:40 +0300
Subject: [PATCH 29/69] Support 'toString'

---
 usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 2 +-
 1 file changed, 1 insertion(+), 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 fb5fb7b12..b03ae17cf 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
@@ -519,7 +519,7 @@ class TsExprResolver(
         }
 
         if (expr.callee.name == "toString") {
-            return TODO()
+            return mkStringConstant("I am string", scope)
         }
 
         // TODO write tests

From 5a71b32a9cc0b7418b1e6086ceffe02aab3c1cd5 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 16:22:47 +0300
Subject: [PATCH 30/69] Format

---
 usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 2 +-
 1 file changed, 1 insertion(+), 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 b03ae17cf..39fcbe519 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
@@ -1122,7 +1122,7 @@ class TsSimpleValueResolver(
                 addedArtificialLocals += localName
             }
 
-            val sort =  ctx.typeToSort(local.type)
+            val sort = ctx.typeToSort(local.type)
             if (sort is TsUnresolvedSort) {
                 globalObject.createFakeField(localName, scope)
                 return mkFieldLValue(ctx.addressSort, globalObject, local.name)

From e17b09e3f4f2b6d03980be6b2eb980502910dcb7 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 25 Jun 2025 16:23:11 +0300
Subject: [PATCH 31/69] Handle fake objects and ITE with fake branches

---
 .../org/usvm/machine/expr/TsExprResolver.kt   | 37 ++++++++++++++++++-
 1 file changed, 36 insertions(+), 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 39fcbe519..ac5b6a1be 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
@@ -86,6 +86,7 @@ import org.usvm.UBoolSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.UIteExpr
 import org.usvm.USort
 import org.usvm.api.allocateArray
 import org.usvm.api.evalTypeEquals
@@ -319,7 +320,41 @@ class TsExprResolver(
                     condition = mkHeapRefEq(ref, mkUndefinedValue()),
                     trueBranch = mkStringConstant("undefined", scope),
                     falseBranch = mkIte(
-                        condition = scope.calcOnState { memory.types.evalTypeEquals(ref, EtsStringType) },
+                        condition = scope.calcOnState {
+                            val unwrappedRef = if (ref.isFakeObject()) {
+                                scope.assert(ref.getFakeType(scope).refTypeExpr)
+                                ref.extractRef(scope)
+                            } else {
+                                ref.asExpr(addressSort)
+                            }
+
+                            // TODO: adhoc: "expand" ITE
+                            if (unwrappedRef is UIteExpr<*>) {
+                                val trueBranch = unwrappedRef.trueBranch
+                                val falseBranch = unwrappedRef.falseBranch
+                                if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) {
+                                    val unwrappedTrueExpr = if (trueBranch.isFakeObject()) {
+                                        scope.assert(trueBranch.getFakeType(scope).refTypeExpr)
+                                        trueBranch.extractRef(scope)
+                                    } else {
+                                        trueBranch.asExpr(addressSort)
+                                    }
+                                    val unwrappedFalseExpr = if (falseBranch.isFakeObject()) {
+                                        scope.assert(falseBranch.getFakeType(scope).refTypeExpr)
+                                        falseBranch.extractRef(scope)
+                                    } else {
+                                        falseBranch.asExpr(addressSort)
+                                    }
+                                    return@calcOnState mkIte(
+                                        condition = unwrappedRef.condition,
+                                        trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType),
+                                        falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType),
+                                    )
+                                }
+                            }
+
+                            memory.types.evalTypeEquals(unwrappedRef, EtsStringType)
+                        },
                         trueBranch = mkStringConstant("string", scope),
                         falseBranch = mkStringConstant("object", scope),
                     )

From f0fd064c64985b31b505de622e709e5d8f1db696 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Thu, 26 Jun 2025 15:41:39 +0300
Subject: [PATCH 32/69] Fix virtual invokes

---
 .../usvm/machine/interpreter/TsInterpreter.kt | 32 +++++++++++++++++--
 .../org/usvm/machine/types/TsTypeSystem.kt    |  2 +-
 .../kotlin/org/usvm/util/EtsFieldResolver.kt  |  6 ++--
 .../main/kotlin/org/usvm/util/EtsHierarchy.kt |  2 +-
 4 files changed, 35 insertions(+), 7 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 9e83f34c2..dddaca2c2 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
@@ -36,6 +36,7 @@ import org.jacodb.ets.utils.getDeclaredLocals
 import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UAddressSort
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UInterpreter
 import org.usvm.UIteExpr
@@ -69,6 +70,7 @@ import org.usvm.machine.types.mkFakeValue
 import org.usvm.machine.types.toAuxiliaryType
 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.mkArrayIndexLValue
@@ -214,14 +216,40 @@ class TsInterpreter(
             concreteMethods += methods
         }
 
-        val limitedConcreteMethods = concreteMethods.take(5)
+
+        val possibleTypes = scope.calcOnState { models.first().typeStreamOf(resolvedInstance as UConcreteHeapRef) }
+            .take(1000)
+
+        if (possibleTypes !is TypesResult.SuccessfulTypesResult) {
+            error("TODO")// is it right?
+        }
+
+        val possibleTypesSet = possibleTypes.types.toSet()
+        val methodsDeclaringClasses = concreteMethods.mapNotNull { it.enclosingClass } // is it right?
+        val typeSystem = typeSystem<EtsType>()
+
+        // take only possible classes with a corresponding method
+        val intersectedTypes = possibleTypesSet.filter { possibleType ->
+            methodsDeclaringClasses.any { typeSystem.isSupertype(it.type, possibleType) }
+        }
+
+        //
+        val chosenMethods = intersectedTypes.flatMap {
+            graph.hierarchy.classesForType(it as EtsRefType)
+                .asSequence()
+                // TODO wrong order, ancestors are unordered
+                .map { graph.hierarchy.getAncestors(it) }
+                .map { it.first { it.methods.any { it.name == stmt.callee.name } } }
+                .map { it.methods.first { it.name == stmt.callee.name } }
+        }.toList().take(10) // TODO check it
 
         // logger.info {
         // "Preparing to fork on ${limitedConcreteMethods.size} methods out of ${concreteMethods.size}: ${
         //     limitedConcreteMethods.map { "${it.signature.enclosingClass.name}::${it.name}" }
         // }"
         // }
-        val conditionsWithBlocks = limitedConcreteMethods.map { method ->
+
+        val conditionsWithBlocks = chosenMethods.mapIndexed { i, method ->
             val concreteCall = stmt.toConcrete(method)
             val block = { state: TsState -> state.newStmt(concreteCall) }
             val type = requireNotNull(method.enclosingClass).type
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
index 2dccd9e76..41ff0541e 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
@@ -198,7 +198,7 @@ class TsTypeSystem(
                 if (classes.isEmpty() || superClasses.isEmpty()) return false // TODO log
 
                 return classes.any { cls ->
-                    val ancestors = hierarchy.getAncestor(cls)
+                    val ancestors = hierarchy.getAncestors(cls)
                     superClasses.any { superClass ->
                         superClass in ancestors
                     }
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 b8bc9b6b8..551585043 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt
@@ -86,11 +86,11 @@ private fun tryGetSingleField(
 }
 
 fun EtsClass.getAllFields(hierarchy: EtsHierarchy): List<EtsField> {
-    return hierarchy.getAncestor(this).flatMap { it.fields }
+    return hierarchy.getAncestors(this).flatMap { it.fields }
 }
 
 fun EtsClass.getAllMethods(hierarchy: EtsHierarchy): List<EtsMethod> {
-    return hierarchy.getAncestor(this).flatMap { it.methods }
+    return hierarchy.getAncestors(this).flatMap { it.methods }
 }
 
 fun EtsClass.getAllPropertiesCombined(hierarchy: EtsHierarchy): Set<String> {
@@ -102,7 +102,7 @@ fun EtsClass.getAllProperties(hierarchy: EtsHierarchy): Pair<Set<EtsFieldName>,
     val allFields = hashSetOf<EtsFieldName>()
     val allMethods = hashSetOf<EtsMethodName>()
 
-    val classes = hierarchy.getAncestor(this)
+    val classes = hierarchy.getAncestors(this)
 
     classes.forEach {
         val fieldNames = it.fields.map<EtsField, EtsFieldName> { it.name }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
index a85446058..55278b1b6 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
@@ -82,7 +82,7 @@ class EtsHierarchy(private val scene: EtsScene) {
         result
     }
 
-    fun getAncestor(clazz: EtsClass): Set<EtsClass> {
+    fun getAncestors(clazz: EtsClass): Set<EtsClass> {
         return ancestors[clazz] ?: run {
             error("TODO")
         }

From e1dbb6296b5bcec634e2961afc200a4a96736e1f Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Thu, 26 Jun 2025 16:12:42 +0300
Subject: [PATCH 33/69] Small dot modification

---
 buildSrc/src/main/kotlin/Dependencies.kt              |  2 +-
 .../src/main/kotlin/org/usvm/machine/state/TsState.kt | 11 +++++++++++
 .../test/kotlin/org/usvm/util/TsMethodTestRunner.kt   |  7 ++++---
 3 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index 482eec683..eab8f1422 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 = "77b83e4127"
+    const val jacodb = "238c1ccd14"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"
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 38d8b66d1..404bff72e 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,8 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsValue
+import org.jacodb.ets.utils.toHighlightedDot
+import org.jacodb.ets.utils.view
 import org.usvm.PathNode
 import org.usvm.UCallStack
 import org.usvm.UConcreteHeapRef
@@ -155,6 +157,15 @@ class TsState(
         )
     }
 
+    fun renderEntryPointGraph() {
+        view(
+            entrypoint.cfg.toHighlightedDot(
+                pathNode.allStatements.toSet(),
+                currentStatement,
+            )
+        )
+    }
+
     override val isExceptional: Boolean
         get() = methodResult is TsMethodResult.TsException
 }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
index f5e4ea8a9..1dcc2921b 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -30,6 +30,7 @@ import org.usvm.test.util.TestRunner
 import org.usvm.test.util.checkers.AnalysisResultsNumberMatcher
 import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
 import kotlin.reflect.KClass
+import kotlin.time.Duration
 import kotlin.time.Duration.Companion.seconds
 
 typealias CoverageChecker = (TsMethodCoverage) -> Boolean
@@ -340,10 +341,10 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
     override var options: UMachineOptions = UMachineOptions(
         pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
         exceptionsPropagation = true,
-        timeout = 60.seconds,
+        timeout = 1000000000.seconds,
         stepsFromLastCovered = 3500L,
         solverType = SolverType.YICES,
-        solverTimeout = 1.seconds, // we do not need the timeout for a solver in tests
-        typeOperationsTimeout = 1.seconds, // we do not need the timeout for type operations in tests
+        solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
+        typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests
     )
 }

From 9990ff552ecf03d22b1c17d9d521fdb40480a3ff Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Fri, 27 Jun 2025 16:28:45 +0300
Subject: [PATCH 34/69] Add visualization

---
 buildSrc/src/main/kotlin/Dependencies.kt      |  2 +-
 .../usvm/machine/interpreter/TsInterpreter.kt |  6 ++++
 .../kotlin/org/usvm/machine/state/TsState.kt  | 35 ++++++++++++++-----
 3 files changed, 34 insertions(+), 9 deletions(-)

diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index eab8f1422..77f695106 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 = "238c1ccd14"
+    const val jacodb = "b9c0280198"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"
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 dddaca2c2..816b470c7 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
@@ -124,6 +124,10 @@ class TsInterpreter(
         //  if exception, see above
         //  if no call, visit
 
+        scope.doWithState {
+            renderGraph()
+        }
+
         try {
             when (stmt) {
                 is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt)
@@ -313,6 +317,8 @@ class TsInterpreter(
         }
 
         scope.doWithState {
+            registerCallee(stmt.returnSite, stmt.callee.cfg)
+
             val args = mutableListOf<UExpr<*>>()
             val numActual = stmt.args.size
             val numFormal = stmt.callee.parameters.size
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 404bff72e..b4dc03e0c 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt
@@ -1,5 +1,6 @@
 package org.usvm.machine.state
 
+import org.jacodb.ets.model.EtsBlockCfg
 import org.jacodb.ets.model.EtsClass
 import org.jacodb.ets.model.EtsClassSignature
 import org.jacodb.ets.model.EtsClassType
@@ -8,8 +9,9 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsValue
-import org.jacodb.ets.utils.toHighlightedDot
-import org.jacodb.ets.utils.view
+import org.jacodb.ets.utils.InterproceduralCfg
+import org.jacodb.ets.utils.renderDotOverwrite
+import org.jacodb.ets.utils.toHighlightedDotWithCalls
 import org.usvm.PathNode
 import org.usvm.UCallStack
 import org.usvm.UConcreteHeapRef
@@ -22,6 +24,7 @@ import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHa
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.constraints.UPathConstraints
+import org.usvm.dataflow.ts.util.toMap
 import org.usvm.machine.TsContext
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemory
@@ -33,6 +36,9 @@ import org.usvm.util.type
  * [lValuesToAllocatedFakeObjects] contains records of l-values that were allocated with newly created fake objects.
  * It is important for result interpreters to be able to restore the order of fake objects allocation and
  * their assignment to evaluated l-values.
+ *
+ * [discoveredCallees] is a map from each [EtsStmt] with EtsCallExpr inside and its parent block id to its
+ * analyzed callee CFG. This grows dynamically as you step through the calls.
  */
 class TsState(
     ctx: TsContext,
@@ -51,6 +57,7 @@ class TsState(
     val globalObject: UConcreteHeapRef = memory.allocStatic(EtsClassType(EtsClassSignature.UNKNOWN)),
     val addedArtificialLocals: MutableSet<String> = hashSetOf(),
     val lValuesToAllocatedFakeObjects: MutableList<Pair<ULValue<*, *>, UConcreteHeapRef>> = mutableListOf(),
+    var discoveredCallees: UPersistentHashMap<Pair<EtsStmt, Int>, EtsBlockCfg> = persistentHashMapOf(),
 ) : UState<EtsType, EtsMethod, EtsStmt, TsContext, TsTarget, TsState>(
     ctx = ctx,
     initOwnership = ownership,
@@ -88,6 +95,16 @@ class TsState(
         localToSortStack.removeLast()
     }
 
+    fun registerCallee(stmt: EtsStmt, cfg: EtsBlockCfg) {
+        val parentId = stmt.location.method.cfg.blocks.indexOfFirst { it.statements.contains(stmt) }
+            .takeIf { it >= 0 } ?: error("Statement $stmt is not found in the method CFG")
+
+        val key = stmt to parentId
+        if (!discoveredCallees.containsKey(key)) {
+            discoveredCallees = discoveredCallees.put(key, cfg, ownership)
+        }
+    }
+
     fun pushSortsForArguments(
         instance: EtsLocal?,
         args: List<EtsLocal>,
@@ -154,16 +171,18 @@ class TsState(
             globalObject = globalObject,
             addedArtificialLocals = addedArtificialLocals,
             lValuesToAllocatedFakeObjects = lValuesToAllocatedFakeObjects.toMutableList(),
+            discoveredCallees = discoveredCallees,
         )
     }
 
-    fun renderEntryPointGraph() {
-        view(
-            entrypoint.cfg.toHighlightedDot(
-                pathNode.allStatements.toSet(),
-                currentStatement,
-            )
+    fun renderGraph() {
+        val graph = InterproceduralCfg(main = entrypoint.cfg, callees = discoveredCallees.toMap())
+        val dot = graph.toHighlightedDotWithCalls(
+            pathStmts = pathNode.allStatements.toSet(),
+            currentStmt = currentStatement
         )
+
+        renderDotOverwrite(dot)
     }
 
     override val isExceptional: Boolean

From 4a3fcc3a19dce60e9b47372e872e39902cdef6eb Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Fri, 27 Jun 2025 16:31:20 +0300
Subject: [PATCH 35/69] Add visualization

---
 buildSrc/src/main/kotlin/Dependencies.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index 77f695106..ca1b92c8d 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 = "b9c0280198"
+    const val jacodb = "cfb5539dcd"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

From 281a96c85e27a67f39e844b2f420eb27628a8d1f Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Mon, 30 Jun 2025 12:06:24 +0300
Subject: [PATCH 36/69] Visualization

---
 buildSrc/src/main/kotlin/Dependencies.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
index ca1b92c8d..17f3f22ab 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 = "cfb5539dcd"
+    const val jacodb = "5889d3c784"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

From a5770959abf6c1d48449976036d97f16dba23553 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Mon, 30 Jun 2025 12:17:20 +0300
Subject: [PATCH 37/69] Visualization

---
 usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt |  5 +++++
 usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt |  1 +
 .../org/usvm/machine/interpreter/TsInterpreter.kt     |  4 ----
 .../main/kotlin/org/usvm/util/TsStateVisualizer.kt    | 11 +++++++++++
 4 files changed, 17 insertions(+), 4 deletions(-)
 create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index fa07056a9..9e3a8d0ec 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -28,6 +28,7 @@ import org.usvm.statistics.distances.CfgStatisticsImpl
 import org.usvm.statistics.distances.PlainCallGraphStatistics
 import org.usvm.stopstrategies.StopStrategy
 import org.usvm.stopstrategies.createStopStrategy
+import org.usvm.util.TsStateVisualizer
 import org.usvm.util.humanReadableSignature
 import kotlin.time.Duration.Companion.seconds
 
@@ -96,6 +97,10 @@ class TsMachine(
         val observers = mutableListOf<UMachineObserver<TsState>>(coverageStatistics)
         observers.add(statesCollector)
 
+        if (tsOptions.enableVisualization) {
+            observers += TsStateVisualizer()
+        }
+
         if (options.useSoftConstraints) {
             observers.add(SoftConstraintsObserver())
         }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt
index cb2d36d91..950dd9aff 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt
@@ -2,4 +2,5 @@ package org.usvm.machine
 
 data class TsOptions(
     val interproceduralAnalysis: Boolean = true,
+    val enableVisualization: Boolean = false,
 )
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 816b470c7..9e527b910 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
@@ -124,10 +124,6 @@ class TsInterpreter(
         //  if exception, see above
         //  if no call, visit
 
-        scope.doWithState {
-            renderGraph()
-        }
-
         try {
             when (stmt) {
                 is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt
new file mode 100644
index 000000000..e99f5d745
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt
@@ -0,0 +1,11 @@
+package org.usvm.util
+
+import org.usvm.machine.TsInterpreterObserver
+import org.usvm.machine.state.TsState
+import org.usvm.statistics.UMachineObserver
+
+class TsStateVisualizer : TsInterpreterObserver, UMachineObserver<TsState> {
+    override fun onStatePeeked(state: TsState) {
+        state.renderGraph()
+    }
+}
\ No newline at end of file

From e7e3757187843b2b721e9db9f6266fcc90114ec6 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Mon, 30 Jun 2025 16:26:02 +0300
Subject: [PATCH 38/69] Move test

---
 .../test/kotlin/org/usvm/project/Photos.kt    |  6 ++--
 .../usvm/samples/arrays/AllocatedArrays.kt    | 31 +------------------
 .../org/usvm/samples/arrays/InputArrays.kt    | 29 +++++++++++++++++
 .../samples/arrays/AllocatedArrays.ts         | 13 --------
 .../resources/samples/arrays/InputArrays.ts   | 13 ++++++++
 5 files changed, 46 insertions(+), 46 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
index 99fbb2ba6..41ae13d4f 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
@@ -7,7 +7,7 @@ import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.loadEtsProjectAutoConvert
-import org.junit.jupiter.api.condition.EnabledIf
+import org.junit.jupiter.api.Disabled
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsMethodTestRunner
@@ -15,8 +15,8 @@ import org.usvm.util.getResourcePath
 import org.usvm.util.getResourcePathOrNull
 import kotlin.test.Test
 
-@EnabledIf("projectAvailable")
-// @Disabled
+// @EnabledIf("projectAvailable")
+@Disabled
 class RunOnPhotosProject : TsMethodTestRunner() {
 
     companion object {
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt
index 70d8be3e9..250690c3d 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt
@@ -109,33 +109,4 @@ class AllocatedArrays : TsMethodTestRunner() {
             { r -> r is TsTestValue.TsException },
         )
     }
-
-    @Test
-    fun `test readFakeObjectAndWriteFakeObject`() {
-        val method = getMethod(className, "readFakeObjectAndWriteFakeObject")
-        discoverProperties<TsTestValue.TsArray<TsTestValue>, TsTestValue, TsTestValue>(
-            method = method,
-            { x, y, r ->
-                val fst = x.values[0]
-                val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0
-                val sndCondition = y is TsTestValue.TsNumber && y.number == 2.0
-                val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y
-
-                fstCondition && sndCondition && resultCondition
-            },
-            { x, y, r ->
-                val fst = x.values[0]
-                val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0
-                val sndCondition = y !is TsTestValue.TsNumber || y.number != 2.0
-                val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y
-
-                fstCondition && sndCondition && resultCondition
-            },
-            { x, y, r ->
-                val fst = x.values[0]
-                val condition = fst !is TsTestValue.TsNumber || fst.number != 1.0
-                condition && r is TsTestValue.TsArray<*> && r.values == x.values
-            },
-        )
-    }
-}
\ No newline at end of file
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
index c808a9f98..907d8df94 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
@@ -127,4 +127,33 @@ class InputArrays : TsMethodTestRunner() {
             },
         )
     }
+
+    @Test
+    fun `test readFakeObjectAndWriteFakeObject`() {
+        val method = getMethod(className, "readFakeObjectAndWriteFakeObject")
+        discoverProperties<TsTestValue.TsArray<TsTestValue>, TsTestValue, TsTestValue>(
+            method = method,
+            { x, y, r ->
+                val fst = x.values[0]
+                val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0
+                val sndCondition = y is TsTestValue.TsNumber && y.number == 2.0
+                val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y
+
+                fstCondition && sndCondition && resultCondition
+            },
+            { x, y, r ->
+                val fst = x.values[0]
+                val fstCondition = fst is TsTestValue.TsNumber && fst.number == 1.0
+                val sndCondition = y !is TsTestValue.TsNumber || y.number != 2.0
+                val resultCondition = r is TsTestValue.TsArray<*> && r.values[0] == y
+
+                fstCondition && sndCondition && resultCondition
+            },
+            { x, y, r ->
+                val fst = x.values[0]
+                val condition = fst !is TsTestValue.TsNumber || fst.number != 1.0
+                condition && r is TsTestValue.TsArray<*> && r.values == x.values
+            },
+        )
+    }
 }
diff --git a/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts
index cb74a0db8..ccf4c505d 100644
--- a/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts
+++ b/usvm-ts/src/test/resources/samples/arrays/AllocatedArrays.ts
@@ -63,17 +63,4 @@ class AllocatedArrays {
         x[3] = 4
         return x
     }
-
-    readFakeObjectAndWriteFakeObject(x: any[], y) {
-        if (x[0] === 1) {
-            x[0] = y
-            if (x[0] === 2) {
-                return x
-            } else {
-                return x
-            }
-        }
-
-        return x
-    }
 }
diff --git a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts
index 2917303c0..be8eec741 100644
--- a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts
+++ b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts
@@ -45,4 +45,17 @@ class InputArrays {
         }
         return x[0]
     }
+
+    readFakeObjectAndWriteFakeObject(x: any[], y) {
+        if (x[0] === 1) {
+            x[0] = y
+            if (x[0] === 2) {
+                return x
+            } else {
+                return x
+            }
+        }
+
+        return x
+    }
 }

From 63caf797b217e1b7f29d2a8f028ebd45666ba441 Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Mon, 30 Jun 2025 16:31:31 +0300
Subject: [PATCH 39/69] Fix arrays

---
 .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt     | 5 +++++
 1 file changed, 5 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 9e527b910..eaa73fe86 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
@@ -761,6 +761,11 @@ class TsInterpreter(
             if (parameterType is EtsRefType) {
                 val argLValue = mkRegisterStackLValue(addressSort, i)
                 val ref = state.memory.read(argLValue).asExpr(addressSort)
+                if (parameterType is EtsArrayType) {
+                    state.pathConstraints += state.memory.types.evalTypeEquals(ref, parameterType)
+                    return@forEachIndexed
+                }
+
                 val resolvedParameterType = graph.hierarchy.classesForType(parameterType)
 
                 if (resolvedParameterType.isEmpty()) {

From c17d54659dba1c315873b36d75b08a9635fd6e0b Mon Sep 17 00:00:00 2001
From: Alexey Menshutin <alex.menshutin99@gmail.com>
Date: Tue, 1 Jul 2025 12:31:09 +0300
Subject: [PATCH 40/69] Fix type streams

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt    | 3 ++-
 .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt  | 3 ++-
 2 files changed, 4 insertions(+), 2 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 ac5b6a1be..8664a5f08 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
@@ -899,7 +899,8 @@ class TsExprResolver(
             // this field should present in the object.
             // That's not true in the common case for TS, but that's the decision we made.
             val auxiliaryType = EtsAuxiliaryType(properties = setOf(field.name))
-            pathConstraints += memory.types.evalIsSubtype(resolvedAddr, auxiliaryType)
+            // assert is required to update models
+            scope.assert(memory.types.evalIsSubtype(resolvedAddr, auxiliaryType))
         }
 
         // TODO
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 eaa73fe86..856c127c5 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
@@ -560,7 +560,8 @@ class TsInterpreter(
                         // If we access some field, we expect that the object must have this field.
                         // It is not always true for TS, but we decided to process it so.
                         val supertype = EtsAuxiliaryType(properties = setOf(lhv.field.name))
-                        pathConstraints += memory.types.evalIsSubtype(instance, supertype)
+                        // assert is required to update models
+                        scope.assert(memory.types.evalIsSubtype(instance, supertype))
                     }
 
                     // If there is no such field, we create a fake field for the expr

From 3ab240ec596c5200a043e6c45b40b7270ad2deca Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 14:24:14 +0300
Subject: [PATCH 41/69] Remove forking warning

---
 usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt | 2 --
 1 file changed, 2 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 8664a5f08..7ad2c6c15 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
@@ -693,8 +693,6 @@ class TsExprResolver(
                         ctx.mkTrue() to { state: TsState -> state.newStmt(it) }
                     } // TODO error with true Expr
 
-                    logger.warn { "Forking on ${blocks.size} branches" }
-
                     scope.forkMulti(blocks)
 
                     return null

From 0dd77963f78d7fc1e8bec32fb200b38f0df24c3b Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 14:25:19 +0300
Subject: [PATCH 42/69] Warn only when necessary

---
 usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
index 55278b1b6..213a58b50 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt
@@ -49,7 +49,9 @@ class EtsHierarchy(private val scene: EtsScene) {
             }
         }
 
-        logger.warn { "Ancestors map is built in $time ms" }
+        if (time > 100) {
+            logger.warn { "Ancestors map is built in $time ms" }
+        }
 
         return@lazy result
     }

From 258a0d8ba962aced0ef60f1f1c34760946c4b027 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 14:58:59 +0300
Subject: [PATCH 43/69] Refine operators

---
 .../usvm/machine/operator/TsBinaryOperator.kt | 201 ++++--------------
 1 file changed, 47 insertions(+), 154 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
index 2a1094918..f5c8be782 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
@@ -595,6 +595,7 @@ sealed interface TsBinaryOperator {
                             rhsValue = rhs.extractBool(scope)
                             rhsType.boolTypeExpr
                         }
+
                         fp64Sort -> {
                             rhsValue = rhs.extractFp(scope)
                             rhsType.fpTypeExpr
@@ -629,7 +630,7 @@ sealed interface TsBinaryOperator {
             // Strict equality checks that both sides are of the same type,
             // therefore they have to be processed in the other methods.
             // Otherwise, they would have the same sorts.
-            return lhs.ctx.mkFalse()
+            return mkFalse()
         }
     }
 
@@ -974,52 +975,39 @@ sealed interface TsBinaryOperator {
         }
     }
 
-    data object Sub : TsBinaryOperator {
-        override fun TsContext.onBool(
-            lhs: UBoolExpr,
-            rhs: UBoolExpr,
-            scope: TsStepScope,
-        ): UExpr<*> {
-            return mkFpSubExpr(fpRoundingModeSortDefaultValue(), boolToFp(lhs), boolToFp(rhs))
-        }
-
-        override fun TsContext.onFp(
+    data object Sub : TsArithmeticOperator {
+        override fun TsContext.apply(
             lhs: UExpr<KFp64Sort>,
             rhs: UExpr<KFp64Sort>,
-            scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             return mkFpSubExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
         }
+    }
 
-        override fun TsContext.onRef(
-            lhs: UHeapRef,
-            rhs: UHeapRef,
-            scope: TsStepScope,
-        ): UExpr<*> {
-            return internalResolve(lhs, rhs, scope)
+    data object Mul : TsArithmeticOperator {
+        override fun TsContext.apply(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+        ): UExpr<KFp64Sort> {
+            return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
         }
+    }
 
-        override fun TsContext.resolveFakeObject(
-            lhs: UExpr<*>,
-            rhs: UExpr<*>,
-            scope: TsStepScope,
-        ): UExpr<*> {
-            return internalResolve(lhs, rhs, scope)
+    data object Div : TsArithmeticOperator {
+        override fun TsContext.apply(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+        ): UExpr<KFp64Sort> {
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
         }
+    }
 
-        override fun TsContext.internalResolve(
-            lhs: UExpr<*>,
-            rhs: UExpr<*>,
-            scope: TsStepScope,
-        ): UExpr<*> {
-            val lhsNumeric = mkNumericExpr(lhs, scope)
-            val rhsNumeric = mkNumericExpr(rhs, scope)
-
-            return mkFpSubExpr(
-                fpRoundingModeSortDefaultValue(),
-                lhsNumeric,
-                rhsNumeric
-            )
+    data object Rem : TsArithmeticOperator {
+        override fun TsContext.apply(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+        ): UExpr<KFp64Sort> {
+            return mkFpRemExpr(lhs, rhs)
         }
     }
 
@@ -1107,10 +1095,8 @@ sealed interface TsBinaryOperator {
         ): UExpr<*> {
             check(lhs.isFakeObject() || rhs.isFakeObject())
 
-            return scope.calcOnState {
-                val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
-                iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
-            }
+            val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
+            return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
         }
 
         override fun TsContext.internalResolve(
@@ -1121,9 +1107,7 @@ sealed interface TsBinaryOperator {
             check(!lhs.isFakeObject() && !rhs.isFakeObject())
 
             val lhsTruthyExpr = mkTruthyExpr(lhs, scope)
-            return scope.calcOnState {
-                iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
-            }
+            return iteWriteIntoFakeObject(scope, lhsTruthyExpr, lhs, rhs)
         }
     }
 
@@ -1132,7 +1116,7 @@ sealed interface TsBinaryOperator {
             lhs: UBoolExpr,
             rhs: UBoolExpr,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             return mkAnd(lhs.not(), rhs)
         }
 
@@ -1140,7 +1124,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<KFp64Sort>,
             rhs: UExpr<KFp64Sort>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             return mkFpLessExpr(lhs, rhs)
         }
 
@@ -1148,7 +1132,7 @@ sealed interface TsBinaryOperator {
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             TODO("Not yet implemented")
         }
 
@@ -1156,7 +1140,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             TODO("Not yet implemented")
         }
 
@@ -1164,7 +1148,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             TODO("Not yet implemented")
         }
     }
@@ -1174,7 +1158,7 @@ sealed interface TsBinaryOperator {
             lhs: UBoolExpr,
             rhs: UBoolExpr,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             return mkAnd(lhs, rhs.not())
         }
 
@@ -1182,7 +1166,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<KFp64Sort>,
             rhs: UExpr<KFp64Sort>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             return mkFpGreaterExpr(lhs, rhs)
         }
 
@@ -1190,7 +1174,7 @@ sealed interface TsBinaryOperator {
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             TODO("Not yet implemented")
         }
 
@@ -1198,7 +1182,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             TODO("Not yet implemented")
         }
 
@@ -1206,64 +1190,17 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UBoolExpr {
             TODO("Not yet implemented")
         }
     }
 
-    data object Mul : TsBinaryOperator {
-        override fun TsContext.onBool(
-            lhs: UBoolExpr,
-            rhs: UBoolExpr,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            val left = mkNumericExpr(lhs, scope)
-            val right = mkNumericExpr(rhs, scope)
-            return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
-        }
-
-        override fun TsContext.onFp(
+    sealed interface TsArithmeticOperator : TsBinaryOperator {
+        fun TsContext.apply(
             lhs: UExpr<KFp64Sort>,
             rhs: UExpr<KFp64Sort>,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
-        }
-
-        override fun TsContext.onRef(
-            lhs: UHeapRef,
-            rhs: UHeapRef,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            val left = mkNumericExpr(lhs, scope)
-            val right = mkNumericExpr(rhs, scope)
-            return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
-        }
+        ): UExpr<KFp64Sort>
 
-        override fun TsContext.resolveFakeObject(
-            lhs: UExpr<*>,
-            rhs: UExpr<*>,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            check(lhs.isFakeObject() || rhs.isFakeObject())
-            val left = mkNumericExpr(lhs, scope)
-            val right = mkNumericExpr(rhs, scope)
-            return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
-        }
-
-        override fun TsContext.internalResolve(
-            lhs: UExpr<*>,
-            rhs: UExpr<*>,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            check(!lhs.isFakeObject() && !rhs.isFakeObject())
-            val left = mkNumericExpr(lhs, scope)
-            val right = mkNumericExpr(rhs, scope)
-            return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
-        }
-    }
-
-    data object Div : TsBinaryOperator {
         override fun TsContext.onBool(
             lhs: UBoolExpr,
             rhs: UBoolExpr,
@@ -1271,7 +1208,7 @@ sealed interface TsBinaryOperator {
         ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
-            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+            return apply(left, right)
         }
 
         override fun TsContext.onFp(
@@ -1279,7 +1216,7 @@ sealed interface TsBinaryOperator {
             rhs: UExpr<KFp64Sort>,
             scope: TsStepScope,
         ): UExpr<KFp64Sort> {
-            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
+            return apply(lhs, rhs)
         }
 
         override fun TsContext.onRef(
@@ -1289,7 +1226,7 @@ sealed interface TsBinaryOperator {
         ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
-            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+            return apply(left, right)
         }
 
         override fun TsContext.resolveFakeObject(
@@ -1299,7 +1236,7 @@ sealed interface TsBinaryOperator {
         ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
-            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+            return apply(left, right)
         }
 
         override fun TsContext.internalResolve(
@@ -1309,51 +1246,7 @@ sealed interface TsBinaryOperator {
         ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
-            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
-        }
-    }
-
-    data object Rem : TsBinaryOperator {
-        override fun TsContext.onBool(
-            lhs: UBoolExpr,
-            rhs: UBoolExpr,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            return internalResolve(lhs, rhs, scope)
-        }
-
-        override fun TsContext.onFp(
-            lhs: UExpr<KFp64Sort>,
-            rhs: UExpr<KFp64Sort>,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            return internalResolve(lhs, rhs, scope)
-        }
-
-        override fun TsContext.onRef(
-            lhs: UHeapRef,
-            rhs: UHeapRef,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            return internalResolve(lhs, rhs, scope)
-        }
-
-        override fun TsContext.resolveFakeObject(
-            lhs: UExpr<*>,
-            rhs: UExpr<*>,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            return internalResolve(lhs, rhs, scope)
-        }
-
-        override fun TsContext.internalResolve(
-            lhs: UExpr<*>,
-            rhs: UExpr<*>,
-            scope: TsStepScope,
-        ): UExpr<KFp64Sort> {
-            val lhsExpr = mkNumericExpr(lhs, scope)
-            val rhsExpr = mkNumericExpr(rhs, scope)
-            return mkFpRemExpr(lhsExpr, rhsExpr)
+            return apply(left, right)
         }
     }
 }

From 1b92d9cb954b3d9bc9c776ccedbaf808cc5f63b2 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 15:05:52 +0300
Subject: [PATCH 44/69] Mark flaky test as repeated

---
 usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
index cbcbae38a..93ab7021d 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
@@ -1,6 +1,7 @@
 package org.usvm.samples.types
 
 import org.jacodb.ets.model.EtsScene
+import org.junit.jupiter.api.RepeatedTest
 import org.junit.jupiter.api.Test
 import org.usvm.api.TsTestValue
 import org.usvm.util.TsMethodTestRunner
@@ -30,7 +31,7 @@ class TypeStream : TsMethodTestRunner() {
         )
     }
 
-    @Test
+    @RepeatedTest(10, failureThreshold = 1)
     fun `use unique field`() {
         val method = getMethod(className, "useUniqueField")
         discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
@@ -51,4 +52,4 @@ class TypeStream : TsMethodTestRunner() {
             { value, r -> value.name == "SecondChild" && r.number == 3.0 },
         )
     }
-}
\ No newline at end of file
+}

From 61d633ce5e67849d098ce7966c32f9c9188284f2 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 15:47:15 +0300
Subject: [PATCH 45/69] Make `withMode` generic extension

---
 .../kotlin/org/usvm/util/TsTestResolver.kt    | 30 +++++++++----------
 1 file changed, 15 insertions(+), 15 deletions(-)

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 d7b607500..0f3d7e17a 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -82,8 +82,8 @@ class TsTestResolver {
             }
         }
 
-        val before = beforeMemoryScope.withMode(ResolveMode.MODEL) { (this as MemoryScope).resolveState() }
-        val after = afterMemoryScope.withMode(ResolveMode.CURRENT) { (this as MemoryScope).resolveState() }
+        val before = beforeMemoryScope.withMode(ResolveMode.MODEL) { resolveState() }
+        val after = afterMemoryScope.withMode(ResolveMode.CURRENT) { resolveState() }
 
         return TsTest(method, before, after, result, trace = emptyList())
     }
@@ -490,19 +490,6 @@ open class TsTestStateResolver(
 
     internal var resolveMode: ResolveMode = ResolveMode.ERROR
 
-    internal inline fun <R> withMode(
-        resolveMode: ResolveMode,
-        body: TsTestStateResolver.() -> R,
-    ): R {
-        val prevValue = this.resolveMode
-        try {
-            this.resolveMode = resolveMode
-            return body()
-        } finally {
-            this.resolveMode = prevValue
-        }
-    }
-
     fun <T : USort> evaluateInModel(expr: UExpr<T>): UExpr<T> {
         return model.eval(expr)
     }
@@ -518,3 +505,16 @@ open class TsTestStateResolver(
 enum class ResolveMode {
     MODEL, CURRENT, ERROR
 }
+
+internal inline fun <S : TsTestStateResolver, R> S.withMode(
+    resolveMode: ResolveMode,
+    body: S.() -> R,
+): R {
+    val prevValue = this.resolveMode
+    try {
+        this.resolveMode = resolveMode
+        return body()
+    } finally {
+        this.resolveMode = prevValue
+    }
+}

From 55f0a2f29a5ca95621e04b85188841f5e8e92438 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 15:55:52 +0300
Subject: [PATCH 46/69] Remove empty lines

---
 usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 2 --
 1 file changed, 2 deletions(-)

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 0f3d7e17a..b3aaafef1 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -136,9 +136,7 @@ class TsTestResolver {
         fun resolveState(): TsParametersState {
             val thisInstance = resolveThisInstance()
             val parameters = resolveParameters()
-
             val globals = resolveGlobals()
-
             return TsParametersState(thisInstance, parameters, globals)
         }
     }

From d2e972bbaaa991fbda405cabe8e27567c3eb9741 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 16:48:00 +0300
Subject: [PATCH 47/69] Assert instance inside fake object is not null. Make
 tests more lenient

---
 .../org/usvm/machine/expr/TsExprResolver.kt   |  5 ++
 .../org/usvm/samples/arrays/InputArrays.kt    |  6 ++-
 .../org/usvm/samples/types/TypeStream.kt      | 49 ++++++++++++++-----
 .../org/usvm/util/TsMethodTestRunner.kt       |  3 +-
 .../resources/samples/types/TypeStream.ts     | 36 +++++++-------
 5 files changed, 67 insertions(+), 32 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 7ad2c6c15..68e5b3e20 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
@@ -957,6 +957,11 @@ class TsExprResolver(
     override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
         val instanceRef = resolve(value.instance)?.asExpr(addressSort) ?: return null
 
+        if (instanceRef.isFakeObject()) {
+            val ref = instanceRef.extractRef(scope)
+            checkUndefinedOrNullPropertyRead(ref) ?: return null
+        }
+
         checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
 
         // TODO It is a hack for array's length
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
index 907d8df94..e70dc93f3 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
@@ -18,11 +18,13 @@ class InputArrays : TsMethodTestRunner() {
             { x, r -> r is TsTestValue.TsException },
             { x, r ->
                 r as TsTestValue.TsNumber
-                (x.values[0] as TsTestValue.TsNumber).number == 1.0 && r.number == 1.0
+                val x0 = x.values[0] as TsTestValue.TsNumber
+                x0.number == 1.0 && r.number == 1.0
             },
             { x, r ->
                 r as TsTestValue.TsNumber
-                (x.values[0] as TsTestValue.TsNumber).number != 1.0 && r.number == 2.0
+                val x0 = x.values[0] as TsTestValue.TsNumber
+                x0.number != 1.0 && r.number == 2.0
             },
             invariants = arrayOf(
                 { _, r ->
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
index 93ab7021d..5d87ce6a4 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
@@ -16,7 +16,7 @@ class TypeStream : TsMethodTestRunner() {
         val method = getMethod(className, "ancestorId")
         discoverProperties<TsTestValue.TsClass, TsTestValue.TsClass>(
             method = method,
-            { value, r -> r.name == value.name },
+            { x, r -> r.name == x.name }
         )
     }
 
@@ -25,31 +25,58 @@ class TypeStream : TsMethodTestRunner() {
         val method = getMethod(className, "virtualInvokeForAncestor")
         discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
             method = method,
-            { value, r -> value.name == "Parent" && r.number == 1.0 },
-            { value, r -> value.name == "FirstChild" && r.number == 2.0 },
-            { value, r -> value.name == "SecondChild" && r.number == 3.0 },
+            { x, r -> x.name == "Parent" && r.number == 1.0 },
+            { x, r -> x.name == "FirstChild" && r.number == 2.0 },
+            { x, r -> x.name == "SecondChild" && r.number == 3.0 },
+            invariants = arrayOf(
+                { _, r -> r.number in listOf(1.0, 2.0, 3.0) }
+            )
         )
     }
 
     @RepeatedTest(10, failureThreshold = 1)
     fun `use unique field`() {
         val method = getMethod(className, "useUniqueField")
-        discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
+        discoverProperties<TsTestValue, TsTestValue>(
             method = method,
+            { x, r ->
+                x as TsTestValue.TsClass
+                r as TsTestValue.TsNumber
+                x.name == "FirstChild" && r.number == 1.0
+            },
             invariants = arrayOf(
-                { value, r -> value.name == "FirstChild" && r.number == 1.0 }
+                { _, r ->
+                    r !is TsTestValue.TsNumber || r.number == 1.0
+                }
             )
         )
     }
 
-    @Test
+    @RepeatedTest(10, failureThreshold = 1)
     fun `use non unique field`() {
         val method = getMethod(className, "useNonUniqueField")
-        discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
+        discoverProperties<TsTestValue, TsTestValue>(
             method = method,
-            { value, r -> value.name == "Parent" && r.number == 1.0 },
-            { value, r -> value.name == "FirstChild" && r.number == 2.0 },
-            { value, r -> value.name == "SecondChild" && r.number == 3.0 },
+            { x, r ->
+                x as TsTestValue.TsClass
+                r as TsTestValue.TsNumber
+                x.name == "Parent" && r.number == 1.0
+            },
+            { x, r ->
+                x as TsTestValue.TsClass
+                r as TsTestValue.TsNumber
+                x.name == "FirstChild" && r.number == 2.0
+            },
+            { x, r ->
+                x as TsTestValue.TsClass
+                r as TsTestValue.TsNumber
+                x.name == "SecondChild" && r.number == 3.0
+            },
+            invariants = arrayOf(
+                { _, r ->
+                    r !is TsTestValue.TsNumber || r.number in listOf(1.0, 2.0, 3.0)
+                }
+            )
         )
     }
 }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
index 1dcc2921b..ce5198b8f 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -329,10 +329,11 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
         val tsMachineOptions = TsOptions()
         TsMachine(scene, options, tsMachineOptions).use { machine ->
             val states = machine.analyze(listOf(method))
-            states.map { state ->
+            val resolved = states.map { state ->
                 val resolver = TsTestResolver()
                 resolver.resolve(method, state)
             }
+            resolved
         }
     }
 
diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts
index ea2c6e5e6..dcbf7fa7c 100644
--- a/usvm-ts/src/test/resources/samples/types/TypeStream.ts
+++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts
@@ -3,17 +3,17 @@
 
 class TypeStream {
     ancestorId(ancestor: Parent): Parent {
-        return ancestor
+        return ancestor;
     }
 
     virtualInvokeForAncestor(ancestor: Parent): number {
-        const number = ancestor.virtualMethod();
-        if (number == 100) {
-            return 1
-        } else if (number == 200) {
-            return 2
+        const virtualInvokeResult = ancestor.virtualMethod();
+        if (virtualInvokeResult == 100) {
+            return 1;
+        } else if (virtualInvokeResult == 200) {
+            return 2;
         } else {
-            return 3
+            return 3;
         }
     }
 
@@ -21,12 +21,12 @@ class TypeStream {
         // noinspection JSUnusedLocalSymbols
         const _ = value.firstChildField;
         const virtualInvokeResult = value.virtualMethod();
-        if (virtualInvokeResult == 100) {
-            return -1 // unreachable
-        } else if (virtualInvokeResult == 200) {
-            return 1
+        if (virtualInvokeResult == 200) {
+            return 1;
+        } else if (virtualInvokeResult == 100) {
+            return -1; // unreachable
         } else {
-            return -2 // unreachable
+            return -1; // unreachable
         }
     }
 
@@ -35,17 +35,17 @@ class TypeStream {
         const _ = value.parentField;
         const virtualInvokeResult = value.virtualMethod();
         if (virtualInvokeResult == 100) {
-            return 1
+            return 1;
         } else if (virtualInvokeResult == 200) {
-            return 2
+            return 2;
         } else {
-            return 3
+            return 3;
         }
     }
 }
 
 class Parent {
-    parentField: number = -10
+    parentField: number = -10;
 
     virtualMethod(): number {
         return 100;
@@ -53,7 +53,7 @@ class Parent {
 }
 
 class FirstChild extends Parent {
-    firstChildField: number = 10
+    firstChildField: number = 10;
 
     override virtualMethod(): number {
         return 200;
@@ -61,7 +61,7 @@ class FirstChild extends Parent {
 }
 
 class SecondChild extends Parent {
-    secondChildField: number = 20
+    secondChildField: number = 20;
 
     override virtualMethod(): number {
         return 300;

From 0e4b1a4c6892238578ae0b275d29df8799ed62f5 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 16:49:24 +0300
Subject: [PATCH 48/69] Unify

---
 usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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 b3aaafef1..31d2cfdfa 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -355,8 +355,7 @@ open class TsTestStateResolver(
             model.eval(type.refTypeExpr).isTrue -> {
                 val lValue = getIntermediateRefLValue(expr.address)
                 val value = finalStateMemory.read(lValue)
-                val ref = model.eval(value)
-                resolveExpr(ref)
+                resolveExpr(model.eval(value))
             }
 
             else -> error("Unsupported")

From 34dd6a5e5d6cf04b1906ba457b4d6d1708411875 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 17:26:15 +0300
Subject: [PATCH 49/69] Fix type stream tests

---
 .../usvm/machine/interpreter/TsInterpreter.kt |  3 +-
 .../org/usvm/samples/types/TypeStream.kt      | 63 ++++++++++++++-----
 .../resources/samples/types/TypeStream.ts     | 38 ++++++-----
 3 files changed, 75 insertions(+), 29 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 856c127c5..6b1effda6 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
@@ -286,7 +286,8 @@ class TsInterpreter(
 
                 // TODO mistake, should be separated into several hierarchies
                 //      or evalTypeEqual with several concrete types
-                memory.types.evalIsSubtype(ref, type)
+                // memory.types.evalIsSubtype(ref, type)
+                memory.types.evalTypeEquals(ref, type)
             }
             constraint to block
         }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
index 5d87ce6a4..b63c97403 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/TypeStream.kt
@@ -12,24 +12,53 @@ class TypeStream : TsMethodTestRunner() {
     override val scene: EtsScene = loadSampleScene(className, folderPrefix = "types")
 
     @Test
-    fun `test an ancestor as argument`() {
-        val method = getMethod(className, "ancestorId")
-        discoverProperties<TsTestValue.TsClass, TsTestValue.TsClass>(
+    fun `test ancestor instanceof`() {
+        val method = getMethod(className, "instanceOf")
+        discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
             method = method,
-            { x, r -> r.name == x.name }
+            { x, r ->
+                x.name == "FirstChild" && r.number == 1.0
+            },
+            { x, r ->
+                x.name == "SecondChild" && r.number == 2.0
+            },
+            { x, r ->
+                x.name == "Parent" && r.number == 3.0
+            },
+            invariants = arrayOf(
+                { x, r ->
+                    x.name in listOf("Parent", "FirstChild", "SecondChild")
+                },
+                { _, r ->
+                    r.number in listOf(1.0, 2.0, 3.0)
+                },
+                { _, r -> r.number != -1.0 }
+            )
         )
     }
 
     @Test
     fun `test virtual invoke on an ancestor`() {
-        val method = getMethod(className, "virtualInvokeForAncestor")
+        val method = getMethod(className, "virtualInvokeOnAncestor")
         discoverProperties<TsTestValue.TsClass, TsTestValue.TsNumber>(
             method = method,
-            { x, r -> x.name == "Parent" && r.number == 1.0 },
-            { x, r -> x.name == "FirstChild" && r.number == 2.0 },
-            { x, r -> x.name == "SecondChild" && r.number == 3.0 },
+            { x, r ->
+                x.name == "FirstChild" && r.number == 1.0
+            },
+            { x, r ->
+                x.name == "SecondChild" && r.number == 2.0
+            },
+            { x, r ->
+                x.name == "Parent" && r.number == 3.0
+            },
             invariants = arrayOf(
-                { _, r -> r.number in listOf(1.0, 2.0, 3.0) }
+                { x, r ->
+                    x.name in listOf("Parent", "FirstChild", "SecondChild")
+                },
+                { _, r ->
+                    r.number in listOf(1.0, 2.0, 3.0)
+                },
+                { _, r -> r.number != -1.0 }
             )
         )
     }
@@ -45,9 +74,12 @@ class TypeStream : TsMethodTestRunner() {
                 x.name == "FirstChild" && r.number == 1.0
             },
             invariants = arrayOf(
+                { x, _ ->
+                    x !is TsTestValue.TsClass || x.name == "FirstChild"
+                },
                 { _, r ->
                     r !is TsTestValue.TsNumber || r.number == 1.0
-                }
+                },
             )
         )
     }
@@ -60,22 +92,25 @@ class TypeStream : TsMethodTestRunner() {
             { x, r ->
                 x as TsTestValue.TsClass
                 r as TsTestValue.TsNumber
-                x.name == "Parent" && r.number == 1.0
+                x.name == "FirstChild" && r.number == 1.0
             },
             { x, r ->
                 x as TsTestValue.TsClass
                 r as TsTestValue.TsNumber
-                x.name == "FirstChild" && r.number == 2.0
+                x.name == "SecondChild" && r.number == 2.0
             },
             { x, r ->
                 x as TsTestValue.TsClass
                 r as TsTestValue.TsNumber
-                x.name == "SecondChild" && r.number == 3.0
+                x.name == "Parent" && r.number == 3.0
             },
             invariants = arrayOf(
                 { _, r ->
                     r !is TsTestValue.TsNumber || r.number in listOf(1.0, 2.0, 3.0)
-                }
+                },
+                { _, r ->
+                    r !is TsTestValue.TsNumber || r.number != -1.0
+                },
             )
         )
     }
diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts
index dcbf7fa7c..37e3d06a2 100644
--- a/usvm-ts/src/test/resources/samples/types/TypeStream.ts
+++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts
@@ -2,32 +2,41 @@
 // noinspection JSUnusedGlobalSymbols
 
 class TypeStream {
-    ancestorId(ancestor: Parent): Parent {
-        return ancestor;
+    instanceOf(ancestor: Parent): number {
+        if (ancestor instanceof FirstChild) {
+            return 1;
+        } else if (ancestor instanceof SecondChild) {
+            return 2;
+        } else if (ancestor instanceof Parent) {
+            return 3;
+        }
+        return -1; // unreachable
     }
 
-    virtualInvokeForAncestor(ancestor: Parent): number {
+    virtualInvokeOnAncestor(ancestor: Parent): number {
         const virtualInvokeResult = ancestor.virtualMethod();
         if (virtualInvokeResult == 100) {
             return 1;
         } else if (virtualInvokeResult == 200) {
             return 2;
-        } else {
+        } else if (virtualInvokeResult == 300) {
             return 3;
         }
+        return -1; // unreachable
     }
 
     useUniqueField(value: any): number {
         // noinspection JSUnusedLocalSymbols
         const _ = value.firstChildField;
         const virtualInvokeResult = value.virtualMethod();
-        if (virtualInvokeResult == 200) {
+        if (virtualInvokeResult == 100) {
             return 1;
-        } else if (virtualInvokeResult == 100) {
-            return -1; // unreachable
-        } else {
-            return -1; // unreachable
+        } else if (virtualInvokeResult == 200) {
+            return 2; // unreachable
+        } else if (virtualInvokeResult == 300) {
+            return 3; // unreachable
         }
+        return -1; // unreachable
     }
 
     useNonUniqueField(value: any): number {
@@ -38,17 +47,18 @@ class TypeStream {
             return 1;
         } else if (virtualInvokeResult == 200) {
             return 2;
-        } else {
+        } else if (virtualInvokeResult == 300) {
             return 3;
         }
+        return -1; // unreachable
     }
 }
 
 class Parent {
-    parentField: number = -10;
+    parentField: number = 42;
 
     virtualMethod(): number {
-        return 100;
+        return 300;
     }
 }
 
@@ -56,7 +66,7 @@ class FirstChild extends Parent {
     firstChildField: number = 10;
 
     override virtualMethod(): number {
-        return 200;
+        return 100;
     }
 }
 
@@ -64,6 +74,6 @@ class SecondChild extends Parent {
     secondChildField: number = 20;
 
     override virtualMethod(): number {
-        return 300;
+        return 200;
     }
 }

From f59eb5580c4abcefc2b733a9917d9634db568091 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 17:49:19 +0300
Subject: [PATCH 50/69] Use isSubtype+isSupertype

---
 .../org/usvm/machine/interpreter/TsInterpreter.kt | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 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 6b1effda6..dfbd668ee 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
@@ -216,7 +216,6 @@ class TsInterpreter(
             concreteMethods += methods
         }
 
-
         val possibleTypes = scope.calcOnState { models.first().typeStreamOf(resolvedInstance as UConcreteHeapRef) }
             .take(1000)
 
@@ -234,13 +233,13 @@ class TsInterpreter(
         }
 
         //
-        val chosenMethods = intersectedTypes.flatMap {
-            graph.hierarchy.classesForType(it as EtsRefType)
+        val chosenMethods = intersectedTypes.flatMap { clazz ->
+            graph.hierarchy.classesForType(clazz as EtsRefType)
                 .asSequence()
                 // TODO wrong order, ancestors are unordered
                 .map { graph.hierarchy.getAncestors(it) }
                 .map { it.first { it.methods.any { it.name == stmt.callee.name } } }
-                .map { it.methods.first { it.name == stmt.callee.name } }
+                .map { clazz to it.methods.first { it.name == stmt.callee.name } }
         }.toList().take(10) // TODO check it
 
         // logger.info {
@@ -249,7 +248,7 @@ class TsInterpreter(
         // }"
         // }
 
-        val conditionsWithBlocks = chosenMethods.mapIndexed { i, method ->
+        val conditionsWithBlocks = chosenMethods.mapIndexed { i, (clazz, method) ->
             val concreteCall = stmt.toConcrete(method)
             val block = { state: TsState -> state.newStmt(concreteCall) }
             val type = requireNotNull(method.enclosingClass).type
@@ -286,8 +285,10 @@ class TsInterpreter(
 
                 // TODO mistake, should be separated into several hierarchies
                 //      or evalTypeEqual with several concrete types
-                // memory.types.evalIsSubtype(ref, type)
-                memory.types.evalTypeEquals(ref, type)
+                mkAnd(
+                    memory.types.evalIsSubtype(ref, clazz),
+                    memory.types.evalIsSupertype(ref, type)
+                )
             }
             constraint to block
         }

From 61ad56023572a2109b3823180660ac136dd2619d Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 18:17:57 +0300
Subject: [PATCH 51/69] Fix test with super

---
 usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt | 1 -
 usvm-ts/src/test/resources/samples/Call.ts       | 4 ++++
 2 files changed, 4 insertions(+), 1 deletion(-)

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 2f69267f2..10c237030 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -200,7 +200,6 @@ class Call : TsMethodTestRunner() {
         )
     }
 
-    @Disabled("Calls to super are broken in IR")
     @Test
     fun `test virtual child`() {
         val method = getMethod(className, "callVirtualChild")
diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts
index 243387976..ae58e985b 100644
--- a/usvm-ts/src/test/resources/samples/Call.ts
+++ b/usvm-ts/src/test/resources/samples/Call.ts
@@ -198,6 +198,10 @@ class Parent {
 }
 
 class Child extends Parent {
+    constructor() {
+        // super();
+    }
+
     override virtualMethod(): number {
         return 200;
     }

From 0014070984421ef7fb336a64484955d1715e4c05 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Tue, 1 Jul 2025 18:19:22 +0300
Subject: [PATCH 52/69] Add test with non-overridden virtual call

---
 .../org/usvm/machine/interpreter/TsInterpreter.kt  | 14 ++++++++------
 usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt   | 10 ++++++++++
 usvm-ts/src/test/resources/samples/Call.ts         |  9 +++++++++
 3 files changed, 27 insertions(+), 6 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 dfbd668ee..b5f806eae 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
@@ -191,12 +191,14 @@ class TsInterpreter(
                     return
                 }
                 val cls = classes.single()
-                val method = cls.methods
-                    .singleOrNull { it.name == stmt.callee.name }
-                    ?: run {
-                        TODO("Overloads are not supported yet")
-                    }
-                concreteMethods += method
+                // val method = cls.methods
+                //     .singleOrNull { it.name == stmt.callee.name }
+                //     ?: run {
+                //         TODO("Overloads are not supported yet")
+                //     }
+                // concreteMethods += method
+                val suitableMethods = cls.methods.filter { it.name == stmt.callee.name }
+                concreteMethods += suitableMethods
             } else {
                 logger.warn {
                     "Could not resolve method: ${stmt.callee} on type: $type"
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 10c237030..4a0854c08 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -209,6 +209,16 @@ class Call : TsMethodTestRunner() {
         )
     }
 
+    @Disabled("Non-overridden virtual calls are not supported yet")
+    @Test
+    fun `test base call`() {
+        val method = getMethod(className, "callBaseMethod")
+        discoverProperties<TsTestValue.TsNumber>(
+            method = method,
+            { r -> r.number == 42.0 },
+        )
+    }
+
     @Test
     fun `test virtual dispatch`() {
         val method = getMethod(className, "virtualDispatch")
diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts
index ae58e985b..3341a30e5 100644
--- a/usvm-ts/src/test/resources/samples/Call.ts
+++ b/usvm-ts/src/test/resources/samples/Call.ts
@@ -118,6 +118,11 @@ class Call {
         return obj.virtualMethod(); // 200
     }
 
+    callBaseMethod(): number {
+        let obj: Child = new Child();
+        return obj.baseMethod(); // 42
+    }
+
     virtualDispatch(obj: Parent): number {
         if (obj instanceof Child) {
             return obj.virtualMethod(); // 200
@@ -195,6 +200,10 @@ class Parent {
     virtualMethod(): number {
         return 100;
     }
+
+    baseMethod(): number {
+        return 42;
+    }
 }
 
 class Child extends Parent {

From f6fe2da80dce57cb9a15a4ee860642150cabc584 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 01:02:53 +0300
Subject: [PATCH 53/69] Show stop reason

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

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index 9e3a8d0ec..d2fd85dec 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -125,7 +125,7 @@ class TsMachine(
                 val result = strategy.shouldStop()
 
                 if (result) {
-                    logger.warn { "Stop strategy finished execution $strategy" }
+                    logger.warn { "Stop strategy finished execution: ${strategy.stopReason()}" }
                 }
 
                 return result

From 98964a9e7c872511ce7a6acd15ab4b4fdc2329b5 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 01:02:59 +0300
Subject: [PATCH 54/69] Format

---
 .../src/main/kotlin/org/usvm/machine/TsContext.kt    |  8 ++++----
 .../src/main/kotlin/org/usvm/machine/TsMachine.kt    | 12 ++++--------
 usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt | 11 +++++++++--
 3 files changed, 17 insertions(+), 14 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 c9110f2ed..e1052fbde 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -78,6 +78,8 @@ class TsContext(
         is EtsAnyType -> unresolvedSort
         is EtsUnknownType -> unresolvedSort
         is EtsAliasType -> typeToSort(type.originalType)
+        is EtsEnumValueType -> unresolvedSort
+
         is EtsGenericType -> {
             if (type.constraint == null && type.defaultType == null) {
                 unresolvedSort
@@ -85,10 +87,8 @@ class TsContext(
                 TODO("Not yet implemented")
             }
         }
-        is EtsEnumValueType -> unresolvedSort
-        else -> {
-            TODO("${type::class.simpleName} is not yet supported: $type")
-        }
+
+        else -> TODO("${type::class.simpleName} is not yet supported: $type")
     }
 
     fun arrayDescriptorOf(type: EtsArrayType): EtsType {
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
index d2fd85dec..7d7002900 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt
@@ -111,14 +111,10 @@ class TsMachine(
             val strategy = createStopStrategy(
                 options,
                 targets,
-                timeStatisticsFactory =
-                    { timeStatistics },
-                stepsStatisticsFactory =
-                    { stepsStatistics },
-                coverageStatisticsFactory =
-                    { coverageStatistics },
-                getCollectedStatesCount =
-                    { statesCollector.collectedStates.size }
+                timeStatisticsFactory = { timeStatistics },
+                stepsStatisticsFactory = { stepsStatistics },
+                coverageStatisticsFactory = { coverageStatistics },
+                getCollectedStatesCount = { statesCollector.collectedStates.size },
             )
 
             override fun shouldStop(): Boolean {
diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
index e4f511b08..543cf6737 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
@@ -24,14 +24,19 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
 
         @JvmStatic
         private fun projectAvailable(): Boolean {
-            return getResourcePathOrNull(PROJECT_PATH) != null && getResourcePathOrNull(SDK_PATH) != null
+            val isProjectPresent = getResourcePathOrNull(PROJECT_PATH) != null
+            val isSdkPreset = getResourcePathOrNull(SDK_PATH) != null
+            return isProjectPresent && isSdkPreset
         }
     }
 
     override val scene: EtsScene = run {
         val projectPath = getResourcePath(PROJECT_PATH)
         val sdkPath = getResourcePathOrNull(SDK_PATH)
-            ?: error("Could not load SDK from resources '$SDK_PATH'. Try running './gradlew generateSdkIR' to generate it.")
+            ?: error(
+                "Could not load SDK from resources '$SDK_PATH'. " +
+                    "Try running './gradlew generateSdkIR' to generate it."
+            )
         loadEtsProjectFromIR(projectPath, sdkPath)
     }
 
@@ -84,6 +89,7 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
                     .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
                     .filterNot { it.name == "build" }
             }
+        
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
             val states = machine.analyze(methods)
@@ -96,6 +102,7 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
         val method = scene.projectClasses
             .flatMap { it.methods }
             .single { it.name == "createKvStore" && it.enclosingClass?.name == "KvStoreModel" }
+
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
             val states = machine.analyze(listOf(method))

From 0616f030a0288764ca3238a1a9fa149c57376271 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 01:12:04 +0300
Subject: [PATCH 55/69] Rename DemoPhotos

---
 .../usvm/project/{Photos.kt => DemoPhotos.kt} | 27 +++++++++++--------
 1 file changed, 16 insertions(+), 11 deletions(-)
 rename usvm-ts/src/test/kotlin/org/usvm/project/{Photos.kt => DemoPhotos.kt} (82%)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
similarity index 82%
rename from usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
rename to usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
index 41ae13d4f..69520e64c 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/Photos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
@@ -17,7 +17,7 @@ import kotlin.test.Test
 
 // @EnabledIf("projectAvailable")
 @Disabled
-class RunOnPhotosProject : TsMethodTestRunner() {
+class RunOnDemoPhotosProject : TsMethodTestRunner() {
 
     companion object {
         private const val PROJECT_PATH = "/projects/Demo_Photos/source/entry"
@@ -25,28 +25,32 @@ class RunOnPhotosProject : TsMethodTestRunner() {
 
         @JvmStatic
         private fun projectAvailable(): Boolean {
-            return getResourcePathOrNull(PROJECT_PATH) != null && getResourcePathOrNull(SDK_PATH) != null
+            val isProjectPresent = getResourcePathOrNull(PROJECT_PATH) != null
+            val isSdkPreset = getResourcePathOrNull(SDK_PATH) != null
+            return isProjectPresent && isSdkPreset
         }
     }
 
     override val scene: EtsScene = run {
         val projectPath = getResourcePath(PROJECT_PATH)
         val sdkPath = getResourcePathOrNull(SDK_PATH)
-            ?: error("Could not load SDK from resources '$SDK_PATH'. Try running './gradlew generateSdkIR' to generate it.")
+            ?: error(
+                "Could not load SDK from resources '$SDK_PATH'. " +
+                    "Try running './gradlew generateSdkIR' to generate it."
+            )
         loadEtsProjectAutoConvert(projectPath, sdkPath)
     }
 
     @Test
     fun `test run on each method`() {
         val exceptions = mutableListOf<Throwable>()
-        val classes = scene.projectClasses.filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) }
+        val classes = scene.projectClasses
+            .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) }
 
         println("Total classes: ${classes.size}")
 
-        classes
-            // .filter { it.name == "NewAlbumPage" }
-            .forEach { clazz ->
-            val methods = clazz.methods
+        classes.forEach { cls ->
+            val methods = cls.methods
                 .filterNot { it.cfg.stmts.isEmpty() }
                 .filterNot { it.isStatic }
                 .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
@@ -78,9 +82,9 @@ class RunOnPhotosProject : TsMethodTestRunner() {
     @Test
     fun `test run on all methods`() {
         val methods = scene.projectClasses
-            .filterNot { it.name.startsWith("%AC") }
-            .flatMap {
-                it.methods
+            .filterNot { it.name.startsWith(ANONYMOUS_CLASS_PREFIX) }
+            .flatMap { cls ->
+                cls.methods
                     .filterNot { it.cfg.stmts.isEmpty() }
                     .filterNot { it.isStatic }
                     .filterNot { it.name.startsWith("%AM") }
@@ -89,6 +93,7 @@ class RunOnPhotosProject : TsMethodTestRunner() {
                     .filterNot { it.name == STATIC_INIT_METHOD_NAME }
                     .filterNot { it.name == CONSTRUCTOR_NAME }
             }
+
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
             val states = machine.analyze(methods)

From 571386ddc4bc18da7494f41674c270e271f7c8ed Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 01:13:15 +0300
Subject: [PATCH 56/69] Cleanup

---
 usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
index 543cf6737..27a86eb39 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt
@@ -89,7 +89,7 @@ class RunOnDemoCalcProject : TsMethodTestRunner() {
                     .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
                     .filterNot { it.name == "build" }
             }
-        
+
         val tsOptions = TsOptions()
         TsMachine(scene, options, tsOptions).use { machine ->
             val states = machine.analyze(methods)

From 74b457c042b3aca8f909a030a90b03259d6ffcda Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 01:13:22 +0300
Subject: [PATCH 57/69] Use constant

---
 usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
index 69520e64c..5e06a6335 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
@@ -87,7 +87,7 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() {
                 cls.methods
                     .filterNot { it.cfg.stmts.isEmpty() }
                     .filterNot { it.isStatic }
-                    .filterNot { it.name.startsWith("%AM") }
+                    .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) }
                     .filterNot { it.name == "build" }
                     .filterNot { it.name == INSTANCE_INIT_METHOD_NAME }
                     .filterNot { it.name == STATIC_INIT_METHOD_NAME }

From 914dd4370c0d8a240f659405432ace26e15969d8 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:19:19 +0300
Subject: [PATCH 58/69] Use timeout 120s

---
 usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
index 5e06a6335..1c4bf3e3a 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
@@ -7,16 +7,17 @@ import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME
 import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME
 import org.jacodb.ets.utils.loadEtsProjectAutoConvert
-import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.condition.EnabledIf
 import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.TsMethodTestRunner
 import org.usvm.util.getResourcePath
 import org.usvm.util.getResourcePathOrNull
 import kotlin.test.Test
+import kotlin.time.Duration.Companion.seconds
 
-// @EnabledIf("projectAvailable")
-@Disabled
+@EnabledIf("projectAvailable")
+// @Disabled
 class RunOnDemoPhotosProject : TsMethodTestRunner() {
 
     companion object {
@@ -63,7 +64,7 @@ class RunOnDemoPhotosProject : TsMethodTestRunner() {
 
             runCatching {
                 val tsOptions = TsOptions()
-                TsMachine(scene, options, tsOptions).use { machine ->
+                TsMachine(scene, options.copy(timeout = 120.seconds), tsOptions).use { machine ->
                     val states = machine.analyze(methods)
                     states.let {}
                 }

From aa515cbeb3c7c37f31911b8e72c664bf1233b0b0 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:20:04 +0300
Subject: [PATCH 59/69] Add AnyType to top type stream, handle Any in
 isSupertype

---
 .../main/kotlin/org/usvm/machine/types/TsTypeSystem.kt    | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
index 41ff0541e..ee131ee94 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt
@@ -62,6 +62,8 @@ class TsTypeSystem(
         // "unknown" is the safe supertype: every value is assignable to unknown.
         if (unwrappedSupertype is EtsUnknownType) return true
 
+        // "any" is the universal subtype: any can be assigned to any type.
+        if (unwrappedType is EtsAnyType) return true
         // "never" is the universal subtype: never can be assigned to any type.
         if (unwrappedType is EtsNeverType) return true
 
@@ -75,12 +77,12 @@ class TsTypeSystem(
         // As supertype, null/undefined only accept their own or any/unknown.
         if (unwrappedSupertype is EtsNullType) {
             // null supertype rules
-            return unwrappedType is EtsAnyType || unwrappedType is EtsUnknownType
+            return unwrappedType is EtsUnknownType
         }
 
         if (unwrappedSupertype is EtsUndefinedType) {
             // undefined supertype rules
-            return unwrappedType is EtsAnyType || unwrappedType is EtsUnknownType
+            return unwrappedType is EtsUnknownType
         }
 
         // Primitive types
@@ -296,7 +298,7 @@ class TsTypeSystem(
             is EtsUnclearRefType,
             is EtsClassType ->
                 if ((t as? EtsClassType)?.signature == EtsHierarchy.OBJECT_CLASS.signature) { // TODO change it
-                    scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType
+                    scene.projectAndSdkClasses.asSequence().map { it.type } + EtsStringType + EtsAnyType
                 } else {
                     hierarchy.classesForType(t)
                         .asSequence()

From 52cfb932f122fd788f563b85c1fced15568ec466 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:32:27 +0300
Subject: [PATCH 60/69] Move dot utils

---
 .../kotlin/org/usvm/machine/state/TsState.kt  | 14 -------
 .../src/main/kotlin/org/usvm/util/Utils.kt    | 37 +++++++++++++++++++
 2 files changed, 37 insertions(+), 14 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 b4dc03e0c..a46d93c77 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
@@ -9,9 +9,6 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsStmt
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsValue
-import org.jacodb.ets.utils.InterproceduralCfg
-import org.jacodb.ets.utils.renderDotOverwrite
-import org.jacodb.ets.utils.toHighlightedDotWithCalls
 import org.usvm.PathNode
 import org.usvm.UCallStack
 import org.usvm.UConcreteHeapRef
@@ -24,7 +21,6 @@ import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHa
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.constraints.UPathConstraints
-import org.usvm.dataflow.ts.util.toMap
 import org.usvm.machine.TsContext
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemory
@@ -175,16 +171,6 @@ class TsState(
         )
     }
 
-    fun renderGraph() {
-        val graph = InterproceduralCfg(main = entrypoint.cfg, callees = discoveredCallees.toMap())
-        val dot = graph.toHighlightedDotWithCalls(
-            pathStmts = pathNode.allStatements.toSet(),
-            currentStmt = currentStatement
-        )
-
-        renderDotOverwrite(dot)
-    }
-
     override val isExceptional: Boolean
         get() = methodResult is TsMethodResult.TsException
 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt
index b05ba6d4c..1265d05b1 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt
@@ -9,16 +9,22 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsType
 import org.jacodb.ets.model.EtsUnclearRefType
+import org.jacodb.ets.utils.InterproceduralCfg
+import org.jacodb.ets.utils.toHighlightedDotWithCalls
 import org.usvm.UBoolSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.dataflow.ts.util.toMap
 import org.usvm.machine.TsContext
 import org.usvm.machine.expr.tctx
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
 import org.usvm.machine.types.mkFakeValue
+import java.nio.file.Path
+import kotlin.io.path.createTempDirectory
+import kotlin.io.path.writeText
 
 // Built-in KContext.bvToBool has identical implementation.
 fun TsContext.boolToFp(expr: UExpr<UBoolSort>): UExpr<KFp64Sort> =
@@ -75,3 +81,34 @@ fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHe
 
     return fakeObject
 }
+
+fun TsState.renderGraph() {
+    val graph = InterproceduralCfg(main = entrypoint.cfg, callees = discoveredCallees.toMap())
+    val dot = graph.toHighlightedDotWithCalls(
+        pathStmts = pathNode.allStatements.toSet(),
+        currentStmt = currentStatement,
+    )
+
+    myRenderDot(dot)
+}
+
+fun myRenderDot(
+    dot: String,
+    outDir: Path = createTempDirectory(),
+    baseName: String = "cfg",
+    dotCmd: String = "dot",
+    format: String = "svg", // "svg", "png", "pdf"
+    viewerCmd: String? = when {
+        System.getProperty("os.name").startsWith("Mac") -> "open"
+        System.getProperty("os.name").startsWith("Win") -> "cmd /c start"
+        else -> "xdg-open"
+    },
+) {
+    val dotFile = outDir.resolve("$baseName.dot")
+    val svgFile = outDir.resolveSibling("$baseName.$format")
+    dotFile.writeText(dot)
+    Runtime.getRuntime().exec("$dotCmd $dotFile -T$format -o $svgFile").waitFor()
+    if (viewerCmd != null) {
+        Runtime.getRuntime().exec("$viewerCmd $svgFile").waitFor()
+    }
+}

From 88539113df40b62b673e8aeffc83afd9ffea9916 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:32:32 +0300
Subject: [PATCH 61/69] Format

---
 .../kotlin/org/usvm/machine/interpreter/TsInterpreter.kt     | 5 +++--
 1 file changed, 3 insertions(+), 2 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 b5f806eae..078b4f1fa 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
@@ -218,8 +218,9 @@ class TsInterpreter(
             concreteMethods += methods
         }
 
-        val possibleTypes = scope.calcOnState { models.first().typeStreamOf(resolvedInstance as UConcreteHeapRef) }
-            .take(1000)
+        val possibleTypes = scope.calcOnState {
+            models.first().typeStreamOf(resolvedInstance as UConcreteHeapRef).take(1000)
+        }
 
         if (possibleTypes !is TypesResult.SuccessfulTypesResult) {
             error("TODO")// is it right?

From ce6b9574ce7cf89134a42448dcbef75364533593 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:32:50 +0300
Subject: [PATCH 62/69] Register callee for static initializer

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

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 68e5b3e20..76edc4992 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
@@ -1035,6 +1035,7 @@ class TsExprResolver(
                 scope.doWithState {
                     markInitialized(clazz)
                     pushSortsForArguments(instance = null, args = emptyList(), localToIdx)
+                    registerCallee(currentStatement, initializer.cfg)
                     callStack.push(initializer, currentStatement)
                     memory.stack.push(arrayOf(instanceRef), initializer.localsCount)
                     newStmt(initializer.cfg.stmts.first())

From fa44f6afedff9fbefca9f624899a4e09842f2419 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:33:06 +0300
Subject: [PATCH 63/69] Filter some warnings

---
 .../src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt   | 4 +++-
 1 file changed, 3 insertions(+), 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 76edc4992..78c0d37a5 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
@@ -879,7 +879,9 @@ class TsExprResolver(
 
         val sort = when (etsField) {
             is EtsPropertyResolution.Empty -> {
-                logger.error("Field $field not found, creating fake field")
+                if (field.name !in listOf("i", "LogLevel")) {
+                    logger.warn { "Field $field not found, creating fake field" }
+                }
                 // If we didn't find any real fields, let's create a fake one.
                 // It is possible due to mistakes in the IR or if the field was added explicitly
                 // in the code.

From a8760bfb56f0a342f45756f03486e9c691988e0e Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:34:10 +0300
Subject: [PATCH 64/69] Move TsState visualization utils

---
 .../kotlin/org/usvm/util/TsStateVisualizer.kt | 39 ++++++++++++++++++-
 .../src/main/kotlin/org/usvm/util/Utils.kt    | 31 ---------------
 2 files changed, 38 insertions(+), 32 deletions(-)

diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt
index e99f5d745..c7c10485e 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsStateVisualizer.kt
@@ -1,11 +1,48 @@
 package org.usvm.util
 
+import org.jacodb.ets.utils.InterproceduralCfg
+import org.jacodb.ets.utils.toHighlightedDotWithCalls
+import org.usvm.dataflow.ts.util.toMap
 import org.usvm.machine.TsInterpreterObserver
 import org.usvm.machine.state.TsState
 import org.usvm.statistics.UMachineObserver
+import java.nio.file.Path
+import kotlin.io.path.createTempDirectory
+import kotlin.io.path.writeText
 
 class TsStateVisualizer : TsInterpreterObserver, UMachineObserver<TsState> {
     override fun onStatePeeked(state: TsState) {
         state.renderGraph()
     }
-}
\ No newline at end of file
+}
+
+fun TsState.renderGraph() {
+    val graph = InterproceduralCfg(main = entrypoint.cfg, callees = discoveredCallees.toMap())
+    val dot = graph.toHighlightedDotWithCalls(
+        pathStmts = pathNode.allStatements.toSet(),
+        currentStmt = currentStatement,
+    )
+
+    myRenderDot(dot)
+}
+
+fun myRenderDot(
+    dot: String,
+    outDir: Path = createTempDirectory(),
+    baseName: String = "cfg",
+    dotCmd: String = "dot",
+    format: String = "svg", // "svg", "png", "pdf"
+    viewerCmd: String? = when {
+        System.getProperty("os.name").startsWith("Mac") -> "open"
+        System.getProperty("os.name").startsWith("Win") -> "cmd /c start"
+        else -> "xdg-open"
+    },
+) {
+    val dotFile = outDir.resolve("$baseName.dot")
+    val svgFile = outDir.resolveSibling("$baseName.$format")
+    dotFile.writeText(dot)
+    Runtime.getRuntime().exec("$dotCmd $dotFile -T$format -o $svgFile").waitFor()
+    if (viewerCmd != null) {
+        Runtime.getRuntime().exec("$viewerCmd $svgFile").waitFor()
+    }
+}
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt
index 1265d05b1..aec008bf2 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/Utils.kt
@@ -81,34 +81,3 @@ fun UHeapRef.createFakeField(fieldName: String, scope: TsStepScope): UConcreteHe
 
     return fakeObject
 }
-
-fun TsState.renderGraph() {
-    val graph = InterproceduralCfg(main = entrypoint.cfg, callees = discoveredCallees.toMap())
-    val dot = graph.toHighlightedDotWithCalls(
-        pathStmts = pathNode.allStatements.toSet(),
-        currentStmt = currentStatement,
-    )
-
-    myRenderDot(dot)
-}
-
-fun myRenderDot(
-    dot: String,
-    outDir: Path = createTempDirectory(),
-    baseName: String = "cfg",
-    dotCmd: String = "dot",
-    format: String = "svg", // "svg", "png", "pdf"
-    viewerCmd: String? = when {
-        System.getProperty("os.name").startsWith("Mac") -> "open"
-        System.getProperty("os.name").startsWith("Win") -> "cmd /c start"
-        else -> "xdg-open"
-    },
-) {
-    val dotFile = outDir.resolve("$baseName.dot")
-    val svgFile = outDir.resolveSibling("$baseName.$format")
-    dotFile.writeText(dot)
-    Runtime.getRuntime().exec("$dotCmd $dotFile -T$format -o $svgFile").waitFor()
-    if (viewerCmd != null) {
-        Runtime.getRuntime().exec("$viewerCmd $svgFile").waitFor()
-    }
-}

From 553a67a16948417d6569d2989927bf06ab8c7793 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:47:45 +0300
Subject: [PATCH 65/69] Remove commented code

---
 usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt | 1 -
 1 file changed, 1 deletion(-)

diff --git a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
index 1c4bf3e3a..bca881d04 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/project/DemoPhotos.kt
@@ -17,7 +17,6 @@ import kotlin.test.Test
 import kotlin.time.Duration.Companion.seconds
 
 @EnabledIf("projectAvailable")
-// @Disabled
 class RunOnDemoPhotosProject : TsMethodTestRunner() {
 
     companion object {

From 176cac1e3934b721af9e687a88faf08f6ea0450b Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 16:50:55 +0300
Subject: [PATCH 66/69] Handle fake object *inside* neqNull check

---
 .../org/usvm/machine/expr/TsExprResolver.kt       | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 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 78c0d37a5..684ca3ee1 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
@@ -833,9 +833,15 @@ class TsExprResolver(
     }
 
     fun checkUndefinedOrNullPropertyRead(instance: UHeapRef) = with(ctx) {
+        val ref = if (instance.isFakeObject()) {
+            instance.extractRef(scope)
+        } else {
+            instance
+        }
+
         val neqNull = mkAnd(
-            mkHeapRefEq(instance, mkUndefinedValue()).not(),
-            mkHeapRefEq(instance, mkTsNullValue()).not()
+            mkHeapRefEq(ref, mkUndefinedValue()).not(),
+            mkHeapRefEq(ref, mkTsNullValue()).not(),
         )
 
         scope.fork(
@@ -959,11 +965,6 @@ class TsExprResolver(
     override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
         val instanceRef = resolve(value.instance)?.asExpr(addressSort) ?: return null
 
-        if (instanceRef.isFakeObject()) {
-            val ref = instanceRef.extractRef(scope)
-            checkUndefinedOrNullPropertyRead(ref) ?: return null
-        }
-
         checkUndefinedOrNullPropertyRead(instanceRef) ?: return null
 
         // TODO It is a hack for array's length

From db104d20bd446f82d0976c0b687403b119edd94b Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 17:24:01 +0300
Subject: [PATCH 67/69] Show 5 lines from stacktrace

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

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 078b4f1fa..71d73d81d 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
@@ -143,7 +143,7 @@ class TsInterpreter(
             }
         } catch (e: Exception) {
             logger.error {
-                "Exception: $e\n${e.stackTrace.take(3).joinToString("\n") { "    $it" }}"
+                "Exception: $e\n${e.stackTrace.take(5).joinToString("\n") { "    $it" }}"
             }
             return StepResult(forkedStates = emptySequence(), originalStateAlive = false)
             // todo are exceptional states properly removed?

From 3b665e6cba230af25bcfe3b9cd5c6045690216e8 Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 17:24:14 +0300
Subject: [PATCH 68/69] Extract ref from fake object recursively

---
 .../src/main/kotlin/org/usvm/machine/TsContext.kt    | 12 ++++++++++++
 .../kotlin/org/usvm/machine/expr/TsExprResolver.kt   |  2 +-
 2 files changed, 13 insertions(+), 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 e1052fbde..59fe46d9d 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -164,6 +164,18 @@ class TsContext(
         }
     }
 
+    fun UHeapRef.extractRefOrSelf(scope: TsStepScope): UHeapRef {
+        var current = this
+        while (current.isFakeObject()) {
+            val fakeType = current.getFakeType(scope)
+            scope.doWithState {
+                pathConstraints += fakeType.refTypeExpr
+            }
+            current = current.extractRef(scope)
+        }
+        return current
+    }
+
     fun createFakeObjectRef(): UConcreteHeapRef {
         val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET
         return mkConcreteHeapRef(address)
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 684ca3ee1..f6e55936d 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
@@ -879,7 +879,7 @@ class TsExprResolver(
         field: EtsFieldSignature,
         hierarchy: EtsHierarchy,
     ): UExpr<out USort>? = with(ctx) {
-        val resolvedAddr = if (instanceRef.isFakeObject()) instanceRef.extractRef(scope) else instanceRef
+        val resolvedAddr = instanceRef.extractRefOrSelf(scope)
 
         val etsField = resolveEtsField(instance, field, hierarchy)
 

From 041339e916212c668e8b63d0f4677bbf8a5015ac Mon Sep 17 00:00:00 2001
From: Konstantin Chukharev <lipen00@gmail.com>
Date: Wed, 2 Jul 2025 17:28:30 +0300
Subject: [PATCH 69/69] Kill the state on non-ref instance field access

---
 .../main/kotlin/org/usvm/machine/expr/TsExprResolver.kt    | 7 ++++++-
 1 file changed, 6 insertions(+), 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 f6e55936d..08ac24f9a 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
@@ -963,7 +963,12 @@ class TsExprResolver(
     }
 
     override fun visit(value: EtsInstanceFieldRef): UExpr<out USort>? = with(ctx) {
-        val instanceRef = resolve(value.instance)?.asExpr(addressSort) ?: return null
+        val instanceRefResolved = resolve(value.instance) ?: return null
+        if (instanceRefResolved.sort != addressSort) {
+            scope.assert(falseExpr)
+            return null
+        }
+        val instanceRef = instanceRefResolved.asExpr(addressSort)
 
         checkUndefinedOrNullPropertyRead(instanceRef) ?: return null