144 files changed, 144 insertions, 144 deletions
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)))))