diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-06-02 10:16:26 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-02 17:16:26 +0000 |
| commit | dde15bdbf752246fe7cb504df22261e0ad3835db (patch) | |
| tree | ff0b646059dc67c68e24abcc3af5fb3ceeabdc41 /test/regress/regress1/quantifiers | |
| parent | 338982182dbdabecf6f3b06e659621cf43bed916 (diff) | |
Remove redundant logic ALL_SUPPORTED. (#6664)
Diffstat (limited to 'test/regress/regress1/quantifiers')
10 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress1/quantifiers/anti-sk-simp.smt2 b/test/regress/regress1/quantifiers/anti-sk-simp.smt2 index a9f06d8f0..d6304ec1f 100644 --- a/test/regress/regress1/quantifiers/anti-sk-simp.smt2 +++ b/test/regress/regress1/quantifiers/anti-sk-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --sygus-inference ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun f (Int) Int) (declare-fun a () Int) diff --git a/test/regress/regress1/quantifiers/bi-artm-s.smt2 b/test/regress/regress1/quantifiers/bi-artm-s.smt2 index b97c339fc..af8ee945d 100644 --- a/test/regress/regress1/quantifiers/bi-artm-s.smt2 +++ b/test/regress/regress1/quantifiers/bi-artm-s.smt2 @@ -2,7 +2,7 @@ ; EXPECT: unsat (set-option :incremental "false") (set-info :status unsat) -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-fun Y () String) (set-info :notes "ufP_1 is uf type conv P") (declare-fun ufP_1 (Int) Int) diff --git a/test/regress/regress1/quantifiers/cdt-0208-to.smt2 b/test/regress/regress1/quantifiers/cdt-0208-to.smt2 index 8f0312616..76e747168 100644 --- a/test/regress/regress1/quantifiers/cdt-0208-to.smt2 +++ b/test/regress/regress1/quantifiers/cdt-0208-to.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-sort A$ 0) (declare-sort A_set$ 0) diff --git a/test/regress/regress1/quantifiers/ext-ex-deq-trigger.smt2 b/test/regress/regress1/quantifiers/ext-ex-deq-trigger.smt2 index f6f96fe02..bac3f375d 100644 --- a/test/regress/regress1/quantifiers/ext-ex-deq-trigger.smt2 +++ b/test/regress/regress1/quantifiers/ext-ex-deq-trigger.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --relational-triggers ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress1/quantifiers/is-even.smt2 b/test/regress/regress1/quantifiers/is-even.smt2 index 9aaac5e09..0ccfff31f 100644 --- a/test/regress/regress1/quantifiers/is-even.smt2 +++ b/test/regress/regress1/quantifiers/is-even.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (define-funs-rec ((is-even ((x Int)) Int) (is-odd ((y Int)) Int)) ((ite (= x 0) 1 (ite (= (is-odd (- x 1)) 0) 1 0)) (ite (= y 0) 0 (ite (= (is-even (- y 1)) 0) 1 0)))) diff --git a/test/regress/regress1/quantifiers/macro-subtype-param.smt2 b/test/regress/regress1/quantifiers/macro-subtype-param.smt2 index 97ff827a7..4a0fc3f06 100644 --- a/test/regress/regress1/quantifiers/macro-subtype-param.smt2 +++ b/test/regress/regress1/quantifiers/macro-subtype-param.smt2 @@ -6,7 +6,7 @@ ; EXPECT: in term : (R (as x (List Real)))") ; EXIT: 1 -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil))))) diff --git a/test/regress/regress1/quantifiers/parametric-lists.smt2 b/test/regress/regress1/quantifiers/parametric-lists.smt2 index f236c1ec7..4fe8221ab 100644 --- a/test/regress/regress1/quantifiers/parametric-lists.smt2 +++ b/test/regress/regress1/quantifiers/parametric-lists.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((List 1)) ((par (T) ((cons (head T) (tail (List T))) (nil))))) (declare-datatypes ((KV 0)) (((kv (key Int) (value Int)) (nilKV)))) diff --git a/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 index fe593e8c0..f810b00ff 100644 --- a/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 +++ b/test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-sort A$ 0) (declare-sort B$ 0) diff --git a/test/regress/regress1/quantifiers/subtype-param-unk.smt2 b/test/regress/regress1/quantifiers/subtype-param-unk.smt2 index 1828a68b2..69bf38c3f 100644 --- a/test/regress/regress1/quantifiers/subtype-param-unk.smt2 +++ b/test/regress/regress1/quantifiers/subtype-param-unk.smt2 @@ -6,7 +6,7 @@ ; EXIT: 1 ; this will fail if type rule for APPLY_UF requires arguments to be subtypes -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil))))) diff --git a/test/regress/regress1/quantifiers/subtype-param.smt2 b/test/regress/regress1/quantifiers/subtype-param.smt2 index c4cdfb244..eea7a366e 100644 --- a/test/regress/regress1/quantifiers/subtype-param.smt2 +++ b/test/regress/regress1/quantifiers/subtype-param.smt2 @@ -5,7 +5,7 @@ ; EXPECT: in term : (Q (as x (Array Int Real)))") ; EXIT: 1 -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((List 1)) ((par (T) ((cons (hd T) (tl (List T))) (nil))))) |