diff --git a/usvm-core/src/main/kotlin/org/usvm/Context.kt b/usvm-core/src/main/kotlin/org/usvm/Context.kt
index dfda6180df..61f40773aa 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Context.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Context.kt
@@ -42,6 +42,7 @@ import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElements
 import org.usvm.collection.set.ref.UInputRefSetWithAllocatedElementsReading
 import org.usvm.collection.set.ref.UInputRefSetWithInputElements
 import org.usvm.collection.set.ref.UInputRefSetWithInputElementsReading
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UAddressCounter
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.splitUHeapRef
@@ -66,6 +67,7 @@ open class UContext<USizeSort : USort>(
         components.mkComposer(this) as (UReadOnlyMemory<*>) -> UComposer<*, USizeSort>
     }
 
+    val defaultOwnership = MutabilityOwnership()
     val sizeExprs by lazy { components.mkSizeExprProvider(this) }
     val statesForkProvider by lazy { components.mkStatesForkProvider() }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt
index c689ba2725..1025dfc0b7 100644
--- a/usvm-core/src/main/kotlin/org/usvm/Mocks.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/Mocks.kt
@@ -2,11 +2,12 @@ package org.usvm
 
 import io.ksmt.utils.cast
 import kotlinx.collections.immutable.PersistentList
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
+import org.usvm.collections.immutable.persistentHashMapOf
 import kotlinx.collections.immutable.persistentListOf
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.merging.MergeGuard
-import org.usvm.merging.UMergeable
+import org.usvm.merging.UOwnedMergeable
 
 interface UMockEvaluator {
     fun <Sort : USort> eval(symbol: UMockSymbol<Sort>): UExpr<Sort>
@@ -26,14 +27,15 @@ interface UMocker<Method> : UMockEvaluator {
 
     fun getTrackedExpression(trackedLiteral: TrackedLiteral): UExpr<USort>
 
-    fun clone(): UMocker<Method>
+    fun clone(ownership: MutabilityOwnership): UMocker<Method>
 }
 
 class UIndexedMocker<Method>(
-    private var methodMockClauses: PersistentMap<Method, PersistentList<UMockSymbol<out USort>>> = persistentHashMapOf(),
-    private var trackedSymbols: PersistentMap<TrackedLiteral, UExpr<out USort>> = persistentHashMapOf(),
+    private var methodMockClauses: UPersistentHashMap<Method, PersistentList<UMockSymbol<out USort>>> = persistentHashMapOf(),
+    private var trackedSymbols: UPersistentHashMap<TrackedLiteral, UExpr<out USort>> = persistentHashMapOf(),
     private var untrackedSymbols: PersistentList<UExpr<out USort>> = persistentListOf(),
-) : UMocker<Method>, UMergeable<UIndexedMocker<Method>, MergeGuard> {
+    internal var ownership: MutabilityOwnership,
+) : UMocker<Method>, UOwnedMergeable<UIndexedMocker<Method>, MergeGuard> {
     override fun <Sort : USort> call(
         method: Method,
         args: Sequence<UExpr<out USort>>,
@@ -42,7 +44,7 @@ class UIndexedMocker<Method>(
         val currentClauses = methodMockClauses.getOrDefault(method, persistentListOf())
         val index = currentClauses.size
         val const = sort.uctx.mkIndexedMethodReturnValue(method, index, sort)
-        methodMockClauses = methodMockClauses.put(method, currentClauses.add(const))
+        methodMockClauses = methodMockClauses.put(method, currentClauses.add(const), ownership)
 
         return const
     }
@@ -50,7 +52,7 @@ class UIndexedMocker<Method>(
     override fun <Sort : USort> eval(symbol: UMockSymbol<Sort>): UExpr<Sort> = symbol
 
     override val trackedLiterals: Collection<TrackedLiteral>
-        get() = trackedSymbols.keys
+        get() = trackedSymbols.keys()
 
     /**
      * Creates a mock symbol. If [trackedLiteral] is not null, created expression
@@ -60,7 +62,7 @@ class UIndexedMocker<Method>(
         val const = sort.uctx.mkTrackedSymbol(sort)
 
         if (trackedLiteral != null) {
-            trackedSymbols = trackedSymbols.put(trackedLiteral, const)
+            trackedSymbols = trackedSymbols.put(trackedLiteral, const, ownership)
         } else {
             untrackedSymbols = untrackedSymbols.add(const)
         }
@@ -71,10 +73,11 @@ class UIndexedMocker<Method>(
     override fun getTrackedExpression(trackedLiteral: TrackedLiteral): UExpr<USort> {
         if (trackedLiteral !in trackedSymbols) error("Access by unregistered track literal $trackedLiteral")
 
-        return trackedSymbols.getValue(trackedLiteral).cast()
+        return trackedSymbols[trackedLiteral]!!.cast()
     }
 
-    override fun clone(): UIndexedMocker<Method> = UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols)
+    override fun clone(ownership: MutabilityOwnership): UIndexedMocker<Method> =
+        UIndexedMocker(methodMockClauses, trackedSymbols, untrackedSymbols, ownership)
 
     /**
      * Check if this [UIndexedMocker] can be merged with [other] indexed mocker.
@@ -83,14 +86,14 @@ class UIndexedMocker<Method>(
      *
      * @return the merged indexed mocker.
      */
-    override fun mergeWith(other: UIndexedMocker<Method>, by: MergeGuard): UIndexedMocker<Method>? {
+    override fun mergeWith(other: UIndexedMocker<Method>, by: MergeGuard, ownership: MutabilityOwnership): UIndexedMocker<Method>? {
         if (methodMockClauses !== other.methodMockClauses
             || trackedSymbols !== other.trackedSymbols
             || untrackedSymbols !== other.untrackedSymbols
         ) {
             return null
         }
-
+        this.ownership = ownership
         return this
     }
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/State.kt b/usvm-core/src/main/kotlin/org/usvm/State.kt
index 5f920c6c10..4505a3add0 100644
--- a/usvm-core/src/main/kotlin/org/usvm/State.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/State.kt
@@ -4,7 +4,6 @@ import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.constraints.UPathConstraints
 import org.usvm.memory.UMemory
 import org.usvm.merging.UMergeable
-import org.usvm.merging.UOwnedMergeable
 import org.usvm.model.UModelBase
 import org.usvm.targets.UTarget
 import org.usvm.targets.UTargetsSet
@@ -14,7 +13,7 @@ typealias StateId = UInt
 abstract class UState<Type, Method, Statement, Context, Target, State>(
     // TODO: add interpreter-specific information
     val ctx: Context,
-    private var ownership : MutabilityOwnership,
+    initOwnership : MutabilityOwnership,
     open val callStack: UCallStack<Method, Statement>,
     open val pathConstraints: UPathConstraints<Type>,
     open val memory: UMemory<Type, Method>,
@@ -26,7 +25,7 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
     open var pathNode: PathNode<Statement>,
     open var forkPoints: PathNode<PathNode<Statement>>,
     open val targets: UTargetsSet<Target, Statement>,
-) : UOwnedMergeable<State, Unit>
+) : UMergeable<State, Unit>
     where Context : UContext<*>,
           Target : UTarget<Statement, Target>,
           State : UState<Type, Method, Statement, Context, Target, State> {
@@ -35,19 +34,23 @@ abstract class UState<Type, Method, Statement, Context, Target, State>(
      * TODO: Can be replaced with overridden hashCode
      */
     val id: StateId = ctx.getNextStateId()
+
+    open var ownership = initOwnership
+        protected set
     
-    fun changeOwnership(newOwnership: MutabilityOwnership) {
+    protected fun changeOwnership(newOwnership: MutabilityOwnership) {
         ownership = newOwnership
         pathConstraints.changeOwnership(ownership)
+        memory.changeOwnership(ownership)
     }
 
     /**
      * Creates new state structurally identical to this.
      * If [newConstraints] is null, clones [pathConstraints]. Otherwise, uses [newConstraints] in cloned state.
      */
-    abstract fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints<Type>? = null): State
+    abstract fun clone(newConstraints: UPathConstraints<Type>? = null): State
 
-    override fun mergeWith(other: State, by: Unit, ownership: MutabilityOwnership): State? = null
+    override fun mergeWith(other: State, by: Unit): State? = null
 
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
diff --git a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt
index 412d4cbe43..4656307739 100644
--- a/usvm-core/src/main/kotlin/org/usvm/StateForker.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/StateForker.kt
@@ -52,8 +52,7 @@ object WithSolverStateForker : StateForker {
 
             trueModels.isNotEmpty() && falseModels.isNotEmpty() -> {
                 val posState = state
-                posState.changeOwnership(MutabilityOwnership())
-                val negState = state.clone(MutabilityOwnership())
+                val negState = state.clone()
 
                 posState.models = trueModels
                 negState.models = falseModels
@@ -101,11 +100,9 @@ object WithSolverStateForker : StateForker {
             val (trueModels, _, _) = splitModelsByCondition(curState.models, condition)
 
             val nextRoot = if (trueModels.isNotEmpty()) {
-                val newOwnership = MutabilityOwnership()
-                val root = curState.clone(newOwnership)
+                val root = curState.clone()
                 curState.models = trueModels
                 curState.pathConstraints += condition
-                curState.changeOwnership(MutabilityOwnership())
 
                 root
             } else {
@@ -167,14 +164,12 @@ object WithSolverStateForker : StateForker {
                 // heavy plusAssign operator in path constraints.
                 // Therefore, it is better to reuse already constructed [constraintToCheck].
                 if (stateToCheck) {
-                    state.changeOwnership(MutabilityOwnership())
-                    val forkedState = state.clone(newOwnership, constraintsToCheck)
+                    val forkedState = state.clone(constraintsToCheck)
                     state.pathConstraints += newConstraintToOriginalState
                     forkedState.models = listOf(satResult.model)
                     forkedState
                 } else {
-                    val forkedState = state.clone(newOwnership)
-                    state.changeOwnership(MutabilityOwnership())
+                    val forkedState = state.clone()
                     state.pathConstraints += newConstraintToOriginalState
                     state.models = listOf(satResult.model)
                     // TODO: implement path condition setter (don't forget to reset UMemoryBase:types!)
@@ -204,13 +199,13 @@ object NoSolverStateForker : StateForker {
         clonedPathConstraints += condition
 
         val (posState, negState) = if (clonedPathConstraints.isFalse) {
+            // changing ownership is unnecessary
             state.pathConstraints += notCondition
             state.models = falseModels
-            state.changeOwnership(MutabilityOwnership())
 
             null to state.takeIf { !it.pathConstraints.isFalse }
         } else {
-            val falseState = state.clone(newOwnership)
+            val falseState = state.clone()
 
             // TODO how to reuse "clonedPathConstraints" here?
             state.pathConstraints += condition
@@ -242,7 +237,7 @@ object NoSolverStateForker : StateForker {
                 continue
             }
 
-            val nextRoot = curState.clone(newOwnership)
+            val nextRoot = curState.clone()
 
             curState.models = trueModels
             // TODO how to reuse "clonedConstraints"?
diff --git a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
index a80a1e0805..780635c3d3 100644
--- a/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/StepScope.kt
@@ -43,6 +43,8 @@ class StepScope<T : UState<Type, *, Statement, Context, *, T>, Type, Statement,
 
     val isDead: Boolean get() = stepScopeState === DEAD
 
+    val ownership = originalState.ownership
+
     /**
      * Executes [block] on a state.
      *
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 89f259894f..4740d86dd5 100644
--- a/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/api/MemoryApi.kt
@@ -6,7 +6,6 @@ import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
-import org.usvm.memory.UMemory
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.UWritableMemory
 import org.usvm.collection.array.UArrayIndexLValue
@@ -89,7 +88,7 @@ fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayType>.mems
     type: ArrayType,
     sort: Sort,
     sizeSort: USizeSort,
-    contents: Sequence<UExpr<Sort>>
+    contents: Sequence<UExpr<Sort>>,
 ) {
     memsetInternal(ref, type, sort, sizeSort, contents)
 }
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 438955a882..65d77a8574 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
@@ -158,6 +158,7 @@ object ListCollectionApi {
         srcFrom: UExpr<USizeSort>,
         dstFrom: UExpr<USizeSort>,
         length: UExpr<USizeSort>,
+
     ) {
         memory.memcpy(
             srcRef = srcRef,
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 4c7dc1b96b..e3e86f2859 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
@@ -1,12 +1,13 @@
 package org.usvm.collection.array
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -50,6 +51,7 @@ interface UArrayRegion<ArrayType, Sort : USort, USizeSort : USort> : UMemoryRegi
         fromDstIdx: UExpr<USizeSort>,
         toDstIdx: UExpr<USizeSort>,
         operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership,
     ): UArrayRegion<ArrayType, Sort, USizeSort>
 
     fun initializeAllocatedArray(
@@ -57,30 +59,33 @@ interface UArrayRegion<ArrayType, Sort : USort, USizeSort : USort> : UMemoryRegi
         arrayType: ArrayType,
         sort: Sort,
         content: Map<UExpr<USizeSort>, UExpr<Sort>>,
-        operationGuard: UBoolExpr
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership,
     ): UArrayRegion<ArrayType, Sort, USizeSort>
 }
 
 internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
-    private var allocatedArrays: PersistentMap<UConcreteHeapAddress, UAllocatedArray<ArrayType, Sort, USizeSort>> = persistentHashMapOf(),
+    private var allocatedArrays: UPersistentHashMap<UConcreteHeapAddress, UAllocatedArray<ArrayType, Sort, USizeSort>> = persistentHashMapOf(),
     private var inputArray: UInputArray<ArrayType, Sort, USizeSort>? = null
 ) : UArrayRegion<ArrayType, Sort, USizeSort> {
 
     private fun getAllocatedArray(
         arrayType: ArrayType,
         sort: Sort,
-        address: UConcreteHeapAddress
+        address: UConcreteHeapAddress,
+        ownership: MutabilityOwnership
     ): UAllocatedArray<ArrayType, Sort, USizeSort> {
-        var collection = allocatedArrays[address]
-        if (collection == null) {
-            collection = UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address).emptyRegion()
-            allocatedArrays = allocatedArrays.put(address, collection)
-        }
+        val (updatedArrays, collection) = 
+            allocatedArrays.getOrPut(address, UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address).emptyRegion(), ownership)
+        allocatedArrays = updatedArrays
         return collection
     }
 
-    private fun updateAllocatedArray(ref: UConcreteHeapAddress, updated: UAllocatedArray<ArrayType, Sort, USizeSort>) =
-        UArrayMemoryRegion(allocatedArrays.put(ref, updated), inputArray)
+    private fun updateAllocatedArray(
+        ref: UConcreteHeapAddress,
+        updated: UAllocatedArray<ArrayType, Sort, USizeSort>,
+        ownership: MutabilityOwnership
+    ) = UArrayMemoryRegion(allocatedArrays.put(ref, updated, ownership), inputArray)
 
     private fun getInputArray(arrayType: ArrayType, sort: Sort): UInputArray<ArrayType, Sort, USizeSort> {
         if (inputArray == null)
@@ -91,27 +96,28 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
     private fun updateInput(updated: UInputArray<ArrayType, Sort, USizeSort>) =
         UArrayMemoryRegion(allocatedArrays, updated)
 
-    override fun read(key: UArrayIndexLValue<ArrayType, Sort, USizeSort>): 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 read(key: UArrayIndexLValue<ArrayType, Sort, USizeSort>, ownership: MutabilityOwnership): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
+        concreteMapper = { concreteRef -> getAllocatedArray(key.arrayType, key.sort, concreteRef.address, ownership).read(key.index, ownership) },
+        symbolicMapper = { symbolicRef -> getInputArray(key.arrayType, key.sort).read(symbolicRef to key.index, ownership) }
     )
 
     override fun write(
         key: UArrayIndexLValue<ArrayType, Sort, USizeSort>,
         value: UExpr<Sort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): UMemoryRegion<UArrayIndexLValue<ArrayType, Sort, USizeSort>, 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)
+            val oldRegion = region.getAllocatedArray(key.arrayType, key.sort, concreteRef.address, ownership)
+            val newRegion = oldRegion.write(key.index, value, innerGuard, ownership)
+            region.updateAllocatedArray(concreteRef.address, newRegion, ownership)
         },
         blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
             val oldRegion = region.getInputArray(key.arrayType, key.sort)
-            val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard)
+            val newRegion = oldRegion.write(symbolicRef to key.index, value, innerGuard, ownership)
             region.updateInput(newRegion)
         }
     )
@@ -125,23 +131,24 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
         fromDstIdx: UExpr<USizeSort>,
         toDstIdx: UExpr<USizeSort>,
         operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership,
     ) = foldHeapRef2(
         ref0 = srcRef,
         ref1 = dstRef,
         initial = this,
         initialGuard = operationGuard,
         blockOnConcrete0Concrete1 = { region, srcConcrete, dstConcrete, guard ->
-            val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address)
-            val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address)
+            val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address, ownership)
+            val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address, ownership)
             val adapter = USymbolicArrayAllocatedToAllocatedCopyAdapter(
                 fromSrcIdx, fromDstIdx, toDstIdx, USizeExprKeyInfo()
             )
             val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
-            region.updateAllocatedArray(dstConcrete.address, newDstCollection)
+            region.updateAllocatedArray(dstConcrete.address, newDstCollection, ownership)
         },
 
         blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
-            val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address)
+            val srcCollection = region.getAllocatedArray(type, elementSort, srcConcrete.address, ownership)
             val dstCollection = region.getInputArray(type, elementSort)
             val adapter = USymbolicArrayAllocatedToInputCopyAdapter(
                 fromSrcIdx,
@@ -154,7 +161,7 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
         },
         blockOnSymbolic0Concrete1 = { region, srcSymbolic, dstConcrete, guard ->
             val srcCollection = region.getInputArray(type, elementSort)
-            val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address)
+            val dstCollection = region.getAllocatedArray(type, elementSort, dstConcrete.address, ownership)
             val adapter = USymbolicArrayInputToAllocatedCopyAdapter(
                 srcSymbolic to fromSrcIdx,
                 fromDstIdx,
@@ -162,7 +169,7 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
                 USizeExprKeyInfo()
             )
             val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
-            region.updateAllocatedArray(dstConcrete.address, newDstCollection)
+            region.updateAllocatedArray(dstConcrete.address, newDstCollection, ownership)
         },
         blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
             val srcCollection = region.getInputArray(type, elementSort)
@@ -183,10 +190,11 @@ internal class UArrayMemoryRegion<ArrayType, Sort : USort, USizeSort : USort>(
         arrayType: ArrayType,
         sort: Sort,
         content: Map<UExpr<USizeSort>, UExpr<Sort>>,
-        operationGuard: UBoolExpr
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): UArrayMemoryRegion<ArrayType, Sort, USizeSort> {
         val arrayId = UAllocatedArrayId<_, _, USizeSort>(arrayType, sort, address)
         val newCollection = arrayId.initializedArray(content, operationGuard)
-        return UArrayMemoryRegion(allocatedArrays.put(address, newCollection), inputArray)
+        return UArrayMemoryRegion(allocatedArrays.put(address, newCollection, ownership), inputArray)
     }
 }
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 8136f72a3f..c9bb414a03 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
@@ -6,7 +6,6 @@ import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.collection.array.length.UArrayLengthLValue
-import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UWritableMemory
 import org.usvm.mkSizeExpr
 import org.usvm.uctx
@@ -29,7 +28,7 @@ internal fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<*>.mem
         "memcpy is not applicable to $region"
     }
 
-    val newRegion = region.memcpy(srcRef, dstRef, type, elementSort, fromSrcIdx, fromDstIdx, toDstIdx, guard)
+    val newRegion = region.memcpy(srcRef, dstRef, type, elementSort, fromSrcIdx, fromDstIdx, toDstIdx, guard, ownership)
     setRegion(regionId, newRegion)
 }
 
@@ -52,7 +51,14 @@ internal fun <ArrayType, Sort : USort, USizeSort : USort> UWritableMemory<ArrayT
         "allocateArrayInitialized is not applicable to $region"
     }
 
-    val newRegion = region.initializeAllocatedArray(address.address, type, elementSort, arrayValues, operationGuard = trueExpr)
+    val newRegion = region.initializeAllocatedArray(
+        address.address,
+        type,
+        elementSort,
+        arrayValues,
+        operationGuard = trueExpr,
+        ownership = ownership
+    )
 
     setRegion(regionId, newRegion)
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt
index 46f49fb279..71a5e28624 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/UArrayModelRegion.kt
@@ -2,6 +2,7 @@ package org.usvm.collection.array
 
 import org.usvm.UExpr
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
@@ -12,9 +13,9 @@ abstract class UArrayModelRegion<ArrayType, Sort : USort, USizeSort : USort>(
 ) : UReadOnlyMemoryRegion<UArrayIndexLValue<ArrayType, Sort, USizeSort>, Sort> {
     abstract val inputArray: UReadOnlyMemoryRegion<USymbolicArrayIndex<USizeSort>, Sort>
 
-    override fun read(key: UArrayIndexLValue<ArrayType, Sort, USizeSort>): UExpr<Sort> {
+    override fun read(key: UArrayIndexLValue<ArrayType, Sort, USizeSort>, ownership: MutabilityOwnership): UExpr<Sort> {
         val ref = modelEnsureConcreteInputRef(key.ref)
-        return inputArray.read(ref to key.index)
+        return inputArray.read(ref to key.index, ownership)
     }
 }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt
index d621bca821..bc52685804 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/USymbolicArrayId.kt
@@ -42,7 +42,7 @@ class UAllocatedArrayId<ArrayType, Sort : USort, USizeSort : USort> internal con
     override fun instantiate(
         collection: USymbolicCollection<UAllocatedArrayId<ArrayType, Sort, USizeSort>, UExpr<USizeSort>, Sort>,
         key: UExpr<USizeSort>,
-        composer: UComposer<*, *>?
+        composer: UComposer<*, *>?,
     ): UExpr<Sort> {
         if (collection.updates.isEmpty()) {
             return composer.compose(defaultValue)
@@ -123,7 +123,7 @@ class UInputArrayId<ArrayType, Sort : USort, USizeSort : USort> internal constru
     override fun instantiate(
         collection: USymbolicCollection<UInputArrayId<ArrayType, Sort, USizeSort>, USymbolicArrayIndex<USizeSort>, Sort>,
         key: USymbolicArrayIndex<USizeSort>,
-        composer: UComposer<*, *>?
+        composer: UComposer<*, *>?,
     ): UExpr<Sort> {
         if (composer == null) {
             return sort.uctx.withSizeSort<USizeSort>().mkInputArrayReading(collection, key.first, key.second)
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 693b237371..1234b8a464 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
@@ -1,12 +1,13 @@
 package org.usvm.collection.array.length
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -42,11 +43,11 @@ interface UArrayLengthsRegion<ArrayType, USizeSort : USort> : UMemoryRegion<UArr
 internal class UArrayLengthsMemoryRegion<ArrayType, USizeSort : USort>(
     private val sort: USizeSort,
     private val arrayType: ArrayType,
-    private val allocatedLengths: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentHashMapOf(),
+    private val allocatedLengths: UPersistentHashMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentHashMapOf(),
     private var inputLengths: UInputArrayLengths<ArrayType, USizeSort>? = null
 ) : UArrayLengthsRegion<ArrayType, USizeSort> {
 
-    private fun updateAllocated(updated: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>>) =
+    private fun updateAllocated(updated: UPersistentHashMap<UConcreteHeapAddress, UExpr<USizeSort>>) =
         UArrayLengthsMemoryRegion(sort, arrayType, updated, inputLengths)
 
     private fun getInputLength(ref: UArrayLengthLValue<ArrayType, USizeSort>): UInputArrayLengths<ArrayType, USizeSort> {
@@ -58,28 +59,30 @@ internal class UArrayLengthsMemoryRegion<ArrayType, USizeSort : USort>(
     private fun updatedInput(updated: UInputArrayLengths<ArrayType, USizeSort>) =
         UArrayLengthsMemoryRegion(sort, arrayType, allocatedLengths, updated)
 
-    override fun read(key: UArrayLengthLValue<ArrayType, USizeSort>): UExpr<USizeSort> = key.ref.mapWithStaticAsSymbolic(
-        concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
-        symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) }
+    override fun read(key: UArrayLengthLValue<ArrayType, USizeSort>, ownership: MutabilityOwnership): UExpr<USizeSort> =
+        key.ref.mapWithStaticAsSymbolic(
+            concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
+            symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef, ownership) }
     )
 
     override fun write(
         key: UArrayLengthLValue<ArrayType, USizeSort>,
         value: UExpr<USizeSort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRefWithStaticAsSymbolic(
         key.ref,
         initial = this,
         initialGuard = guard,
         blockOnConcrete = { region, (concreteRef, innerGuard) ->
-            val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard) {
+            val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard, ownership) {
                 sort.sampleUValue()
             }
             region.updateAllocated(newRegion)
         },
         blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
             val oldRegion = region.getInputLength(key)
-            val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
+            val newRegion = oldRegion.write(symbolicRef, value, innerGuard, ownership)
             region.updatedInput(newRegion)
         }
     )
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt
index 625520868b..2d330e66a7 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/array/length/UArrayLengthModelRegion.kt
@@ -3,6 +3,7 @@ package org.usvm.collection.array.length
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
@@ -13,9 +14,9 @@ abstract class UArrayLengthModelRegion<ArrayType, USizeSort : USort>(
 ) : UReadOnlyMemoryRegion<UArrayLengthLValue<ArrayType, USizeSort>, USizeSort> {
     abstract val inputArrayLength: UReadOnlyMemoryRegion<UHeapRef, USizeSort>
 
-    override fun read(key: UArrayLengthLValue<ArrayType, USizeSort>): UExpr<USizeSort> {
+    override fun read(key: UArrayLengthLValue<ArrayType, USizeSort>, ownership: MutabilityOwnership): UExpr<USizeSort> {
         val ref = modelEnsureConcreteInputRef(key.ref)
-        return inputArrayLength.read(ref)
+        return inputArrayLength.read(ref, ownership)
     }
 }
 
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 400496f117..381b9e40f3 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
@@ -1,12 +1,13 @@
 package org.usvm.collection.field
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -39,11 +40,11 @@ interface UFieldsRegion<Field, Sort : USort> : UMemoryRegion<UFieldLValue<Field,
 internal class UFieldsMemoryRegion<Field, Sort : USort>(
     private val sort: Sort,
     private val field: Field,
-    private val allocatedFields: PersistentMap<UConcreteHeapAddress, UExpr<Sort>> = persistentHashMapOf(),
+    private val allocatedFields: UPersistentHashMap<UConcreteHeapAddress, UExpr<Sort>> = persistentHashMapOf(),
     private var inputFields: UInputFields<Field, Sort>? = null
 ) : UFieldsRegion<Field, Sort> {
 
-    private fun updateAllocated(updated: PersistentMap<UConcreteHeapAddress, UExpr<Sort>>) =
+    private fun updateAllocated(updated: UPersistentHashMap<UConcreteHeapAddress, UExpr<Sort>>) =
         UFieldsMemoryRegion(sort, field, updated, inputFields)
 
     private fun getInputFields(ref: UFieldLValue<Field, Sort>): UInputFields<Field, Sort> {
@@ -55,28 +56,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.mapWithStaticAsSymbolic(
+    override fun read(key: UFieldLValue<Field, Sort>, ownership: MutabilityOwnership): UExpr<Sort> = key.ref.mapWithStaticAsSymbolic(
         concreteMapper = { concreteRef -> allocatedFields[concreteRef.address] ?: sort.sampleUValue() },
-        symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef) }
+        symbolicMapper = { symbolicRef -> getInputFields(key).read(symbolicRef, ownership) }
     )
 
     override fun write(
         key: UFieldLValue<Field, Sort>,
         value: UExpr<Sort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): 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) {
+            val newRegion = region.allocatedFields.guardedWrite(concreteRef.address, value, innerGuard, ownership) {
                 sort.sampleUValue()
             }
             region.updateAllocated(newRegion)
         },
         blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
             val oldRegion = region.getInputFields(key)
-            val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
+            val newRegion = oldRegion.write(symbolicRef, value, innerGuard, ownership)
             region.updateInput(newRegion)
         }
     )
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt
index a4b6aab5a2..052b32e47c 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/field/UFieldsModelRegion.kt
@@ -3,6 +3,7 @@ package org.usvm.collection.field
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
@@ -13,9 +14,9 @@ abstract class UFieldsModelRegion<Field, Sort : USort>(
 ) : UReadOnlyMemoryRegion<UFieldLValue<Field, Sort>, Sort> {
     abstract val inputFields: UReadOnlyMemoryRegion<UHeapRef, Sort>
 
-    override fun read(key: UFieldLValue<Field, Sort>): UExpr<Sort> {
+    override fun read(key: UFieldLValue<Field, Sort>, ownership: MutabilityOwnership): UExpr<Sort> {
         val ref = modelEnsureConcreteInputRef(key.ref)
-        return inputFields.read(ref)
+        return inputFields.read(ref, ownership)
     }
 }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt
index 81a280919b..3bd90a17e9 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/length/UMapLengthModelRegion.kt
@@ -3,6 +3,7 @@ package org.usvm.collection.map.length
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
@@ -13,9 +14,9 @@ abstract class UMapLengthModelRegion<MapType, USizeSort : USort>(
 ) : UReadOnlyMemoryRegion<UMapLengthLValue<MapType, USizeSort>, USizeSort> {
     abstract val inputMapLength: UReadOnlyMemoryRegion<UHeapRef, USizeSort>
 
-    override fun read(key: UMapLengthLValue<MapType, USizeSort>): UExpr<USizeSort> {
+    override fun read(key: UMapLengthLValue<MapType, USizeSort>, ownership: MutabilityOwnership): UExpr<USizeSort> {
         val ref = modelEnsureConcreteInputRef(key.ref)
-        return inputMapLength.read(ref)
+        return inputMapLength.read(ref, ownership)
     }
 }
 
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 0ceacf1974..4ef9ae06f9 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
@@ -1,12 +1,13 @@
 package org.usvm.collection.map.length
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -43,11 +44,11 @@ interface UMapLengthRegion<MapType, USizeSort : USort> : UMemoryRegion<UMapLengt
 internal class UMapLengthMemoryRegion<MapType, USizeSort : USort>(
     private val sort: USizeSort,
     private val mapType: MapType,
-    private val allocatedLengths: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentHashMapOf(),
+    private val allocatedLengths: UPersistentHashMap<UConcreteHeapAddress, UExpr<USizeSort>> = persistentHashMapOf(),
     private var inputLengths: UInputMapLength<MapType, USizeSort>? = null
 ) : UMapLengthRegion<MapType, USizeSort> {
 
-    private fun updateAllocated(updated: PersistentMap<UConcreteHeapAddress, UExpr<USizeSort>>) =
+    private fun updateAllocated(updated: UPersistentHashMap<UConcreteHeapAddress, UExpr<USizeSort>>) =
         UMapLengthMemoryRegion(sort, mapType, updated, inputLengths)
 
     private fun getInputLength(ref: UMapLengthLValue<MapType, USizeSort>): UInputMapLength<MapType, USizeSort> {
@@ -59,28 +60,30 @@ internal class UMapLengthMemoryRegion<MapType, USizeSort : USort>(
     private fun updateInput(updated: UInputMapLength<MapType, USizeSort>) =
         UMapLengthMemoryRegion(sort, mapType, allocatedLengths, updated)
 
-    override fun read(key: UMapLengthLValue<MapType, USizeSort>): UExpr<USizeSort> = key.ref.mapWithStaticAsSymbolic(
-        concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
-        symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef) }
+    override fun read(key: UMapLengthLValue<MapType, USizeSort>, ownership: MutabilityOwnership): UExpr<USizeSort> =
+        key.ref.mapWithStaticAsSymbolic(
+            concreteMapper = { concreteRef -> allocatedLengths[concreteRef.address] ?: sort.sampleUValue() },
+            symbolicMapper = { symbolicRef -> getInputLength(key).read(symbolicRef, ownership) }
     )
 
     override fun write(
         key: UMapLengthLValue<MapType, USizeSort>,
         value: UExpr<USizeSort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.ref,
         initial = this,
         initialGuard = guard,
         blockOnConcrete = { region, (concreteRef, innerGuard) ->
-            val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard) {
+            val newRegion = region.allocatedLengths.guardedWrite(concreteRef.address, value, innerGuard, ownership) {
                 sort.sampleUValue()
             }
             region.updateAllocated(newRegion)
         },
         blockOnSymbolic = { region, (symbolicRef, innerGuard) ->
             val oldRegion = region.getInputLength(key)
-            val newRegion = oldRegion.write(symbolicRef, value, innerGuard)
+            val newRegion = oldRegion.write(symbolicRef, value, innerGuard, ownership)
             region.updateInput(newRegion)
         }
     )
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapModelRegion.kt
index 14021f29c1..ff10f56048 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapModelRegion.kt
@@ -3,6 +3,7 @@ package org.usvm.collection.map.primitive
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.collection.map.USymbolicMapKey
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
@@ -14,9 +15,9 @@ abstract class UMapModelRegion<MapType, KeySort : USort, ValueSort : USort, Reg
 ) : UReadOnlyMemoryRegion<UMapEntryLValue<MapType, KeySort, ValueSort, Reg>, ValueSort> {
     abstract val inputMap: UReadOnlyMemoryRegion<USymbolicMapKey<KeySort>, ValueSort>
 
-    override fun read(key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>): UExpr<ValueSort> {
+    override fun read(key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>, ownership: MutabilityOwnership): UExpr<ValueSort> {
         val mapRef = modelEnsureConcreteInputRef(key.mapRef)
-        return inputMap.read(mapRef to key.mapKey)
+        return inputMap.read(mapRef to key.mapKey, ownership)
     }
 }
 
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 44a1707ddd..bcf85ca99c 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
@@ -1,13 +1,14 @@
 package org.usvm.collection.map.primitive
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.collection.map.USymbolicMapKey
 import org.usvm.collection.set.primitive.USetRegion
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -58,7 +59,8 @@ interface UMapRegion<MapType, KeySort : USort, ValueSort : USort, Reg : Region<R
         dstRef: UHeapRef,
         mapType: MapType,
         srcKeySet: USetRegion<MapType, KeySort, *>,
-        initialGuard: UBoolExpr
+        initialGuard: UBoolExpr,
+        ownership: MutabilityOwnership,
     ): UMapRegion<MapType, KeySort, ValueSort, Reg>
 }
 
@@ -67,7 +69,7 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
     private val valueSort: ValueSort,
     private val mapType: MapType,
     private val keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
-    private var allocatedMaps: PersistentMap<UAllocatedMapId<MapType, KeySort, ValueSort, Reg>, UAllocatedMap<MapType, KeySort, ValueSort, Reg>> = persistentHashMapOf(),
+    private var allocatedMaps: UPersistentHashMap<UAllocatedMapId<MapType, KeySort, ValueSort, Reg>, UAllocatedMap<MapType, KeySort, ValueSort, Reg>> = persistentHashMapOf(),
     private var inputMap: UInputMap<MapType, KeySort, ValueSort, Reg>? = null,
 ) : UMapRegion<MapType, KeySort, ValueSort, Reg> {
     init {
@@ -77,25 +79,24 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
     }
 
     private fun getAllocatedMap(
-        id: UAllocatedMapId<MapType, KeySort, ValueSort, Reg>
+        id: UAllocatedMapId<MapType, KeySort, ValueSort, Reg>,
+        ownership: MutabilityOwnership
     ): UAllocatedMap<MapType, KeySort, ValueSort, Reg> {
-        var collection = allocatedMaps[id]
-        if (collection == null) {
-            collection = id.emptyRegion()
-            allocatedMaps = allocatedMaps.put(id, collection)
-        }
+        val (updatesMaps, collection) =  allocatedMaps.getOrPut(id, id.emptyRegion(), ownership)
+        allocatedMaps = updatesMaps
         return collection
     }
 
     private fun updateAllocatedMap(
         id: UAllocatedMapId<MapType, KeySort, ValueSort, Reg>,
-        updatedMap: UAllocatedMap<MapType, KeySort, ValueSort, Reg>
+        updatedMap: UAllocatedMap<MapType, KeySort, ValueSort, Reg>,
+        ownership: MutabilityOwnership
     ) = UMapMemoryRegion(
         keySort,
         valueSort,
         mapType,
         keyInfo,
-        allocatedMaps.put(id, updatedMap),
+        allocatedMaps.put(id, updatedMap, ownership),
         inputMap
     )
 
@@ -116,32 +117,36 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
         updatedMap
     )
 
-    override fun read(key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>): UExpr<ValueSort> =
+    override fun read(
+        key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>,
+        ownership: MutabilityOwnership
+    ): UExpr<ValueSort> =
         key.mapRef.mapWithStaticAsSymbolic(
             concreteMapper = { concreteRef ->
                 val id = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, concreteRef.address)
-                getAllocatedMap(id).read(key.mapKey)
+                getAllocatedMap(id, ownership).read(key.mapKey, ownership)
             },
-            symbolicMapper = { symbolicRef -> getInputMap().read(symbolicRef to key.mapKey) }
+            symbolicMapper = { symbolicRef -> getInputMap().read(symbolicRef to key.mapKey, ownership) }
         )
 
     override fun write(
         key: UMapEntryLValue<MapType, KeySort, ValueSort, Reg>,
         value: UExpr<ValueSort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.mapRef,
         initial = this,
         initialGuard = guard,
         blockOnConcrete = { region, (concreteRef, guard) ->
             val id = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, concreteRef.address)
-            val map = region.getAllocatedMap(id)
-            val newMap = map.write(key.mapKey, value, guard)
-            region.updateAllocatedMap(id, newMap)
+            val map = region.getAllocatedMap(id, ownership)
+            val newMap = map.write(key.mapKey, value, guard, ownership)
+            region.updateAllocatedMap(id, newMap, ownership)
         },
         blockOnSymbolic = { region, (symbolicRef, guard) ->
             val map = region.getInputMap()
-            val newMap = map.write(symbolicRef to key.mapKey, value, guard)
+            val newMap = map.write(symbolicRef to key.mapKey, value, guard, ownership)
             region.updateInputMap(newMap)
         }
     )
@@ -151,7 +156,8 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
         dstRef: UHeapRef,
         mapType: MapType,
         srcKeySet: USetRegion<MapType, KeySort, *>,
-        initialGuard: UBoolExpr
+        initialGuard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRef2(
         ref0 = srcRef,
         ref1 = dstRef,
@@ -159,20 +165,20 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
         initialGuard = initialGuard,
         blockOnConcrete0Concrete1 = { region, srcConcrete, dstConcrete, guard ->
             val srcId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, srcConcrete.address)
-            val srcCollection = region.getAllocatedMap(srcId)
-            val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address)
+            val srcCollection = region.getAllocatedMap(srcId, ownership)
+            val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address, ownership)
 
             val dstId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, dstConcrete.address)
-            val dstCollection = region.getAllocatedMap(dstId)
+            val dstCollection = region.getAllocatedMap(dstId, ownership)
 
             val adapter = UAllocatedToAllocatedSymbolicMapMergeAdapter(srcKeys)
             val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
-            region.updateAllocatedMap(dstId, newDstCollection)
+            region.updateAllocatedMap(dstId, newDstCollection, ownership)
         },
         blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
             val srcId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, srcConcrete.address)
-            val srcCollection = region.getAllocatedMap(srcId)
-            val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address)
+            val srcCollection = region.getAllocatedMap(srcId, ownership)
+            val srcKeys = srcKeySet.allocatedSetElements(srcConcrete.address, ownership)
 
             val dstCollection = getInputMap()
             val adapter = UAllocatedToInputSymbolicMapMergeAdapter(dstSymbolic, srcKeys)
@@ -184,11 +190,11 @@ internal class UMapMemoryRegion<MapType, KeySort : USort, ValueSort : USort, Reg
             val srcKeys = srcKeySet.inputSetElements()
 
             val dstId = UAllocatedMapId(keySort, valueSort, mapType, keyInfo, dstConcrete.address)
-            val dstCollection = region.getAllocatedMap(dstId)
+            val dstCollection = region.getAllocatedMap(dstId, ownership)
 
             val adapter = UInputToAllocatedSymbolicMapMergeAdapter(srcSymbolic, srcKeys)
             val newDstCollection = dstCollection.copyRange(srcCollection, adapter, guard)
-            region.updateAllocatedMap(dstId, newDstCollection)
+            region.updateAllocatedMap(dstId, newDstCollection, ownership)
         },
         blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
             val srcCollection = region.getInputMap()
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt
index 4d6b2adc84..68762b3330 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionApi.kt
@@ -6,6 +6,7 @@ import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.collection.set.primitive.USetRegion
 import org.usvm.collection.set.primitive.USetRegionId
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.USymbolicCollectionKeyInfo
 import org.usvm.memory.UWritableMemory
 import org.usvm.regions.Region
@@ -18,7 +19,7 @@ internal fun <MapType, KeySort : USort, ValueSort : USort, Reg : Region<Reg>> UW
     sort: ValueSort,
     keyInfo: USymbolicCollectionKeyInfo<UExpr<KeySort>, Reg>,
     keySet: USetRegionId<MapType, KeySort, Nothing>,
-    guard: UBoolExpr
+    guard: UBoolExpr,
 ) {
     val regionId = UMapRegionId(keySort, sort, mapType, keyInfo)
     val region = getRegion(regionId)
@@ -32,6 +33,6 @@ internal fun <MapType, KeySort : USort, ValueSort : USort, Reg : Region<Reg>> UW
         "mapMerge is not applicable to set $region"
     }
 
-    val newRegion = region.merge(srcRef, dstRef, mapType, keySetRegion, guard)
+    val newRegion = region.merge(srcRef, dstRef, mapType, keySetRegion, guard, ownership)
     setRegion(regionId, newRegion)
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionTranslator.kt
index 17f6458518..c420db92fa 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionTranslator.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/UMapRegionTranslator.kt
@@ -154,7 +154,7 @@ private class UInputMapUpdatesTranslator<KeySort : USort, ValueSort : USort>(
 ) : U2DUpdatesTranslator<UAddressSort, KeySort, ValueSort>(exprTranslator, initialValue) {
     override fun KContext.translateRangedUpdate(
         previous: KExpr<KArray2Sort<UAddressSort, KeySort, ValueSort>>,
-        update: URangedUpdateNode<*, *, USymbolicMapKey<KeySort>, ValueSort>
+        update: URangedUpdateNode<*, *, USymbolicMapKey<KeySort>, ValueSort>,
     ): KExpr<KArray2Sort<UAddressSort, KeySort, ValueSort>> {
         check(update.adapter is USymbolicMapMergeAdapter<*, *, USymbolicMapKey<KeySort>, *>) {
             "Unexpected adapter: ${update.adapter}"
@@ -165,7 +165,7 @@ private class UInputMapUpdatesTranslator<KeySort : USort, ValueSort : USort>(
             previous,
             update,
             update.sourceCollection as USymbolicCollection<USymbolicCollectionId<Any, ValueSort, *>, Any, ValueSort>,
-            update.adapter as USymbolicMapMergeAdapter<*, Any, USymbolicMapKey<KeySort>, *>
+            update.adapter as USymbolicMapMergeAdapter<*, Any, USymbolicMapKey<KeySort>, *>,
         )
     }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt
index 6c94e61d88..2ae4440fbf 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/primitive/USymbolicMapMergeAdapter.kt
@@ -63,7 +63,7 @@ class UAllocatedToAllocatedSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<UExpr<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: UExpr<KeySort>,
-        composer: UComposer<*, *>,
+        composer: UComposer<*, *>
     ) {
         check(srcCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $dstCollectionId" }
@@ -114,7 +114,7 @@ class UAllocatedToInputSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<USymbolicMapKey<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: UExpr<KeySort>,
-        composer: UComposer<*, *>,
+        composer: UComposer<*, *>
     ) {
         check(srcCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $dstCollectionId" }
@@ -166,7 +166,7 @@ class UInputToAllocatedSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<UExpr<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: USymbolicMapKey<KeySort>,
-        composer: UComposer<*, *>,
+        composer: UComposer<*, *>
     ) {
         check(srcCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is UAllocatedMapId<*, KeySort, *, *>) { "Unexpected collection: $dstCollectionId" }
@@ -219,7 +219,7 @@ class UInputToInputSymbolicMapMergeAdapter<MapType, KeySort : USort>(
         dstCollectionId: USymbolicCollectionId<USymbolicMapKey<KeySort>, *, *>,
         guard: UBoolExpr,
         srcKey: USymbolicMapKey<KeySort>,
-        composer: UComposer<*, *>,
+        composer: UComposer<*, *>
     ) {
         check(srcCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $srcCollectionId" }
         check(dstCollectionId is USymbolicMapId<*, *, *, *, *, *, *>) { "Unexpected collection: $dstCollectionId" }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt
index 126aa229ba..a5aef9aa2a 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapModelRegion.kt
@@ -4,6 +4,7 @@ import org.usvm.UAddressSort
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.collection.map.USymbolicMapKey
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UModelEvaluator
 import org.usvm.model.modelEnsureConcreteInputRef
@@ -14,9 +15,9 @@ abstract class URefMapModelRegion<MapType, ValueSort : USort>(
 ) : UReadOnlyMemoryRegion<URefMapEntryLValue<MapType, ValueSort>, ValueSort> {
     abstract val inputMap: UReadOnlyMemoryRegion<USymbolicMapKey<UAddressSort>, ValueSort>
 
-    override fun read(key: URefMapEntryLValue<MapType, ValueSort>): UExpr<ValueSort> {
+    override fun read(key: URefMapEntryLValue<MapType, ValueSort>, ownership: MutabilityOwnership): UExpr<ValueSort> {
         val mapRef = modelEnsureConcreteInputRef(key.mapRef)
-        return inputMap.read(mapRef to key.mapKey)
+        return inputMap.read(mapRef to key.mapKey, ownership)
     }
 }
 
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 a842d980d1..ea16b54c22 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
@@ -1,7 +1,5 @@
 package org.usvm.collection.map.ref
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
@@ -12,6 +10,9 @@ import org.usvm.USort
 import org.usvm.collection.map.USymbolicMapKey
 import org.usvm.collection.set.ref.URefSetEntryLValue
 import org.usvm.collection.set.ref.URefSetRegion
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -52,7 +53,8 @@ interface URefMapRegion<MapType, ValueSort : USort>
         mapType: MapType,
         sort: ValueSort,
         keySet: URefSetRegion<MapType>,
-        operationGuard: UBoolExpr
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): URefMapRegion<MapType, ValueSort>
 }
 
@@ -73,14 +75,14 @@ internal data class UAllocatedRefMapWithAllocatedKeysId(
 internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
     private val valueSort: ValueSort,
     private val mapType: MapType,
-    private var allocatedMapWithAllocatedKeys: PersistentMap<UAllocatedRefMapWithAllocatedKeysId, UExpr<ValueSort>> = persistentHashMapOf(),
-    private var inputMapWithAllocatedKeys: PersistentMap<UInputRefMapWithAllocatedKeysId<MapType, ValueSort>, UInputRefMapWithAllocatedKeys<MapType, ValueSort>> = persistentHashMapOf(),
-    private var allocatedMapWithInputKeys: PersistentMap<UAllocatedRefMapWithInputKeysId<MapType, ValueSort>, UAllocatedRefMapWithInputKeys<MapType, ValueSort>> = persistentHashMapOf(),
+    private var allocatedMapWithAllocatedKeys: UPersistentHashMap<UAllocatedRefMapWithAllocatedKeysId, UExpr<ValueSort>> = persistentHashMapOf(),
+    private var inputMapWithAllocatedKeys: UPersistentHashMap<UInputRefMapWithAllocatedKeysId<MapType, ValueSort>, UInputRefMapWithAllocatedKeys<MapType, ValueSort>> = persistentHashMapOf(),
+    private var allocatedMapWithInputKeys: UPersistentHashMap<UAllocatedRefMapWithInputKeysId<MapType, ValueSort>, UAllocatedRefMapWithInputKeys<MapType, ValueSort>> = persistentHashMapOf(),
     private var inputMapWithInputKeys: UInputRefMap<MapType, ValueSort>? = null,
 ) : URefMapRegion<MapType, ValueSort> {
 
     private fun updateAllocatedMapWithAllocatedKeys(
-        updated: PersistentMap<UAllocatedRefMapWithAllocatedKeysId, UExpr<ValueSort>>
+        updated: UPersistentHashMap<UAllocatedRefMapWithAllocatedKeysId, UExpr<ValueSort>>
     ) = URefMapMemoryRegion(
         valueSort,
         mapType,
@@ -94,24 +96,23 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         UInputRefMapWithAllocatedKeysId(valueSort, mapType, keyAddress)
 
     private fun getInputMapWithAllocatedKeys(
-        id: UInputRefMapWithAllocatedKeysId<MapType, ValueSort>
+        id: UInputRefMapWithAllocatedKeysId<MapType, ValueSort>,
+        ownership: MutabilityOwnership
     ): UInputRefMapWithAllocatedKeys<MapType, ValueSort> {
-        var collection = inputMapWithAllocatedKeys[id]
-        if (collection == null) {
-            collection = id.emptyRegion()
-            inputMapWithAllocatedKeys = inputMapWithAllocatedKeys.put(id, collection)
-        }
+        val (updatedMap, collection) = inputMapWithAllocatedKeys.getOrPut(id, id.emptyRegion(), ownership)
+        inputMapWithAllocatedKeys = updatedMap
         return collection
     }
 
     private fun updateInputMapWithAllocatedKeys(
         id: UInputRefMapWithAllocatedKeysId<MapType, ValueSort>,
-        updatedMap: UInputRefMapWithAllocatedKeys<MapType, ValueSort>
+        updatedMap: UInputRefMapWithAllocatedKeys<MapType, ValueSort>,
+        ownership: MutabilityOwnership
     ) = URefMapMemoryRegion(
         valueSort,
         mapType,
         allocatedMapWithAllocatedKeys,
-        inputMapWithAllocatedKeys.put(id, updatedMap),
+        inputMapWithAllocatedKeys.put(id, updatedMap, ownership),
         allocatedMapWithInputKeys,
         inputMapWithInputKeys
     )
@@ -120,25 +121,24 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         UAllocatedRefMapWithInputKeysId(valueSort, mapType, mapAddress)
 
     private fun getAllocatedMapWithInputKeys(
-        id: UAllocatedRefMapWithInputKeysId<MapType, ValueSort>
+        id: UAllocatedRefMapWithInputKeysId<MapType, ValueSort>,
+        ownership: MutabilityOwnership
     ): UAllocatedRefMapWithInputKeys<MapType, ValueSort> {
-        var collection = allocatedMapWithInputKeys[id]
-        if (collection == null) {
-            collection = id.emptyRegion()
-            allocatedMapWithInputKeys = allocatedMapWithInputKeys.put(id, collection)
-        }
+        val  (updatedMap, collection) = allocatedMapWithInputKeys.getOrPut(id, id.emptyRegion(), ownership)
+        allocatedMapWithInputKeys = updatedMap
         return collection
     }
 
     private fun updateAllocatedMapWithInputKeys(
         id: UAllocatedRefMapWithInputKeysId<MapType, ValueSort>,
-        updatedMap: UAllocatedRefMapWithInputKeys<MapType, ValueSort>
+        updatedMap: UAllocatedRefMapWithInputKeys<MapType, ValueSort>,
+        ownership: MutabilityOwnership
     ) = URefMapMemoryRegion(
         valueSort,
         mapType,
         allocatedMapWithAllocatedKeys,
         inputMapWithAllocatedKeys,
-        allocatedMapWithInputKeys.put(id, updatedMap),
+        allocatedMapWithInputKeys.put(id, updatedMap, ownership),
         inputMapWithInputKeys
     )
 
@@ -160,7 +160,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
             updatedMap
         )
 
-    override fun read(key: URefMapEntryLValue<MapType, ValueSort>): UExpr<ValueSort> =
+    override fun read(key: URefMapEntryLValue<MapType, ValueSort>, ownership: MutabilityOwnership): UExpr<ValueSort> =
         key.mapRef.mapWithStaticAsSymbolic(
             concreteMapper = { concreteRef ->
                 key.mapKey.mapWithStaticAsSymbolic(
@@ -170,7 +170,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                     },
                     symbolicMapper = { symbolicKey ->
                         val id = allocatedMapWithInputKeyId(concreteRef.address)
-                        getAllocatedMapWithInputKeys(id).read(symbolicKey)
+                        getAllocatedMapWithInputKeys(id, ownership).read(symbolicKey, ownership)
                     }
                 )
             },
@@ -178,10 +178,10 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                 key.mapKey.mapWithStaticAsSymbolic(
                     concreteMapper = { concreteKey ->
                         val id = inputMapWithAllocatedKeyId(concreteKey.address)
-                        getInputMapWithAllocatedKeys(id).read(symbolicRef)
+                        getInputMapWithAllocatedKeys(id, ownership).read(symbolicRef, ownership)
                     },
                     symbolicMapper = { symbolicKey ->
-                        getInputMapWithInputKeys().read(symbolicRef to symbolicKey)
+                        getInputMapWithInputKeys().read(symbolicRef to symbolicKey, ownership)
                     }
                 )
             }
@@ -190,7 +190,8 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
     override fun write(
         key: URefMapEntryLValue<MapType, ValueSort>,
         value: UExpr<ValueSort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership,
     ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.mapRef,
         initial = this,
@@ -202,16 +203,16 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                 initialGuard = mapGuard,
                 blockOnConcrete = { region, (concreteKeyRef, guard) ->
                     val id = UAllocatedRefMapWithAllocatedKeysId(concreteMapRef.address, concreteKeyRef.address)
-                    val newMap = region.allocatedMapWithAllocatedKeys.guardedWrite(id, value, guard) {
+                    val newMap = region.allocatedMapWithAllocatedKeys.guardedWrite(id, value, guard, ownership) {
                         valueSort.sampleUValue()
                     }
                     region.updateAllocatedMapWithAllocatedKeys(newMap)
                 },
                 blockOnSymbolic = { region, (symbolicKeyRef, guard) ->
                     val id = allocatedMapWithInputKeyId(concreteMapRef.address)
-                    val newMap = region.getAllocatedMapWithInputKeys(id)
-                        .write(symbolicKeyRef, value, guard)
-                    region.updateAllocatedMapWithInputKeys(id, newMap)
+                    val newMap = region.getAllocatedMapWithInputKeys(id, ownership)
+                        .write(symbolicKeyRef, value, guard, ownership)
+                    region.updateAllocatedMapWithInputKeys(id, newMap, ownership)
                 }
             )
         },
@@ -222,13 +223,13 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                 initialGuard = mapGuard,
                 blockOnConcrete = { region, (concreteKeyRef, guard) ->
                     val id = inputMapWithAllocatedKeyId(concreteKeyRef.address)
-                    val newMap = region.getInputMapWithAllocatedKeys(id)
-                        .write(symbolicMapRef, value, guard)
-                    region.updateInputMapWithAllocatedKeys(id, newMap)
+                    val newMap = region.getInputMapWithAllocatedKeys(id, ownership)
+                        .write(symbolicMapRef, value, guard, ownership)
+                    region.updateInputMapWithAllocatedKeys(id, newMap, ownership)
                 },
                 blockOnSymbolic = { region, (symbolicKeyRef, guard) ->
                     val newMap = region.getInputMapWithInputKeys()
-                        .write(symbolicMapRef to symbolicKeyRef, value, guard)
+                        .write(symbolicMapRef to symbolicKeyRef, value, guard, ownership)
                     region.updateInputMapWithInputKeys(newMap)
                 }
             )
@@ -255,7 +256,8 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         mapType: MapType,
         sort: ValueSort,
         keySet: URefSetRegion<MapType>,
-        operationGuard: UBoolExpr
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRef2(
         ref0 = srcRef,
         ref1 = dstRef,
@@ -268,41 +270,42 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
                 srcMapRef = srcConcrete,
                 guard = guard,
                 keySet = keySet,
+                ownership = ownership,
                 read = { initialAllocatedMapState[it] ?: valueSort.sampleUValue() },
                 mkDstKeyId = { UAllocatedRefMapWithAllocatedKeysId(dstConcrete.address, it) },
                 write = { result, dstKeyId, value, g ->
-                    result.guardedWrite(dstKeyId, value, g) { valueSort.sampleUValue() }
+                    result.guardedWrite(dstKeyId, value, g, ownership) { valueSort.sampleUValue() }
                 }
             )
             val updatedRegion = region.updateAllocatedMapWithAllocatedKeys(updatedAllocatedMap)
 
-            val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address)
+            val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address, ownership)
             val srcInputKeysId = updatedRegion.allocatedMapWithInputKeyId(srcConcrete.address)
-            val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId)
+            val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId, ownership)
 
             val dstInputKeysId = updatedRegion.allocatedMapWithInputKeyId(dstConcrete.address)
-            val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId)
+            val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId, ownership)
 
             val adapter = UAllocatedToAllocatedSymbolicRefMapMergeAdapter(srcKeys)
             val updatedDstCollection = dstInputKeysCollection.copyRange(srcInputKeysCollection, adapter, guard)
-            updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection)
+            updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, ownership)
         },
         blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
             val initialAllocatedMapState = region.allocatedMapWithAllocatedKeys
             val updatedRegion = region.mergeAllocatedMapAllocatedKeys(
-                initial = region, srcMapRef = srcConcrete, guard = guard, keySet = keySet,
+                initial = region, srcMapRef = srcConcrete, guard = guard, keySet = keySet, ownership = ownership,
                 read = { initialAllocatedMapState[it] ?: valueSort.sampleUValue() },
                 mkDstKeyId = { inputMapWithAllocatedKeyId(it) },
                 write = { result, dstKeyId, value, g ->
-                    val newMap = result.getInputMapWithAllocatedKeys(dstKeyId)
-                        .write(dstSymbolic, value, g)
-                    result.updateInputMapWithAllocatedKeys(dstKeyId, newMap)
+                    val newMap = result.getInputMapWithAllocatedKeys(dstKeyId, ownership)
+                        .write(dstSymbolic, value, g, ownership)
+                    result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, ownership)
                 }
             )
 
-            val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address)
+            val srcKeys = keySet.allocatedSetWithInputElements(srcConcrete.address, ownership)
             val srcInputKeysId = updatedRegion.allocatedMapWithInputKeyId(srcConcrete.address)
-            val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId)
+            val srcInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(srcInputKeysId, ownership)
 
             val dstInputKeysCollection = updatedRegion.getInputMapWithInputKeys()
 
@@ -313,11 +316,11 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         blockOnSymbolic0Concrete1 = { region, srcSymbolic, dstConcrete, guard ->
             val updatedAllocatedMap = region.mergeInputMapAllocatedKeys(
                 initial = region.allocatedMapWithAllocatedKeys,
-                srcMapRef = srcSymbolic, guard = guard, keySet = keySet,
-                read = { region.getInputMapWithAllocatedKeys(it).read(srcSymbolic) },
+                srcMapRef = srcSymbolic, guard = guard, keySet = keySet, ownership = ownership,
+                read = { region.getInputMapWithAllocatedKeys(it, ownership).read(srcSymbolic, ownership) },
                 mkDstKeyId = { UAllocatedRefMapWithAllocatedKeysId(dstConcrete.address, it) },
                 write = { result, dstKeyId, value, g ->
-                    result.guardedWrite(dstKeyId, value, g) { sort.sampleUValue() }
+                    result.guardedWrite(dstKeyId, value, g, ownership) { sort.sampleUValue() }
                 }
             )
             val updatedRegion = region.updateAllocatedMapWithAllocatedKeys(updatedAllocatedMap)
@@ -326,21 +329,21 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
             val srcInputKeysCollection = updatedRegion.getInputMapWithInputKeys()
 
             val dstInputKeysId = updatedRegion.allocatedMapWithInputKeyId(dstConcrete.address)
-            val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId)
+            val dstInputKeysCollection = updatedRegion.getAllocatedMapWithInputKeys(dstInputKeysId, ownership)
 
             val adapter = UInputToAllocatedSymbolicRefMapMergeAdapter(srcSymbolic, srcKeys)
             val updatedDstCollection = dstInputKeysCollection.copyRange(srcInputKeysCollection, adapter, guard)
-            updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection)
+            updatedRegion.updateAllocatedMapWithInputKeys(dstInputKeysId, updatedDstCollection, ownership)
         },
         blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
             val updatedRegion = region.mergeInputMapAllocatedKeys(
-                initial = region, srcMapRef = srcSymbolic, guard = guard, keySet = keySet,
-                read = { region.getInputMapWithAllocatedKeys(it).read(srcSymbolic) },
+                initial = region, srcMapRef = srcSymbolic, guard = guard, keySet = keySet, ownership = ownership,
+                read = { region.getInputMapWithAllocatedKeys(it, ownership).read(srcSymbolic, ownership) },
                 mkDstKeyId = { inputMapWithAllocatedKeyId(it) },
                 write = { result, dstKeyId, value, g ->
-                    val newMap = result.getInputMapWithAllocatedKeys(dstKeyId)
-                        .write(dstSymbolic, value, g)
-                    result.updateInputMapWithAllocatedKeys(dstKeyId, newMap)
+                    val newMap = result.getInputMapWithAllocatedKeys(dstKeyId, ownership)
+                        .write(dstSymbolic, value, g, ownership)
+                    result.updateInputMapWithAllocatedKeys(dstKeyId, newMap, ownership)
                 }
             )
             val srcKeys = keySet.inputSetWithInputElements()
@@ -359,15 +362,17 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         srcMapRef: UHeapRef,
         guard: UBoolExpr,
         keySet: URefSetRegion<MapType>,
+        ownership: MutabilityOwnership,
         read: (UInputRefMapWithAllocatedKeysId<MapType, ValueSort>) -> UExpr<ValueSort>,
         mkDstKeyId: (UConcreteHeapAddress) -> DstKeyId,
         write: (R, DstKeyId, UExpr<ValueSort>, UBoolExpr) -> R
     ) = mergeAllocatedKeys(
         initial,
-        inputMapWithAllocatedKeys.keys,
+        inputMapWithAllocatedKeys.keys(),
         guard,
         keySet,
         srcMapRef,
+        ownership,
         { it.keyAddress },
         read,
         mkDstKeyId,
@@ -379,15 +384,17 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         srcMapRef: UConcreteHeapRef,
         guard: UBoolExpr,
         keySet: URefSetRegion<MapType>,
+        ownership: MutabilityOwnership,
         read: (UAllocatedRefMapWithAllocatedKeysId) -> UExpr<ValueSort>,
         mkDstKeyId: (UConcreteHeapAddress) -> DstKeyId,
         write: (R, DstKeyId, UExpr<ValueSort>, UBoolExpr) -> R
     ) = mergeAllocatedKeys(
         initial,
-        allocatedMapWithAllocatedKeys.keys.filter { it.mapAddress == srcMapRef.address },
+        allocatedMapWithAllocatedKeys.keys().filter { it.mapAddress == srcMapRef.address },
         guard,
         keySet,
         srcMapRef,
+        ownership,
         { it.keyAddress },
         read,
         mkDstKeyId,
@@ -400,6 +407,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         guard: UBoolExpr,
         keySet: URefSetRegion<MapType>,
         srcMapRef: UHeapRef,
+        ownership: MutabilityOwnership,
         srcKeyConcreteAddress: (SrcKeyId) -> UConcreteHeapAddress,
         read: (SrcKeyId) -> UExpr<ValueSort>,
         mkDstKeyId: (UConcreteHeapAddress) -> DstKeyId,
@@ -409,7 +417,7 @@ internal class URefMapMemoryRegion<MapType, ValueSort : USort>(
         val srcValue = read(srcKeyId)
 
         val keyRef = guard.uctx.mkConcreteHeapRef(srcKeyAddress)
-        val srcContains = keySet.read(URefSetEntryLValue(srcMapRef, keyRef, mapType))
+        val srcContains = keySet.read(URefSetEntryLValue(srcMapRef, keyRef, mapType), ownership)
         val mergedGuard = guard.uctx.mkAnd(srcContains, guard)
 
         write(result, mkDstKeyId(srcKeyAddress), srcValue, mergedGuard)
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt
index b66dba4dc4..1eb6bb396a 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionApi.kt
@@ -27,6 +27,6 @@ internal fun <MapType, ValueSort : USort> UWritableMemory<*>.refMapMerge(
         "refMapMerge is not applicable to set $region"
     }
 
-    val newRegion = region.merge(srcRef, dstRef, mapType, sort, keySet, guard)
+    val newRegion = region.merge(srcRef, dstRef, mapType, sort, keySet, guard, ownership)
     setRegion(regionId, newRegion)
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt
index 422249e38c..c955e4ecc0 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/map/ref/URefMapRegionTranslator.kt
@@ -153,7 +153,7 @@ private class UAllocatedRefMapUpdatesTranslator<ValueSort : USort>(
             previous,
             update,
             update.sourceCollection as USymbolicCollection<USymbolicCollectionId<Any, ValueSort, *>, Any, ValueSort>,
-            update.adapter as USymbolicRefMapMergeAdapter<*, Any, UHeapRef, *>
+            update.adapter as USymbolicRefMapMergeAdapter<*, Any, UHeapRef, *>,
         )
     }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt
index 5af60da358..3dc300ed58 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/USetCollectionDecoder.kt
@@ -5,7 +5,7 @@ import io.ksmt.expr.KExpr
 import io.ksmt.expr.KFunctionApp
 import io.ksmt.sort.KBoolSort
 import io.ksmt.utils.uncheckedCast
-import kotlinx.collections.immutable.persistentHashMapOf
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
@@ -41,7 +41,7 @@ abstract class USetCollectionDecoder<ElementSort : USort> {
         val usedSetKeys = hashSetOf<KFunctionApp<KBoolSort>>()
         assertions.flatMapTo(usedSetKeys) { appCollector.applyVisitor(it) }
 
-        val entries = persistentHashMapOf<USymbolicSetElement<ElementSort>, UBoolExpr>().builder()
+        var entries = persistentHashMapOf<USymbolicSetElement<ElementSort>, UBoolExpr>()
         for (key in usedSetKeys) {
             val keyInSet = model.eval(key, isComplete = false)
             if (!keyInSet.isTrue) continue
@@ -49,13 +49,13 @@ abstract class USetCollectionDecoder<ElementSort : USort> {
             val (rawSetRef, rawElement) = key.args
             val setRef: UHeapRef = rawSetRef.uncheckedCast()
             val element: UExpr<ElementSort> = rawElement.uncheckedCast()
-
+ 
             val setRefModel = model.eval(setRef, isComplete = true).mapAddress(mapping)
             val elementModel = model.eval(element, isComplete = true).mapAddress(mapping)
 
-            entries[setRefModel to elementModel] = inputFunction.ctx.trueExpr
+            entries = entries.put(setRefModel to elementModel, inputFunction.ctx.trueExpr, evaluator.ctx.defaultOwnership)
         }
 
-        return UMemory2DArray(entries.build(), constValue = inputFunction.ctx.falseExpr)
+        return UMemory2DArray(entries, constValue = inputFunction.ctx.falseExpr)
     }
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt
index 36ac911376..c881ddd529 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetModelRegion.kt
@@ -8,6 +8,7 @@ import org.usvm.UBoolSort
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.collection.set.USetCollectionDecoder
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.isFalse
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UMemory2DArray
@@ -21,18 +22,18 @@ abstract class USetModelRegion<SetType, ElementSort : USort, Reg : Region<Reg>>(
     USetReadOnlyRegion<SetType, ElementSort, Reg> {
     abstract val inputSet: UMemory2DArray<UAddressSort, ElementSort, UBoolSort>
 
-    override fun read(key: USetEntryLValue<SetType, ElementSort, Reg>): UBoolExpr {
+    override fun read(key: USetEntryLValue<SetType, ElementSort, Reg>, ownership: MutabilityOwnership): UBoolExpr {
         val setRef = modelEnsureConcreteInputRef(key.setRef)
-        return inputSet.read(setRef to key.setElement)
+        return inputSet.read(setRef to key.setElement, ownership)
     }
 
-    override fun setEntries(ref: UHeapRef): UPrimitiveSetEntries<SetType, ElementSort, Reg> = with(regionId) {
+    override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): UPrimitiveSetEntries<SetType, ElementSort, Reg> = with(regionId) {
         val setRef = modelEnsureConcreteInputRef(ref)
 
         check(inputSet.constValue.isFalse) { "Set model is not complete" }
 
         val result = UPrimitiveSetEntries<SetType, ElementSort, Reg>()
-        inputSet.values.keys.forEach {
+        inputSet.values.keys().forEach {
             if (it.first == setRef) {
                 result.add(USetEntryLValue(elementSort, setRef, it.second, setType, elementInfo))
             }
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 74ec7eeed3..35921cd7fe 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
@@ -1,7 +1,6 @@
 package org.usvm.collection.set.primitive
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UConcreteHeapAddress
@@ -11,6 +10,8 @@ import org.usvm.USort
 import org.usvm.collection.set.USymbolicSetEntries
 import org.usvm.collection.set.USymbolicSetElement
 import org.usvm.collection.set.USymbolicSetElementsCollector
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -62,14 +63,14 @@ typealias UPrimitiveSetEntries<SetType, ElementSort, Reg> = USymbolicSetEntries<
 
 interface USetReadOnlyRegion<SetType, ElementSort : USort, Reg : Region<Reg>> :
     UReadOnlyMemoryRegion<USetEntryLValue<SetType, ElementSort, Reg>, UBoolSort> {
-    fun setEntries(ref: UHeapRef): UPrimitiveSetEntries<SetType, ElementSort, Reg>
+    fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): UPrimitiveSetEntries<SetType, ElementSort, Reg>
 }
 
 interface USetRegion<SetType, ElementSort : USort, Reg : Region<Reg>> :
     USetReadOnlyRegion<SetType, ElementSort, Reg>,
     UMemoryRegion<USetEntryLValue<SetType, ElementSort, Reg>, UBoolSort> {
 
-    fun allocatedSetElements(address: UConcreteHeapAddress): UAllocatedSet<SetType, ElementSort, Reg>
+    fun allocatedSetElements(address: UConcreteHeapAddress, ownership: MutabilityOwnership): UAllocatedSet<SetType, ElementSort, Reg>
 
     fun inputSetElements(): UInputSet<SetType, ElementSort, Reg>
 
@@ -77,6 +78,7 @@ interface USetRegion<SetType, ElementSort : USort, Reg : Region<Reg>> :
         srcRef: UHeapRef,
         dstRef: UHeapRef,
         operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): USetRegion<SetType, ElementSort, Reg>
 }
 
@@ -84,7 +86,7 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
     private val setType: SetType,
     private val elementSort: ElementSort,
     private val elementInfo: USymbolicCollectionKeyInfo<UExpr<ElementSort>, Reg>,
-    private var allocatedSets: PersistentMap<UAllocatedSetId<SetType, ElementSort, Reg>, UAllocatedSet<SetType, ElementSort, Reg>> = persistentHashMapOf(),
+    private var allocatedSets: UPersistentHashMap<UAllocatedSetId<SetType, ElementSort, Reg>, UAllocatedSet<SetType, ElementSort, Reg>> = persistentHashMapOf(),
     private var inputSet: UInputSet<SetType, ElementSort, Reg>? = null,
 ) : USetRegion<SetType, ElementSort, Reg> {
     init {
@@ -93,24 +95,26 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
         }
     }
 
-    override fun allocatedSetElements(address: UConcreteHeapAddress): UAllocatedSet<SetType, ElementSort, Reg> =
-        getAllocatedSet(UAllocatedSetId(address, elementSort, setType, elementInfo))
+    override fun allocatedSetElements(
+        address: UConcreteHeapAddress,
+        ownership: MutabilityOwnership
+    ): UAllocatedSet<SetType, ElementSort, Reg> =
+        getAllocatedSet(UAllocatedSetId(address, elementSort, setType, elementInfo), ownership)
 
     private fun getAllocatedSet(
-        id: UAllocatedSetId<SetType, ElementSort, Reg>
+        id: UAllocatedSetId<SetType, ElementSort, Reg>,
+        ownership: MutabilityOwnership,
     ): UAllocatedSet<SetType, ElementSort, Reg> {
-        var collection = allocatedSets[id]
-        if (collection == null) {
-            collection = id.emptyRegion()
-            allocatedSets = allocatedSets.put(id, collection)
-        }
+        val (updatesSets, collection) = allocatedSets.getOrPut(id, id.emptyRegion(), ownership)
+        allocatedSets = updatesSets
         return collection
     }
 
     private fun updateAllocatedSet(
         id: UAllocatedSetId<SetType, ElementSort, Reg>,
-        updated: UAllocatedSet<SetType, ElementSort, Reg>
-    ) = USetMemoryRegion(setType, elementSort, elementInfo, allocatedSets.put(id, updated), inputSet)
+        updated: UAllocatedSet<SetType, ElementSort, Reg>,
+        ownership: MutabilityOwnership,
+    ) = USetMemoryRegion(setType, elementSort, elementInfo, allocatedSets.put(id, updated, ownership), inputSet)
 
     override fun inputSetElements(): UInputSet<SetType, ElementSort, Reg> {
         if (inputSet == null) {
@@ -122,29 +126,29 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
     private fun updateInputSet(updated: UInputSet<SetType, ElementSort, Reg>) =
         USetMemoryRegion(setType, elementSort, elementInfo, allocatedSets, updated)
 
-    override fun read(key: USetEntryLValue<SetType, ElementSort, Reg>): UExpr<UBoolSort> =
+    override fun read(key: USetEntryLValue<SetType, ElementSort, Reg>, ownership: MutabilityOwnership): UExpr<UBoolSort> =
         key.setRef.mapWithStaticAsSymbolic(
-            { concreteRef -> allocatedSetElements(concreteRef.address).read(key.setElement) },
-            { symbolicRef -> inputSetElements().read(symbolicRef to key.setElement) }
+            { concreteRef -> allocatedSetElements(concreteRef.address, ownership).read(key.setElement, ownership) },
+            { symbolicRef -> inputSetElements().read(symbolicRef to key.setElement, ownership) }
         )
-
     override fun write(
         key: USetEntryLValue<SetType, ElementSort, Reg>,
         value: UExpr<UBoolSort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.setRef,
         initial = this,
         initialGuard = guard,
         blockOnConcrete = { region, (concreteRef, guard) ->
             val id = UAllocatedSetId(concreteRef.address, elementSort, setType, elementInfo)
-            val newCollection = region.getAllocatedSet(id)
-                .write(key.setElement, value, guard)
-            region.updateAllocatedSet(id, newCollection)
+            val newCollection = region.getAllocatedSet(id, ownership)
+                .write(key.setElement, value, guard, ownership)
+            region.updateAllocatedSet(id, newCollection, ownership)
         },
         blockOnSymbolic = { region, (symbolicRef, guard) ->
             val newCollection = region.inputSetElements()
-                .write(symbolicRef to key.setElement, value, guard)
+                .write(symbolicRef to key.setElement, value, guard, ownership)
             region.updateInputSet(newCollection)
         }
     )
@@ -152,7 +156,8 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
     override fun union(
         srcRef: UHeapRef,
         dstRef: UHeapRef,
-        operationGuard: UBoolExpr
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership,
     ) = foldHeapRef2(
         ref0 = srcRef,
         ref1 = dstRef,
@@ -160,18 +165,18 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
         initialGuard = operationGuard,
         blockOnConcrete0Concrete1 = { region, srcConcrete, dstConcrete, guard ->
             val srcId = UAllocatedSetId(srcConcrete.address, elementSort, setType, elementInfo)
-            val srcCollection = region.getAllocatedSet(srcId)
+            val srcCollection = region.getAllocatedSet(srcId, ownership)
 
             val dstId = UAllocatedSetId(dstConcrete.address, elementSort, setType, elementInfo)
-            val dstCollection = region.getAllocatedSet(dstId)
+            val dstCollection = region.getAllocatedSet(dstId, ownership)
 
             val adapter = UAllocatedToAllocatedSymbolicSetUnionAdapter(srcCollection)
             val updated = dstCollection.copyRange(srcCollection, adapter, guard)
-            region.updateAllocatedSet(dstId, updated)
+            region.updateAllocatedSet(dstId, updated, ownership)
         },
         blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
             val srcId = UAllocatedSetId(srcConcrete.address, elementSort, setType, elementInfo)
-            val srcCollection = region.getAllocatedSet(srcId)
+            val srcCollection = region.getAllocatedSet(srcId, ownership)
 
             val dstCollection = region.inputSetElements()
 
@@ -183,11 +188,11 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
             val srcCollection = region.inputSetElements()
 
             val dstId = UAllocatedSetId(dstConcrete.address, elementSort, setType, elementInfo)
-            val dstCollection = region.getAllocatedSet(dstId)
+            val dstCollection = region.getAllocatedSet(dstId, ownership)
 
             val adapter = UInputToAllocatedSymbolicSetUnionAdapter(srcSymbolic, srcCollection)
             val updated = dstCollection.copyRange(srcCollection, adapter, guard)
-            region.updateAllocatedSet(dstId, updated)
+            region.updateAllocatedSet(dstId, updated, ownership)
         },
         blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
             val srcCollection = region.inputSetElements()
@@ -199,13 +204,13 @@ internal class USetMemoryRegion<SetType, ElementSort : USort, Reg : Region<Reg>>
         },
     )
 
-    override fun setEntries(ref: UHeapRef): UPrimitiveSetEntries<SetType, ElementSort, Reg> =
+    override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): UPrimitiveSetEntries<SetType, ElementSort, Reg> =
         foldHeapRefWithStaticAsSymbolic(
             ref = ref,
             initial = UPrimitiveSetEntries(),
             initialGuard = ref.uctx.trueExpr,
             blockOnConcrete = { entries, (concreteRef, _) ->
-                val setElements = allocatedSetElements(concreteRef.address)
+                val setElements = allocatedSetElements(concreteRef.address, ownership)
                 val elements = USymbolicSetElementsCollector.collect(setElements.updates)
                 elements.elements.forEach { elem ->
                     entries.add(USetEntryLValue(elementSort, concreteRef, elem, setType, elementInfo))
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt
index 5d463a20f8..b8cc054bd4 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USetRegionApi.kt
@@ -4,6 +4,7 @@ import org.usvm.UBoolExpr
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.USymbolicCollectionKeyInfo
 import org.usvm.memory.UWritableMemory
@@ -24,7 +25,7 @@ internal fun <SetType, KeySort : USort, Reg : Region<Reg>> UWritableMemory<*>.se
         "setUnion is not applicable to $region"
     }
 
-    val newRegion = region.union(srcRef, dstRef, guard)
+    val newRegion = region.union(srcRef, dstRef, guard, ownership)
     setRegion(regionId, newRegion)
 }
 
@@ -38,5 +39,5 @@ fun <SetType, KeySort : USort, Reg : Region<Reg>> UReadOnlyMemory<*>.setEntries(
     val region = getRegion(regionId) as? USetReadOnlyRegion<SetType, KeySort, Reg>
         ?: return UPrimitiveSetEntries<SetType, KeySort, Reg>().apply { markAsInput() }
 
-    return region.setEntries(setRef)
+    return region.setEntries(setRef, ownership)
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
index 6a387f8c57..de974e427b 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/primitive/USymbolicSetUnionAdapter.kt
@@ -251,7 +251,7 @@ class UInputToInputSymbolicSetUnionAdapter<SetType, ElemSort : USort>(
                 dstCollectionId.setType,
                 dstCollectionId.elementSort,
                 dstCollectionId.keyInfo() as USymbolicCollectionKeyInfo<UExpr<USort>, Nothing>,
-                guard
+                guard 
             )
         }
     }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt
index 36c8df5ff9..e0995de2b7 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetModelRegion.kt
@@ -7,6 +7,7 @@ import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UHeapRef
 import org.usvm.collection.set.USetCollectionDecoder
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.isFalse
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.model.UMemory2DArray
@@ -18,18 +19,18 @@ abstract class URefSetModelRegion<SetType>(
 ) : UReadOnlyMemoryRegion<URefSetEntryLValue<SetType>, UBoolSort>, URefSetReadOnlyRegion<SetType> {
     abstract val inputSet: UMemory2DArray<UAddressSort, UAddressSort, UBoolSort>
 
-    override fun read(key: URefSetEntryLValue<SetType>): UBoolExpr {
+    override fun read(key: URefSetEntryLValue<SetType>, ownership: MutabilityOwnership): UBoolExpr {
         val setRef = modelEnsureConcreteInputRef(key.setRef)
-        return inputSet.read(setRef to key.setElement)
+        return inputSet.read(setRef to key.setElement, ownership)
     }
 
-    override fun setEntries(ref: UHeapRef): URefSetEntries<SetType> {
+    override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): URefSetEntries<SetType> {
         val setRef = modelEnsureConcreteInputRef(ref)
 
         check(inputSet.constValue.isFalse) { "Set model is not complete" }
 
         val result = URefSetEntries<SetType>()
-        inputSet.values.keys.forEach {
+        inputSet.values.keys().forEach {
             if (it.first == setRef) {
                 result.add(URefSetEntryLValue(setRef, it.second, regionId.setType))
             }
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 27de317e53..bf8281fccb 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
@@ -1,7 +1,5 @@
 package org.usvm.collection.set.ref
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
@@ -10,6 +8,9 @@ import org.usvm.UHeapRef
 import org.usvm.collection.set.USymbolicSetEntries
 import org.usvm.collection.set.USymbolicSetElement
 import org.usvm.collection.set.USymbolicSetElementsCollector
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -62,33 +63,34 @@ typealias URefSetEntries<SetType> = USymbolicSetEntries<URefSetEntryLValue<SetTy
 
 interface URefSetReadOnlyRegion<SetType> :
     UReadOnlyMemoryRegion<URefSetEntryLValue<SetType>, UBoolSort> {
-    fun setEntries(ref: UHeapRef): URefSetEntries<SetType>
+    fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): URefSetEntries<SetType>
 }
 
 interface URefSetRegion<SetType> :
     URefSetReadOnlyRegion<SetType>,
     UMemoryRegion<URefSetEntryLValue<SetType>, UBoolSort> {
 
-    fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress): UAllocatedRefSetWithInputElements<SetType>
+    fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress, ownership: MutabilityOwnership): UAllocatedRefSetWithInputElements<SetType>
     fun inputSetWithInputElements(): UInputRefSetWithInputElements<SetType>
 
     fun union(
         srcRef: UHeapRef,
         dstRef: UHeapRef,
         operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): URefSetRegion<SetType>
 }
 
 internal class URefSetMemoryRegion<SetType>(
     private val setType: SetType,
     private val sort: UBoolSort,
-    private var allocatedSetWithAllocatedElements: PersistentMap<UAllocatedRefSetWithAllocatedElementId, UBoolExpr> = persistentHashMapOf(),
-    private var allocatedSetWithInputElements: PersistentMap<UAllocatedRefSetWithInputElementsId<SetType>, UAllocatedRefSetWithInputElements<SetType>> = persistentHashMapOf(),
-    private var inputSetWithAllocatedElements: PersistentMap<UInputRefSetWithAllocatedElementsId<SetType>, UInputRefSetWithAllocatedElements<SetType>> = persistentHashMapOf(),
+    private var allocatedSetWithAllocatedElements: UPersistentHashMap<UAllocatedRefSetWithAllocatedElementId, UBoolExpr> = persistentHashMapOf(),
+    private var allocatedSetWithInputElements: UPersistentHashMap<UAllocatedRefSetWithInputElementsId<SetType>, UAllocatedRefSetWithInputElements<SetType>> = persistentHashMapOf(),
+    private var inputSetWithAllocatedElements: UPersistentHashMap<UInputRefSetWithAllocatedElementsId<SetType>, UInputRefSetWithAllocatedElements<SetType>> = persistentHashMapOf(),
     private var inputSetWithInputElements: UInputRefSetWithInputElements<SetType>? = null
 ) : URefSetRegion<SetType> {
     private fun updateAllocatedSetWithAllocatedElements(
-        updated: PersistentMap<UAllocatedRefSetWithAllocatedElementId, UBoolExpr>
+        updated: UPersistentHashMap<UAllocatedRefSetWithAllocatedElementId, UBoolExpr>
     ) = URefSetMemoryRegion(
         setType, sort,
         updated,
@@ -101,26 +103,25 @@ internal class URefSetMemoryRegion<SetType>(
         UAllocatedRefSetWithInputElementsId(setAddress, setType, sort)
 
     private fun getAllocatedSetWithInputElements(
-        id: UAllocatedRefSetWithInputElementsId<SetType>
+        id: UAllocatedRefSetWithInputElementsId<SetType>,
+        ownership: MutabilityOwnership
     ): UAllocatedRefSetWithInputElements<SetType> {
-        var collection = allocatedSetWithInputElements[id]
-        if (collection == null) {
-            collection = id.emptyRegion()
-            allocatedSetWithInputElements = allocatedSetWithInputElements.put(id, collection)
-        }
+        val (updatedSet, collection) = allocatedSetWithInputElements.getOrPut(id, id.emptyRegion(), ownership)
+        allocatedSetWithInputElements = updatedSet
         return collection
     }
 
-    override fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress) =
-        getAllocatedSetWithInputElements(allocatedSetWithInputElementsId(setRef))
+    override fun allocatedSetWithInputElements(setRef: UConcreteHeapAddress, ownership: MutabilityOwnership) =
+        getAllocatedSetWithInputElements(allocatedSetWithInputElementsId(setRef), ownership)
 
     private fun updateAllocatedSetWithInputElements(
         id: UAllocatedRefSetWithInputElementsId<SetType>,
-        updatedSet: UAllocatedRefSetWithInputElements<SetType>
+        updatedSet: UAllocatedRefSetWithInputElements<SetType>,
+        ownership: MutabilityOwnership
     ) = URefSetMemoryRegion(
         setType, sort,
         allocatedSetWithAllocatedElements,
-        allocatedSetWithInputElements.put(id, updatedSet),
+        allocatedSetWithInputElements.put(id, updatedSet, ownership),
         inputSetWithAllocatedElements,
         inputSetWithInputElements
     )
@@ -129,24 +130,26 @@ internal class URefSetMemoryRegion<SetType>(
         UInputRefSetWithAllocatedElementsId(elementAddress, setType, sort)
 
     private fun getInputSetWithAllocatedElements(
-        id: UInputRefSetWithAllocatedElementsId<SetType>
+        id: UInputRefSetWithAllocatedElementsId<SetType>,
+        ownership: MutabilityOwnership
     ): UInputRefSetWithAllocatedElements<SetType> {
         var collection = inputSetWithAllocatedElements[id]
         if (collection == null) {
             collection = id.emptyRegion()
-            inputSetWithAllocatedElements = inputSetWithAllocatedElements.put(id, collection)
+            inputSetWithAllocatedElements = inputSetWithAllocatedElements.put(id, collection, ownership)
         }
         return collection
     }
 
     private fun updateInputSetWithAllocatedElements(
         id: UInputRefSetWithAllocatedElementsId<SetType>,
-        updatedSet: UInputRefSetWithAllocatedElements<SetType>
+        updatedSet: UInputRefSetWithAllocatedElements<SetType>,
+        ownership: MutabilityOwnership
     ) = URefSetMemoryRegion(
         setType, sort,
         allocatedSetWithAllocatedElements,
         allocatedSetWithInputElements,
-        inputSetWithAllocatedElements.put(id, updatedSet),
+        inputSetWithAllocatedElements.put(id, updatedSet, ownership),
         inputSetWithInputElements
     )
 
@@ -165,7 +168,7 @@ internal class URefSetMemoryRegion<SetType>(
             updatedSet
         )
 
-    override fun read(key: URefSetEntryLValue<SetType>): UBoolExpr =
+    override fun read(key: URefSetEntryLValue<SetType>, ownership: MutabilityOwnership): UBoolExpr =
         key.setRef.mapWithStaticAsSymbolic(
             { concreteRef ->
                 key.setElement.mapWithStaticAsSymbolic(
@@ -175,7 +178,7 @@ internal class URefSetMemoryRegion<SetType>(
                     },
                     { symbolicElem ->
                         val id = allocatedSetWithInputElementsId(concreteRef.address)
-                        getAllocatedSetWithInputElements(id).read(symbolicElem)
+                        getAllocatedSetWithInputElements(id, ownership).read(symbolicElem, ownership)
                     }
                 )
             },
@@ -183,10 +186,10 @@ internal class URefSetMemoryRegion<SetType>(
                 key.setElement.mapWithStaticAsSymbolic(
                     { concreteElem ->
                         val id = inputSetWithAllocatedElementsId(concreteElem.address)
-                        getInputSetWithAllocatedElements(id).read(symbolicRef)
+                        getInputSetWithAllocatedElements(id, ownership).read(symbolicRef, ownership)
                     },
                     { symbolicElem ->
-                        inputSetWithInputElements().read(symbolicRef to symbolicElem)
+                        inputSetWithInputElements().read(symbolicRef to symbolicElem, ownership)
                     }
                 )
             }
@@ -195,7 +198,8 @@ internal class URefSetMemoryRegion<SetType>(
     override fun write(
         key: URefSetEntryLValue<SetType>,
         value: UBoolExpr,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRefWithStaticAsSymbolic(
         ref = key.setRef,
         initial = this,
@@ -207,16 +211,16 @@ internal class URefSetMemoryRegion<SetType>(
                 initialGuard = setGuard,
                 blockOnConcrete = { region, (concreteElemRef, guard) ->
                     val id = UAllocatedRefSetWithAllocatedElementId(concreteSetRef.address, concreteElemRef.address)
-                    val newMap = region.allocatedSetWithAllocatedElements.guardedWrite(id, value, guard) {
+                    val newMap = region.allocatedSetWithAllocatedElements.guardedWrite(id, value, guard, ownership) {
                         sort.uctx.falseExpr
                     }
                     region.updateAllocatedSetWithAllocatedElements(newMap)
                 },
                 blockOnSymbolic = { region, (symbolicElemRef, guard) ->
                     val id = allocatedSetWithInputElementsId(concreteSetRef.address)
-                    val newMap = region.getAllocatedSetWithInputElements(id)
-                        .write(symbolicElemRef, value, guard)
-                    region.updateAllocatedSetWithInputElements(id, newMap)
+                    val newMap = region.getAllocatedSetWithInputElements(id, ownership)
+                        .write(symbolicElemRef, value, guard, ownership)
+                    region.updateAllocatedSetWithInputElements(id, newMap, ownership)
                 }
             )
         },
@@ -227,13 +231,13 @@ internal class URefSetMemoryRegion<SetType>(
                 initialGuard = setGuard,
                 blockOnConcrete = { region, (concreteElemRef, guard) ->
                     val id = inputSetWithAllocatedElementsId(concreteElemRef.address)
-                    val newMap = region.getInputSetWithAllocatedElements(id)
-                        .write(symbolicSetRef, value, guard)
-                    region.updateInputSetWithAllocatedElements(id, newMap)
+                    val newMap = region.getInputSetWithAllocatedElements(id, ownership)
+                        .write(symbolicSetRef, value, guard, ownership)
+                    region.updateInputSetWithAllocatedElements(id, newMap, ownership)
                 },
                 blockOnSymbolic = { region, (symbolicElemRef, guard) ->
                     val newMap = region.inputSetWithInputElements()
-                        .write(symbolicSetRef to symbolicElemRef, value, guard)
+                        .write(symbolicSetRef to symbolicElemRef, value, guard, ownership)
                     region.updateInputSetWithInputElements(newMap)
                 }
             )
@@ -243,7 +247,8 @@ internal class URefSetMemoryRegion<SetType>(
     override fun union(
         srcRef: UHeapRef,
         dstRef: UHeapRef,
-        operationGuard: UBoolExpr
+        operationGuard: UBoolExpr,
+        ownership: MutabilityOwnership
     ) = foldHeapRef2(
         ref0 = srcRef,
         ref1 = dstRef,
@@ -258,20 +263,20 @@ internal class URefSetMemoryRegion<SetType>(
                 read = { initialAllocatedSetState[it] ?: sort.uctx.falseExpr },
                 mkDstKeyId = { UAllocatedRefSetWithAllocatedElementId(dstConcrete.address, it) },
                 write = { result, dstKeyId, value, g ->
-                    result.guardedWrite(dstKeyId, value, g) { sort.uctx.falseExpr }
+                    result.guardedWrite(dstKeyId, value, g, ownership) { sort.uctx.falseExpr }
                 }
             )
             val updatedRegion = region.updateAllocatedSetWithAllocatedElements(updatedAllocatedSet)
 
             val srcId = allocatedSetWithInputElementsId(srcConcrete.address)
-            val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId)
+            val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId, ownership)
 
             val dstId = allocatedSetWithInputElementsId(dstConcrete.address)
-            val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId)
+            val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId, ownership)
 
             val adapter = UAllocatedToAllocatedSymbolicRefSetUnionAdapter(srcCollection)
             val updated = dstCollection.copyRange(srcCollection, adapter, guard)
-            updatedRegion.updateAllocatedSetWithInputElements(dstId, updated)
+            updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, ownership)
         },
         blockOnConcrete0Symbolic1 = { region, srcConcrete, dstSymbolic, guard ->
             val initialAllocatedSetState = region.allocatedSetWithAllocatedElements
@@ -280,14 +285,14 @@ internal class URefSetMemoryRegion<SetType>(
                 read = { initialAllocatedSetState[it] ?: sort.uctx.falseExpr },
                 mkDstKeyId = { inputSetWithAllocatedElementsId(it) },
                 write = { result, dstKeyId, value, g ->
-                    val newMap = result.getInputSetWithAllocatedElements(dstKeyId)
-                        .write(dstSymbolic, value, g)
-                    result.updateInputSetWithAllocatedElements(dstKeyId, newMap)
+                    val newMap = result.getInputSetWithAllocatedElements(dstKeyId, ownership)
+                        .write(dstSymbolic, value, g, ownership)
+                    result.updateInputSetWithAllocatedElements(dstKeyId, newMap, ownership)
                 }
             )
 
             val srcId = allocatedSetWithInputElementsId(srcConcrete.address)
-            val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId)
+            val srcCollection = updatedRegion.getAllocatedSetWithInputElements(srcId, ownership)
 
             val dstCollection = updatedRegion.inputSetWithInputElements()
 
@@ -299,10 +304,10 @@ internal class URefSetMemoryRegion<SetType>(
             val updatedAllocatedSet = region.unionInputSetAllocatedElements(
                 initial = region.allocatedSetWithAllocatedElements,
                 guard = guard,
-                read = { region.getInputSetWithAllocatedElements(it).read(srcSymbolic) },
+                read = { region.getInputSetWithAllocatedElements(it, ownership).read(srcSymbolic, ownership) },
                 mkDstKeyId = { UAllocatedRefSetWithAllocatedElementId(dstConcrete.address, it) },
                 write = { result, dstKeyId, value, g ->
-                    result.guardedWrite(dstKeyId, value, g) { sort.uctx.falseExpr }
+                    result.guardedWrite(dstKeyId, value, g, ownership) { sort.uctx.falseExpr }
                 }
             )
             val updatedRegion = region.updateAllocatedSetWithAllocatedElements(updatedAllocatedSet)
@@ -310,21 +315,21 @@ internal class URefSetMemoryRegion<SetType>(
             val srcCollection = updatedRegion.inputSetWithInputElements()
 
             val dstId = allocatedSetWithInputElementsId(dstConcrete.address)
-            val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId)
+            val dstCollection = updatedRegion.getAllocatedSetWithInputElements(dstId, ownership)
 
             val adapter = UInputToAllocatedSymbolicRefSetUnionAdapter(srcSymbolic, srcCollection)
             val updated = dstCollection.copyRange(srcCollection, adapter, guard)
-            updatedRegion.updateAllocatedSetWithInputElements(dstId, updated)
+            updatedRegion.updateAllocatedSetWithInputElements(dstId, updated, ownership)
         },
         blockOnSymbolic0Symbolic1 = { region, srcSymbolic, dstSymbolic, guard ->
             val updatedRegion = region.unionInputSetAllocatedElements(
                 initial = region, guard = guard,
-                read = { region.getInputSetWithAllocatedElements(it).read(srcSymbolic) },
+                read = { region.getInputSetWithAllocatedElements(it, ownership).read(srcSymbolic, ownership) },
                 mkDstKeyId = { inputSetWithAllocatedElementsId(it) },
                 write = { result, dstKeyId, value, g ->
-                    val newMap = result.getInputSetWithAllocatedElements(dstKeyId)
-                        .write(dstSymbolic, value, g)
-                    result.updateInputSetWithAllocatedElements(dstKeyId, newMap)
+                    val newMap = result.getInputSetWithAllocatedElements(dstKeyId, ownership)
+                        .write(dstSymbolic, value, g, ownership)
+                    result.updateInputSetWithAllocatedElements(dstKeyId, newMap, ownership)
                 }
             )
             val srcCollection = updatedRegion.inputSetWithInputElements()
@@ -344,7 +349,7 @@ internal class URefSetMemoryRegion<SetType>(
         write: (R, DstKeyId, UBoolExpr, UBoolExpr) -> R
     ) = unionAllocatedElements(
         initial,
-        inputSetWithAllocatedElements.keys,
+        inputSetWithAllocatedElements.keys(),
         guard,
         read,
         { mkDstKeyId(it.elementAddress) },
@@ -360,7 +365,7 @@ internal class URefSetMemoryRegion<SetType>(
         write: (R, DstKeyId, UBoolExpr, UBoolExpr) -> R
     ) = unionAllocatedElements(
         initial,
-        allocatedSetWithAllocatedElements.keys.filter { it.setAddress == srcAddress },
+        allocatedSetWithAllocatedElements.keys().filter { it.setAddress == srcAddress },
         guard,
         read,
         { mkDstKeyId(it.elementAddress) },
@@ -382,13 +387,13 @@ internal class URefSetMemoryRegion<SetType>(
         write(result, mkDstKeyId(srcKeyId), guard.uctx.trueExpr, mergedGuard)
     }
 
-    override fun setEntries(ref: UHeapRef): URefSetEntries<SetType> =
+    override fun setEntries(ref: UHeapRef, ownership: MutabilityOwnership): URefSetEntries<SetType> =
         foldHeapRefWithStaticAsSymbolic(
             ref = ref,
             initial = URefSetEntries(),
             initialGuard = ref.uctx.trueExpr,
             blockOnConcrete = { entries, (concreteRef, _) ->
-                allocatedSetWithAllocatedElements.keys.forEach { entry ->
+                allocatedSetWithAllocatedElements.keys().forEach { entry ->
                     if (entry.setAddress == concreteRef.address) {
                         val elem = ref.uctx.mkConcreteHeapRef(entry.elementAddress)
                         entries.add(URefSetEntryLValue(concreteRef, elem, setType))
@@ -397,7 +402,7 @@ internal class URefSetMemoryRegion<SetType>(
 
                 val elementsId = allocatedSetWithInputElementsId(concreteRef.address)
                 val elements = USymbolicSetElementsCollector.collect(
-                    getAllocatedSetWithInputElements(elementsId).updates
+                    getAllocatedSetWithInputElements(elementsId, ownership).updates
                 )
                 elements.elements.forEach { elem ->
                     entries.add(URefSetEntryLValue(concreteRef, elem, setType))
@@ -410,7 +415,7 @@ internal class URefSetMemoryRegion<SetType>(
                 entries
             },
             blockOnSymbolic = { entries, (symbolicRef, _) ->
-                inputSetWithAllocatedElements.keys.forEach { entry ->
+                inputSetWithAllocatedElements.keys().forEach { entry ->
                     val elem = ref.uctx.mkConcreteHeapRef(entry.elementAddress)
                     entries.add(URefSetEntryLValue(symbolicRef, elem, setType))
                 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt
index ff77cf7e7b..91a5bb988b 100644
--- a/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/collection/set/ref/URefSetRegionApi.kt
@@ -2,6 +2,7 @@ package org.usvm.collection.set.ref
 
 import org.usvm.UBoolExpr
 import org.usvm.UHeapRef
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UReadOnlyMemory
 import org.usvm.memory.UWritableMemory
 import org.usvm.uctx
@@ -19,7 +20,7 @@ internal fun <SetType> UWritableMemory<*>.refSetUnion(
         "setUnion is not applicable to $region"
     }
 
-    val newRegion = region.union(srcRef, dstRef, guard)
+    val newRegion = region.union(srcRef, dstRef, guard, ownership)
     setRegion(regionId, newRegion)
 }
 
@@ -31,5 +32,5 @@ fun <SetType> UReadOnlyMemory<*>.refSetEntries(
     val region = getRegion(regionId) as? URefSetReadOnlyRegion<SetType>
         ?: return URefSetEntries<SetType>().apply { markAsInput() }
 
-    return region.setEntries(setRef)
+    return region.setEntries(setRef, ownership)
 }
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 877a8ee1eb..ae6add434f 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/EqualityConstraints.kt
@@ -33,7 +33,7 @@ import org.usvm.solver.UExprTranslator
  */
 class UEqualityConstraints private constructor(
     internal val ctx: UContext<*>,
-    private var ownership: MutabilityOwnership,
+    internal var ownership: MutabilityOwnership,
     private val equalReferences: DisjointSets<UHeapRef>,
     var distinctReferences: UPersistentHashSet<UHeapRef>,
     var referenceDisequalities: UPersistentMultiMap<UHeapRef, UHeapRef>,
@@ -47,10 +47,7 @@ class UEqualityConstraints private constructor(
         persistentHashMapOf(),
         persistentHashMapOf(),
     )
-    
-    fun changeOwnership(newOwnership: MutabilityOwnership) {
-        ownership = newOwnership
-    } 
+
     /**
      * Determines whether a static ref could be assigned to a symbolic, according to additional information.
      */
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 5fcd3286e4..87043c36d6 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/PathConstraints.kt
@@ -49,8 +49,8 @@ open class UPathConstraints<Type>(
 
     fun changeOwnership(newOwnership: MutabilityOwnership) {
        ownership = newOwnership
-       numericConstraints.changeOwnership(newOwnership)
-       equalityConstraints.changeOwnership(newOwnership)
+       numericConstraints.ownership = newOwnership
+       equalityConstraints.ownership = newOwnership
     }
 
     /**
diff --git a/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt b/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt
index c3c9fa84fb..2b26a36c30 100644
--- a/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/constraints/UNumericConstraints.kt
@@ -64,16 +64,12 @@ private typealias ConstraintTerms<Sort> = UExpr<Sort>
 class UNumericConstraints<Sort : UBvSort> private constructor(
     private val ctx: UContext<*>,
     val sort: Sort,
-    private var ownership: MutabilityOwnership,
+    internal var ownership: MutabilityOwnership,
     private var numericConstraints: UPersistentHashMap<ConstraintTerms<Sort>, Constraint<Sort>>,
     private var constraintWatchList: UPersistentMultiMap<ConstraintTerms<Sort>, ConstraintTerms<Sort>>,
 ) : UOwnedMergeable<UNumericConstraints<Sort>, MutableMergeGuard> {
     constructor(ctx: UContext<*>, sort: Sort, ownership: MutabilityOwnership) : this(ctx, sort, ownership, persistentHashMapOf(), persistentHashMapOf())
 
-    fun changeOwnership(newOwnership: MutabilityOwnership) {
-        ownership = newOwnership
-    }
-
     private val constraintPropagationQueue = arrayListOf<ConstraintUpdateEvent<Sort>>()
 
     /**
@@ -1965,8 +1961,8 @@ class UNumericConstraints<Sort : UBvSort> private constructor(
 
         fun size(): Int =
             inferredTermLowerBounds.size +
-                    termUpperBounds.size +
-                    termDisequalities.size
+                termUpperBounds.size +
+                termDisequalities.size
 
         fun lowerBound(bias: KBitVecValue<Sort>): ValueConstraint<Sort>? =
             concreteLowerBounds[bias]
@@ -2174,11 +2170,15 @@ class UNumericConstraints<Sort : UBvSort> private constructor(
     class TermConstraintSet<Sort : UBvSort>(
         val termConstraints: UPersistentMultiMap<TermsConstraint<Sort>, KBitVecValue<Sort>>,
         val termDependency: UPersistentMultiMap<ConstraintTerms<Sort>, TermsConstraint<Sort>>,
-        val size : Int
+        val size: Int
     ) {
         constructor() : this(persistentHashMapOf(), persistentHashMapOf(), 0)
 
-        fun addTermConstraint(bias: KBitVecValue<Sort>, constraint: TermsConstraint<Sort>, ownership: MutabilityOwnership): TermConstraintSet<Sort> {
+        fun addTermConstraint(
+            bias: KBitVecValue<Sort>,
+            constraint: TermsConstraint<Sort>,
+            ownership: MutabilityOwnership
+        ): TermConstraintSet<Sort> {
             var newSize = size
             val constraints = termConstraints[constraint].also { if (it  == null) newSize++ } ?: persistentHashSetOf()
             val updatedConstraints =  constraints.add(bias, ownership)
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 3b704321fa..d0d2dba8f1 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt
@@ -1,7 +1,5 @@
 package org.usvm.memory
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.INITIAL_CONCRETE_ADDRESS
 import org.usvm.INITIAL_STATIC_ADDRESS
 import org.usvm.UBoolExpr
@@ -14,10 +12,13 @@ import org.usvm.UIndexedMocker
 import org.usvm.UMockEvaluator
 import org.usvm.UMocker
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.constraints.UTypeConstraints
 import org.usvm.constraints.UTypeEvaluator
 import org.usvm.merging.MergeGuard
-import org.usvm.merging.UMergeable
+import org.usvm.merging.UOwnedMergeable
 
 interface UMemoryRegionId<Key, Sort : USort> {
     val sort: Sort
@@ -26,11 +27,11 @@ interface UMemoryRegionId<Key, Sort : USort> {
 }
 
 interface UReadOnlyMemoryRegion<Key, Sort : USort> {
-    fun read(key: Key): UExpr<Sort>
+    fun read(key: Key, ownership: MutabilityOwnership): UExpr<Sort>
 }
 
 interface UMemoryRegion<Key, Sort : USort> : UReadOnlyMemoryRegion<Key, Sort> {
-    fun write(key: Key, value: UExpr<Sort>, guard: UBoolExpr): UMemoryRegion<Key, Sort>
+    fun write(key: Key, value: UExpr<Sort>, guard: UBoolExpr, ownership: MutabilityOwnership): UMemoryRegion<Key, Sort>
 }
 
 interface ULValue<Key, Sort : USort> {
@@ -62,13 +63,14 @@ class UAddressCounter {
 }
 
 interface UReadOnlyMemory<Type> {
+    val ownership : MutabilityOwnership
     val stack: UReadOnlyRegistersStack
     val mocker: UMockEvaluator
     val types: UTypeEvaluator<Type>
 
     private fun <Key, Sort : USort> read(regionId: UMemoryRegionId<Key, Sort>, key: Key): UExpr<Sort> {
         val region = getRegion(regionId)
-        return region.read(key)
+        return region.read(key, ownership)
     }
 
     fun <Key, Sort : USort> read(lvalue: ULValue<Key, Sort>) = read(lvalue.memoryRegionId, lvalue.key)
@@ -92,13 +94,17 @@ interface UWritableMemory<Type> : UReadOnlyMemory<Type> {
 @Suppress("MemberVisibilityCanBePrivate")
 class UMemory<Type, Method>(
     internal val ctx: UContext<*>,
+    override var ownership: MutabilityOwnership,
     override val types: UTypeConstraints<Type>,
     override val stack: URegistersStack = URegistersStack(),
-    private val mocks: UIndexedMocker<Method> = UIndexedMocker(),
-    persistentRegions: PersistentMap<UMemoryRegionId<*, *>, UMemoryRegion<*, *>> = persistentHashMapOf(),
-) : UWritableMemory<Type>, UMergeable<UMemory<Type, Method>, MergeGuard> {
-    private val regions = persistentRegions.builder()
+    private val mocks: UIndexedMocker<Method> = UIndexedMocker(ownership = ownership),
+    private var regions: UPersistentHashMap<UMemoryRegionId<*, *>, UMemoryRegion<*, *>> = persistentHashMapOf(),
+) : UWritableMemory<Type>, UOwnedMergeable<UMemory<Type, Method>, MergeGuard> {
 
+    fun changeOwnership(newOwnership: MutabilityOwnership) {
+        ownership = newOwnership
+        mocks.ownership = newOwnership
+    }
     override val mocker: UMocker<Method>
         get() = mocks
 
@@ -106,9 +112,9 @@ class UMemory<Type, Method>(
     override fun <Key, Sort : USort> getRegion(regionId: UMemoryRegionId<Key, Sort>): UMemoryRegion<Key, Sort> {
         if (regionId is URegisterStackId) return stack as UMemoryRegion<Key, Sort>
 
-        return regions.getOrPut(regionId) {
-            regionId.emptyRegion()
-        } as UMemoryRegion<Key, Sort>
+        val (updatedRegions, region) = regions.getOrPut(regionId, regionId.emptyRegion(), ownership)
+        regions = updatedRegions
+        return region as UMemoryRegion<Key, Sort>
     }
 
     override fun <Key, Sort : USort> setRegion(
@@ -119,7 +125,7 @@ class UMemory<Type, Method>(
             check(newRegion === stack) { "Stack is mutable" }
             return
         }
-        regions[regionId] = newRegion
+        regions = regions.put(regionId, newRegion, ownership)
     }
 
     override fun <Key, Sort : USort> write(lvalue: ULValue<Key, Sort>, rvalue: UExpr<Sort>, guard: UBoolExpr) =
@@ -132,7 +138,7 @@ class UMemory<Type, Method>(
         guard: UBoolExpr
     ) {
         val region = getRegion(regionId)
-        val newRegion = region.write(key, value, guard)
+        val newRegion = region.write(key, value, guard, ownership)
         setRegion(regionId, newRegion)
     }
 
@@ -152,13 +158,13 @@ class UMemory<Type, Method>(
 
     override fun nullRef(): UHeapRef = ctx.nullRef
 
-    fun clone(typeConstraints: UTypeConstraints<Type>): UMemory<Type, Method> =
-        UMemory(ctx, typeConstraints, stack.clone(), mocks.clone(), regions.build())
+    fun clone(typeConstraints: UTypeConstraints<Type>, ownership: MutabilityOwnership): UMemory<Type, Method> =
+        UMemory(ctx, ownership, typeConstraints, stack.clone(), mocks.clone(ownership), regions)
 
     override fun toWritableMemory() =
     // To be perfectly rigorous, we should clone stack and types here.
         // But in fact they should not be used, so to optimize things up, we don't touch them.
-        UMemory(ctx, types, stack, mocks, regions.build())
+        UMemory(ctx, ownership, types, stack, mocks, regions)
 
 
     /**
@@ -172,9 +178,9 @@ class UMemory<Type, Method>(
      *
      * @return the merged memory.
      */
-    override fun mergeWith(other: UMemory<Type, Method>, by: MergeGuard): UMemory<Type, Method>? {
-        val ids = regions.keys
-        val otherIds = other.regions.keys
+    override fun mergeWith(other: UMemory<Type, Method>, by: MergeGuard, ownership: MutabilityOwnership): UMemory<Type, Method>? {
+        val ids = regions.keys()
+        val otherIds = other.regions.keys()
         if (ids != otherIds) {
             return null
         }
@@ -189,10 +195,10 @@ class UMemory<Type, Method>(
             }
         }
 
-        val mergedRegions = regions.build()
+        val mergedRegions = regions
         val mergedStack = stack.mergeWith(other.stack, by) ?: return null
-        val mergedMocks = mocks.mergeWith(other.mocks, by) ?: return null
+        val mergedMocks = mocks.mergeWith(other.mocks, by, ownership) ?: return null
 
-        return UMemory(ctx, types, mergedStack, mergedMocks, mergedRegions)
+        return UMemory(ctx, ownership, types, mergedStack, mergedMocks, mergedRegions)
     }
 }
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 f5375d2149..e4f484a7a7 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/RegistersStack.kt
@@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr
 import org.usvm.UBoolExpr
 import org.usvm.UExpr
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.isTrue
 import org.usvm.merging.MergeGuard
 import org.usvm.merging.UMergeable
@@ -30,7 +31,8 @@ class URegisterStackLValue<Sort : USort>(
 interface UReadOnlyRegistersStack : UReadOnlyMemoryRegion<URegisterStackLValue<*>, USort> {
     fun <Sort : USort> readRegister(index: Int, sort: Sort): KExpr<Sort>
 
-    override fun read(key: URegisterStackLValue<*>): UExpr<USort> = readRegister(key.idx, key.sort)
+    override fun read(key: URegisterStackLValue<*>, ownership: MutabilityOwnership): UExpr<USort> =
+        readRegister(key.idx, key.sort)
 }
 
 class URegistersStack(
@@ -54,6 +56,7 @@ class URegistersStack(
         key: URegisterStackLValue<*>,
         value: UExpr<USort>,
         guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): UMemoryRegion<URegisterStackLValue<*>, USort> {
         check(guard.isTrue) { "Guarded writes are not supported for register" }
         writeRegister(key.idx, value)
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 921e1d1f88..2f21046594 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollection.kt
@@ -7,6 +7,8 @@ import org.usvm.UComposer
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.isFalse
 import org.usvm.isTrue
 import org.usvm.uctx
@@ -116,7 +118,8 @@ data class USymbolicCollection<out CollectionId : USymbolicCollectionId<Key, Sor
     override fun write(
         key: Key,
         value: UExpr<Sort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership,
     ): USymbolicCollection<CollectionId, Key, Sort> {
         assert(value.sort == sort)
 
@@ -213,7 +216,7 @@ data class USymbolicCollection<out CollectionId : USymbolicCollectionId<Key, Sor
         return this.copy(updates = updatesCopy)
     }
 
-    override fun read(key: Key): UExpr<Sort> = read(key, composer = null)
+    override fun read(key: Key, ownership: MutabilityOwnership): UExpr<Sort> = read(key, composer = null)
 
     override fun toString(): String =
         buildString {
@@ -245,16 +248,17 @@ class GuardBuilder(nonMatchingUpdates: UBoolExpr) {
         get() = nonMatchingUpdatesGuard.isFalse
 }
 
-inline fun <K, VSort : USort> PersistentMap<K, UExpr<VSort>>.guardedWrite(
+inline fun <K, VSort : USort> UPersistentHashMap<K, UExpr<VSort>>.guardedWrite(
     key: K,
     value: UExpr<VSort>,
     guard: UBoolExpr,
+    ownership: MutabilityOwnership,
     defaultValue: () -> UExpr<VSort>
-): PersistentMap<K, UExpr<VSort>> {
+): UPersistentHashMap<K, UExpr<VSort>> {
     val guardedValue = guard.uctx.mkIte(
         guard,
         { value },
         { get(key) ?: defaultValue() }
     )
-    return put(key, guardedValue)
+    return put(key, guardedValue, ownership)
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
index 9309b8ef0e..819f615a89 100644
--- a/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/memory/UpdateNodes.kt
@@ -226,7 +226,7 @@ class URangedUpdateNode<CollectionId : USymbolicCollectionId<SrcKey, Sort, Colle
         memory: UWritableMemory<*>,
         dstCollectionId: USymbolicCollectionId<DstKey, *, *>,
         key: DstKey,
-        composer: UComposer<*, *>,
+        composer: UComposer<*, *>
     ) {
         val convertedKey = adapter.convert(key, composer)
         sourceCollection.applyTo(memory, convertedKey, composer)
@@ -236,7 +236,7 @@ class URangedUpdateNode<CollectionId : USymbolicCollectionId<SrcKey, Sort, Colle
             dstCollectionId,
             composer.compose(guard),
             convertedKey,
-            composer
+            composer,
         )
     }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/merging/Merging.kt b/usvm-core/src/main/kotlin/org/usvm/merging/Merging.kt
index 2afde23ca4..c1f7139f7c 100644
--- a/usvm-core/src/main/kotlin/org/usvm/merging/Merging.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/merging/Merging.kt
@@ -14,5 +14,4 @@ interface UOwnedMergeable<Entity, By> {
      * @return Merged entity with new ownership or `null` if `this` and [other] are non-mergeable.
      */
     fun mergeWith(other: Entity, by: By, ownership: MutabilityOwnership): Entity?
-    
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt
index 6e4d41b251..3061af3558 100644
--- a/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/merging/MergingPathSelector.kt
@@ -37,7 +37,7 @@ class MergingPathSelector<State : UState<*, *, *, *, *, State>>(
         val resultState = when (val selectorState = selectorState) {
             is SelectorState.Advancing -> {
                 val closeState = closeStatesSearcher.findCloseStates(state).firstOrNull() ?: return state
-                val mergedState = state.mergeWith(closeState, Unit, MutabilityOwnership())
+                val mergedState = state.mergeWith(closeState, Unit)
                 if (mergedState == null) {
                     selectorState.steps++
                     if (selectorState.steps == advanceLimit) {
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 9743188f61..ec6fc9f924 100644
--- a/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/LazyModelDecoder.kt
@@ -14,6 +14,7 @@ import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.UMockEvaluator
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UMemoryRegionId
 import org.usvm.memory.UReadOnlyMemoryRegion
 import org.usvm.solver.UExprTranslator
@@ -141,6 +142,6 @@ open class ULazyModelDecoder<Type>(
         private val regionId: UMemoryRegionId<Key, Sort>,
         private val value: UExpr<Sort>
     ) : UReadOnlyMemoryRegion<Key, Sort> {
-        override fun read(key: Key): UExpr<Sort> = value
+        override fun read(key: Key, ownership: MutabilityOwnership): UExpr<Sort> = value
     }
 }
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 59feb5405f..39a0c42a44 100644
--- a/usvm-core/src/main/kotlin/org/usvm/model/Model.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/Model.kt
@@ -10,6 +10,7 @@ import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.UMockEvaluator
 import org.usvm.USort
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.ULValue
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -37,6 +38,7 @@ open class UModelBase<Type>(
     override val mocker: UMockEvaluator,
     val regions: Map<UMemoryRegionId<*, *>, UReadOnlyMemoryRegion<*, *>>,
     val nullRef: UConcreteHeapRef,
+    override val ownership: MutabilityOwnership = ctx.defaultOwnership,
 ) : UModel, UWritableMemory<Type> {
     @Suppress("LeakingThis")
     protected open val composer = ctx.composer(this)
diff --git a/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt b/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt
index 5604612f43..a7061cc4bb 100644
--- a/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/ModelRegions.kt
@@ -1,10 +1,11 @@
 package org.usvm.model
 
 import io.ksmt.expr.KExpr
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import org.usvm.UExpr
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UReadOnlyMemoryRegion
 
@@ -13,7 +14,7 @@ import org.usvm.memory.UReadOnlyMemoryRegion
  * A specific [UMemoryRegion] for one-dimensional regions generalized by a single expression of a [KeySort].
  */
 class UMemory1DArray<KeySort : USort, Sort : USort> internal constructor(
-    private val values: PersistentMap<UExpr<KeySort>, UExpr<Sort>>,
+    private val values: UPersistentHashMap<UExpr<KeySort>, UExpr<Sort>>,
     private val constValue: UExpr<Sort>,
 ) : UReadOnlyMemoryRegion<KExpr<KeySort>, Sort> {
 
@@ -25,7 +26,7 @@ class UMemory1DArray<KeySort : USort, Sort : USort> internal constructor(
         mappedConstValue: UExpr<Sort>,
     ) : this(persistentHashMapOf(), mappedConstValue)
 
-    override fun read(key: KExpr<KeySort>): UExpr<Sort> = values.getOrDefault(key, constValue)
+    override fun read(key: KExpr<KeySort>, ownership: MutabilityOwnership): UExpr<Sort> = values.getOrDefault(key, constValue)
 }
 
 /**
@@ -33,7 +34,7 @@ class UMemory1DArray<KeySort : USort, Sort : USort> internal constructor(
  * of two expressions with [Key1Sort] and [Key2Sort] sorts.
  */
 class UMemory2DArray<Key1Sort : USort, Key2Sort : USort, Sort : USort> internal constructor(
-    val values: PersistentMap<Pair<UExpr<Key1Sort>, UExpr<Key2Sort>>, UExpr<Sort>>,
+    val values: UPersistentHashMap<Pair<UExpr<Key1Sort>, UExpr<Key2Sort>>, UExpr<Sort>>,
     val constValue: UExpr<Sort>,
 ) : UReadOnlyMemoryRegion<Pair<KExpr<Key1Sort>, KExpr<Key2Sort>>, Sort> {
     /**
@@ -44,7 +45,7 @@ class UMemory2DArray<Key1Sort : USort, Key2Sort : USort, Sort : USort> internal
         mappedConstValue: UExpr<Sort>,
     ) : this(persistentHashMapOf(), mappedConstValue)
 
-    override fun read(key: Pair<KExpr<Key1Sort>, KExpr<Key2Sort>>): UExpr<Sort> {
+    override fun read(key: Pair<KExpr<Key1Sort>, KExpr<Key2Sort>>, ownership: MutabilityOwnership): UExpr<Sort> {
         return values.getOrDefault(key, constValue)
     }
 }
diff --git a/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt b/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt
index be68857e07..0bb7e7e2c0 100644
--- a/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/model/UModelEvaluator.kt
@@ -27,7 +27,7 @@ import io.ksmt.sort.KSort
 import io.ksmt.sort.KSortVisitor
 import io.ksmt.sort.KUninterpretedSort
 import io.ksmt.utils.uncheckedCast
-import kotlinx.collections.immutable.persistentHashMapOf
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.NULL_ADDRESS
 import org.usvm.UContext
 import org.usvm.UExpr
@@ -114,20 +114,20 @@ open class UModelEvaluator<SizeSort : USort>(
     ): UMemory1DArray<Idx, Value> {
         val interpretation = model.interpretation(translated)
 
-        val stores = persistentHashMapOf<UExpr<Idx>, UExpr<Value>>().builder()
+        var stores = persistentHashMapOf<UExpr<Idx>, UExpr<Value>>()
         val defaultValue = interpretation?.let {
             traverse1DArrayEntries(interpretation) { idx, value ->
-                stores[idx.mapAddress(addressesMapping)] = value.mapAddress(addressesMapping)
+                stores = stores.put(idx.mapAddress(addressesMapping), value.mapAddress(addressesMapping), ctx.defaultOwnership)
             }
         }
 
         if (defaultValue != null) {
-            return UMemory1DArray(stores.build(), defaultValue.mapAddress(addressesMapping))
+            return UMemory1DArray(stores, defaultValue.mapAddress(addressesMapping))
         }
 
         return completed1DArrays.getOrPut(translated) {
             val completedDefault = translated.sort.range.accept(this)
-            UMemory1DArray(stores.build(), completedDefault.uncheckedCast())
+            UMemory1DArray(stores, completedDefault.uncheckedCast())
         }.uncheckedCast()
     }
 
@@ -136,26 +136,26 @@ open class UModelEvaluator<SizeSort : USort>(
      * Complete model according to the array range (value) sort if array is free in the model.
      * */
     open fun <Idx1 : USort, Idx2 : USort, Value : USort> evalAndCompleteArray2DMemoryRegion(
-        translated: KDecl<KArray2Sort<Idx1, Idx2, Value>>,
+        translated: KDecl<KArray2Sort<Idx1, Idx2, Value>>
     ): UMemory2DArray<Idx1, Idx2, Value> {
         val interpretation = model.interpretation(translated)
 
-        val stores = persistentHashMapOf<Pair<UExpr<Idx1>, UExpr<Idx2>>, UExpr<Value>>().builder()
+        var stores = persistentHashMapOf<Pair<UExpr<Idx1>, UExpr<Idx2>>, UExpr<Value>>()
         val defaultValue = interpretation?.let {
             traverse2DArrayEntries(interpretation) { idx1, idx2, value ->
                 val mappedIdx1 = idx1.mapAddress(addressesMapping)
                 val mappedIdx2 = idx2.mapAddress(addressesMapping)
-                stores[mappedIdx1 to mappedIdx2] = value.mapAddress(addressesMapping)
+                stores = stores.put(mappedIdx1 to mappedIdx2, value.mapAddress(addressesMapping), ctx.defaultOwnership)
             }
         }
 
         if (defaultValue != null) {
-            return UMemory2DArray(stores.build(), defaultValue.mapAddress(addressesMapping))
+            return UMemory2DArray(stores, defaultValue.mapAddress(addressesMapping))
         }
 
         return completed2DArrays.getOrPut(translated) {
             val completedDefault = translated.sort.range.accept(this)
-            UMemory2DArray(stores.build(), completedDefault.uncheckedCast())
+            UMemory2DArray(stores, completedDefault.uncheckedCast())
         }.uncheckedCast()
     }
 
diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt
index da88a0d0da..8c270cc04f 100644
--- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt
@@ -136,7 +136,7 @@ private fun <Method, Statement, Target, State> createPathSelector(
 
             wrappedSelectors.first().add(initialStates.toList())
             wrappedSelectors.drop(1).forEach {
-                it.add(initialStates.map { it.clone(MutabilityOwnership()) }.toList())
+                it.add(initialStates.map { it.clone() }.toList())
             }
 
             ParallelPathSelector(wrappedSelectors)
diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt b/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt
index a50473d866..e9487e3888 100644
--- a/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt
@@ -57,7 +57,7 @@ abstract class U1DUpdatesTranslator<KeySort : USort, Sort : USort>(
 
     override fun visitUpdate(
         previous: KExpr<KArraySort<KeySort, Sort>>,
-        update: UUpdateNode<UExpr<KeySort>, Sort>,
+        update: UUpdateNode<UExpr<KeySort>, Sort>
     ): KExpr<KArraySort<KeySort, Sort>> = with(previous.uctx) {
         when (update) {
             is UPinpointUpdateNode -> {
diff --git a/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt b/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt
index b8a6c973d9..ec66ed1aaf 100644
--- a/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt
+++ b/usvm-core/src/main/kotlin/org/usvm/utils/StateUtils.kt
@@ -27,7 +27,7 @@ internal fun <Type> UState<Type, *, *, *, *, *>.isSat(): Boolean {
 
 @Suppress("MoveVariableDeclarationIntoWhen")
 internal fun <Type, State : UState<Type, *, *, *, *, State>> State.checkSat(condition: UBoolExpr): State? {
-    val conditionalState = clone(MutabilityOwnership())
+    val conditionalState = clone()
     conditionalState.pathConstraints += condition
 
     // If this state did not fork at all or was sat at the last fork point, it must be still sat, so we can just
diff --git a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt
index 62e12db253..3b077f9e39 100644
--- a/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/CompositionTest.kt
@@ -27,6 +27,7 @@ import org.usvm.collection.array.USymbolicArrayInputToInputCopyAdapter
 import org.usvm.collection.array.length.UInputArrayLengthId
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.collection.field.UInputFieldId
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.constraints.UTypeEvaluator
 import org.usvm.memory.UFlatUpdates
 import org.usvm.memory.UMemory
@@ -54,6 +55,7 @@ internal class CompositionTest {
     private lateinit var memory: UReadOnlyMemory<Type>
 
     private lateinit var ctx: UContext<USizeSort>
+    private lateinit var ownership: MutabilityOwnership
     private lateinit var concreteNull: UConcreteHeapRef
     private lateinit var composer: UComposer<Type, USizeSort>
 
@@ -63,6 +65,7 @@ internal class CompositionTest {
         every { components.mkTypeSystem(any()) } returns mockk()
 
         ctx = UContext(components)
+        ownership = MutabilityOwnership()
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
         every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory<Type> -> UComposer(ctx, memory) } }
 
@@ -255,7 +258,7 @@ internal class CompositionTest {
         val fstValueFromHeap = 42.toBv()
         val sndValueFromHeap = 43.toBv()
 
-        val heapToComposeWith = UMemory<KClass<Array<*>>, Any>(ctx, mockk())
+        val heapToComposeWith = UMemory<KClass<Array<*>>, Any>(ctx, MutabilityOwnership(), mockk())
 
         heapToComposeWith.writeArrayLength(fstConcreteAddress, fstValueFromHeap, arrayType, sizeSort)
         heapToComposeWith.writeArrayLength(sndConcreteAddress, sndValueFromHeap, arrayType, sizeSort)
@@ -310,7 +313,7 @@ internal class CompositionTest {
 
         val answer = 43.toBv()
 
-        val composer = UComposer(ctx, UMemory<KClass<*>, Any>(ctx, mockk())) // TODO replace with jacoDB type
+        val composer = UComposer(ctx, UMemory<KClass<*>, Any>(ctx, MutabilityOwnership(), mockk())) // TODO replace with jacoDB type
 
         every { fstAddress.accept(composer) } returns sndAddress
         every { fstIndex.accept(composer) } returns sndIndex
@@ -340,13 +343,13 @@ internal class CompositionTest {
         // create a reading from the region
         val fstArrayIndexReading = mkInputArrayReading(region, fstAddress, fstIndex)
 
-        val sndMemory = UMemory<KClass<*>, Any>(ctx, mockk(), mockk())
+        val sndMemory = UMemory<KClass<*>, Any>(ctx, MutabilityOwnership(), mockk(), mockk())
         // create a heap with a record: (sndAddress, sndIndex) = 2
         sndMemory.writeArrayIndex(sndAddress, sndIndex, arrayType, mkBv32Sort(), 2.toBv(), mkTrue())
 
         val sndComposer = UComposer(ctx, sndMemory)
 
-        val fstMemory = UMemory<KClass<*>, Any>(ctx, mockk(), mockk())
+        val fstMemory = UMemory<KClass<*>, Any>(ctx, ownership, mockk(), mockk())
         // create a heap with a record: (fstAddress, fstIndex) = 1
         fstMemory.writeArrayIndex(fstAddress, fstIndex, arrayType, mkBv32Sort(), 1.toBv(), mkTrue())
 
@@ -416,7 +419,7 @@ internal class CompositionTest {
         val fstValue = 42.toBv()
         val sndValue = 43.toBv()
 
-        val heapToComposeWith = UMemory<KClass<Array<*>>, Any>(ctx, mockk())
+        val heapToComposeWith = UMemory<KClass<Array<*>>, Any>(ctx, MutabilityOwnership(), mockk())
 
         heapToComposeWith.writeArrayIndex(
             fstAddressForCompose, concreteIndex, arrayType, regionArray.sort, fstValue, guard = trueExpr
@@ -448,8 +451,8 @@ internal class CompositionTest {
 
         val regionArray = UAllocatedArrayId<_, _, USizeSort>(arrayType, addressSort, 0)
             .emptyRegion()
-            .write(mkBv(0), symbolicAddress, trueExpr)
-            .write(mkBv(1), mkConcreteHeapRef(1), trueExpr)
+            .write(mkBv(0), symbolicAddress, trueExpr, ownership)
+            .write(mkBv(1), mkConcreteHeapRef(1), trueExpr, ownership)
 
         val reading = mkAllocatedArrayReading(regionArray, symbolicIndex)
 
@@ -487,7 +490,7 @@ internal class CompositionTest {
         val region = USymbolicCollection(
             UInputFieldId(field, bv32Sort),
             updates,
-        ).write(aAddress, 43.toBv(), guard = trueExpr)
+        ).write(aAddress, 43.toBv(), guard = trueExpr, ownership)
 
         every { aAddress.accept(any()) } returns aAddress
         every { bAddress.accept(any()) } returns aAddress
@@ -505,7 +508,7 @@ internal class CompositionTest {
 
         val answer = 43.toBv()
 
-        val composeMemory = UMemory<Type, Any>(ctx, mockk())
+        val composeMemory = UMemory<Type, Any>(ctx, MutabilityOwnership(),  mockk())
         composeMemory.writeField(aAddress, field, bv32Sort, 42.toBv(), guard = trueExpr)
 
         val composer = UComposer(ctx, composeMemory)
@@ -556,7 +559,7 @@ internal class CompositionTest {
         val symbolicRef2 = mkRegisterReading(2, addressSort) as UHeapRef
         val composedSymbolicHeapRef = mkConcreteHeapRef(1)
 
-        val composeMemory = UMemory<Type, Any>(ctx, mockk())
+        val composeMemory = UMemory<Type, Any>(ctx, MutabilityOwnership(), mockk())
 
         composeMemory.writeArrayIndex(composedSymbolicHeapRef, mkBv(3), arrayType, bv32Sort, mkBv(1337), trueExpr)
 
@@ -570,7 +573,7 @@ internal class CompositionTest {
 
         val fromRegion0 = UInputArrayId<_, _, USizeSort>(arrayType, bv32Sort)
             .emptyRegion()
-            .write(symbolicRef0 to mkBv(0), mkBv(42), trueExpr)
+            .write(symbolicRef0 to mkBv(0), mkBv(42), trueExpr, ownership)
 
         val adapter1 = USymbolicArrayInputToInputCopyAdapter(
             symbolicRef0 to mkSizeExpr(0),
@@ -594,7 +597,7 @@ internal class CompositionTest {
 
         val idx0 = mkRegisterReading(3, bv32Sort)
 
-        val reading0 = fromRegion2.read(symbolicRef2 to idx0)
+        val reading0 = fromRegion2.read(symbolicRef2 to idx0, ownership)
 
         val composedExpr0 = composer.compose(reading0)
         val composedReading0 = assertIs<UAllocatedArrayReading<Type, UBv32Sort, USizeSort>>(composedExpr0)
@@ -627,7 +630,7 @@ internal class CompositionTest {
         val composer = UComposer(this, composedMemory)
 
         val region = UAllocatedArrayId<_, _, USizeSort>(mockk<Type>(), addressSort, 1).emptyRegion()
-        val reading = region.read(mkRegisterReading(0, sizeSort))
+        val reading = region.read(mkRegisterReading(0, sizeSort), ownership)
 
         val expr = composer.compose(reading)
         assertSame(concreteNull, expr)
@@ -645,10 +648,10 @@ internal class CompositionTest {
 
         val region = UInputFieldId(field, bv32Sort)
             .emptyRegion()
-            .write(ref0, mkBv(0), trueExpr)
-            .write(ref1, mkBv(1), trueExpr)
+            .write(ref0, mkBv(0), trueExpr, ownership)
+            .write(ref1, mkBv(1), trueExpr, ownership)
 
-        val reading = region.read(ref2)
+        val reading = region.read(ref2, ownership)
 
         val composer = spyk(UComposer(this, composedMemory))
 
diff --git a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt
index 54cc603ec2..461d7ba251 100644
--- a/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/TestUtil.kt
@@ -48,7 +48,7 @@ internal class TestState(
     override val entrypoint: TestMethod = ""
 ) : UState<Any, TestMethod, TestInstruction, UContext<*>, TestTarget, TestState>(ctx, ownership, callStack, pathConstraints, memory, models, pathLocation, PathNode.root(), targetTrees) {
 
-    override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints<Any>?): TestState = this
+    override fun clone(newConstraints: UPathConstraints<Any>?): TestState = this
 
     override val isExceptional = false
 }
diff --git a/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt b/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt
index 6b0e87f7b8..587f921dbc 100644
--- a/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/api/collections/SymbolicCollectionTestBase.kt
@@ -65,7 +65,7 @@ abstract class SymbolicCollectionTestBase {
 
 
         pathConstraints = UPathConstraints(ctx, ownership)
-        memory = UMemory(ctx, pathConstraints.typeConstraints)
+        memory = UMemory(ctx, ownership, pathConstraints.typeConstraints)
         scope = StepScope(StateStub(ctx, ownership, pathConstraints, memory), UForkBlackList.createDefault())
     }
 
@@ -80,9 +80,11 @@ abstract class SymbolicCollectionTestBase {
         ctx, ownership, UCallStack(),
         pathConstraints, memory, emptyList(), PathNode.root(), PathNode.root(), UTargetsSet.empty()
     ) {
-        override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints<SingleTypeSystem.SingleType>?): StateStub {
-            val clonedConstraints = newConstraints ?: pathConstraints.clone(ownership)
-            return StateStub(ctx, ownership, clonedConstraints, memory.clone(clonedConstraints.typeConstraints))
+        override fun clone(newConstraints: UPathConstraints<SingleTypeSystem.SingleType>?): StateStub {
+            this.changeOwnership(MutabilityOwnership())
+            val cloneOwnership = MutabilityOwnership()
+            val clonedConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership)
+            return StateStub(ctx, cloneOwnership, clonedConstraints, memory.clone(clonedConstraints.typeConstraints, cloneOwnership))
         }
 
         override val isExceptional: Boolean
diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt
index ee4cb4455d..1f932ec13e 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemCpyTest.kt
@@ -30,7 +30,7 @@ class HeapMemCpyTest {
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
         val eqConstraints = UEqualityConstraints(ctx, ownership)
         val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints)
-        heap = UMemory(ctx, typeConstraints)
+        heap = UMemory(ctx, ownership, typeConstraints)
         arrayType = mockk<Type>()
         arrayValueSort = ctx.sizeSort
     }
diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt
index 8cb3e75fb4..68dbe2c17f 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapMemsetTest.kt
@@ -40,7 +40,7 @@ class HeapMemsetTest {
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
         val eqConstraints = UEqualityConstraints(ctx, ownership)
         val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints)
-        heap = UMemory(ctx, typeConstraints)
+        heap = UMemory(ctx, ownership, typeConstraints)
         arrayType = mockk<Type>()
         arrayValueSort = ctx.addressSort
     }
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 eb0854c5c8..35770d17ad 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefEqTest.kt
@@ -10,18 +10,21 @@ import org.usvm.UComponents
 import org.usvm.UContext
 import org.usvm.USizeSort
 import org.usvm.api.allocateConcreteRef
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import kotlin.test.assertSame
 
 class HeapRefEqTest {
     private lateinit var ctx: UContext<USizeSort>
     private lateinit var heap: UMemory<Type, Any>
+    private lateinit var ownership : MutabilityOwnership
 
     @BeforeEach
     fun initializeContext() {
         val components: UComponents<Type, USizeSort> = mockk()
         every { components.mkTypeSystem(any()) } returns mockk()
         ctx = UContext(components)
-        heap = UMemory(ctx, mockk())
+        ownership = MutabilityOwnership()
+        heap = UMemory(ctx, ownership, mockk())
     }
 
     @Test
@@ -156,4 +159,4 @@ class HeapRefEqTest {
         val expected = concreteRef1EqConcreteRef2 or (symbolicRefEqGuard and symbolicIteEq)
         assertSame(expected, refsEq)
     }
-}
\ No newline at end of file
+}
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 7b9c7b2df7..5379221a3e 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/HeapRefSplittingTest.kt
@@ -37,7 +37,7 @@ import kotlin.test.assertSame
 class HeapRefSplittingTest {
     private lateinit var ctx: UContext<USizeSort>
     private lateinit var heap: UMemory<Type, Any>
-    private val ownership = MutabilityOwnership()
+    private  lateinit var  ownership : MutabilityOwnership
 
     private lateinit var valueFieldDescr: Pair<Field, UBv32Sort>
     private lateinit var addressFieldDescr: Pair<Field, UAddressSort>
@@ -48,10 +48,11 @@ class HeapRefSplittingTest {
         val components: UComponents<Type, USizeSort> = mockk()
         every { components.mkTypeSystem(any()) } returns mockk()
         ctx = UContext(components)
+        ownership = MutabilityOwnership()
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
         val eqConstraints = UEqualityConstraints(ctx, ownership)
         val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints)
-        heap = UMemory(ctx, typeConstraints)
+        heap = UMemory(ctx, ownership,  typeConstraints)
 
         valueFieldDescr = mockk<Field>() to ctx.bv32Sort
         addressFieldDescr = mockk<Field>() to ctx.addressSort
diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt
index b1ec385875..b66a51da33 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/MemoryRegionTest.kt
@@ -16,6 +16,7 @@ import org.usvm.UHeapRef
 import org.usvm.USizeSort
 import org.usvm.collection.array.UAllocatedArrayId
 import org.usvm.collection.array.UInputArrayId
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.mkSizeExpr
 import org.usvm.regions.SetRegion
 import org.usvm.regions.emptyRegionTree
@@ -26,12 +27,14 @@ import kotlin.test.assertTrue
 
 class MemoryRegionTest {
     private lateinit var ctx: UContext<USizeSort>
+    private lateinit var ownership : MutabilityOwnership
 
     @BeforeEach
     fun initializeContext() {
         val components: UComponents<Type, USizeSort> = mockk()
         every { components.mkTypeSystem(any()) } returns mockk()
         ctx = UContext(components)
+        ownership = MutabilityOwnership()
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
     }
 
@@ -98,15 +101,15 @@ class MemoryRegionTest {
 
         val memoryRegion = UAllocatedArrayId<_, _, USizeSort>(mockk<Type>(), sizeSort, 0)
             .emptyRegion()
-            .write(idx1, mkBv(0), trueExpr)
-            .write(idx2, mkBv(1), trueExpr)
+            .write(idx1, mkBv(0), trueExpr, ownership)
+            .write(idx2, mkBv(1), trueExpr, ownership)
 
         val updatesBefore = memoryRegion.updates.toList()
         assertEquals(2, updatesBefore.size)
         assertTrue(updatesBefore.first().includesConcretely(idx1, trueExpr))
         assertTrue(updatesBefore.last().includesConcretely(idx2, trueExpr))
 
-        val memoryRegionAfter = memoryRegion.write(idx2, mkBv(2), trueExpr)
+        val memoryRegionAfter = memoryRegion.write(idx2, mkBv(2), trueExpr, ownership)
 
         val updatesAfter = memoryRegionAfter.updates.toList()
         assertEquals(2, updatesAfter.size)
@@ -141,13 +144,13 @@ class MemoryRegionTest {
                 val idx = indices.random(random)
                 val value = refs.random(random)
 
-                memoryRegion = memoryRegion.write(ref to idx, value, trueExpr)
+                memoryRegion = memoryRegion.write(ref to idx, value, trueExpr, ownership)
             }
 
             val readRef = symbolicRefs.random(random)
             val readIdx = indices.random(random)
 
-            memoryRegion.read(readRef to readIdx)
+            memoryRegion.read(readRef to readIdx, ownership)
         }
     }
-}
\ No newline at end of file
+}
diff --git a/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt b/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt
index f5aa639763..bc8aa31e81 100644
--- a/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/memory/SetEntriesTest.kt
@@ -42,7 +42,7 @@ class SetEntriesTest {
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
         val eqConstraints = UEqualityConstraints(ctx, ownership)
         val typeConstraints = UTypeConstraints(components.mkTypeSystem(ctx), eqConstraints)
-        heap = UMemory(ctx, typeConstraints)
+        heap = UMemory(ctx, ownership, typeConstraints)
         setType = mockk<Type>()
     }
 
diff --git a/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt b/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt
index b46c9efea8..2967d7ba43 100644
--- a/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/merging/MemoryMergingTest.kt
@@ -49,8 +49,8 @@ class MemoryMergingTest {
     fun `Empty memory`() = with(ctx) {
         val byCondition = mkConst("cond", boolSort)
         val pathConstraints = UPathConstraints<SingleType>(this, ownership)
-        val memoryLeft = UMemory<SingleType, Method>(this, pathConstraints.typeConstraints)
-        val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints)
+        val memoryLeft = UMemory<SingleType, Method>(this, ownership, pathConstraints.typeConstraints)
+        val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints, ownership)
 
         checkMergedEqualsToOriginal(
             memoryLeft,
@@ -67,12 +67,12 @@ class MemoryMergingTest {
         val byCondition = mkConst("cond", boolSort)
         val pathConstraints = UPathConstraints<SingleType>(this, ownership)
 
-        val memoryLeft = UMemory<SingleType, Method>(this, pathConstraints.typeConstraints)
+        val memoryLeft = UMemory<SingleType, Method>(this, ownership, pathConstraints.typeConstraints)
         memoryLeft.stack.push(3)
         memoryLeft.stack.writeRegister(0, mkBv(42))
         memoryLeft.stack.writeRegister(1, mkBv(1337))
 
-        val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints)
+        val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints, MutabilityOwnership())
         memoryRight.stack.writeRegister(0, mkBv(13))
         memoryRight.stack.writeRegister(2, mkBv(9))
 
@@ -92,7 +92,8 @@ class MemoryMergingTest {
             val byCondition = mkConst("cond", boolSort)
             val pathConstraints = UPathConstraints<SingleType>(this, ownership)
 
-            val memoryLeft = UMemory<SingleType, Method>(this, pathConstraints.typeConstraints)
+            val leftOwnership = ownership
+            val memoryLeft = UMemory<SingleType, Method>(this, leftOwnership, pathConstraints.typeConstraints)
 
             val ref1 = allocateConcreteRef()
             val ref2 = allocateConcreteRef()
@@ -102,7 +103,7 @@ class MemoryMergingTest {
             memoryLeft.writeField(ref2, Unit, addressSort, mkRegisterReading(2, addressSort), trueExpr)
             memoryLeft.writeField(ref3, Unit, addressSort, mkRegisterReading(3, addressSort), trueExpr)
 
-            val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints)
+            val memoryRight = memoryLeft.clone(pathConstraints.typeConstraints, MutabilityOwnership())
             memoryRight.writeField(ref1, Unit, addressSort, mkRegisterReading(-1, addressSort), trueExpr)
             memoryRight.writeField(ref2, Unit, addressSort, mkRegisterReading(-2, addressSort), trueExpr)
             memoryRight.writeField(ref3, Unit, addressSort, mkRegisterReading(-3, addressSort), trueExpr)
@@ -125,7 +126,7 @@ class MemoryMergingTest {
         vararg getters: (UMemory<SingleType, Method>) -> UExpr<out USort>,
     ) = with(ctx) {
         val mergeGuard = MutableMergeGuard(this).apply { appendThis(sequenceOf(byCondition)) }
-        val mergedMemory = checkNotNull(memoryLeft.mergeWith(memoryRight, mergeGuard))
+        val mergedMemory = checkNotNull(memoryLeft.mergeWith(memoryRight, mergeGuard, MutabilityOwnership()))
 
         for (getter in getters) {
             val leftExpr: UExpr<USort> = getter(memoryLeft).uncheckedCast()
diff --git a/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt
index 5d9ad247bb..90223020d4 100644
--- a/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelCompositionTest.kt
@@ -2,7 +2,7 @@ package org.usvm.model
 
 import io.mockk.every
 import io.mockk.mockk
-import kotlinx.collections.immutable.persistentMapOf
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.junit.jupiter.api.Assertions.assertEquals
 import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
@@ -37,6 +37,7 @@ import kotlin.test.assertSame
 
 class ModelCompositionTest {
     private lateinit var ctx: UContext<USizeSort>
+    private lateinit var ownership: MutabilityOwnership
     private lateinit var concreteNull: UConcreteHeapRef
 
     @BeforeEach
@@ -44,6 +45,7 @@ class ModelCompositionTest {
         val components: UComponents<*, USizeSort> = mockk()
         every { components.mkTypeSystem(any()) } returns mockk()
         ctx = UContext(components)
+        ownership = MutabilityOwnership()
 
         every { components.mkComposer(ctx) } answers { { memory: UReadOnlyMemory<Type> -> UComposer(ctx, memory) } }
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
@@ -62,11 +64,11 @@ class ModelCompositionTest {
 
         val region = UAllocatedArrayId<_, _, USizeSort>(mockk<Type>(), bv32Sort, 1)
             .emptyRegion()
-            .write(0.toBv(), 0.toBv(), trueExpr)
-            .write(1.toBv(), 1.toBv(), trueExpr)
-            .write(mkRegisterReading(1, sizeSort), 2.toBv(), trueExpr)
-            .write(mkRegisterReading(2, sizeSort), 3.toBv(), trueExpr)
-        val reading = region.read(mkRegisterReading(0, sizeSort))
+            .write(0.toBv(), 0.toBv(), trueExpr, ownership)
+            .write(1.toBv(), 1.toBv(), trueExpr, ownership)
+            .write(mkRegisterReading(1, sizeSort), 2.toBv(), trueExpr, ownership)
+            .write(mkRegisterReading(2, sizeSort), 3.toBv(), trueExpr, ownership)
+        val reading = region.read(mkRegisterReading(0, sizeSort), ownership)
 
         val expr = composer.compose(reading)
         assertSame(mkBv(2), expr)
@@ -79,8 +81,9 @@ class ModelCompositionTest {
 
         val composedSymbolicHeapRef = ctx.mkConcreteHeapRef(-1)
         val inputArray = UMemory2DArray(
-            persistentMapOf((composedSymbolicHeapRef to mkBv(0)) to mkBv(1)), mkBv(0)
+            persistentHashMapOf(ownership, (composedSymbolicHeapRef to mkBv(0)) to  mkBv(1)), mkBv(0)
         )
+
         val arrayModel = UArrayEagerModelRegion(arrayMemoryId, inputArray)
 
         val stackModel = URegistersStackEagerModel(
@@ -111,7 +114,7 @@ class ModelCompositionTest {
 
         val idx = mkRegisterReading(1, sizeSort)
 
-        val reading = concreteRegion.read(idx)
+        val reading = concreteRegion.read(idx, ownership)
 
         val expr = composer.compose(reading)
         assertSame(mkBv(1), expr)
@@ -132,7 +135,7 @@ class ModelCompositionTest {
         val arrayType = mockk<Type>()
 
         val arrayLengthMemoryId = UArrayLengthsRegionId(sizeSort, arrayType)
-        val inputLength = UMemory1DArray(persistentMapOf(composedRef0 to mkBv(42)), mkBv(0))
+        val inputLength = UMemory1DArray(persistentHashMapOf(ownership, composedRef0 to mkBv(42)), mkBv(0))
         val arrayLengthModel = UArrayLengthEagerModelRegion(arrayLengthMemoryId, inputLength)
 
         val stackModel = URegistersStackEagerModel(
@@ -153,10 +156,10 @@ class ModelCompositionTest {
 
         val region = UInputArrayLengthId(arrayType, bv32Sort)
             .emptyRegion()
-            .write(symbolicRef1, 0.toBv(), trueExpr)
-            .write(symbolicRef2, 1.toBv(), trueExpr)
-            .write(symbolicRef3, 2.toBv(), trueExpr)
-        val reading = region.read(symbolicRef0)
+            .write(symbolicRef1, 0.toBv(), trueExpr, ownership)
+            .write(symbolicRef2, 1.toBv(), trueExpr, ownership)
+            .write(symbolicRef3, 2.toBv(), trueExpr, ownership)
+        val reading = region.read(symbolicRef0, ownership)
 
         val expr = composer.compose(reading)
         assertSame(mkBv(42), expr)
@@ -177,7 +180,7 @@ class ModelCompositionTest {
         val field = mockk<Field>()
         val fieldMemoryId = UFieldsRegionId(field, addressSort)
 
-        val inputField = UMemory1DArray(persistentMapOf(composedRef0 to composedRef0), concreteNull)
+        val inputField = UMemory1DArray(persistentHashMapOf(ownership, composedRef0 to composedRef0), concreteNull)
         val fieldModel = UFieldsEagerModelRegion(fieldMemoryId, inputField)
 
         val stackModel = URegistersStackEagerModel(
@@ -198,10 +201,10 @@ class ModelCompositionTest {
 
         val region = UInputFieldId(field, addressSort)
             .emptyRegion()
-            .write(symbolicRef1, symbolicRef1, trueExpr)
-            .write(symbolicRef2, symbolicRef2, trueExpr)
-            .write(symbolicRef3, symbolicRef3, trueExpr)
-        val reading = region.read(symbolicRef0)
+            .write(symbolicRef1, symbolicRef1, trueExpr, ownership)
+            .write(symbolicRef2, symbolicRef2, trueExpr, ownership)
+            .write(symbolicRef3, symbolicRef3, trueExpr, ownership)
+        val reading = region.read(symbolicRef0, ownership)
 
         val expr = composer.compose(reading)
         assertSame(composedRef0, expr)
@@ -230,9 +233,9 @@ class ModelCompositionTest {
 
         run {
             val region = emptyRegion
-                .write(index0, nonDefaultValue0, trueGuard)
-                .write(index0, nonDefaultValue1, falseGuard)
-            val reading = region.read(index0)
+                .write(index0, nonDefaultValue0, trueGuard, ownership)
+                .write(index0, nonDefaultValue1, falseGuard, ownership)
+            val reading = region.read(index0, ownership)
 
             val expr = composer.compose(reading)
             assertEquals(nonDefaultValue0, expr)
@@ -240,9 +243,9 @@ class ModelCompositionTest {
 
         run {
             val region = emptyRegion
-                .write(index1, nonDefaultValue0, trueGuard)
-                .write(index0, nonDefaultValue1, falseGuard)
-            val reading = region.read(index0)
+                .write(index1, nonDefaultValue0, trueGuard, ownership)
+                .write(index0, nonDefaultValue1, falseGuard, ownership)
+            val reading = region.read(index0, ownership)
 
             val expr = composer.compose(reading)
             assertEquals(defaultValue, expr)
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 03d4054171..c110617472 100644
--- a/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/model/ModelDecodingTest.kt
@@ -74,8 +74,8 @@ class ModelDecodingTest {
 
         stack = URegistersStack()
         stack.push(10)
-        mocker = UIndexedMocker()
-        heap = UMemory(ctx, pc.typeConstraints, stack, mocker)
+        mocker = UIndexedMocker(ownership = ownership)
+        heap = UMemory(ctx, ownership, pc.typeConstraints, stack, mocker)
     }
 
     @Test
diff --git a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt
index 1566188f85..5b50a547a3 100644
--- a/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/solver/SoftConstraintsTest.kt
@@ -132,11 +132,11 @@ open class SoftConstraintsTest {
         val secondInputRef = mkRegisterReading(1, addressSort)
         val region = UInputArrayLengthId(arrayType, sizeSort)
             .emptyRegion()
-            .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr)
+            .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr, ownership)
 
         val size = 25
 
-        val reading = region.read(secondInputRef)
+        val reading = region.read(secondInputRef, ownership)
 
         val pc = UPathConstraints<Type>(ctx, ownership)
         pc += reading eq size.toBv()
@@ -158,7 +158,7 @@ open class SoftConstraintsTest {
         val inputRef = mkRegisterReading(0, addressSort)
         val region = UInputArrayLengthId(arrayType, sizeSort)
             .emptyRegion()
-            .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr)
+            .write(inputRef, mkRegisterReading(3, sizeSort), guard = trueExpr, ownership)
 
         val pc = UPathConstraints<Type>(ctx, ownership)
         pc += (inputRef eq nullRef).not()
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 16a05dcad3..7569676364 100644
--- a/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/solver/TranslationTest.kt
@@ -32,6 +32,7 @@ import org.usvm.collection.array.USymbolicArrayInputToInputCopyAdapter
 import org.usvm.collection.array.length.UInputArrayLengthId
 import org.usvm.collection.field.UInputFieldId
 import org.usvm.collection.map.ref.URefMapEntryLValue
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.memory.UMemory
 import org.usvm.mkSizeExpr
 import org.usvm.memory.key.USizeExprKeyInfo
@@ -41,6 +42,7 @@ import kotlin.test.assertSame
 
 class TranslationTest {
     private lateinit var ctx: RecordingCtx
+    private lateinit var ownership: MutabilityOwnership
     private lateinit var heap: UMemory<Type, Any>
     private lateinit var translator: UExprTranslator<Type, *>
 
@@ -69,8 +71,9 @@ class TranslationTest {
         every { components.mkTypeSystem(any()) } returns mockk()
 
         ctx = RecordingCtx(components)
+        ownership = MutabilityOwnership()
         every { components.mkSizeExprProvider(any()) } answers { UBv32SizeExprProvider(ctx) }
-        heap = UMemory(ctx, mockk())
+        heap = UMemory(ctx, ownership, mockk())
         translator = UExprTranslator(ctx)
 
         valueFieldDescr = mockk<Field>() to ctx.bv32Sort
@@ -144,13 +147,13 @@ class TranslationTest {
 
         val region = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort)
             .emptyRegion()
-            .write(ref1 to idx1, val1, trueExpr)
-            .write(ref2 to idx2, val2, trueExpr)
+            .write(ref1 to idx1, val1, trueExpr, ownership)
+            .write(ref2 to idx2, val2, trueExpr, ownership)
 
         val ref3 = mkRegisterReading(4, addressSort)
         val idx3 = mkRegisterReading(5, sizeSort)
 
-        val reading = region.read(ref3 to idx3)
+        val reading = region.read(ref3 to idx3, ownership)
 
         val translated = translator.translate(reading)
 
@@ -175,8 +178,8 @@ class TranslationTest {
 
         val region = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort)
             .emptyRegion()
-            .write(ref1 to idx1, val1, trueExpr)
-            .write(ref2 to idx2, val2, trueExpr)
+            .write(ref1 to idx1, val1, trueExpr, ownership)
+            .write(ref2 to idx2, val2, trueExpr, ownership)
 
         val concreteRef = allocateConcreteRef()
 
@@ -193,13 +196,13 @@ class TranslationTest {
             .copyRange(region, adapter, trueExpr)
 
         val idx = mkRegisterReading(4, sizeSort)
-        val reading = concreteRegion.read(idx)
+        val reading = concreteRegion.read(idx, ownership)
 
 
         val keyInfo = region.collectionId.keyInfo()
         val key = keyInfo.mapKey(adapter.convert(translator.translate(idx), composer = null), translator)
         val innerReading =
-            translator.translate(region.read(key))
+            translator.translate(region.read(key, ownership))
         val guard =
             translator.translate((mkBvSignedLessOrEqualExpr(mkBv(0), idx)) and mkBvSignedLessOrEqualExpr(idx, mkBv(5)))
         val expected = mkIte(guard, innerReading, mkBv(0))
@@ -227,12 +230,12 @@ class TranslationTest {
 
         val region = UInputFieldId(mockk<Field>(), bv32Sort)
             .emptyRegion()
-            .write(ref1, mkBv(1), g1)
-            .write(ref2, mkBv(2), g2)
-            .write(ref3, mkBv(3), g3)
+            .write(ref1, mkBv(1), g1, ownership)
+            .write(ref2, mkBv(2), g2, ownership)
+            .write(ref3, mkBv(3), g3, ownership)
 
         val ref0 = mkRegisterReading(0, addressSort)
-        val reading = region.read(ref0)
+        val reading = region.read(ref0, ownership)
 
         val ref0Eq1Or2Or3 = (ref0 eq ref1) or (ref0 eq ref2) or (ref0 eq ref3)
         val readingNeq123 = (reading neq mkBv(1)) and (reading neq mkBv(2)) and (reading neq mkBv(3))
@@ -253,12 +256,12 @@ class TranslationTest {
 
         val region = UInputArrayLengthId(mockk<Field>(), bv32Sort)
             .emptyRegion()
-            .write(ref1, mkBv(1), trueExpr)
-            .write(ref2, mkBv(2), trueExpr)
-            .write(ref3, mkBv(3), trueExpr)
+            .write(ref1, mkBv(1), trueExpr, ownership)
+            .write(ref2, mkBv(2), trueExpr, ownership)
+            .write(ref3, mkBv(3), trueExpr, ownership)
 
         val ref0 = mkRegisterReading(0, addressSort)
-        val reading = region.read(ref0)
+        val reading = region.read(ref0, ownership)
 
         val ref0Eq1Or2Or3 = (ref0 eq ref1) or (ref0 eq ref2) or (ref0 eq ref3)
         val readingNeq123 = (reading neq mkBv(1)) and (reading neq mkBv(2)) and (reading neq mkBv(3))
@@ -283,8 +286,8 @@ class TranslationTest {
 
         val inputRegion1 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort)
             .emptyRegion()
-            .write(ref1 to idx1, val1, trueExpr)
-            .write(ref2 to idx2, val2, trueExpr)
+            .write(ref1 to idx1, val1, trueExpr, ownership)
+            .write(ref2 to idx2, val2, trueExpr, ownership)
 
 
         val adapter = USymbolicArrayInputToInputCopyAdapter(
@@ -297,12 +300,12 @@ class TranslationTest {
         var inputRegion2 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, bv32Sort).emptyRegion()
 
         val idx = mkRegisterReading(4, sizeSort)
-        val reading1 = inputRegion2.read(ref2 to idx)
+        val reading1 = inputRegion2.read(ref2 to idx, ownership)
 
         inputRegion2 = inputRegion2
             .copyRange(inputRegion1, adapter, trueExpr)
 
-        val reading2 = inputRegion2.read(ref2 to idx)
+        val reading2 = inputRegion2.read(ref2 to idx, ownership)
 
         val expr = (reading1 neq reading2) and (ref1 neq ref2)
         val translated = translator.translate(expr)
@@ -383,8 +386,8 @@ class TranslationTest {
 
         val inputRegion1 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, addressSort)
             .emptyRegion()
-            .write(ref1 to idx1, val1, trueExpr)
-            .write(ref2 to idx2, val2, trueExpr)
+            .write(ref1 to idx1, val1, trueExpr, ownership)
+            .write(ref2 to idx2, val2, trueExpr, ownership)
 
         val adapter = USymbolicArrayInputToInputCopyAdapter(
             ref1 to mkSizeExpr(0),
@@ -396,12 +399,12 @@ class TranslationTest {
         var inputRegion2 = UInputArrayId<_, _, USizeSort>(valueArrayDescr, addressSort).emptyRegion()
 
         val idx = mkRegisterReading(4, sizeSort)
-        val reading1 = inputRegion2.read(ref2 to idx)
+        val reading1 = inputRegion2.read(ref2 to idx, ownership)
 
         inputRegion2 = inputRegion2
             .copyRange(inputRegion1, adapter, trueExpr)
 
-        val reading2 = inputRegion2.read(ref2 to idx)
+        val reading2 = inputRegion2.read(ref2 to idx, ownership)
 
         val expr = (reading1 neq reading2) and (ref1 neq ref2)
         val translated = translator.translate(expr)
@@ -424,8 +427,8 @@ class TranslationTest {
 
         val allocatedRegion1 = UAllocatedArrayId<_, _, USizeSort>(valueArrayDescr, addressSort, 1)
             .emptyRegion()
-            .write(idx1, val1, trueExpr)
-            .write(idx2, val2, trueExpr)
+            .write(idx1, val1, trueExpr, ownership)
+            .write(idx2, val2, trueExpr, ownership)
 
         val adapter = USymbolicArrayAllocatedToAllocatedCopyAdapter(
             mkSizeExpr(0), mkSizeExpr(0), mkSizeExpr(5), USizeExprKeyInfo()
@@ -435,12 +438,12 @@ class TranslationTest {
             .emptyRegion()
 
         val idx = mkRegisterReading(4, sizeSort)
-        val readingBeforeCopy = allocatedRegion2.read(idx)
+        val readingBeforeCopy = allocatedRegion2.read(idx, ownership)
 
         allocatedRegion2 = allocatedRegion2
             .copyRange(allocatedRegion1, adapter, trueExpr)
 
-        val readingAfterCopy = allocatedRegion2.read(idx)
+        val readingAfterCopy = allocatedRegion2.read(idx, ownership)
 
         val outsideOfCopy = mkBvSignedLessExpr(idx, mkBv(0)) or mkBvSignedLessExpr(mkBv(5), idx)
         val expr = (readingBeforeCopy neq readingAfterCopy) and outsideOfCopy
@@ -458,15 +461,15 @@ class TranslationTest {
     fun testCachingOfTranslatedMemoryUpdates() = with(ctx) {
         val allocatedRegion = UAllocatedArrayId<_, _, USizeSort>(valueArrayDescr, sizeSort, 0)
             .emptyRegion()
-            .write(mkRegisterReading(0, sizeSort), mkBv(0), trueExpr)
-            .write(mkRegisterReading(1, sizeSort), mkBv(1), trueExpr)
+            .write(mkRegisterReading(0, sizeSort), mkBv(0), trueExpr, ownership)
+            .write(mkRegisterReading(1, sizeSort), mkBv(1), trueExpr, ownership)
 
         val allocatedRegionExtended = allocatedRegion
-            .write(mkRegisterReading(2, sizeSort), mkBv(2), trueExpr)
-            .write(mkRegisterReading(3, sizeSort), mkBv(3), trueExpr)
+            .write(mkRegisterReading(2, sizeSort), mkBv(2), trueExpr, ownership)
+            .write(mkRegisterReading(3, sizeSort), mkBv(3), trueExpr, ownership)
 
-        val reading = allocatedRegion.read(mkRegisterReading(4, sizeSort))
-        val readingExtended = allocatedRegionExtended.read(mkRegisterReading(5, sizeSort))
+        val reading = allocatedRegion.read(mkRegisterReading(4, sizeSort), ownership)
+        val readingExtended = allocatedRegionExtended.read(mkRegisterReading(5, sizeSort), ownership)
 
         translator.translate(reading)
 
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 676abc5f32..83df9804c0 100644
--- a/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt
+++ b/usvm-core/src/test/kotlin/org/usvm/types/TypeSolverTest.kt
@@ -79,8 +79,7 @@ class TypeSolverTest {
     }
 
     private val pc = UPathConstraints<TestType>(ctx, ownership)
-    private val memory = UMemory<TestType, Method>(ctx, pc.typeConstraints)
-
+    private val memory = UMemory<TestType, Method>(ctx, ownership, pc.typeConstraints)
     @Test
     fun `Test concrete ref -- open type inheritance`() {
         val ref = memory.allocConcrete(base1)
@@ -346,18 +345,18 @@ class TypeSolverTest {
         val idx2 = 0.toBv()
 
         val field = mockk<Field>()
-        val heap = UMemory<TestType, Any>(ctx, mockk())
+        val heap = UMemory<TestType, Any>(ctx, ownership, mockk())
 
         heap.writeField(val1, field, bv32Sort, 1.toBv(), trueExpr)
         heap.writeField(val2, field, bv32Sort, 2.toBv(), trueExpr)
 
         val inputRegion = UInputArrayId<_, _, USizeSort>(mockk<TestType>(), addressSort)
             .emptyRegion()
-            .write(arr1 to idx1, val1, trueExpr)
-            .write(arr2 to idx2, val2, trueExpr)
+            .write(arr1 to idx1, val1, trueExpr, ownership)
+            .write(arr2 to idx2, val2, trueExpr, ownership)
 
-        val firstReading = inputRegion.read(arr1 to idx1)
-        val secondReading = inputRegion.read(arr2 to idx2)
+        val firstReading = inputRegion.read(arr1 to idx1, ownership)
+        val secondReading = inputRegion.read(arr2 to idx2, ownership)
 
         pc += mkIsSubtypeExpr(arr1, base1)
         pc += mkIsSubtypeExpr(arr2, base1)
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt
index 253aeaf092..a91e2c6de9 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcTransformer.kt
@@ -10,6 +10,7 @@ import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.UTransformer
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.machine.interpreter.statics.JcStaticFieldLValue
 import org.usvm.machine.interpreter.statics.JcStaticFieldReading
 import org.usvm.machine.interpreter.statics.JcStaticFieldRegionId
@@ -62,7 +63,7 @@ class JcStaticFieldModel<Sort : USort>(
     private val translatedFields: Map<JcField, UExpr<Sort>>,
     private val translator: UExprTranslator<*, *>
 ) : UReadOnlyMemoryRegion<JcStaticFieldLValue<Sort>, Sort> {
-    override fun read(key: JcStaticFieldLValue<Sort>): UExpr<Sort> {
+    override fun read(key: JcStaticFieldLValue<Sort>, ownership: MutabilityOwnership): UExpr<Sort> {
         val translated = translatedFields[key.field]
             ?: translator.translate(
                 key.sort.jctx.mkStaticFieldReading(key.memoryRegionId as JcStaticFieldRegionId, key.field, key.sort)
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt
index c40114a44e..aa565921ff 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/JcCallSiteRegion.kt
@@ -1,13 +1,14 @@
 package org.usvm.machine.interpreter
 
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.jacodb.api.jvm.cfg.JcLambdaExpr
 import org.usvm.UAddressSort
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapAddress
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.machine.JcContext
 import org.usvm.memory.UMemoryRegion
 import org.usvm.memory.UMemoryRegionId
@@ -22,21 +23,22 @@ class JcLambdaCallSiteRegionId(private val ctx: JcContext) : UMemoryRegionId<Not
 
 internal class JcLambdaCallSiteMemoryRegion(
     private val ctx: JcContext,
-    private val callSites: PersistentMap<UConcreteHeapAddress, JcLambdaCallSite> = persistentHashMapOf()
+    private val callSites: UPersistentHashMap<UConcreteHeapAddress, JcLambdaCallSite> = persistentHashMapOf()
 ) : UMemoryRegion<Nothing, UAddressSort> {
-    fun writeCallSite(callSite: JcLambdaCallSite) =
-        JcLambdaCallSiteMemoryRegion(ctx, callSites.put(callSite.ref.address, callSite))
+    fun writeCallSite(callSite: JcLambdaCallSite, ownership: MutabilityOwnership) =
+        JcLambdaCallSiteMemoryRegion(ctx, callSites.put(callSite.ref.address, callSite, ownership))
 
     fun findCallSite(ref: UConcreteHeapRef): JcLambdaCallSite? = callSites[ref.address]
 
-    override fun read(key: Nothing): UExpr<UAddressSort> {
+    override fun read(key: Nothing, ownership: MutabilityOwnership): UExpr<UAddressSort> {
         error("Unsupported operation for call site region")
     }
 
     override fun write(
         key: Nothing,
         value: UExpr<UAddressSort>,
-        guard: UBoolExpr
+        guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): UMemoryRegion<Nothing, UAddressSort> {
         error("Unsupported operation for call site region")
     }
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 3b2f49f8e7..577f26a165 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
@@ -424,7 +424,7 @@ class JcExprResolver(
 
     private fun UWritableMemory<JcType>.writeCallSite(callSite: JcLambdaCallSite) {
         val callSiteRegion = getRegion(ctx.lambdaCallSiteRegionId) as JcLambdaCallSiteMemoryRegion
-        val updatedRegion = callSiteRegion.writeCallSite(callSite)
+        val updatedRegion = callSiteRegion.writeCallSite(callSite, ownership)
         setRegion(ctx.lambdaCallSiteRegionId, updatedRegion)
     }
 
@@ -637,7 +637,7 @@ class JcExprResolver(
 
         val enumValuesFieldLengthLValue = UArrayLengthLValue(enumValuesRef, enumValuesArrayDescriptor, sizeSort)
         val enumValuesFieldLengthBeforeClinit =
-            enumValuesFieldLengthLValue.memoryRegionId.emptyRegion().read(enumValuesFieldLengthLValue)
+            enumValuesFieldLengthLValue.memoryRegionId.emptyRegion().read(enumValuesFieldLengthLValue, ownership)
         val enumValuesFieldLengthAfterClinit = memory.read(enumValuesFieldLengthLValue)
 
         // Ensure that $VALUES in a model has the same length as the $VALUES in the memory
@@ -652,13 +652,13 @@ class JcExprResolver(
                 UArrayIndexLValue(addressSort, enumValuesRef, mkSizeExpr(ordinal), cp.objectType)
             val enumConstantRefAfterClinit = memory.read(enumConstantLValue)
             val enumConstantRefBeforeClinit =
-                enumConstantLValue.memoryRegionId.emptyRegion().read(enumConstantLValue)
+                enumConstantLValue.memoryRegionId.emptyRegion().read(enumConstantLValue, ownership)
 
             val ordinalFieldLValue =
                 UFieldLValue(sizeSort, enumConstantRefAfterClinit, enumOrdinalField)
             val ordinalFieldValueAfterClinit = memory.read(ordinalFieldLValue)
             val ordinalEmptyRegion = ordinalFieldLValue.memoryRegionId.emptyRegion()
-            val ordinalFieldValueBeforeClinit = ordinalEmptyRegion.read(ordinalFieldLValue)
+            val ordinalFieldValueBeforeClinit = ordinalEmptyRegion.read(ordinalFieldLValue, ownership)
 
             // Ensure that the ordinal of each enum constant equals to the real ordinal value
             scope.assert(mkEq(ordinalFieldValueAfterClinit, ordinalFieldValueBeforeClinit))
@@ -1008,7 +1008,7 @@ class JcExprResolver(
                     if (sort === voidSort) return@forEach
 
                     val memoryRegion = memory.getRegion(JcStaticFieldRegionId(sort)) as JcStaticFieldsMemoryRegion<*>
-                    memoryRegion.mutatePrimitiveStaticFieldValuesToSymbolic(staticInitializer.enclosingClass)
+                    memoryRegion.mutatePrimitiveStaticFieldValuesToSymbolic(staticInitializer.enclosingClass, scope.ownership)
                 }
             }
         }
@@ -1154,4 +1154,4 @@ class JcSimpleValueResolver(
         scope.calcOnState {
             mkStringConstRef(value)
         }
-}
\ No newline at end of file
+}
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt
index 87e58f9244..8f8db30c97 100644
--- a/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt
+++ b/usvm-jvm/src/main/kotlin/org/usvm/machine/interpreter/statics/JcStaticFieldsRegion.kt
@@ -1,8 +1,6 @@
 package org.usvm.machine.interpreter.statics
 
 import kotlinx.collections.immutable.PersistentList
-import kotlinx.collections.immutable.PersistentMap
-import kotlinx.collections.immutable.persistentHashMapOf
 import kotlinx.collections.immutable.persistentListOf
 import org.jacodb.api.jvm.JcClassOrInterface
 import org.jacodb.api.jvm.JcField
@@ -16,6 +14,9 @@ import org.usvm.UBoolExpr
 import org.usvm.UBoolSort
 import org.usvm.UExpr
 import org.usvm.USort
+import org.usvm.collections.immutable.implementations.immutableMap.UPersistentHashMap
+import org.usvm.collections.immutable.internal.MutabilityOwnership
+import org.usvm.collections.immutable.persistentHashMapOf
 import org.usvm.isTrue
 import org.usvm.machine.JcContext
 import org.usvm.machine.jctx
@@ -46,13 +47,14 @@ data class JcStaticFieldRegionId<Sort : USort>(
 
 internal class JcStaticFieldsMemoryRegion<Sort : USort>(
     private val sort: Sort,
-    private var fieldValuesByClass: PersistentMap<JcClassOrInterface, PersistentMap<JcField, UExpr<Sort>>> = persistentHashMapOf(),
+    // TODO multimap
+    private var fieldValuesByClass: UPersistentHashMap<JcClassOrInterface, UPersistentHashMap<JcField, UExpr<Sort>>> = persistentHashMapOf(),
     private var initialStatics: PersistentList<JcField> = persistentListOf()
 ) : UMemoryRegion<JcStaticFieldLValue<Sort>, Sort> {
     val mutableStaticFields: List<JcField>
         get() = initialStatics
 
-    override fun read(key: JcStaticFieldLValue<Sort>): UExpr<Sort> {
+    override fun read(key: JcStaticFieldLValue<Sort>, ownership: MutabilityOwnership): UExpr<Sort> {
         val field = key.field
         return fieldValuesByClass[field.enclosingClass]?.get(field)
             ?: sort.jctx.mkStaticFieldReading(key.memoryRegionId as JcStaticFieldRegionId, field, sort)
@@ -62,36 +64,32 @@ internal class JcStaticFieldsMemoryRegion<Sort : USort>(
         key: JcStaticFieldLValue<Sort>,
         value: UExpr<Sort>,
         guard: UBoolExpr,
+        ownership: MutabilityOwnership
     ): UMemoryRegion<JcStaticFieldLValue<Sort>, Sort> {
         val field = key.field
-
         val enclosingClass = field.enclosingClass
-        if (enclosingClass !in fieldValuesByClass) {
-            fieldValuesByClass = fieldValuesByClass.put(enclosingClass, persistentHashMapOf())
-        }
-
-        val newFieldValues = fieldValuesByClass
-            .getValue(enclosingClass)
-            .guardedWrite(key.field, value, guard) { key.sort.sampleUValue() }
-        val newFieldsByClass = fieldValuesByClass.put(enclosingClass, newFieldValues)
+        val classFields =  fieldValuesByClass.getOrDefault(enclosingClass, persistentHashMapOf())
+        
+        val newFieldValues = classFields.guardedWrite(key.field, value, guard, ownership) { key.sort.sampleUValue() }
+        val newFieldsByClass = fieldValuesByClass.put(enclosingClass, newFieldValues, ownership)
 
         return JcStaticFieldsMemoryRegion(sort, newFieldsByClass, initialStatics)
     }
 
-    fun mutatePrimitiveStaticFieldValuesToSymbolic(enclosingClass: JcClassOrInterface) {
+    fun mutatePrimitiveStaticFieldValuesToSymbolic(enclosingClass: JcClassOrInterface, ownership: MutabilityOwnership) {
         val staticFields = fieldValuesByClass[enclosingClass] ?: return
 
         val staticsToRemove = staticFields
-            .keys
+            .keys()
             .filter { fieldShouldBeSymbolic(it) }
 
         initialStatics = initialStatics.addAll(staticsToRemove)
 
         // Remove concrete fields from the region
         val updatedStaticFields = staticsToRemove.fold(staticFields) { acc, field ->
-            acc.remove(field)
+            acc.remove(field, ownership)
         }
-        fieldValuesByClass = fieldValuesByClass.put(enclosingClass, updatedStaticFields)
+        fieldValuesByClass = fieldValuesByClass.put(enclosingClass, updatedStaticFields, ownership)
     }
 
     companion object {
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 39cbc40b4f..9bd688be4a 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
@@ -21,7 +21,7 @@ class JcState(
     override val entrypoint: JcMethod,
     callStack: UCallStack<JcMethod, JcInst> = UCallStack(),
     pathConstraints: UPathConstraints<JcType> = UPathConstraints(ctx, ownership),
-    memory: UMemory<JcType, JcMethod> = UMemory(ctx, pathConstraints.typeConstraints),
+    memory: UMemory<JcType, JcMethod> = UMemory(ctx, ownership, pathConstraints.typeConstraints),
     models: List<UModelBase<JcType>> = listOf(),
     pathNode: PathNode<JcInst> = PathNode.root(),
     forkPoints: PathNode<PathNode<JcInst>> = PathNode.root(),
@@ -38,15 +38,17 @@ class JcState(
     forkPoints,
     targets
 ) {
-    override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints<JcType>?): JcState {
-        val clonedConstraints = newConstraints ?: pathConstraints.clone(ownership)
+    override fun clone(newConstraints: UPathConstraints<JcType>?): JcState {
+        this.changeOwnership(MutabilityOwnership())
+        val cloneOwnership = MutabilityOwnership()
+        val clonedConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership)
         return JcState(
             ctx,
-            ownership,
+            cloneOwnership,
             entrypoint,
             callStack.clone(),
             clonedConstraints,
-            memory.clone(clonedConstraints.typeConstraints),
+            memory.clone(clonedConstraints.typeConstraints, cloneOwnership),
             models,
             pathNode,
             forkPoints,
@@ -60,7 +62,10 @@ class JcState(
      *
      * @return the merged state. TODO: Now it may reuse some of the internal components of the former states.
      */
-    override fun mergeWith(other: JcState, by: Unit, ownership: MutabilityOwnership): JcState? {
+    override fun mergeWith(other: JcState, by: Unit): JcState? {
+        this.changeOwnership(MutabilityOwnership())
+        other.changeOwnership(MutabilityOwnership())
+        val newOwnership = MutabilityOwnership()
         require(entrypoint == other.entrypoint) { "Cannot merge states with different entrypoints" }
         // TODO: copy-paste
 
@@ -69,11 +74,11 @@ class JcState(
 
         val mergeGuard = MutableMergeGuard(ctx)
         val mergedCallStack = callStack.mergeWith(other.callStack, Unit) ?: return null
-        val mergedPathConstraints = pathConstraints.mergeWith(other.pathConstraints, mergeGuard, ownership)
+        val mergedPathConstraints = pathConstraints.mergeWith(other.pathConstraints, mergeGuard, newOwnership)
             ?: return null
         val mergedMemory = 
-            memory.clone(mergedPathConstraints.typeConstraints)
-                  .mergeWith(other.memory, mergeGuard)
+            memory.clone(mergedPathConstraints.typeConstraints, newOwnership)
+                  .mergeWith(other.memory, mergeGuard, newOwnership)
             ?: return null
         val mergedModels = models + other.models
         val methodResult = if (other.methodResult == JcMethodResult.NoCall && methodResult == JcMethodResult.NoCall) {
@@ -86,7 +91,7 @@ class JcState(
 
         return JcState(
             ctx,
-            ownership,
+            newOwnership,
             entrypoint,
             mergedCallStack,
             mergedPathConstraints,
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt
index d1dfd600eb..a42718d0c9 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyMachine.kt
@@ -2,6 +2,7 @@ package org.usvm.machine
 
 import org.usvm.UMachine
 import org.usvm.UPathSelector
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.language.PyCallable
 import org.usvm.language.PyPinnedCallable
 import org.usvm.language.PyProgram
@@ -60,10 +61,12 @@ class PyMachine(
         )
 
     private fun getInitialState(target: PyUnpinnedCallable): PyState {
-        val pathConstraints = PyPathConstraints(ctx)
+        val initOwnership = MutabilityOwnership()
+        val pathConstraints = PyPathConstraints(ctx,initOwnership )
         val memory = UMemory<PythonType, PyCallable>(
             ctx,
-            pathConstraints.typeConstraints
+            initOwnership,
+            pathConstraints.typeConstraints,
         ).apply {
             stack.push(target.numberOfArguments)
         }
@@ -78,6 +81,7 @@ class PyMachine(
 
         return PyState(
             ctx,
+            initOwnership,
             target,
             symbols,
             pathConstraints,
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt
index c7384dd257..c2a91fbee8 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyPathConstraints.kt
@@ -5,6 +5,7 @@ import kotlinx.collections.immutable.persistentHashSetOf
 import org.usvm.UBoolExpr
 import org.usvm.UBv32Sort
 import org.usvm.UContext
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.constraints.UEqualityConstraints
 import org.usvm.constraints.ULogicalConstraints
 import org.usvm.constraints.UNumericConstraints
@@ -14,26 +15,28 @@ import org.usvm.machine.types.PythonType
 
 class PyPathConstraints(
     ctx: UContext<*>,
+    ownership: MutabilityOwnership,
     logicalConstraints: ULogicalConstraints = ULogicalConstraints.empty(),
-    equalityConstraints: UEqualityConstraints = UEqualityConstraints(ctx),
+    equalityConstraints: UEqualityConstraints = UEqualityConstraints(ctx, ownership),
     typeConstraints: UTypeConstraints<PythonType> = UTypeConstraints(
         ctx.typeSystem(),
         equalityConstraints
     ),
-    numericConstraints: UNumericConstraints<UBv32Sort> = UNumericConstraints(ctx, sort = ctx.bv32Sort),
+    numericConstraints: UNumericConstraints<UBv32Sort> = UNumericConstraints(ctx, sort = ctx.bv32Sort, ownership = ownership),
     var pythonSoftConstraints: PersistentSet<UBoolExpr> = persistentHashSetOf(),
 ) : UPathConstraints<PythonType>(
     ctx,
+    ownership,
     logicalConstraints,
     equalityConstraints,
     typeConstraints,
     numericConstraints
 ) {
-    override fun clone(): PyPathConstraints {
+    override fun clone(ownership: MutabilityOwnership): PyPathConstraints {
         val clonedLogicalConstraints = logicalConstraints.clone()
-        val clonedEqualityConstraints = equalityConstraints.clone()
+        val clonedEqualityConstraints = equalityConstraints.clone(ownership)
         val clonedTypeConstraints = typeConstraints.clone(clonedEqualityConstraints)
-        val clonedNumericConstraints = numericConstraints.clone()
+        val clonedNumericConstraints = numericConstraints.clone(ownership)
         return PyPathConstraints(
             ctx = ctx,
             logicalConstraints = clonedLogicalConstraints,
@@ -41,6 +44,7 @@ class PyPathConstraints(
             typeConstraints = clonedTypeConstraints,
             numericConstraints = clonedNumericConstraints,
             pythonSoftConstraints = pythonSoftConstraints,
+            ownership = ownership
         )
     }
 }
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt
index 1c4c3e3150..881f0d1439 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/PyState.kt
@@ -10,6 +10,7 @@ import org.usvm.UCallStack
 import org.usvm.UMockSymbol
 import org.usvm.UPathSelector
 import org.usvm.UState
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.constraints.UPathConstraints
 import org.usvm.language.PyCallable
 import org.usvm.language.PyInstruction
@@ -32,6 +33,7 @@ private val targets = UTargetsSet.empty<PyTarget, PyInstruction>()
 
 class PyState(
     ctx: PyContext,
+    ownership: MutabilityOwnership,
     private val pythonCallable: PyUnpinnedCallable,
     val inputSymbols: List<UninterpretedSymbolicPythonObject>,
     override val pathConstraints: PyPathConstraints,
@@ -50,6 +52,7 @@ class PyState(
     var uniqueInstructions: PersistentSet<PyInstruction> = persistentSetOf(),
 ) : UState<PythonType, PyCallable, PyInstruction, PyContext, PyTarget, PyState>(
     ctx,
+    ownership,
     callStack,
     pathConstraints,
     memory,
@@ -60,10 +63,13 @@ class PyState(
 ) {
     override fun clone(newConstraints: UPathConstraints<PythonType>?): PyState {
         require(newConstraints is PyPathConstraints?)
-        val newPathConstraints = newConstraints ?: pathConstraints.clone()
-        val newMemory = memory.clone(newPathConstraints.typeConstraints)
+        this.changeOwnership(ownership)
+        val cloneOwnership = MutabilityOwnership()
+        val newPathConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership)
+        val newMemory = memory.clone(newPathConstraints.typeConstraints, cloneOwnership)
         return PyState(
             ctx,
+            cloneOwnership,
             pythonCallable,
             inputSymbols,
             newPathConstraints,
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt
index d1ef3676d8..fd413321c6 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayIndexRegion.kt
@@ -6,6 +6,7 @@ import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.collection.array.UArrayIndexLValue
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.machine.PyContext
 import org.usvm.machine.model.PyModel
 import org.usvm.machine.model.getConcreteType
@@ -18,8 +19,8 @@ class WrappedArrayIndexRegion<ArrayType, Sort : USort>(
     private val ctx: PyContext,
     private val nullRef: UConcreteHeapRef,
 ) : UReadOnlyMemoryRegion<UArrayIndexLValue<ArrayType, Sort, KIntSort>, UAddressSort> {
-    override fun read(key: UArrayIndexLValue<ArrayType, Sort, KIntSort>): UExpr<UAddressSort> {
-        val underlyingResult = region.read(key)
+    override fun read(key: UArrayIndexLValue<ArrayType, Sort, KIntSort>, ownership: MutabilityOwnership): UExpr<UAddressSort> {
+        val underlyingResult = region.read(key, ownership)
         val array = key.ref as UConcreteHeapRef
         if (array.address > 0) {
             // allocated object
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt
index 11fdd51c16..92d5210d8e 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedArrayLengthRegion.kt
@@ -3,6 +3,7 @@ package org.usvm.machine.model.regions
 import io.ksmt.sort.KIntSort
 import org.usvm.UExpr
 import org.usvm.collection.array.length.UArrayLengthLValue
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.isTrue
 import org.usvm.machine.PyContext
 import org.usvm.machine.types.ArrayType
@@ -12,8 +13,8 @@ class WrappedArrayLengthRegion(
     private val ctx: PyContext,
     private val region: UReadOnlyMemoryRegion<UArrayLengthLValue<ArrayType, KIntSort>, KIntSort>,
 ) : UReadOnlyMemoryRegion<UArrayLengthLValue<ArrayType, KIntSort>, KIntSort> {
-    override fun read(key: UArrayLengthLValue<ArrayType, KIntSort>): UExpr<KIntSort> {
-        val underlyingResult = region.read(key)
+    override fun read(key: UArrayLengthLValue<ArrayType, KIntSort>, ownership: MutabilityOwnership): UExpr<KIntSort> {
+        val underlyingResult = region.read(key, ownership)
         if (ctx.mkArithLt(underlyingResult, ctx.mkIntNum(0)).isTrue) {
             return ctx.mkIntNum(0)
         }
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt
index fb4ed5b2ef..16ac0e336b 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefMapRegion.kt
@@ -4,6 +4,7 @@ import org.usvm.UAddressSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.collection.map.ref.URefMapEntryLValue
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.machine.PyContext
 import org.usvm.machine.types.PythonType
 import org.usvm.memory.UReadOnlyMemoryRegion
@@ -15,10 +16,10 @@ class WrappedRefMapRegion<MapType>(
     private val keys: Set<UConcreteHeapRef>,
     private val underlyingModel: UModelBase<PythonType>,
 ) : UReadOnlyMemoryRegion<URefMapEntryLValue<MapType, UAddressSort>, UAddressSort> {
-    override fun read(key: URefMapEntryLValue<MapType, UAddressSort>): UExpr<UAddressSort> {
+    override fun read(key: URefMapEntryLValue<MapType, UAddressSort>, ownership: MutabilityOwnership): UExpr<UAddressSort> {
         if (key.mapKey !in keys) {
             return underlyingModel.eval(ctx.nullRef)
         }
-        return region.read(key)
+        return region.read(key, ownership)
     }
 }
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt
index 7b5dbb7244..7b335fc0d9 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedRefSetRegion.kt
@@ -4,6 +4,7 @@ import org.usvm.UBoolSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.collection.set.ref.URefSetEntryLValue
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.PyContext
 import org.usvm.memory.UReadOnlyMemoryRegion
@@ -13,10 +14,10 @@ class WrappedRefSetRegion<SetType>(
     private val region: UReadOnlyMemoryRegion<URefSetEntryLValue<SetType>, UBoolSort>,
     private val keys: Set<UConcreteHeapRef>,
 ) : UReadOnlyMemoryRegion<URefSetEntryLValue<SetType>, UBoolSort> {
-    override fun read(key: URefSetEntryLValue<SetType>): UExpr<UBoolSort> {
+    override fun read(key: URefSetEntryLValue<SetType>, ownership: MutabilityOwnership): UExpr<UBoolSort> {
         if (!isAllocatedConcreteHeapRef(key.setRef) && key.setElement !in keys) {
             return ctx.falseExpr
         }
-        return region.read(key)
+        return region.read(key, ownership)
     }
 }
diff --git a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt
index aaa34c92df..b2cc479dea 100644
--- a/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt
+++ b/usvm-python/usvm-python-main/src/main/kotlin/org/usvm/machine/model/regions/WrappedSetRegion.kt
@@ -5,6 +5,7 @@ import io.ksmt.sort.KIntSort
 import org.usvm.UBoolSort
 import org.usvm.UExpr
 import org.usvm.collection.set.primitive.USetEntryLValue
+import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.isAllocatedConcreteHeapRef
 import org.usvm.machine.PyContext
 import org.usvm.memory.UReadOnlyMemoryRegion
@@ -15,10 +16,10 @@ class WrappedSetRegion<SetType>(
     private val region: UReadOnlyMemoryRegion<USetEntryLValue<SetType, KIntSort, USizeRegion>, UBoolSort>,
     private val keys: Set<KInterpretedValue<KIntSort>>,
 ) : UReadOnlyMemoryRegion<USetEntryLValue<SetType, KIntSort, USizeRegion>, UBoolSort> {
-    override fun read(key: USetEntryLValue<SetType, KIntSort, USizeRegion>): UExpr<UBoolSort> {
+    override fun read(key: USetEntryLValue<SetType, KIntSort, USizeRegion>, ownership: MutabilityOwnership): UExpr<UBoolSort> {
         if (!isAllocatedConcreteHeapRef(key.setRef) && key.setElement !in keys) {
             return ctx.falseExpr
         }
-        return region.read(key)
+        return region.read(key, ownership)
     }
 }
diff --git a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt
index 4904a4720e..7d923cc7cb 100644
--- a/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt
+++ b/usvm-sample-language/src/main/kotlin/org/usvm/machine/SampleState.kt
@@ -25,7 +25,7 @@ class SampleState(
     override val entrypoint: Method<*>,
     callStack: UCallStack<Method<*>, Stmt> = UCallStack(),
     pathConstraints: UPathConstraints<SampleType> = UPathConstraints(ctx, ownership),
-    memory: UMemory<SampleType, Method<*>> = UMemory(ctx, pathConstraints.typeConstraints),
+    memory: UMemory<SampleType, Method<*>> = UMemory(ctx, ownership, pathConstraints.typeConstraints),
     models: List<UModelBase<SampleType>> = listOf(),
     pathNode: PathNode<Stmt> = PathNode.root(),
     forkPoints: PathNode<PathNode<Stmt>> = PathNode.root(),
@@ -43,15 +43,17 @@ class SampleState(
     forkPoints,
     targets
 ) {
-    override fun clone(ownership: MutabilityOwnership, newConstraints: UPathConstraints<SampleType>?): SampleState {
-        val clonedConstraints = newConstraints ?: pathConstraints.clone(ownership)
+    override fun clone(newConstraints: UPathConstraints<SampleType>?): SampleState {
+        this.changeOwnership(MutabilityOwnership())
+        val cloneOwnership = MutabilityOwnership()
+        val clonedConstraints = newConstraints ?: pathConstraints.clone(cloneOwnership)
         return SampleState(
             ctx,
-            ownership,
+            cloneOwnership,
             entrypoint,
             callStack.clone(),
             clonedConstraints,
-            memory.clone(clonedConstraints.typeConstraints),
+            memory.clone(clonedConstraints.typeConstraints, cloneOwnership),
             models,
             pathNode,
             forkPoints,
@@ -76,7 +78,7 @@ class SampleState(
         val mergedCallStack = callStack.mergeWith(other.callStack, Unit) ?: return null
         val mergedPathConstraints = pathConstraints.mergeWith(other.pathConstraints, mergeGuard, ownership)
             ?: return null
-        val mergedMemory = memory.clone(mergedPathConstraints.typeConstraints).mergeWith(other.memory, mergeGuard)
+        val mergedMemory = memory.clone(mergedPathConstraints.typeConstraints, ownership).mergeWith(other.memory, mergeGuard, ownership)
             ?: return null
         val mergedModels = models + other.models
         val mergedReturnRegister = if (returnRegister == null && other.returnRegister == null) {
diff --git a/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt b/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt
index efe5545e5a..a216983104 100644
--- a/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/algorithms/PersistentMultiMapBuilder.kt
@@ -21,8 +21,8 @@ fun <K,V> UPersistentMultiMap<K,V>.addToSet(
     value: V,
     ownership: MutabilityOwnership,
 ): UPersistentMultiMap<K,V> {
-    val current = this[key]
-    val updated = current?.add(value, ownership) ?: persistentHashSetOf<V>().add(value, ownership)
+    val current = getOrDefault(key, persistentHashSetOf())
+    val updated = current.add(value, ownership)
     return this.put(key, updated, ownership)
 }
 
@@ -31,8 +31,8 @@ fun <K,V> UPersistentMultiMap<K,V>.addAll(
     values: Set<V>,
     ownership: MutabilityOwnership,
 ) : UPersistentMultiMap<K,V> {
-    val current = this[key]
-    val updated = current?.addAll(values, ownership) ?: persistentHashSetOf<V>().addAll(values, ownership)
+    val current = getOrDefault(key, persistentHashSetOf())
+    val updated = current.addAll(values, ownership)
     return this.put(key, updated, ownership)
 }
 
diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt
index 752d84614e..6a070ce91d 100644
--- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/extensions.kt
@@ -61,6 +61,8 @@ fun <K, V> persistentHashMapOf(): UPersistentHashMap<K, V> = UPersistentHashMap.
 fun <K, V> persistentHashMapOf(map : Map<K,V>, owner : MutabilityOwnership): UPersistentHashMap<K, V> =
         persistentHashMapOf<K, V>().putAll(map, owner)
 
+fun <K, V> persistentHashMapOf(owner : MutabilityOwnership, vararg pairs : Pair<K,V> ): UPersistentHashMap<K,V> =
+        pairs.fold(persistentHashMapOf<K,V>()) { acc, (k, v) -> acc.put(k, v, owner) }
 
 /**
  * Returns a persistent map containing all entries from this map.
diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt
index 321d0d841f..d0205d55f3 100644
--- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieIterator.kt
@@ -173,3 +173,6 @@ internal abstract class UPersistentHashMapBaseIterator<K, V, T>(
 
 internal class UPersistentHashMapEntriesIterator<K, V>(node: TrieNode<K, V>)
     : UPersistentHashMapBaseIterator<K, V, Map.Entry<K, V>>(node, Array(TRIE_MAX_HEIGHT + 1) { TrieNodeEntriesIterator<K, V>() })
+
+internal class UPersistentHashMapKeysIterator<K, V>(node: TrieNode<K, V>)
+    : UPersistentHashMapBaseIterator<K, V, K>(node, Array(TRIE_MAX_HEIGHT + 1) { TrieNodeKeysIterator<K, V>() })
diff --git a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt
index b9c3034538..9e6200e202 100644
--- a/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/collections/immutable/implementations/immutableMap/TrieNode.kt
@@ -716,15 +716,24 @@ class TrieNode<K, V>(
             nodePositions -= mask
         }
     }
+    
+    fun keys() = UPersistentHashMapKeysIterator(this).asSequence().toSet()
 
     fun isEmpty() = singleOrNull() == null
     fun isNotEmpty() = singleOrNull() != null
-    
+
     fun containsKey(key: K) : Boolean = containsKey(key.hashCode(), key, 0)
 
     operator fun contains(key : K) = containsKey(key)
 
     operator fun get(key : K) = get(key.hashCode(), key, 0)
+
+    fun getOrDefault(key : K, defaultValue : V) = get(key) ?: defaultValue
+    fun getOrPut(key : K, value : V, owner: MutabilityOwnership) : Pair<TrieNode<K,V>, V> { 
+        val current = get(key) ?: return put(key, value, owner) to value
+        return this to current
+    }
+
     fun put(key : K, value : V, owner: MutabilityOwnership) : TrieNode<K,V> =
         mutablePut(key.hashCode(), key, value, 0, owner)
 
diff --git a/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt b/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt
index be61e46e36..f41dc17cda 100644
--- a/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt
+++ b/usvm-util/src/main/kotlin/org/usvm/regions/RegionTree.kt
@@ -58,7 +58,7 @@ class RegionTree<Reg, Value>(
                 // fixme: here we might have a deep recursion, maybe we should rewrite it
                 entry.second.splitRecursively(region, filterPredicate).completelyCoveredRegionTree
             }
-            val outside = entries.remove(region)
+            val outside = entries.remove(region)    
             val disjointRegionTree = RegionTree(outside)
 
             return RecursiveSplitResult(completelyCoveredRegionTree, disjointRegionTree)