diff options
Diffstat (limited to 'test/regress')
7 files changed, 52 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 new file mode 100644 index 000000000..040bc33c1 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvand 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 new file mode 100644 index 000000000..2fb5d9bec --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvlshr 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 new file mode 100644 index 000000000..c83b0ca73 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 new file mode 100644 index 000000000..f54abccfd --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (bvult x a) ))) + +(check-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 new file mode 100644 index 000000000..a10f2fbea --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (bvult a x)))) + +(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 new file mode 100644 index 000000000..6a1987c49 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --cbqi-bv +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) 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 index 235d353ef..84e9fa7ce 100644 --- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 +++ b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 @@ -4,7 +4,6 @@ (set-info :status sat) (declare-fun a () (_ BitVec 32)) (declare-fun b () (_ BitVec 32)) -(declare-fun c () (_ BitVec 32)) (assert (forall ((x (_ BitVec 32))) (not (= (bvmul x a) b)))) |