diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-12-07 18:06:30 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-07 18:06:30 -0800 |
| commit | a35585fc3b20d70f88a156cd0403f6aa5c9a0dbe (patch) | |
| tree | d01198fb90b57e33d68fac3084f03fb9e7fb7b1e /test/regress/regress0 | |
| parent | bbca987e023b2dbf386a62731b94e41c06f32526 (diff) | |
Disable algebraic BV subtheory by default and make experimental. (#5596)
Fixes #5370, #5462.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/issue5370.smt2 | 14 | ||||
| -rw-r--r-- | test/regress/regress0/issue5462.smt2 | 24 |
2 files changed, 38 insertions, 0 deletions
diff --git a/test/regress/regress0/issue5370.smt2 b/test/regress/regress0/issue5370.smt2 new file mode 100644 index 000000000..848567e2c --- /dev/null +++ b/test/regress/regress0/issue5370.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --bv-to-bool +; REQUIRES: symfpu +(set-logic ALL) +(set-info :status sat) +(declare-fun c () (Array (_ BitVec 2) (_ BitVec 1))) +(declare-fun b () (Array (_ BitVec 2) (_ BitVec 1))) +(declare-fun a () (_ BitVec 2)) +(declare-fun ag () (_ BitVec 1)) +(declare-fun ak () (_ BitVec 2)) +(assert (and (= a ((_ zero_extend 1) (select b (_ bv0 2)))) (= (_ bv1 1) + (bvsdiv (bvcomp a ak) (bvand (ite (= (_ bv0 1) (bvcomp ag (select c (bvadd a + (_ bv1 2))))) (_ bv1 1) (_ bv0 1)) (ite (= b (store (store c (bvadd a (_ bv1 + 2)) ag) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1))))))) +(check-sat) diff --git a/test/regress/regress0/issue5462.smt2 b/test/regress/regress0/issue5462.smt2 new file mode 100644 index 000000000..ebf103c85 --- /dev/null +++ b/test/regress/regress0/issue5462.smt2 @@ -0,0 +1,24 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun a () (Array (_ BitVec 32) (_ BitVec 4))) +(declare-fun b () (Array (_ BitVec 32) (_ BitVec 4))) +(declare-fun o () (_ BitVec 1)) +(declare-fun h () (_ BitVec 32)) +(declare-fun i () (_ BitVec 32)) +(declare-fun j () (_ BitVec 32)) +(declare-fun l () (_ BitVec 32)) +(declare-fun m () (_ BitVec 32)) +(assert (= (_ bv1 1) (bvmul (ite (= (_ bv1 1) (ite (= h (_ bv0 32)) (_ bv1 1) + (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnor (bvcomp o (ite (= l (bvor ((_ + zero_extend 28) (select b (bvadd i (_ bv3 32)))) (bvlshr ((_ zero_extend 28) + (select b (bvudiv i (_ bv1 32)))) ((_ zero_extend 28) (select b (bvadd i (_ + bv2 32))))))) (_ bv1 1) (_ bv0 1))) (bvsmod (ite (= (_ bv0 1) (ite (= i (_ + bv1 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvshl (ite (= (_ bv1 1) + (ite (= b (store (store (store (store a (bvadd j (_ bv3 32)) (_ bv0 4)) + (bvsdiv j (_ bv2 32)) (_ bv1 4)) (bvadd j (_ bv1 32)) (_ bv0 4)) j ((_ + extract 3 0) l))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= (_ bv0 + 32) (bvor ((_ zero_extend 28) (select a (bvadd m (_ bv3 32)))) (bvadd (bvor + ((_ zero_extend 28) (select a (bvadd m (_ bv1 32)))) ((_ zero_extend 28) + (select a (bvnor m (_ bv0 32))))) ((_ zero_extend 28) (select a (bvadd m (_ + bv2 32))))))) (_ bv1 1) (_ bv0 1)))))))) +(check-sat) |