more bugfixes for bitvectors

3 files changed, 53 insertions, 2 deletions

diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 0e559f6f2..25f977f3b 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -62,8 +62,9 @@ TESTS =	\
 	slice-17.smt \
 	slice-18.smt \
 	slice-19.smt \
-	slice-20.smt
-	
+	slice-20.smt \
+	ext_con_004_001_1024.smt 
+		
 EXTRA_DIST = $(TESTS)
 
 # synonyms for "check"
diff --git a/test/regress/regress0/bv/core/bitvec0.smt b/test/regress/regress0/bv/core/bitvec0.smt
new file mode 100644
index 000000000..12766375f
--- /dev/null
+++ b/test/regress/regress0/bv/core/bitvec0.smt
@@ -0,0 +1,24 @@
+(benchmark bitvec0.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 ((a BitVec[32]))
+  :extrafuns ((t BitVec[32]))
+  :extrafuns ((b BitVec[32]))
+  :extrafuns ((aa BitVec[32]))
+  :extrafuns ((c BitVec[32]))
+  :extrafuns ((d BitVec[32]))
+  :extrafuns ((aaaa BitVec[32]))
+  :extrafuns ((bbb BitVec[32]))
+  :extrafuns ((aaa BitVec[32]))
+  :extrafuns ((z BitVec[32]))
+  :formula
+(let (?cvc_0 (extract[6:2] a)) (let (?cvc_1 (extract[2:2] t)) (let (?cvc_2 (extract[6:6] t)) (let (?cvc_3 (extract[2:0] b)) (let (?cvc_4 (extract[2:0] c)) (not (and (and (and (if_then_else (= (concat (concat bv0[1] (extract[3:2] a)) (extract[6:5] a)) ?cvc_0) (= ?cvc_0 bv0[5]) (if_then_else (or (or (= bv2[3] bv6[3])  (= bv0[3] bv6[3]) )  (= bv7[3] bv6[3]) ) false true)) (and (if_then_else (= (concat (extract[3:2] t) (extract[6:5] t)) (extract[5:2] t)) (= ?cvc_1 ?cvc_2) true) (if_then_else (= (extract[4:0] t) (extract[6:2] t)) (and (and (= ?cvc_1 (extract[4:4] t)) (= (extract[0:0] t) ?cvc_2)) (= (extract[1:1] t) (extract[5:5] t))) true))) (implies (and (and (= ?cvc_3 (extract[2:0] aa)) (= ?cvc_4 ?cvc_3)) (= ?cvc_4 (extract[2:0] d))) (= (extract[1:1] d) (extract[1:1] aa)))) (and (and (and (if_then_else (= bv7[3] (extract[2:0] aaaa)) (= bv1[1] (extract[1:1] aaaa)) true) (if_then_else (= (extract[2:0] bbb) (extract[2:0] aaa)) (= (extract[1:1] bbb) (extract[1:1] aaa)) true)) (= (concat (concat (concat bv4[3] bv1[1]) bv1[1]) bv2[2]) (concat (concat bv1[1] bv7[5]) bv0[1]))) (if_then_else (= bv3[2] (extract[1:0] z)) (= bv1[1] (extract[0:0] z)) true)))))))))
+)
diff --git a/test/regress/regress0/bv/core/ext_con_004_001_1024.smt b/test/regress/regress0/bv/core/ext_con_004_001_1024.smt
new file mode 100644
index 000000000..95d1aa0fd
--- /dev/null
+++ b/test/regress/regress0/bv/core/ext_con_004_001_1024.smt
@@ -0,0 +1,26 @@
+(benchmark ext_con_004_001_1024.smt
+:source { Generated by Roberto Bruttomesso }
+:status unsat
+:category { crafted }
+:logic QF_BV
+:extrafuns ((a BitVec[1024]))
+:extrafuns ((dummy BitVec[256]))
+:extrafuns ((v1 BitVec[1024]))
+:extrafuns ((v2 BitVec[1024]))
+:extrafuns ((v3 BitVec[1024]))
+:extrafuns ((v4 BitVec[1024]))
+:formula
+(let (?shared a)
+(and
+(not (= (extract[767:512] v1) (extract[511:256] v1)))
+(not (= (extract[767:512] v2) (extract[511:256] v2)))
+(not (= (extract[767:512] v3) (extract[511:256] v3)))
+(not (= (extract[767:512] v4) (extract[511:256] v4)))
+(or
+(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v1    ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v1    ))))
+(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v2    ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v2    ))))
+(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v3    ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v3    ))))
+(and (= (extract[1023:256] ?shared) (concat (extract[1023:512] v4    ) dummy)) (= (extract[767:0] ?shared) (concat dummy (extract[511:0] v4    ))))
+)
+))
+)