diff options
Diffstat (limited to 'test/regress/regress0/quantifiers')
8 files changed, 8 insertions, 8 deletions
diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 index a39aa4ef5..c48593a36 100644 --- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 +++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --cegqi --dt-rewrite-error-sel ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) (assert (exists ((y Int)) (forall ((x List)) (not (= (head x) (+ y 7)))))) (check-sat) diff --git a/test/regress/regress0/quantifiers/is-even-pred.smt2 b/test/regress/regress0/quantifiers/is-even-pred.smt2 index 9808f4936..e4559df2a 100644 --- a/test/regress/regress0/quantifiers/is-even-pred.smt2 +++ b/test/regress/regress0/quantifiers/is-even-pred.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (define-funs-rec ((is-even ((x Int)) Bool) (is-odd ((x Int)) Bool)) ((or (= x 0) (is-odd (- x 1))) (and (not (= x 0)) (is-even (- x 1))))) diff --git a/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 index aaf9b2c1f..3712b5a42 100644 --- a/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 +++ b/test/regress/regress0/quantifiers/matching-lia-1arg.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --purify-triggers ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-fun P (Int) Bool) (assert (forall ((x Int)) (P (* 2 x)))) (assert (not (P 38))) diff --git a/test/regress/regress0/quantifiers/mix-match.smt2 b/test/regress/regress0/quantifiers/mix-match.smt2 index 110df2fa4..9329f4c56 100644 --- a/test/regress/regress0/quantifiers/mix-match.smt2 +++ b/test/regress/regress0/quantifiers/mix-match.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun P (Real) Bool) (assert (forall ((x Int)) (P x))) diff --git a/test/regress/regress0/quantifiers/partial-trigger.smt2 b/test/regress/regress0/quantifiers/partial-trigger.smt2 index beea57bdb..47a60d4bf 100644 --- a/test/regress/regress0/quantifiers/partial-trigger.smt2 +++ b/test/regress/regress0/quantifiers/partial-trigger.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --partial-triggers ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun P (Int) Bool) (assert (forall ((x Int) (y Int)) (=> (> y 6) (or (> x y) (P x))))) diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 index 67fb5bf24..764c2dbed 100644 --- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 +++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --cegqi ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-datatypes ((nat 0)) (( (Suc (pred nat)) (zero)))) (declare-fun y () nat) diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2 index 343458bee..7e8d70126 100644 --- a/test/regress/regress0/quantifiers/rew-to-scala.smt2 +++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((Formula!953 0)) (((And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32)))))) (declare-fun error_value!964 () Bool) diff --git a/test/regress/regress0/quantifiers/simp-len.smt2 b/test/regress/regress0/quantifiers/simp-len.smt2 index 06ae23f8d..3d132e435 100644 --- a/test/regress/regress0/quantifiers/simp-len.smt2 +++ b/test/regress/regress0/quantifiers/simp-len.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) |