From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 23 Sep 2020 13:00:59 +0000 (-0700)
Subject: bv2int: new options for bvand translation (#5096)
X-Git-Tag: cvc5-1.0.0~2815
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9967954ba1b7b405b6d92d83ebc0adc43f6623b9;p=cvc5.git

bv2int: new options for bvand translation (#5096)

Currently, (bvand x y) is translated into a sum of ITEs.
This PR introduces two more options for the translation of (bvand x y):

bv: cast the integer translations of x and y back to bit-vectors, do a bvand, and cast the result to integers.
iand: use the builtin iand operator.
These options are added to many of the tests, and some new tests are added.
In addition, some tests are cleaned up (e.g., removing --no-check-unsat-cores for satisfiable benchmarks).
Finally, some tests are moved from regress0 to regress2 because they take several seconds to complete (2 -- 10 seconds).
---

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 4e1a89259..683fe61bd 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -642,6 +642,12 @@ header = "options/smt_options.h"
 [[option.mode.SUM]]
   name = "sum"
   help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity"
+[[option.mode.IAND]]
+  name = "iand"
+  help = "Translate bvand to the iand operator (experimental)"
+[[option.mode.BV]]
+  name = "bv"
+  help = "Translate bvand back to bit-vectors"
 
 [[option]]
   name       = "BVAndIntegerGranularity"
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index aa1b5ac5b..9ee4e2b7d 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -169,7 +169,8 @@ Node BVToInt::eliminationPass(Node n)
   {
     current = toVisit.back();
     // assert that the node is binarized
-    kind::Kind_t k = current.getKind();
+    // The following variable is only used in assertions
+    CVC4_UNUSED kind::Kind_t k = current.getKind();
     uint64_t numChildren = current.getNumChildren();
     Assert((numChildren == 2)
            || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
@@ -350,7 +351,8 @@ Node BVToInt::translateWithChildren(Node original,
   // ultbv and sltbv were supposed to be eliminated before this point.
   Assert(oldKind != kind::BITVECTOR_ULTBV);
   Assert(oldKind != kind::BITVECTOR_SLTBV);
-  uint64_t originalNumChildren = original.getNumChildren();
+  // The following variable will only be used in assertions.
+  CVC4_UNUSED uint64_t originalNumChildren = original.getNumChildren();
   Node returnNode;
   switch (oldKind)
   {
@@ -414,15 +416,43 @@ Node BVToInt::translateWithChildren(Node original,
     }
     case kind::BITVECTOR_AND:
     {
-      // Construct an ite, based on granularity.
+      // We support three configurations:
+      // 1. translating to IAND
+      // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV
+      // operators)
+      // 3. translating into a sum
       uint64_t bvsize = original[0].getType().getBitVectorSize();
-      Assert(translated_children.size() == 2);
-      Node newNode = createBitwiseNode(translated_children[0],
+      if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND)
+      {
+        Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
+        returnNode = d_nm->mkNode(
+            kind::IAND, iAndOp, translated_children[0], translated_children[1]);
+      }
+      else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV)
+      {
+        // translate the children back to BV
+        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
+        Node x = translated_children[0];
+        Node y = translated_children[1];
+        Node bvx = d_nm->mkNode(intToBVOp, x);
+        Node bvy = d_nm->mkNode(intToBVOp, y);
+        // perform bvand on the bit-vectors
+        Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy);
+        // translate the result to integers
+        returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand);
+      }
+      else
+      {
+        Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM);
+        // Construct a sum of ites, based on granularity.
+        Assert(translated_children.size() == 2);
+        Node newNode = createBitwiseNode(translated_children[0],
                                        translated_children[1],
                                        bvsize,
                                        options::BVAndIntegerGranularity(),
                                        &oneBitAnd);
-      returnNode = newNode;
+        returnNode = newNode;
+      }
       break;
     }
     case kind::BITVECTOR_SHL:
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 87b3c7310..bc45a3105 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -220,12 +220,8 @@ set(regress_0_tests
   regress0/bv/bv-to-bool1.smtv1.smt2
   regress0/bv/bv-to-bool2.smt2
   regress0/bv/bv_to_int1.smt2
-  regress0/bv/bv_to_int2.smt2
-  regress0/bv/bv_to_int_bvmul1.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
-  regress0/bv/bv_to_int_bitwise.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
-  regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_elim_err.smt2
   regress0/bv/bv_to_int_zext.smt2
@@ -2102,7 +2098,11 @@ set(regress_2_tests
   regress2/bug765.smt2
   regress2/bug812.smt2
   regress2/bv/opStructure_MBA_6.scrambled.min.smt2
+  regress2/bv_to_int2.smt2
   regress2/bv_to_int_ashr.smt2
+  regress2/bv_to_int_bitwise.smt2
+  regress2/bv_to_int_bvmul1.smt2
+  regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
   regress2/bv_to_int_inc1.smt2
   regress2/bv_to_int_mask_array_1.smt2
   regress2/bv_to_int_mask_array_2.smt2
@@ -2201,8 +2201,12 @@ set(regress_3_tests
   regress3/bmc-ibm-5.smtv1.smt2
   regress3/bmc-ibm-7.smtv1.smt2
   regress3/bv_to_int_and_or.smt2
+  regress3/bv_to_int_bench_9839.smt2.minimized.smt2
   regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
+  regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
   regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
+  regress3/bv_to_int_quant1.smt2
+  regress3/bv_to_int_quant2.smt2
   regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
   regress3/eq_diamond14.smtv1.smt2
   regress3/friedman_n6_i4.smtv1.smt2
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index 970a9fd75..9111ac25c 100644
--- a/test/regress/regress0/bv/bv_to_int1.smt2
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2
deleted file mode 100644
index d60f4903b..000000000
--- a/test/regress/regress0/bv/bv_to_int2.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
-; EXPECT: sat
-(set-logic QF_BV)
-(declare-fun a () (_ BitVec 8))
-(declare-fun b () (_ BitVec 8))
-(assert (bvult (bvshl a b) (bvlshr a b)))
-
-(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
deleted file mode 100644
index 444551776..000000000
--- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2
+++ /dev/null
@@ -1,9 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5   --no-check-unsat-cores
-; EXPECT: unsat
-(set-logic QF_BV)
-(declare-fun s () (_ BitVec 4))
-(declare-fun t () (_ BitVec 4))
-(assert (not (= (bvlshr s (bvor (bvand t #b0000) s)) #b0000)))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
deleted file mode 100644
index e21415244..000000000
--- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
-; EXPECT: sat
-(set-logic QF_BV)
-(declare-fun a () (_ BitVec 8))
-(declare-fun b () (_ BitVec 8))
-(assert (bvult (bvmul a b) (bvudiv a b)))
-(assert (bvugt a (_ bv0 8)))
-
-(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 4bbe5685e..91e0c45fd 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
index 5879542eb..3e545ef03 100644
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-fun a () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
deleted file mode 100644
index 6196b2bb9..000000000
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2
+++ /dev/null
@@ -1,81 +0,0 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores
-;EXPECT: unsat
-
-(set-logic QF_UFBV)
-(declare-fun z$n0s32 () (_ BitVec 32))
-(declare-fun dataOut () (_ BitVec 32))
-(declare-fun z$2 () (_ BitVec 1))
-(declare-fun stageOne () (_ BitVec 32))
-(declare-fun z$4 () (_ BitVec 1))
-(declare-fun stageTwo () (_ BitVec 32))
-(declare-fun z$6 () (_ BitVec 1))
-(declare-fun tmp_stageOne () (_ BitVec 32))
-(declare-fun z$8 () (_ BitVec 1))
-(declare-fun tmp_stageTwo () (_ BitVec 32))
-(declare-fun z$10 () (_ BitVec 1))
-(declare-fun reset_ () (_ BitVec 1))
-(declare-fun z$14 () (_ BitVec 1))
-(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
-(declare-fun z$15 () (_ BitVec 32))
-(declare-fun z$17 () (_ BitVec 32))
-(declare-fun dataOut$next () (_ BitVec 32))
-(declare-fun z$19 () (_ BitVec 1))
-(declare-fun c1 () (_ BitVec 32))
-(declare-fun dataIn () (_ BitVec 32))
-(declare-fun z$23 () (_ BitVec 32))
-(declare-fun stageOne$next () (_ BitVec 32))
-(declare-fun z$25 () (_ BitVec 1))
-(declare-fun c2 () (_ BitVec 32))
-(declare-fun z$28 () (_ BitVec 32))
-(declare-fun stageTwo$next () (_ BitVec 32))
-(declare-fun z$30 () (_ BitVec 1))
-(declare-fun tmp_stageOne$next () (_ BitVec 32))
-(declare-fun z$32 () (_ BitVec 1))
-(declare-fun tmp_stageTwo$next () (_ BitVec 32))
-(declare-fun z$34 () (_ BitVec 1))
-(declare-fun z$35 () (_ BitVec 1))
-(declare-fun z$55 () (_ BitVec 32))
-(declare-fun z$57 () (_ BitVec 1))
-(declare-fun z$58 () (_ BitVec 1))
-(declare-fun z$59 () (_ BitVec 1))
-(declare-fun prop$next () (_ BitVec 1))
-(declare-fun z$61 () (_ BitVec 1))
-(declare-fun z$54 () (_ BitVec 1))
-(declare-fun z$63 () (_ BitVec 1))
-(assert
- (= z$15 (Add_32_32_32 stageTwo stageOne)))
-(assert
- (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
-(assert
- (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
-
- 
-(assert
- (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
-(assert
- (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
- (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
-(assert
- (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
-(assert
- (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
-(assert
- (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
-(assert
- (let (($x52 (= z$2 (_ bv1 1))))
- (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
- (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
-(assert
- (= z$63 (_ bv1 1)))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
index f43c8c860..0a0ec7b20 100644
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-sort S 0)
diff --git a/test/regress/regress2/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2
new file mode 100644
index 000000000..4c1ca0c00
--- /dev/null
+++ b/test/regress/regress2/bv_to_int2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvshl a b) (bvlshr a b)))
+
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 11952839f..5516f974b 100644
--- a/test/regress/regress2/bv_to_int_ashr.smt2
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2
new file mode 100644
index 000000000..373f9c323
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_bitwise.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 4))
+(declare-fun t () (_ BitVec 4))
+(assert (not (= (bvlshr s (bvor (bvand t #b0000) s)) #b0000)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress2/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2
new file mode 100644
index 000000000..cfd5c4b9a
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_bvmul1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvmul a b) (bvudiv a b)))
+(assert (bvugt a (_ bv0 8)))
+
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
new file mode 100644
index 000000000..babf9af32
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
@@ -0,0 +1,80 @@
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-unsat-cores
+;EXPECT: unsat
+(set-logic QF_UFBV)
+(declare-fun z$n0s32 () (_ BitVec 32))
+(declare-fun dataOut () (_ BitVec 32))
+(declare-fun z$2 () (_ BitVec 1))
+(declare-fun stageOne () (_ BitVec 32))
+(declare-fun z$4 () (_ BitVec 1))
+(declare-fun stageTwo () (_ BitVec 32))
+(declare-fun z$6 () (_ BitVec 1))
+(declare-fun tmp_stageOne () (_ BitVec 32))
+(declare-fun z$8 () (_ BitVec 1))
+(declare-fun tmp_stageTwo () (_ BitVec 32))
+(declare-fun z$10 () (_ BitVec 1))
+(declare-fun reset_ () (_ BitVec 1))
+(declare-fun z$14 () (_ BitVec 1))
+(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun z$15 () (_ BitVec 32))
+(declare-fun z$17 () (_ BitVec 32))
+(declare-fun dataOut$next () (_ BitVec 32))
+(declare-fun z$19 () (_ BitVec 1))
+(declare-fun c1 () (_ BitVec 32))
+(declare-fun dataIn () (_ BitVec 32))
+(declare-fun z$23 () (_ BitVec 32))
+(declare-fun stageOne$next () (_ BitVec 32))
+(declare-fun z$25 () (_ BitVec 1))
+(declare-fun c2 () (_ BitVec 32))
+(declare-fun z$28 () (_ BitVec 32))
+(declare-fun stageTwo$next () (_ BitVec 32))
+(declare-fun z$30 () (_ BitVec 1))
+(declare-fun tmp_stageOne$next () (_ BitVec 32))
+(declare-fun z$32 () (_ BitVec 1))
+(declare-fun tmp_stageTwo$next () (_ BitVec 32))
+(declare-fun z$34 () (_ BitVec 1))
+(declare-fun z$35 () (_ BitVec 1))
+(declare-fun z$55 () (_ BitVec 32))
+(declare-fun z$57 () (_ BitVec 1))
+(declare-fun z$58 () (_ BitVec 1))
+(declare-fun z$59 () (_ BitVec 1))
+(declare-fun prop$next () (_ BitVec 1))
+(declare-fun z$61 () (_ BitVec 1))
+(declare-fun z$54 () (_ BitVec 1))
+(declare-fun z$63 () (_ BitVec 1))
+(assert
+ (= z$15 (Add_32_32_32 stageTwo stageOne)))
+(assert
+ (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
+(assert
+ (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
+
+ 
+(assert
+ (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
+ (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
+(assert
+ (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
+(assert
+ (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x52 (= z$2 (_ bv1 1))))
+ (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
+ (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
+(assert
+ (= z$63 (_ bv1 1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2
index 0d09a7252..4b22c8ed8 100644
--- a/test/regress/regress2/bv_to_int_inc1.smt2
+++ b/test/regress/regress2/bv_to_int_inc1.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --incremental --solve-bv-as-int=sum
+; COMMAND-LINE: --incremental --solve-bv-as-int=iand
+; COMMAND-LINE: --incremental --solve-bv-as-int=bv
 ; EXPECT sat
 ; EXPECT sat
 ; EXPECT unsat
diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index 970f27fb9..b1c8b9509 100644
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,4 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
index 0960b9359..c054f9693 100644
--- a/test/regress/regress2/bv_to_int_mask_array_2.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2
@@ -1,4 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=iand
+; COMMAND-LINE: --solve-bv-as-int=bv
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2
index 329ee715a..37582d9d8 100644
--- a/test/regress/regress2/bv_to_int_mask_array_3.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4)))
diff --git a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2
new file mode 100644
index 000000000..aeacda35e
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE:  --solve-bv-as-int=bv 
+; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum     
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun _substvar_1171_ () (_ BitVec 32))
+(assert (bvsge ((_ sign_extend 0) _substvar_1171_) (_ bv0 32)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
index a2c964e9a..67f8f69ad 100644
--- a/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-models
-; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-models
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum      --no-check-models
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum      --no-check-models
 ; EXPECT: sat
 (set-logic BV)
 (declare-fun s () (_ BitVec 3))
diff --git a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
new file mode 100644
index 000000000..300883882
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE:  --solve-bv-as-int=bv 
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum     
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=sum    
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=bitwise    
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=iand    
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=2 --solve-bv-as-int=sum     
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun t () (_ BitVec 4))
+(declare-fun s () (_ BitVec 4))
+(assert (bvult (_ bv8 4) (bvadd (_ bv8 4) (bvlshr t s))))
+(assert (forall ((x (_ BitVec 4))) (bvule (bvadd (_ bv8 4) (bvlshr x s)) (_ bv8 4))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
index 22656d17f..1db79b1e9 100644
--- a/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE:  --solve-bv-as-int=bv --no-check-unsat-cores
 ; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic BV)
diff --git a/test/regress/regress3/bv_to_int_quant1.smt2 b/test/regress/regress3/bv_to_int_quant1.smt2
new file mode 100644
index 000000000..22656d17f
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_quant1.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE:  --cegqi-all --full-saturate-quant --bvand-integer-granularity=1 --solve-bv-as-int=sum  --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic BV)
+(declare-fun s () (_ BitVec 4))
+(assert (bvult s (_ bv4 4)))
+(assert (forall ((x (_ BitVec 4))) (= (bvlshr x s) (_ bv0 4))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress3/bv_to_int_quant2.smt2 b/test/regress/regress3/bv_to_int_quant2.smt2
new file mode 100644
index 000000000..c2bf6d9d0
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_quant2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=sum --no-check-models
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=bv --no-check-models
+; COMMAND-LINE: --cegqi-all --full-saturate-quant --solve-bv-as-int=iand --no-check-models
+; EXPECT: sat
+(set-logic BV)
+(declare-fun s () (_ BitVec 4))
+(assert (bvult s (_ bv4 4)))
+(assert (forall ((x (_ BitVec 4))) (= (bvand x s) (_ bv0 4))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress3/bv_to_int_signed_sub_or.smt2 b/test/regress/regress3/bv_to_int_signed_sub_or.smt2
new file mode 100644
index 000000000..50cce4511
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_signed_sub_or.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
+; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=sum --no-check-unsat-cores
+; COMMAND-LINE: --bvand-integer-granularity=1 --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
+; COMMAND-LINE: --bvand-integer-granularity=2 --solve-bv-as-int=sum --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 4))
+(declare-fun t () (_ BitVec 4))
+(assert (bvsgt s t))
+(assert (bvsge t (bvsub t (bvor (bvor s t) (bvneg s)))))
+(check-sat)
+(exit)