bv: Enable bitblast solver by default. (#6660)

This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes #3958, #5396, #5736, #5743, #5947.

10 files changed, 61 insertions, 14 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6036b021b..707e5e43d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -235,6 +235,16 @@ set(regress_0_tests
   regress0/bv/bug440.smtv1.smt2
   regress0/bv/bug733.smt2
   regress0/bv/bug734.smt2
+  regress0/bv/bv-abstr-bug.smt2
+  regress0/bv/bv-abstr-bug2.smt2
+  regress0/bv/bv-int-collapse1.smt2
+  regress0/bv/bv-int-collapse2.smt2
+  regress0/bv/bv-options4.smt2
+  regress0/bv/bv-to-bool1.smtv1.smt2
+  regress0/bv/bv-to-bool2.smt2
+  regress0/bv/bv2nat-ground-c.smt2
+  regress0/bv/bv2nat-simp-range.smt2
+  regress0/bv/bv_to_int1.smt2
   regress0/bv/bv_to_int_5230_binary.smt2
   regress0/bv/bv_to_int_5230_missing_op.smt2
   regress0/bv/bv_to_int_5230_shift_const.smt2
@@ -242,20 +252,10 @@ set(regress_0_tests
   regress0/bv/bv_to_int_5293_1.smt2
   regress0/bv/bv_to_int_5293_2.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
-  regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.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
-  regress0/bv/bv_to_int1.smt2
-  regress0/bv/bv-abstr-bug.smt2
-  regress0/bv/bv-abstr-bug2.smt2
-  regress0/bv/bv-int-collapse1.smt2
-  regress0/bv/bv-int-collapse2.smt2
-  regress0/bv/bv-options4.smt2
-  regress0/bv/bv-to-bool1.smtv1.smt2
-  regress0/bv/bv-to-bool2.smt2
-  regress0/bv/bv2nat-ground-c.smt2
-  regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bvcomp.cvc
   regress0/bv/bvmul-pow2-only.smt2
   regress0/bv/bvsimple.cvc
@@ -421,6 +421,7 @@ set(regress_0_tests
   regress0/bv/issue-4076.smt2
   regress0/bv/issue-4130.smt2
   regress0/bv/issue3621.smt2
+  regress0/bv/issue5396.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2
@@ -660,6 +661,9 @@ set(regress_0_tests
   regress0/issue5540-2-dump-model.smt2
   regress0/issue5540-model-decls.smt2
   regress0/issue5550-num-children.smt2
+  regress0/issue5736.smt2
+  regress0/issue5743.smt2
+  regress0/issue5947.smt2
   regress0/issue6605-2-abd-triv.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
@@ -1501,6 +1505,7 @@ set(regress_1_tests
   regress1/bv/incorrect1.smtv1.smt2
   regress1/bv/issue3654.smt2
   regress1/bv/issue3776.smt2
+  regress1/bv/issue3958.smt2
   regress1/bv/min-pp-rewrite-error.smt2
   regress1/bv/test-bv-abstraction.smt2
   regress1/bv/unsound1.smt2
diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2
index a31036f71..1f5015d14 100644
--- a/test/regress/regress0/bv/bv-int-collapse1.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --bv-solver=lazy
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2
index 5cf6a600c..d56188dad 100644
--- a/test/regress/regress0/bv/bv-int-collapse2.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --bv-solver=lazy
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/issue5396.smt2 b/test/regress/regress0/bv/issue5396.smt2
new file mode 100644
index 000000000..7f6d3ab38
--- /dev/null
+++ b/test/regress/regress0/bv/issue5396.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_BVLIA)
+(set-info :status unsat)
+(declare-fun a () Int)
+(assert (= (bv2nat (bvor ((_ int2bv 3) a) ((_ int2bv 3) a))) 0))
+(assert (distinct ((_ extract 0 0) (bvsdiv ((_ int2bv 3) (bv2nat (bvmul ((_ int2bv 3) a) ((_ int2bv 3) a)))) ((_ int2bv 3) 1))) (_ bv0 1)))
+(check-sat)
diff --git a/test/regress/regress0/issue5736.smt2 b/test/regress/regress0/issue5736.smt2
new file mode 100644
index 000000000..dd4d4f951
--- /dev/null
+++ b/test/regress/regress0/issue5736.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -q --check-unsat-cores --check-models
+(set-info :status sat)
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 32)))
+(declare-fun b () (Array (_ BitVec 32) (_ BitVec 32)))
+(declare-fun c () (_ BitVec 32))
+(declare-fun d () (_ BitVec 32))
+(declare-fun e () (_ BitVec 32))
+(declare-fun f () (_ BitVec 32))
+(declare-fun g () (Array (_ BitVec 32) (_ BitVec 32)))
+(assert (= (= d e) (= (select a c) f)))
+(assert (= g (store b (bvxor (_ bv4 32) f) (_ bv0 32))))
+(check-sat)
diff --git a/test/regress/regress0/issue5743.smt2 b/test/regress/regress0/issue5743.smt2
new file mode 100644
index 000000000..b53f0fbef
--- /dev/null
+++ b/test/regress/regress0/issue5743.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --check-models -q
+(set-logic QF_AUFBV)
+(set-info :status sat)
+(declare-fun bv_22-0 () (_ BitVec 1))
+(declare-fun arr-8324605531633220487_-1461211092162269148-0 () (Array (_ BitVec 1) Bool))
+(assert (select arr-8324605531633220487_-1461211092162269148-0 (bvlshr bv_22-0 bv_22-0)))
+(check-sat)
diff --git a/test/regress/regress0/issue5947.smt2 b/test/regress/regress0/issue5947.smt2
new file mode 100644
index 000000000..4fbcfb00b
--- /dev/null
+++ b/test/regress/regress0/issue5947.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q --check-models
+(set-logic QF_UFBVLIA)
+(set-info :status sat)
+(declare-fun f ((_ BitVec 3)) Int)
+(declare-fun x () (_ BitVec 3))
+(declare-fun y () (_ BitVec 3))
+(assert (not (= (f (bvxor x y)) (f (bvxnor x y)))))
+(check-sat)
diff --git a/test/regress/regress1/bv/bv2nat-ground.smt2 b/test/regress/regress1/bv/bv2nat-ground.smt2
index 50550f530..7e0da282e 100644
--- a/test/regress/regress1/bv/bv2nat-ground.smt2
+++ b/test/regress/regress1/bv/bv2nat-ground.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: --bv-solver=lazy
 ; EXPECT: unsat
 (set-logic QF_BVLIA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/bv/issue3958.smt2 b/test/regress/regress1/bv/issue3958.smt2
new file mode 100644
index 000000000..5ed71630d
--- /dev/null
+++ b/test/regress/regress1/bv/issue3958.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-const v4 Bool)
+(declare-const v8 Bool)
+(declare-const bv_21-0 (_ BitVec 21))
+(assert (or (= bv_21-0 bv_21-0 bv_21-0 (_ bv0 21) bv_21-0) v4))
+(assert (or (= (_ bv0 21) (bvudiv bv_21-0 bv_21-0) (_ bv0 21) (_ bv0 21)) v8))
+(check-sat)
diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index 094a32772..150320824 100644
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -45,6 +45,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core)
   d_smtEngine->setLogic("QF_BV");
 
   d_smtEngine->setOption("bitblast", "eager");
+  d_smtEngine->setOption("bv-solver", "lazy");
   d_smtEngine->setOption("incremental", "false");
   // Notice that this unit test uses the theory engine of a created SMT
   // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized