diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress0/bv | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress0/bv')
-rw-r--r-- | test/regress/regress0/bv/Makefile.am | 17 | ||||
-rw-r--r-- | test/regress/regress0/bv/bench_38.delta.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/bv/bug787.smt2 | 91 | ||||
-rw-r--r-- | test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv-int-collapse2-sat.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv2nat-ground.smt2 | 18 | ||||
-rw-r--r-- | test/regress/regress0/bv/bv2nat-simp-range-sat.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress0/bv/cmu-rdk-3.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress0/bv/decision-weight00.smt2 | 19 | ||||
-rw-r--r-- | test/regress/regress0/bv/divtest.smt2 | 53 | ||||
-rw-r--r-- | test/regress/regress0/bv/unsound1.smt2 | 23 |
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) |