diff options
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) +) |