adding some previously-failing "bug" test cases for bitvectors

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 493572dc9df988c5771ca1b3d9a9468ed15dd7f1..4fbf5998b0dd04cc25ec04bd86c5db087dcf7130 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -17,10 +17,20 @@ SMT2_TESTS =
 CVC_TESTS = bvsimple.cvc
 
 # Regression tests derived from bug reports
-BUG_TESTS =
+BUG_TESTS = \
+       bug260a.smt \
+       bug260b.smt
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
        test00.smt \
        bvcomp.cvc
+
+# synonyms for "check" in this directory
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:

diff --git a/test/regress/regress0/bv/bug260a.smt b/test/regress/regress0/bv/bug260a.smt
new file mode 100644 (file)
index 0000000..984c160
--- /dev/null
+++ b/test/regress/regress0/bv/bug260a.smt
@@ -0,0 +1,12 @@
+(benchmark B_
+:logic QF_BV
+:extrafuns ((a BitVec[32]))
+:status sat
+:formula
+(let (?n1 (extract[6:2] a))
+(let (?n2 bv0[3])
+(let (?n3 (extract[6:5] a))
+(let (?n4 (concat ?n2 ?n3))
+(flet ($n5 (= ?n1 ?n4))
+$n5
+))))))

diff --git a/test/regress/regress0/bv/bug260b.smt b/test/regress/regress0/bv/bug260b.smt
new file mode 100644 (file)
index 0000000..f185aba
--- /dev/null
+++ b/test/regress/regress0/bv/bug260b.smt
@@ -0,0 +1,12 @@
+(benchmark B_
+:logic QF_BV
+:extrafuns ((a BitVec[32]))
+:status sat
+:formula
+(let (?n1 bv0[5])
+(let (?n2 bv0[3])
+(let (?n3 (extract[6:5] a))
+(let (?n4 (concat ?n2 ?n3))
+(flet ($n5 (= ?n1 ?n4))
+$n5
+))))))

diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 7af2ecdaed684bcbccea0a1831fa168fe4b1b1f8..9a036ada03ed09d3ecdb7fddb744594359cc3384 100644 (file)
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -68,7 +68,8 @@ TESTS =       \
        a95test0002.smt \
        bitvec0.smt \
        bitvec2.smt \
-       bitvec5.smt
+       bitvec5.smt \
+       bitvec7.smt
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/bv/core/bitvec7.smt b/test/regress/regress0/bv/core/bitvec7.smt
new file mode 100644 (file)
index 0000000..52229ed
--- /dev/null
+++ b/test/regress/regress0/bv/core/bitvec7.smt
@@ -0,0 +1,16 @@
+(benchmark bitvec7.smt
+  :source {
+Hand-crafted bit-vector benchmarks.  Some are from the SVC benchmark suite.
+Contributed by Vijay Ganesh (vganesh@stanford.edu).  Translated into SMT-LIB
+format by Clark Barrett using CVC3.
+
+}
+  :status unsat
+  :difficulty { 0 }
+  :category { crafted }
+  :logic QF_BV
+  :extrafuns ((bv BitVec[10]))
+  :extrapreds ((a))
+  :formula
+(not (and (= (extract[5:3] bv96[8]) (extract[4:2] (concat bv121[7] (extract[0:0] bv)))) (= (concat bv1[1] (ite a bv0[1] bv1[1])) (extract[1:0] (ite a bv6[3] bv3[3])))))
+)