diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-03 19:16:39 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-03 19:38:21 -0400 |
| commit | 428572ea18afa8fdcaaedfa0c293182cf5a00a3d (patch) | |
| tree | 34c0fe0547e3aea8c5ef67f0ba3afc8d55df2500 /test | |
| parent | e99ed158fb2c5e030f38d048d2b2f2be6b11c7fb (diff) | |
Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
| -rw-r--r-- | test/regress/regress0/boolean-terms-kernel1.smt2 | 13 | ||||
| -rw-r--r-- | test/regress/regress0/boolean-terms-kernel2.smt2 | 19 |
3 files changed, 34 insertions, 0 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 664958e5a..5df8577af 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -47,6 +47,8 @@ SMT_TESTS = \ # Regression tests for SMT2 inputs SMT2_TESTS = \ arrayinuf_declare.smt2 \ + boolean-terms-kernel1.smt2 \ + boolean-terms-kernel2.smt2 \ chained-equality.smt2 \ ite2.smt2 \ ite3.smt2 \ diff --git a/test/regress/regress0/boolean-terms-kernel1.smt2 b/test/regress/regress0/boolean-terms-kernel1.smt2 new file mode 100644 index 000000000..a999a6a76 --- /dev/null +++ b/test/regress/regress0/boolean-terms-kernel1.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic QF_ABV) +(declare-fun b () (_ BitVec 32)) +(declare-fun hk () (Array Bool (_ BitVec 32))) +(push 1) +(assert (not (= b (select hk true)))) +(check-sat) +(pop 1) +(assert (not (= b (_ bv0 32)))) +(assert (= b (select hk true))) +(check-sat) diff --git a/test/regress/regress0/boolean-terms-kernel2.smt2 b/test/regress/regress0/boolean-terms-kernel2.smt2 new file mode 100644 index 000000000..a4e49dd90 --- /dev/null +++ b/test/regress/regress0/boolean-terms-kernel2.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: sat +(set-logic QF_ABV) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun a () (Array Bool (Array (_ BitVec 32) (_ BitVec 32)))) +(declare-fun v2 () (_ BitVec 32)) +(declare-fun r0 () (_ BitVec 32)) +(declare-fun r1 () (_ BitVec 32)) +(declare-fun l () (_ BitVec 32)) +(declare-fun i () (_ BitVec 32)) +(assert c) +(push 1) +(assert (not (=> false (not (= i (select (select a true) (bvsub (bvmul (bvsdiv v2 (_ bv2 32)) (bvadd (bvmul (_ bv2 32) l) (_ bv1 32))) (_ bv1 32)))))))) +(check-sat) +(pop 1) +(assert (not (=> (= i (select (select a true) (bvsub (bvmul (bvsdiv v2 (_ bv2 32)) (bvadd (bvmul (_ bv2 32) l) (_ bv1 32))) (_ bv1 32)))) (not (= r1 (ite b i r0)))))) +(check-sat) |