From 76ddc879647a67cf4c8ea2a31027568f35c2535c Mon Sep 17 00:00:00 2001
From: Yury Kamenev <yurkam447@gmail.com>
Date: Tue, 19 Sep 2023 16:41:02 +0300
Subject: [PATCH] Introduced static refs, supported enums (#61)

---
 usvm-core/src/main/kotlin/org/usvm/Context.kt |  72 +++--
 .../src/main/kotlin/org/usvm/Expressions.kt   |  46 ++-
 .../src/main/kotlin/org/usvm/api/MemoryApi.kt |   3 +-
 .../usvm/api/collection/ListCollectionApi.kt  |   6 +-
 .../api/collection/ObjectMapCollectionApi.kt  |   6 +-
 .../org/usvm/collection/array/ArrayRegion.kt  |  44 ++-
 .../usvm/collection/array/ArrayRegionApi.kt   |   2 +-
 .../array/length/ArrayLengthRegion.kt         |  15 +-
 .../org/usvm/collection/field/FieldsRegion.kt |  44 ++-
 .../collection/map/length/UMapLengthRegion.kt |  15 +-
 .../collection/map/primitive/UMapRegion.kt    |  14 +-
 .../usvm/collection/map/ref/URefMapRegion.kt  |  28 +-
 .../collection/set/primitive/USetRegion.kt    |   8 +-
 .../usvm/collection/set/ref/URefSetRegion.kt  |  16 +-
 .../usvm/constraints/EqualityConstraints.kt   | 165 +++++++++--
 .../org/usvm/constraints/PathConstraints.kt   |  30 +-
 .../org/usvm/constraints/TypeConstraints.kt   |  95 ++++++-
 .../org/usvm/memory/HeapRefSplitting.kt       | 121 +++++---
 .../src/main/kotlin/org/usvm/memory/Memory.kt |  39 ++-
 .../kotlin/org/usvm/memory/RegistersStack.kt  |   2 +-
 .../org/usvm/memory/USymbolicCollection.kt    |   2 +-
 .../kotlin/org/usvm/model/LazyModelDecoder.kt |   8 +
 .../src/main/kotlin/org/usvm/model/Model.kt   |   6 +-
 .../kotlin/org/usvm/solver/ExprTranslator.kt  |   8 +-
 .../src/main/kotlin/org/usvm/solver/Solver.kt |   6 +
 .../usvm/solver/USoftConstraintsProvider.kt   |   2 +-
 .../main/kotlin/org/usvm/types/TypeRegion.kt  |   9 +
 .../kotlin/org/usvm/memory/HeapRefEqTest.kt   |  24 +-
 .../org/usvm/memory/HeapRefSplittingTest.kt   |  36 +--
 .../org/usvm/model/ModelDecodingTest.kt       |  10 +-
 .../kotlin/org/usvm/solver/TranslationTest.kt |  20 +-
 .../kotlin/org/usvm/types/TypeSolverTest.kt   |   8 +-
 .../org/usvm/api/util/JcTestResolver.kt       |  36 ++-
 .../org/usvm/machine/JcApproximations.kt      |  56 ++++
 .../main/kotlin/org/usvm/machine/JcContext.kt |  17 ++
 .../org/usvm/machine/JcMethodCallInst.kt      |   5 +-
 .../machine/interpreter/JcExprResolver.kt     | 269 +++++++++++++++---
 .../usvm/machine/interpreter/JcInterpreter.kt | 122 +++++---
 .../interpreter/JcStaticFieldsRegion.kt       |  68 +++++
 .../kotlin/org/usvm/machine/state/JcState.kt  |   4 +-
 .../org/usvm/machine/state/JcStateUtils.kt    |  11 -
 .../src/main/kotlin/org/usvm/util/Utils.kt    |  11 +
 .../org/usvm/samples/enums/ClassWithEnum.java |  26 +-
 .../samples/enums/ComplexEnumExamples.java    |  50 +++-
 .../org/usvm/samples/enums/CustomEnum.java    |  43 +++
 .../usvm/samples/enums/SimpleEnumExample.java |  16 ++
 .../samples/objects/ObjectWithStatics.java    |  27 +-
 .../samples/casts/InstanceOfExampleTest.kt    |   1 +
 .../usvm/samples/codegen/JavaAssertTest.kt    |   1 -
 .../codegen/deepequals/DeepEqualsTest.kt      |  16 +-
 .../usvm/samples/controlflow/SwitchTest.kt    |  14 +-
 .../usvm/samples/enums/ClassWithEnumTest.kt   |  36 +--
 .../samples/enums/ComplexEnumExamplesTest.kt  |  59 +++-
 .../samples/mixed/SerializableExampleTest.kt  |   6 +-
 .../objects/ClassForTestClinitSectionsTest.kt |   1 -
 .../org/usvm/samples/objects/TestStatics.kt   |  14 +-
 .../substitution/StaticsSubstitutionTest.kt   |   2 -
 .../samples/wrappers/BooleanWrapperTest.kt    |   1 -
 .../samples/wrappers/IntegerWrapperTest.kt    |   1 -
 .../org/usvm/machine/SampleExprResolver.kt    |   2 +-
 .../org/usvm/algorithms/DisjointSets.kt       |  27 +-
 61 files changed, 1400 insertions(+), 452 deletions(-)
 create mode 100644 usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcStaticFieldsRegion.kt
 create mode 100644 usvm-jvm/src/samples/java/org/usvm/samples/enums/CustomEnum.java
 create mode 100644 usvm-jvm/src/samples/java/org/usvm/samples/enums/SimpleEnumExample.java

diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt
index 7a022c418c..e19a6e77b0 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Context.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt
@@ -114,38 +114,54 @@ open class UContext(
         }
 
     fun mkHeapRefEq(lhs: UHeapRef, rhs: UHeapRef): UBoolExpr =
-        when {
-            // fast checks
-            lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
-            lhs is UConcreteHeapRef && rhs is UConcreteHeapRef -> mkBool(lhs == rhs)
+        mkHeapEqWithFastChecks(lhs, rhs) {
             // unfolding
-            else -> {
-                val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs, ignoreNullRefs = false)
-                val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs, ignoreNullRefs = false)
-
-                val concreteRefLhsToGuard = concreteRefsLhs.associate { it.expr.address to it.guard }
-
-                val conjuncts = mutableListOf<UBoolExpr>(falseExpr)
-
-                concreteRefsRhs.forEach { (concreteRefRhs, guardRhs) ->
-                    val guardLhs = concreteRefLhsToGuard.getOrDefault(concreteRefRhs.address, falseExpr)
-                    // mkAnd instead of mkAnd with flat=false here is OK
-                    val conjunct = mkAnd(guardLhs, guardRhs)
-                    conjuncts += conjunct
-                }
-
-                if (symbolicRefLhs != null && symbolicRefRhs != null) {
-                    val refsEq = super.mkEq(symbolicRefLhs.expr, symbolicRefRhs.expr, order = true)
-                    // mkAnd instead of mkAnd with flat=false here is OK
-                    val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq)
-                    conjuncts += conjunct
-                }
-
-                // it's safe to use mkOr here
-                mkOr(conjuncts)
+            val (concreteRefsLhs, symbolicRefLhs) = splitUHeapRef(lhs, ignoreNullRefs = false)
+            val (concreteRefsRhs, symbolicRefRhs) = splitUHeapRef(rhs, ignoreNullRefs = false)
+
+            val concreteRefLhsToGuard = concreteRefsLhs.associate { it.expr.address to it.guard }
+
+            val conjuncts = mutableListOf<UBoolExpr>(falseExpr)
+
+            concreteRefsRhs.forEach { (concreteRefRhs, guardRhs) ->
+                val guardLhs = concreteRefLhsToGuard.getOrDefault(concreteRefRhs.address, falseExpr)
+                // mkAnd instead of mkAnd with flat=false here is OK
+                val conjunct = mkAnd(guardLhs, guardRhs)
+                conjuncts += conjunct
             }
+
+            if (symbolicRefLhs != null && symbolicRefRhs != null) {
+                val refsEq = super.mkEq(symbolicRefLhs.expr, symbolicRefRhs.expr, order = true)
+                // mkAnd instead of mkAnd with flat=false here is OK
+                val conjunct = mkAnd(symbolicRefLhs.guard, symbolicRefRhs.guard, refsEq)
+                conjuncts += conjunct
+            }
+
+            // it's safe to use mkOr here
+            mkOr(conjuncts)
         }
 
+    private inline fun mkHeapEqWithFastChecks(
+        lhs: UHeapRef,
+        rhs: UHeapRef,
+        blockOnFailedFastChecks: () -> UBoolExpr,
+    ): UBoolExpr = when {
+        lhs is USymbolicHeapRef && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
+        isAllocatedConcreteHeapRef(lhs) && isAllocatedConcreteHeapRef(rhs) -> mkBool(lhs == rhs)
+        isStaticHeapRef(lhs) && isStaticHeapRef(rhs) -> mkBool(lhs == rhs)
+
+        isAllocatedConcreteHeapRef(lhs) && isStaticHeapRef(rhs) -> falseExpr
+        isStaticHeapRef(lhs) && isAllocatedConcreteHeapRef(rhs) -> falseExpr
+
+        isStaticHeapRef(lhs) && rhs is UNullRef -> falseExpr
+        lhs is UNullRef && isStaticHeapRef(rhs) -> falseExpr
+
+        lhs is USymbolicHeapRef && isStaticHeapRef(rhs) -> super.mkEq(lhs, rhs, order = true)
+        isStaticHeapRef(lhs) && rhs is USymbolicHeapRef -> super.mkEq(lhs, rhs, order = true)
+
+        else -> blockOnFailedFastChecks()
+    }
+
     private val uConcreteHeapRefCache = mkAstInterner<UConcreteHeapRef>()
     fun mkConcreteHeapRef(address: UConcreteHeapAddress): UConcreteHeapRef =
         uConcreteHeapRefCache.createIfContextActive {
diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
index dfd4c71268..c3ae7e664f 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
@@ -26,6 +26,8 @@ import io.ksmt.sort.KSort
 import io.ksmt.sort.KUninterpretedSort
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionId
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.contract
 
 //region KSMT aliases
 
@@ -76,8 +78,35 @@ typealias UHeapRef = UExpr<UAddressSort>
 typealias USymbolicHeapRef = USymbol<UAddressSort>
 typealias UConcreteHeapAddress = Int
 
-fun isSymbolicHeapRef(expr: UExpr<*>) =
-    expr.sort == expr.uctx.addressSort && expr is USymbol<*>
+@OptIn(ExperimentalContracts::class)
+fun isSymbolicHeapRef(expr: UExpr<*>): Boolean {
+    contract {
+        returns(true) implies (expr is USymbol<*>)
+    }
+
+    return expr.sort == expr.uctx.addressSort && expr is USymbol<*>
+}
+
+@OptIn(ExperimentalContracts::class)
+fun isAllocatedConcreteHeapRef(expr: UExpr<*>): Boolean {
+    contract {
+        returns(true) implies (expr is UConcreteHeapRef)
+    }
+
+    return expr is UConcreteHeapRef && expr.isAllocated
+}
+
+@OptIn(ExperimentalContracts::class)
+fun isStaticHeapRef(expr: UExpr<*>): Boolean {
+    contract {
+        returns(true) implies (expr is UConcreteHeapRef)
+    }
+
+    return expr is UConcreteHeapRef && expr.isStatic
+}
+
+val UConcreteHeapRef.isAllocated: Boolean get() = address >= INITIAL_CONCRETE_ADDRESS
+val UConcreteHeapRef.isStatic: Boolean get() = address <= INITIAL_STATIC_ADDRESS
 
 class UConcreteHeapRefDecl internal constructor(
     ctx: UContext,
@@ -129,8 +158,9 @@ class UNullRef internal constructor(
     }
 }
 
-// We split all addresses into three parts:
-//     * input values: [Int.MIN_VALUE..0),
+// We split all addresses into four parts:
+//     * static values (represented as allocated but interpreted as input): [Int.MIN_VALUE..INITIAL_STATIC_ADDRESS]
+//     * input values: (INITIAL_STATIC_ADDRESS..0),
 //     * null value: [0]
 //     * allocated values: (0..[Int.MAX_VALUE]
 
@@ -147,10 +177,16 @@ const val INITIAL_INPUT_ADDRESS = NULL_ADDRESS - 1
 
 /**
  * A constant corresponding to the first allocated address in any symbolic memory.
- * Input addresses takes this semi-interval: (0..[Int.MAX_VALUE])
+ * Allocated addresses takes this semi-interval: (0..[Int.MAX_VALUE])
  */
 const val INITIAL_CONCRETE_ADDRESS = NULL_ADDRESS + 1
 
+/**
+ * A constant corresponding to the first static address in any symbolic memory.
+ * Static addresses takes this segment: [[Int.MIN_VALUE]..[INITIAL_STATIC_ADDRESS]]
+ */
+const val INITIAL_STATIC_ADDRESS = -(1 shl 20) // Use value not less than UNINTERPRETED_SORT_MIN_ALLOWED_VALUE in ksmt
+
 
 //endregion
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt
index 2f1416e0f0..05ff2fe5f8 100644
--- a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt
@@ -22,7 +22,8 @@ import org.usvm.collection.array.allocateArrayInitialized as allocateArrayInitia
 fun <Type> UReadOnlyMemory<Type>.typeStreamOf(ref: UHeapRef): UTypeStream<Type> =
     types.getTypeStream(ref)
 
-fun UMemory<*, *>.allocate() = ctx.mkConcreteHeapRef(addressCounter.freshAddress())
+fun UMemory<*, *>.allocateConcreteRef(): UConcreteHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshAllocatedAddress())
+fun UMemory<*, *>.allocateStaticRef(): UConcreteHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshStaticAddress())
 
 fun <Field, Sort : USort> UReadOnlyMemory<*>.readField(
     ref: UHeapRef, field: Field, sort: Sort
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt
index f73b2a6e56..6a8a072470 100644
--- a/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/api/collection/ListCollectionApi.kt
@@ -11,14 +11,14 @@ import org.usvm.api.readArrayIndex
 import org.usvm.api.readArrayLength
 import org.usvm.api.writeArrayIndex
 import org.usvm.api.writeArrayLength
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsConcrete
 import org.usvm.uctx
 
 object ListCollectionApi {
     fun <ListType> UState<ListType, *, *, *, *, *>.mkSymbolicList(
         listType: ListType,
     ): UHeapRef = with(memory.ctx) {
-        val ref = memory.alloc(listType)
+        val ref = memory.allocConcrete(listType)
         memory.writeArrayLength(ref, mkSizeExpr(0), listType)
         ref
     }
@@ -36,7 +36,7 @@ object ListCollectionApi {
         listRef: UHeapRef,
         listType: ListType,
     ): Unit? {
-        listRef.map(
+        listRef.mapWithStaticAsConcrete(
             concreteMapper = {
                 // Concrete list size is always correct
                 it
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt
index 0787d70ebb..dba820f0d5 100644
--- a/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt
@@ -13,14 +13,14 @@ import org.usvm.collection.map.ref.refMapMerge
 import org.usvm.collection.set.ref.URefSetEntryLValue
 import org.usvm.collection.set.ref.URefSetRegionId
 import org.usvm.collection.set.ref.refSetUnion
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsConcrete
 import org.usvm.uctx
 
 object ObjectMapCollectionApi {
     fun <MapType> UState<MapType, *, *, *, *, *>.mkSymbolicObjectMap(
         mapType: MapType,
     ): UHeapRef = with(memory.ctx) {
-        val ref = memory.alloc(mapType)
+        val ref = memory.allocConcrete(mapType)
         val length = UMapLengthLValue(ref, mapType)
         memory.write(length, mkSizeExpr(0), trueExpr)
         ref
@@ -40,7 +40,7 @@ object ObjectMapCollectionApi {
         mapRef: UHeapRef,
         mapType: MapType,
     ): Unit? {
-        mapRef.map(
+        mapRef.mapWithStaticAsConcrete(
             concreteMapper = {
                 // Concrete map size is always correct
                 it
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt
index 345d697a8d..adea7a7d7f 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt
@@ -12,10 +12,10 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
 import org.usvm.memory.foldHeapRef2
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.key.USizeExprKeyInfo
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 
 data class UArrayIndexLValue<ArrayType, Sort : USort>(
     override val sort: Sort,
@@ -92,32 +92,30 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort>(
     private fun updateInput(updated: UInputArray<ArrayType, Sort>) =
         UArrayMemoryRegion(allocatedArrays, updated)
 
-    override fun read(key: UArrayIndexLValue<ArrayType, Sort>): UExpr<Sort> =
-        key.ref.map(
-            { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address).read(key.index) },
-            { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index) }
-        )
+    override fun read(key: UArrayIndexLValue<ArrayType, Sort>): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address).read(key.index) },
+        symbolicMapper = { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index) }
+    )
 
     override fun write(
         key: UArrayIndexLValue<ArrayType, Sort>,
         value: UExpr<Sort>,
         guard: UBoolExpr
-    ): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort>, Sort> =
-        foldHeapRef(
-            key.ref,
-            initial = this,
-            initialGuard = guard,
-            blockOnConcrete = { region, (concreteRef, innerGuard) ->
-                val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address)
-                val newRegion = oldRegion.write(key.index, value, innerGuard)
-                region.updateAllocatedArray(concreteRef.address, newRegion)
-            },
-            blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
-                val oldRegion = region.getInputArray(key.arrayType, key.sort)
-                val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard)
-                region.updateInput(newRegion)
-            }
-        )
+    ): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort>, Sort> = foldHeapRefWithStaticAsSymbolic(
+        key.ref,
+        initial = this,
+        initialGuard = guard,
+        blockOnConcrete = { region, (concreteRef, innerGuard) ->
+            val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address)
+            val newRegion = oldRegion.write(key.index, value, innerGuard)
+            region.updateAllocatedArray(concreteRef.address, newRegion)
+        },
+        blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
+            val oldRegion = region.getInputArray(key.arrayType, key.sort)
+            val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard)
+            region.updateInput(newRegion)
+        }
+    )
 
     override fun memcpy(
         srcRef: UHeapRef,
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt
index 2c590b84b3..7c1a5436f4 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegionApi.kt
@@ -60,7 +60,7 @@ internal fun <ArrayType> UWritableMemory<ArrayType>.allocateArray(
     type: ArrayType,
     length: USizeExpr
 ): UConcreteHeapRef {
-    val address = alloc(type)
+    val address = allocConcrete(type)
 
     val lengthRegionRef = UArrayLengthLValue(address, type)
     write(lengthRegionRef, length, guard = length.uctx.trueExpr)
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt
index 5442093aa2..de315a53fa 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegion.kt
@@ -11,9 +11,9 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.guardedWrite
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.sampleUValue
 import org.usvm.uctx
 
@@ -60,17 +60,16 @@ internal class UArrayLengthsMemoryRegion<ArrayType>(
     private fun updatedInput(updated: UInputArrayLengths<ArrayType>) =
         UArrayLengthsMemoryRegion(sort, arrayType, allocatedLengths, updated)
 
-    override fun read(key: UArrayLengthLValue<ArrayType>): USizeExpr =
-        key.ref.map(
-            { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
-            { symbolicRef -> getInputLength(key).read(symbolicRef) }
-        )
+    override fun read(key: UArrayLengthLValue<ArrayType>): USizeExpr = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
+        symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) }
+    )
 
     override fun write(
         key: UArrayLengthLValue<ArrayType>,
         value: USizeExpr,
         guard: UBoolExpr
-    ) = foldHeapRef(
+    ) = foldHeapRefWithStaticAsSymbolic(
         key.ref,
         initial = this,
         initialGuard = guard,
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt
index a5e24cc7e1..a75a338f92 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/field/FieldsRegion.kt
@@ -11,9 +11,9 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.guardedWrite
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.sampleUValue
 
 data class UFieldLValue<Field, Sort : USort>(override val sort: Sort, val ref: UHeapRef, val field: Field) :
@@ -55,31 +55,29 @@ internal class UFieldsMemoryRegion<Field, Sort : USort>(
     private fun updateInput(updated: UInputFields<Field, Sort>) =
         UFieldsMemoryRegion(sort, field, allocatedFields, updated)
 
-    override fun read(key: UFieldLValue<Field, Sort>): UExpr<Sort> =
-        key.ref.map(
-            { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
-            { symbolicRef -> getInputFields(key).read(symbolicRef) }
-        )
+    override fun read(key: UFieldLValue<Field, Sort>): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
+        symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef) }
+    )
 
     override fun write(
         key: UFieldLValue<Field, Sort>,
         value: UExpr<Sort>,
         guard: UBoolExpr
-    ): UMemoryRegion<UFieldLValue<Field, Sort>, Sort> =
-        foldHeapRef(
-            key.ref,
-            initial = this,
-            initialGuard = guard,
-            blockOnConcrete = { region, (concreteRef, innerGuard) ->
-                val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) {
-                    sort.sampleUValue()
-                }
-                region.updateAllocated(newRegion)
-            },
-            blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
-                val oldRegion = region.getInputFields(key)
-                val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
-                region.updateInput(newRegion)
+    ): UMemoryRegion<UFieldLValue<Field, Sort>, Sort> = foldHeapRefWithStaticAsSymbolic(
+        key.ref,
+        initial = this,
+        initialGuard = guard,
+        blockOnConcrete = { region, (concreteRef, innerGuard) ->
+            val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard) {
+                sort.sampleUValue()
             }
-        )
+            region.updateAllocated(newRegion)
+        },
+        blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
+            val oldRegion = region.getInputFields(key)
+            val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
+            region.updateInput(newRegion)
+        }
+    )
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt
index 246675e281..ffc645b359 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthRegion.kt
@@ -12,9 +12,9 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.guardedWrite
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.sampleUValue
 import org.usvm.uctx
 
