Refactor regressions (#1581)

11 files changed, 2 insertions, 257 deletions

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 912f6871d..44691d1e2 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -92,28 +92,17 @@ SMT_TESTS = \
 	fuzz41.smt \
 	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \
 	smtcompbug.smt \
-	unsound1.smt2 \
 	unsound1-reduced.smt2 \
-	bv2nat-ground.smt2 \
 	bv2nat-ground-c.smt2 \
-	cmu-rdk-3.smt2 \
 	bv2nat-simp-range.smt2 \
-	bv2nat-simp-range-sat.smt2 \
 	bv-int-collapse1.smt2 \
 	bv-int-collapse2.smt2 \
-	bv-int-collapse2-sat.smt2 \
 	divtest_2_5.smt2 \
 	divtest_2_6.smt2 \
 	mul-neg-unsat.smt2 \
 	mul-negpow2.smt2 \
 	bvmul-pow2-only.smt2
 
-# This benchmark is currently disabled as it uses --check-proof
-# bench_38.delta.smt2
-
-# Regression tests for SMT2 inputs
-SMT2_TESTS = divtest.smt2
-
 # Regression tests for PL inputs
 CVC_TESTS = bvsimple.cvc sizecheck.cvc
 
@@ -123,11 +112,9 @@ BUG_TESTS = \
 	bug260b.smt \
 	bug440.smt \
 	bug733.smt2 \
-	bug734.smt2 \
-	bug_extract_mult_leading_bit.smt2 \
-	bug787.smt2
+	bug734.smt2 
 
-TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
+TESTS =	$(SMT_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
 	test00.smt \
diff --git a/test/regress/regress0/bv/bench_38.delta.smt2 b/test/regress/regress0/bv/bench_38.delta.smt2
deleted file mode 100644
index 760614348..000000000
--- a/test/regress/regress0/bv/bench_38.delta.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --fewer-preprocessing-holes --check-proof --quiet
-; EXPECT: unsat
-(set-logic QF_BV)
-(declare-fun x () (_ BitVec 4))
-(assert (and (= (bvudiv (_ bv2 4) x) (_ bv2 4)) (= (_ bv0 4) x) (= (_ bv1 4) x)))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/bug787.smt2 b/test/regress/regress0/bv/bug787.smt2
deleted file mode 100644
index 8e0ba0016..000000000
--- a/test/regress/regress0/bv/bug787.smt2
+++ /dev/null
@@ -1,91 +0,0 @@
-; COMMAND-LINE: --bitblast=eager --no-check-proofs
-; EXPECT: unsat
-(set-logic QF_BV)
-(set-info :status unsat)
-(define-fun hamming-weight ((bv (_ BitVec 4))) (_ BitVec 4)
- (bvadd
-  (bvadd
-   (bvadd ((_ zero_extend 3) ((_ extract 0 0) bv))
-    ((_ zero_extend 3) ((_ extract 1 1) bv)))
-   ((_ zero_extend 3) ((_ extract 2 2) bv)))
-  ((_ zero_extend 3) ((_ extract 3 3) bv))))
-(define-fun left-hamming-weight ((index (_ BitVec 4)) (bv (_ BitVec 4)))
- (_ BitVec 4)
- (hamming-weight (bvand bv (bvnot (bvsub (bvshl index (_ bv1 4)) (_ bv1 4))))))
-(define-fun right-hamming-weight ((index (_ BitVec 4)) (bv (_ BitVec 4)))
- (_ BitVec 4) (hamming-weight (bvand bv (bvsub index (_ bv1 4)))))
-(define-fun bit-1 ((bv (_ BitVec 4))) (_ BitVec 4) (bvand bv (bvneg bv)))
-(define-fun bit-2 ((bv (_ BitVec 4))) (_ BitVec 4)
- (bit-1 (bvand bv (bvsub bv (_ bv1 4)))))
-(define-fun bit-3 ((bv (_ BitVec 4))) (_ BitVec 4)
- (bit-2 (bvand bv (bvsub bv (_ bv1 4)))))
-(define-fun bit-4 ((bv (_ BitVec 4))) (_ BitVec 4)
- (bit-3 (bvand bv (bvsub bv (_ bv1 4)))))
-(define-fun bit-5 ((bv (_ BitVec 4))) (_ BitVec 4)
- (bit-4 (bvand bv (bvsub bv (_ bv1 4)))))
-(define-fun index-bit ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 4)
- (ite (= index (_ bv0 4)) (bit-1 bv)
-  (ite (= index (_ bv1 4)) (bit-2 bv)
-   (ite (= index (_ bv2 4)) (bit-3 bv) (bit-4 bv)))))
-(define-fun permute
- ((index (_ BitVec 4)) (obj-0 (_ BitVec 4)) (obj-1 (_ BitVec 4))
-  (obj-2 (_ BitVec 4)) (obj-3 (_ BitVec 4)))
- (_ BitVec 4)
- (let ((my-index-bit (bvshl (_ bv1 4) index)))
-  (ite (= my-index-bit obj-0) (_ bv0 4)
-   (ite (= my-index-bit obj-1) (_ bv1 4)
-    (ite (= my-index-bit obj-2) (_ bv2 4) (_ bv3 4))))))
-(define-fun left-zeros ((index (_ BitVec 4))) (_ BitVec 8)
- (ite (bvugt index (_ bv2 4)) (ite (bvugt index (_ bv4 4)) (_ bv0 8) (_ bv1 8))
-  (ite (bvugt index (_ bv1 4)) (_ bv2 8) (_ bv3 8))))
-(define-fun centered ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 8)
- (bvshl ((_ zero_extend 4) bv) (left-zeros index)))
-(declare-const v0 (_ BitVec 4))
-(assert (= (_ bv4 4) (hamming-weight v0)))
-(declare-const v1 (_ BitVec 4))
-(assert (= (_ bv4 4) (hamming-weight v1)))
-(declare-const vp1-0 (_ BitVec 4))
-(assert
- (or (= (_ bv1 4) vp1-0) (= (_ bv2 4) vp1-0) (= (_ bv4 4) vp1-0)
-  (= (_ bv8 4) vp1-0)))
-(declare-const vp1-1 (_ BitVec 4))
-(assert
- (or (= (_ bv1 4) vp1-1) (= (_ bv2 4) vp1-1) (= (_ bv4 4) vp1-1)
-  (= (_ bv8 4) vp1-1)))
-(declare-const vp1-2 (_ BitVec 4))
-(assert
- (or (= (_ bv1 4) vp1-2) (= (_ bv2 4) vp1-2) (= (_ bv4 4) vp1-2)
-  (= (_ bv8 4) vp1-2)))
-(declare-const vp1-3 (_ BitVec 4))
-(assert
- (or (= (_ bv1 4) vp1-3) (= (_ bv2 4) vp1-3) (= (_ bv4 4) vp1-3)
-  (= (_ bv8 4) vp1-3)))
-(assert (= (_ bv15 4) (bvor vp1-0 (bvor vp1-1 (bvor vp1-2 vp1-3)))))
-(assert
- (and
-  (= (_ bv0 8)
-     (bvxor
-      (bvand
-       (centered (index-bit (permute (_ bv0 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
-       (centered (index-bit (_ bv0 4) v0) v0))
-      (_ bv8 8)))
-  (= (_ bv0 8)
-     (bvxor
-      (bvand
-       (centered (index-bit (permute (_ bv1 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
-       (centered (index-bit (_ bv1 4) v0) v0))
-      (_ bv8 8)))
-  (= (_ bv0 8)
-     (bvxor
-      (bvand
-       (centered (index-bit (permute (_ bv2 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
-       (centered (index-bit (_ bv2 4) v0) v0))
-      (_ bv8 8)))
-  (= (_ bv0 8)
-     (bvxor
-      (bvand
-       (centered (index-bit (permute (_ bv3 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
-       (centered (index-bit (_ bv3 4) v0) v0))
-      (_ bv8 8)))))
-(check-sat)
-
diff --git a/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 b/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2
deleted file mode 100644
index 8e3728587..000000000
--- a/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-(set-logic QF_BV)
-(set-info :status sat)
-(declare-fun x1 () (_ BitVec 15))
-(declare-fun x2 () (_ BitVec 15))
-(assert (not (= ((_ extract 64 60) (bvmul (concat #b00000000000000000000000000000000000000000000000000 x1) (concat #b10000000000000000000000000000000000000000000000000 x2))) #b00000)))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2
deleted file mode 100644
index 4b97a3de9..000000000
--- a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --rewrite-divk --no-check-proofs --no-check-unsat-cores
-; EXPECT: sat
-(set-logic ALL_SUPPORTED)
-(set-info :status sat)
-(declare-fun t () Int)
-(assert (> t 0))
-(assert (not (= t (bv2nat ((_ int2bv 16) t)))))
-(check-sat)
diff --git a/test/regress/regress0/bv/bv2nat-ground.smt2 b/test/regress/regress0/bv/bv2nat-ground.smt2
deleted file mode 100644
index bfc22850e..000000000
--- a/test/regress/regress0/bv/bv2nat-ground.smt2
+++ /dev/null
@@ -1,18 +0,0 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
-; EXPECT: unsat
-(set-logic QF_BVLIA)
-(set-info :status unsat)
-(declare-const a (_ BitVec 32))
-(declare-const b (_ BitVec 32))
-(declare-const c (_ BitVec 32))
-(declare-const d (_ BitVec 32))
-(declare-const e (_ BitVec 32))
-
-(assert (or (= a b) (= a c) (= a d) (= a e)))
-
-(assert (not (= (bv2nat a) (bv2nat b))))
-(assert (not (= (bv2nat a) (bv2nat c))))
-(assert (not (= (bv2nat a) (bv2nat d))))
-(assert (not (= (bv2nat a) (bv2nat e))))
-
-(check-sat)
diff --git a/test/regress/regress0/bv/bv2nat-simp-range-sat.smt2 b/test/regress/regress0/bv/bv2nat-simp-range-sat.smt2
deleted file mode 100644
index 7e98460b8..000000000
--- a/test/regress/regress0/bv/bv2nat-simp-range-sat.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(set-logic ALL_SUPPORTED)
-(set-info :status sat)
-(declare-fun t () (_ BitVec 16))
-(assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65535))))
-(check-sat)
diff --git a/test/regress/regress0/bv/cmu-rdk-3.smt2 b/test/regress/regress0/bv/cmu-rdk-3.smt2
deleted file mode 100644
index 9e7733889..000000000
--- a/test/regress/regress0/bv/cmu-rdk-3.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --rewrite-divk
-; EXPECT: sat
-(set-logic ALL_SUPPORTED)
-(set-info :status sat)
-
-(declare-fun y () Int)
-(declare-fun x () Int)
-
-(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) 0) 1 0) 0)))) (not (= (ite (>= x 0) 1 0) 0))) (not (= (ite (>= y 0) 1 0) 0))) (not (= (ite (= x y) 1 0) 0))) (not (not (= (ite (= x 0) 1 0) 0)))) (not (not (= (ite (= y 0) 1 0) 0)))) (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) 0) 1 0) 0))) (and (= x (bv2nat ((_ int2bv 3) x))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= y (bv2nat ((_ int2bv 3) y))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) y) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= x (bv2nat ((_ int2bv 3) x))) (= x (bv2nat ((_ int2bv 3) x))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) (_ bv0 1))))
-
-(check-sat)
diff --git a/test/regress/regress0/bv/decision-weight00.smt2 b/test/regress/regress0/bv/decision-weight00.smt2
deleted file mode 100644
index 1feb32c7f..000000000
--- a/test/regress/regress0/bv/decision-weight00.smt2
+++ /dev/null
@@ -1,19 +0,0 @@
-(set-option :produce-models true)
-(set-logic QF_BV)
-(set-info :source |
- Patrice Godefroid, SAGE (systematic dynamic test generation)
- For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf
-|)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status unknown)
-(declare-fun x () (_ BitVec 32))
-(declare-fun y () (_ BitVec 32))
-(declare-fun z () (_ BitVec 4))
-(assert (or
-		(= x (bvmul x y))
-		(and (= x y)
-		     (not (= ((_ extract 2 2) x) ((_ extract 2 2) z))))
-		))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/divtest.smt2 b/test/regress/regress0/bv/divtest.smt2
deleted file mode 100644
index fe91cb87b..000000000
--- a/test/regress/regress0/bv/divtest.smt2
+++ /dev/null
@@ -1,53 +0,0 @@
-(set-logic QF_BV)
-(set-info :status unsat)
-(declare-fun x1 () (_ BitVec 12))
-(declare-fun x2 () (_ BitVec 12))
-(declare-fun x3 () (_ BitVec 12))
-
-(declare-fun y1 () (_ BitVec 12))
-(declare-fun y2 () (_ BitVec 12))
-(declare-fun y3 () (_ BitVec 12))
-
-(declare-fun z1 () (_ BitVec 12))
-(declare-fun z2 () (_ BitVec 12))
-(declare-fun z3 () (_ BitVec 12))
-
-(declare-fun a () (_ BitVec 12))
-
-(declare-fun x01 () (_ BitVec 10))
-(declare-fun x02 () (_ BitVec 10))
-(declare-fun x03 () (_ BitVec 10))
-
-(declare-fun y01 () (_ BitVec 10))
-(declare-fun y02 () (_ BitVec 10))
-(declare-fun y03 () (_ BitVec 10))
-
-(declare-fun z01 () (_ BitVec 10))
-(declare-fun z02 () (_ BitVec 10))
-(declare-fun z03 () (_ BitVec 10))
-
-(declare-fun a0 () (_ BitVec 10))
-
-(assert
-(or 
-(and 
-	(= a (_ bv0 12))
-	(or (not (= (bvudiv x1 a) (bvudiv x2 a)))
-	    (not (= (bvudiv x1 a) (bvudiv x3 a)))
-	    (not (= (bvudiv x2 a) (bvudiv x3 a))))
-	(or (and (= x1 y1) (= y1 x2))
-	    (and (= x1 z1) (= z1 x2)))
-	(or (and (= x2 y2) (= y2 x3))
-	    (and (= x2 z2) (= z2 x3))))
-
-(and 
-	(= a0 (_ bv0 10))
-	(or (not (= (bvurem x01 a0) (bvurem x02 a0)))
-	    (not (= (bvurem x01 a0) (bvurem x03 a0)))
-	    (not (= (bvurem x02 a0) (bvurem x03 a0))))
-	(or (and (= x01 y01) (= y01 x02))
-	    (and (= x01 z01) (= z01 x02)))
-	(or (and (= x02 y02) (= y02 x03))
-	    (and (= x02 z02) (= z02 x03))))))
-	    
-(check-sat)
diff --git a/test/regress/regress0/bv/unsound1.smt2 b/test/regress/regress0/bv/unsound1.smt2
deleted file mode 100644
index 60e764537..000000000
--- a/test/regress/regress0/bv/unsound1.smt2
+++ /dev/null
@@ -1,23 +0,0 @@
-(set-logic QF_BV)
-(set-info :status sat)
-(declare-fun v0 () (_ BitVec 4))
-(assert (let ((e1(_ bv0 1)))
-(let ((e2(_ bv11134 16)))
-(let ((e3 (bvadd e2 ((_ sign_extend 12) v0))))
-(let ((e4 (ite (= e2 ((_ sign_extend 12) v0)) (_ bv1 1) (_ bv0 1))))
-(let ((e5 (bvlshr e3 ((_ sign_extend 12) v0))))
-(let ((e6 (bvxnor e2 ((_ zero_extend 12) v0))))
-(let ((e7 (ite (bvult ((_ sign_extend 15) e1) e2) (_ bv1 1) (_ bv0 1))))
-(let ((e8 (bvugt e7 e1)))
-(let ((e9 (bvule ((_ sign_extend 3) e7) v0)))
-(let ((e10 (bvsgt e5 ((_ zero_extend 12) v0))))
-(let ((e11 (= e6 e3)))
-(let ((e12 (bvslt ((_ zero_extend 15) e4) e5)))
-(let ((e13 (bvugt e5 e2)))
-(let ((e14 (ite e10 e8 e10)))
-(let ((e15 (xor e13 e11)))
-(let ((e16 (xor e14 e15)))
-(let ((e17 (ite e9 e12 e16)))
-e17
-))))))))))))))))))
-(check-sat)