BoolToBV modes (off, ite, all) (#2530)

3 files changed, 16 insertions, 2 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f22796929..9e942aae1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -159,7 +159,8 @@ set(regress_0_tests
   regress0/bv/ackermann2.smt2
   regress0/bv/ackermann3.smt2
   regress0/bv/ackermann4.smt2
-  regress0/bv/bool-to-bv.smt2
+  regress0/bv/bool-to-bv-all.smt2
+  regress0/bv/bool-to-bv-ite.smt2
   regress0/bv/bug260a.smt
   regress0/bv/bug260b.smt
   regress0/bv/bug440.smt
diff --git a/test/regress/regress0/bv/bool-to-bv.smt2 b/test/regress/regress0/bv/bool-to-bv-all.smt2
index 8706c51a8..5947699d9 100644
--- a/test/regress/regress0/bv/bool-to-bv.smt2
+++ b/test/regress/regress0/bv/bool-to-bv-all.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bool-to-bv
+; COMMAND-LINE: --bool-to-bv=all
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun x2 () (_ BitVec 3))
diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2
new file mode 100644
index 000000000..e1be3ea10
--- /dev/null
+++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --bool-to-bv=ite
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun x2 () (_ BitVec 3))
+(declare-fun x1 () (_ BitVec 3))
+(declare-fun x0 () (_ BitVec 3))
+(declare-fun b1 () Bool)
+(declare-fun b2 () Bool)
+(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1)))
+(assert (= #b000 x2))
+(assert (=> b1 b2))
+(assert (= x2 (ite (bvugt x0 x1) (bvadd x0 (_ bv1 3)) (bvadd x1 (_ bv1 3)))))
+(check-sat)