diff --git a/buildSrc/src/main/kotlin/Versions.kt b/buildSrc/src/main/kotlin/Versions.kt
index 8f765786f8..0a2f551ebd 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.7"
     const val collections = "0.3.5"
     const val coroutines = "1.6.4"
-    const val jcdb = "1.2.0"
+    const val jcdb = "1.3.0"
     const val mockk = "1.13.4"
     const val junitParams = "5.9.3"
     const val logback = "1.4.8"
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt
index 7c1126db42..be92d07a6f 100644
--- a/usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/api/EngineApi.kt
@@ -1,14 +1,99 @@
 package org.usvm.api
 
 import org.usvm.UBoolExpr
+import org.usvm.UExpr
 import org.usvm.UHeapRef
+import org.usvm.UNullRef
+import org.usvm.USort
 import org.usvm.UState
+import org.usvm.constraints.UTypeEvaluator
+import org.usvm.memory.mapWithStaticAsConcrete
+import org.usvm.types.UTypeStream
+import org.usvm.types.singleOrNull
+import org.usvm.uctx
 
+fun <Type> UTypeEvaluator<Type>.evalTypeEquals(ref: UHeapRef, type: Type): UBoolExpr =
+    with(ref.uctx) {
+        mkAnd(
+            evalIsSubtype(ref, type),
+            evalIsSupertype(ref, type)
+        )
+    }
 
