diff options
Diffstat (limited to 'test/regress/regress0/quantifiers')
7 files changed, 47 insertions, 2 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index a2f5c18b5..4cfdec90e 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -92,14 +92,19 @@ TESTS = \ bug822.smt2 \ qbv-test-invert-mul.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-bvashr-0.smt2 \ qbv-test-invert-bvurem-1.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 \ diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 new file mode 100644 index 000000000..db7725896 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 @@ -0,0 +1,10 @@ +; 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 (= (bvashr x a) 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 new file mode 100644 index 000000000..e8f7c25db --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) +(declare-fun c () (_ BitVec 1)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvcomp x a) (bvcomp x 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 d40e88248..db7725896 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -5,6 +5,6 @@ (declare-fun a () (_ BitVec 32)) (declare-fun b () (_ BitVec 32)) -(assert (forall ((x (_ BitVec 32))) (not (= (bvlshr x a) b)))) +(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b)))) (check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 new file mode 100644 index 000000000..eec40a425 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvxor x a) (bvmul a a))))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 index 814b0d90b..6ba782597 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-bv --cbqi-bv-inv-in-dis-eq +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep ; EXPECT: sat (set-logic BV) (set-info :status 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 new file mode 100644 index 000000000..21aa519ad --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 64)) + +(assert (forall ((x (_ BitVec 32))) (not (= ((_ sign_extend 32) x) b)))) + +(check-sat) |