Merge branch 'master' into issue6661issue6661

19 files changed, 19 insertions, 19 deletions

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))
 ))