diff --git a/src/main/scala/ir/Expr.scala b/src/main/scala/ir/Expr.scala
index 2aa360440..fd9b92751 100644
--- a/src/main/scala/ir/Expr.scala
+++ b/src/main/scala/ir/Expr.scala
@@ -78,8 +78,21 @@ case object FalseLiteral extends BoolLit {
   override def value = false
 }
 
+object BitVecLiteral {
+  def apply(i: Int) = {
+    eval.BitVectorEval.signedInt2BV(32, BigInt(i))
+  }
+  def apply(i: Long) = {
+    eval.BitVectorEval.signedInt2BV(64, BigInt(i))
+  }
+}
+
 case class BitVecLiteral(value: BigInt, size: Int) extends Literal with CachedHashCode {
   require(size >= 0)
+  require(
+    value >= 0,
+    "bitvector [[value]] must be positive, negatives are represented by twos-complement interpretation of [[value]]"
+  )
   require(value <= getType.maxValue, s"bad value: $value for width $size")
   override def toBoogie: BitVecBLiteral = BitVecBLiteral(value, size)
   override def getType: BitVecType = BitVecType(size)
diff --git a/src/main/scala/translating/offlineLifter/OfflineLifter.scala b/src/main/scala/translating/offlineLifter/OfflineLifter.scala
index 96964dbbb..e8441e4c6 100644
--- a/src/main/scala/translating/offlineLifter/OfflineLifter.scala
+++ b/src/main/scala/translating/offlineLifter/OfflineLifter.scala
@@ -126,7 +126,7 @@ object Lifter {
         try {
           val lift = StmtListLifter()
           lift.builder.pcValue = sp
-          f_A64_decoder[Expr, Int, BitVecLiteral](lift, BitVecLiteral(BigInt(op), 32), BitVecLiteral(sp, 64))
+          f_A64_decoder[Expr, Int, BitVecLiteral](lift, BitVecLiteral(op), BitVecLiteral(sp, 64))
           lift.extract.toSeq
         } catch {
           case e => {
diff --git a/src/main/scala/util/z3/z3process.scala b/src/main/scala/util/z3/z3process.scala
index b4b9786d4..30e7461a8 100644
--- a/src/main/scala/util/z3/z3process.scala
+++ b/src/main/scala/util/z3/z3process.scala
@@ -8,9 +8,17 @@ enum SatResult {
   case Unknown(s: String, errors: List[String])
 }
 
-def checkSATSMT2(smt: String, softTimeoutMillis: Option[Int] = None): SatResult = {
+def checkSATSMT2(smt: String, softTimeoutMillis: Option[Int] = None, timeoutSec: Option[Int] = None): SatResult = {
+  val t = timeoutSec match {
+    case Some(n) => Seq(s"-T:$n")
+    case _ => Seq()
+  }
+  val softT = softTimeoutMillis match {
+    case Some(n) => Seq(s"-t:$n")
+    case None => Seq()
+  }
   val cmd =
-    Seq("z3", "-smt2", "-in") ++ (if softTimeoutMillis.isDefined then Seq(s"-t:${softTimeoutMillis.get}") else Seq())
+    Seq("z3", "-smt2", "-in") ++ t ++ softT
   val output = (cmd #< ByteArrayInputStream(smt.getBytes("UTF-8"))).!!
   val errors = output.split("\n").filter(_.trim.startsWith("(error")).toList
   val outputStripped = output.stripLineEnd
diff --git a/src/test/scala/BitVectorSMTTest.scala b/src/test/scala/BitVectorSMTTest.scala
index 40a2754e9..f6337ec9d 100644
--- a/src/test/scala/BitVectorSMTTest.scala
+++ b/src/test/scala/BitVectorSMTTest.scala
@@ -1,12 +1,18 @@
 import ir.*
+import org.scalacheck.{Arbitrary, Gen}
 import org.scalatest.*
 import org.scalatest.funsuite.*
+import test_util.{CaptureOutput, ExprGen}
 import translating.BasilIRToSMT2
 import translating.PrettyPrinter.*
+import util.Logger
 import util.z3.*
 
 @test_util.tags.UnitTest
-class BitVectorEvalTest extends AnyFunSuite {
+class BitVectorEvalTest
+    extends AnyFunSuite
+    with org.scalatestplus.scalacheck.ScalaCheckPropertyChecks
+    with CaptureOutput {
 
   def genSMT(size: Int) = {
     val max = BitVecType(size).maxValue.toInt
@@ -67,5 +73,20 @@ class BitVectorEvalTest extends AnyFunSuite {
     }
   }
 
+  implicit lazy val arbExpr: Arbitrary[Expr] = Arbitrary(for {
+    sz <- Gen.oneOf(List(30, 31, 32, 33, 60, 63, 64, 65, 66, 70, 90, 128, 126))
+    e <- ExprGen.genNonLiteralExpr(Some(sz))
+  } yield (e))
+
+  test("interp exprs smt") {
+    forAll(minSuccessful(30)) { (exp: Expr) =>
+      val test = BinaryExpr(NEQ, exp, ir.eval.evaluateExpr(exp).get)
+      val q = BasilIRToSMT2.exprUnsat(test, None, false)
+      Logger.info("assert: " + test)
+      assert(util.z3.checkSATSMT2(q, None, Some(5)) == SatResult.UNSAT)
+    }
+  }
+
   genSMT(2)
+
 }
diff --git a/src/test/scala/ExprGen.scala b/src/test/scala/ExprGen.scala
new file mode 100644
index 000000000..cf07273d2
--- /dev/null
+++ b/src/test/scala/ExprGen.scala
@@ -0,0 +1,104 @@
+package test_util
+import ir.*
+import org.scalacheck.Gen
+
+object ExprGen {
+
+  def arbBinOp =
+    Gen.oneOf(
+      BVAND,
+      BVOR,
+      BVADD,
+      BVMUL,
+      BVSHL,
+      BVLSHR,
+      BVNAND,
+      BVNOR,
+      BVXOR,
+      BVXNOR,
+      BVSUB,
+      BVASHR, // broken
+      BVUREM, // broken
+      BVSREM, // broken
+      BVSMOD, // broken
+      BVUDIV, // broken
+      BVSDIV // broken
+    )
+
+  def arbBinComp = Gen.oneOf(BVULE, BVUGT, BVULT, BVUGE, BVSLT, BVSLE, BVSGT, BVSGE, EQ, NEQ, BVCOMP)
+
+  def genValue(givenSize: Option[Int] = None) = for {
+    genSize <- Gen.chooseNum(1, 70)
+    size = givenSize.getOrElse(genSize)
+    maxVal = BitVecType(size).maxValue
+    value <- Gen.chooseNum(BigInt(0), maxVal)
+  } yield (BitVecLiteral(value, size))
+
+  def genUnExp(size: Option[Int] = None) = for {
+    v <- genValue(size)
+    op <- Gen.oneOf(BVNOT, BVNEG)
+  } yield (UnaryExpr(op, v))
+
+  def genExt(givenSize: Option[Int] = None) =
+    if givenSize.exists(_ < 1) then {
+      genValue(givenSize)
+    } else
+      for {
+        genSize <- Gen.chooseNum(1, 70)
+        size = givenSize.getOrElse(genSize)
+        amount <- Gen.chooseNum(0, size - 1)
+        sizeLeft = size - amount
+        v <- if (sizeLeft > 1) then genExpr(Some(sizeLeft)) else genValue(Some(sizeLeft))
+        vv <- genExpr(Some(amount))
+        op <- Gen.oneOf(ZeroExtend(amount, v), SignExtend(amount, v), BinaryExpr(BVCONCAT, v, vv))
+      } yield (op)
+
+  def genBinComp(depthLimit: Int) = for {
+    op <- arbBinComp
+    genSize <- Gen.chooseNum(1, 70)
+    l <- genExpr(Some(genSize), depthLimit)
+    r <- genExpr(Some(genSize), depthLimit)
+  } yield (BinaryExpr(op, l, r))
+
+  def genBinExp(givenSize: Option[Int] = None, depthLimit: Int): Gen[Expr] = {
+    def genBV(min: BigInt, max: BigInt, size: Int) = for {
+      v <- Gen.chooseNum(min, max)
+    } yield BitVecLiteral(v, size)
+    for {
+      genSize <- Gen.chooseNum(1, 70)
+      size = givenSize.getOrElse(genSize)
+      op <- Gen.oneOf(arbBinOp, arbBinComp)
+      maxVal = (BigInt(2).pow(size) - 1)
+      smallMax = maxVal.min(255)
+      rhs <- op match {
+        case BVSDIV => genBV(BigInt(1), maxVal, size)
+        case BVUDIV => genBV(BigInt(1), maxVal, size)
+        case BVSREM => genBV(BigInt(1), maxVal, size)
+        case BVSMOD => genBV(BigInt(1), maxVal, size)
+        case BVSHL => genBV(BigInt(0), smallMax, size)
+        case BVLSHR => genBV(BigInt(0), smallMax, size)
+        case BVASHR => genBV(BigInt(0), smallMax, size)
+        case _ => genExpr(Some(size), depthLimit)
+      }
+      lhs <- genExpr(Some(size), depthLimit)
+      expr = BinaryExpr(op, lhs, rhs)
+      nexpr <- expr.getType match {
+        case BoolType if size != 1 =>
+          Gen.oneOf(ZeroExtend(size - 1, UnaryExpr(BoolToBV1, expr)), SignExtend(size - 1, UnaryExpr(BoolToBV1, expr)))
+        case BoolType => Gen.const(UnaryExpr(BoolToBV1, expr))
+        case BitVecType(bvsz) if size > bvsz => Gen.oneOf(ZeroExtend(size - bvsz, expr), SignExtend(size - bvsz, expr))
+        case BitVecType(sz) if size == sz => Gen.const(expr)
+        case x => throw Exception(s"TYPE $x DOES NOT MATCH EXPECTED $size $expr")
+      }
+      // rhs <- Gen.chooseNum(BigInt(minBound), (BigInt(2).pow(sizeRhs) - 1))
+    } yield nexpr
+  }
+
+  def genExpr(size: Option[Int] = None, depthLimit: Int = 10): Gen[Expr] =
+    if (size.exists(_ <= 1) || depthLimit <= 0) then genValue(size)
+    else Gen.oneOf(genBinExp(size, depthLimit - 1), genUnExp(size), genValue(size))
+
+  def genNonLiteralExpr(size: Option[Int] = None, depthLimit: Int = 3): Gen[Expr] =
+    if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size, depthLimit), genUnExp(size))
+
+}
diff --git a/src/test/scala/TestKnownBitsInterpreter.scala b/src/test/scala/TestKnownBitsInterpreter.scala
index 16d072d42..1b6cde81d 100644
--- a/src/test/scala/TestKnownBitsInterpreter.scala
+++ b/src/test/scala/TestKnownBitsInterpreter.scala
@@ -6,7 +6,7 @@ import org.scalacheck.{Arbitrary, Gen}
 import org.scalatest.*
 import org.scalatest.funsuite.*
 import org.scalatestplus.scalacheck.*
-import test_util.TestValueDomainWithInterpreter
+import test_util.{ExprGen, TestValueDomainWithInterpreter}
 import translating.PrettyPrinter.*
 
 @test_util.tags.UnitTest
@@ -166,102 +166,9 @@ class TestKnownBitsInterpreter
     testInterpret(BigInt("ffffffffffffffff", 16), BigInt("ffffffffffffffff", 16))
   }
 
-  def arbBinOp =
-    Gen.oneOf(
-      BVAND,
-      BVOR,
-      BVADD,
-      BVMUL,
-      BVSHL,
-      BVLSHR,
-      BVNAND,
-      BVNOR,
-      BVXOR,
-      BVXNOR,
-      BVSUB,
-      BVASHR, // broken
-      BVUREM, // broken
-      BVSREM, // broken
-      BVSMOD, // broken
-      BVUDIV, // broken
-      BVSDIV // broken
-    )
-
-  def arbBinComp = Gen.oneOf(BVULE, BVUGT, BVULT, BVUGE, BVSLT, BVSLE, BVSGT, BVSGE, EQ, NEQ, BVCOMP)
-
-  def genValue(givenSize: Option[Int] = None) = for {
-    genSize <- Gen.chooseNum(1, 70)
-    size = givenSize.getOrElse(genSize)
-    maxVal = BitVecType(size).maxValue
-    value <- Gen.chooseNum(BigInt(0), maxVal)
-  } yield (BitVecLiteral(value, size))
-
-  def genUnExp(size: Option[Int] = None) = for {
-    v <- genValue(size)
-    op <- Gen.oneOf(BVNOT, BVNEG)
-  } yield (UnaryExpr(op, v))
-
-  def genExt(givenSize: Option[Int] = None) =
-    if givenSize.exists(_ < 1) then {
-      genValue(givenSize)
-    } else
-      for {
-        genSize <- Gen.chooseNum(1, 70)
-        size = givenSize.getOrElse(genSize)
-        amount <- Gen.chooseNum(0, size - 1)
-        sizeLeft = size - amount
-        v <- if (sizeLeft > 1) then genExpr(Some(sizeLeft)) else genValue(Some(sizeLeft))
-        vv <- genExpr(Some(amount))
-        op <- Gen.oneOf(ZeroExtend(amount, v), SignExtend(amount, v), BinaryExpr(BVCONCAT, v, vv))
-      } yield (op)
-
-  def genBinComp() = for {
-    op <- arbBinComp
-    genSize <- Gen.chooseNum(1, 70)
-    l <- genExpr(Some(genSize))
-    r <- genExpr(Some(genSize))
-  } yield (BinaryExpr(op, l, r))
-
-  def genBinExp(givenSize: Option[Int] = None): Gen[Expr] = {
-    def genBV(min: BigInt, max: BigInt, size: Int) = for {
-      v <- Gen.chooseNum(min, max)
-    } yield BitVecLiteral(v, size)
-    for {
-      genSize <- Gen.chooseNum(1, 70)
-      size = givenSize.getOrElse(genSize)
-      op <- Gen.oneOf(arbBinOp, arbBinComp)
-      maxVal = (BigInt(2).pow(size) - 1)
-      smallMax = maxVal.min(255)
-      rhs <- op match {
-        case BVSDIV => genBV(BigInt(1), maxVal, size)
-        case BVUDIV => genBV(BigInt(1), maxVal, size)
-        case BVSREM => genBV(BigInt(1), maxVal, size)
-        case BVSMOD => genBV(BigInt(1), maxVal, size)
-        case BVSHL => genBV(BigInt(0), smallMax, size)
-        case BVLSHR => genBV(BigInt(0), smallMax, size)
-        case BVASHR => genBV(BigInt(0), smallMax, size)
-        case _ => genExpr(Some(size))
-      }
-      lhs <- genExpr(Some(size))
-      expr = BinaryExpr(op, lhs, rhs)
-      nexpr <- expr.getType match {
-        case BoolType if size != 1 =>
-          Gen.oneOf(ZeroExtend(size - 1, UnaryExpr(BoolToBV1, expr)), SignExtend(size - 1, UnaryExpr(BoolToBV1, expr)))
-        case BoolType => Gen.const(UnaryExpr(BoolToBV1, expr))
-        case BitVecType(bvsz) if size > bvsz => Gen.oneOf(ZeroExtend(size - bvsz, expr), SignExtend(size - bvsz, expr))
-        case BitVecType(sz) if size == sz => Gen.const(expr)
-        case x => throw Exception(s"TYPE $x DOES NOT MATCH EXPECTED $size $expr")
-      }
-      // rhs <- Gen.chooseNum(BigInt(minBound), (BigInt(2).pow(sizeRhs) - 1))
-    } yield nexpr
-  }
-
-  def genExpr(size: Option[Int] = None): Gen[Expr] =
-    if (size.exists(_ <= 1)) then genValue(size) else Gen.oneOf(genBinExp(size), genUnExp(size), genValue(size))
-
   implicit lazy val arbExpr: Arbitrary[Expr] = Arbitrary(for {
     sz <- Gen.chooseNum(0, 70)
-    e <- genExpr(Some(sz))
+    e <- ExprGen.genNonLiteralExpr(Some(sz))
   } yield (e))
 
   def evaluateAbstract(e: Expr): TNum = TNumDomain().evaluateExprToTNum(Map(), e)