diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /test | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/bv/Makefile.am | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/divtest.smt2 | 53 |
2 files changed, 54 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 5d2a54b11..4c2b1c773 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -94,7 +94,7 @@ SMT_TESTS = \ smtcompbug.smt # Regression tests for SMT2 inputs -SMT2_TESTS = +SMT2_TESTS = divtest.smt2 # Regression tests for PL inputs CVC_TESTS = bvsimple.cvc sizecheck.cvc diff --git a/test/regress/regress0/bv/divtest.smt2 b/test/regress/regress0/bv/divtest.smt2 new file mode 100644 index 000000000..fe91cb87b --- /dev/null +++ b/test/regress/regress0/bv/divtest.smt2 @@ -0,0 +1,53 @@ +(set-logic QF_BV) +(set-info :status unsat) +(declare-fun x1 () (_ BitVec 12)) +(declare-fun x2 () (_ BitVec 12)) +(declare-fun x3 () (_ BitVec 12)) + +(declare-fun y1 () (_ BitVec 12)) +(declare-fun y2 () (_ BitVec 12)) +(declare-fun y3 () (_ BitVec 12)) + +(declare-fun z1 () (_ BitVec 12)) +(declare-fun z2 () (_ BitVec 12)) +(declare-fun z3 () (_ BitVec 12)) + +(declare-fun a () (_ BitVec 12)) + +(declare-fun x01 () (_ BitVec 10)) +(declare-fun x02 () (_ BitVec 10)) +(declare-fun x03 () (_ BitVec 10)) + +(declare-fun y01 () (_ BitVec 10)) +(declare-fun y02 () (_ BitVec 10)) +(declare-fun y03 () (_ BitVec 10)) + +(declare-fun z01 () (_ BitVec 10)) +(declare-fun z02 () (_ BitVec 10)) +(declare-fun z03 () (_ BitVec 10)) + +(declare-fun a0 () (_ BitVec 10)) + +(assert +(or +(and + (= a (_ bv0 12)) + (or (not (= (bvudiv x1 a) (bvudiv x2 a))) + (not (= (bvudiv x1 a) (bvudiv x3 a))) + (not (= (bvudiv x2 a) (bvudiv x3 a)))) + (or (and (= x1 y1) (= y1 x2)) + (and (= x1 z1) (= z1 x2))) + (or (and (= x2 y2) (= y2 x3)) + (and (= x2 z2) (= z2 x3)))) + +(and + (= a0 (_ bv0 10)) + (or (not (= (bvurem x01 a0) (bvurem x02 a0))) + (not (= (bvurem x01 a0) (bvurem x03 a0))) + (not (= (bvurem x02 a0) (bvurem x03 a0)))) + (or (and (= x01 y01) (= y01 x02)) + (and (= x01 z01) (= z01 x02))) + (or (and (= x02 y02) (= y02 x03)) + (and (= x02 z02) (= z02 x03)))))) + +(check-sat) |