diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-12-20 18:27:39 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-20 18:27:39 -0800 |
commit | f9149d3b3e785950a846fb195bf9fa9cb1a2d94a (patch) | |
tree | c69c90377a6c24abbc9c608a767507740abfd3b6 /test/regress/regress0 | |
parent | 13cc0e94ac8892fa1cefa53ff1c884d154894b58 (diff) |
Add explicit disequality handling when generating side condition for CBQI BV. (#1447)
This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.
Diffstat (limited to 'test/regress/regress0')
43 files changed, 301 insertions, 114 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index c59570651..bb43d6c1c 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -90,25 +90,38 @@ TESTS = \ qbv-simp.smt2 \ psyco-001-bv.smt2 \ bug822.smt2 \ - qbv-test-invert-mul.smt2 \ + qbv-disequality3.smt2 \ + qbv-inequality2.smt2 \ + qbv-simple-2vars-vo.smt2 \ + qbv-test-invert-bvadd-neq.smt2 \ qbv-test-invert-bvand.smt2 \ - qbv-test-invert-bvcomp.smt2 \ - qbv-test-invert-bvor.smt2 \ - qbv-test-invert-bvlshr-0.smt2 \ + qbv-test-invert-bvand-neq.smt2 \ qbv-test-invert-bvashr-0.smt2 \ + qbv-test-invert-bvashr-0-neq.smt2 \ + qbv-test-invert-bvashr-1.smt2 \ + qbv-test-invert-bvashr-1-neq.smt2 \ + qbv-test-invert-bvlshr-0.smt2 \ + qbv-test-invert-bvlshr-0-neq.smt2 \ + qbv-test-invert-bvlshr-1.smt2 \ + qbv-test-invert-bvlshr-1-neq.smt2 \ + qbv-test-invert-bvmul.smt2 \ + qbv-test-invert-bvmul-neq.smt2 \ + qbv-test-invert-bvor.smt2 \ + qbv-test-invert-bvor-neq.smt2 \ + qbv-test-invert-bvshl-0.smt2 \ + qbv-test-invert-bvudiv-0.smt2 \ + qbv-test-invert-bvudiv-0-neq.smt2 \ + qbv-test-invert-bvudiv-1.smt2 \ + qbv-test-invert-bvudiv-1-neq.smt2 \ + qbv-test-invert-bvult-1.smt2 \ qbv-test-invert-bvurem-1.smt2 \ + qbv-test-invert-bvurem-1-neq.smt2 \ + qbv-test-invert-bvxor.smt2 \ + qbv-test-invert-bvxor-neq.smt2 \ qbv-test-invert-concat-0.smt2 \ qbv-test-invert-concat-1.smt2 \ - qbv-test-invert-disequality.smt2 \ - qbv-test-invert-shl.smt2 \ - qbv-test-invert-udiv-0.smt2 \ - qbv-test-invert-udiv-1.smt2 \ qbv-test-invert-sign-extend.smt2 \ - qbv-test-invert-bvxor.smt2 \ - qbv-simple-2vars-vo.smt2 \ qbv-test-urem-rewrite.smt2 \ - qbv-inequality2.smt2 \ - qbv-test-invert-bvult-1.smt2 \ intersection-example-onelane.proof-node22337.smt2 \ nested9_true-unreach-call.i_575.smt2 \ small-pipeline-fixpoint-3.smt2 \ @@ -127,6 +140,8 @@ TESTS = \ # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 +# disabled since bvcomp handling is currently disabled +# qbv-test-invert-bvcomp.smt2 # removed because they take more than 20s # javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress0/quantifiers/qbv-disequality3.smt2 b/test/regress/regress0/quantifiers/qbv-disequality3.smt2 new file mode 100644 index 000000000..d16157509 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-disequality3.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvmul (bvadd x b) a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 index d53715a2d..1486e176d 100644 --- a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 +++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 @@ -1,11 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) - -(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b)))) +(assert (forall ((x (_ BitVec 8))) (or (bvuge x (bvadd a b)) (bvule x b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 index d74a6cfea..3c4f93243 100644 --- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 +++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2 index 1f72d44e4..ec4626f52 100644 --- a/test/regress/regress0/quantifiers/qbv-simp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simp.smt2 @@ -1,9 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --no-cbqi-full +; EXPECT: unsat (set-logic BV) (set-info :status unsat) (assert (forall - ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32))) + ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8))) (or (and (= A B) (= C D)) (and (= A C) (= B D))))) - + (check-sat) - + diff --git a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 index b6ae95fec..c36322aac 100644 --- a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 +++ b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 @@ -1,16 +1,16 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) -(declare-fun c () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) +(declare-fun c () (_ BitVec 8)) -(assert (not (= a #x00000000))) +(assert (not (= a #x00))) -(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or -(not (= (bvmul x y) #x0000000A)) -(not (= (bvadd y a) #x00000010)) +(assert (forall ((x (_ BitVec 8)) (y (_ BitVec 8))) (or +(not (= (bvmul x y) #x0A)) +(not (= (bvadd y a) #x10)) ))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 new file mode 100644 index 000000000..216a98531 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvadd x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 new file mode 100644 index 000000000..ad3b9a9e5 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvand x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 index d611fcd68..8dd50b1be 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvand x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvand x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 new file mode 100644 index 000000000..e05c3446d --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 index db7725896..30e7c2f8b 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvashr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 new file mode 100644 index 000000000..2835e5956 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 new file mode 100644 index 000000000..c3de64c4c --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvashr a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 index e8f7c25db..3b55c0b9a 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -1,11 +1,11 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: unsat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) (declare-fun c () (_ BitVec 1)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvcomp x a) (bvcomp x b))))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvcomp x a) ((_ extract 7 7) (bvmul a b)))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 new file mode 100644 index 000000000..e05c3446d --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 index db7725896..1018ce72c 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 new file mode 100644 index 000000000..503bc9852 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvlshr a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 new file mode 100644 index 000000000..08479d90e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr a x) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 new file mode 100644 index 000000000..9dc9f98ac --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvmul x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 new file mode 100644 index 000000000..f3dad679b --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvmul x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 new file mode 100644 index 000000000..74c2891cf --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvor x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 index 287da08c7..4145c68b1 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvor x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 new file mode 100644 index 000000000..e85ecc7de --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvshl x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 new file mode 100644 index 000000000..abef84da2 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvshl x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 new file mode 100644 index 000000000..3748eca24 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (= (bvudiv x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 new file mode 100644 index 000000000..2cabb502e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvudiv x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 new file mode 100644 index 000000000..a0e1b62c2 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (distinct a b (_ bv0 8))) +(assert (forall ((x (_ BitVec 8))) (= (bvudiv a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2 index bf69a8b4a..2690a0ac9 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 index 13c1bf10a..a1dca469a 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -1,9 +1,9 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (bvult a x)))) +(assert (forall ((x (_ BitVec 8))) (not (bvult a x)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 new file mode 100644 index 000000000..871df4827 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (= (bvurem a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 index f7fe54e3e..22bd306ee 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvurem a x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 new file mode 100644 index 000000000..4f9c6edc3 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) + +(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a))))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 index eec40a425..ef41eecdd 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 @@ -1,9 +1,9 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: unsat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) +(declare-fun a () (_ BitVec 8)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvxor x a) (bvmul a a))))) +(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 new file mode 100644 index 000000000..769854f6f --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) + +(assert (forall ((x (_ BitVec 8))) (= (concat x a) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 index f4e19fc52..7b66bd859 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= (concat x a) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (concat x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 new file mode 100644 index 000000000..7dab5637e --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) + +(assert (forall ((x (_ BitVec 8))) (= (concat a x) b))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 index 827e74605..13fb3e1c2 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= (concat a x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= (concat a x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 deleted file mode 100644 index 6ba782597..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (= (bvand x a) b))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 deleted file mode 100644 index 84e9fa7ce..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --cbqi-bv -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (not (= (bvmul x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 deleted file mode 100644 index 97a0662eb..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -; COMMAND-LINE: --cbqi-bv -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 32)) - -(assert (forall ((x (_ BitVec 32))) (not (= (bvshl x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 index 21aa519ad..43019c4cb 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 @@ -1,10 +1,10 @@ -; COMMAND-LINE: --cbqi-bv +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) -(declare-fun a () (_ BitVec 32)) -(declare-fun b () (_ BitVec 64)) +(declare-fun a () (_ BitVec 8)) +(declare-fun b () (_ BitVec 16)) -(assert (forall ((x (_ BitVec 32))) (not (= ((_ sign_extend 32) x) b)))) +(assert (forall ((x (_ BitVec 8))) (not (= ((_ sign_extend 8) x) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 deleted file mode 100644 index becfc5315..000000000 --- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun a () (_ BitVec 16)) -(declare-fun b () (_ BitVec 16)) - -(assert (distinct a b (_ bv0 16))) -(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv x a) b)))) - -(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 index 6df69d80b..e57352b8f 100644 --- a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --bv-div-zero-const +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full ; EXPECT: sat (set-logic BV) (set-info :status sat) |