diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
index 74be6469e5..be073618a3 100644
--- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
+++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ExprUtil.kt
@@ -91,7 +91,19 @@ fun TsContext.mkTruthyExpr(
 fun TsContext.mkNumericExpr(
     expr: UExpr<out USort>,
     scope: TsStepScope,
-): UExpr<KFp64Sort> = scope.calcOnState {
+): UExpr<KFp64Sort> {
+    if (expr.isFakeObject()) {
+        val type = expr.getFakeType(scope)
+        return mkIte(
+            condition = type.fpTypeExpr,
+            trueBranch = expr.extractFp(scope),
+            falseBranch = mkIte(
+                condition = type.boolTypeExpr,
+                trueBranch = mkNumericExpr(expr.extractBool(scope), scope),
+                falseBranch = mkNumericExpr(expr.extractRef(scope), scope)
+            )
+        )
+    }
 
     // 7.1.4 ToNumber ( argument )
     //
@@ -107,19 +119,19 @@ fun TsContext.mkNumericExpr(
     // 10. Return ToNumber(primValue).
 
     if (expr.sort == fp64Sort) {
-        return@calcOnState expr.asExpr(fp64Sort)
+        return expr.asExpr(fp64Sort)
     }
 
     if (expr == mkUndefinedValue()) {
-        return@calcOnState mkFp64NaN()
+        return mkFp64NaN()
     }
 
     if (expr == mkTsNullValue()) {
-        return@calcOnState mkFp64(0.0)
+        return mkFp64(0.0)
     }
 
     if (expr.sort == boolSort) {
-        return@calcOnState boolToFp(expr.asExpr(boolSort))
+        return boolToFp(expr.asExpr(boolSort))
     }
 
     // TODO: ToPrimitive, then ToNumber again
@@ -127,7 +139,7 @@ fun TsContext.mkNumericExpr(
 
     // TODO incorrect implementation, returns some number that is not equal to 0 and NaN
     //      https://github.com/UnitTestBot/usvm/issues/280
-    return@calcOnState mkIte(
+    return mkIte(
         condition = mkEq(expr.asExpr(addressSort), mkTsNullValue()),
         trueBranch = mkFp(0.0, fp64Sort),
         falseBranch = mkIte(
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 dde7a449be..1b4d85f3d8 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
@@ -332,13 +332,11 @@ class TsExprResolver(
     }
 
     override fun visit(expr: EtsDivExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        return resolveBinaryOperator(TsBinaryOperator.Div, expr)
     }
 
     override fun visit(expr: EtsRemExpr): UExpr<out USort>? {
-        logger.warn { "visit(${expr::class.simpleName}) is not implemented yet" }
-        error("Not supported $expr")
+        return resolveBinaryOperator(TsBinaryOperator.Rem, expr)
     }
 
     override fun visit(expr: EtsExpExpr): UExpr<out USort>? {
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 abd648eda7..722f86f07b 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
@@ -1217,7 +1217,7 @@ sealed interface TsBinaryOperator {
             lhs: UBoolExpr,
             rhs: UBoolExpr,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
@@ -1227,7 +1227,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<KFp64Sort>,
             rhs: UExpr<KFp64Sort>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
         }
 
@@ -1235,7 +1235,7 @@ sealed interface TsBinaryOperator {
             lhs: UHeapRef,
             rhs: UHeapRef,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
@@ -1245,7 +1245,7 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             check(lhs.isFakeObject() || rhs.isFakeObject())
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
@@ -1256,11 +1256,105 @@ sealed interface TsBinaryOperator {
             lhs: UExpr<*>,
             rhs: UExpr<*>,
             scope: TsStepScope,
-        ): UExpr<*> {
+        ): UExpr<KFp64Sort> {
             check(!lhs.isFakeObject() && !rhs.isFakeObject())
             val left = mkNumericExpr(lhs, scope)
             val right = mkNumericExpr(rhs, scope)
             return mkFpMulExpr(fpRoundingModeSortDefaultValue(), left, right)
         }
     }
+
+    data object Div : TsBinaryOperator {
+        override fun TsContext.onBool(
+            lhs: UBoolExpr,
+            rhs: UBoolExpr,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+
+        override fun TsContext.onFp(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), lhs, rhs)
+        }
+
+        override fun TsContext.onRef(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+
+        override fun TsContext.resolveFakeObject(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+
+        override fun TsContext.internalResolve(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val left = mkNumericExpr(lhs, scope)
+            val right = mkNumericExpr(rhs, scope)
+            return mkFpDivExpr(fpRoundingModeSortDefaultValue(), left, right)
+        }
+    }
+
+    data object Rem : TsBinaryOperator {
+        override fun TsContext.onBool(
+            lhs: UBoolExpr,
+            rhs: UBoolExpr,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.onFp(
+            lhs: UExpr<KFp64Sort>,
+            rhs: UExpr<KFp64Sort>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.onRef(
+            lhs: UHeapRef,
+            rhs: UHeapRef,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.resolveFakeObject(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            return internalResolve(lhs, rhs, scope)
+        }
+
+        override fun TsContext.internalResolve(
+            lhs: UExpr<*>,
+            rhs: UExpr<*>,
+            scope: TsStepScope,
+        ): UExpr<KFp64Sort> {
+            val lhsExpr = mkNumericExpr(lhs, scope)
+            val rhsExpr = mkNumericExpr(rhs, scope)
+            return mkFpRemExpr(lhsExpr, rhsExpr)
+        }
+    }
 }
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
index e4a8efd566..14736f7b5b 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt
@@ -119,11 +119,12 @@ class InputArrays : TsMethodTestRunner() {
             method = method,
             { x, r ->
                 val value = x.values[0]
-                value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull },
+                value is TsTestValue.TsNumber && value.number == 1.0 && r is TsTestValue.TsNull
+            },
             { x, r ->
                 val value = x.values[0]
                 value !is TsTestValue.TsNumber || value.number != 1.0 && r == value
             },
         )
     }
-}
\ No newline at end of file
+}
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt
new file mode 100644
index 0000000000..f8964c6831
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Division.kt
@@ -0,0 +1,64 @@
+package org.usvm.samples.operators
+
+import org.jacodb.ets.model.EtsScene
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.toDouble
+import kotlin.test.Test
+
+class Division : TsMethodTestRunner() {
+    private val className = this::class.simpleName!!
+
+    override val scene: EtsScene = loadSampleScene(className, folderPrefix = "operators")
+
+    @Test
+    fun testTwoNumbersDivision() {
+        val method = getMethod(className, "twoNumbersDivision")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.number / b.number == 4.0 && r.number == 4.0 },
+            { a, b, r -> a.number / b.number == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY },
+            { a, b, r -> a.number / b.number == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY },
+            { a, b, r -> (a.number / b.number).isNaN() && r.number.isNaN() },
+            { a, b, r -> a.number / b.number != 4.0 && r.number == a.number / b.number }
+        )
+    }
+
+    @Test
+    fun testBooleanDivision() {
+        val method = getMethod(className, "booleanDivision")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.value.toDouble() / b.value.toDouble() == 0.0 && r.number == 0.0 },
+            { a, b, r ->
+                a.value.toDouble() / b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() / b.value.toDouble()) || r.number.isNaN())
+            }
+        )
+    }
+
+    @Test
+    fun testMixedDivision() {
+        val method = getMethod(className, "mixedDivision")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.number / b.value.toDouble() == 4.0 && r.number == 4.0 },
+            { a, b, r -> a.number / b.value.toDouble() == Double.POSITIVE_INFINITY && r.number == Double.POSITIVE_INFINITY },
+            { a, b, r -> a.number / b.value.toDouble() == Double.NEGATIVE_INFINITY && r.number == Double.NEGATIVE_INFINITY },
+            { a, b, r -> (a.number / b.value.toDouble()).isNaN() && r.number.isNaN() },
+            { a, b, r -> a.number / b.value.toDouble() != 4.0 && r.number == a.number / b.value.toDouble() }
+        )
+    }
+
+    @Test
+    fun testUnknownDivision() {
+        val method = getMethod(className, "unknownDivision")
+        discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() },
+            { _, _, r -> r.number == 4.0 },
+            { _, _, r -> r.number == Double.POSITIVE_INFINITY },
+            { _, _, r -> r.number == Double.NEGATIVE_INFINITY },
+            { _, _, r -> r.number.isNaN() },
+        )
+    }
+}
\ No newline at end of file
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Remainder.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Remainder.kt
new file mode 100644
index 0000000000..682a798722
--- /dev/null
+++ b/usvm-ts/src/test/kotlin/org/usvm/samples/operators/Remainder.kt
@@ -0,0 +1,80 @@
+package org.usvm.samples.operators
+
+import org.junit.jupiter.api.Disabled
+import org.junit.jupiter.api.Test
+import org.usvm.api.TsTestValue
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.toDouble
+
+class Remainder : TsMethodTestRunner() {
+    private val className = this::class.simpleName!!
+
+    override val scene = loadSampleScene(className, folderPrefix = "operators")
+
+    @Test
+    @Disabled("Never ends")
+    fun testTwoNumbersRemainder() {
+        val method = getMethod(className, "twoNumbersRemainder")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsNumber, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r ->
+                val res = a.number % b.number
+                res != res && (a.number.isNaN() || b.number.isNaN())
+            },
+            { a, b, r ->
+                val res = a.number % b.number
+                res != res && (a.number == Double.POSITIVE_INFINITY || a.number == Double.NEGATIVE_INFINITY)
+            },
+            { a, b, r -> a.number == 0.0 && b.number == 0.0 && r.number.isNaN() },
+            { a, b, r ->
+                b.number == 0.0 && a.number != 0.0 && r.number.isNaN()
+            },
+            { a, b, r ->
+                (b.number == Double.POSITIVE_INFINITY || b.number == Double.NEGATIVE_INFINITY) && r.number == a.number
+            },
+            { a, b, r -> a.number == 0.0 && r.number == a.number },
+            { a, b, r -> a.number % b.number == 4.0 && r.number == 4.0 },
+            { a, b, r ->
+                val res = a.number % b.number
+                !res.isNaN() && res != 4.0 && r.number == res
+            },
+        )
+    }
+
+    @Test
+    fun testBooleanRemainder() {
+        val method = getMethod(className, "booleanRemainder")
+        discoverProperties<TsTestValue.TsBoolean, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.value.toDouble() % b.value.toDouble() == 0.0 && r.number == 0.0 },
+            { a, b, r ->
+                a.value.toDouble() % b.value.toDouble() != 0.0 && (r.number == (a.value.toDouble() % b.value.toDouble()) || r.number.isNaN())
+            }
+        )
+    }
+
+    @Test
+    @Disabled("Wrong result")
+    fun testMixedRemainder() {
+        val method = getMethod(className, "mixedRemainder")
+        discoverProperties<TsTestValue.TsNumber, TsTestValue.TsBoolean, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> a.number % b.value.toDouble() == 4.0 && r.number == 4.0 },
+            { a, b, r -> (a.number % b.value.toDouble()).isNaN() && r.number.isNaN() },
+            { a, b, r -> a.number % b.value.toDouble() != 4.0 && r.number == a.number % b.value.toDouble() }
+        )
+    }
+
+    @Test
+    @Disabled("Never ends")
+    fun testUnknownRemainder() {
+        val method = getMethod(className, "unknownRemainder")
+        discoverProperties<TsTestValue, TsTestValue, TsTestValue.TsNumber>(
+            method = method,
+            { a, b, r -> (a is TsTestValue.TsUndefined || b is TsTestValue.TsUndefined) && r.number.isNaN() },
+            { _, _, r -> r.number == 4.0 },
+            { _, _, r -> r.number.isNaN() },
+            { _, _, r -> !r.number.isNaN() && r.number != 4.0 }
+        )
+    }
+}
\ No newline at end of file
diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
index 8da408fd60..c2a338a3ed 100644
--- a/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
+++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsMethodTestRunner.kt
@@ -18,6 +18,7 @@ import org.jacodb.ets.utils.loadEtsFileAutoConvert
 import org.junit.jupiter.api.TestInstance
 import org.junit.jupiter.api.TestInstance.Lifecycle.PER_CLASS
 import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.api.NoCoverage
 import org.usvm.api.TsMethodCoverage
