diff --git a/README.md b/README.md
index 64512b5ae..b61dcbd3e 100644
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.15)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.16)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.15")
+implementation("io.ksmt:ksmt-core:0.5.16")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.15")
+implementation("io.ksmt:ksmt-z3:0.5.16")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 
diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
index b7cbe44d7..211aded43 100644
--- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
+++ b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.15"
+version = "0.5.16"
 
 repositories {
     mavenCentral()
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 41446e121..319fd5871 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.15")    
+    implementation("io.ksmt:ksmt-core:0.5.16")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.15")
+    implementation("io.ksmt:ksmt-z3:0.5.16")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.15")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.16")
 }
 ```
 
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index 0189ef167..f6d3cae66 100644
--- a/examples/build.gradle.kts
+++ b/examples/build.gradle.kts
@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.15")
+    implementation("io.ksmt:ksmt-core:0.5.16")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.15")
+    implementation("io.ksmt:ksmt-z3:0.5.16")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.15")
+    implementation("io.ksmt:ksmt-runner:0.5.16")
 }
 
 java {
diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
index 5938f1e19..322d90569 100644
--- a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
+++ b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
@@ -493,24 +493,21 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
         transform { if (value) bitwuzlaCtx.trueTerm else bitwuzlaCtx.falseTerm }
     }
 
-    override fun transform(expr: KBitVec8Value): KExpr<KBv8Sort> = transformBv32Number(expr)
-    override fun transform(expr: KBitVec16Value): KExpr<KBv16Sort> = transformBv32Number(expr)
-    override fun transform(expr: KBitVec32Value): KExpr<KBv32Sort> = transformBv32Number(expr)
-    override fun transform(expr: KBitVec64Value): KExpr<KBv64Sort> = transformBv64Number(expr)
+    override fun transform(expr: KBitVec8Value): KExpr<KBv8Sort> = transformBv32Number(expr, expr.byteValue.toInt())
+    override fun transform(expr: KBitVec16Value): KExpr<KBv16Sort> = transformBv32Number(expr, expr.shortValue.toInt())
+    override fun transform(expr: KBitVec32Value): KExpr<KBv32Sort> = transformBv32Number(expr, expr.intValue)
+    override fun transform(expr: KBitVec64Value): KExpr<KBv64Sort> = transformBv64Number(expr, expr.longValue)
 
-    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv32Number(expr: T): T = with(expr) {
+    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv32Number(expr: T, value: Int): T = with(expr) {
         transform {
-            Native.bitwuzlaMkBvValueUint32(
-                bitwuzla,
-                sort.internalizeSort(),
-                numberValue.toInt()
-            ).also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
+            Native.bitwuzlaMkBvValueUint32(bitwuzla, sort.internalizeSort(), value)
+                .also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
         }
     }
 
-    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv64Number(expr: T): T = with(expr) {
+    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv64Number(expr: T, value: Long): T = with(expr) {
         transform {
-            transformBvLongNumber(numberValue.toLong(), sort.sizeBits.toInt())
+            transformBvLongNumber(value, sort.sizeBits.toInt())
                 .also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
         }
     }
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/KBitVecExprs.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/KBitVecExprs.kt
index 7d9868384..f896c363f 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/KBitVecExprs.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/KBitVecExprs.kt
@@ -22,7 +22,7 @@ abstract class KBitVecValue<S : KBvSort>(ctx: KContext) : KInterpretedValue<S>(c
 
 class KBitVec1Value internal constructor(
     ctx: KContext,
-    val value: Boolean
+    @JvmField val value: Boolean
 ) : KBitVecValue<KBv1Sort>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv1Sort> = transformer.transform(this)
 
@@ -50,7 +50,7 @@ abstract class KBitVecNumberValue<S : KBvSort, N : Number>(ctx: KContext) : KBit
 
 class KBitVec8Value internal constructor(
     ctx: KContext,
-    val byteValue: Byte
+    @JvmField val byteValue: Byte
 ) : KBitVecNumberValue<KBv8Sort, Byte>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv8Sort> = transformer.transform(this)
 
@@ -58,7 +58,7 @@ class KBitVec8Value internal constructor(
         get() = byteValue
 
     override val decl: KDecl<KBv8Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(byteValue)
 
     override val sort: KBv8Sort = ctx.bv8Sort
 
@@ -68,7 +68,7 @@ class KBitVec8Value internal constructor(
 
 class KBitVec16Value internal constructor(
     ctx: KContext,
-    val shortValue: Short
+    @JvmField val shortValue: Short
 ) : KBitVecNumberValue<KBv16Sort, Short>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv16Sort> = transformer.transform(this)
 
@@ -76,7 +76,7 @@ class KBitVec16Value internal constructor(
         get() = shortValue
 
     override val decl: KDecl<KBv16Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(shortValue)
 
     override val sort: KBv16Sort = ctx.bv16Sort
 
@@ -86,7 +86,7 @@ class KBitVec16Value internal constructor(
 
 class KBitVec32Value internal constructor(
     ctx: KContext,
-    val intValue: Int
+    @JvmField val intValue: Int
 ) : KBitVecNumberValue<KBv32Sort, Int>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv32Sort> = transformer.transform(this)
 
@@ -94,7 +94,7 @@ class KBitVec32Value internal constructor(
         get() = intValue
 
     override val decl: KDecl<KBv32Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(intValue)
 
     override val sort: KBv32Sort = ctx.bv32Sort
 
@@ -104,7 +104,7 @@ class KBitVec32Value internal constructor(
 
 class KBitVec64Value internal constructor(
     ctx: KContext,
-    val longValue: Long
+    @JvmField val longValue: Long
 ) : KBitVecNumberValue<KBv64Sort, Long>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv64Sort> = transformer.transform(this)
 
@@ -112,7 +112,7 @@ class KBitVec64Value internal constructor(
         get() = longValue
 
     override val decl: KDecl<KBv64Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(longValue)
 
     override val sort: KBv64Sort = ctx.bv64Sort
 
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/BvUtils.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/BvUtils.kt
index 682af33b6..3723689b9 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/utils/BvUtils.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/BvUtils.kt
@@ -29,9 +29,11 @@ object BvUtils {
             powerOfTwo(size - 1u)
     }
 
+    @JvmStatic
     fun <T : KBvSort> KContext.bvMinValueSigned(size: UInt): KBitVecValue<T> =
         mkBvSpecialValue(size, bvMinValueSigned)
 
+    @JvmStatic
     fun KBitVecValue<*>.isBvMinValueSigned(): Boolean = isBvSpecialValue(bvMinValueSigned)
 
     private val bvMaxValueSigned = object : BvSpecialValueSource {
@@ -45,9 +47,11 @@ object BvUtils {
             powerOfTwo(size - 1u) - BigInteger.ONE
     }
 
+    @JvmStatic
     fun <T : KBvSort> KContext.bvMaxValueSigned(size: UInt): KBitVecValue<T> =
         mkBvSpecialValue(size, bvMaxValueSigned)
 
+    @JvmStatic
     fun KBitVecValue<*>.isBvMaxValueSigned(): Boolean = isBvSpecialValue(bvMaxValueSigned)
 
     private val bvMaxValueUnsigned = object : BvSpecialValueSource {
@@ -61,9 +65,11 @@ object BvUtils {
             powerOfTwo(size) - BigInteger.ONE
     }
 
+    @JvmStatic
     fun <T : KBvSort> KContext.bvMaxValueUnsigned(size: UInt): KBitVecValue<T> =
         mkBvSpecialValue(size, bvMaxValueUnsigned)
 
+    @JvmStatic
     fun KBitVecValue<*>.isBvMaxValueUnsigned(): Boolean = isBvSpecialValue(bvMaxValueUnsigned)
 
     private val bvZeroValue = object : BvSpecialValueSource {
@@ -76,9 +82,11 @@ object BvUtils {
         override fun bvDefault(size: UInt): BigInteger = BigInteger.ZERO
     }
 
+    @JvmStatic
     fun <T : KBvSort> KContext.bvZero(size: UInt): KBitVecValue<T> =
         mkBvSpecialValue(size, bvZeroValue)
 
+    @JvmStatic
     fun KBitVecValue<*>.isBvZero(): Boolean = isBvSpecialValue(bvZeroValue)
 
     private val bvOneValue = object : BvSpecialValueSource {
@@ -91,9 +99,11 @@ object BvUtils {
         override fun bvDefault(size: UInt): BigInteger = BigInteger.ONE
     }
 
+    @JvmStatic
     fun <T : KBvSort> KContext.bvOne(size: UInt): KBitVecValue<T> =
         mkBvSpecialValue(size, bvOneValue)
 
+    @JvmStatic
     fun KBitVecValue<*>.isBvOne(): Boolean = isBvSpecialValue(bvOneValue)
 
     private class BvIntValue(val value: Int) : BvSpecialValueSource {
@@ -107,11 +117,14 @@ object BvUtils {
             value.toBigInteger().normalizeValue(size)
     }
 
+    @JvmStatic
     fun <T : KBvSort> KContext.bvValue(size: UInt, value: Int): KBitVecValue<T> =
         mkBvSpecialValue(size, BvIntValue(value))
 
+    @JvmStatic
     fun KBitVecValue<*>.bvValueIs(value: Int): Boolean = isBvSpecialValue(BvIntValue(value))
 
+    @JvmStatic
     fun KBitVecValue<*>.getBit(bit: UInt): Boolean {
         check(bit < sort.sizeBits) { "Requested bit is out of bounds for $sort" }
         return when (this) {
@@ -122,8 +135,10 @@ object BvUtils {
         }
     }
 
+    @JvmStatic
     fun KBitVecValue<*>.signBit(): Boolean = getBit(sort.sizeBits - 1u)
 
+    @JvmStatic
     fun KBitVecValue<*>.signedGreaterOrEqual(other: Int): Boolean = when (this) {
         is KBitVec1Value -> if (value) {
             // 1 >= 1 -> true
@@ -135,33 +150,34 @@ object BvUtils {
             true
         }
 
-        is KBitVec8Value -> numberValue >= other
-        is KBitVec16Value -> numberValue >= other
-        is KBitVec32Value -> numberValue >= other
-        is KBitVec64Value -> numberValue >= other
+        is KBitVec8Value -> byteValue >= other
+        is KBitVec16Value -> shortValue >= other
+        is KBitVec32Value -> intValue >= other
+        is KBitVec64Value -> longValue >= other
         is KBitVecCustomValue -> value.signedValue(sizeBits) >= other.toBigInteger()
         else -> stringValue.toBigInteger(radix = 2).signedValue(sort.sizeBits) >= other.toBigInteger()
     }
 
-    fun KBitVecValue<*>.signedLessOrEqual(other: KBitVecValue<*>): Boolean = when (this) {
-        is KBitVec1Value -> if (value) {
+    @JvmStatic
+    @Suppress("ComplexMethod")
+    fun KBitVecValue<*>.signedLessOrEqual(other: KBitVecValue<*>): Boolean = when {
+        this is KBitVec1Value && other is KBitVec1Value -> if (value) {
             // 1 <= 0 -> true
             // 1 <= 1 -> true
             true
         } else {
             // 0 <= 1 -> false
             // 0 <= 0 -> true
-            val otherValue = (other as KBitVec1Value).value
-            !otherValue
+            !other.value
         }
 
-        is KBitVec8Value -> numberValue <= (other as KBitVec8Value).numberValue
-        is KBitVec16Value -> numberValue <= (other as KBitVec16Value).numberValue
-        is KBitVec32Value -> numberValue <= (other as KBitVec32Value).numberValue
-        is KBitVec64Value -> numberValue <= (other as KBitVec64Value).numberValue
-        is KBitVecCustomValue -> {
+        this is KBitVec8Value && other is KBitVec8Value -> byteValue <= other.byteValue
+        this is KBitVec16Value && other is KBitVec16Value -> shortValue <= other.shortValue
+        this is KBitVec32Value && other is KBitVec32Value -> intValue <= other.intValue
+        this is KBitVec64Value && other is KBitVec64Value -> longValue <= other.longValue
+        this is KBitVecCustomValue && other is KBitVecCustomValue -> {
             val lhs = value.signedValue(sizeBits)
-            val rhs = (other as KBitVecCustomValue).value.signedValue(sizeBits)
+            val rhs = other.value.signedValue(sizeBits)
             lhs <= rhs
         }
 
@@ -172,35 +188,43 @@ object BvUtils {
         }
     }
 
-    fun KBitVecValue<*>.unsignedLessOrEqual(other: KBitVecValue<*>): Boolean = when (this) {
-        is KBitVec1Value -> value <= (other as KBitVec1Value).value
-        is KBitVec8Value -> numberValue.toUByte() <= (other as KBitVec8Value).numberValue.toUByte()
-        is KBitVec16Value -> numberValue.toUShort() <= (other as KBitVec16Value).numberValue.toUShort()
-        is KBitVec32Value -> numberValue.toUInt() <= (other as KBitVec32Value).numberValue.toUInt()
-        is KBitVec64Value -> numberValue.toULong() <= (other as KBitVec64Value).numberValue.toULong()
-        is KBitVecCustomValue -> value <= (other as KBitVecCustomValue).value
+    @JvmStatic
+    fun KBitVecValue<*>.unsignedLessOrEqual(other: KBitVecValue<*>): Boolean = when {
+        this is KBitVec1Value && other is KBitVec1Value -> value <= other.value
+        this is KBitVec8Value && other is KBitVec8Value -> byteValue.toUByte() <= other.byteValue.toUByte()
+        this is KBitVec16Value && other is KBitVec16Value -> shortValue.toUShort() <= other.shortValue.toUShort()
+        this is KBitVec32Value && other is KBitVec32Value -> intValue.toUInt() <= other.intValue.toUInt()
+        this is KBitVec64Value && other is KBitVec64Value -> longValue.toULong() <= other.longValue.toULong()
+        this is KBitVecCustomValue && other is KBitVecCustomValue -> value <= other.value
         // MSB first -> lexical order works
         else -> stringValue <= other.stringValue
     }
 
+    @JvmStatic
     fun KBitVecValue<*>.signedLess(other: KBitVecValue<*>): Boolean =
         signedLessOrEqual(other) && this != other
 
+    @JvmStatic
     fun KBitVecValue<*>.unsignedLess(other: KBitVecValue<*>): Boolean =
         unsignedLessOrEqual(other) && this != other
 
+    @JvmStatic
     fun KBitVecValue<*>.signedGreaterOrEqual(other: KBitVecValue<*>): Boolean =
         other.signedLessOrEqual(this)
 
+    @JvmStatic
     fun KBitVecValue<*>.unsignedGreaterOrEqual(other: KBitVecValue<*>): Boolean =
         other.unsignedLessOrEqual(this)
 
+    @JvmStatic
     fun KBitVecValue<*>.signedGreater(other: KBitVecValue<*>): Boolean =
         other.signedLess(this)
 
+    @JvmStatic
     fun KBitVecValue<*>.unsignedGreater(other: KBitVecValue<*>): Boolean =
         other.unsignedLess(this)
 
+    @JvmStatic
     operator fun <T : KBvSort> KBitVecValue<T>.unaryMinus(): KBitVecValue<T> = bvOperation(
         other = this,
         bv1 = { a, _ -> a xor false },
@@ -211,6 +235,7 @@ object BvUtils {
         bvDefault = { a, _ -> -a },
     )
 
+    @JvmStatic
     operator fun <T : KBvSort> KBitVecValue<T>.plus(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         bv1 = { a, b -> a xor b },
@@ -221,6 +246,7 @@ object BvUtils {
         bvDefault = { a, b -> a + b },
     )
 
+    @JvmStatic
     operator fun <T : KBvSort> KBitVecValue<T>.minus(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         bv1 = { a, b -> a xor b },
@@ -231,6 +257,7 @@ object BvUtils {
         bvDefault = { a, b -> a - b },
     )
 
+    @JvmStatic
     operator fun <T : KBvSort> KBitVecValue<T>.times(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         bv1 = { a, b -> a && b },
@@ -241,6 +268,7 @@ object BvUtils {
         bvDefault = { a, b -> a * b },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.signedDivide(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         signIsImportant = true,
@@ -252,6 +280,7 @@ object BvUtils {
         bvDefault = { a, b -> a / b },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.unsignedDivide(other: KBitVecValue<T>): KBitVecValue<T> = bvUnsignedOperation(
         other = other,
         bv1 = { a, _ -> a },
@@ -262,6 +291,7 @@ object BvUtils {
         bvDefault = { a, b -> a / b },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.signedRem(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         signIsImportant = true,
@@ -273,6 +303,7 @@ object BvUtils {
         bvDefault = { a, b -> a.rem(b) },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.unsignedRem(other: KBitVecValue<T>): KBitVecValue<T> = bvUnsignedOperation(
         other = other,
         bv1 = { _, _ -> false },
@@ -283,6 +314,7 @@ object BvUtils {
         bvDefault = { a, b -> a.rem(b) },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.signedMod(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         signIsImportant = true,
@@ -306,6 +338,7 @@ object BvUtils {
         },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.bitwiseNot(): KBitVecValue<T> = bvOperation(
         other = this,
         bv1 = { a, _ -> a.not() },
@@ -316,6 +349,7 @@ object BvUtils {
         bvDefault = { a, _ -> a.inv() },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.bitwiseOr(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         bv1 = { a, b -> a || b },
@@ -326,6 +360,7 @@ object BvUtils {
         bvDefault = { a, b -> a or b },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.bitwiseXor(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         bv1 = { a, b -> a xor b },
@@ -336,6 +371,7 @@ object BvUtils {
         bvDefault = { a, b -> a xor b },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.bitwiseAnd(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         bv1 = { a, b -> a && b },
@@ -351,6 +387,7 @@ object BvUtils {
     private val bv32PossibleShift = 0 until Int.SIZE_BITS
     private val bv64PossibleShift = 0 until Long.SIZE_BITS
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.shiftLeft(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         bv1 = { a, b -> if (b) false else a },
@@ -367,6 +404,7 @@ object BvUtils {
         },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.shiftRightLogical(other: KBitVecValue<T>): KBitVecValue<T> = bvUnsignedOperation(
         other = other,
         bv1 = { a, b -> if (b) false else a },
@@ -383,6 +421,7 @@ object BvUtils {
         },
     )
 
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.shiftRightArith(other: KBitVecValue<T>): KBitVecValue<T> = bvOperation(
         other = other,
         signIsImportant = true,
@@ -400,6 +439,7 @@ object BvUtils {
         },
     )
 
+    @JvmStatic
     fun KBitVecValue<*>.powerOfTwoOrNull(): Int? {
         val value = bigIntValue()
         val valueMinusOne = value - BigInteger.ONE
@@ -407,6 +447,7 @@ object BvUtils {
         return valueMinusOne.bitLength()
     }
 
+    @JvmStatic
     fun KBitVecValue<*>.bigIntValue(): BigInteger = when (this) {
         is KBitVec1Value -> if (value) BigInteger.ONE else BigInteger.ZERO
         is KBitVecNumberValue<*, *> -> numberValue.toBigInteger()
@@ -414,29 +455,32 @@ object BvUtils {
         else -> stringValue.toBigInteger(radix = 2)
     }
 
+    @JvmStatic
     fun KBitVecValue<*>.toBigIntegerSigned(): BigInteger =
         toBigIntegerUnsigned().signedValue(sort.sizeBits)
 
+    @JvmStatic
     fun KBitVecValue<*>.toBigIntegerUnsigned(): BigInteger =
         bigIntValue().normalizeValue(sort.sizeBits)
 
+    @JvmStatic
     fun concatBv(lhs: KBitVecValue<*>, rhs: KBitVecValue<*>): KBitVecValue<*> = with(lhs.ctx) {
         when {
             lhs is KBitVec8Value && rhs is KBitVec8Value -> {
-                var result = lhs.numberValue.toUByte().toInt() shl Byte.SIZE_BITS
-                result = result or rhs.numberValue.toUByte().toInt()
+                var result = lhs.byteValue.toUByte().toInt() shl Byte.SIZE_BITS
+                result = result or rhs.byteValue.toUByte().toInt()
                 mkBv(result.toShort())
             }
 
             lhs is KBitVec16Value && rhs is KBitVec16Value -> {
-                var result = lhs.numberValue.toUShort().toInt() shl Short.SIZE_BITS
-                result = result or rhs.numberValue.toUShort().toInt()
+                var result = lhs.shortValue.toUShort().toInt() shl Short.SIZE_BITS
+                result = result or rhs.shortValue.toUShort().toInt()
                 mkBv(result)
             }
 
             lhs is KBitVec32Value && rhs is KBitVec32Value -> {
-                var result = lhs.numberValue.toUInt().toLong() shl Int.SIZE_BITS
-                result = result or rhs.numberValue.toUInt().toLong()
+                var result = lhs.intValue.toUInt().toLong() shl Int.SIZE_BITS
+                result = result or rhs.intValue.toUInt().toLong()
                 mkBv(result)
             }
 
@@ -449,6 +493,7 @@ object BvUtils {
         }
     }
 
+    @JvmStatic
     fun KBitVecValue<*>.extractBv(high: Int, low: Int): KBitVecValue<*> = with(ctx) {
         val size = (high - low + 1).toUInt()
         val value = bigIntValue().normalizeValue(sort.sizeBits)
@@ -457,6 +502,7 @@ object BvUtils {
         mkBv(trimHigherBits, size)
     }
 
+    @JvmStatic
     fun KBitVecValue<*>.signExtension(extensionSize: UInt): KBitVecValue<*> =
         if (!signBit()) {
             zeroExtension(extensionSize)
@@ -467,11 +513,13 @@ object BvUtils {
             ctx.mkBv(extendedValue, sort.sizeBits + extensionSize)
         }
 
+    @JvmStatic
     fun KBitVecValue<*>.zeroExtension(extensionSize: UInt): KBitVecValue<*> = with(ctx) {
         mkBv(bigIntValue().normalizeValue(sort.sizeBits), sort.sizeBits + extensionSize)
     }
 
     // Add max value without creation of Bv expr
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.addMaxValueSigned(): KBitVecValue<T> = bvOperation(
         other = this,
         bv1 = { a, _ -> a xor bvMaxValueSigned.bv1 },
@@ -483,6 +531,7 @@ object BvUtils {
     )
 
     // Subtract max value without creation of Bv expr
+    @JvmStatic
     fun <T : KBvSort> KBitVecValue<T>.subMaxValueSigned(): KBitVecValue<T> = bvOperation(
         other = this,
         bv1 = { a, _ -> a xor bvMaxValueSigned.bv1 },
@@ -493,8 +542,10 @@ object BvUtils {
         bvDefault = { a, _ -> a - bvMaxValueSigned.bvDefault(sort.sizeBits) },
     )
 
+    @JvmStatic
     private fun binaryOnes(onesCount: UInt): BigInteger = powerOfTwo(onesCount) - BigInteger.ONE
 
+    @JvmStatic
     private fun concatValues(lhs: BigInteger, rhs: BigInteger, rhsSize: UInt): BigInteger =
         lhs.shiftLeft(rhsSize.toInt()).or(rhs)
 
@@ -507,13 +558,14 @@ object BvUtils {
         crossinline bv32: (UInt, UInt) -> UInt,
         crossinline bv64: (ULong, ULong) -> ULong,
         crossinline bvDefault: (BigInteger, BigInteger) -> BigInteger,
-    ): KBitVecValue<T> = when (this@bvUnsignedOperation) {
-        is KBitVec1Value -> bv1Operation(other, op = bv1)
-        is KBitVec8Value -> bv8UnsignedOperation(other, op = bv8)
-        is KBitVec16Value -> bv16UnsignedOperation(other, op = bv16)
-        is KBitVec32Value -> bv32UnsignedOperation(other, op = bv32)
-        is KBitVec64Value -> bv64UnsignedOperation(other, op = bv64)
-        is KBitVecCustomValue -> bvCustomOperation(other, signed = false, operation = bvDefault)
+    ): KBitVecValue<T> = when {
+        this@bvUnsignedOperation is KBitVec1Value && other is KBitVec1Value -> bv1Operation(other, op = bv1)
+        this@bvUnsignedOperation is KBitVec8Value && other is KBitVec8Value -> bv8UnsignedOperation(other, op = bv8)
+        this@bvUnsignedOperation is KBitVec16Value && other is KBitVec16Value -> bv16UnsignedOperation(other, op = bv16)
+        this@bvUnsignedOperation is KBitVec32Value && other is KBitVec32Value -> bv32UnsignedOperation(other, op = bv32)
+        this@bvUnsignedOperation is KBitVec64Value && other is KBitVec64Value -> bv64UnsignedOperation(other, op = bv64)
+        this@bvUnsignedOperation is KBitVecCustomValue && other is KBitVecCustomValue ->
+            bvCustomOperation(other, signed = false, operation = bvDefault)
         else -> bvOperationDefault(other, signed = false, operation = bvDefault)
     }.uncheckedCast()
 
@@ -527,18 +579,19 @@ object BvUtils {
         crossinline bv32: (Int, Int) -> Int,
         crossinline bv64: (Long, Long) -> Long,
         crossinline bvDefault: (BigInteger, BigInteger) -> BigInteger,
-    ): KBitVecValue<T> = when (this@bvOperation) {
-        is KBitVec1Value -> bv1Operation(other, op = bv1)
-        is KBitVec8Value -> bv8Operation(other, op = bv8)
-        is KBitVec16Value -> bv16Operation(other, op = bv16)
-        is KBitVec32Value -> bv32Operation(other, op = bv32)
-        is KBitVec64Value -> bv64Operation(other, op = bv64)
-        is KBitVecCustomValue -> bvCustomOperation(other, signed = signIsImportant, operation = bvDefault)
+    ): KBitVecValue<T> = when {
+        this@bvOperation is KBitVec1Value && other is KBitVec1Value -> bv1Operation(other, op = bv1)
+        this@bvOperation is KBitVec8Value && other is KBitVec8Value -> bv8Operation(other, op = bv8)
+        this@bvOperation is KBitVec16Value && other is KBitVec16Value -> bv16Operation(other, op = bv16)
+        this@bvOperation is KBitVec32Value && other is KBitVec32Value -> bv32Operation(other, op = bv32)
+        this@bvOperation is KBitVec64Value && other is KBitVec64Value -> bv64Operation(other, op = bv64)
+        this@bvOperation is KBitVecCustomValue && other is KBitVecCustomValue ->
+            bvCustomOperation(other, signed = signIsImportant, operation = bvDefault)
         else -> bvOperationDefault(other, signed = signIsImportant, operation = bvDefault)
     }.uncheckedCast()
 
     private inline fun KBitVec1Value.bv1Operation(
-        other: KBitVecValue<*>,
+        other: KBitVec1Value,
         crossinline op: (Boolean, Boolean) -> Boolean
     ): KBitVec1Value = bvNumericOperation(
         this, other,
@@ -548,87 +601,87 @@ object BvUtils {
     )
 
     private inline fun KBitVec8Value.bv8Operation(
-        other: KBitVecValue<*>,
+        other: KBitVec8Value,
         crossinline op: (Byte, Byte) -> Byte
     ): KBitVec8Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue },
+        unwrap = { it.byteValue },
         wrap = ctx::mkBv,
         op = op
     )
 
     private inline fun KBitVec8Value.bv8UnsignedOperation(
-        other: KBitVecValue<*>,
+        other: KBitVec8Value,
         crossinline op: (UByte, UByte) -> UByte
     ): KBitVec8Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue.toUByte() },
+        unwrap = { it.byteValue.toUByte() },
         wrap = { ctx.mkBv(it.toByte()) },
         op = op
     )
 
     private inline fun KBitVec16Value.bv16Operation(
-        other: KBitVecValue<*>,
+        other: KBitVec16Value,
         crossinline op: (Short, Short) -> Short
     ): KBitVec16Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue },
+        unwrap = { it.shortValue },
         wrap = ctx::mkBv,
         op = op
     )
 
     private inline fun KBitVec16Value.bv16UnsignedOperation(
-        other: KBitVecValue<*>,
+        other: KBitVec16Value,
         crossinline op: (UShort, UShort) -> UShort
     ): KBitVec16Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue.toUShort() },
+        unwrap = { it.shortValue.toUShort() },
         wrap = { ctx.mkBv(it.toShort()) },
         op = op
     )
 
     private inline fun KBitVec32Value.bv32Operation(
-        other: KBitVecValue<*>,
+        other: KBitVec32Value,
         crossinline op: (Int, Int) -> Int
     ): KBitVec32Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue },
+        unwrap = { it.intValue },
         wrap = ctx::mkBv,
         op = op
     )
 
     private inline fun KBitVec32Value.bv32UnsignedOperation(
-        other: KBitVecValue<*>,
+        other: KBitVec32Value,
         crossinline op: (UInt, UInt) -> UInt
     ): KBitVec32Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue.toUInt() },
+        unwrap = { it.intValue.toUInt() },
         wrap = { ctx.mkBv(it.toInt()) },
         op = op
     )
 
     private inline fun KBitVec64Value.bv64Operation(
-        other: KBitVecValue<*>,
+        other: KBitVec64Value,
         crossinline op: (Long, Long) -> Long
     ): KBitVec64Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue },
+        unwrap = { it.longValue },
         wrap = ctx::mkBv,
         op = op
     )
 
     private inline fun KBitVec64Value.bv64UnsignedOperation(
-        other: KBitVecValue<*>,
+        other: KBitVec64Value,
         crossinline op: (ULong, ULong) -> ULong
     ): KBitVec64Value = bvNumericOperation(
         this, other,
-        unwrap = { it.numberValue.toULong() },
+        unwrap = { it.longValue.toULong() },
         wrap = { ctx.mkBv(it.toLong()) },
         op = op
     )
 
     private inline fun KBitVecCustomValue.bvCustomOperation(
-        other: KBitVecValue<*>,
+        other: KBitVecCustomValue,
         signed: Boolean = false,
         crossinline operation: (BigInteger, BigInteger) -> BigInteger
     ): KBitVecCustomValue = bvNumericOperation(
@@ -653,16 +706,13 @@ object BvUtils {
     )
 
     private inline fun <reified T, reified V> bvNumericOperation(
-        arg0: KBitVecValue<*>, arg1: KBitVecValue<*>,
+        arg0: T, arg1: T,
         crossinline unwrap: (T) -> V,
         crossinline wrap: (V) -> T,
         crossinline op: (V, V) -> V
-    ): T {
-        val a0 = unwrap(arg0 as T)
-        val a1 = unwrap(arg1 as T)
-        return wrap(op(a0, a1))
-    }
+    ): T = wrap(op(unwrap(arg0), unwrap(arg1)))
 
+    @JvmStatic
     private fun BigInteger.signedValue(size: UInt): BigInteger {
         val maxValue = powerOfTwo(size - 1u) - BigInteger.ONE
         return if (this > maxValue) {
@@ -681,6 +731,7 @@ object BvUtils {
         fun bvDefault(size: UInt): BigInteger
     }
 
+    @JvmStatic
     private fun <T : KBvSort> KContext.mkBvSpecialValue(size: UInt, source: BvSpecialValueSource): KBitVecValue<T> =
         when (size.toInt()) {
             1 -> mkBv(source.bv1)
@@ -691,14 +742,15 @@ object BvUtils {
             else -> mkBv(source.bvDefault(size), size)
         }.uncheckedCast()
 
+    @JvmStatic
     private fun KBitVecValue<*>.isBvSpecialValue(source: BvSpecialValueSource) = when (this) {
         is KBitVec1Value -> value == source.bv1
-        is KBitVec8Value -> numberValue == source.bv8
-        is KBitVec16Value -> numberValue == source.bv16
-        is KBitVec32Value -> numberValue == source.bv32
-        is KBitVec64Value -> numberValue == source.bv64
+        is KBitVec8Value -> byteValue == source.bv8
+        is KBitVec16Value -> shortValue == source.bv16
+        is KBitVec32Value -> intValue == source.bv32
+        is KBitVec64Value -> longValue == source.bv64
         is KBitVecCustomValue -> value == source.bvDefault(sizeBits)
-        else -> this == ctx.mkBvSpecialValue<KBvSort>(sort.sizeBits, source)
+        else -> stringValue == ctx.mkBvSpecialValue<KBvSort>(sort.sizeBits, source).stringValue
     }
 
 }
diff --git a/ksmt-core/src/test/kotlin/io/ksmt/CustomBvEvalTest.kt b/ksmt-core/src/test/kotlin/io/ksmt/CustomBvEvalTest.kt
new file mode 100644
index 000000000..4fef9609f
--- /dev/null
+++ b/ksmt-core/src/test/kotlin/io/ksmt/CustomBvEvalTest.kt
@@ -0,0 +1,409 @@
+package io.ksmt
+
+import io.ksmt.KContext.SimplificationMode.SIMPLIFY
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.KBitVec1Value
+import io.ksmt.expr.KBitVecNumberValue
+import io.ksmt.expr.KBitVecValue
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.transformer.KTransformerBase
+import io.ksmt.sort.KBv1Sort
+import io.ksmt.sort.KBvSort
+import io.ksmt.sort.KSort
+import io.ksmt.utils.uncheckedCast
+import org.junit.jupiter.api.parallel.Execution
+import org.junit.jupiter.api.parallel.ExecutionMode
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.Arguments
+import org.junit.jupiter.params.provider.MethodSource
+import kotlin.random.nextInt
+import kotlin.test.assertEquals
+
+@Execution(ExecutionMode.CONCURRENT)
+class CustomBvEvalTest : ExpressionEvalTest() {
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvAdd(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvAddExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvAnd(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvAndExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvArithShiftRight(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvArithShiftRightExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvConcat(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvConcatExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvExtract(sizeBits: Int) {
+        repeat(5) {
+            val high = random.nextInt(0 until sizeBits)
+            repeat(5) {
+                val low = random.nextInt(0..high)
+                testOperation(
+                    sizeBits
+                ) { value: KExpr<KBvSort> -> mkBvExtractExpr(high, low, value) }
+            }
+        }
+    }
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvLogicalShiftRight(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvLogicalShiftRightExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvMul(sizeBits: Int) = testOperation(sizeBits, KContext::mkBvMulExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvNAnd(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvNAndExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvNegation(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvNegationExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvNor(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvNorExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvNot(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvNotExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvOr(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvOrExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvReductionAnd(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvReductionAndExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvReductionOr(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvReductionOrExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvRepeat(sizeBits: Int) {
+        repeat(5) {
+            val repetitions = random.nextInt(1..10)
+            testOperation(
+                sizeBits
+            ) { value: KExpr<KBvSort> -> mkBvRepeatExpr(repetitions, value) }
+        }
+    }
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvRotateLeft(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvRotateLeftExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvRotateLeftIndexed(sizeBits: Int) {
+        repeat(5) {
+            val rotation = random.nextInt(0..1024)
+            testOperation(
+                sizeBits
+            ) { value: KExpr<KBvSort> -> mkBvRotateLeftIndexedExpr(rotation, value) }
+        }
+    }
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvRotateRight(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvRotateRightExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvRotateRightIndexed(sizeBits: Int) {
+        repeat(5) {
+            val rotation = random.nextInt(0..1024)
+            testOperation(
+                sizeBits
+            ) { value: KExpr<KBvSort> -> mkBvRotateRightIndexedExpr(rotation, value) }
+        }
+    }
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvShiftLeft(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvShiftLeftExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignedDiv(sizeBits: Int) =
+        testOperationNonZeroSecondArg(sizeBits, KContext::mkBvSignedDivExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignedGreater(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvSignedGreaterExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignedGreaterOrEqual(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvSignedGreaterOrEqualExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignedLess(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvSignedLessExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignedLessOrEqual(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvSignedLessOrEqualExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignedMod(sizeBits: Int) =
+        testOperationNonZeroSecondArg(sizeBits, KContext::mkBvSignedModExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignedRem(sizeBits: Int) =
+        testOperationNonZeroSecondArg(sizeBits, KContext::mkBvSignedRemExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSignExtension(sizeBits: Int) {
+        repeat(5) {
+            val extension = random.nextInt(0..100)
+            testOperation(
+                sizeBits
+            ) { value: KExpr<KBvSort> -> mkBvSignExtensionExpr(extension, value) }
+        }
+    }
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvSub(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvSubExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvUnsignedDiv(sizeBits: Int) =
+        testOperationNonZeroSecondArg(sizeBits, KContext::mkBvUnsignedDivExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvUnsignedGreater(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvUnsignedGreaterExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvUnsignedGreaterOrEqual(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvUnsignedGreaterOrEqualExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvUnsignedLess(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvUnsignedLessExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvUnsignedLessOrEqual(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvUnsignedLessOrEqualExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvUnsignedRem(sizeBits: Int) =
+        testOperationNonZeroSecondArg(sizeBits, KContext::mkBvUnsignedRemExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvXNor(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvXNorExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvXor(sizeBits: Int) =
+        testOperation(sizeBits, KContext::mkBvXorExpr)
+
+    @ParameterizedTest
+    @MethodSource("bvSizes")
+    fun testBvZeroExtension(sizeBits: Int) {
+        repeat(5) {
+            val extension = random.nextInt(0..100)
+            testOperation(
+                sizeBits
+            ) { value: KExpr<KBvSort> -> mkBvZeroExtensionExpr(extension, value) }
+        }
+    }
+
+    private fun <S : KBvSort, T : KSort> testOperation(
+        size: Int,
+        operation: KContext.(KExpr<S>) -> KExpr<T>
+    ) = runTest(size) { sort: S ->
+        randomBvValues(sort).forEach { value ->
+            check(value, operation)
+        }
+    }
+
+    private fun <S : KBvSort, T : KSort> testOperation(
+        size: Int,
+        operation: KContext.(KExpr<S>, KExpr<S>) -> KExpr<T>
+    ) = runTest(size) { sort: S ->
+        randomBvValues(sort).forEach { a ->
+            randomBvValues(sort).forEach { b ->
+                check(a, b, operation)
+            }
+        }
+    }
+
+    private fun <S : KBvSort, T : KSort> testOperation(
+        size: Int,
+        operation: KContext.(KExpr<S>, KExpr<S>, Boolean) -> KExpr<T>
+    ) = runTest(size) { sort: S ->
+        val boolValues = listOf(true, false)
+        randomBvValues(sort).forEach { a ->
+            randomBvValues(sort).forEach { b ->
+                boolValues.forEach { c ->
+                    check(a, b) { x, y -> operation(x, y, c) }
+                }
+            }
+        }
+    }
+
+    private fun <S : KBvSort, T : KSort> testOperationNonZeroSecondArg(
+        size: Int,
+        operation: KContext.(KExpr<S>, KExpr<S>) -> KExpr<T>
+    ) = runTest(size) { sort: S ->
+        randomBvValues(sort).forEach { a ->
+            randomBvNonZeroValues(sort).forEach { b ->
+                check(a, b, operation)
+            }
+        }
+    }
+
+    private fun <S : KBvSort, T : KSort> KContext.check(
+        value: KBitVecValue<S>,
+        op: KContext.(KExpr<S>) -> KExpr<T>
+    ) {
+        val expected = op(value)
+        value.customValues().forEach {
+            checkValue(expected, op(it), expected != value)
+        }
+    }
+
+    private fun <S : KBvSort, T : KSort> KContext.check(
+        a: KBitVecValue<S>,
+        b: KBitVecValue<S>,
+        op: KContext.(KExpr<S>, KExpr<S>) -> KExpr<T>
+    ) {
+        val expected = op(a, b)
+        a.customValues().forEach { ac ->
+            b.customValues().forEach { bc ->
+                checkValue(expected, op(a, bc), expected != a && expected != b)
+                checkValue(expected, op(ac, b), expected != a && expected != b)
+                checkValue(expected, op(ac, bc), expected != a && expected != b)
+            }
+        }
+    }
+
+    private fun <T : KSort> checkValue(expected: KExpr<T>, actual: KExpr<T>, reportError: Boolean) {
+        if (reportError) {
+            assertEquals(expected, actual)
+        }
+    }
+
+    private fun <S : KBvSort> runTest(size: Int, test: KContext.(S) -> Unit) {
+        val ctx = KContext(simplificationMode = SIMPLIFY)
+        val sort = ctx.mkBvSort(size.toUInt())
+        test(ctx, sort.uncheckedCast())
+    }
+
+    private fun <S : KBvSort> KBitVecValue<S>.customValues(): List<KBitVecValue<S>> = buildList {
+        if (this@customValues is KBitVec1Value) {
+            add(CustomBv1Value(ctx, value).uncheckedCast())
+            return@buildList
+        }
+
+        add(CustomBvValue(ctx, sort, stringValue))
+
+        if (this@customValues is KBitVecNumberValue<S, *>) {
+            add(CustomBvNumericValue(ctx, sort, numberValue))
+        }
+    }
+
+    private class CustomBvValue<S : KBvSort>(
+        ctx: KContext,
+        override val sort: S,
+        override val stringValue: String,
+    ) : KBitVecValue<S>(ctx) {
+        override val decl: KDecl<S>
+            get() = error("Should not be executed")
+
+        override fun accept(transformer: KTransformerBase): KExpr<S> {
+            error("Should not be executed")
+        }
+    }
+
+    private class CustomBv1Value(ctx: KContext, val value: Boolean) : KBitVecValue<KBv1Sort>(ctx) {
+        override val stringValue: String
+            get() = ctx.mkBv(value).stringValue
+
+        override val decl: KDecl<KBv1Sort>
+            get() = error("Should not be executed")
+
+        override val sort: KBv1Sort
+            get() = ctx.bv1Sort
+
+        override fun accept(transformer: KTransformerBase): KExpr<KBv1Sort> {
+            error("Should not be executed")
+        }
+    }
+
+    private class CustomBvNumericValue<S : KBvSort, V : Number>(
+        ctx: KContext,
+        override val sort: S,
+        override val numberValue: V
+    ) : KBitVecNumberValue<S, V>(ctx) {
+        override val decl: KDecl<S>
+            get() = error("Should not be executed")
+
+        override fun accept(transformer: KTransformerBase): KExpr<S> {
+            error("Should not be executed")
+        }
+    }
+
+    companion object {
+        private val bvSizesToTest by lazy {
+            val context = KContext()
+            val smallCustomBv = context.mkBvSort(17u)
+            val largeCustomBv = context.mkBvSort(111u)
+
+            listOf(
+                context.bv1Sort,
+                context.bv8Sort,
+                context.bv16Sort,
+                context.bv32Sort,
+                context.bv64Sort,
+                smallCustomBv,
+                largeCustomBv
+            ).map { it.sizeBits.toInt() }
+        }
+
+        @JvmStatic
+        fun bvSizes() = bvSizesToTest.map { Arguments.of(it) }
+    }
+}
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt
index 5ada79d8d..c17d79e3c 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt
@@ -462,19 +462,19 @@ class AstSerializer(
     }
 
     override fun transform(expr: KBitVec8Value) = with(expr) {
-        transform { writeExpr { writeByte(numberValue) } }
+        transform { writeExpr { writeByte(byteValue) } }
     }
 
     override fun transform(expr: KBitVec16Value) = with(expr) {
-        transform { writeExpr { writeShort(numberValue) } }
+        transform { writeExpr { writeShort(shortValue) } }
     }
 
     override fun transform(expr: KBitVec32Value) = with(expr) {
-        transform { writeExpr { writeInt(numberValue) } }
+        transform { writeExpr { writeInt(intValue) } }
     }
 
     override fun transform(expr: KBitVec64Value) = with(expr) {
-        transform { writeExpr { writeLong(numberValue) } }
+        transform { writeExpr { writeLong(longValue) } }
     }
 
     override fun transform(expr: KBitVecCustomValue) = with(expr) {
diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt
index fd9dde704..64c23a232 100644
--- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt
+++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt
@@ -327,19 +327,19 @@ open class KYicesExprInternalizer(
     }
 
     override fun transform(expr: KBitVec8Value): KExpr<KBv8Sort> = with(expr) {
-        transform { yicesCtx.bvConst(sort.sizeBits, numberValue.toLong()) }
+        transform { yicesCtx.bvConst(sort.sizeBits, byteValue.toLong()) }
     }
 
     override fun transform(expr: KBitVec16Value): KExpr<KBv16Sort> = with(expr) {
-        transform { yicesCtx.bvConst(sort.sizeBits, numberValue.toLong()) }
+        transform { yicesCtx.bvConst(sort.sizeBits, shortValue.toLong()) }
     }
 
     override fun transform(expr: KBitVec32Value): KExpr<KBv32Sort> = with(expr) {
-        transform { yicesCtx.bvConst(sort.sizeBits, numberValue.toLong()) }
+        transform { yicesCtx.bvConst(sort.sizeBits, intValue.toLong()) }
     }
 
     override fun transform(expr: KBitVec64Value): KExpr<KBv64Sort> = with(expr) {
-        transform { yicesCtx.bvConst(sort.sizeBits, numberValue) }
+        transform { yicesCtx.bvConst(sort.sizeBits, longValue) }
     }
 
     override fun transform(expr: KBitVecCustomValue): KExpr<KBvSort> = with(expr) {
diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt
index d56674fee..75cdfc558 100644
--- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt
+++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt
@@ -243,15 +243,24 @@ open class KZ3ExprInternalizer(
                 Native.mkBvNumeral(nCtx, bits.size, bits)
             }
 
-            is KBitVec8Value, is KBitVec16Value, is KBitVec32Value -> {
+            is KBitVec8Value -> {
                 val sort = expr.sort.internalizeSort()
-                val intValue = (expr as KBitVecNumberValue<*, *>).numberValue.toInt()
-                Native.mkInt(nCtx, intValue, sort)
+                Native.mkInt(nCtx, expr.byteValue.toInt(), sort)
+            }
+
+            is KBitVec16Value -> {
+                val sort = expr.sort.internalizeSort()
+                Native.mkInt(nCtx, expr.shortValue.toInt(), sort)
+            }
+
+            is KBitVec32Value -> {
+                val sort = expr.sort.internalizeSort()
+                Native.mkInt(nCtx, expr.intValue, sort)
             }
 
             is KBitVec64Value -> {
                 val sort = expr.sort.internalizeSort()
-                Native.mkInt64(nCtx, expr.numberValue, sort)
+                Native.mkInt64(nCtx, expr.longValue, sort)
             }
 
             is KBitVecCustomValue -> {