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