diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 01:41:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 01:41:48 +0000 |
commit | 3af0d6493cdea4be4130076fee93ebbeff669545 (patch) | |
tree | f704b1aa7e7dc5d8d1d23ec8881e4b0a6553bc3a /test | |
parent | af6ac1f03a841a0261190cb7caa15ff1fa1f798c (diff) |
missed one case
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/bv/core/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/bv/core/equality-05.cvc | 6 | ||||
-rw-r--r-- | test/regress/regress0/bv/core/equality-05.smt | 11 | ||||
-rw-r--r-- | test/regress/regress0/bv/core/slice-20.smt | 16 |
4 files changed, 34 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 947dc65ad..0e559f6f2 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -41,6 +41,7 @@ TESTS = \ equality-00.smt \ equality-01.smt \ equality-02.smt \ + equality-05.smt \ bv_eq_diamond10.smt \ slice-01.smt \ slice-02.smt \ diff --git a/test/regress/regress0/bv/core/equality-05.cvc b/test/regress/regress0/bv/core/equality-05.cvc new file mode 100644 index 000000000..93bef502d --- /dev/null +++ b/test/regress/regress0/bv/core/equality-05.cvc @@ -0,0 +1,6 @@ +x,y:BITVECTOR(1); +ASSERT(x = 0bin0); +ASSERT(y = 0bin1); +ASSERT(x = y); +CHECKSAT; + diff --git a/test/regress/regress0/bv/core/equality-05.smt b/test/regress/regress0/bv/core/equality-05.smt new file mode 100644 index 000000000..a7b9f6185 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-05.smt @@ -0,0 +1,11 @@ +(benchmark equality + :status unsat + :logic QF_BV + :extrafuns ((x BitVec[1])) + :extrafuns ((y BitVec[1])) + :assumption (= x bv0[1]) + :assumption (= y bv1[1]) + :assumption (= x y) + :formula +true +) diff --git a/test/regress/regress0/bv/core/slice-20.smt b/test/regress/regress0/bv/core/slice-20.smt new file mode 100644 index 000000000..66fac573b --- /dev/null +++ b/test/regress/regress0/bv/core/slice-20.smt @@ -0,0 +1,16 @@ +(benchmark slice + :status unsat + :logic QF_BV + :extrafuns ((x1 BitVec[4])) + :extrafuns ((y1 BitVec[4])) + :extrafuns ((x2 BitVec[2])) + :extrafuns ((y2 BitVec[2])) + :extrafuns ((x3 BitVec[1])) + :extrafuns ((y3 BitVec[1])) + :assumption (= x1 y1) + :assumption (= x1 (concat x2 x2)) + :assumption (= x2 (concat x3 x3)) + :assumption (= y1 (concat y2 y2)) + :assumption (= y2 (concat y3 y3)) + :formula (not (= x3 y3)) +) |