diff options
Diffstat (limited to 'test')
308 files changed, 325 insertions, 325 deletions
diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp index 04d4ce41d..5d0e6b828 100644 --- a/test/api/sep_log_api.cpp +++ b/test/api/sep_log_api.cpp @@ -130,7 +130,7 @@ int validate_getters(void) Solver slv; /* Setup some options for cvc5 */ - slv.setLogic("QF_ALL_SUPPORTED"); + slv.setLogic("QF_ALL"); slv.setOption("produce-models", "true"); slv.setOption("incremental", "false"); diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 67174ad8e..44ce684dd 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -980,7 +980,7 @@ def test_get_value3(solver): def test_declare_separation_heap(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") integer = solver.getIntegerSort() solver.declareSeparationHeap(integer, integer) # cannot declare separation logic heap more than once @@ -1014,7 +1014,7 @@ def test_get_separation_heap_term1(solver): def test_get_separation_heap_term2(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "false") checkSimpleSeparationConstraints(solver) @@ -1023,7 +1023,7 @@ def test_get_separation_heap_term2(solver): def test_get_separation_heap_term3(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = solver.mkFalse() @@ -1034,7 +1034,7 @@ def test_get_separation_heap_term3(solver): def test_get_separation_heap_term4(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = solver.mkTrue() @@ -1045,7 +1045,7 @@ def test_get_separation_heap_term4(solver): def test_get_separation_heap_term5(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") checkSimpleSeparationConstraints(solver) @@ -1063,7 +1063,7 @@ def test_get_separation_nil_term1(solver): def test_get_separation_nil_term2(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "false") checkSimpleSeparationConstraints(solver) @@ -1072,7 +1072,7 @@ def test_get_separation_nil_term2(solver): def test_get_separation_nil_term3(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = solver.mkFalse() @@ -1083,7 +1083,7 @@ def test_get_separation_nil_term3(solver): def test_get_separation_nil_term4(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = solver.mkTrue() @@ -1094,7 +1094,7 @@ def test_get_separation_nil_term4(solver): def test_get_separation_nil_term5(solver): - solver.setLogic("ALL_SUPPORTED") + solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") checkSimpleSeparationConstraints(solver) diff --git a/test/regress/regress0/bug521.minimized.smt2 b/test/regress/regress0/bug521.minimized.smt2 index 6751d4077..979887682 100644 --- a/test/regress/regress0/bug521.minimized.smt2 +++ b/test/regress/regress0/bug521.minimized.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun _substvar_301_ () Bool) (declare-fun _substvar_300_ () Bool) diff --git a/test/regress/regress0/bug541.smt2 b/test/regress/regress0/bug541.smt2 index 1847a9111..055a98dc8 100644 --- a/test/regress/regress0/bug541.smt2 +++ b/test/regress/regress0/bug541.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((Pair 2)) ((par (T1 T2) ((mk-pair (first T1) (second T2)))))) (assert (= (mk-pair 0.0 0.0) (mk-pair 1.5 2.5))) (check-sat) diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2 index 5968fe00c..a31036f71 100644 --- a/test/regress/regress0/bv/bv-int-collapse1.smt2 +++ b/test/regress/regress0/bv/bv-int-collapse1.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun t () (_ BitVec 16)) (assert (not (= t ((_ int2bv 16) (bv2nat t))))) diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2 index b7e390592..5cf6a600c 100644 --- a/test/regress/regress0/bv/bv-int-collapse2.smt2 +++ b/test/regress/regress0/bv/bv-int-collapse2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun t () Int) (assert (= (+ t 1) (bv2nat ((_ int2bv 16) t)))) diff --git a/test/regress/regress0/bv/bv2nat-simp-range.smt2 b/test/regress/regress0/bv/bv2nat-simp-range.smt2 index bc3ce73b7..31e2b7bd1 100644 --- a/test/regress/regress0/bv/bv2nat-simp-range.smt2 +++ b/test/regress/regress0/bv/bv2nat-simp-range.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun t () (_ BitVec 16)) (assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65536)))) diff --git a/test/regress/regress0/datatypes/bug597-rbt.smt2 b/test/regress/regress0/datatypes/bug597-rbt.smt2 index 236865aa3..4e1ae1784 100644 --- a/test/regress/regress0/datatypes/bug597-rbt.smt2 +++ b/test/regress/regress0/datatypes/bug597-rbt.smt2 @@ -1,5 +1,5 @@ (set-option :global-declarations true) -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) ; Tree type diff --git a/test/regress/regress0/datatypes/bug604.smt2 b/test/regress/regress0/datatypes/bug604.smt2 index dfd11001d..bd48b93f0 100644 --- a/test/regress/regress0/datatypes/bug604.smt2 +++ b/test/regress/regress0/datatypes/bug604.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-datatypes ((PairIntInt 0)) ( ( (pair (firstPairIntInt Int) (secondPairIntInt Int)) ) )) diff --git a/test/regress/regress0/datatypes/bug625.smt2 b/test/regress/regress0/datatypes/bug625.smt2 index 1e9a18d9d..ab6d52275 100644 --- a/test/regress/regress0/datatypes/bug625.smt2 +++ b/test/regress/regress0/datatypes/bug625.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun x1 () Int) (declare-fun x2 () Int) diff --git a/test/regress/regress0/datatypes/cdt-model-cade15.smt2 b/test/regress/regress0/datatypes/cdt-model-cade15.smt2 index 8ddf7c52a..130ff62ad 100644 --- a/test/regress/regress0/datatypes/cdt-model-cade15.smt2 +++ b/test/regress/regress0/datatypes/cdt-model-cade15.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-codatatypes ((Stream 0)) (((C (c Stream)) (D (d Stream)) (E (e Stream))))) diff --git a/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 b/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 index 0741b0ff0..4a9dfce0a 100644 --- a/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 +++ b/test/regress/regress0/datatypes/cdt-non-canon-stream.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-codatatypes ((list 0)) (((cons (head Int) (tail list))))) diff --git a/test/regress/regress0/datatypes/coda_simp_model.smt2 b/test/regress/regress0/datatypes/coda_simp_model.smt2 index 3c30021b0..a895496c0 100644 --- a/test/regress/regress0/datatypes/coda_simp_model.smt2 +++ b/test/regress/regress0/datatypes/coda_simp_model.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort a_ 0) (declare-fun __nun_card_witness_0 () a_) diff --git a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 index 1c2f22275..bbc25da68 100644 --- a/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 +++ b/test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun start!13 () Bool) diff --git a/test/regress/regress0/datatypes/dt-different-params.smt2 b/test/regress/regress0/datatypes/dt-different-params.smt2 index f73d82dc9..56bd79a47 100644 --- a/test/regress/regress0/datatypes/dt-different-params.smt2 +++ b/test/regress/regress0/datatypes/dt-different-params.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-datatypes ((Data 1)) ((par (T) ((data (first T)))))) diff --git a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 index abcff3ddb..0baa867e8 100644 --- a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 +++ b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-datatypes ((Pair 2)) ((par (T S) ((pair (first T) (second S)))))) diff --git a/test/regress/regress0/datatypes/is_test.smt2 b/test/regress/regress0/datatypes/is_test.smt2 index c54a84859..4b0aa59ff 100644 --- a/test/regress/regress0/datatypes/is_test.smt2 +++ b/test/regress/regress0/datatypes/is_test.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((Unit 0)) (((u)))) (declare-fun x () Unit) diff --git a/test/regress/regress0/datatypes/pair-real-bool.smt2 b/test/regress/regress0/datatypes/pair-real-bool.smt2 index c29eeb4e9..f8ed3dd3c 100644 --- a/test/regress/regress0/datatypes/pair-real-bool.smt2 +++ b/test/regress/regress0/datatypes/pair-real-bool.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat ;(set-option :produce-models true) -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-datatypes ((RealTree 0)) ( ( diff --git a/test/regress/regress0/datatypes/sc-cdt1.smt2 b/test/regress/regress0/datatypes/sc-cdt1.smt2 index 3c88c49c0..cc508e2ed 100644 --- a/test/regress/regress0/datatypes/sc-cdt1.smt2 +++ b/test/regress/regress0/datatypes/sc-cdt1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort term 0) (declare-codatatypes ((llist_tree 0) (tree 0)) ( diff --git a/test/regress/regress0/datatypes/stream-singleton.smt2 b/test/regress/regress0/datatypes/stream-singleton.smt2 index 95d5f0c81..5ef101662 100644 --- a/test/regress/regress0/datatypes/stream-singleton.smt2 +++ b/test/regress/regress0/datatypes/stream-singleton.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-codatatypes ((Stream 0)) (((S (s Stream))))) diff --git a/test/regress/regress0/datatypes/tenum-bug.smt2 b/test/regress/regress0/datatypes/tenum-bug.smt2 index 6d25aefd0..3dd418cf3 100644 --- a/test/regress/regress0/datatypes/tenum-bug.smt2 +++ b/test/regress/regress0/datatypes/tenum-bug.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-datatypes ((DNat 0) (Nat 0)) (((dnat (data Nat))) diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc b/test/regress/regress0/datatypes/tuple-no-clash.cvc index ecdc8198f..586d5d259 100644 --- a/test/regress/regress0/datatypes/tuple-no-clash.cvc +++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; x : [ REAL, REAL ]; y : REAL; diff --git a/test/regress/regress0/decision/bug374b.smt2 b/test/regress/regress0/decision/bug374b.smt2 index f9d3f440d..be6d9d555 100644 --- a/test/regress/regress0/decision/bug374b.smt2 +++ b/test/regress/regress0/decision/bug374b.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --decision=justification --no-unconstrained ; EXPECT: unsat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-fun _substvar_245_ () Bool) (declare-fun _substvar_246_ () Bool) (declare-fun _substvar_247_ () Bool) diff --git a/test/regress/regress0/fmf/fd-false.smt2 b/test/regress/regress0/fmf/fd-false.smt2 index 0d8737a90..20170ea1b 100644 --- a/test/regress/regress0/fmf/fd-false.smt2 +++ b/test/regress/regress0/fmf/fd-false.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-fun ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-fun-rec f ((x Int)) Bool false) (assert (not (f 0))) (check-sat) diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2 index e4e1f65b4..cd577add4 100644 --- a/test/regress/regress0/fmf/fmc_unsound_model.smt2 +++ b/test/regress/regress0/fmf/fmc_unsound_model.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat ; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort a 0) (declare-datatypes ((tree 0)) (((Leaf (lab a))))) diff --git a/test/regress/regress0/fmf/forall_unit_data2.smt2 b/test/regress/regress0/fmf/forall_unit_data2.smt2 index 88f2631c5..7ceb74ad3 100644 --- a/test/regress/regress0/fmf/forall_unit_data2.smt2 +++ b/test/regress/regress0/fmf/forall_unit_data2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort a 0) (declare-datatypes ((prod 0)) (((Pair (gx a) (gy a))))) (declare-fun p () prod) diff --git a/test/regress/regress0/fmf/krs-sat.smt2 b/test/regress/regress0/fmf/krs-sat.smt2 index 17c6d9748..317f755d8 100644 --- a/test/regress/regress0/fmf/krs-sat.smt2 +++ b/test/regress/regress0/fmf/krs-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort $$unsorted 0) (declare-fun cowlNothing ($$unsorted) Bool) diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 index d951e6c50..7c9b54594 100644 --- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 +++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort a 0) (declare-fun __nun_card_witness_0 () a) diff --git a/test/regress/regress0/fmf/syn002-si-real-int.smt2 b/test/regress/regress0/fmf/syn002-si-real-int.smt2 index 769bc88af..1e72650c2 100644 --- a/test/regress/regress0/fmf/syn002-si-real-int.smt2 +++ b/test/regress/regress0/fmf/syn002-si-real-int.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort $$unsorted 0) (declare-fun $$rtu (Real) $$unsorted) diff --git a/test/regress/regress0/fmf/tail_rec.smt2 b/test/regress/regress0/fmf/tail_rec.smt2 index 2651db3f2..05ca33aac 100644 --- a/test/regress/regress0/fmf/tail_rec.smt2 +++ b/test/regress/regress0/fmf/tail_rec.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort elem 0) (declare-datatypes ((list 0)) (((Nil) (Cons (hd elem) (tl list))))) (define-fun-rec f ((x list)) elem diff --git a/test/regress/regress0/hung10_itesdk_output1.smt2 b/test/regress/regress0/hung10_itesdk_output1.smt2 index 2dcbf1fcd..37b180ad2 100644 --- a/test/regress/regress0/hung10_itesdk_output1.smt2 +++ b/test/regress/regress0/hung10_itesdk_output1.smt2 @@ -1,4 +1,4 @@ -( set-logic QF_ALL_SUPPORTED) +( set-logic QF_ALL) ( set-info :source | SMT-COMP'06 organizers |) ( set-info :smt-lib-version 2.6) ( set-info :category "check") diff --git a/test/regress/regress0/hung13sdk_output1.smt2 b/test/regress/regress0/hung13sdk_output1.smt2 index 7886153b0..d1c8da682 100644 --- a/test/regress/regress0/hung13sdk_output1.smt2 +++ b/test/regress/regress0/hung13sdk_output1.smt2 @@ -1,4 +1,4 @@ -( set-logic QF_ALL_SUPPORTED) +( set-logic QF_ALL) ( set-info :source | SMT-COMP'06 organizers |) ( set-info :smt-lib-version 2.6) ( set-info :category "check") diff --git a/test/regress/regress0/push-pop/bug654-dd.smt2 b/test/regress/regress0/push-pop/bug654-dd.smt2 index bd8419b57..a3f64d2b1 100644 --- a/test/regress/regress0/push-pop/bug654-dd.smt2 +++ b/test/regress/regress0/push-pop/bug654-dd.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --incremental --fmf-fun --strings-exp -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((List_T_C 0) (T_CustomerType 0)) ( ((List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C))) ((T_CustomerType$C_T_CustomerType (T_CustomerType$C_T_CustomerType$a_CompanyName Int) (T_CustomerType$C_T_CustomerType$a_ContactName Int) (ID Int))) 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)))) diff --git a/test/regress/regress0/rec-fun-const-parse-bug.smt2 b/test/regress/regress0/rec-fun-const-parse-bug.smt2 index b8c054833..a2f30eec3 100644 --- a/test/regress/regress0/rec-fun-const-parse-bug.smt2 +++ b/test/regress/regress0/rec-fun-const-parse-bug.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (define-funs-rec ( diff --git a/test/regress/regress0/rels/addr_book_0.cvc b/test/regress/regress0/rels/addr_book_0.cvc index 5b1ecefd8..bae21f178 100644 --- a/test/regress/regress0/rels/addr_book_0.cvc +++ b/test/regress/regress0/rels/addr_book_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom : TYPE; AtomTup : TYPE = [Atom]; AtomBinTup : TYPE = [Atom, Atom]; diff --git a/test/regress/regress0/rels/atom_univ2.cvc b/test/regress/regress0/rels/atom_univ2.cvc index e01d99dee..b290a2bb0 100644 --- a/test/regress/regress0/rels/atom_univ2.cvc +++ b/test/regress/regress0/rels/atom_univ2.cvc @@ -1,6 +1,6 @@ % EXPECT: unsat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom: TYPE;
a : SET OF [Atom];
diff --git a/test/regress/regress0/rels/card_transpose.cvc b/test/regress/regress0/rels/card_transpose.cvc index bde7fe53e..383b0bc21 100644 --- a/test/regress/regress0/rels/card_transpose.cvc +++ b/test/regress/regress0/rels/card_transpose.cvc @@ -1,5 +1,5 @@ % EXPECT: unknown (INCOMPLETE) -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; ASSERT (CARD(TRANSPOSE(x)) > 0); diff --git a/test/regress/regress0/rels/iden_0.cvc b/test/regress/regress0/rels/iden_0.cvc index 4c2693084..70e365b8f 100644 --- a/test/regress/regress0/rels/iden_0.cvc +++ b/test/regress/regress0/rels/iden_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom: TYPE; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/iden_1.cvc b/test/regress/regress0/rels/iden_1.cvc index 4f0581706..d874c9381 100644 --- a/test/regress/regress0/rels/iden_1.cvc +++ b/test/regress/regress0/rels/iden_1.cvc @@ -1,6 +1,6 @@ % EXPECT: unsat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom:TYPE; AtomPair: TYPE = [Atom, Atom]; x : SET OF AtomPair; diff --git a/test/regress/regress0/rels/join-eq-u-sat.cvc b/test/regress/regress0/rels/join-eq-u-sat.cvc index 0202cbb41..1c45aa46b 100644 --- a/test/regress/regress0/rels/join-eq-u-sat.cvc +++ b/test/regress/regress0/rels/join-eq-u-sat.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/join-eq-u.cvc b/test/regress/regress0/rels/join-eq-u.cvc index 4bc498aec..174e5dc16 100644 --- a/test/regress/regress0/rels/join-eq-u.cvc +++ b/test/regress/regress0/rels/join-eq-u.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc index 297898a81..b3dc944fd 100644 --- a/test/regress/regress0/rels/joinImg_0.cvc +++ b/test/regress/regress0/rels/joinImg_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; OPTION "sets-ext"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_1tup_0.cvc b/test/regress/regress0/rels/rel_1tup_0.cvc index 50d4defd5..90a22856e 100644 --- a/test/regress/regress0/rels/rel_1tup_0.cvc +++ b/test/regress/regress0/rels/rel_1tup_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntTup: TYPE = [INT]; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_complex_0.cvc b/test/regress/regress0/rels/rel_complex_0.cvc index dcb753973..c4cf0a01f 100644 --- a/test/regress/regress0/rels/rel_complex_0.cvc +++ b/test/regress/regress0/rels/rel_complex_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_complex_1.cvc b/test/regress/regress0/rels/rel_complex_1.cvc index 969d0d71c..4b23cdd2b 100644 --- a/test/regress/regress0/rels/rel_complex_1.cvc +++ b/test/regress/regress0/rels/rel_complex_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_conflict_0.cvc b/test/regress/regress0/rels/rel_conflict_0.cvc index c1b82339f..bc6750035 100644 --- a/test/regress/regress0/rels/rel_conflict_0.cvc +++ b/test/regress/regress0/rels/rel_conflict_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; e : IntPair; diff --git a/test/regress/regress0/rels/rel_join_0.cvc b/test/regress/regress0/rels/rel_join_0.cvc index 406b8d312..e0b76f2c9 100644 --- a/test/regress/regress0/rels/rel_join_0.cvc +++ b/test/regress/regress0/rels/rel_join_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_0_1.cvc b/test/regress/regress0/rels/rel_join_0_1.cvc index a7fa7efb9..5fa5f14ef 100644 --- a/test/regress/regress0/rels/rel_join_0_1.cvc +++ b/test/regress/regress0/rels/rel_join_0_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_1.cvc b/test/regress/regress0/rels/rel_join_1.cvc index c8921afb9..da3217642 100644 --- a/test/regress/regress0/rels/rel_join_1.cvc +++ b/test/regress/regress0/rels/rel_join_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_1_1.cvc b/test/regress/regress0/rels/rel_join_1_1.cvc index 75fc08387..ab00ed8b3 100644 --- a/test/regress/regress0/rels/rel_join_1_1.cvc +++ b/test/regress/regress0/rels/rel_join_1_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_2.cvc b/test/regress/regress0/rels/rel_join_2.cvc index cac7ce84d..0f50757fc 100644 --- a/test/regress/regress0/rels/rel_join_2.cvc +++ b/test/regress/regress0/rels/rel_join_2.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_2_1.cvc b/test/regress/regress0/rels/rel_join_2_1.cvc index 3e27b9cc5..4d412c649 100644 --- a/test/regress/regress0/rels/rel_join_2_1.cvc +++ b/test/regress/regress0/rels/rel_join_2_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_3.cvc b/test/regress/regress0/rels/rel_join_3.cvc index 6e190cecf..fb48aba77 100644 --- a/test/regress/regress0/rels/rel_join_3.cvc +++ b/test/regress/regress0/rels/rel_join_3.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_3_1.cvc b/test/regress/regress0/rels/rel_join_3_1.cvc index dedc4ae44..238028e18 100644 --- a/test/regress/regress0/rels/rel_join_3_1.cvc +++ b/test/regress/regress0/rels/rel_join_3_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_4.cvc b/test/regress/regress0/rels/rel_join_4.cvc index 030810f3d..c5210af1c 100644 --- a/test/regress/regress0/rels/rel_join_4.cvc +++ b/test/regress/regress0/rels/rel_join_4.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_5.cvc b/test/regress/regress0/rels/rel_join_5.cvc index 590e581a7..541e7bf37 100644 --- a/test/regress/regress0/rels/rel_join_5.cvc +++ b/test/regress/regress0/rels/rel_join_5.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_6.cvc b/test/regress/regress0/rels/rel_join_6.cvc index 17318872f..cd76d9afe 100644 --- a/test/regress/regress0/rels/rel_join_6.cvc +++ b/test/regress/regress0/rels/rel_join_6.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_join_7.cvc b/test/regress/regress0/rels/rel_join_7.cvc index fff5b6efe..c2f581114 100644 --- a/test/regress/regress0/rels/rel_join_7.cvc +++ b/test/regress/regress0/rels/rel_join_7.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_product_0.cvc b/test/regress/regress0/rels/rel_product_0.cvc index 09981be0b..3765fa8cb 100644 --- a/test/regress/regress0/rels/rel_product_0.cvc +++ b/test/regress/regress0/rels/rel_product_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT, INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_product_0_1.cvc b/test/regress/regress0/rels/rel_product_0_1.cvc index f141c7bd4..160543407 100644 --- a/test/regress/regress0/rels/rel_product_0_1.cvc +++ b/test/regress/regress0/rels/rel_product_0_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT, INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_product_1.cvc b/test/regress/regress0/rels/rel_product_1.cvc index 1826e5a75..6f64ee892 100644 --- a/test/regress/regress0/rels/rel_product_1.cvc +++ b/test/regress/regress0/rels/rel_product_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT, INT]; IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_product_1_1.cvc b/test/regress/regress0/rels/rel_product_1_1.cvc index 2d79cbc0c..8371632b9 100644 --- a/test/regress/regress0/rels/rel_product_1_1.cvc +++ b/test/regress/regress0/rels/rel_product_1_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT, INT]; IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_symbolic_1.cvc b/test/regress/regress0/rels/rel_symbolic_1.cvc index 08ed32411..91df3e6de 100644 --- a/test/regress/regress0/rels/rel_symbolic_1.cvc +++ b/test/regress/regress0/rels/rel_symbolic_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/rels/rel_symbolic_1_1.cvc index df2d7f412..7890ca2e2 100644 --- a/test/regress/regress0/rels/rel_symbolic_1_1.cvc +++ b/test/regress/regress0/rels/rel_symbolic_1_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_symbolic_2_1.cvc b/test/regress/regress0/rels/rel_symbolic_2_1.cvc index 082604dc2..ae0eeffae 100644 --- a/test/regress/regress0/rels/rel_symbolic_2_1.cvc +++ b/test/regress/regress0/rels/rel_symbolic_2_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_symbolic_3_1.cvc b/test/regress/regress0/rels/rel_symbolic_3_1.cvc index da0906dd2..bdfcaf5a8 100644 --- a/test/regress/regress0/rels/rel_symbolic_3_1.cvc +++ b/test/regress/regress0/rels/rel_symbolic_3_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tc_11.cvc b/test/regress/regress0/rels/rel_tc_11.cvc index 813b8235b..c3447622d 100644 --- a/test/regress/regress0/rels/rel_tc_11.cvc +++ b/test/regress/regress0/rels/rel_tc_11.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT, INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tc_2_1.cvc b/test/regress/regress0/rels/rel_tc_2_1.cvc index d5d42eaad..e396b886d 100644 --- a/test/regress/regress0/rels/rel_tc_2_1.cvc +++ b/test/regress/regress0/rels/rel_tc_2_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tc_3.cvc b/test/regress/regress0/rels/rel_tc_3.cvc index dc2138357..080c676a8 100644 --- a/test/regress/regress0/rels/rel_tc_3.cvc +++ b/test/regress/regress0/rels/rel_tc_3.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tc_3_1.cvc b/test/regress/regress0/rels/rel_tc_3_1.cvc index a9b2e8b98..f1d9bbadc 100644 --- a/test/regress/regress0/rels/rel_tc_3_1.cvc +++ b/test/regress/regress0/rels/rel_tc_3_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tc_7.cvc b/test/regress/regress0/rels/rel_tc_7.cvc index 1958c0eee..d68779310 100644 --- a/test/regress/regress0/rels/rel_tc_7.cvc +++ b/test/regress/regress0/rels/rel_tc_7.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tc_8.cvc b/test/regress/regress0/rels/rel_tc_8.cvc index ecf938c23..1a81ab569 100644 --- a/test/regress/regress0/rels/rel_tc_8.cvc +++ b/test/regress/regress0/rels/rel_tc_8.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_3_1.cvc b/test/regress/regress0/rels/rel_tp_3_1.cvc index 00c83e2d2..6284d3041 100644 --- a/test/regress/regress0/rels/rel_tp_3_1.cvc +++ b/test/regress/regress0/rels/rel_tp_3_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_0.cvc b/test/regress/regress0/rels/rel_tp_join_0.cvc index 9aaf6d9b1..7ea179d26 100644 --- a/test/regress/regress0/rels/rel_tp_join_0.cvc +++ b/test/regress/regress0/rels/rel_tp_join_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_1.cvc b/test/regress/regress0/rels/rel_tp_join_1.cvc index 5d9b5447f..845f26dce 100644 --- a/test/regress/regress0/rels/rel_tp_join_1.cvc +++ b/test/regress/regress0/rels/rel_tp_join_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_2.cvc b/test/regress/regress0/rels/rel_tp_join_2.cvc index 40471c1f9..a7b96b83b 100644 --- a/test/regress/regress0/rels/rel_tp_join_2.cvc +++ b/test/regress/regress0/rels/rel_tp_join_2.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_3.cvc b/test/regress/regress0/rels/rel_tp_join_3.cvc index 008b2aa1e..3f39f5773 100644 --- a/test/regress/regress0/rels/rel_tp_join_3.cvc +++ b/test/regress/regress0/rels/rel_tp_join_3.cvc @@ -1,6 +1,6 @@ % EXPECT: unsat % crash on this -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; w : SET OF IntPair; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc index c5a90ff29..852e93466 100644 --- a/test/regress/regress0/rels/rel_tp_join_eq_0.cvc +++ b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_int_0.cvc b/test/regress/regress0/rels/rel_tp_join_int_0.cvc index 8d149a48d..6ab678881 100644 --- a/test/regress/regress0/rels/rel_tp_join_int_0.cvc +++ b/test/regress/regress0/rels/rel_tp_join_int_0.cvc @@ -1,6 +1,6 @@ % EXPECT: unsat % crash on this -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; w : SET OF IntPair; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc index 77de6b829..18eaa51a9 100644 --- a/test/regress/regress0/rels/rel_tp_join_pro_0.cvc +++ b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT, INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_tp_join_var_0.cvc b/test/regress/regress0/rels/rel_tp_join_var_0.cvc index aacf6c054..08a9d0bb5 100644 --- a/test/regress/regress0/rels/rel_tp_join_var_0.cvc +++ b/test/regress/regress0/rels/rel_tp_join_var_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; w : SET OF IntPair; x : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_transpose_0.cvc b/test/regress/regress0/rels/rel_transpose_0.cvc index d46cacead..4687bd47c 100644 --- a/test/regress/regress0/rels/rel_transpose_0.cvc +++ b/test/regress/regress0/rels/rel_transpose_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_transpose_1.cvc b/test/regress/regress0/rels/rel_transpose_1.cvc index bbd6e5743..c205edabc 100644 --- a/test/regress/regress0/rels/rel_transpose_1.cvc +++ b/test/regress/regress0/rels/rel_transpose_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntTup: TYPE = [INT, INT, INT]; x : SET OF IntTup; y : SET OF IntTup; diff --git a/test/regress/regress0/rels/rel_transpose_1_1.cvc b/test/regress/regress0/rels/rel_transpose_1_1.cvc index 627e20fbf..62afa7a93 100644 --- a/test/regress/regress0/rels/rel_transpose_1_1.cvc +++ b/test/regress/regress0/rels/rel_transpose_1_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntTup: TYPE = [INT, INT, INT]; x : SET OF IntTup; y : SET OF IntTup; diff --git a/test/regress/regress0/rels/rel_transpose_3.cvc b/test/regress/regress0/rels/rel_transpose_3.cvc index 06cc82c45..7208b4ce6 100644 --- a/test/regress/regress0/rels/rel_transpose_3.cvc +++ b/test/regress/regress0/rels/rel_transpose_3.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_transpose_4.cvc b/test/regress/regress0/rels/rel_transpose_4.cvc index 882148013..0cf2c3b63 100644 --- a/test/regress/regress0/rels/rel_transpose_4.cvc +++ b/test/regress/regress0/rels/rel_transpose_4.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_transpose_5.cvc b/test/regress/regress0/rels/rel_transpose_5.cvc index 203e8b3d2..8f6d48e35 100644 --- a/test/regress/regress0/rels/rel_transpose_5.cvc +++ b/test/regress/regress0/rels/rel_transpose_5.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_transpose_6.cvc b/test/regress/regress0/rels/rel_transpose_6.cvc index 3923e26b6..c7b8ebbae 100644 --- a/test/regress/regress0/rels/rel_transpose_6.cvc +++ b/test/regress/regress0/rels/rel_transpose_6.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rel_transpose_7.cvc b/test/regress/regress0/rels/rel_transpose_7.cvc index bcc3babc8..4d1426990 100644 --- a/test/regress/regress0/rels/rel_transpose_7.cvc +++ b/test/regress/regress0/rels/rel_transpose_7.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/rels-sharing-simp.cvc b/test/regress/regress0/rels/rels-sharing-simp.cvc index 26bc94a43..641d71d5a 100644 --- a/test/regress/regress0/rels/rels-sharing-simp.cvc +++ b/test/regress/regress0/rels/rels-sharing-simp.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; w : SET OF IntPair; z : SET OF IntPair; diff --git a/test/regress/regress0/sep/dispose-1.smt2 b/test/regress/regress0/sep/dispose-1.smt2 index aff32e241..45dd29459 100644 --- a/test/regress/regress0/sep/dispose-1.smt2 +++ b/test/regress/regress0/sep/dispose-1.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress0/sep/dup-nemp.smt2 b/test/regress/regress0/sep/dup-nemp.smt2 index 454b73f64..5682a0a02 100644 --- a/test/regress/regress0/sep/dup-nemp.smt2 +++ b/test/regress/regress0/sep/dup-nemp.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-sort Loc 0) (declare-const l Loc) diff --git a/test/regress/regress0/sep/issue5343-err.smt2 b/test/regress/regress0/sep/issue5343-err.smt2 index ea37815fa..b3246de59 100644 --- a/test/regress/regress0/sep/issue5343-err.smt2 +++ b/test/regress/regress0/sep/issue5343-err.smt2 @@ -3,6 +3,6 @@ ; EXPECT: (error "ERROR: the type of the separation logic heap has not been declared (e.g. via a declare-heap command), and we have a separation logic constraint (wand true true) ; EXPECT: ") ; EXIT: 1 -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (assert (wand true true)) (check-sat) diff --git a/test/regress/regress0/sep/nspatial-simp.smt2 b/test/regress/regress0/sep/nspatial-simp.smt2 index e57e50ea2..953c5252d 100644 --- a/test/regress/regress0/sep/nspatial-simp.smt2 +++ b/test/regress/regress0/sep/nspatial-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-fun x () Int) (declare-heap (Int Int)) diff --git a/test/regress/regress0/sep/pto-01.smt2 b/test/regress/regress0/sep/pto-01.smt2 index f980ac13f..380e95f7c 100644 --- a/test/regress/regress0/sep/pto-01.smt2 +++ b/test/regress/regress0/sep/pto-01.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress0/sep/pto-02.smt2 b/test/regress/regress0/sep/pto-02.smt2 index 111048c70..2e293558e 100644 --- a/test/regress/regress0/sep/pto-02.smt2 +++ b/test/regress/regress0/sep/pto-02.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress0/sep/sep-01.smt2 b/test/regress/regress0/sep/sep-01.smt2 index 8e577d5b7..f2ca28413 100644 --- a/test/regress/regress0/sep/sep-01.smt2 +++ b/test/regress/regress0/sep/sep-01.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress0/sep/sep-plus1.smt2 b/test/regress/regress0/sep/sep-plus1.smt2 index b843c1eda..ad97e2725 100644 --- a/test/regress/regress0/sep/sep-plus1.smt2 +++ b/test/regress/regress0/sep/sep-plus1.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 index fc7bd0a51..312c97542 100644 --- a/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 +++ b/test/regress/regress0/sep/sep-simp-unsat-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-sort U 0) (declare-heap (U U)) diff --git a/test/regress/regress0/sep/simple-080420-const-sets.smt2 b/test/regress/regress0/sep/simple-080420-const-sets.smt2 index 785017d5c..a8039ce5b 100644 --- a/test/regress/regress0/sep/simple-080420-const-sets.smt2 +++ b/test/regress/regress0/sep/simple-080420-const-sets.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-option :produce-models true) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2 index aac8382a7..2a836bef9 100644 --- a/test/regress/regress0/sep/skolem_emp.smt2 +++ b/test/regress/regress0/sep/skolem_emp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (assert (not (_ emp Int Int))) (check-sat) diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2 index 46d96e84c..2c742c60f 100644 --- a/test/regress/regress0/sep/trees-1.smt2 +++ b/test/regress/regress0/sep/trees-1.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-sort Loc 0) diff --git a/test/regress/regress0/sep/wand-crash.smt2 b/test/regress/regress0/sep/wand-crash.smt2 index 95156a20c..02511bbae 100644 --- a/test/regress/regress0/sep/wand-crash.smt2 +++ b/test/regress/regress0/sep/wand-crash.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (assert (wand (_ emp Int Int) (_ emp Int Int))) (check-sat) diff --git a/test/regress/regress0/sets/card-3sets.cvc b/test/regress/regress0/sets/card-3sets.cvc index cac10f39c..7422df91c 100644 --- a/test/regress/regress0/sets/card-3sets.cvc +++ b/test/regress/regress0/sets/card-3sets.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; x : SET OF INT; y : SET OF INT; z : SET OF INT; diff --git a/test/regress/regress0/sets/card3-ground.smt2 b/test/regress/regress0/sets/card3-ground.smt2 index 54a9a5cfc..7b42b8a8a 100644 --- a/test/regress/regress0/sets/card3-ground.smt2 +++ b/test/regress/regress0/sets/card3-ground.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun S () (Set Int)) (assert (>= (card S) 3)) diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc index 91388a56c..64df0790a 100644 --- a/test/regress/regress0/sets/complement.cvc +++ b/test/regress/regress0/sets/complement.cvc @@ -1,6 +1,6 @@ % EXPECT: sat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom: TYPE; a : SET OF [Atom]; b : SET OF [Atom]; diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc index b8100bf5f..a3dd25477 100644 --- a/test/regress/regress0/sets/complement2.cvc +++ b/test/regress/regress0/sets/complement2.cvc @@ -1,6 +1,6 @@ % EXPECT: unsat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom: TYPE;
a : SET OF Atom;
b : SET OF Atom;
diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc index fa0a31e40..762d186ed 100644 --- a/test/regress/regress0/sets/complement3.cvc +++ b/test/regress/regress0/sets/complement3.cvc @@ -1,6 +1,6 @@ % EXPECT: sat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom : TYPE; C32 : SET OF [Atom]; C2 : SET OF [Atom]; diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc index 06d2b5049..11f9428c3 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc +++ b/test/regress/regress0/sets/cvc-sample.cvc @@ -6,7 +6,7 @@ % EXPECT: unsat % EXPECT: not_entailed OPTION "incremental" true; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; SetInt : TYPE = SET OF INT; x : SET OF INT; y : SET OF INT; diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2 index 51400a05a..47bc7aa58 100644 --- a/test/regress/regress0/sets/dt-simp-mem.smt2 +++ b/test/regress/regress0/sets/dt-simp-mem.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-datatypes ((D 0)) (((A (a Int))))) (declare-fun x1 () D) diff --git a/test/regress/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2 index 2b2322d46..7296fcc28 100644 --- a/test/regress/regress0/sets/emptyset.smt2 +++ b/test/regress/regress0/sets/emptyset.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (assert (member 5 (as emptyset (Set Int) ))) (check-sat) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index cb816a306..06f86ae3c 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-fun A () (Set Int) ) (declare-fun B () (Set Int) ) diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2 index 0b8c5ab65..7b8f78218 100644 --- a/test/regress/regress0/sets/error2.smt2 +++ b/test/regress/regress0/sets/error2.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (assert (= (as emptyset (Set Int)) (singleton 5))) (check-sat) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index 71bb8a3e6..448022a2e 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 index 652307645..a7c2bec8d 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun x () Int) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 index c4ee3b710..ff83b0fb5 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 index eb48b023a..90d3a6372 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 index 35110d831..b20fb4f3d 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) ; Observed behavior diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 index df659f0fb..1c28759b6 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) ; Observed diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 index af67a69a7..8b879b3ec 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2 index b5d85c7e8..35b89645a 100644 --- a/test/regress/regress0/sets/setel-eq.smt2 +++ b/test/regress/regress0/sets/setel-eq.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2 index 8fd29a244..adccd51c5 100644 --- a/test/regress/regress0/sets/sets-equal.smt2 +++ b/test/regress/regress0/sets/sets-equal.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun x () Int) (declare-fun y () Int) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index d3d8a9044..2faf72768 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (define-sort SetInt () (Set Int)) (declare-fun a () (Set Int)) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index 0f43ee10d..8ac414829 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (define-sort SetInt () (Set Int)) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 3bc2da065..b92c4b2cf 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -4,7 +4,7 @@ ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) ; Something simple to test parsing diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2 index caada9606..1ac2e1603 100644 --- a/test/regress/regress0/sets/sets-sharing.smt2 +++ b/test/regress/regress0/sets/sets-sharing.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun S () (Set Int)) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 index 56ba520dc..b794633e3 100644 --- a/test/regress/regress0/sets/sets-union.smt2 +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 index 6a73c5b91..bb969f866 100644 --- a/test/regress/regress0/sets/union-1a-flip.smt2 +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-1a.smt2 b/test/regress/regress0/sets/union-1a.smt2 index 8636cb220..ad684070f 100644 --- a/test/regress/regress0/sets/union-1a.smt2 +++ b/test/regress/regress0/sets/union-1a.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 index e2b19b31a..228452f54 100644 --- a/test/regress/regress0/sets/union-1b-flip.smt2 +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-1b.smt2 b/test/regress/regress0/sets/union-1b.smt2 index c354923c9..8829b6152 100644 --- a/test/regress/regress0/sets/union-1b.smt2 +++ b/test/regress/regress0/sets/union-1b.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 index 6e2933975..52d2e7e8c 100644 --- a/test/regress/regress0/sets/union-2.smt2 +++ b/test/regress/regress0/sets/union-2.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) diff --git a/test/regress/regress0/strings/idof-rewrites.smt2 b/test/regress/regress0/strings/idof-rewrites.smt2 index f52f0c9f3..ce77fed0a 100644 --- a/test/regress/regress0/strings/idof-rewrites.smt2 +++ b/test/regress/regress0/strings/idof-rewrites.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :strings-exp true) (declare-fun s () String) diff --git a/test/regress/regress0/strings/ilc-like.smt2 b/test/regress/regress0/strings/ilc-like.smt2 index bb708ee5c..6c7b0b501 100644 --- a/test/regress/regress0/strings/ilc-like.smt2 +++ b/test/regress/regress0/strings/ilc-like.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress0/strings/indexof-sym-simp.smt2 b/test/regress/regress0/strings/indexof-sym-simp.smt2 index f4cf5c055..f492ca2b0 100644 --- a/test/regress/regress0/strings/indexof-sym-simp.smt2 +++ b/test/regress/regress0/strings/indexof-sym-simp.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :strings-exp true) (declare-fun s () String) diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2 index 3200c815d..18905ae65 100644 --- a/test/regress/regress0/strings/issue1189.smt2 +++ b/test/regress/regress0/strings/issue1189.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.6) -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :strings-exp true) (declare-const x Int) diff --git a/test/regress/regress0/strings/tolower-simple.smt2 b/test/regress/regress0/strings/tolower-simple.smt2 index 9d2273f8d..5de5a2447 100644 --- a/test/regress/regress0/strings/tolower-simple.smt2 +++ b/test/regress/regress0/strings/tolower-simple.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status sat) (declare-const x String) diff --git a/test/regress/regress0/sygus/dt-sel-parse1.sy b/test/regress/regress0/sygus/dt-sel-parse1.sy index 52f068055..05ba6b85e 100644 --- a/test/regress/regress0/sygus/dt-sel-parse1.sy +++ b/test/regress/regress0/sygus/dt-sel-parse1.sy @@ -1,6 +1,6 @@ ; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((IntRange 0)) (((IntRange (lower Int) (upper Int))))) diff --git a/test/regress/regress1/bug507.smt2 b/test/regress/regress1/bug507.smt2 index 0176d1043..fb6998d71 100644 --- a/test/regress/regress1/bug507.smt2 +++ b/test/regress/regress1/bug507.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: -q ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/test/regress/regress1/bug516.smt2 b/test/regress/regress1/bug516.smt2 index 43d18575e..f9d478b07 100644 --- a/test/regress/regress1/bug516.smt2 +++ b/test/regress/regress1/bug516.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --fmf-bound-int -q ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :incremental true) (declare-fun P (Int) Bool) diff --git a/test/regress/regress1/bug519.smt2 b/test/regress/regress1/bug519.smt2 index 6f413ad8b..fdc906faf 100644 --- a/test/regress/regress1/bug519.smt2 +++ b/test/regress/regress1/bug519.smt2 @@ -2,7 +2,7 @@ ; EXPECT: sat ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) ; must make parts 1 through 6 with different deadlines diff --git a/test/regress/regress1/bug521.smt2 b/test/regress/regress1/bug521.smt2 index 73153e71b..276c60c58 100644 --- a/test/regress/regress1/bug521.smt2 +++ b/test/regress/regress1/bug521.smt2 @@ -4,7 +4,7 @@ (set-info :smt-lib-version 2.6) (set-info :status sat) (set-option :produce-models true) -(set-logic ALL_SUPPORTED) +(set-logic ALL) ; done setting options ; Boogie universal background predicate diff --git a/test/regress/regress1/bug543.smt2 b/test/regress/regress1/bug543.smt2 index 9155de7a9..d28540331 100644 --- a/test/regress/regress1/bug543.smt2 +++ b/test/regress/regress1/bug543.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --incremental ; EXPECT: sat (set-option :produce-models true) -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-fun _substvar_1807_ () Bool) (declare-fun local_id_x$1 () (_ BitVec 32)) (declare-fun local_id_x$2 () (_ BitVec 32)) diff --git a/test/regress/regress1/bug567.smt2 b/test/regress/regress1/bug567.smt2 index 94cf3b547..15af93632 100644 --- a/test/regress/regress1/bug567.smt2 +++ b/test/regress/regress1/bug567.smt2 @@ -2,7 +2,7 @@ ; EXPECT: unknown ; EXPECT: unsat ; EXPECT: unknown -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((OptInt0 0)) (((Some (value0 Int)) (None)))) (declare-datatypes ((List0 0)) (((Cons (head0 Int) (tail0 List0)) (Nil)))) diff --git a/test/regress/regress1/bug681.smt2 b/test/regress/regress1/bug681.smt2 index 8bc1bd6d0..1d77cf270 100644 --- a/test/regress/regress1/bug681.smt2 +++ b/test/regress/regress1/bug681.smt2 @@ -1,6 +1,6 @@ ; EXIT: 1 ; EXPECT: (error "Array theory solver does not yet support write-chains connecting two different constant arrays") -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-fun start!1 () Bool) (assert start!1) diff --git a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 index 07f2dae6a..19627c288 100644 --- a/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 +++ b/test/regress/regress1/bv/bv-int-collapse2-sat.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun t () Int) (assert (> t 0)) diff --git a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 index 7e98460b8..9da8d4ca8 100644 --- a/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 +++ b/test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun t () (_ BitVec 16)) (assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65535)))) diff --git a/test/regress/regress1/bv/cmu-rdk-3.smt2 b/test/regress/regress1/bv/cmu-rdk-3.smt2 index 742dd593b..a667da854 100644 --- a/test/regress/regress1/bv/cmu-rdk-3.smt2 +++ b/test/regress/regress1/bv/cmu-rdk-3.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun y () Int) diff --git a/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2 b/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2 index 1d9b4ef37..1e43e3cdc 100644 --- a/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2 +++ b/test/regress/regress1/datatypes/dt-param-card4-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-proofs ; EXPECT: unsat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-datatypes ((Pair 2)) ((par (T S) ((pair (first T) (second S)))))) diff --git a/test/regress/regress1/datatypes/manos-model.smt2 b/test/regress/regress1/datatypes/manos-model.smt2 index e418743fb..24e3d350b 100644 --- a/test/regress/regress1/datatypes/manos-model.smt2 +++ b/test/regress/regress1/datatypes/manos-model.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((tuple2!879 0)) (((tuple2!879!880 (_1!881 Int) (_2!882 Int))))) diff --git a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 index f1d20befc..54668bb1c 100644 --- a/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 +++ b/test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-datatypes ((array!896 0)) (((array!896!897 (size!898 (_ BitVec 32)) (content!899 (Array (_ BitVec 32) (_ BitVec 32))))))) (declare-datatypes ((tuple2!900 0)) (((tuple2!900!901 (_1!902 array!896) (_2!903 (_ BitVec 32)))))) diff --git a/test/regress/regress1/fmf/bug0909.smt2 b/test/regress/regress1/fmf/bug0909.smt2 index 3823e4bcc..84b4af6be 100644 --- a/test/regress/regress1/fmf/bug0909.smt2 +++ b/test/regress/regress1/fmf/bug0909.smt2 @@ -2,7 +2,7 @@ ; EXPECT: unsat ; Preamble -------------- (set-option :produce-models true) -(set-logic ALL_SUPPORTED) +(set-logic ALL) ;(declare-datatypes ((x2 0)) (((x1)))) (declare-datatypes ((x5 0)) (((x3) (x4)))) (declare-sort x6 0) diff --git a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 index d700d3b18..8a853c4b6 100644 --- a/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 +++ b/test/regress/regress1/fmf/bug723-irrelevant-funs.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-fun-rlv --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-fun $$isTrue$$ ((b Bool)) Bool b) (define-fun $$isFalse$$ ((b Bool)) Bool (not b)) (define-fun $$toString$$ ((b Bool)) String (ite b "true" "false")) diff --git a/test/regress/regress1/fmf/datatypes-ufinite-nested.smt2 b/test/regress/regress1/fmf/datatypes-ufinite-nested.smt2 index 6b30907ae..1b7974861 100644 --- a/test/regress/regress1/fmf/datatypes-ufinite-nested.smt2 +++ b/test/regress/regress1/fmf/datatypes-ufinite-nested.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort U 0) (declare-fun a () U) (declare-fun b () U) diff --git a/test/regress/regress1/fmf/datatypes-ufinite.smt2 b/test/regress/regress1/fmf/datatypes-ufinite.smt2 index b0ff1d11b..32fa954c5 100644 --- a/test/regress/regress1/fmf/datatypes-ufinite.smt2 +++ b/test/regress/regress1/fmf/datatypes-ufinite.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort U 0) (declare-fun a () U) (declare-fun b () U) diff --git a/test/regress/regress1/fmf/dt-proper-model.smt2 b/test/regress/regress1/fmf/dt-proper-model.smt2 index 0e66db996..f5164b741 100644 --- a/test/regress/regress1/fmf/dt-proper-model.smt2 +++ b/test/regress/regress1/fmf/dt-proper-model.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort U 0) (declare-datatypes ((D 0)) (((cons (x Int) (y U))))) diff --git a/test/regress/regress1/fmf/fib-core.smt2 b/test/regress/regress1/fmf/fib-core.smt2 index e00f19ad4..1a7950a6d 100644 --- a/test/regress/regress1/fmf/fib-core.smt2 +++ b/test/regress/regress1/fmf/fib-core.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --fmf-inst-engine ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-sort I_fb 0) (declare-fun fb_arg_0_1 (I_fb) Int) diff --git a/test/regress/regress1/fmf/forall_unit_data.smt2 b/test/regress/regress1/fmf/forall_unit_data.smt2 index 5ede5f72d..411c03c8a 100644 --- a/test/regress/regress1/fmf/forall_unit_data.smt2 +++ b/test/regress/regress1/fmf/forall_unit_data.smt2 @@ -2,7 +2,7 @@ ; EXPECT: sat (set-option :produce-models true) (set-option :interactive-mode true) -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort a 0) (declare-datatypes ((w 0)) (((Wrap (unw a))))) (declare-fun x () w) diff --git a/test/regress/regress1/fmf/fore19-exp2-core.smt2 b/test/regress/regress1/fmf/fore19-exp2-core.smt2 index efa38fcfc..475151c59 100644 --- a/test/regress/regress1/fmf/fore19-exp2-core.smt2 +++ b/test/regress/regress1/fmf/fore19-exp2-core.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((St 0) (Ex 0) (List!2293 0)) (((Block!2236 (body!2237 List!2293)) (For!2238 (init!2239 St) (expr!2240 Ex) (step!2241 St) (body!2242 St)) (IfTE (expr!2244 Ex) (then!2245 St) (elze!2246 St)) (Skip!2250) (While (expr!2252 Ex) (body St))) diff --git a/test/regress/regress1/fmf/german169.smt2 b/test/regress/regress1/fmf/german169.smt2 index c4a40ccc1..c0203312b 100644 --- a/test/regress/regress1/fmf/german169.smt2 +++ b/test/regress/regress1/fmf/german169.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-datatypes ((UNIT 0)) (((Unit)))) (declare-datatypes ((BOOL 0)) (((Truth) (Falsity)))) diff --git a/test/regress/regress1/fmf/german73.smt2 b/test/regress/regress1/fmf/german73.smt2 index fbe011cfd..1cb241084 100644 --- a/test/regress/regress1/fmf/german73.smt2 +++ b/test/regress/regress1/fmf/german73.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((UNIT 0)) (((Unit)))) (declare-datatypes ((BOOL 0)) (((Truth) (Falsity)))) diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 index 7f3a5b28f..7241dab4b 100644 --- a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 +++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort a_ 0) (declare-fun __nun_card_witness_0 () a_) diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2 index 378380779..2b91b8c7a 100644 --- a/test/regress/regress1/fmf/loopy_coda.smt2 +++ b/test/regress/regress1/fmf/loopy_coda.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-sort a 0) (declare-fun __nun_card_witness_0 () a) diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 index b2c42d7c5..2ed01adc6 100644 --- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 +++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil)))) (declare-fun app (Lst Lst) Lst) diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2 index 25851f6e0..32974ef41 100644 --- a/test/regress/regress1/fmf/nun-0208-to.smt2 +++ b/test/regress/regress1/fmf/nun-0208-to.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort b__ 0) (declare-fun __nun_card_witness_0_ () b__) (declare-sort a__ 0) diff --git a/test/regress/regress1/fmf/radu-quant-set.smt2 b/test/regress/regress1/fmf/radu-quant-set.smt2 index 09d5cc706..180894ca5 100644 --- a/test/regress/regress1/fmf/radu-quant-set.smt2 +++ b/test/regress/regress1/fmf/radu-quant-set.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-bound ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-const A (Set Int)) (declare-const B (Set Int)) diff --git a/test/regress/regress1/fmf/refcount24.cvc.smt2 b/test/regress/regress1/fmf/refcount24.cvc.smt2 index 75bf89380..54354cab2 100644 --- a/test/regress/regress1/fmf/refcount24.cvc.smt2 +++ b/test/regress/regress1/fmf/refcount24.cvc.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :smt-lib-version 2.6) (set-info :category "unknown") (set-info :status sat) diff --git a/test/regress/regress1/fmf/sc-crash-052316.smt2 b/test/regress/regress1/fmf/sc-crash-052316.smt2 index 5c695e482..5decff044 100644 --- a/test/regress/regress1/fmf/sc-crash-052316.smt2 +++ b/test/regress/regress1/fmf/sc-crash-052316.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-sort g_ 0) (declare-fun __nun_card_witness_0_ () g_) diff --git a/test/regress/regress1/fmf/with-ind-104-core.smt2 b/test/regress/regress1/fmf/with-ind-104-core.smt2 index 508629f8e..2ff74dd48 100644 --- a/test/regress/regress1/fmf/with-ind-104-core.smt2 +++ b/test/regress/regress1/fmf/with-ind-104-core.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((Nat!2409 0)) (((succ!2410 (pred!2411 Nat!2409)) (zero!2412)) )) diff --git a/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2 b/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2 index 01a274e8a..e483abcb8 100644 --- a/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2 +++ b/test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --incremental --fmf-fun -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) (define-fun-rec sum ((l Lst)) Int (ite ((_ is nil) l) 0 (+ (head l) (sum (tail l))))) 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))))) diff --git a/test/regress/regress1/rels/addr_book_1.cvc b/test/regress/regress1/rels/addr_book_1.cvc index 34176f274..8e7cdbd9d 100644 --- a/test/regress/regress1/rels/addr_book_1.cvc +++ b/test/regress/regress1/rels/addr_book_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom : TYPE; AtomTup : TYPE = [Atom]; AtomBinTup : TYPE = [Atom, Atom]; diff --git a/test/regress/regress1/rels/addr_book_1_1.cvc b/test/regress/regress1/rels/addr_book_1_1.cvc index 3273ade3a..c320d925f 100644 --- a/test/regress/regress1/rels/addr_book_1_1.cvc +++ b/test/regress/regress1/rels/addr_book_1_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom : TYPE; AtomTup : TYPE = [Atom]; AtomBinTup : TYPE = [Atom, Atom]; diff --git a/test/regress/regress1/rels/bv1-unit.cvc b/test/regress/regress1/rels/bv1-unit.cvc index 970ebdc8c..95fb5f02c 100644 --- a/test/regress/regress1/rels/bv1-unit.cvc +++ b/test/regress/regress1/rels/bv1-unit.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; DATATYPE unit = u END; BvPair: TYPE = [BITVECTOR(1), unit, BITVECTOR(1)]; x : SET OF BvPair; diff --git a/test/regress/regress1/rels/bv1-unitb.cvc b/test/regress/regress1/rels/bv1-unitb.cvc index 50a5bb48a..0a09614a7 100644 --- a/test/regress/regress1/rels/bv1-unitb.cvc +++ b/test/regress/regress1/rels/bv1-unitb.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; DATATYPE unitb = ub(data : BITVECTOR(1)) END; BvPair: TYPE = [BITVECTOR(1), unitb, BITVECTOR(1)]; x : SET OF BvPair; diff --git a/test/regress/regress1/rels/bv1.cvc b/test/regress/regress1/rels/bv1.cvc index 95e7419ba..7e0f18953 100644 --- a/test/regress/regress1/rels/bv1.cvc +++ b/test/regress/regress1/rels/bv1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; x : SET OF BvPair; y : SET OF BvPair; diff --git a/test/regress/regress1/rels/bv1p-sat.cvc b/test/regress/regress1/rels/bv1p-sat.cvc index 5eceb214c..a48cb6407 100644 --- a/test/regress/regress1/rels/bv1p-sat.cvc +++ b/test/regress/regress1/rels/bv1p-sat.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; x : SET OF BvPair; y : SET OF BvPair; diff --git a/test/regress/regress1/rels/bv1p.cvc b/test/regress/regress1/rels/bv1p.cvc index 130ccae97..0e8803ce6 100644 --- a/test/regress/regress1/rels/bv1p.cvc +++ b/test/regress/regress1/rels/bv1p.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; x : SET OF BvPair; y : SET OF BvPair; diff --git a/test/regress/regress1/rels/bv2.cvc b/test/regress/regress1/rels/bv2.cvc index d7162de7c..f3a729f2e 100644 --- a/test/regress/regress1/rels/bv2.cvc +++ b/test/regress/regress1/rels/bv2.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; BvPair: TYPE = [BITVECTOR(2), BITVECTOR(2)]; x : SET OF BvPair; y : SET OF BvPair; diff --git a/test/regress/regress1/rels/iden_1_1.cvc b/test/regress/regress1/rels/iden_1_1.cvc index 985a35a89..16bf42115 100644 --- a/test/regress/regress1/rels/iden_1_1.cvc +++ b/test/regress/regress1/rels/iden_1_1.cvc @@ -1,6 +1,6 @@ % EXPECT: sat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom:TYPE; AtomPair: TYPE = [Atom, Atom]; x : SET OF AtomPair; diff --git a/test/regress/regress1/rels/join-eq-structure-and.cvc b/test/regress/regress1/rels/join-eq-structure-and.cvc index 177410b1e..329946c46 100644 --- a/test/regress/regress1/rels/join-eq-structure-and.cvc +++ b/test/regress/regress1/rels/join-eq-structure-and.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/join-eq-structure.cvc b/test/regress/regress1/rels/join-eq-structure.cvc index e27d3811c..3cfb309c9 100644 --- a/test/regress/regress1/rels/join-eq-structure.cvc +++ b/test/regress/regress1/rels/join-eq-structure.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/joinImg_0_1.cvc b/test/regress/regress1/rels/joinImg_0_1.cvc index 4e69394bd..789e36a92 100644 --- a/test/regress/regress1/rels/joinImg_0_1.cvc +++ b/test/regress/regress1/rels/joinImg_0_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; OPTION "sets-ext"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress1/rels/joinImg_0_2.cvc b/test/regress/regress1/rels/joinImg_0_2.cvc index e15920804..89d767c7f 100644 --- a/test/regress/regress1/rels/joinImg_0_2.cvc +++ b/test/regress/regress1/rels/joinImg_0_2.cvc @@ -1,6 +1,6 @@ % EXPECT: sat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/joinImg_1.cvc b/test/regress/regress1/rels/joinImg_1.cvc index 81f208fc4..1849ffb84 100644 --- a/test/regress/regress1/rels/joinImg_1.cvc +++ b/test/regress/regress1/rels/joinImg_1.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; diff --git a/test/regress/regress1/rels/joinImg_1_1.cvc b/test/regress/regress1/rels/joinImg_1_1.cvc index 003770a1b..748b57062 100644 --- a/test/regress/regress1/rels/joinImg_1_1.cvc +++ b/test/regress/regress1/rels/joinImg_1_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; diff --git a/test/regress/regress1/rels/joinImg_2.cvc b/test/regress/regress1/rels/joinImg_2.cvc index a4acfe6c6..2ce3f3f69 100644 --- a/test/regress/regress1/rels/joinImg_2.cvc +++ b/test/regress/regress1/rels/joinImg_2.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; diff --git a/test/regress/regress1/rels/joinImg_2_1.cvc b/test/regress/regress1/rels/joinImg_2_1.cvc index 03f88be37..0238b253f 100644 --- a/test/regress/regress1/rels/joinImg_2_1.cvc +++ b/test/regress/regress1/rels/joinImg_2_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; diff --git a/test/regress/regress1/rels/prod-mod-eq.cvc b/test/regress/regress1/rels/prod-mod-eq.cvc index 96ef2ffba..0e6a00fb4 100644 --- a/test/regress/regress1/rels/prod-mod-eq.cvc +++ b/test/regress/regress1/rels/prod-mod-eq.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntPairPair: TYPE = [INT, INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress1/rels/prod-mod-eq2.cvc b/test/regress/regress1/rels/prod-mod-eq2.cvc index b9341a216..871b1b7d7 100644 --- a/test/regress/regress1/rels/prod-mod-eq2.cvc +++ b/test/regress/regress1/rels/prod-mod-eq2.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntPairPair: TYPE = [INT, INT, INT, INT]; x : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_complex_3.cvc b/test/regress/regress1/rels/rel_complex_3.cvc index 492c94432..94639eff0 100644 --- a/test/regress/regress1/rels/rel_complex_3.cvc +++ b/test/regress/regress1/rels/rel_complex_3.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_complex_4.cvc b/test/regress/regress1/rels/rel_complex_4.cvc index f473b00aa..d75bf0cd4 100644 --- a/test/regress/regress1/rels/rel_complex_4.cvc +++ b/test/regress/regress1/rels/rel_complex_4.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_complex_5.cvc b/test/regress/regress1/rels/rel_complex_5.cvc index d64817187..27225e72c 100644 --- a/test/regress/regress1/rels/rel_complex_5.cvc +++ b/test/regress/regress1/rels/rel_complex_5.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT]; x : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_mix_0_1.cvc b/test/regress/regress1/rels/rel_mix_0_1.cvc index 723a9b2e2..75f4965f2 100644 --- a/test/regress/regress1/rels/rel_mix_0_1.cvc +++ b/test/regress/regress1/rels/rel_mix_0_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; IntTup: TYPE = [INT]; x : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_pressure_0.cvc b/test/regress/regress1/rels/rel_pressure_0.cvc index 0e9646f95..5648b7ba8 100644 --- a/test/regress/regress1/rels/rel_pressure_0.cvc +++ b/test/regress/regress1/rels/rel_pressure_0.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tc_10_1.cvc b/test/regress/regress1/rels/rel_tc_10_1.cvc index 65686ef08..391b58bfb 100644 --- a/test/regress/regress1/rels/rel_tc_10_1.cvc +++ b/test/regress/regress1/rels/rel_tc_10_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tc_4.cvc b/test/regress/regress1/rels/rel_tc_4.cvc index a32e8b66d..b194902cb 100644 --- a/test/regress/regress1/rels/rel_tc_4.cvc +++ b/test/regress/regress1/rels/rel_tc_4.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tc_4_1.cvc b/test/regress/regress1/rels/rel_tc_4_1.cvc index 484d09ec3..6dae90f80 100644 --- a/test/regress/regress1/rels/rel_tc_4_1.cvc +++ b/test/regress/regress1/rels/rel_tc_4_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tc_5_1.cvc b/test/regress/regress1/rels/rel_tc_5_1.cvc index a4b2fe1db..d49a19217 100644 --- a/test/regress/regress1/rels/rel_tc_5_1.cvc +++ b/test/regress/regress1/rels/rel_tc_5_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tc_6.cvc b/test/regress/regress1/rels/rel_tc_6.cvc index 2bc552170..b751dc201 100644 --- a/test/regress/regress1/rels/rel_tc_6.cvc +++ b/test/regress/regress1/rels/rel_tc_6.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tc_9_1.cvc b/test/regress/regress1/rels/rel_tc_9_1.cvc index 8a9e8eeca..af7bbb044 100644 --- a/test/regress/regress1/rels/rel_tc_9_1.cvc +++ b/test/regress/regress1/rels/rel_tc_9_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tp_2.cvc b/test/regress/regress1/rels/rel_tp_2.cvc index 441e79c45..73702ea8e 100644 --- a/test/regress/regress1/rels/rel_tp_2.cvc +++ b/test/regress/regress1/rels/rel_tp_2.cvc @@ -1,5 +1,5 @@ % EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/rel_tp_join_2_1.cvc b/test/regress/regress1/rels/rel_tp_join_2_1.cvc index 9a79582b7..51d6c1050 100644 --- a/test/regress/regress1/rels/rel_tp_join_2_1.cvc +++ b/test/regress/regress1/rels/rel_tp_join_2_1.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress1/rels/set-strat.cvc b/test/regress/regress1/rels/set-strat.cvc index 0dee0e84d..c56a2b16e 100644 --- a/test/regress/regress1/rels/set-strat.cvc +++ b/test/regress/regress1/rels/set-strat.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [ INT, INT]; SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ]; x : SET OF IntPair; diff --git a/test/regress/regress1/rels/strat.cvc b/test/regress/regress1/rels/strat.cvc index b91ddbbe8..dc5c2f37d 100644 --- a/test/regress/regress1/rels/strat.cvc +++ b/test/regress/regress1/rels/strat.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; IntPair: TYPE = [ INT, INT]; IntIntPair: TYPE = [ IntPair, IntPair]; x : SET OF IntIntPair; diff --git a/test/regress/regress1/sep/chain-int.smt2 b/test/regress/regress1/sep/chain-int.smt2 index 6aaca31c5..14cd98ae2 100644 --- a/test/regress/regress1/sep/chain-int.smt2 +++ b/test/regress/regress1/sep/chain-int.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/crash1220.smt2 b/test/regress/regress1/sep/crash1220.smt2 index 4df23fd80..241f69b77 100644 --- a/test/regress/regress1/sep/crash1220.smt2 +++ b/test/regress/regress1/sep/crash1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/dispose-list-4-init.smt2 b/test/regress/regress1/sep/dispose-list-4-init.smt2 index 0ee63cc8a..e9915bf4b 100644 --- a/test/regress/regress1/sep/dispose-list-4-init.smt2 +++ b/test/regress/regress1/sep/dispose-list-4-init.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-sort Loc 0) (declare-heap (Loc Loc)) diff --git a/test/regress/regress1/sep/emp2-quant-unsat.smt2 b/test/regress/regress1/sep/emp2-quant-unsat.smt2 index a0921aa31..cdca1a909 100644 --- a/test/regress/regress1/sep/emp2-quant-unsat.smt2 +++ b/test/regress/regress1/sep/emp2-quant-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --quant-epr ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun u () U) diff --git a/test/regress/regress1/sep/finite-witness-sat.smt2 b/test/regress/regress1/sep/finite-witness-sat.smt2 index ce16e6f14..479dbe2b2 100644 --- a/test/regress/regress1/sep/finite-witness-sat.smt2 +++ b/test/regress/regress1/sep/finite-witness-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --quant-epr ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort Loc 0) (declare-const l Loc) (declare-heap (Loc Loc)) diff --git a/test/regress/regress1/sep/fmf-nemp-2.smt2 b/test/regress/regress1/sep/fmf-nemp-2.smt2 index 49420145e..e6e2aca98 100644 --- a/test/regress/regress1/sep/fmf-nemp-2.smt2 +++ b/test/regress/regress1/sep/fmf-nemp-2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --no-check-models ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort U 0) (declare-heap (U Int)) (declare-fun u1 () U) diff --git a/test/regress/regress1/sep/loop-1220.smt2 b/test/regress/regress1/sep/loop-1220.smt2 index 41078391a..c6d239ec0 100644 --- a/test/regress/regress1/sep/loop-1220.smt2 +++ b/test/regress/regress1/sep/loop-1220.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/pto-04.smt2 b/test/regress/regress1/sep/pto-04.smt2 index e3d3ea7a1..7c430da06 100644 --- a/test/regress/regress1/sep/pto-04.smt2 +++ b/test/regress/regress1/sep/pto-04.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/quant_wand.smt2 b/test/regress/regress1/sep/quant_wand.smt2 index bb4e40308..87f0a974b 100644 --- a/test/regress/regress1/sep/quant_wand.smt2 +++ b/test/regress/regress1/sep/quant_wand.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-02.smt2 b/test/regress/regress1/sep/sep-02.smt2 index a67394d90..befb36090 100644 --- a/test/regress/regress1/sep/sep-02.smt2 +++ b/test/regress/regress1/sep/sep-02.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-03.smt2 b/test/regress/regress1/sep/sep-03.smt2 index f29d081fc..aabdaa100 100644 --- a/test/regress/regress1/sep/sep-03.smt2 +++ b/test/regress/regress1/sep/sep-03.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-fmf-priority.smt2 b/test/regress/regress1/sep/sep-fmf-priority.smt2 index d916a50e5..9b72898cd 100644 --- a/test/regress/regress1/sep/sep-fmf-priority.smt2 +++ b/test/regress/regress1/sep/sep-fmf-priority.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --quant-epr ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-sort Loc 0) (declare-const l Loc) diff --git a/test/regress/regress1/sep/sep-neg-1refine.smt2 b/test/regress/regress1/sep/sep-neg-1refine.smt2 index 81b107ab5..867d4ccb8 100644 --- a/test/regress/regress1/sep/sep-neg-1refine.smt2 +++ b/test/regress/regress1/sep/sep-neg-1refine.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-nstrict.smt2 b/test/regress/regress1/sep/sep-neg-nstrict.smt2 index 6594a1075..0896d9180 100644 --- a/test/regress/regress1/sep/sep-neg-nstrict.smt2 +++ b/test/regress/regress1/sep/sep-neg-nstrict.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-nstrict2.smt2 b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 index 0243282a3..e66a39f23 100644 --- a/test/regress/regress1/sep/sep-neg-nstrict2.smt2 +++ b/test/regress/regress1/sep/sep-neg-nstrict2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-simple.smt2 b/test/regress/regress1/sep/sep-neg-simple.smt2 index 8b23a6da8..dc114b0dd 100644 --- a/test/regress/regress1/sep/sep-neg-simple.smt2 +++ b/test/regress/regress1/sep/sep-neg-simple.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-neg-swap.smt2 b/test/regress/regress1/sep/sep-neg-swap.smt2 index ba83f2575..b34e6031f 100644 --- a/test/regress/regress1/sep/sep-neg-swap.smt2 +++ b/test/regress/regress1/sep/sep-neg-swap.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-nterm-again.smt2 b/test/regress/regress1/sep/sep-nterm-again.smt2 index 43fb7b00d..0b38bd189 100644 --- a/test/regress/regress1/sep/sep-nterm-again.smt2 +++ b/test/regress/regress1/sep/sep-nterm-again.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-nterm-val-model.smt2 b/test/regress/regress1/sep/sep-nterm-val-model.smt2 index 635f0895a..34349a5cc 100644 --- a/test/regress/regress1/sep/sep-nterm-val-model.smt2 +++ b/test/regress/regress1/sep/sep-nterm-val-model.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/sep-simp-unc.smt2 b/test/regress/regress1/sep/sep-simp-unc.smt2 index 88950d655..eee6fa211 100644 --- a/test/regress/regress1/sep/sep-simp-unc.smt2 +++ b/test/regress/regress1/sep/sep-simp-unc.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-sort U 0) (declare-heap (U U)) diff --git a/test/regress/regress1/sep/simple-neg-sat.smt2 b/test/regress/regress1/sep/simple-neg-sat.smt2 index 929a8e66f..612776cfa 100644 --- a/test/regress/regress1/sep/simple-neg-sat.smt2 +++ b/test/regress/regress1/sep/simple-neg-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 index 1b7932dc4..c6fa301f0 100644 --- a/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 +++ b/test/regress/regress1/sep/split-find-unsat-w-emp.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/split-find-unsat.smt2 b/test/regress/regress1/sep/split-find-unsat.smt2 index ff725f048..346c0083e 100644 --- a/test/regress/regress1/sep/split-find-unsat.smt2 +++ b/test/regress/regress1/sep/split-find-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: unsat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-heap (Int Int)) diff --git a/test/regress/regress1/sep/wand-0526-sat.smt2 b/test/regress/regress1/sep/wand-0526-sat.smt2 index 556be6c18..a07d0b8ae 100644 --- a/test/regress/regress1/sep/wand-0526-sat.smt2 +++ b/test/regress/regress1/sep/wand-0526-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (declare-fun x () Int) (declare-fun y () Int) diff --git a/test/regress/regress1/sep/wand-false.smt2 b/test/regress/regress1/sep/wand-false.smt2 index 9f95c06b7..3d496782c 100644 --- a/test/regress/regress1/sep/wand-false.smt2 +++ b/test/regress/regress1/sep/wand-false.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) (declare-fun x () Int) diff --git a/test/regress/regress1/sep/wand-nterm-simp.smt2 b/test/regress/regress1/sep/wand-nterm-simp.smt2 index 4ecc8ad1e..47d39eb0b 100644 --- a/test/regress/regress1/sep/wand-nterm-simp.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (_ emp Int Int) (pto x 3))) diff --git a/test/regress/regress1/sep/wand-nterm-simp2.smt2 b/test/regress/regress1/sep/wand-nterm-simp2.smt2 index 5b7c92a4a..647421665 100644 --- a/test/regress/regress1/sep/wand-nterm-simp2.smt2 +++ b/test/regress/regress1/sep/wand-nterm-simp2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) (declare-fun x () Int) diff --git a/test/regress/regress1/sep/wand-simp-sat.smt2 b/test/regress/regress1/sep/wand-simp-sat.smt2 index ec63a762e..79c12c028 100644 --- a/test/regress/regress1/sep/wand-simp-sat.smt2 +++ b/test/regress/regress1/sep/wand-simp-sat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-heap (Int Int)) (declare-fun x () Int) (assert (wand (pto x 1) (pto x 1))) diff --git a/test/regress/regress1/sep/wand-simp-sat2.smt2 b/test/regress/regress1/sep/wand-simp-sat2.smt2 index 315071c05..76aed570f 100644 --- a/test/regress/regress1/sep/wand-simp-sat2.smt2 +++ b/test/regress/regress1/sep/wand-simp-sat2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --no-check-models ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (declare-heap (Int Int)) (declare-fun x () Int) diff --git a/test/regress/regress1/sep/wand-simp-unsat.smt2 b/test/regress/regress1/sep/wand-simp-unsat.smt2 index dabdc18e4..2e90dfb26 100644 --- a/test/regress/regress1/sep/wand-simp-unsat.smt2 +++ b/test/regress/regress1/sep/wand-simp-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: unsat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (declare-fun x () Int) (declare-heap (Int Int)) (assert (wand (pto x 1) (pto x 3))) diff --git a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 index 3c0ef1dda..666d16367 100644 --- a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 +++ b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) ; What was the bug? diff --git a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 index 7b5294aec..4863baa64 100644 --- a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index 282325f14..dcfd13521 100644 --- a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 index 38477c46a..9e5962a24 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) (define-fun smt_set_emp () mySet (as emptyset mySet)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 index e282e446e..88cf21aa8 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) (define-fun smt_set_emp () mySet (as emptyset mySet)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 index 10ed4be7c..1967497da 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 index 6165b98de..cb1dfc842 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 index 83dfe41e5..426661ba2 100644 --- a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 index c455caa28..eded56674 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 index 977bf3795..7d3421463 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 index 623376e37..4c83655ed 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 index 1388b9bfa..535646c7b 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 index 26ee05f3c..4eb8fc269 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 index 8c92d1c6b..6e26ef4c7 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 index d2c8a744d..4fc6b7347 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 index 0121479e9..681033794 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 index 708ebb2ca..eb45d9ef9 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :produce-models true) (set-option :sets-ext true) diff --git a/test/regress/regress1/sets/is_singleton1.smt2 b/test/regress/regress1/sets/is_singleton1.smt2 index 5764a7d45..a6f1961cd 100644 --- a/test/regress/regress1/sets/is_singleton1.smt2 +++ b/test/regress/regress1/sets/is_singleton1.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun S () (Set Int)) (declare-fun x () Int) diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 index e9fca1716..49268953d 100644 --- a/test/regress/regress1/sets/issue2904.smt2 +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) ; conjecture set nonempty(~b & ~c) diff --git a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 index 0fc8ca067..be1e36a97 100644 --- a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 @@ -19,7 +19,7 @@ ; adding terms to d_pendingEverInserted was moved from addToPending() ; to getLemma(). -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc b/test/regress/regress1/sets/sets-tuple-poly.cvc index 3f8662ef7..d286e46e4 100644 --- a/test/regress/regress1/sets/sets-tuple-poly.cvc +++ b/test/regress/regress1/sets/sets-tuple-poly.cvc @@ -1,7 +1,7 @@ % COMMAND-LINE: % EXPECT: sat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; a : SET OF [REAL, INT]; b : SET OF [INT, REAL]; diff --git a/test/regress/regress1/strings/cmu-2db2-extf-reg.smt2 b/test/regress/regress1/strings/cmu-2db2-extf-reg.smt2 index b513494b8..b3d108ef7 100644 --- a/test/regress/regress1/strings/cmu-2db2-extf-reg.smt2 +++ b/test/regress/regress1/strings/cmu-2db2-extf-reg.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress1/strings/cmu-5042-0707-2.smt2 b/test/regress/regress1/strings/cmu-5042-0707-2.smt2 index 637142dfb..4b3e08eae 100644 --- a/test/regress/regress1/strings/cmu-5042-0707-2.smt2 +++ b/test/regress/regress1/strings/cmu-5042-0707-2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress1/strings/cmu-inc-nlpp-071516.smt2 b/test/regress/regress1/strings/cmu-inc-nlpp-071516.smt2 index 1208ca169..f41e68d2d 100644 --- a/test/regress/regress1/strings/cmu-inc-nlpp-071516.smt2 +++ b/test/regress/regress1/strings/cmu-inc-nlpp-071516.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :strings-exp true) diff --git a/test/regress/regress1/strings/cmu-substr-rw.smt2 b/test/regress/regress1/strings/cmu-substr-rw.smt2 index a4d649d7f..4f7e61948 100644 --- a/test/regress/regress1/strings/cmu-substr-rw.smt2 +++ b/test/regress/regress1/strings/cmu-substr-rw.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :strings-exp true) diff --git a/test/regress/regress1/strings/crash-1019.smt2 b/test/regress/regress1/strings/crash-1019.smt2 index 317840ddb..ae7c79ee7 100644 --- a/test/regress/regress1/strings/crash-1019.smt2 +++ b/test/regress/regress1/strings/crash-1019.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) diff --git a/test/regress/regress1/strings/gm-inc-071516-2.smt2 b/test/regress/regress1/strings/gm-inc-071516-2.smt2 index 1650190f8..305bdd58a 100644 --- a/test/regress/regress1/strings/gm-inc-071516-2.smt2 +++ b/test/regress/regress1/strings/gm-inc-071516-2.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :strings-exp true) diff --git a/test/regress/regress1/strings/idof-handg.smt2 b/test/regress/regress1/strings/idof-handg.smt2 index 40aff3168..3766a6d85 100644 --- a/test/regress/regress1/strings/idof-handg.smt2 +++ b/test/regress/regress1/strings/idof-handg.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status sat) (declare-fun s () String) diff --git a/test/regress/regress1/strings/idof-nconst-index.smt2 b/test/regress/regress1/strings/idof-nconst-index.smt2 index eba492220..954d446d2 100644 --- a/test/regress/regress1/strings/idof-nconst-index.smt2 +++ b/test/regress/regress1/strings/idof-nconst-index.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status sat) (declare-fun s () String) diff --git a/test/regress/regress1/strings/idof-neg-index.smt2 b/test/regress/regress1/strings/idof-neg-index.smt2 index c24fcc00a..e886a53fd 100644 --- a/test/regress/regress1/strings/idof-neg-index.smt2 +++ b/test/regress/regress1/strings/idof-neg-index.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) (declare-fun s () String) diff --git a/test/regress/regress1/strings/idof-triv.smt2 b/test/regress/regress1/strings/idof-triv.smt2 index 314adedf8..ce8439f0c 100644 --- a/test/regress/regress1/strings/idof-triv.smt2 +++ b/test/regress/regress1/strings/idof-triv.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :strings-exp true) (declare-fun string () String) diff --git a/test/regress/regress1/strings/ilc-l-nt.smt2 b/test/regress/regress1/strings/ilc-l-nt.smt2 index 9e1cc2bc5..efd733530 100644 --- a/test/regress/regress1/strings/ilc-l-nt.smt2 +++ b/test/regress/regress1/strings/ilc-l-nt.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (set-option :strings-exp true) diff --git a/test/regress/regress1/strings/issue3090.smt2 b/test/regress/regress1/strings/issue3090.smt2 index dc04289d6..dc89ea650 100644 --- a/test/regress/regress1/strings/issue3090.smt2 +++ b/test/regress/regress1/strings/issue3090.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) (declare-const id String) diff --git a/test/regress/regress1/strings/issue3217.smt2 b/test/regress/regress1/strings/issue3217.smt2 index 4fd35999d..7e9acbd78 100644 --- a/test/regress/regress1/strings/issue3217.smt2 +++ b/test/regress/regress1/strings/issue3217.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) (declare-fun a () String) diff --git a/test/regress/regress1/strings/issue3272.smt2 b/test/regress/regress1/strings/issue3272.smt2 index 622e294d8..0fc8cee26 100644 --- a/test/regress/regress1/strings/issue3272.smt2 +++ b/test/regress/regress1/strings/issue3272.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.6) -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status sat) (declare-fun a () String) diff --git a/test/regress/regress1/strings/issue3357.smt2 b/test/regress/regress1/strings/issue3357.smt2 index 6951d47e1..ca80f7f81 100644 --- a/test/regress/regress1/strings/issue3357.smt2 +++ b/test/regress/regress1/strings/issue3357.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) (declare-fun a () String) diff --git a/test/regress/regress1/strings/tolower-find.smt2 b/test/regress/regress1/strings/tolower-find.smt2 index ff27a285a..80c797b3e 100644 --- a/test/regress/regress1/strings/tolower-find.smt2 +++ b/test/regress/regress1/strings/tolower-find.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status sat) (declare-const x String) diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy index b5d7bff91..5af4407f7 100644 --- a/test/regress/regress1/sygus/clock-inc-tuple.sy +++ b/test/regress/regress1/sygus/clock-inc-tuple.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-var m Int) (declare-var s Int) (declare-var inc Int) diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy index d0027d685..9b57339db 100644 --- a/test/regress/regress1/sygus/error1-dt.sy +++ b/test/regress/regress1/sygus/error1-dt.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-active-gen=enum -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((IntRange 0)) (((IntRange (lower Int) (upper Int))))) diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy index f3cfa09a2..fef48f364 100644 --- a/test/regress/regress1/sygus/extract.sy +++ b/test/regress/regress1/sygus/extract.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(declare-datatype Ex ((Ex2 (ex Int))))
(synth-fun ident ((x1 Ex)) Int
diff --git a/test/regress/regress1/sygus/issue3461.sy b/test/regress/regress1/sygus/issue3461.sy index 08b5738c1..ebd6dd346 100644 --- a/test/regress/regress1/sygus/issue3461.sy +++ b/test/regress/regress1/sygus/issue3461.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-out=status -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatype Doc ((D (owner Int) (body Int)))) diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy index c6b7d032a..f1c99a28f 100644 --- a/test/regress/regress1/sygus/list-head-x.sy +++ b/test/regress/regress1/sygus/list-head-x.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) diff --git a/test/regress/regress2/bug394.smt2 b/test/regress/regress2/bug394.smt2 index 79fbf2e44..c0c8ca48c 100644 --- a/test/regress/regress2/bug394.smt2 +++ b/test/regress/regress2/bug394.smt2 @@ -15,7 +15,7 @@ (set-option :print-success false) (set-info :smt-lib-version 2.6) ;(set-option :produce-models true) -(set-logic ALL_SUPPORTED) +(set-logic ALL) ; done setting options ; Boogie universal background predicate diff --git a/test/regress/regress2/bug674.smt2 b/test/regress/regress2/bug674.smt2 index cce0c963a..dc736539a 100644 --- a/test/regress/regress2/bug674.smt2 +++ b/test/regress/regress2/bug674.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --quant-ind --incremental -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) (define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2)))) (define-fun-rec rev ((l Lst)) Lst (ite ((_ is nil) l) nil (app (rev (tail l)) (cons (head l) nil)))) diff --git a/test/regress/regress2/bug765.smt2 b/test/regress/regress2/bug765.smt2 index 6c1c633a9..b0d85363d 100644 --- a/test/regress/regress2/bug765.smt2 +++ b/test/regress/regress2/bug765.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((Color 0)) ( ((red) (white) (blue)) diff --git a/test/regress/regress2/issue6495-dup-pat-term.smt2 b/test/regress/regress2/issue6495-dup-pat-term.smt2 index 3c8d0df61..c619bb37d 100644 --- a/test/regress/regress2/issue6495-dup-pat-term.smt2 +++ b/test/regress/regress2/issue6495-dup-pat-term.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: -i -q
; EXPECT: unsat
-(set-logic ALL_SUPPORTED)
+(set-logic ALL)
(set-info :status unsat)
(declare-sort |T@[Int]Int| 0)
(declare-datatypes ((T@Vec_2846 0)) (((Vec_2846 (|v#Vec_2846| |T@[Int]Int|) (|l#Vec_2846| Int) ) ) ))
diff --git a/test/regress/regress2/quantifiers/nunchaku2309663.nun.min.smt2 b/test/regress/regress2/quantifiers/nunchaku2309663.nun.min.smt2 index 2ae8a60f4..c6f8a1be2 100644 --- a/test/regress/regress2/quantifiers/nunchaku2309663.nun.min.smt2 +++ b/test/regress/regress2/quantifiers/nunchaku2309663.nun.min.smt2 @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --finite-model-find -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-datatypes ((nat__ 0)) (((Suc__ (_select_Suc___0 nat__)) (zero__)))) (declare-sort a__ 0) diff --git a/test/regress/regress2/strings/cmu-dis-0707-3.smt2 b/test/regress/regress2/strings/cmu-dis-0707-3.smt2 index fcdcded39..4df45e833 100644 --- a/test/regress/regress2/strings/cmu-dis-0707-3.smt2 +++ b/test/regress/regress2/strings/cmu-dis-0707-3.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-info :smt-lib-version 2.6) (set-option :strings-exp true) diff --git a/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 index 140c7c659..02e5f6492 100644 --- a/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 +++ b/test/regress/regress2/strings/cmu-disagree-0707-dd.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (set-option :strings-exp true) (set-option :strings-fmf true) diff --git a/test/regress/regress2/strings/cmu-prereg-fmf.smt2 b/test/regress/regress2/strings/cmu-prereg-fmf.smt2 index 0d6827cf7..30ea49f4b 100644 --- a/test/regress/regress2/strings/cmu-prereg-fmf.smt2 +++ b/test/regress/regress2/strings/cmu-prereg-fmf.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --strings-exp --strings-fmf ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun url () String) diff --git a/test/regress/regress2/strings/cmu-repl-len-nterm.smt2 b/test/regress/regress2/strings/cmu-repl-len-nterm.smt2 index 004db77ed..f55a61b2e 100644 --- a/test/regress/regress2/strings/cmu-repl-len-nterm.smt2 +++ b/test/regress/regress2/strings/cmu-repl-len-nterm.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun url () String) diff --git a/test/regress/regress2/strings/issue3203.smt2 b/test/regress/regress2/strings/issue3203.smt2 index 6d4064ad5..f0bc8d031 100644 --- a/test/regress/regress2/strings/issue3203.smt2 +++ b/test/regress/regress2/strings/issue3203.smt2 @@ -1,6 +1,6 @@ ; Temporarily disable checking of unsat cores (see issue #3606) ; COMMAND-LINE: --no-check-unsat-cores -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) (declare-fun a () String) diff --git a/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 b/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 index 04ea50b72..91502a9e7 100644 --- a/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 +++ b/test/regress/regress3/quantifiers/ForElimination-scala-9.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (declare-datatypes ((Statement!1556 0) (Expression!1578 0) (List!1617 0)) ( ((Assign!1557 (varID!1558 (_ BitVec 32)) (expr!1559 Expression!1578)) (Block!1560 (body!1561 List!1617)) (For!1562 (init!1563 Statement!1556) (expr!1564 Expression!1578) (step!1565 Statement!1556) (body!1566 Statement!1556)) (IfThenElse!1567 (expr!1568 Expression!1578) (then!1569 Statement!1556) (elze!1570 Statement!1556)) (Print!1571 (msg!1572 (_ BitVec 32)) (varID!1573 (_ BitVec 32))) (Skip!1574) (While!1575 (expr!1576 Expression!1578) (body!1577 Statement!1556))) ((And!1579 (lhs!1580 Expression!1578) (rhs!1581 Expression!1578)) (Division!1582 (lhs!1583 Expression!1578) (rhs!1584 Expression!1578)) (Equals!1585 (lhs!1586 Expression!1578) (rhs!1587 Expression!1578)) (GreaterThan!1588 (lhs!1589 Expression!1578) (rhs!1590 Expression!1578)) (IntLiteral!1591 (value!1592 (_ BitVec 32))) (LessThan!1593 (lhs!1594 Expression!1578) (rhs!1595 Expression!1578)) (Minus!1596 (lhs!1597 Expression!1578) (rhs!1598 Expression!1578)) (Modulo!1599 (lhs!1600 Expression!1578) (rhs!1601 Expression!1578)) (Neg!1602 (expr!1603 Expression!1578)) (Not!1604 (expr!1605 Expression!1578)) (Or!1606 (lhs!1607 Expression!1578) (rhs!1608 Expression!1578)) (Plus!1609 (lhs!1610 Expression!1578) (rhs!1611 Expression!1578)) (Times!1612 (lhs!1613 Expression!1578) (rhs!1614 Expression!1578)) (Var!1615 (varID!1616 (_ BitVec 32)))) diff --git a/test/regress/regress4/bug396.smt2 b/test/regress/regress4/bug396.smt2 index 639d4f7eb..d3f04bd5a 100644 --- a/test/regress/regress4/bug396.smt2 +++ b/test/regress/regress4/bug396.smt2 @@ -13,7 +13,7 @@ (set-option :print-success false) (set-info :smt-lib-version 2.6) ;(set-option :produce-models true) -(set-logic ALL_SUPPORTED) +(set-logic ALL) ; done setting options ; Boogie universal background predicate diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index bc8f3ed74..018207293 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1552,7 +1552,7 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct) TEST_F(TestApiBlackSolver, declareSeparationHeap) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); Sort integer = d_solver.getIntegerSort(); ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer)); // cannot declare separation logic heap more than once @@ -1592,7 +1592,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm1) TEST_F(TestApiBlackSolver, getSeparationHeapTerm2) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "false"); checkSimpleSeparationConstraints(&d_solver); @@ -1601,7 +1601,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm2) TEST_F(TestApiBlackSolver, getSeparationHeapTerm3) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkFalse(); @@ -1612,7 +1612,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm3) TEST_F(TestApiBlackSolver, getSeparationHeapTerm4) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkTrue(); @@ -1623,7 +1623,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm4) TEST_F(TestApiBlackSolver, getSeparationHeapTerm5) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); checkSimpleSeparationConstraints(&d_solver); @@ -1642,7 +1642,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm1) TEST_F(TestApiBlackSolver, getSeparationNilTerm2) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "false"); checkSimpleSeparationConstraints(&d_solver); @@ -1651,7 +1651,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm2) TEST_F(TestApiBlackSolver, getSeparationNilTerm3) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkFalse(); @@ -1662,7 +1662,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm3) TEST_F(TestApiBlackSolver, getSeparationNilTerm4) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); Term t = d_solver.mkTrue(); @@ -1673,7 +1673,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm4) TEST_F(TestApiBlackSolver, getSeparationNilTerm5) { - d_solver.setLogic("ALL_SUPPORTED"); + d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); d_solver.setOption("produce-models", "true"); checkSimpleSeparationConstraints(&d_solver); diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index e51929cad..7a6e34abb 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -500,7 +500,7 @@ TEST_F(TestTheoryWhiteLogicInfo, smtlib_logics) ASSERT_FALSE(info.hasEverything()); ASSERT_FALSE(info.hasNothing()); - info = LogicInfo("QF_ALL_SUPPORTED"); + info = LogicInfo("QF_ALL"); ASSERT_TRUE(info.isLocked()); ASSERT_FALSE(info.isPure(THEORY_BOOL)); ASSERT_TRUE(info.isSharingEnabled()); @@ -519,7 +519,7 @@ TEST_F(TestTheoryWhiteLogicInfo, smtlib_logics) ASSERT_FALSE(info.hasEverything()); ASSERT_FALSE(info.hasNothing()); - info = LogicInfo("ALL_SUPPORTED"); + info = LogicInfo("ALL"); ASSERT_TRUE(info.isLocked()); ASSERT_FALSE(info.isPure(THEORY_BOOL)); ASSERT_TRUE(info.isSharingEnabled()); |