diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
index 012702dbb..3b45d71f3 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt
@@ -2,6 +2,7 @@ package org.usvm.machine
 
 import io.ksmt.sort.KFp64Sort
 import io.ksmt.utils.asExpr
+import org.jacodb.ets.base.EtsAnyType
 import org.jacodb.ets.base.EtsBooleanType
 import org.jacodb.ets.base.EtsNullType
 import org.jacodb.ets.base.EtsNumberType
@@ -19,10 +20,13 @@ import org.usvm.UContext
 import org.usvm.UExpr
 import org.usvm.USort
 import org.usvm.collection.field.UFieldLValue
+import org.usvm.isTrue
 import org.usvm.machine.expr.TsUndefinedSort
 import org.usvm.machine.expr.TsUnresolvedSort
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.types.FakeType
+import org.usvm.types.single
+import org.usvm.util.mkFieldLValue
 import kotlin.contracts.ExperimentalContracts
 import kotlin.contracts.contract
 
@@ -51,6 +55,7 @@ class TsContext(
         is EtsUndefinedType -> addressSort
         is EtsUnknownType -> unresolvedSort
         is EtsUnionType -> unresolvedSort
+        is EtsAnyType -> unresolvedSort
         else -> TODO("Support all JacoDB types, encountered $type")
     }
 
