diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 01:12:31 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 01:12:31 +0000 |
| commit | af6ac1f03a841a0261190cb7caa15ff1fa1f798c (patch) | |
| tree | 56351c49de0cd299548becb15bf5810d6e0dac54 /test | |
| parent | 649c50afb9e35ef467828567d4b1d24a107d6d20 (diff) | |
commit for the version of bitvectors that passes all the unit tests
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/bv/core/Makefile.am | 22 | ||||
| -rw-r--r-- | test/regress/regress0/bv/core/slice-20.cvc | 13 |
2 files changed, 34 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 5b8e6d7d3..947dc65ad 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -41,7 +41,27 @@ TESTS = \ equality-00.smt \ equality-01.smt \ equality-02.smt \ - bv_eq_diamond10.smt + bv_eq_diamond10.smt \ + slice-01.smt \ + slice-02.smt \ + slice-03.smt \ + slice-04.smt \ + slice-05.smt \ + slice-06.smt \ + slice-07.smt \ + slice-08.smt \ + slice-09.smt \ + slice-10.smt \ + slice-11.smt \ + slice-12.smt \ + slice-13.smt \ + slice-14.smt \ + slice-15.smt \ + slice-16.smt \ + slice-17.smt \ + slice-18.smt \ + slice-19.smt \ + slice-20.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/bv/core/slice-20.cvc b/test/regress/regress0/bv/core/slice-20.cvc new file mode 100644 index 000000000..a211b5f2e --- /dev/null +++ b/test/regress/regress0/bv/core/slice-20.cvc @@ -0,0 +1,13 @@ +x1, y1: BITVECTOR(4); +x2, y2: BITVECTOR(2); +x3, y3: BITVECTOR(1); + +ASSERT(x1 = y1); + +ASSERT(x1 = x2 @ x2); +ASSERT(x2 = x3 @ x3); + +ASSERT(y1 = y2 @ y2); +ASSERT(y2 = y3 @ y3); + +QUERY(x3 = y3);
\ No newline at end of file |