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

5 files changed, 53 insertions, 2 deletions

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 493572dc9..4fbf5998b 100644
--- 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
index 000000000..984c16051
--- /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
index 000000000..f185aba81
--- /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 7af2ecdae..9a036ada0 100644
--- 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
index 000000000..52229edcb
--- /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])))))
+)