@@ -70,7 +75,7 @@ class TsContext(
 
         val ref = createFakeObjectRef()
 
-        scope.calcOnState {
+        scope.doWithState {
             when (sort) {
                 boolSort -> {
                     val lvalue = getIntermediateBoolLValue(ref.address)
@@ -86,8 +91,8 @@ class TsContext(
 
                 addressSort -> {
                     val lValue = getIntermediateRefLValue(ref.address)
-                    memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext))
                     memory.write(lValue, this@toFakeObject.asExpr(addressSort), guard = trueExpr)
+                    memory.types.allocate(ref.address, FakeType.fromRef(this@TsContext))
                 }
 
                 else -> TODO("Not yet supported")
@@ -97,6 +102,35 @@ class TsContext(
         return ref
     }
 
+    fun UExpr<out USort>.extractSingleValueFromFakeObjectOrNull(scope: TsStepScope): UExpr<out USort>? {
+        if (!isFakeObject()) return null
+
+        val type = scope.calcOnState {
+            memory.types.getTypeStream(this@extractSingleValueFromFakeObjectOrNull).single() as FakeType
+        }
+
+        return scope.calcOnState {
+            when {
+                type.boolTypeExpr.isTrue -> {
+                    val lValue = getIntermediateBoolLValue(address)
+                    memory.read(lValue).asExpr(boolSort)
+                }
+
+                type.fpTypeExpr.isTrue -> {
+                    val lValue = getIntermediateFpLValue(address)
+                    memory.read(lValue).asExpr(fp64Sort)
+                }
+
+                type.refTypeExpr.isTrue -> {
+                    val lValue = getIntermediateRefLValue(address)
+                    memory.read(lValue).asExpr(addressSort)
+                }
+
+                else -> null
+            }
+        }
+    }
+
     fun createFakeObjectRef(): UConcreteHeapRef {
         val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET
         return mkConcreteHeapRef(address)
@@ -108,15 +142,15 @@ class TsContext(
     private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
 
     fun getIntermediateBoolLValue(addr: Int): UFieldLValue<IntermediateLValueField, UBoolSort> {
-        return UFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL)
+        return mkFieldLValue(boolSort, mkConcreteHeapRef(addr), IntermediateLValueField.BOOL)
     }
 
     fun getIntermediateFpLValue(addr: Int): UFieldLValue<IntermediateLValueField, KFp64Sort> {
-        return UFieldLValue(fp64Sort, mkConcreteHeapRef(addr), IntermediateLValueField.FP)
+        return mkFieldLValue(fp64Sort, mkConcreteHeapRef(addr), IntermediateLValueField.FP)
     }
 
     fun getIntermediateRefLValue(addr: Int): UFieldLValue<IntermediateLValueField, UAddressSort> {
-        return UFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF)
+        return mkFieldLValue(addressSort, mkConcreteHeapRef(addr), IntermediateLValueField.REF)
     }
 }
 
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
index 8213ad375..4f23e58ed 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt
@@ -74,29 +74,28 @@ import org.jacodb.ets.model.EtsField
 import org.jacodb.ets.model.EtsFieldSignature
 import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.utils.getDeclaredLocals
 import org.usvm.UAddressSort
 import org.usvm.UBoolSort
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.api.allocateArray
-import org.usvm.api.makeSymbolicPrimitive
-import org.usvm.collection.array.UArrayIndexLValue
-import org.usvm.collection.array.length.UArrayLengthLValue
-import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.machine.operator.TsBinaryOperator
 import org.usvm.machine.operator.TsUnaryOperator
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
-import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
-import org.usvm.machine.types.FakeType
 import org.usvm.machine.types.mkFakeValue
 import org.usvm.memory.ULValue
-import org.usvm.memory.URegisterStackLValue
 import org.usvm.sizeSort
+import org.usvm.util.fieldLookUp
+import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.mkFieldLValue
+import org.usvm.util.mkRegisterStackLValue
 import org.usvm.util.throwExceptionWithoutStackFrameDrop
 
 private val logger = KotlinLogging.logger {}
@@ -415,7 +414,7 @@ class TsExprResolver(
                 pushSortsForArguments(expr.instance, expr.args, localToIdx)
 
                 callStack.push(method, currentStatement)
-                memory.stack.push(args.toTypedArray(), method.localsCount)
+                memory.stack.push(args.toTypedArray(), method.getDeclaredLocals().size)
 
                 newStmt(method.cfg.stmts.first())
             }
@@ -541,7 +540,12 @@ class TsExprResolver(
             isSigned = true
         )
 
-        val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, value.array.type)
+        val lValue = mkArrayIndexLValue(
+            addressSort,
+            instance,
+            bvIndex.asExpr(ctx.sizeSort),
+            value.array.type as EtsArrayType
+        )
         val expr = scope.calcOnState { memory.read(lValue) }
 
         check(expr.isFakeObject()) { "Only fake objects are allowed in arrays" }
@@ -599,7 +603,7 @@ class TsExprResolver(
 
         // TODO It is a hack for array's length
         if (value.instance.type is EtsArrayType && value.field.name == "length") {
-            val lValue = UArrayLengthLValue(instanceRef, value.instance.type, ctx.sizeSort)
+            val lValue = mkArrayLengthLValue(instanceRef, value.instance.type as EtsArrayType)
             val expr = scope.calcOnState { memory.read(lValue) }
 
             check(expr.sort == ctx.sizeSort)
@@ -612,6 +616,33 @@ class TsExprResolver(
         val lValue = UFieldLValue(sort, instanceRef, value.field.name)
         val expr = scope.calcOnState { memory.read(lValue) }
 
+        val expr = if (sort == unresolvedSort) {
+            val boolLValue = mkFieldLValue(boolSort, instanceRef, value.field)
+            val fpLValue = mkFieldLValue(fp64Sort, instanceRef, value.field)
+            val refLValue = mkFieldLValue(addressSort, instanceRef, value.field)
+
+            scope.calcOnState {
+                val bool = memory.read(boolLValue)
+                val fp = memory.read(fpLValue)
+                val ref = memory.read(refLValue)
+
+                // If a fake object is already created and assigned to the field,
+                // there is no need to recreate another one
+                val fakeRef = if (ref.isFakeObject()) {
+                    ref
+                } else {
+                    mkFakeValue(scope, bool, fp, ref)
+                }
+
+                memory.write(refLValue, fakeRef.asExpr(addressSort), guard = trueExpr)
+
+                fakeRef
+            }
+        } else {
+            val lValue = mkFieldLValue(sort, instanceRef, value.field)
+            scope.calcOnState { memory.read(lValue) }
+        }
+
         if (assertIsSubtype(expr, value.type)) {
             expr
         } else {
@@ -706,20 +737,20 @@ class TsSimpleValueResolver(
         // If we are not in the entrypoint, all correct values are already resolved and we can just return
         // a registerStackLValue for the local
         if (currentMethod != entrypoint) {
-            return URegisterStackLValue(sort, localIdx)
+            return mkRegisterStackLValue(sort, localIdx)
         }
 
         // arguments and this for the first stack frame
         return when (sort) {
-            is UBoolSort -> URegisterStackLValue(sort, localIdx)
-            is KFp64Sort -> URegisterStackLValue(sort, localIdx)
-            is UAddressSort -> URegisterStackLValue(sort, localIdx)
+            is UBoolSort -> mkRegisterStackLValue(sort, localIdx)
+            is KFp64Sort -> mkRegisterStackLValue(sort, localIdx)
+            is UAddressSort -> mkRegisterStackLValue(sort, localIdx)
             is TsUnresolvedSort -> {
                 check(local is EtsThis || local is EtsParameterRef) {
                     "Only This and ParameterRef are expected here"
                 }
 
-                val lValue = URegisterStackLValue(ctx.addressSort, localIdx)
+                val lValue = mkRegisterStackLValue(ctx.addressSort, localIdx)
 
                 val boolRValue = ctx.mkRegisterReading(localIdx, ctx.boolSort)
                 val fpRValue = ctx.mkRegisterReading(localIdx, ctx.fp64Sort)
@@ -728,15 +759,6 @@ class TsSimpleValueResolver(
                 val fakeObject = ctx.mkFakeValue(scope, boolRValue, fpRValue, refRValue)
                 scope.calcOnState {
                     with(ctx) {
-                        val type = FakeType(
-                            boolTypeExpr = makeSymbolicPrimitive(boolSort),
-                            fpTypeExpr = makeSymbolicPrimitive(boolSort),
-                            refTypeExpr = makeSymbolicPrimitive(boolSort)
-                        )
-
-                        scope.assert(type.mkExactlyOneTypeConstraint(ctx))
-
-                        memory.types.allocate(fakeObject.address, type)
                         memory.write(lValue, fakeObject.asExpr(addressSort), guard = trueExpr)
                     }
                 }
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
index 56b52981c..44c201a71 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt
@@ -3,10 +3,12 @@ package org.usvm.machine.interpreter
 import io.ksmt.utils.asExpr
 import mu.KotlinLogging
 import org.jacodb.ets.base.EtsArrayAccess
+import org.jacodb.ets.base.EtsArrayType
 import org.jacodb.ets.base.EtsAssignStmt
 import org.jacodb.ets.base.EtsCallStmt
 import org.jacodb.ets.base.EtsGotoStmt
 import org.jacodb.ets.base.EtsIfStmt
+import org.jacodb.ets.base.EtsInstanceFieldRef
 import org.jacodb.ets.base.EtsLocal
 import org.jacodb.ets.base.EtsNopStmt
 import org.jacodb.ets.base.EtsNullType
@@ -19,12 +21,11 @@ import org.jacodb.ets.base.EtsThrowStmt
 import org.jacodb.ets.base.EtsType
 import org.jacodb.ets.base.EtsValue
 import org.jacodb.ets.model.EtsMethod
+import org.jacodb.ets.utils.getDeclaredLocals
 import org.usvm.StepResult
 import org.usvm.StepScope
 import org.usvm.UInterpreter
 import org.usvm.api.targets.TsTarget
-import org.usvm.collection.array.UArrayIndexLValue
-import org.usvm.collection.array.length.UArrayLengthLValue
 import org.usvm.collections.immutable.internal.MutabilityOwnership
 import org.usvm.forkblacklists.UForkBlackList
 import org.usvm.machine.TsApplicationGraph
@@ -34,13 +35,15 @@ import org.usvm.machine.expr.mkTruthyExpr
 import org.usvm.machine.state.TsMethodResult
 import org.usvm.machine.state.TsState
 import org.usvm.machine.state.lastStmt
-import org.usvm.machine.state.localsCount
 import org.usvm.machine.state.newStmt
 import org.usvm.machine.state.parametersWithThisCount
 import org.usvm.machine.state.returnValue
-import org.usvm.memory.URegisterStackLValue
 import org.usvm.sizeSort
 import org.usvm.targets.UTargetsSet
+import org.usvm.util.mkArrayIndexLValue
+import org.usvm.util.mkArrayLengthLValue
+import org.usvm.util.mkFieldLValue
+import org.usvm.util.mkRegisterStackLValue
 import org.usvm.utils.ensureSat
 
 private val logger = KotlinLogging.logger {}
@@ -139,7 +142,7 @@ class TsInterpreter(
                     val idx = mapLocalToIdx(lastEnteredMethod, lhv)
                     saveSortForLocal(idx, expr.sort)
 
-                    val lValue = URegisterStackLValue(expr.sort, idx)
+                    val lValue = mkRegisterStackLValue(expr.sort, idx)
                     memory.write(lValue, expr.asExpr(lValue.sort), guard = trueExpr)
                 }
 
@@ -155,7 +158,7 @@ class TsInterpreter(
                         isSigned = true
                     ).asExpr(sizeSort)
 
-                    val lengthLValue = UArrayLengthLValue(instance, lhv.array.type, sizeSort)
+                    val lengthLValue = mkArrayLengthLValue(instance, lhv.array.type as EtsArrayType)
                     val currentLength = memory.read(lengthLValue).asExpr(sizeSort)
 
                     val condition = mkBvSignedGreaterOrEqualExpr(bvIndex, currentLength)
@@ -165,10 +168,29 @@ class TsInterpreter(
 
                     val fakeExpr = expr.toFakeObject(scope)
 
-                    val lValue = UArrayIndexLValue(addressSort, instance, bvIndex, lhv.array.type)
+                    val lValue = mkArrayIndexLValue(
+                        addressSort,
+                        instance,
+                        bvIndex.asExpr(sizeSort),
+                        lhv.array.type as EtsArrayType
+                    )
                     memory.write(lValue, fakeExpr, guard = trueExpr)
                 }
 
+                is EtsInstanceFieldRef -> {
+                    val instance = exprResolver.resolve(lhv.instance)?.asExpr(addressSort) ?: return@doWithState
+
+                    val sort = typeToSort(lhv.type)
+                    if (sort == unresolvedSort) {
+                        val fakeObject = expr.toFakeObject(scope)
+                        val lValue = mkFieldLValue(addressSort, instance, lhv.field)
+                        memory.write(lValue, fakeObject, guard = trueExpr)
+                    } else {
+                        val lValue = mkFieldLValue(sort, instance, lhv.field)
+                        memory.write(lValue, expr.asExpr(sort), guard = trueExpr)
+                    }
+                }
+
                 else -> TODO("Not yet implemented")
             }
 
@@ -239,7 +261,8 @@ class TsInterpreter(
 
         val solver = ctx.solver<EtsType>()
 
-        val thisInstanceRef = URegisterStackLValue(ctx.addressSort, method.parameters.count()) // TODO check for statics
+        // TODO check for statics
+        val thisInstanceRef = mkRegisterStackLValue(ctx.addressSort, method.parameters.count())
         val thisRef = state.memory.read(thisInstanceRef).asExpr(ctx.addressSort)
 
         state.pathConstraints += with(ctx) {
@@ -259,7 +282,7 @@ class TsInterpreter(
         state.models = listOf(model)
 
         state.callStack.push(method, returnSite = null)
-        state.memory.stack.push(method.parametersWithThisCount, method.localsCount)
+        state.memory.stack.push(method.parametersWithThisCount, method.getDeclaredLocals().size)
         state.newStmt(method.cfg.instructions.first())
 
         state.memory.types.allocate(ctx.mkTsNullValue().address, EtsNullType)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
index b114efb70..3e627fb2b 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt
@@ -56,21 +56,24 @@ sealed interface TsBinaryOperator {
         rhs: UExpr<out USort>,
         scope: TsStepScope,
     ): UExpr<out USort> {
-        if (lhs.isFakeObject() || rhs.isFakeObject()) {
-            return resolveFakeObject(lhs, rhs, scope)
+        val lhsValue = lhs.extractSingleValueFromFakeObjectOrNull(scope) ?: lhs
+        val rhsValue = rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs
+
+        if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) {
+            return resolveFakeObject(lhsValue, rhsValue, scope)
         }
 
-        val lhsSort = lhs.sort
-        if (lhsSort == rhs.sort) {
+        val lhsSort = lhsValue.sort
+        if (lhsSort == rhsValue.sort) {
             return when (lhsSort) {
-                boolSort -> onBool(lhs.asExpr(boolSort), rhs.asExpr(boolSort), scope)
-                fp64Sort -> onFp(lhs.asExpr(fp64Sort), rhs.asExpr(fp64Sort), scope)
-                addressSort -> onRef(lhs.asExpr(addressSort), rhs.asExpr(addressSort), scope)
+                boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope)
+                fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope)
+                addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope)
                 else -> TODO("Unsupported sort $lhsSort")
             }
         }
 
-        return internalResolve(lhs, rhs, scope)
+        return internalResolve(lhsValue, rhsValue, scope)
     }
 
     data object Eq : TsBinaryOperator {
diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt
index 4f42e7602..cb26e5633 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/FakeExprUtil.kt
@@ -7,6 +7,7 @@ import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
 import org.usvm.UHeapRef
 import org.usvm.USort
+import org.usvm.api.makeSymbolicPrimitive
 import org.usvm.api.typeStreamOf
 import org.usvm.collection.field.UFieldLValue
 import org.usvm.machine.IntermediateLValueField
@@ -30,12 +31,23 @@ fun TsContext.mkFakeValue(
         val fakeValueRef = createFakeObjectRef()
         val address = fakeValueRef.address
 
+        val boolTypeExpr = trueExpr
+            .takeIf { boolValue != null && fpValue == null && refValue == null }
+            ?: makeSymbolicPrimitive(boolSort)
+        val fpTypeExpr = trueExpr
+            .takeIf { boolValue == null && fpValue != null && refValue == null }
+            ?: makeSymbolicPrimitive(boolSort)
+        val refTypeExpr = trueExpr
+            .takeIf { boolValue == null && fpValue == null && refValue != null }
+            ?: makeSymbolicPrimitive(boolSort)
+
         val type = FakeType(
-            boolTypeExpr = mkBool(boolValue != null),
-            fpTypeExpr = mkBool(fpValue != null),
-            refTypeExpr = mkBool(refValue != null),
+            boolTypeExpr = boolTypeExpr,
+            fpTypeExpr = fpTypeExpr,
+            refTypeExpr = refTypeExpr,
         )
         memory.types.allocate(address, type)
+        scope.assert(type.mkExactlyOneTypeConstraint(ctx))
 
         if (boolValue != null) {
             val boolLValue = ctx.getIntermediateBoolLValue(address)
diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt
new file mode 100644
index 000000000..08c33868f
--- /dev/null
+++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt
@@ -0,0 +1,44 @@
+package org.usvm.util
+
+import org.jacodb.ets.base.EtsArrayType
+import org.jacodb.ets.model.EtsFieldSignature
+import org.usvm.UExpr
+import org.usvm.UHeapRef
+import org.usvm.USort
+import org.usvm.collection.array.UArrayIndexLValue
+import org.usvm.collection.array.length.UArrayLengthLValue
+import org.usvm.collection.field.UFieldLValue
+import org.usvm.machine.IntermediateLValueField
+import org.usvm.machine.TsSizeSort
+import org.usvm.machine.expr.tctx
+import org.usvm.memory.URegisterStackLValue
+import org.usvm.sizeSort
+
+fun <Sort : USort> mkFieldLValue(
+    sort: Sort,
+    ref: UHeapRef,
+    field: IntermediateLValueField,
+): UFieldLValue<IntermediateLValueField, Sort> = UFieldLValue(sort, ref, field)
+
+fun <Sort : USort> mkFieldLValue(
+    sort: Sort,
+    ref: UHeapRef,
+    field: EtsFieldSignature,
+): UFieldLValue<String, Sort> = UFieldLValue(sort, ref, field.name)
+
+fun <Sort : USort> mkArrayIndexLValue(
+    sort: Sort,
+    ref: UHeapRef,
+    index: UExpr<TsSizeSort>,
+    type: EtsArrayType,
+): UArrayIndexLValue<EtsArrayType, Sort, TsSizeSort> = UArrayIndexLValue(sort, ref, index, type)
+
+fun mkArrayLengthLValue(
+    ref: UHeapRef,
+    type: EtsArrayType,
+): UArrayLengthLValue<EtsArrayType, TsSizeSort> = UArrayLengthLValue(ref, type, ref.tctx.sizeSort)
+
+fun <Sort : USort> mkRegisterStackLValue(
+    sort: Sort,
+    idx: Int,
+): URegisterStackLValue<Sort> = URegisterStackLValue(sort, idx)
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt
new file mode 100644
index 000000000..97a92351e
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/Objects.kt
@@ -0,0 +1,58 @@
+package org.usvm.samples
+
+import org.jacodb.ets.model.EtsScene
+import org.usvm.api.TsValue
+import org.usvm.util.TsMethodTestRunner
+import kotlin.test.Test
+
+class Objects : TsMethodTestRunner() {
+    private val className = this::class.simpleName!!
+
+    override val scene: EtsScene = loadSampleScene(className)
+
+    @Test
+    fun testCreateClassInstance() {
+        val method = getMethod("Example", "createClassInstance")
+        discoverProperties<TsValue.TsNumber>(
+            method = method,
+            { r -> r.number == 5.0 }
+        )
+    }
+
+    @Test
+    fun testCreateClassInstanceAndWriteField() {
+        val method = getMethod("Example", "createClassInstanceAndWriteField")
+        discoverProperties<TsValue.TsClass>(
+            method = method,
+            { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 14.0 }
+        )
+    }
+
+    @Test
+    fun testCreateClassInstanceAndWriteValueOfAnotherType() {
+        val method = getMethod("Example", "createClassInstanceAndWriteValueOfAnotherType")
+        discoverProperties<TsValue.TsClass>(
+            method = method,
+            { r -> r.properties.toList().single().second is TsValue.TsNull }
+        )
+    }
+
+    @Test
+    fun testCreateAnonymousClass() {
+        val method = getMethod("Example", "createAnonymousClass")
+        discoverProperties<TsValue.TsClass>(
+            method = method,
+            { r -> (r.properties.toList().single().second as TsValue.TsNumber).number == 15.0 }
+        )
+    }
+
+    @Test
+    fun testReadFieldValue() {
+        val method = getMethod("Example", "readFieldValue")
+        discoverProperties<TsValue.TsClass, TsValue.TsNumber>(
+            method = method,
+            { x, r -> (x.properties.values.single() as TsValue.TsNumber).number == 1.1 && r.number == 14.0 },
+            { x, r -> (x.properties.values.single() as? TsValue.TsNumber)?.number != 1.1 && r.number == 10.0 }
+        )
+    }
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
index f5bc1209b..75a5db88c 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt
@@ -25,6 +25,7 @@ import org.jacodb.ets.model.EtsMethodSignature
 import org.usvm.UAddressSort
 import org.usvm.UConcreteHeapRef
 import org.usvm.UExpr
+import org.usvm.UHeapRef
 import org.usvm.USort
 import org.usvm.api.GlobalFieldValue
 import org.usvm.api.TsParametersState
@@ -66,7 +67,7 @@ class TsTestResolver {
 
             is TsMethodResult.Success -> {
                 afterMemoryScope.withMode(ResolveMode.CURRENT) {
-                    resolveExpr(res.value, method.returnType)
+                    resolveExpr(res.value, res.value, method.returnType)
                 }
             }
 
@@ -115,64 +116,88 @@ open class TsTestStateResolver(
 ) {
     fun resolveLValue(lValue: ULValue<*, *>, type: EtsType): TsValue {
         val expr = memory.read(lValue)
-        return resolveExpr(expr, type)
+        val symbolicRef =
+            if (lValue.sort is UAddressSort) finalStateMemory.read(lValue).asExpr(ctx.addressSort) else null
+        return resolveExpr(expr, symbolicRef, type)
     }
 
     fun resolveExpr(
         expr: UExpr<out USort>,
+        symbolicRef: UExpr<out USort>? = null,
         type: EtsType,
     ): TsValue = when (type) {
         is EtsPrimitiveType -> resolvePrimitive(expr, type)
-        is EtsRefType -> resolveRef(expr.asExpr(ctx.addressSort), type)
-        else -> resolveUnknownExpr(expr)
+
+        is EtsRefType -> resolveRef(
+            expr.asExpr(ctx.addressSort),
+            symbolicRef?.asExpr(ctx.addressSort) ?: expr.asExpr(ctx.addressSort),
+            type
+        )
+
+        else -> resolveUnknownExpr(expr, symbolicRef)
     }
 
-    fun resolveUnknownExpr(expr: UExpr<out USort>): TsValue = with(expr.tctx) {
-        when (expr.sort) {
-            fp64Sort -> resolvePrimitive(expr, EtsNumberType)
-            boolSort -> resolvePrimitive(expr, EtsBooleanType)
-            addressSort -> {
-                if (expr.isFakeObject()) {
-                    resolveFakeObject(expr)
-                } else {
-                    resolveRef(expr.asExpr(ctx.addressSort), EtsUnknownType)
+    fun resolveUnknownExpr(heapRef: UExpr<out USort>, finalStateMemoryRef: UExpr<out USort>?): TsValue =
+        with(heapRef.tctx) {
+            when (heapRef.sort) {
+                fp64Sort -> resolvePrimitive(heapRef, EtsNumberType)
+                boolSort -> resolvePrimitive(heapRef, EtsBooleanType)
+                addressSort -> {
+                    if (heapRef.isFakeObject()) {
+                        resolveFakeObject(heapRef)
+                    } else {
+                        resolveRef(
+                            heapRef.asExpr(ctx.addressSort),
+                            finalStateMemoryRef?.asExpr(ctx.addressSort),
+                            EtsUnknownType
+                        )
+                    }
                 }
-            }
 
-            else -> TODO()
+                else -> TODO("Unsupported sort: ${heapRef.sort}")
+            }
         }
-    }
 
-    private fun resolveRef(expr: UExpr<UAddressSort>, type: EtsType): TsValue {
-        val instance = model.eval(expr) as UConcreteHeapRef
+    private fun resolveRef(
+        heapRef: UExpr<UAddressSort>,
+        finalStateMemoryRef: UExpr<UAddressSort>?,
+        type: EtsType,
+    ): TsValue {
+        val concreteRef = evaluateInModel(heapRef) as UConcreteHeapRef
 
-        if (instance.address == 0) {
+        if (concreteRef.address == 0) {
             return TsValue.TsUndefined
         }
 
-        if (model.eval(ctx.mkHeapRefEq(expr, ctx.mkTsNullValue())).isTrue) {
+        if (model.eval(ctx.mkHeapRefEq(heapRef, ctx.mkTsNullValue())).isTrue) {
             return TsValue.TsNull
         }
 
         return when (type) {
-            is EtsClassType -> resolveClass(instance, type)
-            is EtsArrayType -> resolveArray(instance, type)
+            is EtsClassType -> resolveClass(concreteRef, finalStateMemoryRef ?: heapRef, type)
+
+            is EtsArrayType -> resolveArray(concreteRef, finalStateMemoryRef ?: heapRef, type)
+
             is EtsUnknownType -> {
-                val type = finalStateMemory.types.getTypeStream(expr).first()
-                resolveRef(expr, type)
+                val type = finalStateMemory.types.getTypeStream(heapRef).first()
+                resolveRef(heapRef, finalStateMemoryRef, type)
             }
 
             else -> error("Unexpected type: $type")
         }
     }
 
-    private fun resolveArray(expr: UConcreteHeapRef, type: EtsArrayType): TsValue.TsArray<*> {
-        val arrayLengthLValue = UArrayLengthLValue(expr, type, ctx.sizeSort)
+    private fun resolveArray(
+        concreteRef: UConcreteHeapRef,
+        heapRef: UHeapRef,
+        type: EtsArrayType,
+    ): TsValue.TsArray<*> {
+        val arrayLengthLValue = UArrayLengthLValue(heapRef, type, ctx.sizeSort)
         val length = model.eval(memory.read(arrayLengthLValue)) as KBitVec32Value
 
         val values = (0 until length.intValue).map {
             val index = ctx.mkSizeExpr(it)
-            val lValue = UArrayIndexLValue(ctx.addressSort, expr, index, type)
+            val lValue = UArrayIndexLValue(ctx.addressSort, heapRef, index, type)
             val value = memory.read(lValue)
 
             if (model.eval(ctx.mkHeapRefEq(value, ctx.mkUndefinedValue())).isTrue) {
@@ -223,7 +248,7 @@ open class TsTestStateResolver(
                 // Note that everything about details of fake object we need to read from final state of the memory
                 // since they are allocated objects
                 val value = finalStateMemory.read(lValue)
-                resolveExpr(model.eval(value), EtsBooleanType)
+                resolveExpr(model.eval(value), value, EtsBooleanType)
             }
 
             model.eval(type.fpTypeExpr).isTrue -> {
@@ -231,7 +256,7 @@ open class TsTestStateResolver(
                 // Note that everything about details of fake object we need to read from final state of the memory
                 // since they are allocated objects
                 val value = finalStateMemory.read(lValue)
-                resolveExpr(model.eval(value), EtsNumberType)
+                resolveExpr(model.eval(value), value, EtsNumberType)
             }
 
             model.eval(type.refTypeExpr).isTrue -> {
@@ -241,7 +266,7 @@ open class TsTestStateResolver(
                 val value = finalStateMemory.read(lValue)
                 val ref = model.eval(value)
                 // TODO mistake with signature, use TypeStream instead
-                resolveExpr(ref, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature))
+                resolveExpr(ref, value, EtsClassType(ctx.scene.projectAndSdkClasses.first().signature))
             }
 
             else -> error("Unsupported")
@@ -264,22 +289,10 @@ open class TsTestStateResolver(
     }
 
     private fun resolveClass(
-        expr: UExpr<out USort>,
+        concreteRef: UConcreteHeapRef,
+        heapRef: UHeapRef,
         classType: EtsClassType,
     ): TsValue {
-        if (expr is UConcreteHeapRef && expr.address == 0) {
-            return TsValue.TsUndefined
-        }
-
-        val nullRef = ctx.mkTsNullValue()
-        if (model.eval(ctx.mkHeapRefEq(expr.asExpr(ctx.addressSort), nullRef)).isTrue) {
-            return TsValue.TsNull
-        }
-
-        check(expr.sort == ctx.addressSort) {
-            "Expected address sort, but got ${expr.sort}"
-        }
-
         val clazz = ctx.scene.projectAndSdkClasses.firstOrNull { it.signature == classType.signature }
             ?: if (classType.signature.name == "Object") {
                 EtsClassImpl(
@@ -301,9 +314,20 @@ open class TsTestStateResolver(
 
         val properties = clazz.fields.associate { field ->
             val sort = ctx.typeToSort(field.type)
-            val lValue = UFieldLValue(sort, expr.asExpr(ctx.addressSort), field.name)
+
+            if (sort == ctx.unresolvedSort) {
+                val lValue = UFieldLValue(ctx.addressSort, heapRef, field.name)
+                val fieldExpr = finalStateMemory.read(lValue) as? UConcreteHeapRef
+                    ?: error("UnresolvedSort should be represented by a fake object instance")
+
+                // TODO check values
+                return@associate field.name to resolveExpr(fieldExpr, fieldExpr, field.type)
+            }
+
+            val lValue = UFieldLValue(sort, concreteRef.asExpr(ctx.addressSort), field.name)
             val fieldExpr = memory.read(lValue)
-            val obj = resolveExpr(fieldExpr, field.type)
+            // TODO check values
+            val obj = resolveExpr(fieldExpr, fieldExpr, field.type)
             field.name to obj
         }
         return TsValue.TsClass(clazz.name, properties)
diff --git a/usvm-ts/src/test/resources/samples/Objects.ts b/usvm-ts/src/test/resources/samples/Objects.ts
new file mode 100644
index 000000000..72e2f3fcb
--- /dev/null
+++ b/usvm-ts/src/test/resources/samples/Objects.ts
@@ -0,0 +1,43 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
+class SimpleClass {
+    x: any = 5;
+}
+
+class Example {
+    createClassInstance() {
+        let x = new SimpleClass();
+        return x.x;
+    }
+
+    createClassInstanceAndWriteField() {
+        let x = new SimpleClass();
+        x.x = 14;
+
+        return x;
+    }
+
+    createClassInstanceAndWriteValueOfAnotherType() {
+        let x = new SimpleClass();
+        x.x = true;
+
+        if (x.x === true) {
+            x.x = null
+        }
+
+        return x;
+    }
+
+    createAnonymousClass() {
+        return {a: 15};
+    }
+
+    readFieldValue(x: SimpleClass) {
+        if (x.x === 1.1) {
+            return 14
+        }
+
+        return 10
+    }
+}