From 4908a7c71ad38f60828fc4f4ecaa56d216cfdc97 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 2 May 2011 20:19:55 +0000
Subject: [PATCH] adding some previously-failing "bug" test cases for
 bitvectors

---
 test/regress/regress0/bv/Makefile.am      | 12 +++++++++++-
 test/regress/regress0/bv/bug260a.smt      | 12 ++++++++++++
 test/regress/regress0/bv/bug260b.smt      | 12 ++++++++++++
 test/regress/regress0/bv/core/Makefile.am |  3 ++-
 test/regress/regress0/bv/core/bitvec7.smt | 16 ++++++++++++++++
 5 files changed, 53 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/bv/bug260a.smt
 create mode 100644 test/regress/regress0/bv/bug260b.smt
 create mode 100644 test/regress/regress0/bv/core/bitvec7.smt

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])))))
+)
-- 
2.30.2