@@ -343,6 +344,7 @@ abstract class TsMethodTestRunner : TestRunner<TsTest, EtsMethod, EtsType?, TsMe
         exceptionsPropagation = true,
         timeout = Duration.INFINITE,
         stepsFromLastCovered = 3500L,
+        solverType = SolverType.YICES,
         solverTimeout = Duration.INFINITE, // we do not need the timeout for a solver in tests
         typeOperationsTimeout = Duration.INFINITE, // we do not need the timeout for type operations in tests
     )
diff --git a/usvm-ts/src/test/resources/samples/operators/Add.ts b/usvm-ts/src/test/resources/samples/operators/Add.ts
index 682dc22547..50da6ca4f8 100644
--- a/usvm-ts/src/test/resources/samples/operators/Add.ts
+++ b/usvm-ts/src/test/resources/samples/operators/Add.ts
@@ -1,6 +1,9 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
 class Add {
     addBoolAndBool(a: boolean, b: boolean): number {
-        res = a + b;
+        let res = a + b;
 
         if (res == 0 && (a || b)) return -1 // unreachable
         if (res < 0 || res > 2) return -1 // unreachable
@@ -16,7 +19,7 @@ class Add {
     }
 
     addBoolAndNumber(a: boolean, b: number): number {
-        res = a + b;
+        let res = a + b;
 
         if (res == 0 && a) return 1 // true -1
         if (res == 0 && !a) return 2 // false 0
@@ -29,7 +32,7 @@ class Add {
     }
 
     addNumberAndNumber(a: number, b: number): number {
-        res = a + b;
+        let res = a + b;
 
         if (a != a) return res
         if (b != b) return res
@@ -40,7 +43,7 @@ class Add {
     }
 
     addNumberAndUndefined(a: number): number {
-        res = a + undefined;
+        let res = a + undefined;
 
         if (res == 0) return -1 // unreachable
 
@@ -48,7 +51,7 @@ class Add {
     }
 
     addNumberAndNull(a: number): number {
-        res = a + null;
+        let res = a + null;
 
         if (res != a) return res
 
@@ -56,7 +59,7 @@ class Add {
     }
 
     addUnknownValues(a, b) {
-        res = a + b;
+        let res = a + b;
 
         if (a === undefined || b === undefined) return res
 
diff --git a/usvm-ts/src/test/resources/samples/operators/Division.ts b/usvm-ts/src/test/resources/samples/operators/Division.ts
new file mode 100644
index 0000000000..d31c459b78
--- /dev/null
+++ b/usvm-ts/src/test/resources/samples/operators/Division.ts
@@ -0,0 +1,84 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
+class Division {
+    twoNumbersDivision(a: number, b: number): number {
+        let res = a / b;
+
+        if (res == 4) {
+            return res
+        }
+
+        if (res == Infinity) {
+            return res
+        }
+
+        if (res == -Infinity) {
+            return res
+        }
+
+        if (res != res) {
+            return res
+        }
+
+        return res
+    }
+
+    booleanDivision(a: boolean, b: boolean): number {
+        let res = a / b;
+
+        if (res == 0) {
+            return res
+        }
+
+        return res
+    }
+
+    mixedDivision(a: number, b: boolean): number {
+        let res = a / b;
+
+        if (res == 4) {
+            return res
+        }
+
+        if (res == Infinity) {
+            return res
+        }
+
+        if (res == -Infinity) {
+            return res
+        }
+
+        if (res != res) {
+            return res
+        }
+
+        return res
+    }
+
+    unknownDivision(a, b): number {
+        let res = a / b;
+
+        if (a === undefined || b === undefined) {
+            return res;
+        }
+
+        if (res == 4) {
+            return res;
+        }
+
+        if (res == Infinity) {
+            return res;
+        }
+
+        if (res == -Infinity) {
+            return res;
+        }
+
+        if (res != res) {
+            return res;
+        }
+
+        return res;
+    }
+}
diff --git a/usvm-ts/src/test/resources/samples/operators/Remainder.ts b/usvm-ts/src/test/resources/samples/operators/Remainder.ts
new file mode 100644
index 0000000000..2e1c6fea16
--- /dev/null
+++ b/usvm-ts/src/test/resources/samples/operators/Remainder.ts
@@ -0,0 +1,76 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
+class Remainder {
+    twoNumbersRemainder(a: number, b: number): number {
+        let res = a % b;
+
+        if (a != a || b != b) {
+            return res // NaN
+        }
+
+        if (a == Infinity || a == -Infinity) {
+            return res // NaN
+        }
+
+        if (a == 0 && b == 0) {
+            return res // NaN
+        }
+
+        if (b == 0) {
+            return res // NaN
+        }
+
+        if (b == Infinity || b == -Infinity) {
+            return res // a
+        }
+
+        if (a == 0) {
+            return res // a
+        }
+
+        if (res == 4) {
+            return res
+        }
+
+        return res
+    }
+
+    booleanRemainder(a: boolean, b: boolean): number {
+        let res = a % b;
+
+        if (res == 0) {
+            return res
+        }
+
+        return res
+    }
+
+    mixedRemainder(a: number, b: boolean): number {
+        let res = a % b;
+
+        if (res == 4) {
+            return res
+        }
+
+        if (res != res) {
+            return res
+        }
+
+        return res
+    }
+
+    unknownRemainder(a, b): number {
+        let res = a % b;
+
+        if (res == 4) {
+            return res;
+        }
+
+        if (res != res) {
+            return res;
+        }
+
+        return res;
+    }
+}
diff --git a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts
index 622f2f0482..724703393f 100644
--- a/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts
+++ b/usvm-ts/src/test/resources/samples/types/StructuralEquality.ts
@@ -1,49 +1,52 @@
+// @ts-nocheck
+// noinspection JSUnusedGlobalSymbols
+
 class A {
-  x: number;
+    x: number;
 
-  constructor(x: number) {
-    this.x = x;
-  }
+    constructor(x: number) {
+        this.x = x;
+    }
 
-  foo (): number {
-    return 21;
-  }
+    foo(): number {
+        return 21;
+    }
 }
 
 class B {
-  x: number;
+    x: number;
 
-  constructor(x: number) {
-    this.x = x;
-  }
+    constructor(x: number) {
+        this.x = x;
+    }
 
-  foo (): number {
-    return this.x;
-  }
+    foo(): number {
+        return this.x;
+    }
 }
 
 class C {
-  x: A;
+    x: A;
 
-  constructor(x: A) {
-    this.x = x;
-  }
+    constructor(x: A) {
+        this.x = x;
+    }
 }
 
 class D {
-  x: B;
+    x: B;
 
-  constructor(x: B) {
-    this.x = x;
-  }
+    constructor(x: B) {
+        this.x = x;
+    }
 }
 
 class Example {
-  testFunction() : C {
-    const obj: A = new B(11);
-    const number = obj.foo();
+    testFunction(): C {
+        const obj: A = new B(11);
+        const number = obj.foo();
 
-    const aaa: C = new D(new A(number));
-    return aaa
-  }
+        const aaa: C = new D(new A(number));
+        return aaa
+    }
 }
diff --git a/usvm-ts/src/test/resources/samples/types/TypeStream.ts b/usvm-ts/src/test/resources/samples/types/TypeStream.ts
index 26d0de229a..ea2c6e5e6b 100644
--- a/usvm-ts/src/test/resources/samples/types/TypeStream.ts
+++ b/usvm-ts/src/test/resources/samples/types/TypeStream.ts
@@ -45,25 +45,25 @@ class TypeStream {
 }
 
 class Parent {
+    parentField: number = -10
+
     virtualMethod(): number {
         return 100;
     }
-
-    parentField: number = -10
 }
 
 class FirstChild extends Parent {
+    firstChildField: number = 10
+
     override virtualMethod(): number {
         return 200;
     }
-
-    firstChildField: number = 10
 }
 
 class SecondChild extends Parent {
+    secondChildField: number = 20
+
     override virtualMethod(): number {
         return 300;
     }
-
-    secondChildField: number = 20
 }