diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-04 06:30:35 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-04 13:30:35 +0000 |
commit | 125b1c56d64b6dde1638565152b86950ef3c1342 (patch) | |
tree | 4469c67dd1c3029d33d5537040c0610bbd217b42 /test/regress/regress0 | |
parent | 2e001991f926c307ff0f812dafca4d9dc6e4d831 (diff) |
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.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/bv/bv-int-collapse1.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv-int-collapse2.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/issue5396.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/issue5736.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress0/issue5743.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/issue5947.smt2 | 8 |
6 files changed, 35 insertions, 2 deletions
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) |