diff options
Diffstat (limited to 'test/regress/regress1/bv')
| -rw-r--r-- | test/regress/regress1/bv/Makefile.am | 14 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bench_38.delta.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bug787.smt2 | 91 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bug_extract_mult_leading_bit.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bv-int-collapse2-sat.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bv2nat-ground.smt2 | 18 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 | 5 | ||||
| -rw-r--r-- | test/regress/regress1/bv/cmu-rdk-3.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress1/bv/decision-weight00.smt2 | 20 | ||||
| -rw-r--r-- | test/regress/regress1/bv/divtest.smt2 | 53 | ||||
| -rw-r--r-- | test/regress/regress1/bv/unsound1.smt2 | 23 |
11 files changed, 256 insertions, 1 deletions
diff --git a/test/regress/regress1/bv/Makefile.am b/test/regress/regress1/bv/Makefile.am index fa58e0dee..b144a0507 100644 --- a/test/regress/regress1/bv/Makefile.am +++ b/test/regress/regress1/bv/Makefile.am @@ -19,10 +19,22 @@ endif TESTS = \ bv-proof00.smt \ fuzz34.smt \ - fuzz38.smt + fuzz38.smt \ + bug_extract_mult_leading_bit.smt2 \ + bug787.smt2 \ + bv-int-collapse2-sat.smt2 \ + cmu-rdk-3.smt2 \ + decision-weight00.smt2 \ + divtest.smt2 \ + bv2nat-ground.smt2 \ + bv2nat-simp-range-sat.smt2 \ + unsound1.smt2 EXTRA_DIST = $(TESTS) +# This benchmark is currently disabled as it uses --check-proof +# bench_38.delta.smt2 + # synonyms for "check" in this directory .PHONY: regress regress1 test regress regress1 test: check diff --git a/test/regress/regress1/bv/bench_38.delta.smt2 b/test/regress/regress1/bv/bench_38.delta.smt2 new file mode 100644 index 000000000..760614348 --- /dev/null +++ b/test/regress/regress1/bv/bench_38.delta.smt2 @@ -0,0 +1,7 @@ +; 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/regress1/bv/bug787.smt2 b/test/regress/regress1/bv/bug787.smt2 new file mode 100644 index 000000000..8e0ba0016 --- /dev/null +++ b/test/regress/regress1/bv/bug787.smt2 @@ -0,0 +1,91 @@ +; 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/regress1/bv/bug_extract_mult_leading_bit.smt2 b/test/regress/regress1/bv/bug_extract_mult_leading_bit.smt2 new file mode 100644 index 000000000..8e3728587 --- /dev/null +++ b/test/regress/regress1/bv/bug_extract_mult_leading_bit.smt2 @@ -0,0 +1,7 @@ +(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/regress1/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 new file mode 100644 index 000000000..4b97a3de9 --- /dev/null +++ b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 @@ -0,0 +1,8 @@ +; 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/regress1/bv/bv2nat-ground.smt2 b/test/regress/regress1/bv/bv2nat-ground.smt2 new file mode 100644 index 000000000..bfc22850e --- /dev/null +++ b/test/regress/regress1/bv/bv2nat-ground.smt2 @@ -0,0 +1,18 @@ +; 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/regress1/bv/bv2nat-simp-range-sat.smt2 b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 new file mode 100644 index 000000000..7e98460b8 --- /dev/null +++ b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 @@ -0,0 +1,5 @@ +(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/regress1/bv/cmu-rdk-3.smt2 b/test/regress/regress1/bv/cmu-rdk-3.smt2 new file mode 100644 index 000000000..9e7733889 --- /dev/null +++ b/test/regress/regress1/bv/cmu-rdk-3.smt2 @@ -0,0 +1,11 @@ +; 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/regress1/bv/decision-weight00.smt2 b/test/regress/regress1/bv/decision-weight00.smt2 new file mode 100644 index 000000000..be52810e0 --- /dev/null +++ b/test/regress/regress1/bv/decision-weight00.smt2 @@ -0,0 +1,20 @@ +(set-option :produce-models true) +(set-logic QF_BV) +(set-info :status sat) +(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/regress1/bv/divtest.smt2 b/test/regress/regress1/bv/divtest.smt2 new file mode 100644 index 000000000..fe91cb87b --- /dev/null +++ b/test/regress/regress1/bv/divtest.smt2 @@ -0,0 +1,53 @@ +(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/regress1/bv/unsound1.smt2 b/test/regress/regress1/bv/unsound1.smt2 new file mode 100644 index 000000000..60e764537 --- /dev/null +++ b/test/regress/regress1/bv/unsound1.smt2 @@ -0,0 +1,23 @@ +(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) |