@@ -63,17 +63,16 @@ internal class UMapLengthMemoryRegion<MapType>(
     private fun updateInput(updated: UInputMapLength<MapType>) =
         UMapLengthMemoryRegion(sort, mapType, allocatedLengths, updated)
 
-    override fun read(key: UMapLengthLValue<MapType>): USizeExpr =
-        key.ref.map(
-            { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
-            { symbolicRef -> getInputLength(key).read(symbolicRef) }
-        )
+    override fun read(key: UMapLengthLValue<MapType>): USizeExpr = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
+        symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) }
+    )
 
     override fun write(
         key: UMapLengthLValue<MapType>,
         value: UExpr<USizeSort>,
         guard: UBoolExpr
-    ) = foldHeapRef(
+    ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.ref,
         initial = this,
         initialGuard = guard,
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt
index 3b863224f1..3fb767de5a 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegion.kt
@@ -13,9 +13,9 @@ import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionKeyInfo
-import org.usvm.memory.foldHeapRef
 import org.usvm.memory.foldHeapRef2
-import org.usvm.memory.map
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.regions.Region
 import org.usvm.uctx
 
@@ -117,21 +117,19 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
     )
 
     override fun read(key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>): UExpr<ValueSort> =
-        key.mapRef.map(
-            { concreteRef ->
+        key.mapRef.mapWithStaticAsSymbolic(
+            concreteMapper = { concreteRef ->
                 val id = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, concreteRef.address)
                 getAllocatedMap(id).read(key.mapKey)
             },
-            { symbolicRef ->
-                getInputMap().read(symbolicRef to key.mapKey)
-            }
+            symbolicMapper = { symbolicRef -> getInputMap().read(symbolicRef to key.mapKey) }
         )
 
     override fun write(
         key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>,
         value: UExpr<ValueSort>,
         guard: UBoolExpr
-    ) = foldHeapRef(
+    ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.mapRef,
         initial = this,
         initialGuard = guard,
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegion.kt
index 0b991d2f06..144715cff7 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegion.kt
@@ -16,10 +16,10 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
 import org.usvm.memory.foldHeapRef2
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.guardedWrite
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.sampleUValue
 import org.usvm.uctx
 
@@ -161,26 +161,26 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         )
 
     override fun read(key: URefMapEntryLValue<MapType, ValueSort>): UExpr<ValueSort> =
-        key.mapRef.map(
-            { concreteRef ->
-                key.mapKey.map(
-                    { concreteKey ->
+        key.mapRef.mapWithStaticAsSymbolic(
+            concreteMapper = { concreteRef ->
+                key.mapKey.mapWithStaticAsSymbolic(
+                    concreteMapper = { concreteKey ->
                         val id = UAllocatedRefMapWithAllocatedKeysId(concreteRef.address, concreteKey.address)
                         allocatedMapWithAllocatedKeys[id] ?: valueSort.sampleUValue()
                     },
-                    { symbolicKey ->
+                    symbolicMapper = { symbolicKey ->
                         val id = allocatedMapWithInputKeyId(concreteRef.address)
                         getAllocatedMapWithInputKeys(id).read(symbolicKey)
                     }
                 )
             },
-            { symbolicRef ->
-                key.mapKey.map(
-                    { concreteKey ->
+            symbolicMapper = { symbolicRef ->
+                key.mapKey.mapWithStaticAsSymbolic(
+                    concreteMapper = { concreteKey ->
                         val id = inputMapWithAllocatedKeyId(concreteKey.address)
                         getInputMapWithAllocatedKeys(id).read(symbolicRef)
                     },
-                    { symbolicKey ->
+                    symbolicMapper = { symbolicKey ->
                         getInputMapWithInputKeys().read(symbolicRef to symbolicKey)
                     }
                 )
@@ -191,12 +191,12 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         key: URefMapEntryLValue<MapType, ValueSort>,
         value: UExpr<ValueSort>,
         guard: UBoolExpr
-    ) = foldHeapRef(
+    ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.mapRef,
         initial = this,
         initialGuard = guard,
         blockOnConcrete = { mapRegion, (concreteMapRef, mapGuard) ->
-            foldHeapRef(
+            foldHeapRefWithStaticAsSymbolic(
                 ref = key.mapKey,
                 initial = mapRegion,
                 initialGuard = mapGuard,
@@ -216,7 +216,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
             )
         },
         blockOnSymbolic = { mapRegion, (symbolicMapRef, mapGuard) ->
-            foldHeapRef(
+            foldHeapRefWithStaticAsSymbolic(
                 ref = key.mapKey,
                 initial = mapRegion,
                 initialGuard = mapGuard,
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt
index 241f83f233..077cc97208 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegion.kt
@@ -14,9 +14,9 @@ import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
 import org.usvm.memory.USymbolicCollectionKeyInfo
-import org.usvm.memory.foldHeapRef
 import org.usvm.memory.foldHeapRef2
-import org.usvm.memory.map
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.regions.Region
 import org.usvm.uctx
 
@@ -112,7 +112,7 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
         USetMemoryRegion(setType, elementSort, elementInfo, allocatedSets, updated)
 
     override fun read(key: USetEntryLValue<SetType, ElementSort, Reg>): UExpr<UBoolSort> =
-        key.setRef.map(
+        key.setRef.mapWithStaticAsSymbolic(
             { concreteRef -> allocatedSetElements(concreteRef.address).read(key.setElement) },
             { symbolicRef -> inputSetElements().read(symbolicRef to key.setElement) }
         )
@@ -121,7 +121,7 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
         key: USetEntryLValue<SetType, ElementSort, Reg>,
         value: UExpr<UBoolSort>,
         guard: UBoolExpr
-    ) = foldHeapRef(
+    ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.setRef,
         initial = this,
         initialGuard = guard,
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt
index 385cec4b5f..0ad7df57ea 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegion.kt
@@ -12,10 +12,10 @@ import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.USymbolicCollection
-import org.usvm.memory.foldHeapRef
 import org.usvm.memory.foldHeapRef2
+import org.usvm.memory.foldHeapRefWithStaticAsSymbolic
 import org.usvm.memory.guardedWrite
-import org.usvm.memory.map
+import org.usvm.memory.mapWithStaticAsSymbolic
 import org.usvm.uctx
 
 data class URefSetEntryLValue<SetType>(
@@ -154,9 +154,9 @@ internal class URefSetMemoryRegion<SetType>(
         )
 
     override fun read(key: URefSetEntryLValue<SetType>): UBoolExpr =
-        key.setRef.map(
+        key.setRef.mapWithStaticAsSymbolic(
             { concreteRef ->
-                key.setElement.map(
+                key.setElement.mapWithStaticAsSymbolic(
                     { concreteElem ->
                         val id = UAllocatedRefSetWithAllocatedElementId(concreteRef.address, concreteElem.address)
                         allocatedSetWithAllocatedElements[id] ?: sort.uctx.falseExpr
@@ -168,7 +168,7 @@ internal class URefSetMemoryRegion<SetType>(
                 )
             },
             { symbolicRef ->
-                key.setElement.map(
+                key.setElement.mapWithStaticAsSymbolic(
                     { concreteElem ->
                         val id = inputSetWithAllocatedElementsId(concreteElem.address)
                         getInputSetWithAllocatedElements(id).read(symbolicRef)
@@ -184,12 +184,12 @@ internal class URefSetMemoryRegion<SetType>(
         key: URefSetEntryLValue<SetType>,
         value: UBoolExpr,
         guard: UBoolExpr
-    ) = foldHeapRef(
+    ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.setRef,
         initial = this,
         initialGuard = guard,
         blockOnConcrete = { setRegion, (concreteSetRef, setGuard) ->
-            foldHeapRef(
+            foldHeapRefWithStaticAsSymbolic(
                 ref = key.setElement,
                 initial = setRegion,
                 initialGuard = setGuard,
@@ -209,7 +209,7 @@ internal class URefSetMemoryRegion<SetType>(
             )
         },
         blockOnSymbolic = { setRegion, (symbolicSetRef, setGuard) ->
-            foldHeapRef(
+            foldHeapRefWithStaticAsSymbolic(
                 ref = key.setElement,
                 initial = setRegion,
                 initialGuard = setGuard,
diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt
index 8513ce275a..349c8ded4a 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt
@@ -1,8 +1,12 @@
 package org.usvm.constraints
 
+import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
+import org.usvm.UHeapRef
+import org.usvm.UNullRef
 import org.usvm.USymbolicHeapRef
 import org.usvm.algorithms.DisjointSets
+import org.usvm.isStaticHeapRef
 
 /**
  * Represents equality constraints between symbolic heap references. There are three kinds of constraints:
@@ -19,19 +23,30 @@ import org.usvm.algorithms.DisjointSets
  * such that [equalReferences].find(x) == x.
  */
 class UEqualityConstraints private constructor(
-    private val ctx: UContext,
-    val equalReferences: DisjointSets<USymbolicHeapRef>,
-    private val mutableDistinctReferences: MutableSet<USymbolicHeapRef>,
-    private val mutableReferenceDisequalities: MutableMap<USymbolicHeapRef, MutableSet<USymbolicHeapRef>>,
-    private val mutableNullableDisequalities: MutableMap<USymbolicHeapRef, MutableSet<USymbolicHeapRef>>,
+    internal val ctx: UContext,
+    val equalReferences: DisjointSets<UHeapRef>,
+    private val mutableDistinctReferences: MutableSet<UHeapRef>,
+    private val mutableReferenceDisequalities: MutableMap<UHeapRef, MutableSet<UHeapRef>>,
+    private val mutableNullableDisequalities: MutableMap<UHeapRef, MutableSet<UHeapRef>>,
 ) {
-    constructor(ctx: UContext) : this(ctx, DisjointSets(), mutableSetOf(ctx.nullRef), mutableMapOf(), mutableMapOf())
+    constructor(ctx: UContext) : this(
+        ctx,
+        DisjointSets(representativeSelector = RefsRepresentativeSelector),
+        mutableSetOf(ctx.nullRef),
+        mutableMapOf(),
+        mutableMapOf()
+    )
 
-    val distinctReferences: Set<USymbolicHeapRef> = mutableDistinctReferences
+    val distinctReferences: Set<UHeapRef> = mutableDistinctReferences
 
-    val referenceDisequalities: Map<USymbolicHeapRef, Set<USymbolicHeapRef>> = mutableReferenceDisequalities
+    val referenceDisequalities: Map<UHeapRef, Set<UHeapRef>> = mutableReferenceDisequalities
 
-    val nullableDisequalities: Map<USymbolicHeapRef, Set<USymbolicHeapRef>> = mutableNullableDisequalities
+    val nullableDisequalities: Map<UHeapRef, Set<UHeapRef>> = mutableNullableDisequalities
+
+    /**
+     * Determines whether a static ref could be assigned to a symbolic, according to additional information.
+     */
+    private lateinit var isStaticRefAssignableToSymbolic: (UConcreteHeapRef, USymbolicHeapRef) -> Boolean
 
     init {
         equalReferences.subscribe(::rename)
@@ -47,16 +62,16 @@ class UEqualityConstraints private constructor(
         mutableReferenceDisequalities.clear()
     }
 
-    private fun containsReferenceDisequality(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) =
+    private fun containsReferenceDisequality(ref1: UHeapRef, ref2: UHeapRef): Boolean =
         referenceDisequalities[ref1]?.contains(ref2) ?: false
 
-    private fun containsNullableDisequality(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) =
+    private fun containsNullableDisequality(ref1: UHeapRef, ref2: UHeapRef) =
         nullableDisequalities[ref1]?.contains(ref2) ?: false
 
     /**
      * Returns if [ref1] is identical to [ref2] in *all* models.
      */
-    internal fun areEqual(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) =
+    internal fun areEqual(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef): Boolean =
         equalReferences.connected(ref1, ref2)
 
     /**
@@ -64,7 +79,7 @@ class UEqualityConstraints private constructor(
      */
     internal fun isNull(ref: USymbolicHeapRef) = areEqual(ctx.nullRef, ref)
 
-    private fun areDistinctRepresentatives(repr1: USymbolicHeapRef, repr2: USymbolicHeapRef): Boolean {
+    private fun areDistinctRepresentatives(repr1: UHeapRef, repr2: UHeapRef): Boolean {
         if (repr1 == repr2) {
             return false
         }
@@ -79,6 +94,7 @@ class UEqualityConstraints private constructor(
     internal fun areDistinct(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef): Boolean {
         val repr1 = equalReferences.find(ref1)
         val repr2 = equalReferences.find(ref2)
+
         return areDistinctRepresentatives(repr1, repr2)
     }
 
@@ -88,9 +104,22 @@ class UEqualityConstraints private constructor(
     internal fun isNotNull(ref: USymbolicHeapRef) = areDistinct(ctx.nullRef, ref)
 
     /**
-     * Adds an assertion that [ref1] is always equal to [ref2].
+     * Adds an assertion that two symbolic refs are always equal.
      */
-    internal fun makeEqual(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) {
+    internal fun makeEqual(firstSymbolicRef: USymbolicHeapRef, secondSymbolicRef: USymbolicHeapRef) {
+        makeRefEqual(firstSymbolicRef, secondSymbolicRef)
+    }
+
+    /**
+     * Adds an assertion that the symbolic ref [symbolicRef] always equals to the static ref [staticRef].
+     */
+    internal fun makeEqual(symbolicRef: USymbolicHeapRef, staticRef: UConcreteHeapRef) {
+        requireStaticRef(staticRef)
+
+        makeRefEqual(symbolicRef, staticRef)
+    }
+
+    private fun makeRefEqual(ref1: UHeapRef, ref2: UHeapRef) {
         if (isContradicting) {
             return
         }
@@ -105,7 +134,7 @@ class UEqualityConstraints private constructor(
      * Here we react to merging of equivalence classes of [from] and [to] into one represented by [to], by eliminating
      * [from] and merging its disequality constraints into [to].
      */
-    private fun rename(to: USymbolicHeapRef, from: USymbolicHeapRef) {
+    private fun rename(to: UHeapRef, from: UHeapRef) {
         if (distinctReferences.contains(from)) {
             if (distinctReferences.contains(to)) {
                 contradiction()
@@ -126,7 +155,7 @@ class UEqualityConstraints private constructor(
             mutableReferenceDisequalities.remove(from)
             fromDiseqs.forEach {
                 mutableReferenceDisequalities[it]?.remove(from)
-                makeNonEqual(to, it)
+                makeRefNonEqual(to, it)
             }
         }
 
@@ -143,17 +172,17 @@ class UEqualityConstraints private constructor(
             }
         } else if (containsNullableDisequality(from, to)) {
             // If x === y, nullable disequality can hold only if both references are null
-            makeEqual(to, nullRepr)
+            makeRefEqual(to, nullRepr)
         } else {
             val removedFrom = mutableNullableDisequalities.remove(from)
             removedFrom?.forEach {
                 mutableNullableDisequalities[it]?.remove(from)
-                makeNonEqualOrBothNull(to, it)
+                makeRefNonEqualOrBothNull(to, it)
             }
         }
     }
 
-    private fun addDisequalityUnguarded(repr1: USymbolicHeapRef, repr2: USymbolicHeapRef) {
+    private fun addDisequalityUnguarded(repr1: UHeapRef, repr2: UHeapRef) {
         when (distinctReferences.size) {
             0 -> {
                 require(referenceDisequalities.isEmpty())
@@ -209,13 +238,31 @@ class UEqualityConstraints private constructor(
     }
 
     /**
-     * Adds an assertion that [ref1] is never equal to [ref2].
+     * Adds an assertion that between two [USymbolicHeapRef] refs that they are never equal.
+     */
+    internal fun makeNonEqual(symbolicRef1: USymbolicHeapRef, symbolicRef2: USymbolicHeapRef) {
+        makeRefNonEqual(symbolicRef1, symbolicRef2)
+    }
+
+    /**
+     * Adds an assertion that the symbolic ref [symbolicRef] is never equal to the static ref [staticRef].
      */
-    internal fun makeNonEqual(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) {
+    internal fun makeNonEqual(symbolicRef: USymbolicHeapRef, staticRef: UConcreteHeapRef) {
+        requireStaticRef(staticRef)
+
+        makeRefNonEqual(symbolicRef, staticRef)
+    }
+
+    private fun makeRefNonEqual(ref1: UHeapRef, ref2: UHeapRef) {
         if (isContradicting) {
             return
         }
 
+        if (isStaticHeapRef(ref1) && isStaticHeapRef(ref2) && ref1 != ref2) {
+            // No need to do anything for static refs as they could not be equal
+            return
+        }
+
         val repr1 = equalReferences.find(ref1)
         val repr2 = equalReferences.find(ref2)
 
@@ -234,16 +281,25 @@ class UEqualityConstraints private constructor(
      * Adds an assertion that [ref1] is never equal to [ref2] or both are null.
      */
     internal fun makeNonEqualOrBothNull(ref1: USymbolicHeapRef, ref2: USymbolicHeapRef) {
+        makeRefNonEqualOrBothNull(ref1, ref2)
+    }
+
+    private fun makeRefNonEqualOrBothNull(ref1: UHeapRef, ref2: UHeapRef) {
         if (isContradicting) {
             return
         }
 
+        if (isStaticHeapRef(ref1) && isStaticHeapRef(ref2) && ref1 != ref2) {
+            // No need to do anything for static refs as they could not be equal or null
+            return
+        }
+
         val repr1 = equalReferences.find(ref1)
         val repr2 = equalReferences.find(ref2)
 
         if (repr1 == repr2) {
             // In this case, (repr1 != repr2) || (repr1 == null && repr2 == null) is equivalent to (repr1 == null).
-            makeEqual(repr1, ctx.nullRef)
+            makeRefEqual(repr1, ctx.nullRef)
             return
         }
 
@@ -263,7 +319,7 @@ class UEqualityConstraints private constructor(
         (mutableNullableDisequalities.getOrPut(repr2) { mutableSetOf() }).add(repr1)
     }
 
-    private fun removeNullableDisequality(repr1: USymbolicHeapRef, repr2: USymbolicHeapRef) {
+    private fun removeNullableDisequality(repr1: UHeapRef, repr2: UHeapRef) {
         if (containsNullableDisequality(repr1, repr2)) {
             mutableNullableDisequalities[repr1]?.remove(repr2)
             mutableNullableDisequalities[repr2]?.remove(repr1)
@@ -276,10 +332,51 @@ class UEqualityConstraints private constructor(
      * [equalityCallback] (x, y) is called.
      * Note that the order of arguments matters: the first argument is a representative of the new equivalence class.
      */
-    fun subscribe(equalityCallback: (USymbolicHeapRef, USymbolicHeapRef) -> Unit) {
+    fun subscribeEquality(equalityCallback: (UHeapRef, UHeapRef) -> Unit) {
         equalReferences.subscribe(equalityCallback)
     }
 
+    /**
+     * Sets [isStaticRefAssignableToSymbolic] according to information from [UTypeConstraints].
+     */
+    fun setTypesCheck(isStaticRefAssignableToSymbolic: (UConcreteHeapRef, USymbolicHeapRef) -> Boolean) {
+        this.isStaticRefAssignableToSymbolic = isStaticRefAssignableToSymbolic
+    }
+
+    /**
+     * Given a newly allocated static ref [allocatedStaticRef], updates [distinctReferences] and
+     * [mutableReferenceDisequalities] in the following way - removes all symbolic refs that may be equal to the
+     * [allocatedStaticRef] (according to the [isStaticRefAssignableToSymbolic]) from the [distinctReferences] and
+     * moves the information about disequality for these refs to the [mutableReferenceDisequalities].
+     * After that, adds the [allocatedStaticRef] to the [mutableDistinctReferences].
+     */
+    internal fun updateDisequality(allocatedStaticRef: UConcreteHeapRef) {
+        if (!isStaticHeapRef(allocatedStaticRef)) {
+            return
+        }
+
+        // Move from the clique to the [mutableDistinctReferences]
+        // all symbolic refs that are typely compatible with this static ref
+        val referencesToRemove = distinctReferences.filter {
+            it is USymbolicHeapRef && it !is UNullRef && isStaticRefAssignableToSymbolic(allocatedStaticRef, it)
+        }
+
+        // Here we need to save a copy of distinct refs to use all of them except the single ref from removed references
+        val oldDistinctRefs = distinctReferences.toSet()
+
+        for (ref in referencesToRemove) {
+            val otherDistinctRefs = oldDistinctRefs - ref
+            mutableDistinctReferences.remove(ref)
+
+            mutableReferenceDisequalities.getOrPut(ref) { hashSetOf() }.addAll(otherDistinctRefs)
+            otherDistinctRefs.forEach {
+                mutableReferenceDisequalities.getOrPut(it) { hashSetOf() } += ref
+            }
+        }
+
+        mutableDistinctReferences += allocatedStaticRef
+    }
+
     /**
      * Creates a mutable copy of this structure.
      * Note that current subscribers get unsubscribed!
@@ -293,8 +390,8 @@ class UEqualityConstraints private constructor(
 
         val newEqualReferences = equalReferences.clone()
         val newDistinctReferences = distinctReferences.toMutableSet()
-        val newReferenceDisequalities = mutableMapOf<USymbolicHeapRef, MutableSet<USymbolicHeapRef>>()
-        val newNullableDisequalities = mutableMapOf<USymbolicHeapRef, MutableSet<USymbolicHeapRef>>()
+        val newReferenceDisequalities = mutableMapOf<UHeapRef, MutableSet<UHeapRef>>()
+        val newNullableDisequalities = mutableMapOf<UHeapRef, MutableSet<UHeapRef>>()
 
         referenceDisequalities.mapValuesTo(newReferenceDisequalities) { it.value.toMutableSet() }
         nullableDisequalities.mapValuesTo(newNullableDisequalities) { it.value.toMutableSet() }
@@ -307,4 +404,18 @@ class UEqualityConstraints private constructor(
             newNullableDisequalities
         )
     }
+
+    private fun requireStaticRef(ref: UHeapRef) {
+        require(isStaticHeapRef(ref)) {
+            "Expected static ref but got $ref"
+        }
+    }
+
+    /**
+     * A representative selector that prefers static refs over all others, and the null ref over other symbolic.
+     */
+    object RefsRepresentativeSelector : DisjointSets.RepresentativeSelector<UHeapRef> {
+        override fun shouldSelectAsRepresentative(value: UHeapRef): Boolean =
+            isStaticHeapRef(value) || value is UNullRef
+    }
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt
index 0d40f0322e..63f3af01bb 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt
@@ -4,6 +4,7 @@ import kotlinx.collections.immutable.PersistentSet
 import kotlinx.collections.immutable.persistentSetOf
 import org.usvm.UAndExpr
 import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UEqExpr
 import org.usvm.UFalse
@@ -13,6 +14,7 @@ import org.usvm.UNotExpr
 import org.usvm.UOrExpr
 import org.usvm.USizeSort
 import org.usvm.USymbolicHeapRef
+import org.usvm.isStaticHeapRef
 import org.usvm.isSymbolicHeapRef
 import org.usvm.uctx
 
@@ -38,6 +40,11 @@ open class UPathConstraints<Type, Context : UContext> private constructor(
      */
     val numericConstraints: UNumericConstraints<USizeSort> = UNumericConstraints(ctx, sort = ctx.sizeSort)
 ) {
+    init {
+        // Use the information from the type constraints to check whether any static ref is assignable to any symbolic ref
+        equalityConstraints.setTypesCheck(typeConstraints::canStaticRefBeEqualToSymbolic)
+    }
+
     /**
      * Constraints solved by SMT solver.
      */
@@ -66,6 +73,12 @@ open class UPathConstraints<Type, Context : UContext> private constructor(
                 constraint is UEqExpr<*> && isSymbolicHeapRef(constraint.lhs) && isSymbolicHeapRef(constraint.rhs) ->
                     equalityConstraints.makeEqual(constraint.lhs as USymbolicHeapRef, constraint.rhs as USymbolicHeapRef)
 
+                constraint is UEqExpr<*> && isSymbolicHeapRef(constraint.lhs) && isStaticHeapRef(constraint.rhs) ->
+                    equalityConstraints.makeEqual(constraint.lhs as USymbolicHeapRef, constraint.rhs as UConcreteHeapRef)
+
+                constraint is UEqExpr<*> && isStaticHeapRef(constraint.lhs) && isSymbolicHeapRef(constraint.rhs) ->
+                    equalityConstraints.makeEqual(constraint.rhs as USymbolicHeapRef, constraint.lhs as UConcreteHeapRef)
+
                 constraint is UIsSubtypeExpr<*> -> {
                     typeConstraints.addSupertype(constraint.ref, constraint.supertype as Type)
                 }
@@ -79,15 +92,14 @@ open class UPathConstraints<Type, Context : UContext> private constructor(
                 constraint is UNotExpr -> {
                     val notConstraint = constraint.arg
                     when {
-                        notConstraint is UEqExpr<*> &&
-                                isSymbolicHeapRef(notConstraint.lhs) &&
-                                isSymbolicHeapRef(notConstraint.rhs) -> {
-                            require(notConstraint.rhs.sort == addressSort)
-                            equalityConstraints.makeNonEqual(
-                                notConstraint.lhs as USymbolicHeapRef,
-                                notConstraint.rhs as USymbolicHeapRef
-                            )
-                        }
+                        notConstraint is UEqExpr<*> && isSymbolicHeapRef(notConstraint.lhs) && isSymbolicHeapRef(notConstraint.rhs) ->
+                            equalityConstraints.makeNonEqual(notConstraint.lhs as USymbolicHeapRef, notConstraint.rhs as USymbolicHeapRef)
+
+                        notConstraint is UEqExpr<*> && isSymbolicHeapRef(notConstraint.lhs) && isStaticHeapRef(notConstraint.rhs) ->
+                            equalityConstraints.makeNonEqual(notConstraint.lhs as USymbolicHeapRef, notConstraint.rhs as UConcreteHeapRef)
+
+                        notConstraint is UEqExpr<*> && isStaticHeapRef(notConstraint.lhs) && isSymbolicHeapRef(notConstraint.rhs) ->
+                            equalityConstraints.makeNonEqual(notConstraint.rhs as USymbolicHeapRef, notConstraint.lhs as UConcreteHeapRef)
 
                         notConstraint is UIsSubtypeExpr<*> -> typeConstraints.excludeSupertype(
                             notConstraint.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 b63ea46ba0..b183bd510c 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/TypeConstraints.kt
@@ -3,10 +3,12 @@ package org.usvm.constraints
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UConcreteHeapRef
+import org.usvm.UContext
 import org.usvm.UHeapRef
 import org.usvm.UNullRef
 import org.usvm.USymbolicHeapRef
-import org.usvm.memory.map
+import org.usvm.isStaticHeapRef
+import org.usvm.memory.mapWithStaticAsConcrete
 import org.usvm.types.USingleTypeStream
 import org.usvm.types.UTypeRegion
 import org.usvm.types.UTypeStream
@@ -38,8 +40,10 @@ class UTypeConstraints<Type>(
     private val concreteRefToType: MutableMap<UConcreteHeapAddress, Type> = mutableMapOf(),
     symbolicRefToTypeRegion: MutableMap<USymbolicHeapRef, UTypeRegion<Type>> = mutableMapOf(),
 ) : UTypeEvaluator<Type> {
+    private val ctx: UContext get() = equalityConstraints.ctx
+
     init {
-        equalityConstraints.subscribe(::intersectRegions)
+        equalityConstraints.subscribeEquality(::intersectRegions)
     }
 
     val symbolicRefToTypeRegion get(): Map<USymbolicHeapRef, UTypeRegion<Type>> = _symbolicRefToTypeRegion
@@ -68,10 +72,31 @@ class UTypeConstraints<Type>(
      */
     fun allocate(ref: UConcreteHeapAddress, type: Type) {
         concreteRefToType[ref] = type
+
+        equalityConstraints.updateDisequality(ctx.mkConcreteHeapRef(ref))
+    }
+
+    /**
+     * Checks that the static ref [staticRef] can be equal by reference to the symbolic ref [symbolicRef]
+     * according to their types, i.e., does a [UTypeStream] for the [symbolicRef] `contain` a concrete type of the [staticRef].
+     */
+    internal fun canStaticRefBeEqualToSymbolic(staticRef: UConcreteHeapRef, symbolicRef: USymbolicHeapRef): Boolean {
+        require(isStaticHeapRef(staticRef)) {
+            "Expected static ref but $staticRef was passed"
+        }
+
+        val symbolicTypes = getTypeStream(symbolicRef)
+        if (symbolicTypes.isEmpty) {
+            // Empty type stream is possible only for the null ref, and static ref could not be equal to it
+            return false
+        }
+        val concreteType = concreteRefToType[staticRef.address] ?: error("Unknown type of the static ref $staticRef")
+
+        return !symbolicTypes.filterBySupertype(concreteType).isEmpty
     }
 
     /**
-     * @param useRepresentative use the representive from the [equalityConstraints] for the [symbolicRef]. The false
+     * @param useRepresentative use the representative from the [equalityConstraints] for the [symbolicRef]. The false
      * value used, when we intersect regions on their refs union.
      * @see intersectRegions
      */
@@ -81,12 +106,26 @@ class UTypeConstraints<Type>(
         } else {
             symbolicRef
         }
+
+        // The representative can be a static ref, so we need to construct a type region from its concrete type.
+        if (representative is UConcreteHeapRef) {
+            return concreteRefToType[representative.address]?.let {
+                UTypeRegion.fromSingleType(typeSystem, it)
+            } ?: topTypeRegion
+        }
+
         return _symbolicRefToTypeRegion[representative] ?: topTypeRegion
     }
 
 
     private fun setTypeRegion(symbolicRef: USymbolicHeapRef, value: UTypeRegion<Type>) {
-        _symbolicRefToTypeRegion[equalityConstraints.equalReferences.find(symbolicRef)] = value
+        val representative = equalityConstraints.equalReferences.find(symbolicRef)
+        if (representative is UConcreteHeapRef) {
+            // No need to set a type region for static refs as they already have a concrete type.
+            return
+        }
+
+        _symbolicRefToTypeRegion[representative as USymbolicHeapRef] = value
     }
 
     /**
@@ -222,9 +261,47 @@ class UTypeConstraints<Type>(
             else -> error("Unexpected ref: $ref")
         }
 
-    private fun intersectRegions(to: USymbolicHeapRef, from: USymbolicHeapRef) {
-        val region = getTypeRegion(from, useRepresentative = false).intersect(getTypeRegion(to))
-        updateRegionCanBeEqualNull(to, region::intersect)
+    private fun intersectRegions(to: UHeapRef, from: UHeapRef) {
+        when {
+            to is USymbolicHeapRef && from is USymbolicHeapRef -> {
+                // For both symbolic refs we need to intersect both regions
+                val region = getTypeRegion(from, useRepresentative = false).intersect(getTypeRegion(to))
+                updateRegionCanBeEqualNull(to, region::intersect)
+            }
+
+            to is UConcreteHeapRef && from is UConcreteHeapRef -> {
+                // For both concrete refs we need to check types are the same
+                val toType = concreteRefToType.getValue(to.address)
+                val fromType = concreteRefToType.getValue(from.address)
+
+                if (toType != fromType) {
+                    contradiction()
+                }
+            }
+
+            to is UConcreteHeapRef -> {
+                // Here we have a pair of symbolic-concrete refs
+                val concreteToType = concreteRefToType.getValue(to.address)
+                val symbolicFromType = getTypeRegion(from as USymbolicHeapRef, useRepresentative = false)
+
+                if (symbolicFromType.addSupertype(concreteToType).isEmpty) {
+                    contradiction()
+                }
+            }
+
+            from is UConcreteHeapRef -> {
+                // Here to is symbolic and from is concrete
+                val concreteType = concreteRefToType.getValue(from.address)
+                val symbolicType = getTypeRegion(to as USymbolicHeapRef)
+                // We need to set only the concrete type instead of all these symbolic types - make it using both subtype/supertype
+                val regionFromConcreteType = symbolicType.addSubtype(concreteType).addSupertype(concreteType)
+
+                // static could not be equal null
+                updateRegionCannotBeEqualNull(to, regionFromConcreteType::intersect)
+            }
+
+            else -> error("Unexpected refs $to, $from")
+        }
     }
 
     private fun updateRegionCannotBeEqualNull(
@@ -277,7 +354,7 @@ class UTypeConstraints<Type>(
      * Evaluates the [ref] <: [supertype] in the current [UTypeConstraints]. Always returns true on null references.
      */
     override fun evalIsSubtype(ref: UHeapRef, supertype: Type): UBoolExpr =
-        ref.map(
+        ref.mapWithStaticAsConcrete(
             concreteMapper = { concreteRef ->
                 val concreteType = concreteRefToType.getValue(concreteRef.address)
                 if (typeSystem.isSupertype(supertype, concreteType)) {
@@ -303,7 +380,7 @@ class UTypeConstraints<Type>(
         )
 
     override fun evalIsSupertype(ref: UHeapRef, subtype: Type): UBoolExpr =
-        ref.map(
+        ref.mapWithStaticAsConcrete(
             concreteMapper = { concreteRef ->
                 val concreteType = concreteRefToType.getValue(concreteRef.address)
                 if (typeSystem.isSupertype(concreteType, subtype)) {
diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt
index db37e52322..a5d830a4f4 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt
@@ -10,6 +10,7 @@ import org.usvm.UNullRef
 import org.usvm.USort
 import org.usvm.USymbolicHeapRef
 import org.usvm.isFalse
+import org.usvm.isStaticHeapRef
 import org.usvm.uctx
 
 data class GuardedExpr<out T>(
@@ -32,9 +33,9 @@ internal data class SplitHeapRefs(
 )
 
 /**
- * Traverses the [ref] non-recursively and collects [UConcreteHeapRef]s and [USymbolicHeapRef] as well as
- * guards for them. If the object is not a [UConcreteHeapRef] nor a [USymbolicHeapRef], e.g. KConst<UAddressSort>,
- * treats such an object as a [USymbolicHeapRef].
+ * Traverses the [ref] non-recursively and collects allocated [UConcreteHeapRef]s and [USymbolicHeapRef] with static
+ * [UConcreteHeapRef] as well as guards for them. If the object is not a [UConcreteHeapRef] nor a [USymbolicHeapRef],
+ * e.g. KConst<UAddressSort>, treats such an object as a [USymbolicHeapRef].
  *
  * The result [SplitHeapRefs.symbolicHeapRef] will be `null` if there are no [USymbolicHeapRef]s as
  * leafs in the [ref] ite. Otherwise, it will contain an ite with the guard protecting from bubbled up concrete refs.
@@ -51,7 +52,10 @@ internal fun splitUHeapRef(
     val concreteHeapRefs = mutableListOf<GuardedExpr<UConcreteHeapRef>>()
 
     val symbolicHeapRef = filter(ref, initialGuard, ignoreNullRefs) { guarded ->
-        if (guarded.expr is UConcreteHeapRef) {
+        val expr = guarded.expr
+
+        // Static refs may alias symbolic refs so they should be not filtered out
+        if (expr is UConcreteHeapRef && !isStaticHeapRef(expr)) {
             @Suppress("UNCHECKED_CAST")
             concreteHeapRefs += (guarded as GuardedExpr<UConcreteHeapRef>)
             false
@@ -68,8 +72,8 @@ internal fun splitUHeapRef(
 
 /**
  * Accumulates value starting with [initial], traversing [ref], accumulating guards and applying the [blockOnConcrete]
- * on [UConcreteHeapRef]s and [blockOnSymbolic] on [USymbolicHeapRef]. An argument for the [blockOnSymbolic] is
- * obtained by removing all concrete heap refs from the [ref] if it's ite.
+ * on allocated [UConcreteHeapRef]s, the [blockOnStatic] on static [UConcreteHeapRef]s, and [blockOnSymbolic] on
+ * [USymbolicHeapRef]. An argument for the [blockOnSymbolic] is obtained by removing all concrete heap refs from the [ref] if it's ite.
  *
  * @param initialGuard the initial value fot the guard to be passed to [blockOnConcrete] and [blockOnSymbolic].
  * @param ignoreNullRefs if true, then null references will be ignored. It means that all leafs with nulls
@@ -81,21 +85,23 @@ internal inline fun <R> foldHeapRef(
     initialGuard: UBoolExpr,
     ignoreNullRefs: Boolean = true,
     blockOnConcrete: (R, GuardedExpr<UConcreteHeapRef>) -> R,
+    blockOnStatic: (R, GuardedExpr<UConcreteHeapRef>) -> R,
     blockOnSymbolic: (R, GuardedExpr<UHeapRef>) -> R,
 ): R {
     if (initialGuard.isFalse) {
         return initial
     }
 
-    return when (ref) {
-        is UConcreteHeapRef -> blockOnConcrete(initial, ref with initialGuard)
-        is UNullRef -> if (!ignoreNullRefs) {
+    return when {
+        isStaticHeapRef(ref) -> blockOnStatic(initial, ref with initialGuard)
+        ref is UConcreteHeapRef -> blockOnConcrete(initial, ref with initialGuard)
+        ref is UNullRef -> if (!ignoreNullRefs) {
             blockOnSymbolic(initial, ref with initialGuard)
         } else {
             initial
         }
-        is USymbolicHeapRef ->  blockOnSymbolic(initial, ref with initialGuard)
-        is UIteExpr<UAddressSort> -> {
+        ref is USymbolicHeapRef ->  blockOnSymbolic(initial, ref with initialGuard)
+        ref is UIteExpr<UAddressSort> -> {
             val (concreteHeapRefs, symbolicHeapRef) = splitUHeapRef(ref, initialGuard)
 
             var acc = initial
@@ -108,6 +114,26 @@ internal inline fun <R> foldHeapRef(
     }
 }
 
+/**
+ * Executes [foldHeapRef] with passed [blockOnSymbolic] as a blockOnStatic.
+ */
+internal inline fun <R> foldHeapRefWithStaticAsSymbolic(
+    ref: UHeapRef,
+    initial: R,
+    initialGuard: UBoolExpr,
+    ignoreNullRefs: Boolean = true,
+    blockOnConcrete: (R, GuardedExpr<UConcreteHeapRef>) -> R,
+    blockOnSymbolic: (R, GuardedExpr<UHeapRef>) -> R,
+): R = foldHeapRef(
+    ref,
+    initial,
+    initialGuard,
+    ignoreNullRefs,
+    blockOnConcrete = blockOnConcrete,
+    blockOnStatic = blockOnSymbolic,
+    blockOnSymbolic = blockOnSymbolic
+)
+
 internal inline fun <R> foldHeapRef2(
     ref0: UHeapRef,
     ref1: UHeapRef,
@@ -118,13 +144,13 @@ internal inline fun <R> foldHeapRef2(
     blockOnConcrete0Symbolic1: (R, UConcreteHeapRef, UHeapRef, UBoolExpr) -> R,
     blockOnSymbolic0Concrete1: (R, UHeapRef, UConcreteHeapRef, UBoolExpr) -> R,
     blockOnSymbolic0Symbolic1: (R, UHeapRef, UHeapRef, UBoolExpr) -> R,
-): R = foldHeapRef(
+): R = foldHeapRefWithStaticAsSymbolic(
     ref = ref0,
     initial = initial,
     initialGuard = initialGuard,
     ignoreNullRefs = ignoreNullRefs,
     blockOnConcrete = { r0, (concrete0, guard0) ->
-        foldHeapRef(
+        foldHeapRefWithStaticAsSymbolic(
             ref = ref1,
             initial = r0,
             initialGuard = guard0,
@@ -132,22 +158,22 @@ internal inline fun <R> foldHeapRef2(
             blockOnConcrete = { r1, (concrete1, guard1) ->
                 blockOnConcrete0Concrete1(r1, concrete0, concrete1, guard1)
             },
-            blockOnSymbolic = { r1, (symbolic1, guard1) ->
-                blockOnConcrete0Symbolic1(r1, concrete0, symbolic1, guard1)
+            blockOnSymbolic = { r1, (inputRef1, guard1) ->
+                blockOnConcrete0Symbolic1(r1, concrete0, inputRef1, guard1)
             }
         )
     },
-    blockOnSymbolic = { r0, (symbolic0, guard0) ->
-        foldHeapRef(
+    blockOnSymbolic = { r0, (inputRef0, guard0) ->
+        foldHeapRefWithStaticAsSymbolic(
             ref = ref1,
             initial = r0,
             initialGuard = guard0,
             ignoreNullRefs = ignoreNullRefs,
             blockOnConcrete = { r1, (concrete1, guard1) ->
-                blockOnSymbolic0Concrete1(r1, symbolic0, concrete1, guard1)
+                blockOnSymbolic0Concrete1(r1, inputRef0, concrete1, guard1)
             },
-            blockOnSymbolic = { r1, (symbolic1, guard1) ->
-                blockOnSymbolic0Symbolic1(r1, symbolic0, symbolic1, guard1)
+            blockOnSymbolic = { r1, (inputRef1, guard1) ->
+                blockOnSymbolic0Symbolic1(r1, inputRef0, inputRef1, guard1)
             }
         )
     },
@@ -159,9 +185,9 @@ private const val DONE = 2
 
 
 /**
- * Reassembles [this] non-recursively with applying [concreteMapper] on [UConcreteHeapRef] and
- * [symbolicMapper] on [USymbolicHeapRef]. Respects [UIteExpr], so the structure of the result expression will be
- * the same as [this] is, but implicit simplifications may occur.
+ * Reassembles [this] non-recursively with applying [concreteMapper] on allocated [UConcreteHeapRef], [staticMapper] on
+ * static [UConcreteHeapRef], and [symbolicMapper] on [USymbolicHeapRef]. Respects [UIteExpr], so the structure of
+ * the result expression will be the same as [this] is, but implicit simplifications may occur.
  *
  * @param ignoreNullRefs if true, then null references will be ignored. It means that all leafs with nulls
  * considered unsatisfiable, so we assume their guards equal to false. If [ignoreNullRefs] is true and [this] is
@@ -169,17 +195,19 @@ private const val DONE = 2
  */
 internal inline fun <Sort : USort> UHeapRef.map(
     concreteMapper: (UConcreteHeapRef) -> UExpr<Sort>,
+    staticMapper: (UConcreteHeapRef) -> UExpr<Sort>,
     symbolicMapper: (USymbolicHeapRef) -> UExpr<Sort>,
     ignoreNullRefs: Boolean = true,
-): UExpr<Sort> = when (this) {
-    is UConcreteHeapRef -> concreteMapper(this)
-    is UNullRef -> {
+): UExpr<Sort> = when {
+    isStaticHeapRef(this) -> staticMapper(this)
+    this is UConcreteHeapRef -> concreteMapper(this)
+    this is UNullRef -> {
         require(!ignoreNullRefs) { "Got nullRef on the top!" }
         symbolicMapper(this)
     }
 
-    is USymbolicHeapRef -> symbolicMapper(this)
-    is UIteExpr<UAddressSort> -> {
+    this is USymbolicHeapRef -> symbolicMapper(this)
+    this is UIteExpr<UAddressSort> -> {
         /**
          * This code simulates DFS on a binary tree without an explicit recursion. Pair.second represents the first
          * unprocessed child of the pair.first (`0` means the left child, `1` means the right child).
@@ -192,10 +220,11 @@ internal inline fun <Sort : USort> UHeapRef.map(
 
         while (nodeToChild.isNotEmpty()) {
             val (ref, state) = nodeToChild.removeLast()
-            when (ref) {
-                is UConcreteHeapRef -> completelyMapped += concreteMapper(ref)
-                is USymbolicHeapRef -> completelyMapped += symbolicMapper(ref)
-                is UIteExpr<UAddressSort> -> {
+            when {
+                isStaticHeapRef(ref) -> completelyMapped += staticMapper(ref)
+                ref is UConcreteHeapRef -> completelyMapped += concreteMapper(ref)
+                ref is USymbolicHeapRef -> completelyMapped += symbolicMapper(ref)
+                ref is UIteExpr<UAddressSort> -> {
 
                     when (state) {
                         LEFT_CHILD -> {
@@ -238,6 +267,34 @@ internal inline fun <Sort : USort> UHeapRef.map(
     else -> error("Unexpected ref: $this")
 }
 
+/**
+ * Executes [foldHeapRef] with passed [concreteMapper] as a staticMapper.
+ */
+internal inline fun <Sort : USort> UHeapRef.mapWithStaticAsConcrete(
+    concreteMapper: (UConcreteHeapRef) -> UExpr<Sort>,
+    symbolicMapper: (USymbolicHeapRef) -> UExpr<Sort>,
+    ignoreNullRefs: Boolean = true,
+): UExpr<Sort> = map(
+    concreteMapper,
+    staticMapper = concreteMapper,
+    symbolicMapper,
+    ignoreNullRefs
+)
+
+/**
+ * Executes [foldHeapRef] with passed [symbolicMapper] as a staticMapper.
+ */
+internal inline fun <Sort : USort> UHeapRef.mapWithStaticAsSymbolic(
+    concreteMapper: (UConcreteHeapRef) -> UExpr<Sort>,
+    symbolicMapper: (UHeapRef) -> UExpr<Sort>,
+    ignoreNullRefs: Boolean = true,
+): UExpr<Sort> = map(
+    concreteMapper,
+    staticMapper = symbolicMapper,
+    symbolicMapper,
+    ignoreNullRefs
+)
+
 /**
  * Filters [ref] non-recursively with [predicate] and returns the result. A guard in the argument of the
  * [predicate] consists of a predicate from the root to the passed leaf.
diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
index 2f1a20e847..c01ad80597 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
@@ -3,6 +3,7 @@ package org.usvm.memory
 import kotlinx.collections.immutable.PersistentMap
 import kotlinx.collections.immutable.persistentMapOf
 import org.usvm.INITIAL_CONCRETE_ADDRESS
+import org.usvm.INITIAL_STATIC_ADDRESS
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UConcreteHeapRef
@@ -38,14 +39,25 @@ interface ULValue<Key, Sort : USort> {
 }
 
 /**
- * Current heap address holder. Calling [freshAddress] advances counter globally.
- * That is, allocation of an object in one state advances counter in all states.
+ * Current heap address holder. Calling [freshAllocatedAddress] updates [lastAllocatedAddress] or [lastStaticAddress] globally,
+ * depending on was an allocated object created or static.
+ * That is, allocation of an object in one state updates counter in all states.
  * This would help to avoid overlapping addresses in merged states.
  * Copying is prohibited.
  */
 object UAddressCounter {
-    private var lastAddress = INITIAL_CONCRETE_ADDRESS
-    fun freshAddress(): UConcreteHeapAddress = lastAddress++
+    private var lastAllocatedAddress: Int = INITIAL_CONCRETE_ADDRESS
+    private var lastStaticAddress: Int = INITIAL_STATIC_ADDRESS
+
+    /**
+     * Returns the [lastAllocatedAddress] and increments it.
+     */
+    fun freshAllocatedAddress(): UConcreteHeapAddress = lastAllocatedAddress++
+
+    /**
+     * Returns the [lastStaticAddress] and decrements it.
+     */
+    fun freshStaticAddress(): UConcreteHeapAddress = lastStaticAddress--
 }
 
 interface UReadOnlyMemory<Type> {
@@ -72,7 +84,8 @@ interface UWritableMemory<Type> : UReadOnlyMemory<Type> {
 
     fun <Key, Sort : USort> write(lvalue: ULValue<Key, Sort>, rvalue: UExpr<Sort>, guard: UBoolExpr)
 
-    fun alloc(type: Type): UConcreteHeapRef
+    fun allocConcrete(type: Type): UConcreteHeapRef
+    fun allocStatic(type: Type): UConcreteHeapRef
 }
 
 @Suppress("MemberVisibilityCanBePrivate")
@@ -125,10 +138,18 @@ class UMemory<Type, Method>(
         setRegion(regionId, newRegion)
     }
 
-    override fun alloc(type: Type): UConcreteHeapRef {
-        val concreteHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshAddress())
-        types.allocate(concreteHeapRef.address, type)
-        return concreteHeapRef
+    override fun allocConcrete(type: Type): UConcreteHeapRef {
+        val allocatedHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshAllocatedAddress())
+        types.allocate(allocatedHeapRef.address, type)
+
+        return allocatedHeapRef
+    }
+
+    override fun allocStatic(type: Type): UConcreteHeapRef {
+        val staticHeapRef = ctx.mkConcreteHeapRef(addressCounter.freshStaticAddress())
+        types.allocate(staticHeapRef.address, type)
+
+        return staticHeapRef
     }
 
     override fun nullRef(): UHeapRef = ctx.nullRef
diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt b/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
index dfe221d556..0cda291249 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
@@ -10,7 +10,7 @@ import org.usvm.uctx
 
 object URegisterStackId : UMemoryRegionId<URegisterStackLValue<*>, USort> {
     override val sort: USort
-        get() = error("Register stack has not sort")
+        get() = error("Register stack has no sort")
 
     override fun emptyRegion(): UMemoryRegion<URegisterStackLValue<*>, USort> = URegistersStack()
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt
index 2ee76ca86b..7f3f68062b 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt
@@ -102,7 +102,7 @@ data class USymbolicCollection<out CollectionId : USymbolicCollectionId<Key, Sor
         val newUpdates = if (sort == sort.uctx.addressSort) {
             // we must split symbolic and concrete heap refs here,
             // because later in [splittingRead] we check value is UConcreteHeapRef
-            foldHeapRef(
+            foldHeapRefWithStaticAsSymbolic(
                 ref = value.asExpr(value.uctx.addressSort),
                 initial = updates,
                 initialGuard = guard,
diff --git a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
index 4a5bb6131e..fbba3b26db 100644
--- a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
@@ -3,6 +3,7 @@ package org.usvm.model
 import io.ksmt.expr.KExpr
 import io.ksmt.solver.KModel
 import io.ksmt.sort.KUninterpretedSort
+import org.usvm.INITIAL_STATIC_ADDRESS
 import org.usvm.INITIAL_INPUT_ADDRESS
 import org.usvm.NULL_ADDRESS
 import org.usvm.UAddressSort
@@ -66,6 +67,13 @@ open class ULazyModelDecoder<Type>(
             if (interpretedAddress == interpreterdNullRef) {
                 continue
             }
+
+            // Static refs already have negative addresses, so just reuse them
+            if (interpretedAddress.valueIdx <= INITIAL_STATIC_ADDRESS) {
+                result[interpretedAddress] = ctx.mkConcreteHeapRef(interpretedAddress.valueIdx)
+                continue
+            }
+
             result[interpretedAddress] = ctx.mkConcreteHeapRef(counter--)
         }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/model/Model.kt b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt
index c72bd3f35d..758077a8a3 100644
--- a/usvm-core/src/main/kotlin/org/usvm/model/Model.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt
@@ -73,7 +73,11 @@ open class UModelBase<Type>(
         error("Illegal operation for a model")
     }
 
-    override fun alloc(type: Type): UConcreteHeapRef {
+    override fun allocConcrete(type: Type): UConcreteHeapRef {
+        error("Illegal operation for a model")
+    }
+
+    override fun allocStatic(type: Type): UConcreteHeapRef {
         error("Illegal operation for a model")
     }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt
index 855ba88eac..8f48358561 100644
--- a/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt
@@ -62,6 +62,7 @@ import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
 import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
 import org.usvm.collection.set.ref.URefSetRegionDecoder
 import org.usvm.collection.set.ref.USymbolicRefSetId
+import org.usvm.isStaticHeapRef
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.regions.Region
 import java.util.concurrent.ConcurrentHashMap
@@ -101,8 +102,11 @@ open class UExprTranslator<Type>(
         return const
     }
 
-    override fun transform(expr: UConcreteHeapRef): KExpr<UAddressSort> =
-        error("Unexpected UConcreteHeapRef $expr in UExprTranslator, that has to be impossible by construction!")
+    override fun transform(expr: UConcreteHeapRef): KExpr<UAddressSort> {
+        require(isStaticHeapRef(expr)) { "Unexpected ref: $expr" }
+
+        return ctx.mkUninterpretedSortValue(ctx.addressSort, expr.address)
+    }
 
     private val _declToIsExpr = mutableMapOf<KDecl<UBoolSort>, UIsExpr<Type>>()
     val declToIsExpr: Map<KDecl<UBoolSort>, UIsExpr<Type>> get() = _declToIsExpr
diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
index 0305caea76..9be38f9ac3 100644
--- a/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
@@ -10,6 +10,7 @@ import org.usvm.UHeapRef
 import org.usvm.constraints.UEqualityConstraints
 import org.usvm.constraints.UPathConstraints
 import org.usvm.isFalse
+import org.usvm.isStaticHeapRef
 import org.usvm.isTrue
 import org.usvm.model.UModelBase
 import org.usvm.model.UModelDecoder
@@ -49,6 +50,11 @@ open class USolverBase<Type, Context : UContext>(
 
         val nullRepr = constraints.equalReferences.find(ctx.nullRef)
         for (ref in constraints.distinctReferences) {
+            // Static refs are already translated as a values of an uninterpreted sort
+            if (isStaticHeapRef(ref)) {
+                continue
+            }
+
             val refIndex = if (ref == nullRepr) 0 else index++
             val translatedRef = translator.translate(ref)
             val preInterpretedValue = ctx.mkUninterpretedSortValue(ctx.addressSort, refIndex)
diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt b/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt
index b95becb8a4..abe69c3e15 100644
--- a/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/USoftConstraintsProvider.kt
@@ -108,7 +108,7 @@ class USoftConstraintsProvider<Type>(override val ctx: UContext) : UTransformer<
 
     override fun transform(
         expr: UConcreteHeapRef,
-    ): UExpr<UAddressSort> = error("Illegal operation since UConcreteHeapRef must not be translated into a solver")
+    ): UExpr<UAddressSort> = expr
 
     override fun transform(expr: UNullRef): UExpr<UAddressSort> = expr
 
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 688910b09e..96dd1437e8 100644
--- a/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/types/TypeRegion.kt
@@ -273,4 +273,13 @@ class UTypeRegion<Type>(
         subtypes: PersistentSet<Type> = this.subtypes,
         notSubtypes: PersistentSet<Type> = this.notSubtypes,
     ) = UTypeRegion(typeSystem, typeStream, supertypes, notSupertypes, subtypes, notSubtypes)
+
+    companion object {
+        fun <Type> fromSingleType(typeSystem: UTypeSystem<Type>, type: Type): UTypeRegion<Type> = UTypeRegion(
+            typeSystem,
+            USingleTypeStream(typeSystem, type),
+            supertypes = persistentSetOf(type),
+            subtypes = persistentSetOf(type)
+        )
+    }
 }
diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
index 60898ac25c..9519f6f5a3 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
@@ -8,7 +8,7 @@ import org.junit.jupiter.api.Test
 import org.usvm.Type
 import org.usvm.UComponents
 import org.usvm.UContext
-import org.usvm.api.allocate
+import org.usvm.api.allocateConcreteRef
 import kotlin.test.assertSame
 
 class HeapRefEqTest {
@@ -41,7 +41,7 @@ class HeapRefEqTest {
 
     @Test
     fun testSymbolicAndConcreteHeapRefEq() = with(ctx) {
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = mkRegisterReading(0, addressSort)
         val expr = mkHeapRefEq(ref1, ref2)
         assertSame(falseExpr, expr)
@@ -57,15 +57,15 @@ class HeapRefEqTest {
 
     @Test
     fun testConcreteHeapRefEqFalse() = with(ctx) {
-        val ref1 = heap.allocate()
-        val ref2 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
+        val ref2 = heap.allocateConcreteRef()
         val expr = mkHeapRefEq(ref1, ref2)
         assertSame(falseExpr, expr)
     }
 
     @Test
     fun testConcreteHeapRefEqTrue() = with(ctx) {
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = ref1
         val expr = mkHeapRefEq(ref1, ref2)
         assertSame(trueExpr, expr)
@@ -73,7 +73,7 @@ class HeapRefEqTest {
 
     @Test
     fun testInterleavedWithNullHeapRefEq() = with(ctx) {
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = nullRef
         val expr = mkHeapRefEq(ref1, ref2)
         assertSame(falseExpr, expr)
@@ -81,7 +81,7 @@ class HeapRefEqTest {
 
     @Test
     fun testInterleavedHeapRefEq() = with(ctx) {
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = mkRegisterReading(0, addressSort)
         val expr = mkHeapRefEq(ref1, ref2)
         assertSame(falseExpr, expr)
@@ -89,11 +89,11 @@ class HeapRefEqTest {
 
     @Test
     fun testSimpleIteConcreteHeapRefEq() = with(ctx) {
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = ref1
         val cond1 by boolSort
 
-        val ref3 = heap.allocate()
+        val ref3 = heap.allocateConcreteRef()
         val ref4 = ref3
         val cond2  by boolSort
 
@@ -118,7 +118,7 @@ class HeapRefEqTest {
 
     @Test
     fun testSimpleIteHeapRefEq() = with(ctx) {
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = mkRegisterReading(0, addressSort)
         val cond1 by boolSort
 
@@ -137,8 +137,8 @@ class HeapRefEqTest {
         val symbolicRef2 = mkRegisterReading(1, addressSort)
         val symbolicRef3 = mkRegisterReading(2, addressSort)
 
-        val concreteRef1 = heap.allocate()
-        val concreteRef2 = heap.allocate()
+        val concreteRef1 = heap.allocateConcreteRef()
+        val concreteRef2 = heap.allocateConcreteRef()
 
         val cond1 by boolSort
         val cond2 by boolSort
diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
index 1034374502..2d2bbe2e86 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
@@ -14,7 +14,7 @@ import org.usvm.UComponents
 import org.usvm.UContext
 import org.usvm.collection.field.UInputFieldReading
 import org.usvm.UIteExpr
-import org.usvm.api.allocate
+import org.usvm.api.allocateConcreteRef
 import org.usvm.api.readArrayIndex
 import org.usvm.api.readField
 import org.usvm.api.writeArrayIndex
@@ -46,8 +46,8 @@ class HeapRefSplittingTest {
 
     @Test
     fun testConcreteWriting() = with(ctx) {
-        val ref1 = heap.allocate()
-        val ref2 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
+        val ref2 = heap.allocateConcreteRef()
 
         val value1 = mkBv(0)
         val value2 = mkBv(1)
@@ -64,7 +64,7 @@ class HeapRefSplittingTest {
 
     @Test
     fun testIteWriting() = with(ctx) {
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = mkRegisterReading(0, addressSort)
 
         val cond by boolSort
@@ -86,9 +86,9 @@ class HeapRefSplittingTest {
 
     @Test
     fun testInterleavedWritingToArray(): Unit = with(ctx) {
-        val arrayRef = heap.allocate()
+        val arrayRef = heap.allocateConcreteRef()
 
-        val ref1 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
         val ref2 = mkRegisterReading(0, addressSort)
 
         val idx1 by sizeSort
@@ -112,15 +112,15 @@ class HeapRefSplittingTest {
 
     @Test
     fun testSeveralWritingsToArray() = with(ctx) {
-        val ref = heap.allocate()
+        val ref = heap.allocateConcreteRef()
 
         val idx1 = mkRegisterReading(0, sizeSort)
         val idx2 = mkRegisterReading(1, sizeSort)
         val idx3 = mkRegisterReading(2, sizeSort)
 
-        val val1 = heap.allocate()
-        val val2 = heap.allocate()
-        val val3 = heap.allocate()
+        val val1 = heap.allocateConcreteRef()
+        val val2 = heap.allocateConcreteRef()
+        val val3 = heap.allocateConcreteRef()
 
         heap.writeArrayIndex(ref, idx1, arrayDescr.first, arrayDescr.second, val1, trueExpr)
         heap.writeArrayIndex(ref, idx2, arrayDescr.first, arrayDescr.second, val2, trueExpr)
@@ -137,16 +137,16 @@ class HeapRefSplittingTest {
 
     @Test
     fun testWritingIteToArrayByIteIndex() = with(ctx) {
-        val ref1 = heap.allocate()
-        val ref2 = heap.allocate()
+        val ref1 = heap.allocateConcreteRef()
+        val ref2 = heap.allocateConcreteRef()
         val cond1 by boolSort
         val ref = mkIte(cond1, ref1, ref2)
 
         val idx = mkRegisterReading(0, sizeSort)
 
 
-        val val1 = heap.allocate()
-        val val2 = heap.allocate()
+        val val1 = heap.allocateConcreteRef()
+        val val2 = heap.allocateConcreteRef()
         val cond2 by boolSort
         val value = mkIte(cond2, val1, val2)
 
@@ -171,9 +171,9 @@ class HeapRefSplittingTest {
         val ref2 = mkRegisterReading(1, addressSort)
         val ref3 = mkRegisterReading(2, addressSort)
 
-        val val1 = heap.allocate()
+        val val1 = heap.allocateConcreteRef()
         val val2 = mkRegisterReading(3, addressSort)
-        val val3 = heap.allocate()
+        val val3 = heap.allocateConcreteRef()
 
         heap.writeField(ref1, addressFieldDescr.first, addressFieldDescr.second, val1, trueExpr)
         heap.writeField(ref2, addressFieldDescr.first, addressFieldDescr.second, val2, trueExpr)
@@ -191,7 +191,7 @@ class HeapRefSplittingTest {
 
     @Test
     fun testInterleavedWritingToArrayButNoMatchedUpdates() = with(ctx) {
-        val arrayRef = heap.allocate()
+        val arrayRef = heap.allocateConcreteRef()
 
         val ref1 = mkRegisterReading(0, addressSort)
         val ref2 = mkRegisterReading(1, addressSort)
@@ -246,7 +246,7 @@ class HeapRefSplittingTest {
     @Test
     fun testInterleavedValueWriting() = with(ctx) {
         val ref1 = mkRegisterReading(0, addressSort)
-        val ref2 = heap.allocate()
+        val ref2 = heap.allocateConcreteRef()
 
         val cond by boolSort
 
diff --git a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
index d3ba084ce8..4cece0627a 100644
--- a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
@@ -13,7 +13,7 @@ import org.usvm.UComponents
 import org.usvm.UConcreteHeapRef
 import org.usvm.UContext
 import org.usvm.UIndexedMocker
-import org.usvm.api.allocate
+import org.usvm.api.allocateConcreteRef
 import org.usvm.api.readArrayIndex
 import org.usvm.api.readField
 import org.usvm.api.writeArrayIndex
@@ -71,7 +71,7 @@ class ModelDecodingTest {
     fun testSimpleWritingToFields() = with(ctx) {
         val field = mockk<Field>()
 
-        val concreteRef = heap.allocate()
+        val concreteRef = heap.allocateConcreteRef()
         val symbolicRef0 = stack.readRegister(0, addressSort)
         val symbolicRef1 = stack.readRegister(1, addressSort)
 
@@ -93,7 +93,7 @@ class ModelDecodingTest {
     fun testSimpleWritingToAddressFields() = with(ctx) {
         val field = mockk<Field>()
 
-        val concreteRef = heap.allocate()
+        val concreteRef = heap.allocateConcreteRef()
         val symbolicRef0 = stack.readRegister(0, addressSort)
         val symbolicRef1 = stack.readRegister(1, addressSort)
 
@@ -119,7 +119,7 @@ class ModelDecodingTest {
 
         val mockedValue = mocker.call(method, emptySequence(), addressSort).first
         val ref1 = heap.readField(mockedValue, field, addressSort)
-        heap.writeField(ref1, field, addressSort, heap.allocate(), trueExpr)
+        heap.writeField(ref1, field, addressSort, heap.allocateConcreteRef(), trueExpr)
         val ref2 = heap.readField(mockedValue, field, addressSort)
 
         pc += ref1 neq ref2
@@ -156,7 +156,7 @@ class ModelDecodingTest {
     fun testSimpleSeveralWritingsToArray() = with(ctx) {
         val array = mockk<Type>()
 
-        val concreteRef = heap.allocate()
+        val concreteRef = heap.allocateConcreteRef()
         val symbolicRef0 = stack.readRegister(0, addressSort)
         val symbolicRef1 = stack.readRegister(1, addressSort)
         val symbolicRef2 = stack.readRegister(2, addressSort)
diff --git a/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
index d7021bd2c0..dc93acc85d 100644
--- a/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
@@ -18,7 +18,7 @@ import org.usvm.UComponents
 import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.UHeapRef
-import org.usvm.api.allocate
+import org.usvm.api.allocateConcreteRef
 import org.usvm.api.readArrayIndex
 import org.usvm.api.writeArrayIndex
 import org.usvm.collection.array.UAllocatedArrayId
@@ -76,7 +76,7 @@ class TranslationTest {
 
     @Test
     fun testTranslateConstAddressSort() = with(ctx) {
-        val ref = heap.allocate()
+        val ref = heap.allocateConcreteRef()
         val idx = mkRegisterReading(0, sizeSort)
 
         val expr = heap.readArrayIndex(ref, idx, addressArrayDescr, addressSort)
@@ -87,7 +87,7 @@ class TranslationTest {
 
     @Test
     fun testTranslateConstValueSort() = with(ctx) {
-        val ref = heap.allocate()
+        val ref = heap.allocateConcreteRef()
         val idx = mkRegisterReading(0, sizeSort)
 
         val expr = heap.readArrayIndex(ref, idx, valueArrayDescr, bv32Sort)
@@ -98,7 +98,7 @@ class TranslationTest {
 
     @Test
     fun testTranslateWritingsToAllocatedArray() = with(ctx) {
-        val ref = heap.allocate()
+        val ref = heap.allocateConcreteRef()
         val idx1 = mkRegisterReading(0, sizeSort)
         val idx2 = mkRegisterReading(1, sizeSort)
 
@@ -173,7 +173,7 @@ class TranslationTest {
             .write(ref1 to idx1, val1, trueExpr)
             .write(ref2 to idx2, val2, trueExpr)
 
-        val concreteRef = heap.allocate()
+        val concreteRef = heap.allocateConcreteRef()
 
 
         val adapter = USymbolicArrayInputToAllocatedCopyAdapter(
@@ -312,7 +312,7 @@ class TranslationTest {
 
     @Test
     fun testSymbolicMapRefKeyRead() = with(ctx) {
-        val concreteMapRef = heap.allocate()
+        val concreteMapRef = heap.allocateConcreteRef()
         val symbolicMapRef = mkRegisterReading(20, addressSort)
 
         runSymbolicMapRefKeyReadChecks(concreteMapRef)
@@ -320,12 +320,12 @@ class TranslationTest {
     }
 
     private fun runSymbolicMapRefKeyReadChecks(mapRef: UHeapRef) = with(ctx) {
-        val otherConcreteMapRef = heap.allocate()
+        val otherConcreteMapRef = heap.allocateConcreteRef()
         val otherSymbolicMapRef = mkRegisterReading(10, addressSort)
 
-        val concreteRef0 = heap.allocate()
-        val concreteRef1 = heap.allocate()
-        val concreteRefMissed = heap.allocate()
+        val concreteRef0 = heap.allocateConcreteRef()
+        val concreteRef1 = heap.allocateConcreteRef()
+        val concreteRefMissed = heap.allocateConcreteRef()
 
         val symbolicRef0 = mkRegisterReading(0, addressSort)
         val symbolicRef1 = mkRegisterReading(1, addressSort)
diff --git a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt
index 6ba5aac78b..7377a76c6a 100644
--- a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt
@@ -74,7 +74,7 @@ class TypeSolverTest {
 
     @Test
     fun `Test concrete ref -- open type inheritance`() {
-        val ref = memory.alloc(base1)
+        val ref = memory.allocConcrete(base1)
         val types = memory.typeStreamOf(ref)
         types.take100AndAssertEqualsToSetOf(base1)
     }
@@ -103,7 +103,7 @@ class TypeSolverTest {
 
     @Test
     fun `Test concrete ref -- empty intersection simplification`() = with(ctx) {
-        val ref = memory.alloc(base1)
+        val ref = memory.allocConcrete(base1)
         pc += mkIsSubtypeExpr(ref, base2)
         assertTrue(pc.isFalse)
     }
@@ -327,8 +327,8 @@ class TypeSolverTest {
         val arr1 = mkRegisterReading(0, addressSort)
         val arr2 = mkRegisterReading(1, addressSort)
 
-        val val1 = memory.alloc(base2)
-        val val2 = memory.alloc(base2)
+        val val1 = memory.allocConcrete(base2)
+        val val2 = memory.allocConcrete(base2)
 
         pc += mkHeapRefEq(arr1, nullRef).not()
         pc += mkHeapRefEq(arr2, nullRef).not()
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt
index 5774c8445d..3a6898c364 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestResolver.kt
@@ -2,11 +2,13 @@ package org.usvm.api.util
 
 import io.ksmt.utils.asExpr
 import org.jacodb.api.JcArrayType
+import org.jacodb.api.JcClassOrInterface
 import org.jacodb.api.JcClassType
 import org.jacodb.api.JcPrimitiveType
 import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
 import org.jacodb.api.JcTypedMethod
+import org.jacodb.api.ext.allSuperHierarchySequence
 import org.jacodb.api.ext.boolean
 import org.jacodb.api.ext.byte
 import org.jacodb.api.ext.char
@@ -14,11 +16,12 @@ import org.jacodb.api.ext.double
 import org.jacodb.api.ext.float
 import org.jacodb.api.ext.ifArrayGetElementType
 import org.jacodb.api.ext.int
+import org.jacodb.api.ext.isEnum
 import org.jacodb.api.ext.long
 import org.jacodb.api.ext.short
 import org.jacodb.api.ext.toType
 import org.jacodb.api.ext.void
-import org.usvm.INITIAL_CONCRETE_ADDRESS
+import org.usvm.INITIAL_STATIC_ADDRESS
 import org.usvm.INITIAL_INPUT_ADDRESS
 import org.usvm.NULL_ADDRESS
 import org.usvm.UConcreteHeapAddress
@@ -204,14 +207,15 @@ class JcTestResolver(
         }
 
         private fun resolveArray(ref: UConcreteHeapRef, heapRef: UHeapRef, type: JcArrayType): Any {
-            val lengthRef = UArrayLengthLValue(heapRef, ctx.arrayDescriptorOf(type))
+            val arrayDescriptor = ctx.arrayDescriptorOf(type)
+            val lengthRef = UArrayLengthLValue(heapRef, arrayDescriptor)
             val resolvedLength = resolveLValue(lengthRef, ctx.cp.int) as Int
             val length = if (resolvedLength in 0..10_000) resolvedLength else 0 // TODO hack
 
             val cellSort = ctx.typeToSort(type.elementType)
 
             fun <T> resolveElement(idx: Int): T {
-                val elemRef = UArrayIndexLValue(cellSort, heapRef, ctx.mkBv(idx), ctx.arrayDescriptorOf(type))
+                val elemRef = UArrayIndexLValue(cellSort, heapRef, ctx.mkBv(idx), arrayDescriptor)
                 @Suppress("UNCHECKED_CAST")
                 return resolveLValue(elemRef, type.elementType) as T
             }
@@ -243,14 +247,21 @@ class JcTestResolver(
         }
 
         private fun resolveObject(ref: UConcreteHeapRef, heapRef: UHeapRef, type: JcRefType): Any {
-            if (type.jcClass == ctx.classType.jcClass && ref.address >= INITIAL_CONCRETE_ADDRESS) {
+            if (type.jcClass == ctx.classType.jcClass && ref.address <= INITIAL_STATIC_ADDRESS) {
+                // Note that non-negative addresses are possible only for the result value.
                 return resolveAllocatedClass(ref)
             }
 
-            if (type.jcClass == ctx.stringType.jcClass && ref.address >= INITIAL_CONCRETE_ADDRESS) {
+            if (type.jcClass == ctx.stringType.jcClass && ref.address <= INITIAL_STATIC_ADDRESS) {
+                // Note that non-negative addresses are possible only for the result value.
                 return resolveAllocatedString(ref)
             }
 
+            val anyEnumAncestor = type.getEnumAncestorOrNull()
+            if (anyEnumAncestor != null) {
+                return resolveEnumValue(heapRef, anyEnumAncestor)
+            }
+
             val clazz = resolveType(type)
             val instance = Reflection.allocateInstance(clazz)
             resolvedCache[ref.address] = instance
@@ -275,6 +286,16 @@ class JcTestResolver(
             return instance
         }
 
+        private fun resolveEnumValue(heapRef: UHeapRef, enumAncestor: JcClassOrInterface): Any {
+            with(ctx) {
+                val ordinalLValue = UFieldLValue(sizeSort, heapRef, enumOrdinalField)
+                val ordinalFieldValue = resolveLValue(ordinalLValue, cp.int)
+                val enumClass = resolveType(enumAncestor.toType())
+
+                return enumClass.enumConstants[ordinalFieldValue as Int]
+            }
+        }
+
         private fun resolveAllocatedClass(ref: UConcreteHeapRef): Class<*> {
             val classTypeField = ctx.classTypeSyntheticField
             val classTypeLValue = UFieldLValue(ctx.addressSort, ref, classTypeField)
@@ -338,6 +359,9 @@ class JcTestResolver(
         private fun <T : USort> evaluateInModel(expr: UExpr<T>): UExpr<T> {
             return model.eval(expr)
         }
-    }
 
+        // TODO simple org.jacodb.api.ext.JcClasses.isEnum does not work with enums with abstract methods
+        private fun JcRefType.getEnumAncestorOrNull(): JcClassOrInterface? =
+            (sequenceOf(jcClass) + jcClass.allSuperHierarchySequence).firstOrNull { it.isEnum }
+    }
 }
\ No newline at end of file
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 67230cd030..7ab46177b9 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcApproximations.kt
@@ -34,6 +34,8 @@ import org.usvm.machine.state.JcState
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.skipMethodInvocationWithValue
 import org.usvm.uctx
+import org.usvm.util.allocHeapRef
+import org.usvm.util.write
 
 class JcMethodApproximationResolver(
     private val ctx: JcContext,
@@ -66,6 +68,10 @@ class JcMethodApproximationResolver(
             if (approximateUnsafeVirtualMethod(methodCall)) return true
         }
 
+        if (method.name == "clone" && method.enclosingClass == ctx.cp.objectClass) {
+            if (approximateArrayClone(methodCall)) return true
+        }
+
         return approximateEmptyNativeMethod(methodCall)
     }
 
@@ -277,6 +283,56 @@ class JcMethodApproximationResolver(
         scope.forkMulti(arrayTypeConstraintsWithBlockOnStates)
     }
 
+    private fun approximateArrayClone(methodCall: JcMethodCall): Boolean {
+        val instance = methodCall.arguments.first().asExpr(ctx.addressSort)
+        if (instance !is UConcreteHeapRef) {
+            return false
+        }
+
+        val arrayType = scope.calcOnState {
+            (memory.types.getTypeStream(instance).take(2).single())
+        }
+        if (arrayType !is JcArrayType) {
+            return false
+        }
+
+        exprResolver.resolveArrayClone(methodCall, instance, arrayType)
+        return true
+    }
+
+    private fun JcExprResolver.resolveArrayClone(
+        methodCall: JcMethodCall,
+        instance: UConcreteHeapRef,
+        arrayType: JcArrayType
+    ) = with(ctx) {
+        scope.doWithState {
+            checkNullPointer(instance) ?: return@doWithState
+
+            val arrayDescriptor = arrayDescriptorOf(arrayType)
+            val elementType = requireNotNull(arrayType.ifArrayGetElementType)
+
+            val lengthRef = UArrayLengthLValue(instance, arrayDescriptor)
+            val length = scope.calcOnState { memory.read(lengthRef).asExpr(sizeSort) }
+
+            val arrayRef = memory.allocHeapRef(arrayType, useStaticAddress = useStaticAddressForAllocation())
+            memory.write(UArrayLengthLValue(arrayRef, arrayDescriptor), length)
+
+            // It is very important to use arrayDescriptor here but not elementType correspondingly as in creating
+            // new arrays
+            memory.memcpy(
+                srcRef = instance,
+                dstRef = arrayRef,
+                arrayDescriptor,
+                elementSort = typeToSort(elementType),
+                fromSrc = mkBv(0),
+                fromDst = mkBv(0),
+                length
+            )
+
+            skipMethodInvocationWithValue(methodCall, arrayRef)
+        }
+    }
+
     private fun JcExprResolver.addArrayCopyForType(
         methodCall: JcMethodCall,
         branches: MutableList<Pair<UBoolExpr, (JcState) -> Unit>>,
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt
index b3e3c3eda9..dc51178790 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcContext.kt
@@ -52,6 +52,14 @@ class JcContext(
             ?: error("No string type in classpath")
     }
 
+    private val enumType: JcRefType by lazy {
+        cp.findTypeOrNull("java.lang.Enum") as? JcRefType
+            ?: error("No enum type in classpath")
+    }
+
+    // TODO store it in JcComponents? Make it mutable?
+    internal val useNegativeAddressesInStaticInitializer: Boolean = false
+
     fun mkVoidValue(): JcVoidValue = voidValue
 
     fun typeToSort(type: JcType) = when (type) {
@@ -93,6 +101,15 @@ class JcContext(
         stringType.jcClass.toType().declaredFields.first { it.name == "value" }
     }
 
+    val stringCoderField: JcTypedField by lazy {
+        stringType.jcClass.toType().declaredFields.first { it.name == "coder" }
+    }
+
+    // Do not use JcTypedField here as its type is not required, however JcTypedField does not have required overridden `equals` method
+    val enumOrdinalField: JcField by lazy {
+        enumType.jcClass.declaredFields.first { it.name == "ordinal" }
+    }
+
     val primitiveTypes: Set<JcPrimitiveType> by lazy {
         setOf(
             cp.boolean,
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt
index 41760a4d9b..13099df7de 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcMethodCallInst.kt
@@ -1,12 +1,14 @@
 package org.usvm.machine
 
 import org.jacodb.api.JcMethod
+import org.jacodb.api.JcRefType
 import org.jacodb.api.cfg.JcExpr
 import org.jacodb.api.cfg.JcInst
 import org.jacodb.api.cfg.JcInstLocation
 import org.jacodb.api.cfg.JcInstVisitor
 import org.jacodb.impl.cfg.JcInstLocationImpl
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
 
 /**
@@ -28,7 +30,8 @@ sealed interface JcMethodCallBaseInst : JcInst {
  * Can be used as initial instruction to start an analysis process.
  * */
 data class JcMethodEntrypointInst(
-    override val method: JcMethod
+    override val method: JcMethod,
+    val entrypointArguments: List<Pair<JcRefType, UHeapRef>>
 ) : JcMethodCallBaseInst {
     // We don't care about the location of the entrypoint
     override val location: JcInstLocation
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt
index 76c649e1db..7fd0043522 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcExprResolver.kt
@@ -5,6 +5,8 @@ import io.ksmt.utils.asExpr
 import io.ksmt.utils.cast
 import io.ksmt.utils.uncheckedCast
 import org.jacodb.api.JcArrayType
+import org.jacodb.api.JcClassOrInterface
+import org.jacodb.api.JcClassType
 import org.jacodb.api.JcMethod
 import org.jacodb.api.JcPrimitiveType
 import org.jacodb.api.JcRefType
@@ -71,13 +73,16 @@ 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.enumValues
 import org.jacodb.api.ext.float
 import org.jacodb.api.ext.ifArrayGetElementType
 import org.jacodb.api.ext.int
 import org.jacodb.api.ext.isAssignable
+import org.jacodb.api.ext.isEnum
 import org.jacodb.api.ext.long
 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.jacodb.impl.bytecode.JcFieldImpl
 import org.jacodb.impl.types.FieldInfo
@@ -106,6 +111,8 @@ import org.usvm.machine.state.addVirtualMethodCallStmt
 import org.usvm.machine.state.throwExceptionWithoutStackFrameDrop
 import org.usvm.memory.ULValue
 import org.usvm.memory.URegisterStackLValue
+import org.usvm.util.allocHeapRef
+import org.usvm.util.enumValuesField
 import org.usvm.util.write
 
 /**
@@ -118,6 +125,7 @@ class JcExprResolver(
     private val localToIdx: (JcMethod, JcLocal) -> Int,
     private val mkTypeRef: (JcType, JcState) -> UConcreteHeapRef,
     private val mkStringConstRef: (String, JcState) -> UConcreteHeapRef,
+    private val classInitializerAnalysisAlwaysRequiredForType: (JcRefType) -> Boolean,
     private val hardMaxArrayLength: Int = 1_500, // TODO: move to options
 ) : JcExprVisitor<UExpr<out USort>?> {
     /**
@@ -125,12 +133,17 @@ class JcExprResolver(
      *
      * @return a symbolic expression, with the sort corresponding to the [type].
      */
-    fun resolveJcExpr(expr: JcExpr, type: JcType = expr.type): UExpr<out USort>? =
-        if (expr.type != type) {
+    fun resolveJcExpr(expr: JcExpr, type: JcType = expr.type): UExpr<out USort>? {
+        val resolvedExpr = if (expr.type != type) {
             resolveCast(expr, type)
         } else {
             expr.accept(this)
-        }
+        } ?: return null
+
+        ensureExprCorrectness(resolvedExpr, type) ?: return null
+
+        return resolvedExpr
+    }
 
     fun resolveJcNotNullRefExpr(expr: JcExpr, type: JcType): UHeapRef? {
         check(type is JcRefType) { "Non ref type: $expr" }
@@ -287,6 +300,11 @@ class JcExprResolver(
 
     override fun visitJcStringConstant(value: JcStringConstant): UExpr<out USort> = with(ctx) {
         scope.calcOnState {
+            // Equal string constants always have equal references
+            val ref = resolveStringConstant(value.value)
+            val stringValueLValue = UFieldLValue(addressSort, ref, stringValueField.field)
+            val stringCoderLValue = UFieldLValue(byteSort, ref, stringCoderField.field)
+
             // String.value type depends on the JVM version
             val charValues = when (stringValueField.fieldType.ifArrayGetElementType) {
                 cp.char -> value.value.asSequence().map { mkBv(it.code, charSort) }
@@ -305,12 +323,9 @@ class JcExprResolver(
             // overwrite array type because descriptor is element type
             memory.types.allocate(charArrayRef.address, stringValueField.fieldType)
 
-            // Equal string constants always have equal references
-            val ref = resolveStringConstant(value.value)
-
-            // String constants are immutable. Therefore, it is correct to overwrite value and type.
-            val stringValueLValue = UFieldLValue(addressSort, ref, stringValueField.field)
+            // String constants are immutable. Therefore, it is correct to overwrite value, coder and type.
             memory.write(stringValueLValue, charArrayRef)
+            memory.write(stringCoderLValue, mkBv(0, byteSort))
             memory.types.allocate(ref.address, stringType)
 
             ref
@@ -331,13 +346,13 @@ class JcExprResolver(
 
     fun resolveClassRef(type: JcType): UConcreteHeapRef = scope.calcOnState {
         val ref = mkTypeRef(type, this)
+        val classRefTypeLValue = UFieldLValue(ctx.addressSort, ref, ctx.classTypeSyntheticField)
 
         // Ref type is java.lang.Class
         memory.types.allocate(ref.address, ctx.classType)
 
-        // Save ref original class type
-        val classRefType = memory.alloc(type)
-        val classRefTypeLValue = UFieldLValue(ctx.addressSort, ref, ctx.classTypeSyntheticField)
+        // Save ref original class type with the negative address
+        val classRefType = memory.allocStatic(type)
         memory.write(classRefTypeLValue, classRefType)
 
         ref
@@ -376,17 +391,19 @@ class JcExprResolver(
         checkNewArrayLength(size) ?: return null
 
         scope.calcOnState {
-            val ref = memory.alloc(expr.type)
+            val ref = memory.allocHeapRef(expr.type, useStaticAddress = useStaticAddressForAllocation())
 
             val arrayDescriptor = arrayDescriptorOf(expr.type as JcArrayType)
             memory.write(UArrayLengthLValue(ref, arrayDescriptor), size)
+            // overwrite array type because descriptor is element type (which is Object for arrays of refs)
+            memory.types.allocate(ref.address, expr.type)
 
             ref
         }
     }
 
     override fun visitJcNewExpr(expr: JcNewExpr): UExpr<out USort> =
-        scope.calcOnState { memory.alloc(expr.type) }
+        scope.calcOnState { memory.allocHeapRef(expr.type, useStaticAddress = useStaticAddressForAllocation()) }
 
     override fun visitJcPhiExpr(expr: JcPhiExpr): UExpr<out USort> =
         error("Unexpected expr: $expr")
@@ -413,7 +430,6 @@ class JcExprResolver(
             scope.doWithState { addVirtualMethodCallStmt(expr.method.method, arguments) }
         }
 
-
     override fun visitJcStaticCallExpr(expr: JcStaticCallExpr): UExpr<out USort>? =
         resolveInvoke(
             expr.method,
@@ -450,24 +466,28 @@ class JcExprResolver(
         argumentExprs: () -> List<JcValue>,
         argumentTypes: () -> List<JcType>,
         onNoCallPresent: JcStepScope.(List<UExpr<out USort>>) -> Unit,
-    ): UExpr<out USort>? = ensureStaticFieldsInitialized(method.enclosingType) {
-        val arguments = mutableListOf<UExpr<out USort>>()
+    ): UExpr<out USort>? {
+        val instanceRef = if (instanceExpr != null) {
+            resolveJcExpr(instanceExpr)?.asExpr(ctx.addressSort) ?: return null
+        } else {
+            null
+        }
 
-        if (instanceExpr != null) {
-            val instance = resolveJcExpr(instanceExpr)?.asExpr(ctx.addressSort) ?: return null
-            checkNullPointer(instance) ?: return null
+        val arguments = mutableListOf<UExpr<out USort>>()
+        if (instanceRef != null) {
+            checkNullPointer(instanceRef) ?: return null
 
             // Ensure instance is subtype of method class
-            if (!assertIsSubtype(instance, method.enclosingType)) return null
+            if (!assertIsSubtype(instanceRef, method.enclosingType)) return null
 
-            arguments += instance
+            arguments += instanceRef
         }
 
         argumentExprs().zip(argumentTypes()) { expr, type ->
             arguments += resolveJcExpr(expr, type) ?: return null
         }
 
-        resolveInvokeNoStaticInitializationCheck { onNoCallPresent(arguments) }
+        return resolveInvokeNoStaticInitializationCheck { onNoCallPresent(arguments) }
     }
 
     private inline fun resolveInvokeNoStaticInitializationCheck(
@@ -544,37 +564,166 @@ class JcExprResolver(
 
     // region lvalue resolving
 
-    private fun resolveFieldRef(instance: JcValue?, field: JcTypedField): ULValue<*, *>? =
-        ensureStaticFieldsInitialized(field.enclosingType) {
-            with(ctx) {
-                if (instance != null) {
-                    val instanceRef = resolveJcExpr(instance)?.asExpr(addressSort) ?: return null
-                    checkNullPointer(instanceRef) ?: return null
-
-                    // Ensure instance is subtype of field class
-                    if (!assertIsSubtype(instanceRef, field.enclosingType)) return null
-
-                    val sort = ctx.typeToSort(field.fieldType)
-                    UFieldLValue(sort, instanceRef, field.field)
-                } else {
-                    val sort = ctx.typeToSort(field.fieldType)
-                    val classRef = resolveClassRef(field.enclosingType)
-                    UFieldLValue(sort, classRef, field.field)
-                }
+    private fun resolveFieldRef(instance: JcValue?, field: JcTypedField): ULValue<*, *>? {
+        with(ctx) {
+            val instanceRef = if (instance != null) {
+                resolveJcExpr(instance)?.asExpr(addressSort) ?: return null
+            } else {
+                null
+            }
+
+            if (instanceRef != null) {
+                checkNullPointer(instanceRef) ?: return null
+
+                // Ensure instance is subtype of field class
+                if (!assertIsSubtype(instanceRef, field.enclosingType)) return null
+
+                val sort = ctx.typeToSort(field.fieldType)
+                return UFieldLValue(sort, instanceRef, field.field)
+            }
+
+            return ensureStaticFieldsInitialized(field.enclosingType, classInitializerAnalysisRequired = true) {
+                val sort = ctx.typeToSort(field.fieldType)
+                JcStaticFieldLValue(field.field, ctx, sort)
+            }
+        }
+    }
+
+    fun ensureExprCorrectness(expr: UExpr<*>, type: JcType): Unit? {
+        if (type !is JcClassType || !type.jcClass.isEnum) {
+            return Unit
+        }
+
+        return ensureStaticFieldsInitialized(type.jcClass.toType(), classInitializerAnalysisRequired = true) {
+            scope.calcOnState {
+                ensureEnumInstanceCorrectness(expr.asExpr(ctx.addressSort), type.jcClass)
             }
         }
+    }
+
+    /**
+     * This method adds a few constraints for the instance of an enum type to satisfy its invariants in Java:
+     * - Its ordinal takes this semi-interval: [0..$VALUES.size).
+     * - It equals by reference to the one of the enum constant of this enum type or null — this invariant is represented
+     * as a constraint that this instance equals by reference to the array reading from the $VALUES field by its ordinal or null.
+     *
+     * Without such constraints, false positive can appear — for example, forking on the negative ordinal, or incorrect enum
+     * values could be constructed as method parameters.
+     */
+    private fun JcState.ensureEnumInstanceCorrectness(
+        enumInstance: UHeapRef,
+        type: JcClassOrInterface,
+    ): Unit? = with(ctx) {
+        if (enumInstance is UConcreteHeapRef) {
+            // We do not need to ensure correctness for existing enum constants
+            return Unit
+        }
+
+        val enumValues = type.enumValues
+
+        val maxOrdinalValue = enumValues!!.size.toBv()
+        val ordinalFieldOfEnumInstanceLValue = UFieldLValue(sizeSort, enumInstance, enumOrdinalField)
+        val ordinalFieldValue = memory.read(ordinalFieldOfEnumInstanceLValue)
+
+        val ordinalCorrectnessConstraints =
+            mkBvSignedLessOrEqualExpr(mkBv(0), ordinalFieldValue) and mkBvSignedLessExpr(
+                ordinalFieldValue,
+                maxOrdinalValue
+            )
+
+        val enumValuesField = type.enumValuesField
+        val enumValuesFieldLValue = JcStaticFieldLValue(enumValuesField.field, ctx, addressSort)
+        val enumValuesRef = memory.read(enumValuesFieldLValue)
+
+        val oneOfEnumInstancesLValue =
+            UArrayIndexLValue(addressSort, enumValuesRef, ordinalFieldValue, cp.objectType)
+        val oneOfEnumInstancesRef = memory.read(oneOfEnumInstancesLValue)
+        val oneOfEnumInstancesEqualityConstraint = mkHeapRefEq(enumInstance, oneOfEnumInstancesRef)
+
+        val oneOfEnumInstances = ordinalCorrectnessConstraints and oneOfEnumInstancesEqualityConstraint
+        val isEnumNull = mkHeapRefEq(enumInstance, nullRef)
+        // A dirty hack to make both branches possible - with null enum value and
+        // the enum value equal to the one of corresponding enum constants
+        val invariantsConstraint = mkIteNoSimplify(isEnumNull, trueExpr, oneOfEnumInstances)
+
+
+        scope.assert(invariantsConstraint)
+    }
+
+    /**
+     * This method ensures enum constants are correct in any model. It is provided by adding a few constraints:
+     * - The length of the $VALUES field is always the same as after interpreting the corresponding static initializer.
+     * - The ordinal of each enum constant is always the same as after interpreting the corresponding static initializer.
+     * - Each enum constant always equals by reference to the array reading from the $VALUES array by its ordinal.
+     *
+     * Without such constraints, incorrect enum values could be constructed in case of aliasing method parameters with
+     * the enum constants (represented as static refs), or the $VALUES array.
+     */
+    private fun JcState.ensureEnumStaticInitializerInvariants(type: JcClassOrInterface) = with(ctx) {
+        val enumValues = type.enumValues ?: error("Expected enum values containing in the enum type $type")
+        val enumValuesField = type.enumValuesField
+        val enumValuesFieldLValue = JcStaticFieldLValue(enumValuesField.field, ctx, addressSort)
+        val enumValuesRef = memory.read(enumValuesFieldLValue)
+
+        val enumValuesType = enumValuesField.fieldType as JcArrayType
+        val enumValuesArrayDescriptor = arrayDescriptorOf(enumValuesType)
+
+        val enumValuesFieldLengthLValue = UArrayLengthLValue(enumValuesRef, enumValuesArrayDescriptor)
+        val enumValuesFieldLengthBeforeClinit =
+            enumValuesFieldLengthLValue.memoryRegionId.emptyRegion().read(enumValuesFieldLengthLValue)
+        val enumValuesFieldLengthAfterClinit = memory.read(enumValuesFieldLengthLValue)
+
+        // Ensure that $VALUES in a model has the same length as the $VALUES in the memory
+        scope.assert(mkEq(enumValuesFieldLengthBeforeClinit, enumValuesFieldLengthAfterClinit))
+            ?: error("Cannot assert correctness constraint for the \$VALUES of the enum class ${type.name}")
+
+        enumValues.indices.forEach { ordinal ->
+            // {0x1 <- 1}{0x2 <- 2}ordinal
+            // read(ordinal, 0x1) = 1
+            // read(ordinal, 0x2) = 2
+            val enumConstantLValue =
+                UArrayIndexLValue(addressSort, enumValuesRef, mkSizeExpr(ordinal), cp.objectType)
+            val enumConstantRefAfterClinit = memory.read(enumConstantLValue)
+            val enumConstantRefBeforeClinit =
+                enumConstantLValue.memoryRegionId.emptyRegion().read(enumConstantLValue)
+
+            val ordinalFieldLValue =
+                UFieldLValue(sizeSort, enumConstantRefAfterClinit, enumOrdinalField)
+            val ordinalFieldValueAfterClinit = memory.read(ordinalFieldLValue)
+            val ordinalEmptyRegion = ordinalFieldLValue.memoryRegionId.emptyRegion()
+            val ordinalFieldValueBeforeClinit = ordinalEmptyRegion.read(ordinalFieldLValue)
+
+            // Ensure that the ordinal of each enum constant equals to the real ordinal value
+            scope.assert(mkEq(ordinalFieldValueAfterClinit, ordinalFieldValueBeforeClinit))
+                ?: error("Cannot assert enum correctness constraint for a constant of the enum class ${type.name}")
+
+            // Ensure that each enum constant in a model equals by reference to the corresponding value in the memory
+            scope.assert(mkEq(enumConstantRefBeforeClinit, enumConstantRefAfterClinit))
+                ?: error("Cannot assert enum correctness constraint for a constant of the enum class ${type.name}")
+        }
+    }
+
 
     /**
      * Run a class static initializer for [type] if it didn't run before the current state.
      * The class static initialization state is tracked by the synthetic [staticFieldsInitializedFlagField] field.
      * */
-    private inline fun <T> ensureStaticFieldsInitialized(type: JcRefType, body: () -> T): T? {
+    private inline fun <T> ensureStaticFieldsInitialized(
+        type: JcRefType,
+        classInitializerAnalysisRequired: Boolean,
+        body: () -> T,
+    ): T? {
         // java.lang.Object has no static fields, but has non-trivial initializer
         if (type == ctx.cp.objectType) {
             return body()
         }
 
-        val initializer = type.jcClass.declaredMethods.firstOrNull { it.isClassInitializer }
+        if (!classInitializerAnalysisRequired && !classInitializerAnalysisAlwaysRequiredForType(type)) {
+            return body()
+        }
+
+        val jcClass = type.jcClass
+        val initializer = jcClass.declaredMethods.firstOrNull { it.isClassInitializer }
 
         // Class has no static initializer
         if (initializer == null) {
@@ -596,6 +745,11 @@ class JcExprResolver(
                 val result = methodResult
                 if (result is JcMethodResult.Success && result.method == initializer) {
                     methodResult = JcMethodResult.NoCall
+
+                    mutatePrimitiveFieldValuesToSymbolic(scope, initializer)
+                    if (jcClass.isEnum) {
+                        ensureEnumStaticInitializerInvariants(jcClass)
+                    }
                 }
             }
 
@@ -649,7 +803,8 @@ class JcExprResolver(
     // region implicit exceptions
 
     fun allocateException(type: JcRefType): (JcState) -> Unit = { state ->
-        val address = state.memory.alloc(type)
+        // TODO should we consider exceptions with negative addresses?
+        val address = state.memory.allocConcrete(type)
         state.throwExceptionWithoutStackFrameDrop(address, type)
     }
 
@@ -829,6 +984,36 @@ class JcExprResolver(
         return block(result0, result1)
     }
 
+    /**
+     * Always use negative addresses in enum static initializers,
+     * for static initializers of other classes depends on [JcContext.useNegativeAddressesInStaticInitializer].
+     */
+    fun JcState.useStaticAddressForAllocation(): Boolean {
+        val isEnumStaticInitializer = lastEnteredMethod.let { it.isClassInitializer && it.enclosingClass.isEnum }
+        if (isEnumStaticInitializer) {
+            return true
+        }
+
+        return ctx.useNegativeAddressesInStaticInitializer && callStack.any { it.method.isClassInitializer }
+    }
+
+    /**
+     * Consider all mutable primitive fields allocated in the static initializer as symbolic values.
+     */
+    private fun mutatePrimitiveFieldValuesToSymbolic(
+        scope: JcStepScope,
+        staticInitializer: JcMethod
+    ) {
+        scope.calcOnState {
+            with(ctx) {
+                // We can use any sort here as it is not used
+                val staticFieldsMemoryRegionId = JcStaticFieldRegionId(staticInitializer.enclosingClass.toType(), voidSort)
+                val staticFieldsMemoryRegion = memory.getRegion(staticFieldsMemoryRegionId) as JcStaticFieldsMemoryRegion
+                staticFieldsMemoryRegion.mutatePrimitiveStaticFieldValuesToSymbolic(this@calcOnState)
+            }
+        }
+    }
+
     companion object {
         /**
          * Synthetic field to track static field initialization state.
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 be67f37f79..5e6f15c3b9 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
@@ -28,16 +28,19 @@ import org.jacodb.api.cfg.JcSwitchInst
 import org.jacodb.api.cfg.JcThis
 import org.jacodb.api.cfg.JcThrowInst
 import org.jacodb.api.ext.boolean
+import org.jacodb.api.ext.isEnum
 import org.jacodb.api.ext.void
-import org.usvm.INITIAL_INPUT_ADDRESS
 import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapRef
+import org.usvm.UHeapRef
 import org.usvm.UInterpreter
-import org.usvm.api.allocate
+import org.usvm.api.allocateStaticRef
 import org.usvm.api.targets.JcTarget
 import org.usvm.api.typeStreamOf
+import org.usvm.isAllocatedConcreteHeapRef
+import org.usvm.isStaticHeapRef
 import org.usvm.machine.JcApplicationGraph
 import org.usvm.machine.JcConcreteMethodCallInst
 import org.usvm.machine.JcContext
@@ -48,10 +51,10 @@ import org.usvm.machine.JcMethodEntrypointInst
 import org.usvm.machine.JcVirtualMethodCallInst
 import org.usvm.machine.state.JcMethodResult
 import org.usvm.machine.state.JcState
-import org.usvm.machine.state.addEntryMethodCall
 import org.usvm.machine.state.addNewMethodCall
 import org.usvm.machine.state.lastStmt
 import org.usvm.machine.state.localIdx
+import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.parametersWithThisCount
 import org.usvm.machine.state.returnValue
@@ -80,16 +83,18 @@ class JcInterpreter(
 
     fun getInitialState(method: JcMethod, targets: List<JcTarget> = emptyList()): JcState {
         val state = JcState(ctx, targets = targets)
-        state.newStmt(JcMethodEntrypointInst(method))
-
         val typedMethod = with(applicationGraph) { method.typed }
 
+        val entrypointArguments = mutableListOf<Pair<JcRefType, UHeapRef>>()
         if (!method.isStatic) {
             with(ctx) {
                 val thisLValue = URegisterStackLValue(addressSort, 0)
                 val ref = state.memory.read(thisLValue).asExpr(addressSort)
                 state.pathConstraints += mkEq(ref, nullRef).not()
-                state.pathConstraints += mkIsSubtypeExpr(ref, typedMethod.enclosingType)
+                val thisType = typedMethod.enclosingType
+                state.pathConstraints += mkIsSubtypeExpr(ref, thisType)
+
+                entrypointArguments += thisType to ref
             }
         }
 
@@ -100,6 +105,8 @@ class JcInterpreter(
                     val argumentLValue = URegisterStackLValue(typeToSort(type), method.localIdx(idx))
                     val ref = state.memory.read(argumentLValue).asExpr(addressSort)
                     state.pathConstraints += mkIsSubtypeExpr(ref, type)
+
+                    entrypointArguments += type to ref
                 }
             }
         }
@@ -109,6 +116,8 @@ class JcInterpreter(
         val model = (solver.checkWithSoftConstraints(state.pathConstraints) as USatResult).model
         state.models = listOf(model)
 
+        val entrypointInst = JcMethodEntrypointInst(method, entrypointArguments)
+        state.newStmt(entrypointInst)
         return state
     }
 
@@ -196,7 +205,23 @@ class JcInterpreter(
         when (stmt) {
             is JcMethodEntrypointInst -> {
                 scope.doWithState {
-                    addEntryMethodCall(applicationGraph, stmt)
+                    if (callStack.isEmpty()) {
+                        val method = stmt.method
+                        callStack.push(method, returnSite = null)
+                        memory.stack.push(method.parametersWithThisCount, method.localsCount)
+                    }
+                }
+
+                val exprResolver = exprResolverWithScope(scope)
+                // Run static initializer for all enum arguments of the entrypoint
+                for ((type, ref) in stmt.entrypointArguments) {
+                    exprResolver.ensureExprCorrectness(ref, type) ?: return
+                }
+
+                val method = stmt.method
+                val entryPoint = applicationGraph.entryPoints(method).single()
+                scope.doWithState {
+                    newStmt(entryPoint)
                 }
             }
 
@@ -352,6 +377,7 @@ class JcInterpreter(
             ::mapLocalToIdxMapper,
             ::typeInstanceAllocator,
             ::stringConstantAllocator,
+            ::classInitializerAlwaysAnalysisRequiredForType
         )
 
     private val localVarToIdx = mutableMapOf<JcMethod, MutableMap<String, Int>>() // (method, localName) -> idx
@@ -378,8 +404,8 @@ class JcInterpreter(
     // Equal string constants must have equal references
     private fun stringConstantAllocator(value: String, state: JcState): UConcreteHeapRef =
         stringConstantAllocatedRefs.getOrPut(value) {
-            // Allocate globally unique ref
-            state.memory.allocate()
+            // Allocate globally unique ref with a negative address
+            state.memory.allocateStaticRef()
         }
 
     private val typeInstanceAllocatedRefs = mutableMapOf<JcTypeInfo, UConcreteHeapRef>()
@@ -387,11 +413,16 @@ class JcInterpreter(
     private fun typeInstanceAllocator(type: JcType, state: JcState): UConcreteHeapRef {
         val typeInfo = resolveTypeInfo(type)
         return typeInstanceAllocatedRefs.getOrPut(typeInfo) {
-            // Allocate globally unique ref
-            state.memory.allocate()
+            // Allocate globally unique ref with a negative address
+            state.memory.allocateStaticRef()
         }
     }
 
+    private fun classInitializerAlwaysAnalysisRequiredForType(type: JcRefType): Boolean {
+        // Always analyze a static initializer for enums
+        return type.jcClass.isEnum
+    }
+
     private fun resolveTypeInfo(type: JcType): JcTypeInfo = when (type) {
         is JcClassType -> JcClassTypeInfo(type.jcClass)
         is JcPrimitiveType -> JcPrimitiveTypeInfo(type)
@@ -419,52 +450,55 @@ class JcInterpreter(
         val instance = arguments.first().asExpr(ctx.addressSort)
         val concreteRef = scope.calcOnState { models.first().eval(instance) } as UConcreteHeapRef
 
-        if (concreteRef.address <= INITIAL_INPUT_ADDRESS) {
-            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)
-                    )
-                }
-            }
+        if (isAllocatedConcreteHeapRef(concreteRef) || isStaticHeapRef(concreteRef)) {
+            // We have only one type for allocated and static heap refs
+            val type = scope.calcOnState { memory.typeStreamOf(concreteRef) }.first()
 
-            val typeConstraintsWithBlockOnStates = mutableListOf<Pair<UBoolExpr, (JcState) -> Unit>>()
+            val concreteMethod = type.findMethod(method)
+                ?: error("Can't find method $method in type ${type.typeName}")
 
-            inheritors.mapIndexedTo(typeConstraintsWithBlockOnStates) { idx, type ->
-                val isExpr = typeConstraints[idx]
+            scope.doWithState {
+                val concreteCall = methodCall.toConcreteMethodCall(concreteMethod.method)
+                newStmt(concreteCall)
+            }
 
-                val block = { state: JcState ->
-                    val concreteMethod = type.findMethod(method)
-                        ?: error("Can't find method $method in type ${type.typeName}")
+            return@with
+        }
 
-                    val concreteCall = methodCall.toConcreteMethodCall(concreteMethod.method)
-                    state.newStmt(concreteCall)
-                }
+        val typeStream = scope.calcOnState { models.first().typeStreamOf(concreteRef) }
 
-                isExpr to block
+        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)
+                )
             }
+        }
 
-            if (forkOnRemainingTypes) {
-                val excludeAllTypesConstraint = ctx.mkAnd(typeConstraints.map { ctx.mkNot(it) })
-                typeConstraintsWithBlockOnStates += excludeAllTypesConstraint to { } // do nothing, just exclude types
-            }
+        val typeConstraintsWithBlockOnStates = mutableListOf<Pair<UBoolExpr, (JcState) -> Unit>>()
 
-            scope.forkMulti(typeConstraintsWithBlockOnStates)
-        } else {
-            val type = scope.calcOnState { memory.typeStreamOf(concreteRef) }.first()
+        inheritors.mapIndexedTo(typeConstraintsWithBlockOnStates) { idx, type ->
+            val isExpr = typeConstraints[idx]
 
-            val concreteMethod = type.findMethod(method)
-                ?: error("Can't find method $method in type ${type.typeName}")
+                val block = { state: JcState ->
+                    val concreteMethod = type.findMethod(method)
+                        ?: error("Can't find method $method in type ${type.typeName}")
 
-            scope.doWithState {
                 val concreteCall = methodCall.toConcreteMethodCall(concreteMethod.method)
-                newStmt(concreteCall)
+                state.newStmt(concreteCall)
             }
+
+            isExpr to block
         }
+
+        if (forkOnRemainingTypes) {
+            val excludeAllTypesConstraint = ctx.mkAnd(typeConstraints.map { ctx.mkNot(it) })
+            typeConstraintsWithBlockOnStates += excludeAllTypesConstraint to { } // do nothing, just exclude types
+        }
+
+        scope.forkMulti(typeConstraintsWithBlockOnStates)
     }
 
     private fun approximateMethod(scope: JcStepScope, methodCall: JcMethodCall): Boolean {
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcStaticFieldsRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcStaticFieldsRegion.kt
new file mode 100644
index 0000000000..95d9334334
--- /dev/null
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcStaticFieldsRegion.kt
@@ -0,0 +1,68 @@
+package org.usvm.machine.interpreter
+
+import io.ksmt.utils.cast
+import kotlinx.collections.immutable.PersistentMap
+import kotlinx.collections.immutable.persistentHashMapOf
+import org.jacodb.api.JcRefType
+import org.jacodb.api.JcField
+import org.jacodb.api.ext.toType
+import org.jacodb.impl.cfg.util.isPrimitive
+import org.usvm.UBoolExpr
+import org.usvm.UExpr
+import org.usvm.USort
+import org.usvm.api.makeSymbolicPrimitive
+import org.usvm.machine.JcContext
+import org.usvm.machine.state.JcState
+import org.usvm.memory.ULValue
+import org.usvm.memory.UMemoryRegion
+import org.usvm.memory.UMemoryRegionId
+import org.usvm.memory.guardedWrite
+import org.usvm.sampleUValue
+
+data class JcStaticFieldLValue<Sort : USort>(
+    val field: JcField,
+    val ctx: JcContext,
+    override val sort: Sort,
+) : ULValue<JcStaticFieldLValue<Sort>, Sort> {
+    override val memoryRegionId: UMemoryRegionId<JcStaticFieldLValue<Sort>, Sort> =
+        // Do not use the presented sort here - we always write and read using voidSort
+        JcStaticFieldRegionId(field.enclosingClass.toType(), ctx.voidSort).cast()
+
+    override val key: JcStaticFieldLValue<Sort>
+        get() = this
+}
+
+data class JcStaticFieldRegionId(
+    private val type: JcRefType,
+    override val sort: USort, // this sort does not matter as it is not used
+) : UMemoryRegionId<JcStaticFieldLValue<USort>, USort> {
+    override fun emptyRegion(): UMemoryRegion<JcStaticFieldLValue<USort>, USort> = JcStaticFieldsMemoryRegion(type)
+}
+
+internal class JcStaticFieldsMemoryRegion(
+    private val type: JcRefType, // this property doesn't matter and is useful only for debugging
+    private var classFieldValues: PersistentMap<JcField, UExpr<USort>> = persistentHashMapOf(),
+) : UMemoryRegion<JcStaticFieldLValue<USort>, USort> {
+    override fun read(key: JcStaticFieldLValue<USort>): UExpr<USort> = classFieldValues[key.field] ?: key.sort.sampleUValue()
+
+    override fun write(
+        key: JcStaticFieldLValue<USort>,
+        value: UExpr<USort>,
+        guard: UBoolExpr
+    ): UMemoryRegion<JcStaticFieldLValue<USort>, USort> {
+        val newFieldValues = classFieldValues.guardedWrite(key.field, value, guard) { key.sort.sampleUValue() }
+
+        return JcStaticFieldsMemoryRegion(type, newFieldValues)
+    }
+
+    fun mutatePrimitiveStaticFieldValuesToSymbolic(state: JcState) {
+        val mutablePrimitiveStaticFieldsToSymbolicValues = classFieldValues.entries.filter { (field, _) ->
+            field.type.isPrimitive && !field.isFinal
+        }.associate { (field, value) ->
+            field to state.makeSymbolicPrimitive(value.sort)
+        }
+
+        // Mutate field values in place because we do not have any LValue to write on it into memory
+        classFieldValues = classFieldValues.putAll(mutablePrimitiveStaticFieldsToSymbolicValues)
+    }
+}
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt
index e947887632..066c9ded34 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/state/JcState.kt
@@ -20,7 +20,7 @@ class JcState(
     models: List<UModelBase<JcType>> = listOf(),
     override var pathLocation: PathsTrieNode<JcState, JcInst> = ctx.mkInitialLocation(),
     var methodResult: JcMethodResult = JcMethodResult.NoCall,
-    targets: List<JcTarget> = emptyList()
+    targets: List<JcTarget> = emptyList(),
 ) : UState<JcType, JcMethod, JcInst, JcContext, JcTarget, JcState>(
     ctx,
     callStack,
@@ -40,7 +40,7 @@ class JcState(
             models,
             pathLocation,
             methodResult,
-            targetsImpl
+            targetsImpl,
         )
     }
 
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 78f96eff04..4dafd26f58 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
@@ -57,17 +57,6 @@ fun JcState.throwExceptionAndDropStackFrame() {
     }
 }
 
-fun JcState.addEntryMethodCall(
-    applicationGraph: JcApplicationGraph,
-    methodCall: JcMethodEntrypointInst,
-) {
-    val method = methodCall.method
-    val entryPoint = applicationGraph.entryPoints(method).single()
-    callStack.push(method, returnSite = null)
-    memory.stack.push(method.parametersWithThisCount, method.localsCount)
-    newStmt(entryPoint)
-}
-
 fun JcState.addNewMethodCall(
     applicationGraph: JcApplicationGraph,
     methodCall: JcConcreteMethodCallInst
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt b/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt
index 8919648d52..c31085efd7 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/util/Utils.kt
@@ -1,7 +1,12 @@
 package org.usvm.util
 
+import org.jacodb.api.JcClassOrInterface
 import org.jacodb.api.JcRefType
 import org.jacodb.api.JcType
+import org.jacodb.api.JcTypedField
+import org.jacodb.api.ext.findFieldOrNull
+import org.jacodb.api.ext.toType
+import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.machine.JcContext
@@ -14,7 +19,13 @@ fun JcContext.extractJcType(clazz: KClass<*>): JcType = cp.findTypeOrNull(clazz.
 
 fun JcContext.extractJcRefType(clazz: KClass<*>): JcRefType = extractJcType(clazz) as JcRefType
 
+val JcClassOrInterface.enumValuesField: JcTypedField
+    get() = toType().findFieldOrNull("\$VALUES") ?: error("No \$VALUES field found for the enum type $this")
+
 @Suppress("UNCHECKED_CAST")
 fun UWritableMemory<*>.write(ref: ULValue<*, *>, value: UExpr<*>) {
     write(ref as ULValue<*, USort>, value as UExpr<USort>, value.uctx.trueExpr)
 }
+
+internal fun UWritableMemory<JcType>.allocHeapRef(type: JcType, useStaticAddress: Boolean): UConcreteHeapRef =
+    if (useStaticAddress) allocStatic(type) else allocConcrete(type)
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java b/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java
index b5fe513b58..66cbaef429 100644
--- a/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/enums/ClassWithEnum.java
@@ -22,7 +22,6 @@ public int useGetter(String s) {
         }
     }
 
-    @SuppressWarnings("UnnecessaryLocalVariable")
     public int useEnumInDifficultIf(String s) {
         if ("TRYIF".equalsIgnoreCase(s)) {
             final ManyConstantsEnum[] values = ManyConstantsEnum.values();
@@ -51,7 +50,7 @@ public int nullField(StatusEnum statusEnum) {
         // catch NPE
         statusEnum.s.length();
 
-        statusEnum.s = "404";
+        statusEnum.s = "-200";
         return statusEnum.s.length();
     }
 
@@ -62,6 +61,8 @@ public int changeEnum(StatusEnum statusEnum) {
             statusEnum = StatusEnum.READY;
         }
 
+        // ERROR -> READY -> 0
+        // READY -> ERROR -> 1
         return statusEnum.ordinal();
     }
 
@@ -102,7 +103,8 @@ public int virtualFunction(StatusEnum parameter) {
         return Math.abs(value);
     }
 
-    enum StatusEnum {
+    @SuppressWarnings("LombokGetterMayBeUsed")
+    public enum StatusEnum {
         READY(0, 10, "200") {
             @Override
             public int virtualFunction() {
@@ -141,7 +143,7 @@ static StatusEnum fromCode(int code) {
                 }
             }
 
-            throw new IllegalArgumentException("No enum corresponding to given code: " + code);
+            throw new IllegalArgumentException("No enum corresponding to given code");
         }
 
         static StatusEnum fromIsReady(boolean isReady) {
@@ -204,6 +206,7 @@ static void invokeIncrementStatic() {
 
     public int implementingInterfaceEnumInDifficultBranch(String s) {
         if ("SUCCESS".equalsIgnoreCase(s)) {
+            //noinspection ConstantValue
             return EnumImplementingInterface.x + EnumImplementingInterface.A_INHERITOR.ordinal();
         } else {
             return EnumImplementingInterface.y + EnumImplementingInterface.B_INHERITOR.ordinal();
@@ -239,7 +242,7 @@ boolean affectSystemStaticAndInitEnumFromItAndGetItFromEnumFun() {
         return OuterStaticUsageEnum.A.getOuterStatic() != prevStaticValue;
     }
 
-    static int staticInt = 0;
+    static int staticInt = 42;
 
     enum OuterStaticUsageEnum {
         A;
@@ -260,4 +263,17 @@ public String toString() {
             return String.format("%s(y = %d)", name(), y);
         }
     }
+
+    @SuppressWarnings("unused")
+    int takeTwoEnumParameters(OuterStaticUsageEnum first, StatusEnum second, StatusEnum third) {
+        // For this method we should analyze static initializers for classes of all arguments, even though the first argument is unused
+        if (second == null) return 1;
+        if (third == null) return 2;
+
+        if (second != third) {
+            return 0;
+        } else {
+            return -1;
+        }
+    }
 }
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/enums/ComplexEnumExamples.java b/usvm-jvm/src/samples/java/org/usvm/samples/enums/ComplexEnumExamples.java
index eef6af49a3..5a77742066 100644
--- a/usvm-jvm/src/samples/java/org/usvm/samples/enums/ComplexEnumExamples.java
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/enums/ComplexEnumExamples.java
@@ -5,6 +5,11 @@
 import java.util.HashMap;
 import java.util.Map;
 
+import static org.usvm.samples.enums.ComplexEnumExamples.Color.BLUE;
+import static org.usvm.samples.enums.ComplexEnumExamples.Color.GREEN;
+import static org.usvm.samples.enums.ComplexEnumExamples.Color.RED;
+import static org.usvm.samples.enums.SimpleEnumExample.SUCCESS;
+
 public class ComplexEnumExamples {
 
     public enum Color {
@@ -32,6 +37,7 @@ public int countEqualColors(@NotNull Color a, @NotNull Color b, @NotNull Color c
             equalToB++;
         }
 
+        //noinspection ManualMinMaxCalculation
         if (equalToA > equalToB) {
             return equalToA;
         } else {
@@ -55,7 +61,7 @@ public int countNullColors(Color a, Color b) {
     public int enumToEnumMapCountValues(@NotNull Map<Color, Color> map) {
         int count = 0;
         for (Color color: map.values()) {
-            if (color == Color.RED) {
+            if (color == RED) {
                 count++;
             }
         }
@@ -65,7 +71,8 @@ public int enumToEnumMapCountValues(@NotNull Map<Color, Color> map) {
     public int enumToEnumMapCountKeys(@NotNull Map<Color, Color> map) {
         int count = 0;
         for (Color key: map.keySet()) {
-            if (key == Color.GREEN || Color.BLUE.equals(key)) {
+            //noinspection StatementWithEmptyBody
+            if (key == GREEN || BLUE.equals(key)) {
                 count++;
             } else {
                 // Do nothing
@@ -102,10 +109,47 @@ public Map<Color, Integer> countValuesInArray(Color @NotNull [] colors) {
     public int countRedInArray(@NotNull Color @NotNull [] colors) {
         int count = 0;
         for (Color c : colors) {
-            if (c == Color.RED) {
+            if (c == RED) {
                 count++;
             }
         }
         return count;
     }
+
+    public String customEnumName(CustomEnum customEnum) {
+        if (customEnum == null) {
+            return "";
+        }
+
+        return customEnum.name();
+    }
+
+    public int enumCustomField(SimpleEnumExample e) {
+        if (e == null) {
+            return 42;
+        }
+
+        return e.x;
+    }
+
+    public String enumName(SimpleEnumExample e) {
+        if (e == null) {
+            return "";
+        }
+
+        if (e == SUCCESS) {
+            return "S";
+        }
+
+        return e.name();
+    }
+
+    @SuppressWarnings("unused")
+    public int unusedEnumParameter(SimpleEnumExample e) {
+        if (e == null) {
+            return 0;
+        }
+
+        return 42;
+    }
 }
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/enums/CustomEnum.java b/usvm-jvm/src/samples/java/org/usvm/samples/enums/CustomEnum.java
new file mode 100644
index 0000000000..86f3ee5b80
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/enums/CustomEnum.java
@@ -0,0 +1,43 @@
+package org.usvm.samples.enums;
+
+public class CustomEnum {
+    private static final CustomEnum[] values = new CustomEnum[2];
+    public static final CustomEnum VALUE1 = new CustomEnum("VALUE1");
+    public static final CustomEnum VALUE2 = new CustomEnum("VALUE2");
+
+    private static int counter = 0;
+    private final String name;
+    private final int ordinal;
+
+    private CustomEnum(String name) {
+        this.name = name;
+        this.ordinal = counter;
+        values[counter++] = this;
+    }
+
+    public static CustomEnum[] values() {
+        return values.clone();
+    }
+
+    public static CustomEnum valueOf(String name) {
+        for (CustomEnum customEnum : values) {
+            if (customEnum.name.equals(name)) {
+                return customEnum;
+            }
+        }
+        throw new IllegalArgumentException("No enum constant with name " + name);
+    }
+
+    public String name() {
+        return name;
+    }
+
+    public int ordinal() {
+        return ordinal;
+    }
+
+    @Override
+    public String toString() {
+        return String.format("CustomEnum: {name: %s, ordinal: %d}", name, ordinal);
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/enums/SimpleEnumExample.java b/usvm-jvm/src/samples/java/org/usvm/samples/enums/SimpleEnumExample.java
new file mode 100644
index 0000000000..fb6cd4a264
--- /dev/null
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/enums/SimpleEnumExample.java
@@ -0,0 +1,16 @@
+package org.usvm.samples.enums;
+
+public enum SimpleEnumExample {
+    SUCCESS(10), ERROR(-10);
+
+    final int x;
+
+    SimpleEnumExample(int x) {
+        this.x = x;
+    }
+
+    @Override
+    public String toString() {
+        return String.format("Enum: {name: %s, x: %d, ordinal: %d}", name(), x, ordinal());
+    }
+}
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithStatics.java b/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithStatics.java
index c7fca63153..2ed228a94e 100644
--- a/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithStatics.java
+++ b/usvm-jvm/src/samples/java/org/usvm/samples/objects/ObjectWithStatics.java
@@ -3,11 +3,13 @@
 public class ObjectWithStatics {
     static Object refStaticField;
 
-    static int primitiveStaticField;
+    static int mutablePrimitiveStaticField;
+    final static int finalPrimitiveStaticField;
 
     static {
         refStaticField = new Object();
-        primitiveStaticField = 17;
+        mutablePrimitiveStaticField = 17;
+        finalPrimitiveStaticField = 42;
     }
 
     private Object getRefFiled() {
@@ -15,14 +17,14 @@ private Object getRefFiled() {
     }
 
     private int getPrimitiveFiled() {
-        return primitiveStaticField;
+        return mutablePrimitiveStaticField;
     }
 
     int staticsAreEqual() {
         if (ObjectWithStatics.refStaticField != getRefFiled()) {
             return 1;
         }
-        if (ObjectWithStatics.primitiveStaticField != getPrimitiveFiled()) {
+        if (ObjectWithStatics.mutablePrimitiveStaticField != getPrimitiveFiled()) {
             return 2;
         }
         return 0;
@@ -30,15 +32,26 @@ int staticsAreEqual() {
 
     int mutateStatics() {
         int initial = getPrimitiveFiled();
-        primitiveStaticField++;
+        mutablePrimitiveStaticField++;
         int mutated = getPrimitiveFiled();
         return mutated - initial;
     }
 
-    int staticsInitialized() {
-        if (ObjectWithStatics.primitiveStaticField != 17) {
+    int useMutablePrimitiveStaticField() {
+        if (ObjectWithStatics.mutablePrimitiveStaticField != 17) {
+            // The static field primitiveStaticField is mutable primitive, so this stmt is reachable
             return 1;
         }
+
+        return 0;
+    }
+
+    int useFinalPrimitiveStaticField() {
+        if (ObjectWithStatics.finalPrimitiveStaticField != 42) {
+            // We consider final primitive static fields as immutable, so this stmt is unreachable
+            return 1;
+        }
+
         return 0;
     }
 }
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 ae4145dcba..4592ef9032 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
@@ -134,6 +134,7 @@ internal class InstanceOfExampleTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("TODO fix type streams: USupportTypeStream.from(Object[]).filterBySupertype(anyType)")
     fun testInstanceOfAsPartOfInternalExpressionsCastClass() {
         checkDiscoveredProperties(
             InstanceOfExample::instanceOfAsPartOfInternalExpressionsCastClass,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt
index b439473632..e1c1d0684f 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/codegen/JavaAssertTest.kt
@@ -1,6 +1,5 @@
 package org.usvm.samples.codegen
 
-import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
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 e3d6dde6f9..d767ac1240 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,11 +8,11 @@ import org.usvm.test.util.checkers.eq
 
 class DeepEqualsTest : JavaMethodTestRunner() {
     @Test
-    @Disabled("An operation is not implemented: Class constant")
     fun testReturnList() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::returnList,
             eq(1),
+            { _, r -> r!!.size == 2 }
         )
     }
 
@@ -26,10 +26,12 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("No successful execution")
     fun testReturnMap() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::returnMap,
             eq(1),
+            { _, r ->  r!!.isCorrectMap() }
         )
     }
 
@@ -49,7 +51,6 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("An operation is not implemented: Class constant")
     fun testReturn2DList() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::return2DList,
@@ -67,18 +68,22 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
+    @Disabled("No successful execution")
     fun testReturn2DMap() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::return2DMap,
             eq(1),
+            { _, r -> r!!.size == 2 && r.keys.toSortedSet() == sortedSetOf(0, 1) && r.values.all { it.isCorrectMap() } }
         )
     }
 
     @Test
+    @Disabled("No successful execution")
     fun testIntegers2DList() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::returnIntegers2DList,
             eq(1),
+            { _, r -> r!!.size == 2 && r.all { it == listOf(1) } }
         )
     }
 
@@ -160,7 +165,6 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Support multidimensional arrays initialization")
     fun testDoubleMultiArray() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::fillDoubleMultiArrayWithConstValue,
@@ -169,7 +173,6 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Support multidimensional arrays initialization")
     fun testIntegerWrapperMultiArray() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::fillIntegerWrapperMultiArrayWithConstValue,
@@ -178,7 +181,6 @@ class DeepEqualsTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Support multidimensional arrays initialization")
     fun testDoubleWrapperMultiArray() {
         checkDiscoveredProperties(
             DeepEqualsTestingClass::fillDoubleWrapperMultiArrayWithConstValue,
@@ -190,3 +192,7 @@ class DeepEqualsTest : JavaMethodTestRunner() {
 private fun Array<Array<IntArray>>.flatten(): List<Int> = flatMap {
     row -> row.flatMap { it.toList() }
 }
+
+private fun Map<Int, DeepEqualsTestingClass>.isCorrectMap(): Boolean {
+    return size == 2 && keys.toSortedSet() == sortedSetOf(0, 1)
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt
index 9d9dd31921..0ca397583a 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/controlflow/SwitchTest.kt
@@ -3,9 +3,8 @@ package org.usvm.samples.controlflow
 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 java.math.RoundingMode.CEILING
 import java.math.RoundingMode.DOWN
 import java.math.RoundingMode.HALF_DOWN
@@ -50,15 +49,14 @@ internal class SwitchTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Index 1 out of bounds for length 1")
-    fun testEnumSwitch() {
+    fun testRoundingModeSwitch() {
         checkDiscoveredProperties(
             Switch::enumSwitch,
-            eq(7),
+            ignoreNumberOfAnalysisResults,
             { _, m, _ -> m == null }, // NPE
             { _, m, r -> m == HALF_DOWN && r == 1 }, // We will minimize two of these branches
-            { _, m, r -> m == HALF_EVEN && r == 1 }, // We will minimize two of these branches
-            { _, m, r -> m == HALF_UP && r == 1 }, // We will minimize two of these branches
+//            { _, m, r -> m == HALF_EVEN && r == 1 }, // We will minimize two of these branches
+//            { _, m, r -> m == HALF_UP && r == 1 }, // We will minimize two of these branches
             { _, m, r -> m == DOWN && r == 2 },
             { _, m, r -> m == CEILING && r == 3 },
             { _, m, r -> m !in setOf(HALF_DOWN, HALF_EVEN, HALF_UP, DOWN, CEILING) && r == -1 },
@@ -82,7 +80,7 @@ internal class SwitchTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("An operation is not implemented: Not yet implemented. Support strings")
+    @Disabled("Exceeds timeout")
     fun testStringSwitch() {
         checkDiscoveredProperties(
             Switch::stringSwitch,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt
index b74e85ebd6..5e2b6114ea 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ClassWithEnumTest.kt
@@ -23,7 +23,6 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
 //    }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
     fun testGetter() {
         checkDiscoveredProperties(
             ClassWithEnum::useGetter,
@@ -34,7 +33,7 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 0 out of bounds for length 0")
+    @Disabled("Log message invocation failed: java.lang.NullPointerException")
     fun testDifficultIfBranch() {
         checkDiscoveredProperties(
             ClassWithEnum::useEnumInDifficultIf,
@@ -45,30 +44,27 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [1]. Support enums")
     fun testNullParameter() {
         checkDiscoveredProperties(
             ClassWithEnum::nullEnumAsParameter,
             between(2..3),
             { _, e, _ -> e == null },
-            { _, e, r -> e == READY && r == 0 || e == ERROR && r == -1 },
+            { _, e, r -> e == READY && r == 0 || e == ERROR && r == 1 },
         )
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
     fun testNullField() {
         checkDiscoveredPropertiesWithExceptions(
             ClassWithEnum::nullField,
             eq(3),
             { _, e, r -> e == null && r.isException<NullPointerException>() },
             { _, e, r -> e == ERROR && r.isException<NullPointerException>() },
-            { _, e, r -> e == READY && r.getOrNull()!! == 3 && READY.s.length == 3 },
+            { _, e, r -> e == READY && r.getOrNull()!! == 4 },
         )
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
     fun testChangeEnum() {
         checkDiscoveredPropertiesWithExceptions(
             ClassWithEnum::changeEnum,
@@ -79,7 +75,6 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
     fun testChangeMutableField() {
         checkDiscoveredPropertiesWithExceptions(
             ClassWithEnum::changeMutableField,
@@ -90,7 +85,7 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
+    @Disabled("Expected exactly 3 executions, but 8 found")
     fun testCheckName() {
         checkDiscoveredProperties(
             ClassWithEnum::checkName,
@@ -149,7 +144,6 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
 //    }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
     fun testFromCode() {
         checkDiscoveredProperties(
             StatusEnum::fromCode,
@@ -161,7 +155,6 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
     fun testFromIsReady() {
         checkDiscoveredProperties(
             StatusEnum::fromIsReady,
@@ -172,7 +165,6 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 3 out of bounds for length 3")
     fun testPublicGetCodeMethod() {
         checkThisAndParamsMutations(
             StatusEnum::publicGetCode,
@@ -183,7 +175,7 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 0 out of bounds for length 0")
+    @Disabled("Log message invocation failed: java.lang.NullPointerException")
     fun testImplementingInterfaceEnumInDifficultBranch() {
         checkDiscoveredProperties(
             ClassWithEnum::implementingInterfaceEnumInDifficultBranch,
@@ -194,7 +186,6 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled(" Index 0 out of bounds for length 0")
     fun testAffectSystemStaticAndUseInitEnumFromIt() {
         checkDiscoveredProperties(
             ClassWithEnum::affectSystemStaticAndInitEnumFromItAndReturnField,
@@ -204,7 +195,6 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled(" Index 0 out of bounds for length 0")
     fun testAffectSystemStaticAndInitEnumFromItAndGetItFromEnumFun() {
         checkDiscoveredProperties(
             ClassWithEnum::affectSystemStaticAndInitEnumFromItAndGetItFromEnumFun,
@@ -212,4 +202,18 @@ class ClassWithEnumTest : JavaMethodTestRunner() {
             { _, r -> r == true },
         )
     }
-}
\ No newline at end of file
+
+    @Test
+    fun twoEnumParameters() {
+        checkDiscoveredProperties(
+            ClassWithEnum::takeTwoEnumParameters,
+            eq(4),
+            { _, _, second, third, r ->
+                second != null && third != null && second == third && r == -1
+            },
+            { _, _, second, third, r ->
+                second != null && third != null && second != third && r == 0
+            }
+        )
+    }
+}
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ComplexEnumExamplesTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ComplexEnumExamplesTest.kt
index 1eef02ef85..8f8648583d 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ComplexEnumExamplesTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/enums/ComplexEnumExamplesTest.kt
@@ -7,13 +7,13 @@ import org.usvm.samples.enums.ComplexEnumExamples.Color
 import org.usvm.samples.enums.ComplexEnumExamples.Color.BLUE
 import org.usvm.samples.enums.ComplexEnumExamples.Color.GREEN
 import org.usvm.samples.enums.ComplexEnumExamples.Color.RED
+import org.usvm.samples.enums.SimpleEnumExample.*
 import org.usvm.test.util.checkers.eq
 import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
 
-
 class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [1, 2]")
+    @Disabled("Hangs")
     fun testEnumToEnumMapCountValues() {
         checkDiscoveredProperties(
             ComplexEnumExamples::enumToEnumMapCountValues,
@@ -25,7 +25,7 @@ class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("No result found")
+    @Disabled("Exceeds timeout")
     fun testEnumToEnumMapCountKeys() {
         checkDiscoveredProperties(
             ComplexEnumExamples::enumToEnumMapCountKeys,
@@ -40,7 +40,7 @@ class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("No result found")
+    @Disabled("Exceeds timeout")
     fun testEnumToEnumMapCountMatches() {
         checkDiscoveredProperties(
             ComplexEnumExamples::enumToEnumMapCountMatches,
@@ -51,7 +51,7 @@ class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [0]")
+    @Disabled("TODO the first matcher does not matches. Discover whether it should or not - perhaps it's an issue with calculating coverage.")
     fun testCountEqualColors() {
         checkDiscoveredProperties(
             ComplexEnumExamples::countEqualColors,
@@ -63,7 +63,7 @@ class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [0]")
+    @Disabled("TODO the first matcher does not matches. Discover whether it should or not - perhaps it's an issue with calculating coverage.")
     fun testCountNullColors() {
         checkDiscoveredProperties(
             ComplexEnumExamples::countNullColors,
@@ -75,7 +75,6 @@ class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("JcTypedMethodImpl.getParameters: Index 1 out of bounds for length 1")
     fun testFindState() {
         checkDiscoveredProperties(
             ComplexEnumExamples::findState,
@@ -85,7 +84,7 @@ class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [2]")
+    @Disabled("Exceeds timeout")
     fun testCountValuesInArray() {
         fun Color.isCorrectlyCounted(inputs: Array<Color>, counts: Map<Color, Int>): Boolean =
             inputs.count { it == this } == (counts[this] ?: 0)
@@ -100,12 +99,52 @@ class ComplexEnumExamplesTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled(" Index 0 out of bounds for length 0")
     fun testCountRedInArray() {
         checkDiscoveredProperties(
             ComplexEnumExamples::countRedInArray,
-            eq(3),
+            ignoreNumberOfAnalysisResults,
             { _, colors, result -> colors.count { it == RED } == result }
         )
     }
+
+    @Test
+    @Disabled("TODO this test cannot be supported for now - it uses an `artificial` enum.")
+    fun testCustomEnumName() {
+        checkDiscoveredProperties(
+            ComplexEnumExamples::customEnumName,
+            ignoreNumberOfAnalysisResults,
+            { _, m, s -> m == null && s == "" },
+            { _, m, r -> (m == CustomEnum.VALUE1 || m == CustomEnum.VALUE2) && m.name() == r }
+        )
+    }
+
+    @Test
+    fun testEnumCustomField() {
+        checkDiscoveredProperties(
+            ComplexEnumExamples::enumCustomField,
+            ignoreNumberOfAnalysisResults,
+            { _, m, r -> m == null && r == 42 },
+            { _, m, r -> (m == SUCCESS || m == ERROR) && m.x == r }
+        )
+    }
+
+    @Test
+    fun testEnumName() {
+        checkDiscoveredProperties(
+            ComplexEnumExamples::enumName,
+            ignoreNumberOfAnalysisResults,
+            { _, m, s -> m == null && s == "" },
+            { _, m, r -> (m == SUCCESS || m == ERROR) && m.name == r }
+        )
+    }
+
+    @Test
+    fun testUnusedEnumParameter() {
+        checkDiscoveredProperties(
+            ComplexEnumExamples::unusedEnumParameter,
+            ignoreNumberOfAnalysisResults,
+            { _, m, r -> m == null && r == 0 },
+            { _, m, r -> (m == SUCCESS || m == ERROR) && r == 42 }
+        )
+    }
 }
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SerializableExampleTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SerializableExampleTest.kt
index 7c6ee2bd4c..444a72e285 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SerializableExampleTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/mixed/SerializableExampleTest.kt
@@ -5,14 +5,14 @@ import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
 
-
 internal class SerializableExampleTest : JavaMethodTestRunner() {
-
     @Test
+    @Disabled("Only 1 execution - NPE")
     fun testExample() {
-        checkDiscoveredProperties(
+        checkDiscoveredPropertiesWithExceptions(
             SerializableExample::example,
             eq(1),
+            { _, r -> r.isSuccess }
         )
     }
 }
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ClassForTestClinitSectionsTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ClassForTestClinitSectionsTest.kt
index 47d1678c8f..9a6a82befa 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ClassForTestClinitSectionsTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/ClassForTestClinitSectionsTest.kt
@@ -21,7 +21,6 @@ internal class ClassForTestClinitSectionsTest : JavaMethodTestRunner() {
 //        }
 
     @Test
-    @Disabled("Expected exactly 2 executions, but 1 found") // todo: treat statics as input values
     fun testClinitWithClinitAnalysis() {
         checkDiscoveredProperties(
             ClassForTestClinitSections::resultDependingOnStaticSection,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/TestStatics.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/TestStatics.kt
index 7fe1e0c432..89f7286420 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/TestStatics.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/objects/TestStatics.kt
@@ -24,9 +24,19 @@ class TestStatics : JavaMethodTestRunner() {
     }
 
     @Test
-    fun `Test static initializer`() {
+    fun `Test mutable primitive static field`() {
         checkDiscoveredProperties(
-            ObjectWithStatics::staticsInitialized,
+            ObjectWithStatics::useMutablePrimitiveStaticField,
+            eq(2),
+            { _, r -> r == 0 },
+            { _, r -> r == 1 },
+        )
+    }
+
+    @Test
+    fun `Test final primitive static field`() {
+        checkDiscoveredProperties(
+            ObjectWithStatics::useFinalPrimitiveStaticField,
             eq(1),
             { _, r -> r == 0 },
         )
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/substitution/StaticsSubstitutionTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/substitution/StaticsSubstitutionTest.kt
index 9d8181437c..d7200cff91 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/substitution/StaticsSubstitutionTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/substitution/StaticsSubstitutionTest.kt
@@ -1,6 +1,5 @@
 package org.usvm.samples.substitution
 
-import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
@@ -9,7 +8,6 @@ import org.usvm.test.util.checkers.eq
 class StaticsSubstitutionTest : JavaMethodTestRunner() {
 
     @Test
-    @Disabled("Expected exactly 2 executions, but 1 found") // todo: treat static fields as input values
     fun lessThanZeroWithSubstitution() {
         checkDiscoveredProperties(
             StaticSubstitutionExamples::lessThanZero,
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt
index 16abae13ed..c0efa82e9a 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/BooleanWrapperTest.kt
@@ -1,6 +1,5 @@
 package org.usvm.samples.wrappers
 
-import org.junit.jupiter.api.Disabled
 import org.junit.jupiter.api.Test
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/IntegerWrapperTest.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/IntegerWrapperTest.kt
index f9f2b74f65..279c9a97a2 100644
--- a/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/IntegerWrapperTest.kt
+++ b/usvm-jvm/src/test/kotlin/org/usvm/samples/wrappers/IntegerWrapperTest.kt
@@ -31,7 +31,6 @@ internal class IntegerWrapperTest : JavaMethodTestRunner() {
     }
 
     @Test
-    @Disabled("Some properties were not discovered at positions (from 0): [2]")
     fun numberOfZerosTest() {
         checkDiscoveredProperties(
             IntegerWrapper::numberOfZeros,
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 e874e73ab9..248e48be95 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
@@ -85,7 +85,7 @@ class SampleExprResolver(
     fun resolveStruct(expr: StructExpr): UHeapRef? = with(ctx) {
         when (expr) {
             is StructCreation -> {
-                val ref = scope.calcOnState { memory.alloc(expr.type) }
+                val ref = scope.calcOnState { memory.allocConcrete(expr.type) }
 
                 for ((field, fieldExpr) in expr.fields) {
                     val sort = typeToSort(field.type)
diff --git a/usvm-util/src/main/kotlin/org/usvm/algorithms/DisjointSets.kt b/usvm-util/src/main/kotlin/org/usvm/algorithms/DisjointSets.kt
index 2eea0ca506..9b29d09eaa 100644
--- a/usvm-util/src/main/kotlin/org/usvm/algorithms/DisjointSets.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/algorithms/DisjointSets.kt
@@ -11,8 +11,10 @@ class DisjointSets<T> private constructor(
     private val parent: MutableMap<T, T>,
     private val rank: MutableMap<T, Int>,
     private var unionCallback: ((T, T) -> Unit)?,
+    private val representativeSelector: RepresentativeSelector<T>?
 ) : Iterable<Map.Entry<T, T>> by parent.entries {
-    constructor() : this(mutableMapOf(), mutableMapOf(), unionCallback = null)
+    constructor(representativeSelector: RepresentativeSelector<T>? = null) :
+            this(mutableMapOf(), mutableMapOf(), unionCallback = null, representativeSelector)
 
     /**
      * Returns representative of set containing [x].
@@ -48,6 +50,20 @@ class DisjointSets<T> private constructor(
             return
         }
 
+        representativeSelector?.let {
+            if (it.shouldSelectAsRepresentative(u)) {
+                merge(u, v)
+
+                return
+            }
+
+            if (it.shouldSelectAsRepresentative(v)) {
+                merge(v, u)
+
+                return
+            }
+        }
+
         val rankU = rank[u] ?: 0
         val rankV = rank[v] ?: 0
 
@@ -83,5 +99,12 @@ class DisjointSets<T> private constructor(
      * Creates a copy of this structure.
      * Note that current subscribers get unsubscribed!
      */
-    fun clone() = DisjointSets(parent.toMutableMap(), rank.toMutableMap(), unionCallback = null)
+    fun clone() = DisjointSets(parent.toMutableMap(), rank.toMutableMap(), unionCallback = null, representativeSelector)
+
+    /**
+     * Determines what values should be selected as representative during merging.
+     */
+    fun interface RepresentativeSelector<T> {
+        fun shouldSelectAsRepresentative(value: T): Boolean
+    }
 }