-fun UState<*, *, *, *, *, *>.assume(expr: UBoolExpr) {
-    pathConstraints += expr
+fun <Type> UState<Type, *, *, *, *, *>.objectTypeEquals(
+    lhs: UHeapRef,
+    rhs: UHeapRef
+): UBoolExpr = with(lhs.uctx) {
+    mapTypeStream(
+        ref = lhs,
+        onNull = {
+            // type(null) = type(null); type(null) <: T /\ T <: type(null) ==> true /\ false
+            mapTypeStream(rhs, onNull = { trueExpr }, { _, _ -> falseExpr })
+        },
+        operation = { lhsRef, lhsTypes ->
+            mapTypeStream(
+                rhs,
+                onNull = { falseExpr },
+                operation = { rhsRef, rhsTypes ->
+                    mkTypeEqualsConstraint(lhsRef, lhsTypes, rhsRef, rhsTypes)
+                }
+            )
+        }
+    )
 }
 
-fun UState<*, *, *, *, *, *>.objectTypeEquals(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr {
-    TODO("Objects types equality check: $lhs, $rhs")
+fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
+    ref: UHeapRef,
+    operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>?
+): UExpr<R>? = mapTypeStream(
+    ref = ref,
+    onNull = { return null },
+    operation = { expr, types ->
+        operation(expr, types) ?: return null
+    }
+)
+
+private fun <Type> UState<Type, *, *, *, *, *>.mkTypeEqualsConstraint(
+    lhs: UHeapRef,
+    lhsTypes: UTypeStream<Type>,
+    rhs: UHeapRef,
+    rhsTypes: UTypeStream<Type>,
+): UBoolExpr = with(lhs.uctx) {
+    val lhsType = lhsTypes.singleOrNull()
+    val rhsType = rhsTypes.singleOrNull()
+
+    if (lhsType != null) {
+        return if (lhsType == rhsType) {
+            trueExpr
+        } else {
+            memory.types.evalTypeEquals(rhs, lhsType)
+        }
+    }
+
+    if (rhsType != null) {
+        return memory.types.evalTypeEquals(lhs, rhsType)
+    }
+
+    // TODO: don't mock type equals
+    makeSymbolicPrimitive(boolSort)
 }
+
+private inline fun <Type, R : USort> UState<Type, *, *, *, *, *>.mapTypeStream(
+    ref: UHeapRef,
+    onNull: () -> UExpr<R>,
+    operation: (UHeapRef, UTypeStream<Type>) -> UExpr<R>
+): UExpr<R> = ref.mapWithStaticAsConcrete(
+    ignoreNullRefs = false,
+    concreteMapper = { concreteRef ->
+        val types = memory.types.getTypeStream(concreteRef)
+        operation(concreteRef, types)
+    },
+    symbolicMapper = { symbolicRef ->
+        if (symbolicRef is UNullRef) {
+            onNull()
+        } else {
+            val types = memory.types.getTypeStream(symbolicRef)
+            operation(symbolicRef, types)
+        }
+    },
+)
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
index fd325abcaa..8cb8c30d29 100644
--- a/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/api/MockApi.kt
@@ -1,8 +1,9 @@
 package org.usvm.api
 
+import org.usvm.StepScope
+import org.usvm.UBoolExpr
 import org.usvm.UExpr
 import org.usvm.UHeapRef
-import org.usvm.USizeExpr
 import org.usvm.USort
 import org.usvm.UState
 import org.usvm.uctx
@@ -16,22 +17,28 @@ fun <Method, T : USort> UState<*, Method, *, *, *, *>.makeSymbolicPrimitive(
     return memory.mock { call(lastEnteredMethod, emptySequence(), sort) }
 }
 
-fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicRef(type: Type): UHeapRef {
-    val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
+fun <Type, Method, State> StepScope<State, Type, *>.makeSymbolicRef(
+    type: Type
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { memory.types.evalTypeEquals(it, type) }
 
-    memory.types.addSubtype(ref, type)
-    memory.types.addSupertype(ref, type)
+fun <Type, Method, State> StepScope<State, Type, *>.makeSymbolicRefWithSameType(
+    representative: UHeapRef
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> =
+    mockSymbolicRef { objectTypeEquals(it, representative) }
 
-    return ref
-}
-
-fun <Type, Method> UState<Type, Method, *, *, *, *>.makeSymbolicArray(arrayType: Type, size: USizeExpr): UHeapRef {
-    val ref = memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
+private inline fun <Type, Method, State> StepScope<State, Type, *>.mockSymbolicRef(
+    crossinline mkTypeConstraint: State.(UHeapRef) -> UBoolExpr
+): UHeapRef? where State : UState<Type, Method, *, *, *, State> {
+    val ref = calcOnState {
+        memory.mock { call(lastEnteredMethod, emptySequence(), memory.ctx.addressSort) }
+    }
 
-    memory.types.addSubtype(ref, arrayType)
-    memory.types.addSupertype(ref, arrayType)
+    val typeConstraint = calcOnState {
+        mkTypeConstraint(ref)
+    }
 
-    memory.writeArrayLength(ref, size, arrayType)
+    assert(typeConstraint) ?: return null
 
     return ref
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
index b183bd510c..7f213fb061 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
@@ -16,7 +16,17 @@ import org.usvm.types.UTypeSystem
 import org.usvm.uctx
 
 interface UTypeEvaluator<Type> {
+
+    /**
+     * Check that [ref] = `null` or type([ref]) <: [supertype].
+     * Note that T <: T always holds.
+     * */
     fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr
+
+    /**
+     * Check that [ref] != `null` and [subtype] <: type([ref]).
+     * Note that T <: T always holds.
+     * */
     fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr
     fun getTypeStream(ref: UHeapRef): UTypeStream<Type>
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt b/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt
index cfac8b5d60..216d392836 100644
--- a/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/types/TypeStream.kt
@@ -75,6 +75,11 @@ fun <Type> UTypeStream<Type>.first(): Type = take(1).first()
 
 fun <Type> UTypeStream<Type>.firstOrNull(): Type? = take(1).firstOrNull()
 
+// Note: we try to take at least two types to ensure that we don't have no more than one type.
+fun <Type> UTypeStream<Type>.single(): Type = take(2).single()
+
+fun <Type> UTypeStream<Type>.singleOrNull(): Type? = take(2).singleOrNull()
+
 /**
  * Consists of just one type [singleType].
  */
diff --git a/usvm-jvm/build.gradle.kts b/usvm-jvm/build.gradle.kts
index 0ce6f013a4..2baf1a5e68 100644
--- a/usvm-jvm/build.gradle.kts
+++ b/usvm-jvm/build.gradle.kts
@@ -2,12 +2,32 @@ plugins {
     id("usvm.kotlin-conventions")
 }
 
+val samples by sourceSets.creating {
+    java {
+        srcDir("src/samples/java")
+    }
+}
+
+val `usvm-api` by sourceSets.creating {
+    java {
+        srcDir("src/usvm-api/java")
+    }
+}
+
+val approximations by configurations.creating
+val approximationsRepo = "com.github.UnitTestBot.java-stdlib-approximations"
+val approximationsVersion = "53ceeb23ea"
+
 dependencies {
     implementation(project(":usvm-core"))
 
     implementation("org.jacodb:jacodb-core:${Versions.jcdb}")
     implementation("org.jacodb:jacodb-analysis:${Versions.jcdb}")
 
+    implementation("org.jacodb:jacodb-approximations:${Versions.jcdb}")
+
+    implementation(`usvm-api`.output)
+
     implementation("io.ksmt:ksmt-yices:${Versions.ksmt}")
     implementation("io.ksmt:ksmt-cvc5:${Versions.ksmt}")
     implementation("io.ksmt:ksmt-symfpu:${Versions.ksmt}")
@@ -16,22 +36,14 @@ dependencies {
     testImplementation("org.junit.jupiter:junit-jupiter-params:${Versions.junitParams}")
     testImplementation("ch.qos.logback:logback-classic:${Versions.logback}")
 
+    testImplementation(samples.output)
+
     // https://mvnrepository.com/artifact/org.burningwave/core
     // Use it to export all modules to all
     testImplementation("org.burningwave:core:12.62.7")
-}
-
-sourceSets {
-    val samples by creating {
-        java {
-            srcDir("src/samples/java")
-        }
-    }
 
-    test {
-        compileClasspath += samples.output
-        runtimeClasspath += samples.output
-    }
+    approximations(approximationsRepo, "approximations", approximationsVersion)
+    testImplementation(approximationsRepo, "tests", approximationsVersion)
 }
 
 val samplesImplementation: Configuration by configurations.getting
@@ -43,3 +55,18 @@ dependencies {
     samplesImplementation("com.github.stephenc.findbugs:findbugs-annotations:${Versions.samplesFindBugs}")
     samplesImplementation("org.jetbrains:annotations:${Versions.samplesJetbrainsAnnotations}")
 }
+
+val `usvm-api-jar` = tasks.register<Jar>("usvm-api-jar") {
+    archiveBaseName.set(`usvm-api`.name)
+    from(`usvm-api`.output)
+}
+
+tasks.withType<Test> {
+    dependsOn(`usvm-api-jar`)
+
+    val usvmApiJarPath = `usvm-api-jar`.get().outputs.files.singleFile
+    val usvmApproximationJarPath = approximations.resolvedConfiguration.files.single()
+
+    environment("usvm.jvm.api.jar.path", usvmApiJarPath.absolutePath)
+    environment("usvm.jvm.approximations.jar.path", usvmApproximationJarPath.absolutePath)
+}
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
index 7ab46177b9..36d6b8490a 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
@@ -4,10 +4,12 @@ import io.ksmt.utils.asExpr
 import io.ksmt.utils.uncheckedCast
 import org.jacodb.api.JcArrayType
 import org.jacodb.api.JcMethod
+import org.jacodb.api.JcType
 import org.jacodb.api.ext.boolean
 import org.jacodb.api.ext.byte
 import org.jacodb.api.ext.char
 import org.jacodb.api.ext.double
+import org.jacodb.api.ext.findClassOrNull
 import org.jacodb.api.ext.float
 import org.jacodb.api.ext.ifArrayGetElementType
 import org.jacodb.api.ext.int
@@ -15,6 +17,7 @@ import org.jacodb.api.ext.long
 import org.jacodb.api.ext.objectClass
 import org.jacodb.api.ext.objectType
 import org.jacodb.api.ext.short
+import org.jacodb.api.ext.toType
 import org.jacodb.api.ext.void
 import org.usvm.UBoolExpr
 import org.usvm.UBv32Sort
@@ -24,26 +27,76 @@ import org.usvm.UExpr
 import org.usvm.UFpSort
 import org.usvm.UHeapRef
 import org.usvm.USizeExpr
-import org.usvm.USymbolicHeapRef
+import org.usvm.api.Engine
+import org.usvm.api.SymbolicList
+import org.usvm.api.SymbolicMap
+import org.usvm.api.collection.ListCollectionApi.ensureListSizeCorrect
+import org.usvm.api.collection.ListCollectionApi.mkSymbolicList
+import org.usvm.api.collection.ListCollectionApi.symbolicListCopyRange
+import org.usvm.api.collection.ListCollectionApi.symbolicListGet
+import org.usvm.api.collection.ListCollectionApi.symbolicListInsert
+import org.usvm.api.collection.ListCollectionApi.symbolicListRemove
+import org.usvm.api.collection.ListCollectionApi.symbolicListSet
+import org.usvm.api.collection.ListCollectionApi.symbolicListSize
+import org.usvm.api.collection.ObjectMapCollectionApi.ensureObjectMapSizeCorrect
+import org.usvm.api.collection.ObjectMapCollectionApi.mkSymbolicObjectMap
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapContains
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapGet
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapMergeInto
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapPut
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapRemove
+import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapSize
+import org.usvm.api.makeSymbolicPrimitive
+import org.usvm.api.makeSymbolicRef
+import org.usvm.api.makeSymbolicRefWithSameType
+import org.usvm.api.mapTypeStream
 import org.usvm.api.memcpy
-import org.usvm.api.typeStreamOf
+import org.usvm.api.objectTypeEquals
 import org.usvm.collection.array.length.UArrayLengthLValue
+import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.interpreter.JcExprResolver
 import org.usvm.machine.interpreter.JcStepScope
 import org.usvm.machine.state.JcState
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.skipMethodInvocationWithValue
+import org.usvm.types.first
+import org.usvm.types.single
+import org.usvm.types.singleOrNull
 import org.usvm.uctx
 import org.usvm.util.allocHeapRef
 import org.usvm.util.write
+import kotlin.reflect.KFunction
+import kotlin.reflect.KFunction0
+import kotlin.reflect.KFunction1
+import kotlin.reflect.KFunction2
+import kotlin.reflect.jvm.javaMethod
 
 class JcMethodApproximationResolver(
     private val ctx: JcContext,
-    private val scope: JcStepScope,
     private val applicationGraph: JcApplicationGraph,
-    private val exprResolver: JcExprResolver
 ) {
-    fun approximate(callJcInst: JcMethodCall): Boolean {
+    private var currentScope: JcStepScope? = null
+    private val scope: JcStepScope
+        get() = checkNotNull(currentScope)
+
+    private var currentExprResolver: JcExprResolver? = null
+    private val exprResolver: JcExprResolver
+        get() = checkNotNull(currentExprResolver)
+
+    private val usvmApiEngine by lazy { ctx.cp.findClassOrNull<Engine>() }
+    private val usvmApiSymbolicList by lazy { ctx.cp.findClassOrNull<SymbolicList<*>>() }
+    private val usvmApiSymbolicMap by lazy { ctx.cp.findClassOrNull<SymbolicMap<*, *>>() }
+
+    fun approximate(scope: JcStepScope, exprResolver: JcExprResolver, callJcInst: JcMethodCall): Boolean = try {
+        this.currentScope = scope
+        this.currentExprResolver = exprResolver
+        approximate(callJcInst)
+    } finally {
+        this.currentScope = null
+        this.currentExprResolver = null
+    }
+
+    private fun approximate(callJcInst: JcMethodCall): Boolean {
         if (skipMethodIfThrowable(callJcInst)) {
             return true
         }
@@ -56,6 +109,16 @@ class JcMethodApproximationResolver(
     }
 
     private fun approximateRegularMethod(methodCall: JcMethodCall): Boolean = with(methodCall) {
+        if (method.enclosingClass == usvmApiSymbolicList) {
+            approximateUsvmSymbolicListMethod(methodCall)
+            return true
+        }
+
+        if (method.enclosingClass == usvmApiSymbolicMap) {
+            approximateUsvmSymbolicMapMethod(methodCall)
+            return true
+        }
+
         if (method.enclosingClass == ctx.cp.objectClass) {
             if (approximateObjectVirtualMethod(methodCall)) return true
         }
@@ -76,6 +139,11 @@ class JcMethodApproximationResolver(
     }
 
     private fun approximateStaticMethod(methodCall: JcMethodCall): Boolean = with(methodCall) {
+        if (method.enclosingClass == usvmApiEngine) {
+            approximateUsvmApiEngineStaticMethod(methodCall)
+            return true
+        }
+
         if (method.enclosingClass == ctx.classType.jcClass) {
             if (approximateClassStaticMethod(methodCall)) return true
         }
@@ -159,20 +227,13 @@ class JcMethodApproximationResolver(
         if (method.name == "getClass") {
             val instance = arguments.first().asExpr(ctx.addressSort)
 
-            // Type constraints can't provide types for other refs
-            if (instance !is UConcreteHeapRef && instance !is USymbolicHeapRef) {
-                return false
-            }
-
-            val possibleTypes = scope.calcOnState { memory.typeStreamOf(instance).take(2) }
-
-            /**
-             * Since getClass is a virtual method, typeStream has been constrained
-             * to a single concrete type by the [JcInterpreter.resolveVirtualInvoke]
-             * */
-            val type = possibleTypes.singleOrNull() ?: return false
+            val result = scope.calcOnState {
+                mapTypeStream(instance) { _, types ->
+                    val type = types.singleOrNull()
+                    type?.let { exprResolver.resolveClassRef(it) }
+                }
+            } ?: return false
 
-            val result = exprResolver.resolveClassRef(type)
             scope.doWithState {
                 skipMethodInvocationWithValue(methodCall, result)
             }
@@ -290,7 +351,7 @@ class JcMethodApproximationResolver(
         }
 
         val arrayType = scope.calcOnState {
-            (memory.types.getTypeStream(instance).take(2).single())
+            (memory.types.getTypeStream(instance).single())
         }
         if (arrayType !is JcArrayType) {
             return false
@@ -468,4 +529,304 @@ class JcMethodApproximationResolver(
 
     private fun JcMethod.hasVoidReturnType(): Boolean =
         returnType.typeName == ctx.cp.void.typeName
+
+    private val symbolicListType: JcType by lazy {
+        checkNotNull(usvmApiSymbolicList).toType()
+    }
+
+    private val symbolicMapType: JcType by lazy {
+        checkNotNull(usvmApiSymbolicMap).toType()
+    }
+
+    private val usvmApiEngineMethods: Map<String, (JcMethodCall) -> UExpr<*>?> by lazy {
+        buildMap {
+            dispatchUsvmApiMethod(Engine::assume) {
+                val arg = it.arguments.single().asExpr(ctx.booleanSort)
+                scope.assert(arg)?.let { ctx.voidValue }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicBoolean) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.booleanSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicByte) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.byteSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicChar) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.charSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicShort) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.shortSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicInt) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.integerSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicLong) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.longSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicFloat) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.floatSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicDouble) {
+                scope.calcOnState { makeSymbolicPrimitive(ctx.doubleSort) }
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicBooleanArray) {
+                makeSymbolicArray(ctx.cp.boolean, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicByteArray) {
+                makeSymbolicArray(ctx.cp.byte, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicCharArray) {
+                makeSymbolicArray(ctx.cp.char, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicShortArray) {
+                makeSymbolicArray(ctx.cp.short, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicIntArray) {
+                makeSymbolicArray(ctx.cp.int, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicLongArray) {
+                makeSymbolicArray(ctx.cp.long, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicFloatArray) {
+                makeSymbolicArray(ctx.cp.float, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::makeSymbolicDoubleArray) {
+                makeSymbolicArray(ctx.cp.double, it.arguments.single())
+            }
+            dispatchUsvmApiMethod(Engine::typeEquals) {
+                val (ref0, ref1) = it.arguments.map { it.asExpr(ctx.addressSort) }
+                scope.calcOnState { objectTypeEquals(ref0, ref1) }
+            }
+            dispatchMkRef(Engine::makeSymbolic) {
+                val classRef = it.arguments.single().asExpr(ctx.addressSort)
+                val classRefTypeRepresentative = scope.calcOnState {
+                    memory.read(UFieldLValue(ctx.addressSort, classRef, ctx.classTypeSyntheticField))
+                }
+                scope.makeSymbolicRefWithSameType(classRefTypeRepresentative)
+            }
+            dispatchMkRef2(Engine::makeSymbolicArray) {
+                val (elementClassRefExpr, sizeExpr) = it.arguments
+                val elementClassRef = elementClassRefExpr.asExpr(ctx.addressSort)
+                val elementTypeRepresentative = scope.calcOnState {
+                    memory.read(UFieldLValue(ctx.addressSort, elementClassRef, ctx.classTypeSyntheticField))
+                }
+
+                if (elementTypeRepresentative is UConcreteHeapRef) {
+                    val type = scope.calcOnState { memory.types.getTypeStream(elementTypeRepresentative).first() }
+                    makeSymbolicArray(type, sizeExpr)
+                } else {
+                    // todo: correct type instead of object
+                    makeSymbolicArray(ctx.cp.objectType, sizeExpr)
+                }
+            }
+            dispatchMkList(Engine::makeSymbolicList) {
+                scope.calcOnState { mkSymbolicList(symbolicListType) }
+            }
+            dispatchMkMap(Engine::makeSymbolicMap) {
+                scope.calcOnState { mkSymbolicObjectMap(symbolicMapType) }
+            }
+        }
+    }
+
+    private val usvmApiListMethods: Map<String, (JcMethodCall) -> UExpr<*>?> by lazy {
+        buildMap {
+            dispatchUsvmApiMethod(SymbolicList<*>::size) {
+                val listRef = it.arguments.single().asExpr(ctx.addressSort)
+                scope.ensureListSizeCorrect(listRef, symbolicListType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicListSize(listRef, symbolicListType)
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicList<*>::get) {
+                val (rawListRef, rawIdx) = it.arguments
+                val listRef = rawListRef.asExpr(ctx.addressSort)
+                val idx = rawIdx.asExpr(ctx.sizeSort)
+
+                scope.ensureListSizeCorrect(listRef, symbolicListType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicListGet(listRef, idx, symbolicListType, ctx.addressSort)
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicList<*>::set) {
+                val (rawListRef, rawIdx, rawValueRef) = it.arguments
+                val listRef = rawListRef.asExpr(ctx.addressSort)
+                val idx = rawIdx.asExpr(ctx.sizeSort)
+                val valueRef = rawValueRef.asExpr(ctx.addressSort)
+
+                scope.ensureListSizeCorrect(listRef, symbolicListType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicListSet(listRef, symbolicListType, ctx.addressSort, idx, valueRef)
+                    ctx.voidValue
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicList<*>::insert) {
+                val (rawListRef, rawIdx, rawValueRef) = it.arguments
+                val listRef = rawListRef.asExpr(ctx.addressSort)
+                val idx = rawIdx.asExpr(ctx.sizeSort)
+                val valueRef = rawValueRef.asExpr(ctx.addressSort)
+
+                scope.ensureListSizeCorrect(listRef, symbolicListType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicListInsert(listRef, symbolicListType, ctx.addressSort, idx, valueRef)
+                    ctx.voidValue
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicList<*>::remove) {
+                val (rawListRef, rawIdx) = it.arguments
+                val listRef = rawListRef.asExpr(ctx.addressSort)
+                val idx = rawIdx.asExpr(ctx.sizeSort)
+
+                scope.ensureListSizeCorrect(listRef, symbolicListType) ?: return@dispatchUsvmApiMethod null
+
+                val result = scope.calcOnState {
+                    symbolicListRemove(listRef, symbolicListType, ctx.addressSort, idx)
+                    ctx.voidValue
+                }
+
+                scope.ensureListSizeCorrect(listRef, symbolicListType) ?: return@dispatchUsvmApiMethod null
+
+                result
+            }
+            dispatchUsvmApiMethod(SymbolicList<*>::copy) {
+                val (listRef, dstListRef, srcFromIdx, dstFromIdx, length) = it.arguments
+
+                scope.ensureListSizeCorrect(listRef.asExpr(ctx.addressSort), symbolicListType)
+                    ?: return@dispatchUsvmApiMethod null
+
+                scope.calcOnState {
+                    symbolicListCopyRange(
+                        srcRef = listRef.asExpr(ctx.addressSort),
+                        dstRef = dstListRef.asExpr(ctx.addressSort),
+                        listType = symbolicListType,
+                        sort = ctx.addressSort,
+                        srcFrom = srcFromIdx.asExpr(ctx.sizeSort),
+                        dstFrom = dstFromIdx.asExpr(ctx.sizeSort),
+                        length = length.asExpr(ctx.sizeSort),
+                    )
+                    ctx.voidValue
+                }
+            }
+        }
+    }
+
+    private val usvmApiMapMethods: Map<String, (JcMethodCall) -> UExpr<*>?> by lazy {
+        buildMap {
+            dispatchUsvmApiMethod(SymbolicMap<*, *>::size) {
+                val mapRef = it.arguments.single().asExpr(ctx.addressSort)
+                scope.ensureObjectMapSizeCorrect(mapRef, symbolicMapType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicObjectMapSize(mapRef, symbolicMapType)
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicMap<*, *>::get) {
+                val (mapRef, keyRef) = it.arguments.map { it.asExpr(ctx.addressSort) }
+
+                scope.ensureObjectMapSizeCorrect(mapRef, symbolicMapType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicObjectMapGet(mapRef, keyRef, symbolicMapType, ctx.addressSort)
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicMap<*, *>::set) {
+                val (mapRef, keyRef, valueRef) = it.arguments.map { it.asExpr(ctx.addressSort) }
+
+                scope.ensureObjectMapSizeCorrect(mapRef, symbolicMapType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicObjectMapPut(mapRef, keyRef, valueRef, symbolicMapType, ctx.addressSort)
+                    ctx.voidValue
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicMap<*, *>::remove) {
+                val (mapRef, keyRef) = it.arguments.map { it.asExpr(ctx.addressSort) }
+
+                scope.ensureObjectMapSizeCorrect(mapRef, symbolicMapType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicObjectMapRemove(mapRef, keyRef, symbolicMapType)
+                    ctx.voidValue
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicMap<*, *>::containsKey) {
+                val (mapRef, keyRef) = it.arguments.map { it.asExpr(ctx.addressSort) }
+
+                scope.ensureObjectMapSizeCorrect(mapRef, symbolicMapType) ?: return@dispatchUsvmApiMethod null
+                scope.calcOnState {
+                    symbolicObjectMapContains(mapRef, keyRef, symbolicMapType)
+                }
+            }
+            dispatchUsvmApiMethod(SymbolicMap<*, *>::merge) {
+                val (dstMapRef, srcMapRef) = it.arguments.map { it.asExpr(ctx.addressSort) }
+
+                scope.ensureObjectMapSizeCorrect(dstMapRef, symbolicMapType) ?: return@dispatchUsvmApiMethod null
+                scope.ensureObjectMapSizeCorrect(srcMapRef, symbolicMapType) ?: return@dispatchUsvmApiMethod null
+
+                scope.calcOnState {
+                    symbolicObjectMapMergeInto(dstMapRef, srcMapRef, symbolicMapType, ctx.addressSort)
+                    ctx.voidValue
+                }
+            }
+        }
+    }
+
+    private fun approximateUsvmApiEngineStaticMethod(methodCall: JcMethodCall) {
+        val methodApproximation = usvmApiEngineMethods[methodCall.method.name]
+            ?: error("Unexpected engine api method: ${methodCall.method.name}")
+        val result = methodApproximation(methodCall) ?: return
+        scope.doWithState { skipMethodInvocationWithValue(methodCall, result) }
+    }
+
+    private fun approximateUsvmSymbolicListMethod(methodCall: JcMethodCall) {
+        val methodApproximation = usvmApiListMethods[methodCall.method.name]
+            ?: error("Unexpected list api method: ${methodCall.method.name}")
+        val result = methodApproximation(methodCall) ?: return
+        scope.doWithState { skipMethodInvocationWithValue(methodCall, result) }
+    }
+
+    private fun approximateUsvmSymbolicMapMethod(methodCall: JcMethodCall) {
+        val methodApproximation = usvmApiMapMethods[methodCall.method.name]
+            ?: error("Unexpected map api method: ${methodCall.method.name}")
+        val result = methodApproximation(methodCall) ?: return
+        scope.doWithState { skipMethodInvocationWithValue(methodCall, result) }
+    }
+
+    private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchUsvmApiMethod(
+        apiMethod: KFunction<*>,
+        body: (JcMethodCall) -> UExpr<*>?
+    ) {
+        val methodName = apiMethod.javaMethod?.name
+            ?: error("No name for $apiMethod")
+        this[methodName] = body
+    }
+
+    private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkRef(
+        apiMethod: KFunction1<Nothing, Any>,
+        body: (JcMethodCall) -> UExpr<*>?
+    ) = dispatchUsvmApiMethod(apiMethod, body)
+
+    private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkRef2(
+        apiMethod: KFunction2<Nothing, Nothing, Array<Any>>,
+        body: (JcMethodCall) -> UExpr<*>?
+    ) = dispatchUsvmApiMethod(apiMethod, body)
+
+    private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkList(
+        apiMethod: KFunction0<SymbolicList<Any>>,
+        body: (JcMethodCall) -> UExpr<*>?
+    ) = dispatchUsvmApiMethod(apiMethod, body)
+
+    private fun MutableMap<String, (JcMethodCall) -> UExpr<*>?>.dispatchMkMap(
+        apiMethod: KFunction0<SymbolicMap<Any, Any>>,
+        body: (JcMethodCall) -> UExpr<*>?
+    ) = dispatchUsvmApiMethod(apiMethod, body)
+
+    private fun makeSymbolicArray(elementType: JcType, size: UExpr<*>): UHeapRef? {
+        val sizeValue = size.asExpr(ctx.sizeSort)
+        val arrayType = ctx.cp.arrayTypeOf(elementType)
+
+        val address = scope.makeSymbolicRef(arrayType) ?: return null
+
+        val arrayDescriptor = ctx.arrayDescriptorOf(arrayType)
+        val lengthRef = UArrayLengthLValue(address, arrayDescriptor)
+        scope.doWithState {
+            memory.write(lengthRef, sizeValue)
+        }
+
+        return address
+    }
 }
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
index 5e6f15c3b9..200ee7c494 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcInterpreter.kt
@@ -38,6 +38,7 @@ import org.usvm.UHeapRef
 import org.usvm.UInterpreter
 import org.usvm.api.allocateStaticRef
 import org.usvm.api.targets.JcTarget
+import org.usvm.api.evalTypeEquals
 import org.usvm.api.typeStreamOf
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.isStaticHeapRef
@@ -467,15 +468,12 @@ class JcInterpreter(
 
         val typeStream = scope.calcOnState { models.first().typeStreamOf(concreteRef) }
 
-        val inheritors = typeSelector.choose(method, typeStream)
-        val typeConstraints = inheritors.map { type ->
-            scope.calcOnState {
-                ctx.mkAnd(
-                    memory.types.evalIsSubtype(instance, type),
-                    memory.types.evalIsSupertype(instance, type)
-                )
+            val inheritors = typeSelector.choose(method, typeStream)
+            val typeConstraints = inheritors.map { type ->
+                scope.calcOnState {
+                    memory.types.evalTypeEquals(instance, type)
+                }
             }
-        }
 
         val typeConstraintsWithBlockOnStates = mutableListOf<Pair<UBoolExpr, (JcState) -> Unit>>()
 
@@ -501,12 +499,11 @@ class JcInterpreter(
         scope.forkMulti(typeConstraintsWithBlockOnStates)
     }
 
+    private val approximationResolver = JcMethodApproximationResolver(ctx, applicationGraph)
+
     private fun approximateMethod(scope: JcStepScope, methodCall: JcMethodCall): Boolean {
         val exprResolver = exprResolverWithScope(scope)
-        val methodApproximationResolver = JcMethodApproximationResolver(
-            ctx, scope, applicationGraph, exprResolver
-        )
-        return methodApproximationResolver.approximate(methodCall)
+        return approximationResolver.approximate(scope, exprResolver, methodCall)
     }
 
     private fun mockNativeMethod(
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/util/JcApproximationUtils.kt b/usvm-jvm/src/main/kotlin/org/usvm/util/JcApproximationUtils.kt
new file mode 100644
index 0000000000..8f9496a61b
--- /dev/null
+++ b/usvm-jvm/src/main/kotlin/org/usvm/util/JcApproximationUtils.kt
@@ -0,0 +1,25 @@
+package org.usvm.util
+
+import org.jacodb.api.JcClasspath
+import org.jacodb.api.JcDatabase
+import org.jacodb.approximation.Approximations
+import org.usvm.machine.logger
+import java.io.File
+
+private const val USVM_API_JAR_PATH = "usvm.jvm.api.jar.path"
+private const val USVM_APPROXIMATIONS_JAR_PATH = "usvm.jvm.approximations.jar.path"
+
+suspend fun JcDatabase.classpathWithApproximations(dirOrJars: List<File>): JcClasspath {
+    val usvmApiJarPath = System.getenv(USVM_API_JAR_PATH)
+    val usvmApproximationsJarPath = System.getenv(USVM_APPROXIMATIONS_JAR_PATH)
+
+    if (usvmApiJarPath == null || usvmApproximationsJarPath == null) {
+        return classpath(dirOrJars)
+    }
+
+    logger.info { "Load USVM API: $usvmApiJarPath" }
+    logger.info { "Load USVM Approximations: $usvmApproximationsJarPath" }
+
+    val cpWithApproximations = dirOrJars + listOf(File(usvmApiJarPath), File(usvmApproximationsJarPath))
+    return classpath(cpWithApproximations, listOf(Approximations))
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/approximations/ApproximationsExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/approximations/ApproximationsExample.java
new file mode 100644
index 0000000000..f6143c273e
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/approximations/ApproximationsExample.java
@@ -0,0 +1,92 @@
+package org.usvm.samples.approximations;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.OptionalDouble;
+
+public class ApproximationsExample {
+    public int modifyList(int execution) {
+        List<Object> list = new ArrayList<>();
+        if (execution == 0) {
+            // IOB
+            if (list.get(5) == null) {
+                return -1;
+            }
+        }
+
+        Object stub = new Object();
+        for (int i = 0; i < 3; i++) {
+            list.add(new Object());
+        }
+
+        if (execution == 1) {
+            if (list.size() == 3) {
+                return 1;
+            } else {
+                return -1;
+            }
+        }
+
+        list.add(0, stub);
+        list.add(stub);
+
+        if (execution == 2) {
+            if (list.size() == 5) {
+                return 2;
+            } else {
+                return -1;
+            }
+        }
+
+        if (execution == 3) {
+            if (list.get(0) == list.get(list.size() - 1)) {
+                return 3;
+            } else {
+                return -1;
+            }
+        }
+
+        if (execution == 4) {
+            if (list.get(0) != list.get(1)) {
+                return 4;
+            } else {
+                return -1;
+            }
+        }
+
+        return 0;
+    }
+
+    public int testOptionalDouble(int execution) {
+        double value = 3.0;
+        OptionalDouble od = OptionalDouble.of(value);
+
+        if (execution == 0) {
+            if (od.isPresent()) {
+                return 0;
+            } else {
+                return -1;
+            }
+        }
+
+        if (execution == 1) {
+            if (od.getAsDouble() == value) {
+                return 1;
+            } else {
+                return -1;
+            }
+        }
+
+        OptionalDouble e = OptionalDouble.empty();
+
+        if (execution == 2) {
+            if (!e.isPresent()) {
+                return 2;
+            } else {
+                return -1;
+            }
+        }
+
+        return 0;
+    }
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/JacoDBContainer.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/JacoDBContainer.kt
index d21e7b1159..10b5415a60 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/JacoDBContainer.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/JacoDBContainer.kt
@@ -3,13 +3,16 @@ package org.usvm.samples
 import kotlinx.coroutines.runBlocking
 import org.jacodb.api.JcClasspath
 import org.jacodb.api.JcDatabase
+import org.jacodb.approximation.Approximations
 import org.jacodb.impl.JcSettings
 import org.jacodb.impl.features.InMemoryHierarchy
 import org.jacodb.impl.jacodb
 import org.usvm.util.allClasspath
+import org.usvm.util.classpathWithApproximations
 import java.io.File
 
 class JacoDBContainer(
+    key: Any?,
     classpath: List<File>,
     builder: JcSettings.() -> Unit,
 ) {
@@ -19,7 +22,12 @@ class JacoDBContainer(
     init {
         val (db, cp) = runBlocking {
             val db = jacodb(builder)
-            db to db.classpath(classpath)
+            val cp = if (samplesWithApproximationsKey == key) {
+                db.classpathWithApproximations(classpath)
+            } else {
+                db.classpath(classpath)
+            }
+            db to cp
         }
         this.db = db
         this.cp = cp
@@ -36,16 +44,19 @@ class JacoDBContainer(
             classpath: List<File> = samplesClasspath,
             builder: JcSettings.() -> Unit = defaultBuilder,
         ): JacoDBContainer =
-            keyToJacoDBContainer.getOrPut(key) { JacoDBContainer(classpath, builder) }
+            keyToJacoDBContainer.getOrPut(key) { JacoDBContainer(key, classpath, builder) }
 
-        private val samplesClasspath = allClasspath.filter { it.name.contains("samples") }
+        private val samplesClasspath = allClasspath.filter {
+            it.name.contains("samples") || it.name.contains("tests")
+        }
 
         private val defaultBuilder: JcSettings.() -> Unit = {
             useProcessJavaRuntime()
-            installFeatures(InMemoryHierarchy)
+            installFeatures(InMemoryHierarchy, Approximations)
             loadByteCode(samplesClasspath)
         }
     }
 }
 
-const val samplesKey = "tests"
\ No newline at end of file
+const val samplesKey = "tests"
+const val samplesWithApproximationsKey = "samplesWithApproximations"
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 bdd691376e..67a8ece40a 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/JavaMethodTestRunner.kt
@@ -726,7 +726,8 @@ open class JavaMethodTestRunner : TestRunner<JcTest, KFunction<*>, KClass<*>?, J
         return values
     }
 
-    protected val cp = JacoDBContainer(samplesKey).cp
+    protected open val jacodbCpKey = samplesKey
+    protected val cp = JacoDBContainer(jacodbCpKey).cp
 
     private val testResolver = JcTestResolver()
 
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsExampleTest.kt
new file mode 100644
index 0000000000..dcef9548f7
--- /dev/null
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsExampleTest.kt
@@ -0,0 +1,38 @@
+package org.usvm.samples.approximations
+
+import org.junit.jupiter.api.Test
+import org.usvm.test.util.checkers.eq
+import org.usvm.util.isException
+
+class ApproximationsExampleTest : ApproximationsTestRunner() {
+
+    @Test
+    fun testArrayListModification() {
+        checkDiscoveredPropertiesWithExceptions(
+            ApproximationsExample::modifyList,
+            eq(6),
+            { _, o, r -> o == 0 && r.isException<IndexOutOfBoundsException>() },
+            { _, o, _ -> o == 1 },
+            { _, o, _ -> o == 2 },
+            { _, o, _ -> o == 3 },
+            { _, o, _ -> o == 4 },
+            invariants = arrayOf(
+                { _, execution, r -> execution !in 1..4 || r.getOrThrow() == execution }
+            )
+        )
+    }
+
+    @Test
+    fun testOptionalDouble() {
+        checkDiscoveredPropertiesWithExceptions(
+            ApproximationsExample::testOptionalDouble,
+            eq(4),
+            { _, o, _ -> o == 0 },
+            { _, o, _ -> o == 1 },
+            { _, o, _ -> o == 2 },
+            invariants = arrayOf(
+                { _, execution, r -> execution !in 0..2 || r.getOrThrow() == execution }
+            )
+        )
+    }
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTest.kt
new file mode 100644
index 0000000000..382deeb16a
--- /dev/null
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTest.kt
@@ -0,0 +1,36 @@
+package org.usvm.samples.approximations
+
+import approximations.java.util.ArrayList_Tests
+import approximations.java.util.OptionalDouble_Tests
+import org.junit.jupiter.api.Test
+import org.usvm.test.util.checkers.eq
+import org.usvm.util.isException
+
+class ApproximationsTest : ApproximationsTestRunner() {
+    @Test
+    fun testOptionalDouble() {
+        checkDiscoveredPropertiesWithExceptions(
+            OptionalDouble_Tests::test_of_0,
+            eq(1),
+            invariants = arrayOf(
+                { execution, r -> r.getOrThrow() == execution }
+            )
+        )
+    }
+
+    @Test
+    fun testArrayList() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayList_Tests::test_get_0,
+            eq(6),
+            { o, r -> o == 0 && r.isException<IndexOutOfBoundsException>() },
+            { o, _ -> o == 1 },
+            { o, _ -> o == 2 },
+            { o, _ -> o == 3 },
+            { o, _ -> o == 4 },
+            invariants = arrayOf(
+                { execution, r -> execution !in 1..4 || r.getOrThrow() == execution }
+            )
+        )
+    }
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTestRunner.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTestRunner.kt
new file mode 100644
index 0000000000..409309d956
--- /dev/null
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ApproximationsTestRunner.kt
@@ -0,0 +1,9 @@
+package org.usvm.samples.approximations
+
+import org.usvm.samples.JavaMethodTestRunner
+import org.usvm.samples.samplesWithApproximationsKey
+
+abstract class ApproximationsTestRunner : JavaMethodTestRunner() {
+    override val jacodbCpKey: String
+        get() = samplesWithApproximationsKey
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ArrayListSpliteratorApproximationsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ArrayListSpliteratorApproximationsTest.kt
new file mode 100644
index 0000000000..0619f2f21f
--- /dev/null
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/approximations/ArrayListSpliteratorApproximationsTest.kt
@@ -0,0 +1,102 @@
+package org.usvm.samples.approximations
+
+import approximations.java.util.ArrayListSpliterator_Tests
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.Test
+import org.usvm.test.util.checkers.eq
+
+class ArrayListSpliteratorApproximationsTest : ApproximationsTestRunner() {
+    @Test
+    fun testCharacteristics() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayListSpliterator_Tests::test_characteristics_0,
+            eq(2),
+            { o, _ -> o == 0 },
+            invariants = arrayOf(
+                { o, r -> o != 0 || r.getOrThrow() == 0 }
+            )
+        )
+    }
+
+    @Test
+    fun testEstimateSize() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayListSpliterator_Tests::test_estimateSize_0,
+            eq(3),
+            { o, _ -> o == 0 },
+            { o, _ -> o == 1 },
+            invariants = arrayOf(
+                { o, r -> o !in 0..1 || r.getOrThrow() == o }
+            )
+        )
+    }
+
+    @Test
+    @Disabled("Index 3 out of bounds for length 3")
+    fun testForEachRemaining() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayListSpliterator_Tests::test_forEachRemaining_0,
+            eq(3),
+            { o, _ -> o == 0 },
+            { o, _ -> o == 1 },
+            invariants = arrayOf(
+                { o, r -> o !in 0..1 || r.getOrThrow() == o }
+            )
+        )
+    }
+
+    @Test
+    fun testGetExactSizeIfKnown() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayListSpliterator_Tests::test_getExactSizeIfKnown_0,
+            eq(3),
+            { o, _ -> o == 0 },
+            { o, _ -> o == 1 },
+            invariants = arrayOf(
+                { o, r -> o !in 0..1 || r.getOrThrow() == o }
+            )
+        )
+    }
+
+    @Test
+    fun testHasCharacteristics() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayListSpliterator_Tests::test_hasCharacteristics_0,
+            eq(2),
+            { o, _ -> o == 0 },
+            invariants = arrayOf(
+                { o, r -> o != 0 || r.getOrThrow() == 0 }
+            )
+        )
+    }
+
+    @Test
+    @Disabled("Unexpected expr of type void: JcLambdaExpr")
+    fun testTryAdvance() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayListSpliterator_Tests::test_tryAdvance_0,
+            eq(4),
+            { o, _ -> o == 0 },
+            { o, _ -> o == 1 },
+            { o, _ -> o == 2 },
+            invariants = arrayOf(
+                { o, r -> o !in 0..2 || r.getOrThrow() == o }
+            )
+        )
+    }
+
+    @Test
+    @Disabled("Unexpected expr of type void: JcLambdaExpr")
+    fun testTrySplit() {
+        checkDiscoveredPropertiesWithExceptions(
+            ArrayListSpliterator_Tests::test_tryAdvance_0,
+            eq(4),
+            { o, _ -> o == 0 },
+            { o, _ -> o == 1 },
+            { o, _ -> o == 2 },
+            invariants = arrayOf(
+                { o, r -> o !in 0..2 || r.getOrThrow() == o }
+            )
+        )
+    }
+}
diff --git a/usvm-jvm/src/usvm-api/java/org/usvm/api/Engine.java b/usvm-jvm/src/usvm-api/java/org/usvm/api/Engine.java
new file mode 100644
index 0000000000..f2d223e4c1
--- /dev/null
+++ b/usvm-jvm/src/usvm-api/java/org/usvm/api/Engine.java
@@ -0,0 +1,116 @@
+package org.usvm.api;
+
+public class Engine {
+    public static void assume(boolean expr) {
+        engineApiStubError();
+    }
+
+    public static <T> T makeSymbolic(Class<T> clazz) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static boolean makeSymbolicBoolean() {
+        engineApiStubError();
+        return false;
+    }
+
+    public static byte makeSymbolicByte() {
+        engineApiStubError();
+        return 0;
+    }
+
+    public static char makeSymbolicChar() {
+        engineApiStubError();
+        return 0;
+    }
+
+    public static short makeSymbolicShort() {
+        engineApiStubError();
+        return 0;
+    }
+
+    public static int makeSymbolicInt() {
+        engineApiStubError();
+        return 0;
+    }
+
+    public static long makeSymbolicLong() {
+        engineApiStubError();
+        return 0;
+    }
+
+    public static float makeSymbolicFloat() {
+        engineApiStubError();
+        return 0;
+    }
+
+    public static double makeSymbolicDouble() {
+        engineApiStubError();
+        return 0;
+    }
+
+    public static <T> T[] makeSymbolicArray(Class<T> clazz, int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static boolean[] makeSymbolicBooleanArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static byte[] makeSymbolicByteArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static char[] makeSymbolicCharArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static short[] makeSymbolicShortArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static int[] makeSymbolicIntArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static long[] makeSymbolicLongArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static float[] makeSymbolicFloatArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static double[] makeSymbolicDoubleArray(int size) {
+        engineApiStubError();
+        return null;
+    }
+
+    public static <T> SymbolicList<T> makeSymbolicList() {
+        engineApiStubError();
+        return null;
+    }
+
+    public static <K, V> SymbolicMap<K, V> makeSymbolicMap() {
+        engineApiStubError();
+        return null;
+    }
+
+    public static boolean typeEquals(Object a, Object b) {
+        engineApiStubError();
+        return false;
+    }
+
+    private static void engineApiStubError() {
+        throw new IllegalStateException("Engine API method must not be invoked");
+    }
+}
diff --git a/usvm-jvm/src/usvm-api/java/org/usvm/api/SymbolicList.java b/usvm-jvm/src/usvm-api/java/org/usvm/api/SymbolicList.java
new file mode 100644
index 0000000000..062a53bdac
--- /dev/null
+++ b/usvm-jvm/src/usvm-api/java/org/usvm/api/SymbolicList.java
@@ -0,0 +1,15 @@
+package org.usvm.api;
+
+public interface SymbolicList<E> {
+    int size();
+
+    E get(int idx);
+
+    void set(int idx, E obj);
+
+    void insert(int idx, E obj);
+
+    void remove(int idx);
+
+    void copy(SymbolicList<E> dst, int srcFrom, int dstFrom, int length);
+}
diff --git a/usvm-jvm/src/usvm-api/java/org/usvm/api/SymbolicMap.java b/usvm-jvm/src/usvm-api/java/org/usvm/api/SymbolicMap.java
new file mode 100644
index 0000000000..c9cf69084a
--- /dev/null
+++ b/usvm-jvm/src/usvm-api/java/org/usvm/api/SymbolicMap.java
@@ -0,0 +1,15 @@
+package org.usvm.api;
+
+public interface SymbolicMap<K, V> {
+    int size();
+
+    V get(K key);
+
+    void set(K key, V value);
+
+    void remove(K key);
+
+    boolean containsKey(K key);
+
+    void merge(SymbolicMap<K, V> src);
+}