diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt
index 2092c26d98..fc3d31436b 100644
--- a/buildSrc/src/main/kotlin/Versions.kt
+++ b/buildSrc/src/main/kotlin/Versions.kt
@@ -4,7 +4,7 @@ object Versions {
     const val ksmt = "0.5.6"
     const val collections = "0.3.5"
     const val coroutines = "1.6.4"
-    const val jcdb = "1.1.3"
+    const val jcdb = "1.2.0"
     const val mockk = "1.13.4"
     const val junitParams = "5.9.3"
     const val logback = "1.4.8"
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 0b42916814..75ba8e1ab5 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -4,4 +4,3 @@ include("usvm-core")
 include("usvm-jvm")
 include("usvm-util")
 include("usvm-sample-language")
-include("usvm-jvm")
diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
index c3bd3d6e1b..c70be3340a 100644
--- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
@@ -23,8 +23,8 @@ class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
 ) {
     private val forkedStates = mutableListOf<T>()
 
-    private val alive: Boolean get() = stepScopeState != DEAD
-    private val canProcessFurtherOnCurrentStep: Boolean get() = stepScopeState == CAN_BE_PROCESSED
+    private inline val alive: Boolean get() = stepScopeState != DEAD
+    private inline val canProcessFurtherOnCurrentStep: Boolean get() = stepScopeState == CAN_BE_PROCESSED
 
     /**
      * Determines whether we interact this scope on the current step.
@@ -42,24 +42,20 @@ class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
      *
      * @return `null` if the underlying state is `null`.
      */
-    fun doWithState(block: T.() -> Unit): Unit? =
-        if (canProcessFurtherOnCurrentStep) {
-            originalState.block()
-        } else {
-            null
-        }
+    fun doWithState(block: T.() -> Unit) {
+        check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
+        return originalState.block()
+    }
 
     /**
      * Executes [block] on a state.
      *
      * @return `null` if the underlying state is `null`, otherwise returns result of calling [block].
      */
-    fun <R> calcOnState(block: T.() -> R): R? =
-        if (canProcessFurtherOnCurrentStep) {
-            originalState.block()
-        } else {
-            null
-        }
+    fun <R> calcOnState(block: T.() -> R): R {
+        check(canProcessFurtherOnCurrentStep) { "Caller should check before processing the current hop further" }
+        return originalState.block()
+    }
 
     /**
      * Forks on a [condition], performing [blockOnTrueState] on a state satisfying [condition] and
@@ -138,7 +134,7 @@ class StepScope<T : UState<Type, Field, *, *>, Type, Field>(
     ): Unit? {
         check(canProcessFurtherOnCurrentStep)
 
-        val (posState, _) = fork(originalState, constraint)
+        val (posState) = forkMulti(originalState, listOf(constraint))
 
         posState?.block()
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/BfsPathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/ps/BfsPathSelector.kt
index c051132586..63e1de55d8 100644
--- a/usvm-core/src/main/kotlin/org/usvm/ps/BfsPathSelector.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/ps/BfsPathSelector.kt
@@ -10,7 +10,10 @@ class BfsPathSelector<State> : UPathSelector<State> {
     override fun peek() = queue.first()
 
     override fun update(state: State) {
-        // nothing to do
+        if (state === queue.first()) {
+            queue.removeFirst()
+            queue.addLast(state)
+        }
     }
 
     override fun add(states: Collection<State>) {
@@ -24,4 +27,4 @@ class BfsPathSelector<State> : UPathSelector<State> {
             else -> queue.remove(state)
         }
     }
-}
\ No newline at end of file
+}
diff --git a/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt b/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt
index b906904188..03f6fb4311 100644
--- a/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/types/SupportTypeStream.kt
@@ -79,12 +79,10 @@ class USupportTypeStream<Type> private constructor(
         )
 
     override fun take(n: Int): Set<Type> {
-        val set = cacheFromQueries.toMutableSet()
-        for (it in cachingSequence) {
-            if (set.size == n) {
-                break
-            }
-            set += it
+        val set = cacheFromQueries.take(n).toMutableSet()
+        val iterator = cachingSequence.iterator()
+        while (set.size < n && iterator.hasNext()) {
+            set += iterator.next()
         }
         return set
     }
diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt
index f33b87b299..f91aff2273 100644
--- a/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt
@@ -24,6 +24,9 @@ class UTypeRegion<Type>(
 
     override val isEmpty: Boolean get() = typeStream.isEmpty
 
+    private val <Type> UTypeRegion<Type>.size: Int
+        get() = supertypes.size + notSupertypes.size + subtypes.size + notSubtypes.size
+
     /**
      * Excludes from this type region types which are not subtypes of [supertype].
      * If new type constraints contradict with already existing ones,
@@ -32,19 +35,30 @@ class UTypeRegion<Type>(
      * The default implementation checks for the following contradictions
      * (here X is type from this region and t is [supertype]):
      *  - X <: t && t <: u && X </: u, i.e. if [notSupertypes] contains supertype of [supertype]
+     *  - X <: t && u <: X && u </: t
      *  - X <: t && X <: u && u </: t && t </: u && t and u can't be multiply inherited
      *  - t is final && t </: X && X <: t
+     *
+     * Also, if u <: X && X <: t && u <: t, then X = u = t.
      */
     fun addSupertype(supertype: Type): UTypeRegion<Type> {
+        // X <: it && it <: supertype -> nothing changes
         if (isEmpty || supertypes.any { typeSystem.isSupertype(supertype, it) }) {
             return this
         }
 
-        if (notSubtypes.any { typeSystem.isSupertype(it, supertype) }) {
+        // X </: it && supertype <: it -> X </: supertype
+        if (notSupertypes.any { typeSystem.isSupertype(it, supertype) }) {
+            return contradiction()
+        }
+
+        // it <: X && it </: supertype -> X </: supertype
+        if (subtypes.any { !typeSystem.isSupertype(supertype, it) }) {
             return contradiction()
         }
 
         val multipleInheritanceIsNotAllowed = !typeSystem.isMultipleInheritanceAllowedFor(supertype)
+
         if (multipleInheritanceIsNotAllowed) {
             // We've already checked it </: supertype
             val incomparableSupertypeWithoutMultipleInheritanceAllowedExists = supertypes.any {
@@ -67,10 +81,15 @@ class UTypeRegion<Type>(
             subtypes
         }
 
+        // it <: X && supertype <: it -> X == supertype
+        if (newSubtypes.any { typeSystem.isSupertype(it, supertype) }) {
+            return checkSingleTypeRegion(supertype)
+        }
+
         val newSupertypes = supertypes.removeAll { typeSystem.isSupertype(it, supertype) }.add(supertype)
         val newTypeStream = typeStream.filterBySupertype(supertype)
 
-        return UTypeRegion(typeSystem, newTypeStream, supertypes = newSupertypes, subtypes = newSubtypes)
+        return clone(newTypeStream, supertypes = newSupertypes, subtypes = newSubtypes)
     }
 
     /**
@@ -94,7 +113,7 @@ class UTypeRegion<Type>(
         val newNotSupertypes = notSupertypes.removeAll { typeSystem.isSupertype(notSupertype, it) }.add(notSupertype)
         val newTypeStream = typeStream.filterByNotSupertype(notSupertype)
 
-        return UTypeRegion(typeSystem, newTypeStream, notSupertypes = newNotSupertypes)
+        return clone(newTypeStream, notSupertypes = newNotSupertypes)
     }
 
     /**
@@ -106,24 +125,34 @@ class UTypeRegion<Type>(
      * (here X is type from this region and t is [subtype]):
      *  - t <: X && u <: t && u </: X, i.e. if [notSubtypes] contains subtype of [subtype]
      *  - t <: X && X <: u && t </: u
+     *
+     *  Also, if t <: X && X <: u && u <: t, then X = u = t.
      */
     fun addSubtype(subtype: Type): UTypeRegion<Type> {
+        // it <: X && subtype <: it -> nothing changes
         if (isEmpty || subtypes.any { typeSystem.isSupertype(it, subtype) }) {
             return this
         }
 
+        // it </: X && it <: subtype -> subtype </: X
         if (notSubtypes.any { typeSystem.isSupertype(subtype, it) }) {
             return contradiction()
         }
 
+        // X <: it && subtype </: it -> subtype </: X
         if (supertypes.any { !typeSystem.isSupertype(it, subtype) }) {
             return contradiction()
         }
 
+        // X <: it && it <: subtype -> X <: subtype -> X == subtype
+        if (supertypes.any { typeSystem.isSupertype(subtype, it) }) {
+            return checkSingleTypeRegion(subtype)
+        }
+
         val newSubtypes = subtypes.removeAll { typeSystem.isSupertype(subtype, it) }.add(subtype)
         val newTypeStream = typeStream.filterBySubtype(subtype)
 
-        return UTypeRegion(typeSystem, newTypeStream, subtypes = newSubtypes)
+        return clone(newTypeStream, subtypes = newSubtypes)
     }
 
     /**
@@ -149,7 +178,7 @@ class UTypeRegion<Type>(
         val newNotSubtypes = notSubtypes.removeAll { typeSystem.isSupertype(it, notSubtype) }.add(notSubtype)
         val newTypeStream = typeStream.filterByNotSubtype(notSubtype)
 
-        return UTypeRegion(typeSystem, newTypeStream, notSubtypes = newNotSubtypes)
+        return clone(newTypeStream, notSubtypes = newNotSubtypes)
     }
 
     override fun intersect(other: UTypeRegion<Type>): UTypeRegion<Type> {
@@ -202,7 +231,43 @@ class UTypeRegion<Type>(
         return RegionComparisonResult.INTERSECTS
     }
 
-}
+    private fun checkSingleTypeRegion(type: Type): UTypeRegion<Type> {
+        if (!typeSystem.isInstantiable(type)) {
+            return contradiction()
+        }
 
-private val <Type> UTypeRegion<Type>.size: Int
-    get() = supertypes.size + subtypes.size + notSupertypes.size + notSubtypes.size
+        // X <: it && type </: it && X == type -> X <: X && X </: X
+        if (supertypes.any { !typeSystem.isSupertype(it, type) }) {
+            return contradiction()
+        }
+
+        // X </: it && type <: it && X == type -> X </: it && X <: it
+        if (notSupertypes.any { typeSystem.isSupertype(it, type) }) {
+            return contradiction()
+        }
+
+        // it <: X && it </: type && X == type -> it <: X && it </: X
+        if (subtypes.any { !typeSystem.isSupertype(type, it) }) {
+            return contradiction()
+        }
+
+        // it </: X && it <: type && X == type -> it </: X && it <: X
+        if (notSubtypes.any { typeSystem.isSupertype(type, it) }) {
+            return contradiction()
+        }
+
+        return clone(
+            USingleTypeStream(typeSystem, type),
+            supertypes = persistentSetOf(type),
+            subtypes = persistentSetOf(type)
+        )
+    }
+
+    private fun clone(
+        typeStream: UTypeStream<Type>,
+        supertypes: PersistentSet<Type> = this.supertypes,
+        notSupertypes: PersistentSet<Type> = this.notSupertypes,
+        subtypes: PersistentSet<Type> = this.subtypes,
+        notSubtypes: PersistentSet<Type> = this.notSubtypes,
+    ) = UTypeRegion(typeSystem, typeStream, supertypes, notSupertypes, subtypes, notSubtypes)
+}
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
index a70ce3945e..3007b1ede0 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMachine.kt
@@ -9,6 +9,7 @@ import org.usvm.CoverageZone
 import org.usvm.PathSelectorCombinationStrategy
 import org.usvm.UMachine
 import org.usvm.UMachineOptions
+import org.usvm.machine.interpreter.JcInterpreter
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.lastStmt
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt
index 944793576f..d2a0b2161e 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTypeSystem.kt
@@ -6,6 +6,7 @@ import org.jacodb.api.JcClasspath
 import org.jacodb.api.JcPrimitiveType
 import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
+import org.jacodb.api.JcTypeVariable
 import org.jacodb.api.ext.isAssignable
 import org.jacodb.api.ext.objectType
 import org.jacodb.api.ext.toType
@@ -20,7 +21,9 @@ class JcTypeSystem(
     private val hierarchy = HierarchyExtensionImpl(cp)
 
     override fun isSupertype(supertype: JcType, type: JcType): Boolean =
-        type.isAssignable(supertype)
+        type.isAssignable(supertype) ||
+                // It is possible when, for example, the returning type of a method is a type variable
+                (supertype is JcTypeVariable && type.isAssignable(supertype.jcClass.toType()))
 
     override fun isMultipleInheritanceAllowedFor(type: JcType): Boolean =
         (type as? JcClassType)?.jcClass?.isInterface ?: false
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt
similarity index 85%
rename from usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt
rename to usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt
index 11c3ca63da..63ae672d63 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcExprResolver.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt
@@ -1,5 +1,6 @@
-package org.usvm.machine
+package org.usvm.machine.interpreter
 
+import io.ksmt.expr.KExpr
 import io.ksmt.utils.asExpr
 import io.ksmt.utils.cast
 import org.jacodb.api.JcArrayType
@@ -33,7 +34,6 @@ import org.jacodb.api.cfg.JcFieldRef
 import org.jacodb.api.cfg.JcFloat
 import org.jacodb.api.cfg.JcGeExpr
 import org.jacodb.api.cfg.JcGtExpr
-import org.jacodb.api.cfg.JcInstanceCallExpr
 import org.jacodb.api.cfg.JcInstanceOfExpr
 import org.jacodb.api.cfg.JcInt
 import org.jacodb.api.cfg.JcLambdaExpr
@@ -91,6 +91,7 @@ import org.usvm.USizeExpr
 import org.usvm.USizeSort
 import org.usvm.USort
 import org.usvm.isTrue
+import org.usvm.machine.JcContext
 import org.usvm.machine.operator.JcBinaryOperator
 import org.usvm.machine.operator.JcUnaryOperator
 import org.usvm.machine.operator.ensureBvExpr
@@ -98,7 +99,6 @@ import org.usvm.machine.operator.mkNarrow
 import org.usvm.machine.operator.wideTo32BitsIfNeeded
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
-import org.usvm.machine.state.addNewMethodCall
 import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop
 import org.usvm.util.extractJcRefType
 
@@ -109,9 +109,9 @@ import org.usvm.util.extractJcRefType
 class JcExprResolver(
     private val ctx: JcContext,
     private val scope: JcStepScope,
-    private val applicationGraph: JcApplicationGraph,
     private val localToIdx: (JcMethod, JcLocal) -> Int,
     private val mkClassRef: (JcRefType, JcState) -> UHeapRef,
+    private val invokeResolver: JcInvokeResolver,
     private val hardMaxArrayLength: Int = 1_500, // TODO: move to options
 ) : JcExprVisitor<UExpr<out USort>?> {
     /**
@@ -141,7 +141,7 @@ class JcExprResolver(
             else -> error("Unexpected value: $value")
         }
 
-    override fun visitExternalJcExpr(expr: JcExpr): UExpr<out USort> = with(ctx) {
+    override fun visitExternalJcExpr(expr: JcExpr): UExpr<out USort> {
         error("Unexpected expression: $expr")
     }
 
@@ -271,20 +271,20 @@ class JcExprResolver(
         nullRef
     }
 
-    override fun visitJcStringConstant(value: JcStringConstant): UExpr<out USort> = with(ctx) {
-        TODO("Not yet implemented")
+    override fun visitJcStringConstant(value: JcStringConstant): UExpr<out USort> {
+        TODO("String constant")
     }
 
-    override fun visitJcMethodConstant(value: JcMethodConstant): UExpr<out USort> = with(ctx) {
-        TODO("Not yet implemented")
+    override fun visitJcMethodConstant(value: JcMethodConstant): UExpr<out USort> {
+        TODO("Method constant")
     }
 
-    override fun visitJcMethodType(value: JcMethodType): UExpr<out USort>? {
-        TODO("Not yet implemented")
+    override fun visitJcMethodType(value: JcMethodType): UExpr<out USort> {
+        TODO("Method type")
     }
 
-    override fun visitJcClassConstant(value: JcClassConstant): UExpr<out USort> = with(ctx) {
-        TODO("Not yet implemented")
+    override fun visitJcClassConstant(value: JcClassConstant): UExpr<out USort> {
+        TODO("Class constant")
     }
 
     // endregion
@@ -305,7 +305,7 @@ class JcExprResolver(
         checkNullPointer(ref) ?: return null
         val arrayDescriptor = arrayDescriptorOf(expr.array.type as JcArrayType)
         val lengthRef = UArrayLengthLValue(ref, arrayDescriptor)
-        val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) } ?: return null
+        val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
         assertHardMaxArrayLength(length) ?: return null
         scope.assert(mkBvSignedLessOrEqualExpr(mkBv(0), length)) ?: return null
         length
@@ -315,14 +315,12 @@ class JcExprResolver(
         val size = resolveCast(expr.dimensions[0], ctx.cp.int)?.asExpr(bv32Sort) ?: return null
         // TODO: other dimensions ( > 1)
         checkNewArrayLength(size) ?: return null
-        val ref = scope.calcOnState { memory.malloc(expr.type, size) } ?: return null
+        val ref = scope.calcOnState { memory.malloc(expr.type, size) }
         ref
     }
 
-    override fun visitJcNewExpr(expr: JcNewExpr): UExpr<out USort>? =
-        scope.calcOnState {
-            memory.alloc(expr.type)
-        }
+    override fun visitJcNewExpr(expr: JcNewExpr): UExpr<out USort> =
+        scope.calcOnState { memory.alloc(expr.type) }
 
     override fun visitJcPhiExpr(expr: JcPhiExpr): UExpr<out USort> =
         error("Unexpected expr: $expr")
@@ -330,70 +328,95 @@ class JcExprResolver(
     // region invokes
 
     override fun visitJcSpecialCallExpr(expr: JcSpecialCallExpr): UExpr<out USort>? =
-        resolveInstanceCallExpr(expr)
+        resolveInvoke(
+            expr.method,
+            instanceExpr = expr.instance,
+            argumentExprs = expr::args,
+            argumentTypes = { expr.method.parameters.map { it.type } }
+        ) { arguments ->
+            with(invokeResolver) { resolveSpecialInvoke(expr.method.method, arguments) }
+        }
 
     override fun visitJcVirtualCallExpr(expr: JcVirtualCallExpr): UExpr<out USort>? =
-        resolveInstanceCallExpr(expr) // TODO resolve actual method for interface invokes
-
-    private fun resolveInstanceCallExpr(expr: JcInstanceCallExpr): UExpr<out USort>? =
-        resolveInvoke(expr.method) {
-            val instance = resolveJcExpr(expr.instance)?.asExpr(ctx.addressSort) ?: return@resolveInvoke null
-            checkNullPointer(instance) ?: return@resolveInvoke null
-            val arguments = mutableListOf<UExpr<out USort>>(instance)
-            val argsWithTypes = expr.args.zip(expr.method.parameters.map { it.type })
-
-            argsWithTypes.mapTo(arguments) { (expr, type) ->
-                resolveJcExpr(expr, type) ?: return@resolveInvoke null
-            }
-            arguments
+        resolveInvoke(
+            expr.method,
+            instanceExpr = expr.instance,
+            argumentExprs = expr::args,
+            argumentTypes = { expr.method.parameters.map { it.type } }
+        ) { arguments ->
+            with(invokeResolver) { resolveVirtualInvoke(expr.method.method, arguments) }
         }
 
     override fun visitJcStaticCallExpr(expr: JcStaticCallExpr): UExpr<out USort>? =
-        resolveInvoke(expr.method) {
-            val argsWithTypes = expr.args.zip(expr.method.parameters.map { it.type })
-
-            argsWithTypes.map { (expr, type) ->
-                resolveJcExpr(expr, type) ?: return@resolveInvoke null
+        resolveInvoke(
+            expr.method,
+            instanceExpr = null,
+            argumentExprs = expr::args,
+            argumentTypes = { expr.method.parameters.map { it.type } }
+        ) { arguments ->
+            with(invokeResolver) {
+                resolveStaticInvoke(expr.method.method, arguments)
             }
         }
 
-    override fun visitJcDynamicCallExpr(expr: JcDynamicCallExpr): UExpr<out USort> = with(ctx) {
-        TODO("Not yet implemented")
-    }
+    override fun visitJcDynamicCallExpr(expr: JcDynamicCallExpr): UExpr<out USort>? =
+        resolveInvoke(
+            expr.method,
+            instanceExpr = null,
+            argumentExprs = expr::args,
+            argumentTypes = expr::callSiteArgTypes
+        ) { arguments ->
+            with(invokeResolver) {
+                resolveDynamicInvoke(expr.method.method, arguments)
+            }
+        }
 
     override fun visitJcLambdaExpr(expr: JcLambdaExpr): UExpr<out USort>? =
-        resolveInvoke(expr.method) {
-            val argsWithTypes = expr.args.zip(expr.method.parameters.map { it.type })
-
-            argsWithTypes.map { (expr, type) ->
-                resolveJcExpr(expr, type) ?: return@resolveInvoke null
+        resolveInvoke(
+            expr.method,
+            instanceExpr = null,
+            argumentExprs = expr::args,
+            argumentTypes = { expr.method.parameters.map { it.type } }
+        ) { arguments ->
+            with(invokeResolver) {
+                resolveLambdaInvoke(expr.method.method, arguments)
             }
         }
 
-    private fun resolveInvoke(
+    private inline fun resolveInvoke(
         method: JcTypedMethod,
-        resolveArguments: () -> List<UExpr<out USort>>?,
+        instanceExpr: JcValue?,
+        argumentExprs: () -> List<JcValue>,
+        argumentTypes: () -> List<JcType>,
+        onNoCallPresent: JcStepScope.(List<UExpr<out USort>>) -> Unit,
     ): UExpr<out USort>? = ensureStaticFieldsInitialized(method.enclosingType) {
-        resolveInvokeNoStaticInitializationCheck(method, resolveArguments)
+        val arguments = mutableListOf<UExpr<out USort>>()
+
+        if (instanceExpr != null) {
+            val instance = resolveJcExpr(instanceExpr)?.asExpr(ctx.addressSort) ?: return null
+            checkNullPointer(instance) ?: return null
+            arguments += instance
+        }
+
+        argumentExprs().zip(argumentTypes()) { expr, type ->
+            arguments += resolveJcExpr(expr, type) ?: return null
+        }
+
+        resolveInvokeNoStaticInitializationCheck { onNoCallPresent(arguments) }
     }
 
-    private fun resolveInvokeNoStaticInitializationCheck(
-        method: JcTypedMethod,
-        resolveArguments: () -> List<UExpr<out USort>>?,
+    private inline fun resolveInvokeNoStaticInitializationCheck(
+        onNoCallPresent: JcStepScope.() -> Unit,
     ): UExpr<out USort>? {
-        val result = scope.calcOnState { methodResult } ?: return null
+        val result = scope.calcOnState { methodResult }
         return when (result) {
             is JcMethodResult.Success -> {
-                check(result.method == method.method) {
-                    "Expected result from ${method.method} but actual is ${result.method}"
-                }
                 scope.doWithState { methodResult = JcMethodResult.NoCall }
                 result.value
             }
 
             is JcMethodResult.NoCall -> {
-                val arguments = resolveArguments() ?: return null
-                scope.doWithState { addNewMethodCall(applicationGraph, method.method, arguments) }
+                scope.onNoCallPresent()
                 null
             }
 
@@ -405,17 +428,17 @@ class JcExprResolver(
 
     // region jc locals
 
-    override fun visitJcLocalVar(value: JcLocalVar): UExpr<out USort>? = with(ctx) {
+    override fun visitJcLocalVar(value: JcLocalVar): UExpr<out USort> = with(ctx) {
         val ref = resolveLocal(value)
         scope.calcOnState { memory.read(ref) }
     }
 
-    override fun visitJcThis(value: JcThis): UExpr<out USort>? = with(ctx) {
+    override fun visitJcThis(value: JcThis): UExpr<out USort> = with(ctx) {
         val ref = resolveLocal(value)
         scope.calcOnState { memory.read(ref) }
     }
 
-    override fun visitJcArgument(value: JcArgument): UExpr<out USort>? = with(ctx) {
+    override fun visitJcArgument(value: JcArgument): UExpr<out USort> = with(ctx) {
         val ref = resolveLocal(value)
         scope.calcOnState { memory.read(ref) }
     }
@@ -425,14 +448,31 @@ class JcExprResolver(
     // region jc complex values
 
     override fun visitJcFieldRef(value: JcFieldRef): UExpr<out USort>? {
-        val ref = resolveFieldRef(value.instance, value.field) ?: return null
-        return scope.calcOnState { memory.read(ref) }
-    }
+        val lValue = resolveFieldRef(value.instance, value.field) ?: return null
+        val expr = scope.calcOnState { memory.read(lValue) }
+
+        if (assertIsSubtype(expr, value.type)) return expr
 
+        return null
+    }
 
     override fun visitJcArrayAccess(value: JcArrayAccess): UExpr<out USort>? {
-        val ref = resolveArrayAccess(value.array, value.index) ?: return null
-        return scope.calcOnState { memory.read(ref) }
+        val lValue = resolveArrayAccess(value.array, value.index) ?: return null
+        val expr = scope.calcOnState { memory.read(lValue) }
+
+        if (assertIsSubtype(expr, value.type)) return expr
+
+        return null
+    }
+
+    private fun assertIsSubtype(expr: KExpr<out USort>, type: JcType): Boolean {
+        if (type is JcRefType) {
+            val heapRef = expr.asExpr(ctx.addressSort)
+            val isExpr = scope.calcOnState { memory.types.evalIsSubtype(heapRef, type) }
+            scope.assert(isExpr) ?: return false
+        }
+
+        return true
     }
 
     // endregion
@@ -451,7 +491,7 @@ class JcExprResolver(
                     val sort = ctx.typeToSort(field.fieldType)
                     val classRef = scope.calcOnState {
                         mkClassRef(field.enclosingType, this)
-                    } ?: return null
+                    }
                     UFieldLValue(sort, classRef, field.field)
                 }
             }
@@ -474,13 +514,13 @@ class JcExprResolver(
             return body()
         }
 
-        val classRef = scope.calcOnState { mkClassRef(type, this) } ?: return null
+        val classRef = scope.calcOnState { mkClassRef(type, this) }
 
         val initializedFlag = staticFieldsInitializedFlag(type, classRef)
 
         val staticFieldsInitialized = scope.calcOnState {
             memory.read(initializedFlag).asExpr(ctx.booleanSort)
-        } ?: return null
+        }
 
 
         if (staticFieldsInitialized.isTrue) {
@@ -498,8 +538,8 @@ class JcExprResolver(
         // Run static initializer before the current statement
         scope.doWithState {
             memory.write(initializedFlag, ctx.trueExpr)
-            addNewMethodCall(applicationGraph, initializer, emptyList())
         }
+        with(invokeResolver) { scope.resolveStaticInvoke(initializer, emptyList()) }
         return null
     }
 
@@ -518,7 +558,7 @@ class JcExprResolver(
 
         val idx = resolveCast(index, ctx.cp.int)?.asExpr(bv32Sort) ?: return null
         val lengthRef = UArrayLengthLValue(arrayRef, arrayDescriptor)
-        val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) } ?: return null
+        val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
 
         assertHardMaxArrayLength(length) ?: return null
 
@@ -592,8 +632,7 @@ class JcExprResolver(
 
     private fun assertHardMaxArrayLength(length: USizeExpr): Unit? = with(ctx) {
         val lengthLeThanMaxLength = mkBvSignedLessOrEqualExpr(length, mkBv(hardMaxArrayLength))
-        scope.assert(lengthLeThanMaxLength) ?: return null
-        return Unit
+        scope.assert(lengthLeThanMaxLength)
     }
 
     // endregion
@@ -646,20 +685,19 @@ class JcExprResolver(
         type: JcType,
     ) = resolveAfterResolved(operand) { expr ->
         when (type) {
-            is JcRefType -> resolveReferenceCast(expr, operand.type as JcRefType, type)
+            is JcRefType -> resolveReferenceCast(expr.asExpr(ctx.addressSort), operand.type as JcRefType, type)
             is JcPrimitiveType -> resolvePrimitiveCast(expr, operand.type as JcPrimitiveType, type)
             else -> error("Unexpected type: $type")
         }
     }
 
     private fun resolveReferenceCast(
-        expr: UExpr<out USort>,
+        expr: UHeapRef,
         typeBefore: JcRefType,
         type: JcRefType,
-    ): UExpr<out USort>? {
+    ): UHeapRef? {
         return if (!typeBefore.isAssignable(type)) {
-            val isExpr = scope.calcOnState { memory.types.evalIsSubtype(expr.asExpr(ctx.addressSort), type) }
-                ?: return null
+            val isExpr = scope.calcOnState { memory.types.evalIsSubtype(expr, type) }
             scope.fork(
                 isExpr,
                 blockOnFalseState = allocateException(classCastExceptionType)
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcFixedInheritorsNumberTypeSelector.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcFixedInheritorsNumberTypeSelector.kt
new file mode 100644
index 0000000000..6d5d35f16f
--- /dev/null
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcFixedInheritorsNumberTypeSelector.kt
@@ -0,0 +1,21 @@
+package org.usvm.machine.interpreter
+
+import org.jacodb.api.JcMethod
+import org.jacodb.api.JcType
+import org.usvm.types.UTypeStream
+
+interface JcTypeSelector {
+    fun choose(method: JcMethod, typeStream: UTypeStream<JcType>): Collection<JcType>
+}
+
+class JcFixedInheritorsNumberTypeSelector(
+    private val inheritorsNumberToChoose: Int = DEFAULT_INHERITORS_NUMBER_TO_CHOOSE,
+) : JcTypeSelector {
+    override fun choose(method: JcMethod, typeStream: UTypeStream<JcType>): Collection<JcType> {
+        return typeStream.take(inheritorsNumberToChoose)
+    }
+
+    companion object {
+        const val DEFAULT_INHERITORS_NUMBER_TO_CHOOSE: Int = 4
+    }
+}
\ No newline at end of file
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
similarity index 96%
rename from usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt
rename to usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
index 691205451e..1392f72417 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcInterpreter.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
@@ -1,4 +1,4 @@
-package org.usvm.machine
+package org.usvm.machine.interpreter
 
 import io.ksmt.utils.asExpr
 import mu.KLogging
@@ -29,6 +29,8 @@ import org.usvm.UBoolExpr
 import org.usvm.UHeapRef
 import org.usvm.UInterpreter
 import org.usvm.URegisterLValue
+import org.usvm.machine.JcApplicationGraph
+import org.usvm.machine.JcContext
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.addEntryMethodCall
@@ -149,14 +151,14 @@ class JcInterpreter(
                 typeConstraintsNegations += currentTypeConstraints.map { ctx.mkNot(it) }
 
                 result
-            } ?: return@forEach
+            }
 
             catchForks += typeConstraint to blockToFork(catchInst)
         }
 
         val typeConditionToMiss = ctx.mkAnd(typeConstraintsNegations)
         val functionBlockOnMiss = block@{ _: JcState ->
-            scope.calcOnState { throwExceptionAndDropStackFrame() } ?: return@block
+            scope.calcOnState { throwExceptionAndDropStackFrame() }
         }
 
         val catchSectionMiss = typeConditionToMiss to functionBlockOnMiss
@@ -262,11 +264,15 @@ class JcInterpreter(
         }
     }
 
+    private val invokeResolver = JcVirtualInvokeResolver(ctx, applicationGraph, JcFixedInheritorsNumberTypeSelector())
+
     private fun exprResolverWithScope(scope: JcStepScope) =
         JcExprResolver(
-            ctx, scope, applicationGraph,
+            ctx,
+            scope,
             ::mapLocalToIdxMapper,
-            ::classInstanceAllocator
+            ::classInstanceAllocator,
+            invokeResolver
         )
 
     private val localVarToIdx = mutableMapOf<JcMethod, MutableMap<String, Int>>() // (method, localName) -> idx
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInvokeResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInvokeResolver.kt
new file mode 100644
index 0000000000..b9a8f63217
--- /dev/null
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInvokeResolver.kt
@@ -0,0 +1,129 @@
+package org.usvm.machine.interpreter
+
+import io.ksmt.utils.asExpr
+import org.jacodb.api.JcClassType
+import org.jacodb.api.JcMethod
+import org.jacodb.api.ext.findMethodOrNull
+import org.usvm.INITIAL_INPUT_ADDRESS
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.USort
+import org.usvm.machine.JcApplicationGraph
+import org.usvm.machine.JcContext
+import org.usvm.machine.state.JcState
+import org.usvm.machine.state.addNewMethodCall
+import org.usvm.machine.state.lastStmt
+import org.usvm.machine.state.newStmt
+import org.usvm.types.first
+
+interface JcInvokeResolver {
+    fun JcStepScope.resolveStaticInvoke(method: JcMethod, arguments: List<UExpr<out USort>>)
+    fun JcStepScope.resolveLambdaInvoke(method: JcMethod, arguments: List<UExpr<out USort>>)
+    fun JcStepScope.resolveVirtualInvoke(method: JcMethod, arguments: List<UExpr<out USort>>)
+    fun JcStepScope.resolveSpecialInvoke(method: JcMethod, arguments: List<UExpr<out USort>>)
+    fun JcStepScope.resolveDynamicInvoke(method: JcMethod, arguments: List<UExpr<out USort>>)
+}
+
+class JcVirtualInvokeResolver(
+    private val ctx: JcContext,
+    private val applicationGraph: JcApplicationGraph,
+    private val typeSelector: JcTypeSelector,
+    private val forkOnRemainingTypes: Boolean = false,
+) : JcInvokeResolver {
+    override fun JcStepScope.resolveStaticInvoke(method: JcMethod, arguments: List<UExpr<out USort>>) {
+        if (skip(method)) {
+            return
+        }
+
+        doWithState { addNewMethodCall(applicationGraph, method, arguments) }
+    }
+
+    override fun JcStepScope.resolveLambdaInvoke(method: JcMethod, arguments: List<UExpr<out USort>>) {
+        if (skip(method)) {
+            return
+        }
+
+        doWithState { addNewMethodCall(applicationGraph, method, arguments) }
+    }
+
+    override fun JcStepScope.resolveVirtualInvoke(
+        method: JcMethod,
+        arguments: List<UExpr<out USort>>,
+    ) {
+        if (skip(method)) {
+            return
+        }
+
+        val instance = arguments.first().asExpr(ctx.addressSort)
+        val concreteRef = calcOnState { models.first().eval(instance) } as UConcreteHeapRef
+
+        if (concreteRef.address <= INITIAL_INPUT_ADDRESS) {
+            val typeStream = calcOnState { models.first().typeStreamOf(concreteRef) }
+
+            val inheritors = typeSelector.choose(method, typeStream)
+            val typeConstraints = inheritors.map { type ->
+                calcOnState {
+                    ctx.mkAnd(memory.types.evalIsSubtype(instance, type), memory.types.evalIsSupertype(instance, type))
+                }
+            }
+
+            val typeConstraintsWithBlockOnStates = mutableListOf<Pair<UBoolExpr, (JcState) -> Unit>>()
+
+            inheritors.mapIndexedTo(typeConstraintsWithBlockOnStates) { idx, type ->
+                val isExpr = typeConstraints[idx]
+                val concreteMethod = (type as JcClassType).findMethodOrNull(method.name, method.description)
+                    ?: error("Can't find method $method in type $type")
+
+                val block = { state: JcState ->
+                    state.addNewMethodCall(applicationGraph, concreteMethod.method, arguments)
+                }
+
+                isExpr to block
+            }
+
+            if (forkOnRemainingTypes) {
+                val excludeAllTypesConstraint = ctx.mkAnd(typeConstraints.map { ctx.mkNot(it) })
+                typeConstraintsWithBlockOnStates += excludeAllTypesConstraint to { } // do nothing, just exclude types
+            }
+
+            forkMulti(typeConstraintsWithBlockOnStates)
+        } else {
+            val type = calcOnState { memory.typeStreamOf(concreteRef) }.first() as JcClassType
+
+            val concreteMethod = type.findMethodOrNull(method.name, method.description)
+                ?: error("Can't find method $method in type $type")
+
+            doWithState { addNewMethodCall(applicationGraph, concreteMethod.method, arguments) }
+        }
+    }
+
+    override fun JcStepScope.resolveSpecialInvoke(
+        method: JcMethod,
+        arguments: List<UExpr<out USort>>,
+    ) {
+        if (skip(method)) {
+            return
+        }
+
+        doWithState { addNewMethodCall(applicationGraph, method, arguments) }
+    }
+
+    override fun JcStepScope.resolveDynamicInvoke(method: JcMethod, arguments: List<UExpr<out USort>>) {
+        TODO("Dynamic invoke")
+    }
+
+    private fun JcStepScope.skip(method: JcMethod): Boolean {
+        // Skip native method in static initializer
+        if ((method.name == "registerNatives" && method.enclosingClass.name == "java.lang.Class")
+            || (method.enclosingClass.name == "java.lang.Throwable")
+        ) {
+            doWithState {
+                val nextStmt = applicationGraph.successors(lastStmt).single()
+                newStmt(nextStmt)
+            }
+            return true
+        }
+        return false
+    }
+}
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt
index 342520e284..f2a57b6f2e 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcStateUtils.kt
@@ -69,20 +69,6 @@ fun JcState.addNewMethodCall(
     method: JcMethod,
     arguments: List<UExpr<out USort>>,
 ) {
-    // TODO: move to appropriate place
-    if (method.enclosingClass.name == "java.lang.Throwable") { // TODO: skipping construction of throwables
-        val nextStmt = applicationGraph.successors(lastStmt).single()
-        newStmt(nextStmt)
-        return
-    }
-
-    // TODO: move to appropriate place. Skip native method in static initializer
-    if (method.name == "registerNatives" && method.enclosingClass.name == "java.lang.Class") {
-        val nextStmt = applicationGraph.successors(lastStmt).single()
-        newStmt(nextStmt)
-        return
-    }
-
     // TODO: find concrete implementation (I guess, the method should be already concrete)
     val entryPoint = applicationGraph.entryPoints(method).singleOrNull()
         ?: error("No entrypoint found for method: $method")
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Ast.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Ast.java
new file mode 100644
index 0000000000..46332066d8
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Ast.java
@@ -0,0 +1,5 @@
+package org.usvm.samples.ast;
+
+public interface Ast {
+    <T> T accept(Visitor<T> visitor);
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/AstExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/AstExample.java
new file mode 100644
index 0000000000..7503a80fc2
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/AstExample.java
@@ -0,0 +1,31 @@
+package org.usvm.samples.ast;
+
+public class AstExample {
+    public int replaceLeafAndCheck(Ast leaf) {
+        DefaultSubstitutor substitutor = new DefaultSubstitutor(0);
+        Ast ast = new Sum(
+                new Minus(
+                        new Constant(13),
+                        new Constant(-16)
+                ),
+                new Minus(
+                        new Constant(13),
+                        leaf
+                )
+        );
+        Ast substituted = ast.accept(substitutor);
+        Evaluator evaluator = new Evaluator();
+        Constant result = substituted.accept(evaluator);
+
+        // (13 - (-16)) + (13 - leaf) == 0
+        if (result.getConstant() == 0) {
+            // too easy
+            if (leaf instanceof Constant) {
+                return -1;
+            }
+            return 0;
+        } else {
+            return 1;
+        }
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Binary.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Binary.java
new file mode 100644
index 0000000000..2707cc3463
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Binary.java
@@ -0,0 +1,18 @@
+package org.usvm.samples.ast;
+
+abstract class Binary implements Ast {
+    private final Ast left, right;
+
+    public Binary(Ast left, Ast right) {
+        this.left = left;
+        this.right = right;
+    }
+
+    public Ast getLeft() {
+        return left;
+    }
+
+    public Ast getRight() {
+        return right;
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Constant.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Constant.java
new file mode 100644
index 0000000000..185fdf6bb7
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Constant.java
@@ -0,0 +1,18 @@
+package org.usvm.samples.ast;
+
+public class Constant implements Ast {
+    final private int constant;
+
+    public Constant(int constant) {
+        this.constant = constant;
+    }
+
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+
+    public int getConstant() {
+        return constant;
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/DefaultSubstitutor.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/DefaultSubstitutor.java
new file mode 100644
index 0000000000..6a59e14199
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/DefaultSubstitutor.java
@@ -0,0 +1,39 @@
+package org.usvm.samples.ast;
+
+public class DefaultSubstitutor implements Visitor<Ast> {
+    private final int defaultValue;
+
+    public DefaultSubstitutor(int defaultValue) {
+        this.defaultValue = defaultValue;
+    }
+
+    @Override
+    public Ast visit(Constant constant) {
+        return constant;
+    }
+
+    @Override
+    public Ast visit(Sum sum) {
+        Ast left = sum.getLeft().accept(this);
+        Ast right = sum.getRight().accept(this);
+        if (left == sum.getLeft() && right == sum.getRight()) {
+            return sum;
+        }
+        return new Sum(left, right);
+    }
+
+    @Override
+    public Ast visit(Minus minus) {
+        Ast left = minus.getLeft().accept(this);
+        Ast right = minus.getRight().accept(this);
+        if (left == minus.getLeft() && right == minus.getRight()) {
+            return minus;
+        }
+        return new Minus(left, right);
+    }
+
+    @Override
+    public Ast visit(Variable variable) {
+        return new Constant(defaultValue);
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Evaluator.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Evaluator.java
new file mode 100644
index 0000000000..a6ca3f357c
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Evaluator.java
@@ -0,0 +1,27 @@
+package org.usvm.samples.ast;
+
+public class Evaluator implements Visitor<Constant> {
+    @Override
+    public Constant visit(Constant constant) {
+        return constant;
+    }
+
+    @Override
+    public Constant visit(Sum sum) {
+        Constant left = sum.getLeft().accept(this);
+        Constant right = sum.getRight().accept(this);
+        return new Constant(left.getConstant() + right.getConstant());
+    }
+
+    @Override
+    public Constant visit(Minus minus) {
+        Constant left = minus.getLeft().accept(this);
+        Constant right = minus.getRight().accept(this);
+        return new Constant(left.getConstant() - right.getConstant());
+    }
+
+    @Override
+    public Constant visit(Variable variable) {
+        throw new IllegalArgumentException();
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Minus.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Minus.java
new file mode 100644
index 0000000000..86be49f57c
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Minus.java
@@ -0,0 +1,12 @@
+package org.usvm.samples.ast;
+
+public class Minus extends Binary {
+    public Minus(Ast left, Ast right) {
+        super(left, right);
+    }
+
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Sum.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Sum.java
new file mode 100644
index 0000000000..5218dfe144
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Sum.java
@@ -0,0 +1,12 @@
+package org.usvm.samples.ast;
+
+public class Sum extends Binary {
+    public Sum(Ast left, Ast right) {
+        super(left, right);
+    }
+
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Variable.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Variable.java
new file mode 100644
index 0000000000..2d7b017b5d
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Variable.java
@@ -0,0 +1,14 @@
+package org.usvm.samples.ast;
+
+public class Variable implements Ast {
+    public final int id;
+
+    public Variable(int id) {
+        this.id = id;
+    }
+
+    @Override
+    public <T> T accept(Visitor<T> visitor) {
+        return visitor.visit(this);
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/ast/Visitor.java b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Visitor.java
new file mode 100644
index 0000000000..ec2d1cb5ad
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/ast/Visitor.java
@@ -0,0 +1,11 @@
+package org.usvm.samples.ast;
+
+public interface Visitor<T> {
+    T visit(Constant constant);
+
+    T visit(Sum sum);
+
+    T visit(Minus minus);
+
+    T visit(Variable variable);
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt
index 5d01c681ef..ce7bc81130 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt
@@ -4,6 +4,7 @@ import org.jacodb.api.ext.findClass
 import org.jacodb.api.ext.toType
 import org.junit.jupiter.api.TestInstance
 import org.usvm.CoverageZone
+import org.usvm.PathSelectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.api.JcClassCoverage
 import org.usvm.api.JcParametersState
@@ -717,7 +718,8 @@ open class JavaMethodTestRunner : TestRunner<JcTest, KFunction<*>, KClass<*>?, J
     override val checkType: (KClass<*>?, KClass<*>?) -> Boolean =
         { expected, actual -> actual == null || expected != null && expected.java.isAssignableFrom(actual.java) }
 
-    override var options: UMachineOptions = UMachineOptions().copy(
+    override var options: UMachineOptions = UMachineOptions(
+        pathSelectionStrategies = listOf(PathSelectionStrategy.FORK_DEPTH),
         coverageZone = CoverageZone.TRANSITIVE,
         exceptionsPropagation = true,
         timeoutMs = 60_000,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt
index 9301ca68e2..f0dc22e2bf 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/casts/InstanceOfExampleTest.kt
@@ -51,7 +51,6 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Support virtual calls")
     fun testVirtualCallWithoutOneInheritor() {
         checkDiscoveredProperties(
             InstanceOfExample::virtualCallWithoutOneInheritor,
@@ -64,7 +63,6 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Support virtual calls")
     fun testVirtualCallWithoutOneInheritorInverse() {
         checkDiscoveredProperties(
             InstanceOfExample::virtualCallWithoutOneInheritorInverse,
@@ -98,6 +96,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
 
 
     @Test
+    @Disabled("java.lang.ArrayStoreException: java.lang.Object. Support connection between array and element type")
     fun testInstanceOfAsPartOfInternalExpressions() {
         checkDiscoveredProperties(
             InstanceOfExample::instanceOfAsPartOfInternalExpressions,
@@ -165,7 +164,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     fun testInstanceOfAsPartOfInternalExpressionsXor() {
         checkDiscoveredProperties(
             InstanceOfExample::instanceOfAsPartOfInternalExpressionsXor,
-            eq(5),
+            ge(5),
             { _, o, r -> (o == null || o.size != 2) && r == 0 },
             { _, o, r ->
                 val o0isSecond = o[0].isInstanceOfArray<CastClassSecondSucc>()
@@ -194,7 +193,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     fun testInstanceOfAsPartOfInternalExpressionsXorInverse() {
         checkDiscoveredProperties(
             InstanceOfExample::instanceOfAsPartOfInternalExpressionsXorInverse,
-            eq(5),
+            ge(5),
             { _, o, r -> (o == null || o.size != 2) && r == 0 },
             { _, o, r ->
                 val o0isSecond = o[0].isInstanceOfArray<CastClassSecondSucc>()
@@ -236,7 +235,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("An operation is not implemented: Support collections")
+    @Disabled("An operation is not implemented: Not yet implemented. Support strings/collections")
     fun testInstanceOfAsInternalExpressionsMap() {
         checkDiscoveredProperties(
             InstanceOfExample::instanceOfAsInternalExpressionsMap,
@@ -249,7 +248,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     fun testSymbolicInstanceOf() {
         checkDiscoveredProperties(
             InstanceOfExample::symbolicInstanceOf,
-            eq(5),
+            ge(5),
             { _, _, i, r -> (i < 1 || i > 3) && r == null },
             { _, o, _, _ -> o == null },
             { _, o, i, _ -> o != null && i > o.lastIndex },
@@ -259,7 +258,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Support virtual calls")
+    @Disabled("Some properties were not discovered at positions (from 0): [4]. Support connection between array and element type")
     fun testComplicatedInstanceOf() {
         checkDiscoveredProperties(
             InstanceOfExample::complicatedInstanceOf,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt
index ecf7147a1e..89823df36a 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/deepequals/DeepEqualsTest.kt
@@ -8,6 +8,7 @@ import org.usvm.test.util.checkers.eq
 
 class DeepEqualsTest : JavaMethodTestRunner() {
     @Test
+    @Disabled("An operation is not implemented: Class constant")
     fun testReturnList() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::returnList,
@@ -16,6 +17,7 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("No entrypoint found for method: (id:1)java.lang.Object#hashCode()")
     fun testReturnSet() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::returnSet,
@@ -48,6 +50,7 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("An operation is not implemented: Class constant")
     fun testReturn2DList() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::return2DList,
@@ -56,6 +59,7 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("No entrypoint found for method: (id:1)java.lang.Object#hashCode()")
     fun testReturn2DSet() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::return2DSet,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt
index 2374f010bb..75690ae5ad 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/exceptions/ExceptionExamplesTest.kt
@@ -114,7 +114,6 @@ internal class ExceptionExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Wait for instanceof support")
     fun testSymbolicExceptions() {
         checkDiscoveredProperties(
             ExceptionExamples::symbolicExceptionCheck,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/AstExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/AstExampleTest.kt
new file mode 100644
index 0000000000..7848e365c5
--- /dev/null
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/AstExampleTest.kt
@@ -0,0 +1,21 @@
+package org.usvm.samples.invokes
+
+import org.junit.jupiter.api.Test
+import org.usvm.samples.JavaMethodTestRunner
+import org.usvm.samples.ast.AstExample
+import org.usvm.samples.ast.Constant
+import org.usvm.test.util.checkers.ge
+
+class AstExampleTest : JavaMethodTestRunner() {
+    @Test
+    fun testSubstituteAndEvaluate() {
+        checkDiscoveredPropertiesWithExceptions(
+            AstExample::replaceLeafAndCheck,
+            ge(4),
+            { _, ast, r -> ast == null && r.exceptionOrNull() is NullPointerException },
+            { _, ast, r -> r.getOrNull() == -1 && ast is Constant && AstExample().replaceLeafAndCheck(ast) == -1 },
+            { _, ast, r -> r.getOrNull() == 0 && ast !is Constant && AstExample().replaceLeafAndCheck(ast) == 0 },
+            { _, ast, r -> r.getOrNull() == 1 && AstExample().replaceLeafAndCheck(ast) == 1 },
+        )
+    }
+}
\ No newline at end of file
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt
index f61a6ddeab..3fc26988e5 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/InvokeExampleTest.kt
@@ -65,7 +65,6 @@ internal class InvokeExampleTest : JavaMethodTestRunner() {
 
 
     @Test
-    @Disabled("Expected exactly 3 executions, but 1 found. Tune coverage zone")
     fun testConstraintsFromOutside() {
         checkDiscoveredProperties(
             InvokeExample::constraintsFromOutside,
@@ -104,7 +103,6 @@ internal class InvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Expected exactly 3 executions, but 2 found. Tune coverage zone")
     fun testExceptionInNestedMethod() {
         checkDiscoveredPropertiesWithExceptions(
             InvokeExample::exceptionInNestedMethod,
@@ -116,7 +114,6 @@ internal class InvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [1, 2, 3]. Tune coverage zone")
     fun testFewNestedExceptions() {
         checkDiscoveredPropertiesWithExceptions(
             InvokeExample::fewNestedException,
@@ -165,7 +162,6 @@ internal class InvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Expected exactly 3 executions, but 2 found. Tune coverage zone")
     fun testChangeArrayWithAssignFromMethod() {
         checkDiscoveredProperties(
             InvokeExample::changeArrayWithAssignFromMethod,
@@ -180,7 +176,6 @@ internal class InvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [1]. Tune coverage zone")
     fun testChangeArrayByMethod() {
         checkDiscoveredProperties(
             InvokeExample::changeArrayByMethod,
@@ -191,15 +186,13 @@ internal class InvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [3]. Tune coverage zone")
     fun testArrayCopyExample() {
         checkDiscoveredProperties(
             InvokeExample::arrayCopyExample,
             ignoreNumberOfAnalysisResults,
             { _, a, _ -> a == null },
             { _, a, _ -> a != null && a.size < 3 },
-            { _, a, r -> a != null && a.size >= 3 && a[0] <= a[1] && r == null },
-            { _, a, r -> a != null && a.size >= 3 && a[0] > a[1] && a[1] <= a[2] && r == null },
+            { _, a, r -> a != null && a.size >= 3 && (a[0] <= a[1] || a[1] <= a[2]) && r == null },
             { _, a, r -> a != null && a.size >= 3 && a[0] > a[1] && a[1] > a[2] && r.contentEquals(a) },
         )
     }
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/SimpleInterfaceExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/SimpleInterfaceExampleTest.kt
index 6235a6615c..8091c4b26d 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/SimpleInterfaceExampleTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/SimpleInterfaceExampleTest.kt
@@ -1,6 +1,5 @@
 package org.usvm.samples.invokes
 
-import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
@@ -8,7 +7,6 @@ import org.usvm.test.util.checkers.eq
 
 internal class SimpleInterfaceExampleTest : JavaMethodTestRunner() {
     @Test
-    @Disabled("Expected exactly 3 executions, but 2 found. Virtual invokes are not supported yet")
     fun testOverrideMethod() {
         checkDiscoveredProperties(
             SimpleInterfaceExample::overrideMethod,
@@ -30,7 +28,6 @@ internal class SimpleInterfaceExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Sequence is empty.")
     fun testInvokeMethodFromImplementor() {
         checkDiscoveredProperties(
             SimpleInterfaceExample::invokeMethodFromImplementor,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt
index b18aaf7fa1..fee1e73518 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/invokes/VirtualInvokeExampleTest.kt
@@ -23,6 +23,7 @@ internal class VirtualInvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("An operation is not implemented: Not yet implemented. Support class constants")
     fun testVirtualNative() {
         checkDiscoveredProperties(
             VirtualInvokeExample::virtualNative,
@@ -32,6 +33,7 @@ internal class VirtualInvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("An operation is not implemented: Not yet implemented. Support class constants")
     fun testGetSigners() {
         checkDiscoveredProperties(
             VirtualInvokeExample::virtualNativeArray,
@@ -118,6 +120,7 @@ internal class VirtualInvokeExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("An operation is not implemented: Not yet implemented. Support strings/integer approximations")
     fun testNullValueInReturnValue() {
         checkDiscoveredProperties(
             VirtualInvokeExample::nullValueInReturnValue,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/loops/TestWhile.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/loops/TestWhile.kt
index 0ab7d93f5a..831e9e4a8d 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/loops/TestWhile.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/loops/TestWhile.kt
@@ -1,9 +1,9 @@
 package org.usvm.samples.loops
 
-import org.junit.jupiter.api.RepeatedTest
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
+import org.usvm.test.util.checkers.ge
 import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
 
 class TestWhile : JavaMethodTestRunner() {
@@ -23,7 +23,7 @@ class TestWhile : JavaMethodTestRunner() {
     fun `Test smallestPowerOfTwo`() {
         checkDiscoveredProperties(
             While::smallestPowerOfTwo,
-            eq(3),
+            ge(3),
             { _, n, r -> r == 0 && n.and(n - 1) == 0 },
             { _, n, r -> r == 1 && n <= 0 },
             { _, n, r -> r == 2 && n > 0 && n.and(n - 1) != 0 },
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt
index 6336e79b5c..23a3879e88 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ObjectWithRefFieldsExampleTest.kt
@@ -4,6 +4,7 @@ import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
+import org.usvm.test.util.checkers.ge
 import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
 import org.usvm.util.isException
 
@@ -60,7 +61,7 @@ internal class ObjectWithRefFieldsExampleTest : JavaMethodTestRunner() {
     fun testWriteToArrayField() {
         checkDiscoveredProperties(
             ObjectWithRefFieldExample::writeToArrayField,
-            eq(3),
+            ge(3),
             { _, _, length, _ -> length < 3 },
             { _, o, length, _ -> length >= 3 && o == null },
             { _, o, length, r ->
@@ -89,6 +90,7 @@ internal class ObjectWithRefFieldsExampleTest : JavaMethodTestRunner() {
         )
     }
 
+    @Test
     fun testCompareTwoDifferentObjectsFromArguments() {
         checkDiscoveredProperties(
             ObjectWithRefFieldExample::compareTwoDifferentObjectsFromArguments,
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleExprResolver.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleExprResolver.kt
index 35a40669d1..e41804563e 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleExprResolver.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleExprResolver.kt
@@ -84,14 +84,14 @@ class SampleExprResolver(
     fun resolveStruct(expr: StructExpr): UHeapRef? = with(ctx) {
         when (expr) {
             is StructCreation -> {
-                val ref = scope.calcOnState { memory.alloc(expr.type) } ?: return null
+                val ref = scope.calcOnState { memory.alloc(expr.type) }
 
                 for ((field, fieldExpr) in expr.fields) {
                     val sort = typeToSort(field.type)
                     val fieldRef = UFieldLValue(sort, ref, field)
                     val fieldUExpr = resolveExpr(fieldExpr) ?: return null
 
-                    scope.doWithState { memory.write(fieldRef, fieldUExpr) } ?: return null
+                    scope.doWithState { memory.write(fieldRef, fieldUExpr) }
                 }
 
                 ref
@@ -110,7 +110,7 @@ class SampleExprResolver(
                 val size = resolveInt(expr.size) ?: return null
                 checkArrayLength(size, expr.values.size) ?: return null
 
-                val ref = scope.calcOnState { memory.malloc(expr.type, size) } ?: return null
+                val ref = scope.calcOnState { memory.malloc(expr.type, size) }
 
                 val cellSort = typeToSort(expr.type.elementType)
 
@@ -118,7 +118,7 @@ class SampleExprResolver(
                 values.forEachIndexed { index, kExpr ->
                     val lvalue = UArrayIndexLValue(cellSort, ref, mkBv(index), expr.type)
 
-                    scope.doWithState { memory.write(lvalue, kExpr) } ?: return null
+                    scope.doWithState { memory.write(lvalue, kExpr) }
                 }
 
                 // TODO: memset is not implemented
@@ -140,7 +140,7 @@ class SampleExprResolver(
                 val ref = resolveArray(expr.array) ?: return null
                 checkNullPointer(ref) ?: return null
                 val lengthRef = UArrayLengthLValue(ref, expr.array.type)
-                val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) } ?: return null
+                val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
                 checkHardMaxArrayLength(length) ?: return null
                 scope.assert(mkBvSignedLessOrEqualExpr(mkBv(0), length)) ?: return null
                 length
@@ -300,7 +300,7 @@ class SampleExprResolver(
 
         val idx = resolveInt(index) ?: return null
         val lengthRef = UArrayLengthLValue(arrayRef, array.type)
-        val length = scope.calcOnState { memory.read(lengthRef).asExpr(ctx.sizeSort) } ?: return null
+        val length = scope.calcOnState { memory.read(lengthRef).asExpr(ctx.sizeSort) }
 
         checkHardMaxArrayLength(length) ?: return null