diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-21 17:43:22 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-21 17:43:22 +0000 |
| commit | 7f49a7aedc16cb46216f92d00881cd3485acc206 (patch) | |
| tree | 7e04162a06a37d17df29b88dcddf7934473f9376 /test | |
| parent | 195fee60c540eec5aa880606c4962e6c25384635 (diff) | |
fixing a bug in the BV rewrite, off by one error when merging constants
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/bv/core/Makefile.am | 5 | ||||
| -rw-r--r-- | test/regress/regress0/bv/core/a78test0002.smt | 19 |
2 files changed, 22 insertions, 2 deletions
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 25f977f3b..9182bfbc6 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -63,8 +63,9 @@ TESTS = \ slice-18.smt \ slice-19.smt \ slice-20.smt \ - ext_con_004_001_1024.smt - + ext_con_004_001_1024.smt \ + a78test0002.smt + EXTRA_DIST = $(TESTS) # synonyms for "check" diff --git a/test/regress/regress0/bv/core/a78test0002.smt b/test/regress/regress0/bv/core/a78test0002.smt new file mode 100644 index 000000000..28f6aea09 --- /dev/null +++ b/test/regress/regress0/bv/core/a78test0002.smt @@ -0,0 +1,19 @@ +(benchmark a78test0002.smt + :source { +Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh +(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using +CVC3. + +} + :status sat + :difficulty { 0 } + :category { industrial } + :logic QF_BV + :extrafuns ((r1 BitVec[16])) + :assumption +(not (= r1 bv0[16])) + :assumption +(not (not (= (concat bv0[16] r1) bv65535[32]))) + :formula +(not false) +) |