diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-28 11:26:07 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-28 11:26:07 +0000 |
| commit | 7fcf0cb48a02115ff93395b89db722d10abf5f41 (patch) | |
| tree | c087609c08ac23331122470afc037a6da463b7c5 /test/regress/regress0/bv | |
| parent | 2f282e67ed10bd58c24cdc14ec53857b79e59a35 (diff) | |
Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bv/smtcompbug.smt | 13 |
2 files changed, 15 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index a21c772b1..937a886f6 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -81,7 +81,8 @@ SMT_TESTS = \ fuzz40.delta01.smt \ fuzz40.smt \ fuzz41.smt \ - calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt + calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \ + smtcompbug.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/bv/smtcompbug.smt b/test/regress/regress0/bv/smtcompbug.smt new file mode 100644 index 000000000..7efe3015c --- /dev/null +++ b/test/regress/regress0/bv/smtcompbug.smt @@ -0,0 +1,13 @@ +(benchmark B_ + :status sat + :category { unknown } + :logic QF_BV + :extrafuns ((x781 BitVec[32])) + :extrafuns ((x803 BitVec[8])) + :extrafuns ((x804 BitVec[8])) + :extrafuns ((x791 BitVec[8])) + :formula (and +(= x804 (bvxor (bvxor (extract[7:0] (bvadd bv1[32] x781)) x791) x803)) +(= (bvnot (extract[0:0] x804)) bv0[1]) +(= x781 bv0[32])) +) |