From 125b1c56d64b6dde1638565152b86950ef3c1342 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Fri, 4 Jun 2021 06:30:35 -0700 Subject: 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. --- test/regress/regress1/bv/bv2nat-ground.smt2 | 2 +- test/regress/regress1/bv/issue3958.smt2 | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/bv/issue3958.smt2 (limited to 'test/regress/regress1') 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) -- cgit v1.2.3