diff --git a/usvm-core/src/main/kotlin/org/usvm/Composition.kt b/usvm-core/src/main/kotlin/org/usvm/Composition.kt
index bf9463c1b7..0540dc988d 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Composition.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Composition.kt
@@ -1,5 +1,9 @@
 package org.usvm
 
+import org.usvm.memory.UReadOnlySymbolicHeap
+import org.usvm.memory.URegionId
+import org.usvm.memory.URegistersStackEvaluator
+
 @Suppress("MemberVisibilityCanBePrivate")
 open class UComposer<Field, Type>(
     ctx: UContext,
diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt
index 11c8578a98..fa112a5130 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Context.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt
@@ -11,6 +11,11 @@ import org.ksmt.sort.KUninterpretedSort
 import org.ksmt.utils.DefaultValueSampler
 import org.ksmt.utils.asExpr
 import org.ksmt.utils.cast
+import org.usvm.memory.UAllocatedArrayRegion
+import org.usvm.memory.UInputArrayLengthRegion
+import org.usvm.memory.UInputArrayRegion
+import org.usvm.memory.UInputFieldRegion
+import org.usvm.memory.splitUHeapRef
 
 @Suppress("LeakingThis")
 open class UContext(
diff --git a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
index e5eb5927a6..caf6eae659 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Expressions.kt
@@ -6,6 +6,17 @@ import org.ksmt.expr.*
 import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.sort.*
+import org.usvm.memory.UAllocatedArrayId
+import org.usvm.memory.UAllocatedArrayRegion
+import org.usvm.memory.UInputArrayId
+import org.usvm.memory.UInputArrayLengthId
+import org.usvm.memory.UInputArrayLengthRegion
+import org.usvm.memory.UInputArrayRegion
+import org.usvm.memory.UInputFieldId
+import org.usvm.memory.UInputFieldRegion
+import org.usvm.memory.URegionId
+import org.usvm.memory.USymbolicArrayIndex
+import org.usvm.memory.USymbolicMemoryRegion
 
 //region KSMT aliases
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/Merging.kt b/usvm-core/src/main/kotlin/org/usvm/Merging.kt
index a2d221fb5b..dbac00d8fe 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Merging.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Merging.kt
@@ -1,5 +1,7 @@
 package org.usvm
 
+import org.usvm.memory.URegionHeap
+
 interface UMerger<Entity> {
     /**
      * @returns Merged entity or null if [left] and [right] are non-mergeable
diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt
index c65f2f5a62..52d79ed588 100644
--- a/usvm-core/src/main/kotlin/org/usvm/State.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/State.kt
@@ -2,6 +2,8 @@ package org.usvm
 
 import kotlinx.collections.immutable.PersistentList
 import org.ksmt.expr.KInterpretedValue
+import org.usvm.memory.UMemoryBase
+import org.usvm.model.UModel
 
 abstract class UState<Type, Field, Method, Statement>(
     // TODO: add interpreter-specific information
diff --git a/usvm-core/src/main/kotlin/org/usvm/Heap.kt b/usvm-core/src/main/kotlin/org/usvm/memory/Heap.kt
similarity index 97%
rename from usvm-core/src/main/kotlin/org/usvm/Heap.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/Heap.kt
index ff96d864d7..e9f7e86c6b 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Heap.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/Heap.kt
@@ -1,8 +1,17 @@
-package org.usvm
+package org.usvm.memory
 
 import kotlinx.collections.immutable.PersistentMap
 import kotlinx.collections.immutable.persistentMapOf
 import org.ksmt.utils.asExpr
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapAddress
+import org.usvm.UConcreteHeapRef
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.USizeExpr
+import org.usvm.USort
+import org.usvm.sampleUValue
 
 interface UReadOnlyHeap<Ref, Value, SizeT, Field, ArrayType, Guard> {
     fun <Sort : USort> readField(ref: Ref, field: Field, sort: Sort): Value
diff --git a/usvm-core/src/main/kotlin/org/usvm/HeapRefSplitting.kt b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt
similarity index 97%
rename from usvm-core/src/main/kotlin/org/usvm/HeapRefSplitting.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt
index 77cfaffabc..6911eeb171 100644
--- a/usvm-core/src/main/kotlin/org/usvm/HeapRefSplitting.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/HeapRefSplitting.kt
@@ -1,4 +1,14 @@
-package org.usvm
+package org.usvm.memory
+
+import org.usvm.UAddressSort
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.UIteExpr
+import org.usvm.USort
+import org.usvm.USymbolicHeapRef
+import org.usvm.isFalse
 
 data class GuardedExpr<out T>(
     val expr: T,
diff --git a/usvm-core/src/main/kotlin/org/usvm/Memory.kt b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
similarity index 92%
rename from usvm-core/src/main/kotlin/org/usvm/Memory.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
index f262946b54..a6e5e230e0 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Memory.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
@@ -1,6 +1,20 @@
-package org.usvm
+package org.usvm.memory
 
 import org.ksmt.utils.asExpr
+import org.usvm.UArrayIndexRef
+import org.usvm.UComposer
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.UFieldRef
+import org.usvm.UHeapRef
+import org.usvm.UIndexedMocker
+import org.usvm.ULValue
+import org.usvm.UMocker
+import org.usvm.URegisterRef
+import org.usvm.USizeExpr
+import org.usvm.USort
+import org.usvm.UTypeStorage
+import org.usvm.UTypeSystem
 
 interface UMemory<LValue, RValue, SizeT, HeapRef, Type> {
     /**
diff --git a/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt
similarity index 96%
rename from usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt
index bc5e7e4ff3..9a44f41ee4 100644
--- a/usvm-core/src/main/kotlin/org/usvm/MemoryRegions.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryRegions.kt
@@ -1,14 +1,31 @@
-package org.usvm
+package org.usvm.memory
 
 import org.ksmt.utils.asExpr
+import org.usvm.UBoolExpr
+import org.usvm.UComposer
+import org.usvm.UConcreteHeapAddress
+import org.usvm.UConcreteHeapRef
+import org.usvm.UConcreteSize
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.UIndexType
+import org.usvm.USizeExpr
+import org.usvm.USizeSort
+import org.usvm.USort
+import org.usvm.sampleUValue
+import org.usvm.uctx
 import org.usvm.util.SetRegion
 import org.usvm.util.emptyRegionTree
 
 //region Memory region
 
 
-interface UMemoryRegion<Key, Sort : USort> {
+interface UReadOnlyMemoryRegion<Key, Sort : USort> {
     fun read(key: Key): UExpr<Sort>
+}
+
+
+interface UMemoryRegion<Key, Sort : USort> : UReadOnlyMemoryRegion<Key, Sort> {
     fun write(key: Key, value: UExpr<Sort>, guard: UBoolExpr): UMemoryRegion<Key, Sort>
 }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt
similarity index 99%
rename from usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt
index 886aff7238..6933c31951 100644
--- a/usvm-core/src/main/kotlin/org/usvm/MemoryUpdates.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/MemoryUpdates.kt
@@ -1,5 +1,10 @@
-package org.usvm
+package org.usvm.memory
 
+import org.usvm.UBoolExpr
+import org.usvm.UComposer
+import org.usvm.UExpr
+import org.usvm.USort
+import org.usvm.isFalse
 import org.usvm.util.Region
 import org.usvm.util.RegionTree
 import org.usvm.util.emptyRegionTree
diff --git a/usvm-core/src/main/kotlin/org/usvm/RegionIds.kt b/usvm-core/src/main/kotlin/org/usvm/memory/RegionIds.kt
similarity index 96%
rename from usvm-core/src/main/kotlin/org/usvm/RegionIds.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/RegionIds.kt
index d36567018f..365fcdc932 100644
--- a/usvm-core/src/main/kotlin/org/usvm/RegionIds.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/RegionIds.kt
@@ -1,6 +1,17 @@
-package org.usvm
+package org.usvm.memory
 
 import org.ksmt.utils.asExpr
+import org.usvm.UBoolExpr
+import org.usvm.UComposer
+import org.usvm.UConcreteHeapAddress
+import org.usvm.UExpr
+import org.usvm.UExprTransformer
+import org.usvm.UHeapRef
+import org.usvm.USizeExpr
+import org.usvm.USizeSort
+import org.usvm.USort
+import org.usvm.isTrue
+import org.usvm.uctx
 
 /**
  * Represents any possible type of regions that can be used in the memory.
diff --git a/usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt b/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
similarity index 95%
rename from usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
index 0b3f326cde..2279232621 100644
--- a/usvm-core/src/main/kotlin/org/usvm/RegistersStack.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
@@ -1,7 +1,10 @@
-package org.usvm
+package org.usvm.memory
 
 import org.ksmt.expr.KExpr
 import org.ksmt.utils.asExpr
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.USort
 import java.util.Stack
 
 interface URegistersStackEvaluator {
diff --git a/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
similarity index 98%
rename from usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt
rename to usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
index a38b843b79..2281bc5b07 100644
--- a/usvm-core/src/main/kotlin/org/usvm/UpdateNodes.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
@@ -1,5 +1,11 @@
-package org.usvm
-
+package org.usvm.memory
+
+import org.usvm.UBoolExpr
+import org.usvm.UComposer
+import org.usvm.UExpr
+import org.usvm.USizeExpr
+import org.usvm.USort
+import org.usvm.isTrue
 import java.util.*
 
 /**
diff --git a/usvm-core/src/main/kotlin/org/usvm/EagerModels.kt b/usvm-core/src/main/kotlin/org/usvm/model/EagerModels.kt
similarity index 83%
rename from usvm-core/src/main/kotlin/org/usvm/EagerModels.kt
rename to usvm-core/src/main/kotlin/org/usvm/model/EagerModels.kt
index a541d59005..b815c565c0 100644
--- a/usvm-core/src/main/kotlin/org/usvm/EagerModels.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/EagerModels.kt
@@ -1,7 +1,24 @@
-package org.usvm
+package org.usvm.model
 
 import org.ksmt.utils.asExpr
 import org.ksmt.utils.sampleValue
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.UIndexedMethodReturnValue
+import org.usvm.UMockEvaluator
+import org.usvm.UMockSymbol
+import org.usvm.USizeExpr
+import org.usvm.USizeSort
+import org.usvm.USort
+import org.usvm.memory.UAddressCounter
+import org.usvm.memory.UMemoryRegion
+import org.usvm.memory.UReadOnlyMemoryRegion
+import org.usvm.memory.URegistersStackEvaluator
+import org.usvm.memory.USymbolicArrayIndex
+import org.usvm.memory.USymbolicHeap
+import org.usvm.uctx
 
 /**
  * An eager model for registers that stores mapping
@@ -52,9 +69,9 @@ class UIndexedMockEagerModel<Method>(
  */
 class UHeapEagerModel<Field, ArrayType>(
     private val nullRef: UConcreteHeapRef,
-    private val resolvedInputFields: Map<Field, UMemoryRegion<UHeapRef, out USort>>,
-    private val resolvedInputArrays: Map<ArrayType, UMemoryRegion<USymbolicArrayIndex, out USort>>,
-    private val resolvedInputLengths: Map<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>,
+    private val resolvedInputFields: Map<Field, UReadOnlyMemoryRegion<UHeapRef, out USort>>,
+    private val resolvedInputArrays: Map<ArrayType, UReadOnlyMemoryRegion<USymbolicArrayIndex, out USort>>,
+    private val resolvedInputLengths: Map<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>,
 ) : USymbolicHeap<Field, ArrayType> {
     override fun <Sort : USort> readField(ref: UHeapRef, field: Field, sort: Sort): UExpr<Sort> {
         // All the expressions in the model are interpreted, therefore, they must
@@ -66,7 +83,7 @@ class UHeapEagerModel<Field, ArrayType>(
         val region = resolvedInputFields.getOrElse(field) {
             // sampleValue here is important
             UMemory1DArray(sort.sampleValue().nullAddress(nullRef))
-        } as UMemoryRegion<UHeapRef, Sort>
+        } as UReadOnlyMemoryRegion<UHeapRef, Sort>
 
         return region.read(ref)
     }
@@ -88,7 +105,7 @@ class UHeapEagerModel<Field, ArrayType>(
         val region = resolvedInputArrays.getOrElse(arrayType) {
             // sampleValue here is important
             UMemory2DArray(sort.sampleValue().nullAddress(nullRef))
-        } as UMemoryRegion<USymbolicArrayIndex, Sort>
+        } as UReadOnlyMemoryRegion<USymbolicArrayIndex, Sort>
 
         return region.read(key)
     }
@@ -99,7 +116,7 @@ class UHeapEagerModel<Field, ArrayType>(
         // which have addresses less or equal than INITIAL_INPUT_ADDRESS
         require(ref is UConcreteHeapRef && ref.address <= UAddressCounter.INITIAL_INPUT_ADDRESS)
 
-        val region = resolvedInputLengths.getOrElse<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>(arrayType) {
+        val region = resolvedInputLengths.getOrElse<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>(arrayType) {
             // sampleValue here is important
             UMemory1DArray(ref.uctx.sizeSort.sampleValue())
         }
diff --git a/usvm-core/src/main/kotlin/org/usvm/LazyModelDecoder.kt b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
similarity index 90%
rename from usvm-core/src/main/kotlin/org/usvm/LazyModelDecoder.kt
rename to usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
index c41951b462..030b106a27 100644
--- a/usvm-core/src/main/kotlin/org/usvm/LazyModelDecoder.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
@@ -1,10 +1,22 @@
-package org.usvm
+package org.usvm.model
 
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.sort.KUninterpretedSort
-import org.usvm.UAddressCounter.Companion.INITIAL_INPUT_ADDRESS
-import org.usvm.UAddressCounter.Companion.NULL_ADDRESS
+import org.usvm.UAddressSort
+import org.usvm.UConcreteHeapRef
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.solver.UExprTranslator
+import org.usvm.UHeapRef
+import org.usvm.USort
+import org.usvm.solver.UTrackingExprTranslator
+import org.usvm.UTypeModel
+import org.usvm.memory.UAddressCounter.Companion.INITIAL_INPUT_ADDRESS
+import org.usvm.memory.UAddressCounter.Companion.NULL_ADDRESS
+import org.usvm.memory.UMemoryBase
+import org.usvm.memory.URegionId
+import org.usvm.uctx
 
 interface UModelDecoder<Memory, Model> {
     fun decode(memory: Memory, model: KModel): Model
diff --git a/usvm-core/src/main/kotlin/org/usvm/LazyModels.kt b/usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt
similarity index 88%
rename from usvm-core/src/main/kotlin/org/usvm/LazyModels.kt
rename to usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt
index 54ddb3b527..00baef982b 100644
--- a/usvm-core/src/main/kotlin/org/usvm/LazyModels.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModels.kt
@@ -1,10 +1,32 @@
-package org.usvm
+package org.usvm.model
 
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.utils.asExpr
 import org.ksmt.utils.cast
 import org.ksmt.utils.sampleValue
+import org.usvm.UAddressSort
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.UIndexedMethodReturnValue
+import org.usvm.UMockEvaluator
+import org.usvm.UMockSymbol
+import org.usvm.USizeExpr
+import org.usvm.USizeSort
+import org.usvm.USort
+import org.usvm.memory.UAddressCounter
+import org.usvm.memory.UInputArrayId
+import org.usvm.memory.UInputArrayLengthId
+import org.usvm.memory.UInputFieldId
+import org.usvm.memory.UMemoryRegion
+import org.usvm.memory.UReadOnlyMemoryRegion
+import org.usvm.memory.URegionId
+import org.usvm.memory.URegistersStackEvaluator
+import org.usvm.memory.USymbolicArrayIndex
+import org.usvm.memory.USymbolicHeap
+import org.usvm.uctx
 
 
 /**
@@ -84,9 +106,9 @@ class ULazyHeapModel<Field, ArrayType>(
     private val addressesMapping: AddressesMapping,
     private val regionIdToInitialValue: Map<URegionId<*, *, *>, KExpr<*>>,
 ) : USymbolicHeap<Field, ArrayType> {
-    private val resolvedInputFields = mutableMapOf<Field, UMemoryRegion<UHeapRef, out USort>>()
-    private val resolvedInputArrays = mutableMapOf<ArrayType, UMemoryRegion<USymbolicArrayIndex, out USort>>()
-    private val resolvedInputLengths = mutableMapOf<ArrayType, UMemoryRegion<UHeapRef, USizeSort>>()
+    private val resolvedInputFields = mutableMapOf<Field, UReadOnlyMemoryRegion<UHeapRef, out USort>>()
+    private val resolvedInputArrays = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<USymbolicArrayIndex, out USort>>()
+    private val resolvedInputLengths = mutableMapOf<ArrayType, UReadOnlyMemoryRegion<UHeapRef, USizeSort>>()
     override fun <Sort : USort> readField(ref: UHeapRef, field: Field, sort: Sort): UExpr<Sort> {
         // All the expressions in the model are interpreted, therefore, they must
         // have concrete addresses. Moreover, the model knows only about input values
diff --git a/usvm-core/src/main/kotlin/org/usvm/Model.kt b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt
similarity index 78%
rename from usvm-core/src/main/kotlin/org/usvm/Model.kt
rename to usvm-core/src/main/kotlin/org/usvm/model/Model.kt
index d2a492783b..d4661610da 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Model.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt
@@ -1,4 +1,12 @@
-package org.usvm
+package org.usvm.model
+
+import org.usvm.UComposer
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.UMockEvaluator
+import org.usvm.USort
+import org.usvm.UTypeModel
+import org.usvm.memory.UReadOnlySymbolicHeap
 
 interface UModel {
     fun <Sort: USort> eval(expr: UExpr<Sort>): UExpr<Sort>
diff --git a/usvm-core/src/main/kotlin/org/usvm/ModelRegions.kt b/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt
similarity index 84%
rename from usvm-core/src/main/kotlin/org/usvm/ModelRegions.kt
rename to usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt
index 27df1e9a1d..7df665a93d 100644
--- a/usvm-core/src/main/kotlin/org/usvm/ModelRegions.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt
@@ -1,12 +1,25 @@
-package org.usvm
+package org.usvm.model
 
 import kotlinx.collections.immutable.PersistentMap
 import kotlinx.collections.immutable.persistentMapOf
 import kotlinx.collections.immutable.toPersistentMap
-import org.ksmt.expr.*
+import org.ksmt.expr.KArray2Store
+import org.ksmt.expr.KArrayConst
+import org.ksmt.expr.KArrayStore
+import org.ksmt.expr.KConst
+import org.ksmt.expr.KExpr
 import org.ksmt.solver.KModel
 import org.ksmt.sort.KArray2Sort
 import org.ksmt.sort.KArraySort
+import org.usvm.UBoolExpr
+import org.usvm.UConcreteHeapRef
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.USort
+import org.usvm.isFalse
+import org.usvm.isTrue
+import org.usvm.memory.UMemoryRegion
+import org.usvm.memory.UReadOnlyMemoryRegion
 
 
 /**
@@ -15,7 +28,7 @@ import org.ksmt.sort.KArraySort
 class UMemory1DArray<KeySort : USort, Sort : USort> internal constructor(
     private val values: PersistentMap<UExpr<KeySort>, UExpr<Sort>>,
     private val constValue: UExpr<Sort>,
-) : UMemoryRegion<KExpr<KeySort>, Sort> {
+) : UReadOnlyMemoryRegion<KExpr<KeySort>, Sort> {
 
     /**
      * A constructor that is used in cases when we try to evaluate
@@ -27,20 +40,6 @@ class UMemory1DArray<KeySort : USort, Sort : USort> internal constructor(
 
     override fun read(key: KExpr<KeySort>): UExpr<Sort> = values.getOrDefault(key, constValue)
 
-    override fun write(
-        key: KExpr<KeySort>,
-        value: UExpr<Sort>,
-        guard: UBoolExpr
-    ): UMemoryRegion<KExpr<KeySort>, Sort> {
-        when {
-            guard.isFalse -> return this
-            else -> require(guard.isTrue)
-        }
-        val newMap = values.put(key, value)
-        return UMemory1DArray(newMap, constValue)
-    }
-
-
     companion object {
         /**
          * A constructor that is used in regular cases for a region
@@ -89,7 +88,7 @@ class UMemory1DArray<KeySort : USort, Sort : USort> internal constructor(
 class UMemory2DArray<Key1Sort : USort, Key2Sort : USort, Sort : USort> internal constructor(
     val values: PersistentMap<Pair<UExpr<Key1Sort>, UExpr<Key2Sort>>, UExpr<Sort>>,
     val constValue: UExpr<Sort>,
-) : UMemoryRegion<Pair<KExpr<Key1Sort>, KExpr<Key2Sort>>, Sort> {
+) : UReadOnlyMemoryRegion<Pair<KExpr<Key1Sort>, KExpr<Key2Sort>>, Sort> {
     /**
      * A constructor that is used in cases when we try to evaluate
      * an expression from a region that was never translated.
@@ -102,19 +101,6 @@ class UMemory2DArray<Key1Sort : USort, Key2Sort : USort, Sort : USort> internal
         return values.getOrDefault(key, constValue)
     }
 
-    override fun write(
-        key: Pair<KExpr<Key1Sort>, KExpr<Key2Sort>>,
-        value: UExpr<Sort>,
-        guard: UBoolExpr
-    ): UMemoryRegion<Pair<KExpr<Key1Sort>, KExpr<Key2Sort>>, Sort> {
-        when {
-            guard.isFalse -> return this
-            else -> require(guard.isTrue)
-        }
-        val newMap = values.put(key, value)
-        return UMemory2DArray(newMap, constValue)
-    }
-
     companion object {
         /**
          * A constructor that is used in regular cases for a region
diff --git a/usvm-core/src/main/kotlin/org/usvm/ExprTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt
similarity index 89%
rename from usvm-core/src/main/kotlin/org/usvm/ExprTranslator.kt
rename to usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt
index ec958b2de9..eb21a16b39 100644
--- a/usvm-core/src/main/kotlin/org/usvm/ExprTranslator.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/ExprTranslator.kt
@@ -1,9 +1,38 @@
-package org.usvm
+package org.usvm.solver
 
 import org.ksmt.expr.KExpr
 import org.ksmt.sort.KBoolSort
 import org.ksmt.utils.cast
 import org.ksmt.utils.mkConst
+import org.usvm.UAddressSort
+import org.usvm.UAllocatedArrayReading
+import org.usvm.UConcreteHeapRef
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.UExprTransformer
+import org.usvm.UHeapReading
+import org.usvm.UHeapRef
+import org.usvm.UIndexedMethodReturnValue
+import org.usvm.UInputArrayLengthReading
+import org.usvm.UInputArrayReading
+import org.usvm.UInputFieldReading
+import org.usvm.UIsExpr
+import org.usvm.UMockSymbol
+import org.usvm.UNullRef
+import org.usvm.URegisterReading
+import org.usvm.USizeExpr
+import org.usvm.USizeSort
+import org.usvm.USort
+import org.usvm.USymbol
+import org.usvm.memory.UAllocatedArrayId
+import org.usvm.memory.UInputArrayId
+import org.usvm.memory.UInputArrayLengthId
+import org.usvm.memory.UInputFieldId
+import org.usvm.memory.URegionId
+import org.usvm.memory.URegionIdVisitor
+import org.usvm.memory.USymbolicArrayIndex
+import org.usvm.memory.USymbolicMemoryRegion
+import org.usvm.uctx
 
 /**
  * Translates custom [UExpr] to a [KExpr]. Region readings are translated via [URegionTranslator]s.
diff --git a/usvm-core/src/main/kotlin/org/usvm/RegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt
similarity index 94%
rename from usvm-core/src/main/kotlin/org/usvm/RegionTranslator.kt
rename to usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt
index 92577efc99..ca4929bdb2 100644
--- a/usvm-core/src/main/kotlin/org/usvm/RegionTranslator.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt
@@ -1,8 +1,18 @@
-package org.usvm
+package org.usvm.solver
 
 import org.ksmt.expr.KExpr
 import org.ksmt.sort.KArray2Sort
 import org.ksmt.sort.KArraySort
+import org.usvm.UExpr
+import org.usvm.USort
+import org.usvm.memory.UArrayId
+import org.usvm.memory.UMemoryUpdatesVisitor
+import org.usvm.memory.UPinpointUpdateNode
+import org.usvm.memory.URangedUpdateNode
+import org.usvm.memory.URegionId
+import org.usvm.memory.USymbolicMemoryRegion
+import org.usvm.memory.UUpdateNode
+import org.usvm.uctx
 import java.util.IdentityHashMap
 
 /**
diff --git a/usvm-core/src/main/kotlin/org/usvm/Solver.kt b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
similarity index 89%
rename from usvm-core/src/main/kotlin/org/usvm/Solver.kt
rename to usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
index 782e76b40f..6e9663e800 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Solver.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/Solver.kt
@@ -1,7 +1,12 @@
-package org.usvm
+package org.usvm.solver
 
 import org.ksmt.solver.KSolver
 import org.ksmt.solver.KSolverStatus
+import org.usvm.UContext
+import org.usvm.UPathCondition
+import org.usvm.memory.UMemoryBase
+import org.usvm.model.UModelBase
+import org.usvm.model.UModelDecoder
 
 sealed interface USolverResult<T>
 
diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt
index 3ff31fe6de..6e69394ecd 100644
--- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt
@@ -12,7 +12,28 @@ import org.ksmt.expr.KExpr
 import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.sort.KBv32Sort
-import org.usvm.UAddressCounter.Companion.NULL_ADDRESS
+import org.usvm.memory.UAddressCounter.Companion.NULL_ADDRESS
+import org.usvm.memory.UAllocatedArrayId
+import org.usvm.memory.UAllocatedArrayRegion
+import org.usvm.memory.UFlatUpdates
+import org.usvm.memory.UInputArrayId
+import org.usvm.memory.UInputArrayLengthId
+import org.usvm.memory.UInputArrayLengthRegion
+import org.usvm.memory.UInputArrayRegion
+import org.usvm.memory.UInputFieldId
+import org.usvm.memory.UInputFieldRegion
+import org.usvm.memory.UInputToInputKeyConverter
+import org.usvm.memory.UMemoryUpdates
+import org.usvm.memory.UPinpointUpdateNode
+import org.usvm.memory.URangedUpdateNode
+import org.usvm.memory.UReadOnlySymbolicHeap
+import org.usvm.memory.URegionHeap
+import org.usvm.memory.URegistersStackEvaluator
+import org.usvm.memory.USymbolicArrayIndex
+import org.usvm.memory.UUpdateNode
+import org.usvm.memory.emptyAllocatedArrayRegion
+import org.usvm.memory.emptyInputArrayRegion
+import org.usvm.model.URegistersStackEagerModel
 import kotlin.reflect.KClass
 import kotlin.test.assertEquals
 import kotlin.test.assertIs
diff --git a/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt b/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt
index 1e6eece8f6..2c643560f9 100644
--- a/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/UContextInterningTest.kt
@@ -4,6 +4,10 @@ import io.mockk.every
 import io.mockk.mockk
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
+import org.usvm.memory.UAllocatedArrayRegion
+import org.usvm.memory.UInputArrayLengthRegion
+import org.usvm.memory.UInputArrayRegion
+import org.usvm.memory.UInputFieldRegion
 
 class UContextInterningTest {
     private lateinit var context: UContext
diff --git a/usvm-core/src/test/kotlin/org/usvm/HeapRefEqTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
similarity index 97%
rename from usvm-core/src/test/kotlin/org/usvm/HeapRefEqTest.kt
rename to usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
index ba256eac57..dc808bd51c 100644
--- a/usvm-core/src/test/kotlin/org/usvm/HeapRefEqTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
@@ -1,8 +1,11 @@
-package org.usvm
+package org.usvm.memory
 
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.ksmt.utils.getValue
+import org.usvm.Field
+import org.usvm.Type
+import org.usvm.UContext
 import kotlin.test.assertSame
 
 class HeapRefEqTest {
diff --git a/usvm-core/src/test/kotlin/org/usvm/HeapRefSplittingTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
similarity index 97%
rename from usvm-core/src/test/kotlin/org/usvm/HeapRefSplittingTest.kt
rename to usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
index 0870c79a7a..ceca24397b 100644
--- a/usvm-core/src/test/kotlin/org/usvm/HeapRefSplittingTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
@@ -1,10 +1,17 @@
-package org.usvm
+package org.usvm.memory
 
 import io.mockk.mockk
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.ksmt.expr.rewrite.simplify.KExprSimplifier
 import org.ksmt.utils.getValue
+import org.usvm.Field
+import org.usvm.Type
+import org.usvm.UAddressSort
+import org.usvm.UBv32Sort
+import org.usvm.UContext
+import org.usvm.UInputFieldReading
+import org.usvm.UIteExpr
 import kotlin.test.assertEquals
 import kotlin.test.assertIs
 import kotlin.test.assertNotNull
diff --git a/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/MapCompositionTest.kt
similarity index 98%
rename from usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt
rename to usvm-core/src/test/kotlin/org/usvm/memory/MapCompositionTest.kt
index 22caf7bf24..039dee2c03 100644
--- a/usvm-core/src/test/kotlin/org/usvm/MapCompositionTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/MapCompositionTest.kt
@@ -1,4 +1,4 @@
-package org.usvm
+package org.usvm.memory
 
 import io.mockk.every
 import io.mockk.mockk
@@ -6,6 +6,16 @@ import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.ksmt.expr.KExpr
 import org.ksmt.utils.mkConst
+import org.usvm.UAddressSort
+import org.usvm.UBv32Sort
+import org.usvm.UComposer
+import org.usvm.UConcreteHeapRef
+import org.usvm.UContext
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.USizeExpr
+import org.usvm.USizeSort
+import org.usvm.shouldNotBeCalled
 import org.usvm.util.SetRegion
 import org.usvm.util.emptyRegionTree
 import kotlin.test.assertFalse
diff --git a/usvm-core/src/test/kotlin/org/usvm/MemoryRegionTests.kt b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt
similarity index 95%
rename from usvm-core/src/test/kotlin/org/usvm/MemoryRegionTests.kt
rename to usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt
index 7f983fa5f0..28cbc77603 100644
--- a/usvm-core/src/test/kotlin/org/usvm/MemoryRegionTests.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTests.kt
@@ -1,8 +1,12 @@
-package org.usvm
+package org.usvm.memory
 
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.ksmt.utils.mkConst
+import org.usvm.UBv32Sort
+import org.usvm.UContext
+import org.usvm.UHeapRef
+import org.usvm.shouldNotBeCalled
 import org.usvm.util.SetRegion
 import org.usvm.util.emptyRegionTree
 import kotlin.test.assertNotNull
diff --git a/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/UpdatesIteratorTest.kt
similarity index 96%
rename from usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt
rename to usvm-core/src/test/kotlin/org/usvm/memory/UpdatesIteratorTest.kt
index a64bd5ae12..239799f481 100644
--- a/usvm-core/src/test/kotlin/org/usvm/UpdatesIteratorTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/UpdatesIteratorTest.kt
@@ -1,7 +1,10 @@
-package org.usvm
+package org.usvm.memory
 
 import org.junit.jupiter.api.Test
 import org.junit.jupiter.api.assertThrows
+import org.usvm.UBv32Sort
+import org.usvm.UContext
+import org.usvm.USort
 import org.usvm.util.SetRegion
 import org.usvm.util.emptyRegionTree
 import kotlin.test.assertTrue
diff --git a/usvm-core/src/test/kotlin/org/usvm/ModelCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt
similarity index 92%
rename from usvm-core/src/test/kotlin/org/usvm/ModelCompositionTest.kt
rename to usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt
index f043947387..bdb0175e50 100644
--- a/usvm-core/src/test/kotlin/org/usvm/ModelCompositionTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt
@@ -1,9 +1,21 @@
-package org.usvm
+package org.usvm.model
 
 import io.mockk.mockk
 import kotlinx.collections.immutable.persistentMapOf
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
+import org.usvm.Field
+import org.usvm.Type
+import org.usvm.UBv32Sort
+import org.usvm.UComposer
+import org.usvm.UConcreteHeapRef
+import org.usvm.UContext
+import org.usvm.memory.UAddressCounter
+import org.usvm.memory.UInputToAllocatedKeyConverter
+import org.usvm.memory.emptyAllocatedArrayRegion
+import org.usvm.memory.emptyInputArrayLengthRegion
+import org.usvm.memory.emptyInputArrayRegion
+import org.usvm.memory.emptyInputFieldRegion
 import kotlin.test.assertSame
 
 class ModelCompositionTest {
diff --git a/usvm-core/src/test/kotlin/org/usvm/ModelDecodingTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
similarity index 94%
rename from usvm-core/src/test/kotlin/org/usvm/ModelDecodingTest.kt
rename to usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
index ba6e6e9222..94a43fc397 100644
--- a/usvm-core/src/test/kotlin/org/usvm/ModelDecodingTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
@@ -1,10 +1,22 @@
-package org.usvm
+package org.usvm.model
 
 import io.mockk.mockk
 import org.junit.jupiter.api.Assertions.assertSame
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
 import org.ksmt.solver.z3.KZ3Solver
+import org.usvm.Field
+import org.usvm.Method
+import org.usvm.Type
+import org.usvm.UContext
+import org.usvm.UIndexedMocker
+import org.usvm.UPathConstraintsSet
+import org.usvm.memory.UMemoryBase
+import org.usvm.memory.URegionHeap
+import org.usvm.memory.URegistersStack
+import org.usvm.solver.USatResult
+import org.usvm.solver.USolverBase
+import org.usvm.solver.UUnsatResult
 import kotlin.test.assertIs
 
 class ModelDecodingTest {
diff --git a/usvm-core/src/test/kotlin/org/usvm/TranslationTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
similarity index 94%
rename from usvm-core/src/test/kotlin/org/usvm/TranslationTest.kt
rename to usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
index ce0a3900ab..989c068d70 100644
--- a/usvm-core/src/test/kotlin/org/usvm/TranslationTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
@@ -1,4 +1,4 @@
-package org.usvm
+package org.usvm.solver
 
 import io.mockk.mockk
 import org.junit.jupiter.api.BeforeEach
@@ -7,6 +7,18 @@ import org.junit.jupiter.api.Test
 import org.ksmt.solver.KSolverStatus
 import org.ksmt.solver.z3.KZ3Solver
 import org.ksmt.utils.mkConst
+import org.usvm.Field
+import org.usvm.Type
+import org.usvm.UAddressSort
+import org.usvm.UBv32Sort
+import org.usvm.UContext
+import org.usvm.memory.UInputToAllocatedKeyConverter
+import org.usvm.memory.UInputToInputKeyConverter
+import org.usvm.memory.URegionHeap
+import org.usvm.memory.emptyAllocatedArrayRegion
+import org.usvm.memory.emptyInputArrayLengthRegion
+import org.usvm.memory.emptyInputArrayRegion
+import org.usvm.memory.emptyInputFieldRegion
 import kotlin.test.assertSame
 
 class TranslationTest {
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Interpreter.kt b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Interpreter.kt
index 6eb3c83a09..9a7c194cb5 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Interpreter.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Interpreter.kt
@@ -1,12 +1,12 @@
 package org.usvm.interpreter
 
 import org.usvm.UContext
-import org.usvm.UMemoryBase
-import org.usvm.UModel
-import org.usvm.UModelBase
+import org.usvm.memory.UMemoryBase
+import org.usvm.model.UModel
+import org.usvm.model.UModelBase
 import org.usvm.UPathCondition
-import org.usvm.USolverBase
-import org.usvm.USatResult
+import org.usvm.solver.USolverBase
+import org.usvm.solver.USatResult
 import org.usvm.language.Call
 import org.usvm.language.Field
 import org.usvm.language.Goto
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/ResultModelConverter.kt b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/ResultModelConverter.kt
index 3af47872df..335ba26efd 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/ResultModelConverter.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/ResultModelConverter.kt
@@ -2,13 +2,13 @@ package org.usvm.interpreter
 
 import org.ksmt.expr.KBitVec32Value
 import org.ksmt.utils.asExpr
-import org.usvm.UAddressCounter.Companion.NULL_ADDRESS
+import org.usvm.memory.UAddressCounter.Companion.NULL_ADDRESS
 import org.usvm.UAddressSort
 import org.usvm.UBoolSort
 import org.usvm.UBv32Sort
 import org.usvm.UContext
 import org.usvm.UExpr
-import org.usvm.UModelBase
+import org.usvm.model.UModelBase
 import org.usvm.USort
 import org.usvm.isTrue
 import org.usvm.language.ArrayCreation
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Runner.kt b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Runner.kt
index 3fcd9cb9a2..b39f0c379e 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Runner.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/Runner.kt
@@ -3,11 +3,11 @@ package org.usvm.interpreter
 import kotlinx.collections.immutable.persistentListOf
 import org.ksmt.solver.yices.KYicesSolver
 import org.usvm.UContext
-import org.usvm.UModelBase
+import org.usvm.model.UModelBase
 import org.usvm.UPathConstraintsSet
-import org.usvm.USolverBase
-import org.usvm.USatResult
-import org.usvm.buildTranslatorAndLazyDecoder
+import org.usvm.solver.USolverBase
+import org.usvm.solver.USatResult
+import org.usvm.model.buildTranslatorAndLazyDecoder
 import org.usvm.language.Field
 import org.usvm.language.Method
 import org.usvm.language.Program
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/State.kt b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/State.kt
index 913f236af1..4ae7664414 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/State.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/State.kt
@@ -5,8 +5,8 @@ import kotlinx.collections.immutable.persistentListOf
 import org.usvm.UCallStack
 import org.usvm.UContext
 import org.usvm.UExpr
-import org.usvm.UMemoryBase
-import org.usvm.UModel
+import org.usvm.memory.UMemoryBase
+import org.usvm.model.UModel
 import org.usvm.UPathCondition
 import org.usvm.UPathConstraintsSet
 import org.usvm.USort
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/StepScope.kt b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/StepScope.kt
index d39517abc3..17d6eb3969 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/StepScope.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/interpreter/StepScope.kt
@@ -2,8 +2,8 @@ package org.usvm.interpreter
 
 import org.usvm.UBoolExpr
 import org.usvm.UContext
-import org.usvm.UMemoryBase
-import org.usvm.UModel
+import org.usvm.memory.UMemoryBase
+import org.usvm.model.UModel
 import org.usvm.UPathCondition
 import org.usvm.fork
 import org.usvm.language.Field