diff --git a/build.gradle.kts b/build.gradle.kts
index b761a87211..1ce1e3d00b 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -132,6 +132,7 @@ allprojects {
 
     repositories {
         mavenCentral()
+        maven("https://jitpack.io")
         maven("https://s01.oss.sonatype.org/content/repositories/orgunittestbotsoot-1004/")
         maven("https://plugins.gradle.org/m2")
         maven("https://www.jetbrains.com/intellij-repository/releases")
diff --git a/gradle.properties b/gradle.properties
index 934a92075b..144762f9b4 100644
--- a/gradle.properties
+++ b/gradle.properties
@@ -26,8 +26,7 @@ junit5Version=5.8.0-RC1
 junit4Version=4.13.2
 junit4PlatformVersion=1.9.0
 mockitoVersion=3.5.13
-z3Version=4.8.9.1
-z3JavaApiVersion=4.8.9
+ksmtVersion=0.4.3
 sootVersion=4.4.0-FORK-2
 kotlinVersion=1.8.0
 log4j2Version=2.13.3
@@ -63,7 +62,6 @@ testNgVersion=7.6.0
 mockitoInlineVersion=4.0.0
 kamlVersion = 0.51.0
 jacksonVersion = 2.12.3
-javasmtSolverZ3Version=4.8.9-sosy1
 slf4jVersion=1.7.36
 eclipseAetherVersion=1.1.0
 mavenWagonVersion=3.5.1
diff --git a/utbot-framework-test/build.gradle b/utbot-framework-test/build.gradle
index 8ac7625d74..012d6e7c3f 100644
--- a/utbot-framework-test/build.gradle
+++ b/utbot-framework-test/build.gradle
@@ -10,16 +10,6 @@ tasks.withType(JavaCompile) {
     targetCompatibility = JavaVersion.VERSION_17
 }
 
-repositories {
-    flatDir {
-        dirs 'dist'
-    }
-}
-
-configurations {
-    z3native
-}
-
 dependencies {
     api project(':utbot-framework-api')
     testImplementation project(':utbot-testing')
@@ -39,7 +29,6 @@ dependencies {
 
     implementation group: 'com.charleskorn.kaml', name: 'kaml', version: kamlVersion
     implementation group: 'com.fasterxml.jackson.module', name: 'jackson-module-kotlin', version: jacksonVersion
-    implementation group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: javasmtSolverZ3Version
     implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
     implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
     implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlinLoggingVersion
@@ -66,12 +55,10 @@ dependencies {
     testImplementation group: 'org.mockito', name: 'mockito-inline', version: mockitoInlineVersion
     testImplementation group: 'org.apache.logging.log4j', name: 'log4j-core', version: log4j2Version
 
-    z3native group: 'com.microsoft.z3', name: 'z3-native-win64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-linux64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-osx', version: z3Version, ext: 'zip'
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
 }
 
-
 test {
     if (System.getProperty('DEBUG', 'false') == 'true') {
         jvmArgs '-Xdebug', '-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=9009'
diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/math/OverflowAsErrorTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/math/OverflowAsErrorTest.kt
index 5a5d233fe8..982c5ceaa7 100644
--- a/utbot-framework-test/src/test/kotlin/org/utbot/examples/math/OverflowAsErrorTest.kt
+++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/math/OverflowAsErrorTest.kt
@@ -8,7 +8,7 @@ import org.utbot.framework.plugin.api.CodegenLanguage
 import org.utbot.testcheckers.eq
 import org.utbot.testcheckers.withSolverTimeoutInMillis
 import org.utbot.testcheckers.withTreatingOverflowAsError
-import org.utbot.testing.AtLeast
+import org.utbot.testing.DoNotCalculate
 import org.utbot.testing.Compilation
 import org.utbot.testing.UtValueTestCaseChecker
 import org.utbot.testing.ignoreExecutionsNumber
@@ -32,12 +32,23 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
             checkWithException(
                 OverflowExamples::intOverflow,
                 eq(5),
-                { x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow
-                { x, _, r -> x * x * x <= 0 && x > 0 && r.isException<OverflowDetectionError>() }, // through overflow (2nd '*')
+                { x, _, r ->
+                    val overflowOccurred = kotlin.runCatching {
+                        Math.multiplyExact(x, x)
+                    }.isFailure
+                    overflowOccurred && r.isException<OverflowDetectionError>()
+                }, // through overflow
+                { x, _, r ->
+                    val twoMul = Math.multiplyExact(x, x)
+                    val overflowOccurred = kotlin.runCatching {
+                        Math.multiplyExact(twoMul, x)
+                    }.isFailure
+                    overflowOccurred && r.isException<OverflowDetectionError>()
+                }, // through overflow (2nd '*')
                 { x, _, r -> x * x * x >= 0 && x >= 0 && r.getOrNull() == 0 },
                 { x, y, r -> x * x * x > 0 && x > 0 && y == 10 && r.getOrNull() == 1 },
                 { x, y, r -> x * x * x > 0 && x > 0 && y != 10 && r.getOrNull() == 0 },
-                coverage = AtLeast(90),
+                coverage = DoNotCalculate
             )
         }
     }
@@ -258,7 +269,7 @@ internal class OverflowAsErrorTest : UtValueTestCaseChecker(
         }
     }
 
-//  Generated Kotlin code does not compile, so disabled for now
+    //  Generated Kotlin code does not compile, so disabled for now
     @Test
     @Disabled
     fun testQuickSort() {
diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionForTests.kt b/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionForTests.kt
index fdc65fd713..a0e9efcb9f 100644
--- a/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionForTests.kt
+++ b/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionForTests.kt
@@ -5,19 +5,19 @@ package com.microsoft.z3
 import kotlin.reflect.KProperty
 
 
-operator fun ArithExpr.plus(other: ArithExpr): ArithExpr = context.mkAdd(this, other)
-operator fun ArithExpr.plus(other: Int): ArithExpr = this + context.mkInt(other)
+operator fun ArithExpr<*>.plus(other: ArithExpr<*>): ArithExpr<*> = context.mkAdd(this, other)
+operator fun ArithExpr<*>.plus(other: Int): ArithExpr<*> = this + context.mkInt(other)
 
-operator fun ArithExpr.minus(other: ArithExpr): ArithExpr = context.mkSub(this, other)
-operator fun ArithExpr.minus(other: Int): ArithExpr = this - context.mkInt(other)
+operator fun ArithExpr<*>.minus(other: ArithExpr<*>): ArithExpr<*> = context.mkSub(this, other)
+operator fun ArithExpr<*>.minus(other: Int): ArithExpr<*> = this - context.mkInt(other)
 
-operator fun ArithExpr.times(other: ArithExpr): ArithExpr = context.mkMul(this, other)
-operator fun ArithExpr.times(other: Int): ArithExpr = this * context.mkInt(other)
+operator fun ArithExpr<*>.times(other: ArithExpr<*>): ArithExpr<*> = context.mkMul(this, other)
+operator fun ArithExpr<*>.times(other: Int): ArithExpr<*> = this * context.mkInt(other)
 
-infix fun Expr.`=`(other: Int): BoolExpr = this eq context.mkInt(other)
-infix fun Expr.`=`(other: Expr): BoolExpr = this eq other
-infix fun Expr.eq(other: Expr): BoolExpr = context.mkEq(this, other)
-infix fun Expr.`!=`(other: Expr): BoolExpr = context.mkNot(this `=` other)
+infix fun Expr<*>.`=`(other: Int): BoolExpr = this eq context.mkInt(other)
+infix fun Expr<*>.`=`(other: Expr<*>): BoolExpr = this eq other
+infix fun Expr<*>.eq(other: Expr<*>): BoolExpr = context.mkEq(this, other)
+infix fun Expr<*>.`!=`(other: Expr<*>): BoolExpr = context.mkNot(this `=` other)
 operator fun BoolExpr.not(): BoolExpr = context.mkNot(this)
 
 infix fun BoolExpr.`⇒`(other: BoolExpr): BoolExpr = this implies other
@@ -27,20 +27,24 @@ infix fun BoolExpr.implies(other: BoolExpr): BoolExpr = context.mkImplies(this,
 infix fun BoolExpr.and(other: BoolExpr): BoolExpr = context.mkAnd(this, other)
 infix fun BoolExpr.or(other: BoolExpr): BoolExpr = context.mkOr(this, other)
 
-infix fun ArithExpr.gt(other: ArithExpr): BoolExpr = context.mkGt(this, other)
-infix fun ArithExpr.gt(other: Int): BoolExpr = context.mkGt(this, context.mkInt(other))
+infix fun ArithExpr<*>.gt(other: ArithExpr<*>): BoolExpr = context.mkGt(this, other)
+infix fun ArithExpr<*>.gt(other: Int): BoolExpr = context.mkGt(this, context.mkInt(other))
 
-infix fun ArithExpr.`=`(other: Int): BoolExpr = context.mkEq(this, context.mkInt(other))
+infix fun ArithExpr<*>.`=`(other: Int): BoolExpr = context.mkEq(this, context.mkInt(other))
 
-operator fun ArrayExpr.get(index: IntExpr): Expr = context.mkSelect(this, index)
-operator fun ArrayExpr.get(index: Int): Expr = this[context.mkInt(index)]
-fun ArrayExpr.set(index: IntExpr, value: Expr): ArrayExpr = context.mkStore(this, index, value)
-fun ArrayExpr.set(index: Int, value: Expr): ArrayExpr = set(context.mkInt(index), value)
+operator fun  ArrayExpr<*, *>.get(index: IntExpr): Expr<*> = context.mkSelect(this, index.cast())
+operator fun  ArrayExpr<*, *>.get(index: Int): Expr<*> = this[context.mkInt(index)]
+fun  ArrayExpr<*, *>.set(index: IntExpr, value: Expr<*>):  ArrayExpr<*, *> = context.mkStore(this, index.cast(), value.cast())
+fun  ArrayExpr<*, *>.set(index: Int, value: Expr<*>):  ArrayExpr<*, *> = set(context.mkInt(index), value)
 
-operator fun SeqExpr.plus(other: SeqExpr): SeqExpr = context.mkConcat(this, other)
-operator fun SeqExpr.plus(other: String): SeqExpr = context.mkConcat(context.mkString(other))
+operator fun SeqExpr<*>.plus(other: SeqExpr<*>): SeqExpr<*> = context.mkConcat(this, other.cast())
+operator fun SeqExpr<*>.plus(other: String): SeqExpr<*> = context.mkConcat(context.mkString(other))
 
-infix fun SeqExpr.`=`(other: String): BoolExpr = context.mkEq(this, context.mkString(other))
+@Suppress("UNCHECKED_CAST")
+fun <T : Sort, R : Sort> Expr<T>.cast(): Expr<R> = this as Expr<R>
+
+
+infix fun SeqExpr<*>.`=`(other: String): BoolExpr = context.mkEq(this, context.mkString(other))
 
 class Const<T>(private val ctx: Context, val produce: (Context, name: String) -> T) {
     operator fun getValue(thisRef: Nothing?, property: KProperty<*>): T = produce(ctx, property.name)
@@ -49,12 +53,12 @@ class Const<T>(private val ctx: Context, val produce: (Context, name: String) ->
 fun Context.declareInt() = Const(this) { ctx, name -> ctx.mkIntConst(name) }
 fun Context.declareBool() = Const(this) { ctx, name -> ctx.mkBoolConst(name) }
 fun Context.declareReal() = Const(this) { ctx, name -> ctx.mkRealConst(name) }
-fun Context.declareString() = Const(this) { ctx, name -> ctx.mkConst(name, stringSort) as SeqExpr }
-fun Context.declareList(sort: ListSort) = Const(this) { ctx, name -> ctx.mkConst(name, sort) }
+fun Context.declareString() = Const(this) { ctx, name -> ctx.mkConst(name, stringSort) as SeqExpr<*> }
+fun Context.declareList(sort: ListSort<*>) = Const(this) { ctx, name -> ctx.mkConst(name, sort) }
 fun Context.declareIntArray() = Const(this) { ctx, name -> ctx.mkArrayConst(name, intSort, intSort) }
 
 
-operator fun FuncDecl.invoke(vararg expr: Expr): Expr = context.mkApp(this, *expr)
+operator fun FuncDecl<*>.invoke(vararg expr: Expr<*>): Expr<*> = context.mkApp(this, *expr)
 
-fun Model.eval(expr: Expr): Expr = this.eval(expr, true)
-fun Model.eval(vararg exprs: Expr): List<Expr> = exprs.map { this.eval(it, true) }
\ No newline at end of file
+fun Model.eval(expr: Expr<*>): Expr<*> = this.eval(expr, true)
+fun Model.eval(vararg exprs: Expr<*>): List<Expr<*>> = exprs.map { this.eval(it, true) }
\ No newline at end of file
diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionTest.kt
index c31298bac8..896d1e3a98 100644
--- a/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionTest.kt
+++ b/utbot-framework-test/src/test/kotlin/org/utbot/framework/z3/extension/Z3ExtensionTest.kt
@@ -99,8 +99,8 @@ class Z3ExtensionTest : Z3Initializer() {
 
             val (aVal, bVal, cVal) = solver.model
                 .eval(a, b, c)
-                .filterIsInstance<SeqExpr>()
-                .map(SeqExpr::getString)
+                .filterIsInstance<SeqExpr<*>>()
+                .map(SeqExpr<*>::getString)
                 .also { list -> assertEquals(3, list.size) }
 
             assertEquals("abcd", "$aVal$bVal")
diff --git a/utbot-framework/build.gradle b/utbot-framework/build.gradle
index 4cb5e4a035..3e0cd02564 100644
--- a/utbot-framework/build.gradle
+++ b/utbot-framework/build.gradle
@@ -1,13 +1,3 @@
-repositories {
-    flatDir {
-        dirs 'dist'
-    }
-}
-
-configurations {
-    z3native
-}
-
 dependencies {
 
     api project(':utbot-fuzzers')
@@ -29,7 +19,6 @@ dependencies {
 
     implementation group: 'com.charleskorn.kaml', name: 'kaml', version: kamlVersion
     implementation group: 'com.fasterxml.jackson.module', name: 'jackson-module-kotlin', version: jacksonVersion
-    implementation group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: javasmtSolverZ3Version
     implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
     implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
     implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlinLoggingVersion
@@ -43,15 +32,6 @@ dependencies {
     implementation group: 'org.junit.jupiter', name: 'junit-jupiter-params', version: '5.8.1'
     implementation group: 'org.junit.jupiter', name: 'junit-jupiter-engine', version: '5.8.1'
 
-    z3native group: 'com.microsoft.z3', name: 'z3-native-win64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-linux64', version: z3Version, ext: 'zip'
-    z3native group: 'com.microsoft.z3', name: 'z3-native-osx', version: z3Version, ext: 'zip'
-}
-
-processResources {
-    configurations.z3native.resolvedConfiguration.resolvedArtifacts.each { artifact ->
-        from(zipTree(artifact.getFile())) {
-            into "lib/x64"
-        }
-    }
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
 }
diff --git a/utbot-framework/dist/z3-native-linux64-4.8.9.1.zip b/utbot-framework/dist/z3-native-linux64-4.8.9.1.zip
deleted file mode 100644
index a5a3ac9e4a..0000000000
Binary files a/utbot-framework/dist/z3-native-linux64-4.8.9.1.zip and /dev/null differ
diff --git a/utbot-framework/dist/z3-native-osx-4.8.9.1.zip b/utbot-framework/dist/z3-native-osx-4.8.9.1.zip
deleted file mode 100644
index 9b42561fc9..0000000000
Binary files a/utbot-framework/dist/z3-native-osx-4.8.9.1.zip and /dev/null differ
diff --git a/utbot-framework/dist/z3-native-win64-4.8.9.1.zip b/utbot-framework/dist/z3-native-win64-4.8.9.1.zip
deleted file mode 100644
index 2024be077e..0000000000
Binary files a/utbot-framework/dist/z3-native-win64-4.8.9.1.zip and /dev/null differ
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt
index b0f7ea8b94..c06bfae5ad 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtExpression.kt
@@ -932,7 +932,7 @@ data class UtMkTermArrayExpression(val array: UtArrayExpressionBase, val default
     override fun hashCode() = hashCode
 }
 
-data class Z3Variable(val type: Type, val expr: Expr) {
+data class Z3Variable(val type: Type, val expr: Expr<*>) {
     private val hashCode = Objects.hash(type, expr)
 
     override fun equals(other: Any?): Boolean {
@@ -950,6 +950,6 @@ data class Z3Variable(val type: Type, val expr: Expr) {
     override fun hashCode() = hashCode
 }
 
-fun Expr.z3Variable(type: Type) = Z3Variable(type, this)
+fun Expr<*>.z3Variable(type: Type) = Z3Variable(type, this)
 
 fun UtExpression.isInteger() = this.sort is UtBvSort
\ No newline at end of file
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt
index 1250023952..f0b6def89e 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolverStatus.kt
@@ -47,7 +47,7 @@ class UtSolverStatusSAT(
 
     private val evaluator: Z3EvaluatorVisitor = translator.evaluator(model)
 
-    fun eval(expression: UtExpression): Expr = evaluator.eval(expression)
+    fun eval(expression: UtExpression): Expr<*> = evaluator.eval(expression)
 
     fun concreteAddr(expression: UtAddrExpression): Address = eval(expression).intValue()
 
@@ -65,7 +65,7 @@ class UtSolverStatusSAT(
      * - val arrayInterpretationFuncDecl: FuncDecl = mfd.parameters[[0]].funcDecl
      * - val interpretation: FuncInterp = z3Solver.model.getFuncInterp(arrayInterpretationFuncDecl)
      */
-    internal fun evalArrayDescriptor(mval: Expr, unsigned: Boolean, filter: (Int) -> Boolean): ArrayDescriptor {
+    internal fun evalArrayDescriptor(mval: Expr<*>, unsigned: Boolean, filter: (Int) -> Boolean): ArrayDescriptor {
         var next = mval
         val stores = mutableMapOf<Int, Any>()
         var const: Any? = null
@@ -79,7 +79,7 @@ class UtSolverStatusSAT(
                     next = next.args[0]
                 }
                 Z3_OP_UNINTERPRETED -> next = model.eval(next)
-                Z3_OP_CONST_ARRAY -> const = if (next.args[0] is ArrayExpr) {
+                Z3_OP_CONST_ARRAY -> const = if (next.args[0] is ArrayExpr<*, *>) {
                     // if we have an array as const value, create a corresponding descriptor for it
                     evalArrayDescriptor(next.args[0], unsigned, filter)
                 } else {
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Util.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Util.kt
new file mode 100644
index 0000000000..ad8f055be7
--- /dev/null
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Util.kt
@@ -0,0 +1,7 @@
+package org.utbot.engine.pc
+
+import com.microsoft.z3.Expr
+import com.microsoft.z3.Sort
+
+@Suppress("UNCHECKED_CAST")
+fun <T : Sort, R : Sort> Expr<T>.cast(): Expr<R> = this as Expr<R>
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt
index ec09cde2cd..adef85f2fb 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3EvaluatorVisitor.kt
@@ -20,38 +20,38 @@ import soot.ByteType
 import soot.CharType
 
 class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3TranslatorVisitor) :
-    UtExpressionVisitor<Expr> by translator {
+    UtExpressionVisitor<Expr<*>> by translator {
 
     // stack of indexes that are visited in expression in derivation tree.
     // For example, we call eval(select(select(a, i), j)
     // On visiting term a, the stack will be equals to [i, j]
-    private val selectIndexStack = mutableListOf<Expr>()
+    private val selectIndexStack = mutableListOf<Expr<*>>()
 
-    private inline fun withPushedSelectIndex(index: UtExpression, block: () -> Expr): Expr {
+    private inline fun withPushedSelectIndex(index: UtExpression, block: () -> Expr<*>): Expr<*> {
         selectIndexStack += eval(index)
         return block().also {
             selectIndexStack.removeLast()
         }
     }
 
-    private inline fun withPoppedSelectIndex(block: () -> Expr): Expr {
+    private inline fun withPoppedSelectIndex(block: () -> Expr<*>): Expr<*> {
         val lastIndex = selectIndexStack.removeLast()
         return block().also {
             selectIndexStack += lastIndex
         }
     }
 
-    private fun foldSelectsFromStack(expr: Expr): Expr {
+    private fun foldSelectsFromStack(expr: Expr<*>): Expr<*> {
         var result = expr
         var i = selectIndexStack.size
-        while (i > 0 && result.sort is ArraySort) {
-            result = translator.withContext { mkSelect(result as ArrayExpr, selectIndexStack[--i]) }
+        while (i > 0 && result.sort is ArraySort<*, *>) {
+            result = translator.withContext { mkSelect(result as ArrayExpr<*, *>, selectIndexStack[--i].cast()) }
         }
         return result
     }
 
 
-    fun eval(expr: UtExpression): Expr {
+    fun eval(expr: UtExpression): Expr<*> {
         val translated = if (expr.sort is UtArraySort) {
             translator.lookUpCache(expr)?.let { foldSelectsFromStack(it) } ?: expr.accept(this)
         } else {
@@ -60,14 +60,14 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         return model.eval(translated)
     }
 
-    override fun visit(expr: UtArraySelectExpression): Expr = expr.run {
+    override fun visit(expr: UtArraySelectExpression): Expr<*> = expr.run {
         // translate arrayExpression here will return evaluation of arrayExpression.select(index)
         withPushedSelectIndex(index) {
             eval(arrayExpression)
         }
     }
 
-    override fun visit(expr: UtConstArrayExpression): Expr = expr.run {
+    override fun visit(expr: UtConstArrayExpression): Expr<*> = expr.run {
         // expr.select(index) = constValue for any index
         if (selectIndexStack.size == 0) {
             translator.withContext { mkConstArray(sort.indexSort.toZ3Sort(this), eval(constValue)) }
@@ -78,17 +78,17 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtMkArrayExpression): Expr =
+    override fun visit(expr: UtMkArrayExpression): Expr<*> =
     // mkArray expression can have more than one dimension
     // so for such case select(select(mkArray(...), i), j))
         // indices i and j are currently in the stack and we need to fold them.
         foldSelectsFromStack(translator.translate(expr))
 
-    override fun visit(expr: UtArrayMultiStoreExpression): Expr = expr.run {
+    override fun visit(expr: UtArrayMultiStoreExpression): Expr<*> = expr.run {
         val lastIndex = selectIndexStack.lastOrNull()
             ?: return translator.withContext {
-                stores.fold(translator.translate(initial) as ArrayExpr) { acc, (index, item) ->
-                    mkStore(acc, eval(index), eval(item))
+                stores.fold(translator.translate(initial) as ArrayExpr<*, *>) { acc, (index, item) ->
+                    mkStore(acc, eval(index).cast(), eval(item).cast())
                 }
             }
         for (store in stores.asReversed()) {
@@ -99,12 +99,12 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         eval(initial)
     }
 
-    override fun visit(expr: UtMkTermArrayExpression): Expr = expr.run {
+    override fun visit(expr: UtMkTermArrayExpression): Expr<*> = expr.run {
         // should we make eval(mkTerm) always true??
         translator.translate(UtTrue)
     }
 
-    override fun visit(expr: UtArrayInsert): Expr = expr.run {
+    override fun visit(expr: UtArrayInsert): Expr<*> = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         when {
@@ -114,7 +114,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayInsertRange): Expr = expr.run {
+    override fun visit(expr: UtArrayInsertRange): Expr<*> = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         val length = eval(length.expr).intValue()
@@ -128,7 +128,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayRemove): Expr = expr.run {
+    override fun visit(expr: UtArrayRemove): Expr<*> = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         if (lastIndex < index) {
@@ -138,7 +138,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayRemoveRange): Expr = expr.run {
+    override fun visit(expr: UtArrayRemoveRange): Expr<*> = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         if (lastIndex < index) {
@@ -149,7 +149,7 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArraySetRange): Expr = expr.run {
+    override fun visit(expr: UtArraySetRange): Expr<*> = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val index = eval(index.expr).intValue()
         val length = eval(length.expr).intValue()
@@ -162,15 +162,15 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtArrayShiftIndexes): Expr = expr.run {
+    override fun visit(expr: UtArrayShiftIndexes): Expr<*> = expr.run {
         val lastIndex = selectIndexStack.last().intValue()
         val offset = eval(offset.expr).intValue()
         eval(arrayExpression.select(mkInt(lastIndex - offset)))
     }
 
-    override fun visit(expr: UtAddrExpression): Expr = eval(expr.internal)
+    override fun visit(expr: UtAddrExpression): Expr<*> = eval(expr.internal)
 
-    override fun visit(expr: UtOpExpression): Expr = expr.run {
+    override fun visit(expr: UtOpExpression): Expr<*> = expr.run {
         val leftResolve = eval(left.expr).z3Variable(left.type)
         val rightResolve = eval(right.expr).z3Variable(right.type)
         translator.withContext {
@@ -178,50 +178,50 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtEqExpression): Expr = expr.run {
+    override fun visit(expr: UtEqExpression): Expr<*> = expr.run {
         translator.withContext { mkEq(eval(left), eval(right)) }
     }
 
-    override fun visit(expr: NotBoolExpression): Expr =
+    override fun visit(expr: NotBoolExpression): Expr<*> =
         translator.withContext { mkNot(eval(expr.expr) as BoolExpr) }
 
-    override fun visit(expr: UtOrBoolExpression): Expr = expr.run {
+    override fun visit(expr: UtOrBoolExpression): Expr<*> = expr.run {
         translator.withContext {
             mkOr(*expr.exprs.map { eval(it) as BoolExpr }.toTypedArray())
         }
     }
 
-    override fun visit(expr: UtAndBoolExpression): Expr = expr.run {
+    override fun visit(expr: UtAndBoolExpression): Expr<*> = expr.run {
         translator.withContext {
             mkAnd(*expr.exprs.map { eval(it) as BoolExpr }.toTypedArray())
         }
     }
 
-    override fun visit(expr: UtAddNoOverflowExpression): Expr = expr.run {
+    override fun visit(expr: UtAddNoOverflowExpression): Expr<*> = expr.run {
         translator.withContext {
             mkBVAddNoOverflow(eval(expr.left) as BitVecExpr, eval(expr.right) as BitVecExpr, true)
         }
     }
 
-    override fun visit(expr: UtSubNoOverflowExpression): Expr = expr.run {
+    override fun visit(expr: UtSubNoOverflowExpression): Expr<*> = expr.run {
         translator.withContext {
             // For some reason mkBVSubNoOverflow does not take "signed" as an argument, yet still works for signed integers
             mkBVSubNoOverflow(eval(expr.left) as BitVecExpr, eval(expr.right) as BitVecExpr) //, true)
         }
     }
 
-    override fun visit(expr: UtNegExpression): Expr = expr.run {
+    override fun visit(expr: UtNegExpression): Expr<*> = expr.run {
         translator.withContext {
             negate(this, eval(variable.expr).z3Variable(variable.type))
         }
     }
 
-    override fun visit(expr: UtCastExpression): Expr = expr.run {
+    override fun visit(expr: UtCastExpression): Expr<*> = expr.run {
         val z3var = eval(variable.expr).z3Variable(variable.type)
         translator.withContext { convertVar(z3var, type).expr }
     }
 
-    override fun visit(expr: UtBoolOpExpression): Expr = expr.run {
+    override fun visit(expr: UtBoolOpExpression): Expr<*> = expr.run {
         val leftResolve = eval(left.expr).z3Variable(left.type)
         val rightResolve = eval(right.expr).z3Variable(right.type)
         translator.withContext {
@@ -229,16 +229,16 @@ class Z3EvaluatorVisitor(private val model: Model, private val translator: Z3Tra
         }
     }
 
-    override fun visit(expr: UtIsExpression): Expr = translator.translate(expr)
+    override fun visit(expr: UtIsExpression): Expr<*> = translator.translate(expr)
 
-    override fun visit(expr: UtInstanceOfExpression): Expr =
+    override fun visit(expr: UtInstanceOfExpression): Expr<*> =
         expr.run { eval(expr.constraint) }
 
-    override fun visit(expr: UtIteExpression): Expr = expr.run {
+    override fun visit(expr: UtIteExpression): Expr<*> = expr.run {
         if (eval(condition).value() as Boolean) eval(thenExpr) else eval(elseExpr)
     }
 
-    override fun visit(expr: UtArrayApplyForAll): Expr = expr.run {
+    override fun visit(expr: UtArrayApplyForAll): Expr<*> = expr.run {
         eval(expr.arrayExpression.select(mkInt(selectIndexStack.last().intValue())))
     }
 }
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt
index 89e775fbd1..6e67867ffa 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Z3TranslatorVisitor.kt
@@ -1,5 +1,6 @@
 package org.utbot.engine.pc
 
+import com.microsoft.z3.*
 import org.utbot.common.WorkaroundReason
 import org.utbot.common.workaround
 import org.utbot.engine.types.TypeRegistry
@@ -13,14 +14,6 @@ import org.utbot.engine.z3.convertVar
 import org.utbot.engine.z3.makeBV
 import org.utbot.engine.z3.makeFP
 import org.utbot.engine.z3.negate
-import com.microsoft.z3.ArrayExpr
-import com.microsoft.z3.BitVecExpr
-import com.microsoft.z3.BoolExpr
-import com.microsoft.z3.Context
-import com.microsoft.z3.Expr
-import com.microsoft.z3.FPSort
-import com.microsoft.z3.IntExpr
-import com.microsoft.z3.Model
 import org.utbot.engine.types.TypeRegistry.Companion.numberOfTypes
 import org.utbot.framework.UtSettings
 import org.utbot.framework.UtSettings.maxTypeNumberForEnumeration
@@ -34,101 +27,102 @@ import soot.Type
 open class Z3TranslatorVisitor(
     private val z3Context: Context,
     private val typeRegistry: TypeRegistry
-) : UtExpressionVisitor<Expr> {
+) : UtExpressionVisitor<Expr<*>> {
 
     //thread-safe
-    private val expressionTranslationCache = IdentityHashMap<UtExpression, Expr>()
+    private val expressionTranslationCache = IdentityHashMap<UtExpression, Expr<*>>()
 
     fun evaluator(model: Model): Z3EvaluatorVisitor = Z3EvaluatorVisitor(model, this)
 
     /**
      * Translate [expr] from [UtExpression] to [Expr]
      */
-    fun translate(expr: UtExpression): Expr =
+    fun translate(expr: UtExpression): Expr<*> =
         expressionTranslationCache.getOrPut(expr) { expr.accept(this) }
 
-    fun lookUpCache(expr: UtExpression): Expr? = expressionTranslationCache[expr]
+    fun lookUpCache(expr: UtExpression): Expr<*>? = expressionTranslationCache[expr]
 
-    fun withContext(block: Context.() -> Expr): Expr {
+    fun withContext(block: Context.() -> Expr<*>): Expr<*> {
         return z3Context.block()
     }
 
-    override fun visit(expr: UtArraySelectExpression): Expr = expr.run {
-        z3Context.mkSelect(translate(arrayExpression) as ArrayExpr, translate(index))
+    override fun visit(expr: UtArraySelectExpression): Expr<*> = expr.run {
+        z3Context.mkSelect(translate(arrayExpression) as ArrayExpr<*, *>, translate(index).cast())
     }
 
+
     /**
      * Creates a const array filled with a fixed value
      */
-    override fun visit(expr: UtConstArrayExpression): Expr = expr.run {
+    override fun visit(expr: UtConstArrayExpression): Expr<*> = expr.run {
         z3Context.mkConstArray(sort.indexSort.toZ3Sort(z3Context), translate(constValue))
     }
 
-    override fun visit(expr: UtMkArrayExpression): Expr = expr.run {
-        z3Context.run { mkConst(name, sort.toZ3Sort(this)) } as ArrayExpr
+    override fun visit(expr: UtMkArrayExpression): Expr<*> = expr.run {
+        z3Context.run { mkConst(name, sort.toZ3Sort(this)) } as ArrayExpr<*, *>
     }
 
-    override fun visit(expr: UtArrayMultiStoreExpression): Expr = expr.run {
-        stores.fold(translate(initial) as ArrayExpr) { acc, (index, item) ->
-            z3Context.mkStore(acc, translate(index), translate(item))
+    override fun visit(expr: UtArrayMultiStoreExpression): Expr<*> = expr.run {
+        stores.fold(translate(initial) as ArrayExpr<*, *>) { acc, (index, item) ->
+            z3Context.mkStore(acc, translate(index).cast(), translate(item).cast())
         }
     }
 
-    override fun visit(expr: UtBvLiteral): Expr = expr.run { z3Context.makeBV(value, size) }
+    override fun visit(expr: UtBvLiteral): Expr<*> = expr.run { z3Context.makeBV(value, size) }
 
-    override fun visit(expr: UtBvConst): Expr = expr.run { z3Context.mkBVConst(name, size) }
+    override fun visit(expr: UtBvConst): Expr<*> = expr.run { z3Context.mkBVConst(name, size) }
 
-    override fun visit(expr: UtAddrExpression): Expr = expr.run { translate(internal) }
+    override fun visit(expr: UtAddrExpression): Expr<*> = expr.run { translate(internal) }
 
-    override fun visit(expr: UtFpLiteral): Expr =
+    override fun visit(expr: UtFpLiteral): Expr<*> =
         expr.run { z3Context.makeFP(value, sort.toZ3Sort(z3Context) as FPSort) }
 
-    override fun visit(expr: UtFpConst): Expr = expr.run { z3Context.mkConst(name, sort.toZ3Sort(z3Context)) }
+    override fun visit(expr: UtFpConst): Expr<*> = expr.run { z3Context.mkConst(name, sort.toZ3Sort(z3Context)) }
 
-    override fun visit(expr: UtOpExpression): Expr = expr.run {
+    override fun visit(expr: UtOpExpression): Expr<*> = expr.run {
         val leftResolve = translate(left.expr).z3Variable(left.type)
         val rightResolve = translate(right.expr).z3Variable(right.type)
         operator.delegate(z3Context, leftResolve, rightResolve)
     }
 
-    override fun visit(expr: UtTrue): Expr = expr.run { z3Context.mkBool(true) }
+    override fun visit(expr: UtTrue): Expr<*> = expr.run { z3Context.mkBool(true) }
 
-    override fun visit(expr: UtFalse): Expr = expr.run { z3Context.mkBool(false) }
+    override fun visit(expr: UtFalse): Expr<*> = expr.run { z3Context.mkBool(false) }
 
-    override fun visit(expr: UtEqExpression): Expr = expr.run { z3Context.mkEq(translate(left), translate(right)) }
+    override fun visit(expr: UtEqExpression): Expr<*> = expr.run { z3Context.mkEq(translate(left), translate(right)) }
 
-    override fun visit(expr: UtBoolConst): Expr = expr.run { z3Context.mkBoolConst(name) }
+    override fun visit(expr: UtBoolConst): Expr<*> = expr.run { z3Context.mkBoolConst(name) }
 
-    override fun visit(expr: NotBoolExpression): Expr =
+    override fun visit(expr: NotBoolExpression): Expr<*> =
         expr.run { z3Context.mkNot(translate(expr.expr) as BoolExpr) }
 
-    override fun visit(expr: UtOrBoolExpression): Expr = expr.run {
+    override fun visit(expr: UtOrBoolExpression): Expr<*> = expr.run {
         z3Context.mkOr(*exprs.map { translate(it) as BoolExpr }.toTypedArray())
     }
 
-    override fun visit(expr: UtAndBoolExpression): Expr = expr.run {
+    override fun visit(expr: UtAndBoolExpression): Expr<*> = expr.run {
         z3Context.mkAnd(*exprs.map { translate(it) as BoolExpr }.toTypedArray())
     }
 
-    override fun visit(expr: UtAddNoOverflowExpression): Expr = expr.run {
+    override fun visit(expr: UtAddNoOverflowExpression): Expr<*> = expr.run {
         z3Context.mkBVAddNoOverflow(translate(expr.left) as BitVecExpr, translate(expr.right) as BitVecExpr, true)
     }
 
-    override fun visit(expr: UtSubNoOverflowExpression): Expr = expr.run {
+    override fun visit(expr: UtSubNoOverflowExpression): Expr<*> = expr.run {
         // For some reason mkBVSubNoOverflow does not take "signed" as an argument, yet still works for signed integers
         z3Context.mkBVSubNoOverflow(translate(expr.left) as BitVecExpr, translate(expr.right) as BitVecExpr) // , true)
     }
 
-    override fun visit(expr: UtNegExpression): Expr = expr.run {
+    override fun visit(expr: UtNegExpression): Expr<*> = expr.run {
         negate(z3Context, translate(variable.expr).z3Variable(variable.type))
     }
 
-    override fun visit(expr: UtCastExpression): Expr = expr.run {
+    override fun visit(expr: UtCastExpression): Expr<*> = expr.run {
         val z3var = translate(variable.expr).z3Variable(variable.type)
         z3Context.convertVar(z3var, type).expr
     }
 
-    override fun visit(expr: UtBoolOpExpression): Expr = expr.run {
+    override fun visit(expr: UtBoolOpExpression): Expr<*> = expr.run {
         val leftResolve = translate(left.expr).z3Variable(left.type)
         val rightResolve = translate(right.expr).z3Variable(right.type)
         operator.delegate(z3Context, leftResolve, rightResolve)
@@ -154,7 +148,7 @@ open class Z3TranslatorVisitor(
      * @see UtIsExpression
      * @see UtSettings.maxTypeNumberForEnumeration
      */
-    override fun visit(expr: UtIsExpression): Expr = expr.run {
+    override fun visit(expr: UtIsExpression): Expr<*> = expr.run {
         val symNumDimensions = translate(typeRegistry.symNumDimensions(addr)) as BitVecExpr
         val symTypeId = translate(typeRegistry.symTypeId(addr)) as BitVecExpr
 
@@ -199,7 +193,7 @@ open class Z3TranslatorVisitor(
 
     }
 
-    override fun visit(expr: UtGenericExpression): Expr = expr.run {
+    override fun visit(expr: UtGenericExpression): Expr<*> = expr.run {
         val constraints = mutableListOf<BoolExpr>()
         for (i in types.indices) {
             val symType = translate(typeRegistry.genericTypeId(addr, i))
@@ -227,7 +221,7 @@ open class Z3TranslatorVisitor(
         )
     }
 
-    private fun encodePossibleTypes(symType: Expr, possibleConcreteTypes: Collection<Type>): BoolExpr {
+    private fun encodePossibleTypes(symType: Expr<*>, possibleConcreteTypes: Collection<Type>): BoolExpr {
         val possibleBaseTypes = possibleConcreteTypes.map { it.baseType }
 
         return if (!useBitVecBasedTypeSystem || possibleConcreteTypes.size < maxTypeNumberForEnumeration) {
@@ -256,7 +250,7 @@ open class Z3TranslatorVisitor(
         }
     }
 
-    override fun visit(expr: UtIsGenericTypeExpression): Expr = expr.run {
+    override fun visit(expr: UtIsGenericTypeExpression): Expr<*> = expr.run {
         val symType = translate(typeRegistry.symTypeId(addr))
         val symNumDimensions = translate(typeRegistry.symNumDimensions(addr))
 
@@ -278,7 +272,7 @@ open class Z3TranslatorVisitor(
         z3Context.mkAnd(typeConstraint, dimensionsConstraint)
     }
 
-    override fun visit(expr: UtEqGenericTypeParametersExpression): Expr = expr.run {
+    override fun visit(expr: UtEqGenericTypeParametersExpression): Expr<*> = expr.run {
         val constraints = mutableListOf<BoolExpr>()
         for ((i, j) in indexMapping) {
             val firstSymType = translate(typeRegistry.genericTypeId(firstAddr, i))
@@ -292,15 +286,15 @@ open class Z3TranslatorVisitor(
         z3Context.mkAnd(*constraints.toTypedArray())
     }
 
-    override fun visit(expr: UtInstanceOfExpression): Expr =
+    override fun visit(expr: UtInstanceOfExpression): Expr<*> =
         expr.run { translate(expr.constraint) }
 
-    override fun visit(expr: UtIteExpression): Expr =
+    override fun visit(expr: UtIteExpression): Expr<*> =
         expr.run { z3Context.mkITE(translate(condition) as BoolExpr, translate(thenExpr), translate(elseExpr)) }
 
-    override fun visit(expr: UtMkTermArrayExpression): Expr = expr.run {
+    override fun visit(expr: UtMkTermArrayExpression): Expr<*> = expr.run {
         z3Context.run {
-            val ourArray = translate(expr.array) as ArrayExpr
+            val ourArray = translate(expr.array) as ArrayExpr<*, *>
             val arraySort = expr.array.sort
             val defaultValue = expr.defaultValue ?: arraySort.itemSort.defaultValue
             val translated = translate(defaultValue)
@@ -316,19 +310,19 @@ open class Z3TranslatorVisitor(
             mkBV2Int(translate(expr) as BitVecExpr, true)
         }
 
-    override fun visit(expr: UtArrayInsert): Expr = error("translate of UtArrayInsert expression")
+    override fun visit(expr: UtArrayInsert): Expr<*> = error("translate of UtArrayInsert expression")
 
-    override fun visit(expr: UtArrayInsertRange): Expr = error("translate of UtArrayInsertRange expression")
+    override fun visit(expr: UtArrayInsertRange): Expr<*> = error("translate of UtArrayInsertRange expression")
 
-    override fun visit(expr: UtArrayRemove): Expr = error("translate of UtArrayRemove expression")
+    override fun visit(expr: UtArrayRemove): Expr<*> = error("translate of UtArrayRemove expression")
 
-    override fun visit(expr: UtArrayRemoveRange): Expr = error("translate of UtArrayRemoveRange expression")
+    override fun visit(expr: UtArrayRemoveRange): Expr<*> = error("translate of UtArrayRemoveRange expression")
 
-    override fun visit(expr: UtArraySetRange): Expr = error("translate of UtArraySetRange expression")
+    override fun visit(expr: UtArraySetRange): Expr<*> = error("translate of UtArraySetRange expression")
 
-    override fun visit(expr: UtArrayShiftIndexes): Expr = error("translate of UtArrayShiftIndexes expression")
+    override fun visit(expr: UtArrayShiftIndexes): Expr<*> = error("translate of UtArrayShiftIndexes expression")
 
-    override fun visit(expr: UtArrayApplyForAll): Expr = error("translate of UtArrayApplyForAll expression")
+    override fun visit(expr: UtArrayApplyForAll): Expr<*> = error("translate of UtArrayApplyForAll expression")
 
 
 }
\ No newline at end of file
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt
index 7fc3dc0904..179bf82133 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Extensions.kt
@@ -32,15 +32,15 @@ import soot.Type
 private val Z3Variable.unsigned: Boolean
     get() = this.type is CharType
 
-fun Expr.value(unsigned: Boolean = false): Any = when (this) {
+fun Expr<*>.value(unsigned: Boolean = false): Any = when (this) {
     is BitVecNum -> this.toIntNum(unsigned)
     is FPNum -> this.toFloatingPointNum()
     is BoolExpr -> this.boolValue == Z3_lbool.Z3_L_TRUE
-    is SeqExpr -> convertSolverString(this.string)
+    is SeqExpr<*> -> convertSolverString(this.string)
     else -> error("${this::class}: $this")
 }
 
-internal fun Expr.intValue() = this.value() as Int
+internal fun Expr<*>.intValue() = this.value() as Int
 
 /**
  * Converts a variable to given type.
@@ -64,7 +64,7 @@ fun Context.convertVar(variable: Z3Variable, toType: Type): Z3Variable {
  *
  * @throws IllegalStateException if given expression cannot be convert to given sort
  */
-internal fun Context.convertVar(variable: Z3Variable, sort: Sort): Expr {
+internal fun Context.convertVar(variable: Z3Variable, sort: Sort): Expr<*> {
     val expr = variable.expr
     return when {
         sort == expr.sort -> expr
@@ -94,7 +94,7 @@ internal fun Context.convertVar(variable: Z3Variable, sort: Sort): Expr {
  * - convert to int for other types, with second step conversion by taking lowest bits
  * (can lead to significant changes if value outside of target type range).
  */
-private fun Context.convertFPtoBV(variable: Z3Variable, sortSize: Int): Expr = when (sortSize) {
+private fun Context.convertFPtoBV(variable: Z3Variable, sortSize: Int): Expr<*> = when (sortSize) {
     Long.SIZE_BITS -> convertFPtoBV(variable, sortSize, Long.MIN_VALUE, Long.MAX_VALUE)
     else -> doNarrowConversion(
         convertFPtoBV(variable, Int.SIZE_BITS, Int.MIN_VALUE, Int.MAX_VALUE) as BitVecExpr,
@@ -105,7 +105,7 @@ private fun Context.convertFPtoBV(variable: Z3Variable, sortSize: Int): Expr = w
 /**
  * Converts FP to BV covering special cases for NaN, Infinity and values outside of [minValue, maxValue] range.
  */
-private fun Context.convertFPtoBV(variable: Z3Variable, sortSize: Int, minValue: Number, maxValue: Number): Expr =
+private fun Context.convertFPtoBV(variable: Z3Variable, sortSize: Int, minValue: Number, maxValue: Number): Expr<*> =
     mkITE(
         mkFPIsNaN(variable.expr as FPExpr), makeConst(0, mkBitVecSort(sortSize)),
         mkITE(
@@ -128,7 +128,7 @@ internal fun Context.doNarrowConversion(expr: BitVecExpr, sortSize: Int): BitVec
 /**
  * Converts a constant value to Z3 constant of given sort - BitVec or FP.
  */
-fun Context.makeConst(const: Number, sort: Sort): Expr = when (sort) {
+fun Context.makeConst(const: Number, sort: Sort): Expr<*> = when (sort) {
     is BitVecSort -> this.makeBV(const, sort.size)
     is FPSort -> this.makeFP(const, sort)
     else -> error("Wrong sort $sort")
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Operators.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Operators.kt
index 01ed0cb2e6..38f120c674 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Operators.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Operators.kt
@@ -15,9 +15,9 @@ import soot.CharType
 import soot.IntType
 import soot.ShortType
 
-typealias BinOperator = Operator<out Expr>
+typealias BinOperator = Operator<out Expr<*>>
 
-sealed class Operator<T : Expr>(
+sealed class Operator<T : Expr<*>>(
     val onBitVec: (Context, BitVecExpr, BitVecExpr) -> T,
     val onFP: (Context, FPExpr, FPExpr) -> T = { _, _, _ -> TODO() },
     val onBool: (Context, BoolExpr, BoolExpr) -> T = { _, _, _ -> TODO() }
@@ -32,7 +32,7 @@ sealed class Operator<T : Expr>(
             doAction(context, aleft, aright)
         }
 
-    protected fun doAction(context: Context, left: Expr, right: Expr): T = when {
+    protected fun doAction(context: Context, left: Expr<*>, right: Expr<*>): T = when {
         left is BitVecExpr && right is BitVecExpr -> onBitVec(context, left, right)
         left is FPExpr && right is FPExpr -> onFP(context, left, right)
         left is BoolExpr && right is BoolExpr -> onBool(context, left, right)
@@ -55,7 +55,7 @@ object Gt : BoolOperator(Context::mkBVSGT, Context::mkFPGt)
 object Eq : BoolOperator(Context::mkEq, Context::mkFPEq, Context::mkEq)
 object Ne : BoolOperator(::ne, ::fpNe, ::ne)
 
-private fun ne(context: Context, left: Expr, right: Expr): BoolExpr = context.mkNot(context.mkEq(left, right))
+private fun ne(context: Context, left: Expr<*>, right: Expr<*>): BoolExpr = context.mkNot(context.mkEq(left, right))
 private fun fpNe(context: Context, left: FPExpr, right: FPExpr): BoolExpr = context.mkNot(context.mkFPEq(left, right))
 
 internal object Rem : BinOperator(Context::mkBVSRem, Context::mkFPRem)
@@ -129,7 +129,7 @@ internal object Cmp : BinOperator(::bvCmp, ::fpCmp)
 internal object Cmpl : BinOperator(::bvCmp, ::fpCmpl)
 internal object Cmpg : BinOperator(::bvCmp, ::fpCmpg)
 
-private fun bvCmp(context: Context, left: BitVecExpr, right: BitVecExpr): Expr =
+private fun bvCmp(context: Context, left: BitVecExpr, right: BitVecExpr): Expr<*> =
     context.mkITE(
         context.mkBVSLE(left, right),
         context.mkITE(context.mkEq(left, right), context.mkBV(0, 32), context.mkBV(-1, 32)),
@@ -146,7 +146,7 @@ private fun fpCmp(context: Context, left: FPExpr, right: FPExpr) =
         context.mkBV(1, 32)
     )
 
-private fun fpCmpl(context: Context, left: FPExpr, right: FPExpr): Expr =
+private fun fpCmpl(context: Context, left: FPExpr, right: FPExpr): Expr<*> =
     context.mkITE(
         context.mkOr(context.mkFPIsNaN(left), context.mkFPIsNaN(right)), context.mkBV(-1, 32),
         context.mkITE(
@@ -156,7 +156,7 @@ private fun fpCmpl(context: Context, left: FPExpr, right: FPExpr): Expr =
         )
     )
 
-private fun fpCmpg(context: Context, left: FPExpr, right: FPExpr): Expr =
+private fun fpCmpg(context: Context, left: FPExpr, right: FPExpr): Expr<*> =
     context.mkITE(
         context.mkOr(context.mkFPIsNaN(left), context.mkFPIsNaN(right)), context.mkBV(1, 32),
         context.mkITE(
@@ -166,7 +166,7 @@ private fun fpCmpg(context: Context, left: FPExpr, right: FPExpr): Expr =
         )
     )
 
-fun negate(context: Context, variable: Z3Variable): Expr = when (variable.expr) {
+fun negate(context: Context, variable: Z3Variable): Expr<*> = when (variable.expr) {
     is BitVecExpr -> context.mkBVNeg(context.alignVar(variable).expr as BitVecExpr)
     is FPExpr -> context.mkFPNeg(variable.expr)
     is BoolExpr -> context.mkNot(variable.expr)
@@ -183,7 +183,7 @@ fun negate(context: Context, variable: Z3Variable): Expr = when (variable.expr)
  * @see <a href="https://docs.oracle.com/javase/specs/jls/se11/html/jls-5.html#jls-5.6.2">
  * Java Language Specification: Binary Numeric Promotion</a>
  */
-fun Context.alignVars(left: Z3Variable, right: Z3Variable): Pair<Expr, Expr> {
+fun Context.alignVars(left: Z3Variable, right: Z3Variable): Pair<Expr<*>, Expr<*>> {
     val maxSort = maxOf(left.expr.sort, right.expr.sort, mkBitVecSort(Int.SIZE_BITS), compareBy { it.rank() })
     return convertVar(left, maxSort) to convertVar(right, maxSort)
 }
@@ -198,7 +198,7 @@ fun Context.alignVars(left: Z3Variable, right: Z3Variable): Pair<Expr, Expr> {
  * @see <a href="https://docs.oracle.com/javase/specs/jls/se11/html/jls-5.html#jls-5.6.2">
  * Java Language Specification: Binary Numeric Promotion</a>
  */
-internal fun Context.alignVarAndConst(left: Z3Variable, right: Number): Pair<Expr, Expr> {
+internal fun Context.alignVarAndConst(left: Z3Variable, right: Number): Pair<Expr<*>, Expr<*>> {
     val maxSort = maxOf(left.expr.sort, toSort(right), mkBitVecSort(Int.SIZE_BITS), compareBy { it.rank() })
     return convertVar(left, maxSort) to makeConst(right, maxSort)
 }
diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt
index 97677c78cd..797273ce84 100644
--- a/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt
+++ b/utbot-framework/src/main/kotlin/org/utbot/engine/z3/Z3initializer.kt
@@ -21,7 +21,7 @@ abstract class Z3Initializer : AutoCloseable {
     companion object {
         private val libraries = listOf("libz3", "libz3java")
         private val vcWinLibrariesToLoadBefore = listOf("vcruntime140", "vcruntime140_1")
-        private val supportedArchs = setOf("amd64", "x86_64")
+        private val supportedArchs = setOf("amd64", "x86_64", "aarch64")
         private val initializeCallback by lazy {
             System.setProperty("z3.skipLibraryLoad", "true")
             val arch = System.getProperty("os.arch")
diff --git a/utbot-framework/src/main/kotlin/org/z3/Z3Extension.kt b/utbot-framework/src/main/kotlin/org/z3/Z3Extension.kt
index 39fb296e85..ad63ebc5d5 100644
--- a/utbot-framework/src/main/kotlin/org/z3/Z3Extension.kt
+++ b/utbot-framework/src/main/kotlin/org/z3/Z3Extension.kt
@@ -5,7 +5,7 @@ package com.microsoft.z3
 import java.lang.Integer.parseUnsignedInt
 import java.lang.Long.parseUnsignedLong
 
-fun Model.eval(expr: Expr): Expr = this.eval(expr, true)
+fun Model.eval(expr: Expr<*>): Expr<*> = this.eval(expr, true)
 
 fun BitVecNum.toIntNum(unsigned: Boolean = false): Any = when (sortSize) {
     Byte.SIZE_BITS -> parseUnsignedLong(this.toBinaryString(), 2).toByte()
@@ -44,7 +44,7 @@ fun FPNum.toFloatingPointNum(): Number = when (sort) {
     else -> error("Unknown type: $sort")
 }
 
-fun Context.mkSeqNth(s: SeqExpr, index: Expr): Expr {
+fun Context.mkSeqNth(s: SeqExpr<*>, index: Expr<*>): Expr<*> {
     this.checkContextMatch(s, index)
     return Expr.create(this, Native.mkSeqNth(nCtx(), s.nativeObject, index.nativeObject))
 }
\ No newline at end of file
diff --git a/utbot-testing/build.gradle b/utbot-testing/build.gradle
index e55cd6e59e..7b72db1e63 100644
--- a/utbot-testing/build.gradle
+++ b/utbot-testing/build.gradle
@@ -32,7 +32,6 @@ dependencies {
     }
 
     implementation group: 'com.fasterxml.jackson.module', name: 'jackson-module-kotlin', version: jacksonVersion
-    implementation group: 'org.sosy-lab', name: 'javasmt-solver-z3', version: javasmtSolverZ3Version
     implementation group: 'com.github.curious-odd-man', name: 'rgxgen', version: rgxgenVersion
     implementation group: 'org.apache.logging.log4j', name: 'log4j-slf4j-impl', version: log4j2Version
     implementation group: 'io.github.microutils', name: 'kotlin-logging', version: kotlinLoggingVersion
@@ -58,4 +57,7 @@ dependencies {
 
     testImplementation group: 'org.mockito', name: 'mockito-inline', version: mockitoInlineVersion
     testImplementation group: 'org.apache.logging.log4j', name: 'log4j-core', version: log4j2Version
+
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-core', version: ksmtVersion
+    implementation group: 'com.github.UnitTestBot.ksmt', name: 'ksmt-z3', version: ksmtVersion
 }
\ No newline at end of file