Better support for HOL parsing and set up (#6697)

This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.

For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).

70 files changed, 104 insertions, 151 deletions

diff --git a/test/regress/regress0/declare-fun-is-match.smt2 b/test/regress/regress0/declare-fun-is-match.smt2
index f3877edca..0b69011c8 100644
--- a/test/regress/regress0/declare-fun-is-match.smt2
+++ b/test/regress/regress0/declare-fun-is-match.smt2
@@ -1,7 +1,6 @@
 ; EXPECT: sat
-; COMMAND-LINE: --uf-ho
 (set-info :smt-lib-version 2.6)
-(set-logic UFIDL)
+(set-logic HO_UFIDL)
 (set-info :status sat)
 (declare-fun match (Int Int) Int)
 (declare-fun is (Int Int) Int)
diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2
index 6a516a3ca..c42bad235 100644
--- a/test/regress/regress0/fp/issue4277-assign-func.smt2
+++ b/test/regress/regress0/fp/issue4277-assign-func.smt2
@@ -1,8 +1,7 @@
 ; COMMAND-LINE: -q
 ; EXPECT: sat
 ; REQUIRES: symfpu
-(set-logic ALL)
-(set-option :uf-ho true)
+(set-logic HO_ALL)
 (set-option :assign-function-values false)
 (set-info :status sat)
 (declare-fun b () (_ BitVec 1))
diff --git a/test/regress/regress0/ho/apply-collapse-sat.smt2 b/test/regress/regress0/ho/apply-collapse-sat.smt2
index 74a9df660..64aaa797d 100644
--- a/test/regress/regress0/ho/apply-collapse-sat.smt2
+++ b/test/regress/regress0/ho/apply-collapse-sat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/apply-collapse-unsat.smt2 b/test/regress/regress0/ho/apply-collapse-unsat.smt2
index 101de9081..45eeb23a7 100644
--- a/test/regress/regress0/ho/apply-collapse-unsat.smt2
+++ b/test/regress/regress0/ho/apply-collapse-unsat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
index 0ed7fe44b..c4b517e56 100644
--- a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
+++ b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
@@ -1,4 +1,3 @@
-% COMMAND-LINE:  --uf-ho
 % EXPECT: % SZS status Unsatisfiable for bug_nodbuilding_interpreted_SYO042^1
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress0/ho/cong-full-apply.smt2 b/test/regress/regress0/ho/cong-full-apply.smt2
index 0ff147b97..493bbf140 100644
--- a/test/regress/regress0/ho/cong-full-apply.smt2
+++ b/test/regress/regress0/ho/cong-full-apply.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status unsat)
 (declare-fun f (Int) Int)
 (declare-fun g (Int) Int)
diff --git a/test/regress/regress0/ho/cong.smt2 b/test/regress/regress0/ho/cong.smt2
index 531356568..b1feafe3e 100644
--- a/test/regress/regress0/ho/cong.smt2
+++ b/test/regress/regress0/ho/cong.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)
diff --git a/test/regress/regress0/ho/declare-fun-variants.smt2 b/test/regress/regress0/ho/declare-fun-variants.smt2
index 990423fb3..de37f7044 100644
--- a/test/regress/regress0/ho/declare-fun-variants.smt2
+++ b/test/regress/regress0/ho/declare-fun-variants.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-fun f (Int Int) Int)
 (declare-fun g (Int) (-> Int Int))
diff --git a/test/regress/regress0/ho/def-fun-flatten.smt2 b/test/regress/regress0/ho/def-fun-flatten.smt2
index af33098f5..81af169a7 100644
--- a/test/regress/regress0/ho/def-fun-flatten.smt2
+++ b/test/regress/regress0/ho/def-fun-flatten.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-fun f (Int Int) Int)
 (define-fun g ((x Int)) (-> Int Int) (f x))
diff --git a/test/regress/regress0/ho/ext-finite-unsat.smt2 b/test/regress/regress0/ho/ext-finite-unsat.smt2
index 1719d5ad1..282cc3bda 100644
--- a/test/regress/regress0/ho/ext-finite-unsat.smt2
+++ b/test/regress/regress0/ho/ext-finite-unsat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)
diff --git a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2
index 7031829d4..175ced858 100644
--- a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2
+++ b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f ((-> U U)) U)
diff --git a/test/regress/regress0/ho/ext-ho.smt2 b/test/regress/regress0/ho/ext-ho.smt2
index 02e51654e..613533ebd 100644
--- a/test/regress/regress0/ho/ext-ho.smt2
+++ b/test/regress/regress0/ho/ext-ho.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f ((-> U U)) U)
diff --git a/test/regress/regress0/ho/ext-sat-partial-eval.smt2 b/test/regress/regress0/ho/ext-sat-partial-eval.smt2
index f3392f1ba..cc63c52ea 100644
--- a/test/regress/regress0/ho/ext-sat-partial-eval.smt2
+++ b/test/regress/regress0/ho/ext-sat-partial-eval.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/ext-sat.smt2 b/test/regress/regress0/ho/ext-sat.smt2
index 772b6eaa0..f91fb8240 100644
--- a/test/regress/regress0/ho/ext-sat.smt2
+++ b/test/regress/regress0/ho/ext-sat.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/finite-fun-ext.smt2 b/test/regress/regress0/ho/finite-fun-ext.smt2
index 005a2109a..63e25cb03 100644
--- a/test/regress/regress0/ho/finite-fun-ext.smt2
+++ b/test/regress/regress0/ho/finite-fun-ext.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 
 (declare-datatype Unit ((unit)))
 
diff --git a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
index 0fc536bd9..747bfd48e 100644
--- a/test/regress/regress0/ho/fta0144-alpha-eq.smt2
+++ b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort Nat$ 0)
 (declare-sort Complex$ 0)
 (declare-sort Real_set$ 0)
diff --git a/test/regress/regress0/ho/fta0210.smt2 b/test/regress/regress0/ho/fta0210.smt2
index 9f0a39f25..864bb9859 100644
--- a/test/regress/regress0/ho/fta0210.smt2
+++ b/test/regress/regress0/ho/fta0210.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort A$ 0)
 (declare-sort Nat$ 0)
 (declare-sort A_poly$ 0)
diff --git a/test/regress/regress0/ho/fun-subtyping.smt2 b/test/regress/regress0/ho/fun-subtyping.smt2
index 8eae3d073..e7cc01772 100644
--- a/test/regress/regress0/ho/fun-subtyping.smt2
+++ b/test/regress/regress0/ho/fun-subtyping.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-fun g (Int) Real)
 (declare-fun h (Int) Real)
 (assert (not (= g h)))
diff --git a/test/regress/regress0/ho/ho-exponential-model.smt2 b/test/regress/regress0/ho/ho-exponential-model.smt2
index 3f0011828..964a45f77 100644
--- a/test/regress/regress0/ho/ho-exponential-model.smt2
+++ b/test/regress/regress0/ho/ho-exponential-model.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status sat)
 (declare-fun f1 (Int Int Int Int) Int)
 (declare-fun f2 (Int Int Int) Int)
diff --git a/test/regress/regress0/ho/ho-match-fun-suffix.smt2 b/test/regress/regress0/ho/ho-match-fun-suffix.smt2
index 1e4ad243c..4418b156f 100644
--- a/test/regress/regress0/ho/ho-match-fun-suffix.smt2
+++ b/test/regress/regress0/ho/ho-match-fun-suffix.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-fun f (Int Int) Int)
 (declare-fun a () Int)
diff --git a/test/regress/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/regress0/ho/ho-matching-enum-2.smt2
index 9581e4c4f..e73afdce2 100644
--- a/test/regress/regress0/ho/ho-matching-enum-2.smt2
+++ b/test/regress/regress0/ho/ho-matching-enum-2.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/ho/ho-matching-enum.smt2 b/test/regress/regress0/ho/ho-matching-enum.smt2
index bd1d2837f..df3a920ec 100644
--- a/test/regress/regress0/ho/ho-matching-enum.smt2
+++ b/test/regress/regress0/ho/ho-matching-enum.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/ho/ho-matching-nested-app.smt2 b/test/regress/regress0/ho/ho-matching-nested-app.smt2
index d6de559e6..506cd55cf 100644
--- a/test/regress/regress0/ho/ho-matching-nested-app.smt2
+++ b/test/regress/regress0/ho/ho-matching-nested-app.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 
 (declare-sort U 0)
diff --git a/test/regress/regress0/ho/ho-std-fmf.smt2 b/test/regress/regress0/ho/ho-std-fmf.smt2
index 61d82d00c..1b23fdb6f 100644
--- a/test/regress/regress0/ho/ho-std-fmf.smt2
+++ b/test/regress/regress0/ho/ho-std-fmf.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --uf-ho --finite-model-find
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status sat)
 (declare-sort U 0)
 (declare-fun P (U U) Bool)
diff --git a/test/regress/regress0/ho/hoa0008.smt2 b/test/regress/regress0/ho/hoa0008.smt2
index f4833aadf..b43920c21 100644
--- a/test/regress/regress0/ho/hoa0008.smt2
+++ b/test/regress/regress0/ho/hoa0008.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort A$ 0)
 (declare-sort Com$ 0)
 (declare-sort Loc$ 0)
diff --git a/test/regress/regress0/ho/issue4990-care-graph.smt2 b/test/regress/regress0/ho/issue4990-care-graph.smt2
index 6c44a94a8..93c87d3c9 100644
--- a/test/regress/regress0/ho/issue4990-care-graph.smt2
+++ b/test/regress/regress0/ho/issue4990-care-graph.smt2
@@ -1,7 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic QF_AUFBVLIA)
-(set-option :uf-ho true)
+(set-logic HO_QF_AUFBVLIA)
 (declare-fun a () Int)
 (declare-fun b () Int)
 (declare-fun c (Int) Int)
diff --git a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
index e97b914a2..9091cf8bd 100644
--- a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
+++ b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2
@@ -1,7 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic QF_AUFBVLIA)
-(set-option :uf-ho true)
+(set-logic HO_QF_AUFBVLIA)
 (declare-fun a (Int) Int)
 (declare-fun b (Int) Int)
 (assert (distinct a b))
diff --git a/test/regress/regress0/ho/ite-apply-eq.smt2 b/test/regress/regress0/ho/ite-apply-eq.smt2
index 474f6887e..2e21d3081 100644
--- a/test/regress/regress0/ho/ite-apply-eq.smt2
+++ b/test/regress/regress0/ho/ite-apply-eq.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status sat)
 (declare-fun x () Int)
 (declare-fun f (Int) Int)
diff --git a/test/regress/regress0/ho/lambda-equality-non-canon.smt2 b/test/regress/regress0/ho/lambda-equality-non-canon.smt2
index 80f3db417..61753d90a 100644
--- a/test/regress/regress0/ho/lambda-equality-non-canon.smt2
+++ b/test/regress/regress0/ho/lambda-equality-non-canon.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status sat)
 (declare-fun f (Int) Int)
 
diff --git a/test/regress/regress0/ho/match-middle.smt2 b/test/regress/regress0/ho/match-middle.smt2
index 0485f9a6f..225faa1a5 100644
--- a/test/regress/regress0/ho/match-middle.smt2
+++ b/test/regress/regress0/ho/match-middle.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status unsat)
 (declare-fun f (Int Int Int) Int)
 (declare-fun h (Int Int Int) Int)
diff --git a/test/regress/regress0/ho/modulo-func-equality.smt2 b/test/regress/regress0/ho/modulo-func-equality.smt2
index 8e300ac72..984835be7 100644
--- a/test/regress/regress0/ho/modulo-func-equality.smt2
+++ b/test/regress/regress0/ho/modulo-func-equality.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (set-info :status unsat)
 (declare-fun P (Int) Bool)
 (declare-fun Q (Int) Bool)
diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2
index 722e970b6..fb5ac3ec6 100644
--- a/test/regress/regress0/ho/shadowing-defs.smt2
+++ b/test/regress/regress0/ho/shadowing-defs.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unknown
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort mu 0)
 
diff --git a/test/regress/regress0/ho/simple-matching-partial.smt2 b/test/regress/regress0/ho/simple-matching-partial.smt2
index 41b2a0bca..18c578367 100644
--- a/test/regress/regress0/ho/simple-matching-partial.smt2
+++ b/test/regress/regress0/ho/simple-matching-partial.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U U) U)
diff --git a/test/regress/regress0/ho/simple-matching.smt2 b/test/regress/regress0/ho/simple-matching.smt2
index 8e2315b2f..cbd70f072 100644
--- a/test/regress/regress0/ho/simple-matching.smt2
+++ b/test/regress/regress0/ho/simple-matching.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)
diff --git a/test/regress/regress0/ho/trans.smt2 b/test/regress/regress0/ho/trans.smt2
index 088abbab1..b33644db3 100644
--- a/test/regress/regress0/ho/trans.smt2
+++ b/test/regress/regress0/ho/trans.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic UF)
+(set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-fun f (U) U)
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
index 848ae0349..6a149cc71 100644
--- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -1,16 +1,16 @@
 ; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
 ; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
-; EXPECT-ERROR: 
+; EXPECT-ERROR:
 ; EXPECT-ERROR: (Op2 <O2> <F>)
 ; EXPECT-ERROR: ^
 ; EXPECT-ERROR: ")
 ; EXIT: 1
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-option :lang sygus2)
 ;(set-option :sygus-out status)
 (set-option :sygus-rec-fun true)
-(set-option :uf-ho true)
+
 
 (define-sort Time () Int)
 
@@ -47,19 +47,19 @@
   (and (<= 0 t tn)
        (match f (
          ((P i) (val t i))
-      
-         ((Op1 op g) 
+
+         ((Op1 op g)
            (match op (
-             (NOT (not (holds g t))) 
+             (NOT (not (holds g t)))
 
-             (Y (and (< 0 t) (holds g (- t 1))))    
+             (Y (and (< 0 t) (holds g (- t 1))))
 
              (G (and (holds g t) (or (= t tn) (holds f (+ t 1)))))
 
              (H (and (holds g t) (or (= t 0) (holds f (- t 1)))))
           )))
 
-         ((Op2 op f g)     
+         ((Op2 op f g)
            (match op (
              (AND (and (holds f t) (holds g t)))
 
@@ -88,6 +88,3 @@
 (constraint (holds (Op1 G (phi X0 X1)) 0))
 
 (check-synth)
-
-
-
diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy
index b08aa8929..2f59598ec 100644
--- a/test/regress/regress0/sygus/sygus-uf.sy
+++ b/test/regress/regress0/sygus/sygus-uf.sy
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 
 (declare-var uf (-> Int Int))
 
diff --git a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 b/test/regress/regress1/fmf/issue4225-univ-fun.smt2
index 9946a4567..af1f1e1a6 100644
--- a/test/regress/regress1/fmf/issue4225-univ-fun.smt2
+++ b/test/regress/regress1/fmf/issue4225-univ-fun.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --finite-model-find --uf-ho
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: unknown
-(set-logic ALL)
+(set-logic HO_ALL)
 ; this is not handled by fmf
 (assert (forall ((a (-> Int Int)) (b Int)) (not (= (a b) 0))))
 (check-sat)
diff --git a/test/regress/regress1/ho/NUM638^1.smt2 b/test/regress/regress1/ho/NUM638^1.smt2
index 59391ce8c..11683b1a7 100644
--- a/test/regress/regress1/ho/NUM638^1.smt2
+++ b/test/regress/regress1/ho/NUM638^1.smt2
@@ -1,8 +1,8 @@
-; COMMAND-LINE: --uf-ho --finite-model-find
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
 
 (set-option :incremental false)
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort nat 0)
 (declare-fun x () nat)
diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p
index e162a63a4..e07ad784f 100644
--- a/test/regress/regress1/ho/NUM925^1.p
+++ b/test/regress/regress1/ho/NUM925^1.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --ho-elim
+% COMMAND-LINE:  --ho-elim
 % EXPECT: % SZS status Theorem for NUM925^1
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress1/ho/SYO056^1.p b/test/regress/regress1/ho/SYO056^1.p
index a8a6bafca..deda234da 100644
--- a/test/regress/regress1/ho/SYO056^1.p
+++ b/test/regress/regress1/ho/SYO056^1.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --finite-model-find
+% COMMAND-LINE:  --finite-model-find
 % EXPECT: % SZS status CounterSatisfiable for SYO056^1
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress1/ho/bound_var_bug.p b/test/regress/regress1/ho/bound_var_bug.p
index 0dc946d6a..23bda7fb2 100644
--- a/test/regress/regress1/ho/bound_var_bug.p
+++ b/test/regress/regress1/ho/bound_var_bug.p
@@ -1,4 +1,3 @@
-% COMMAND-LINE: --uf-ho
 % EXPECT: % SZS status GaveUp for bound_var_bug
 
 % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/misc/leo --foatp e --atp e="$E_HOME"/eprover --atp epclextract="$E_HOME"/epclextract --proofoutput 1 --timeout 30 /Users/blanchette/hgs/afp_mining/tools/judgment_day_2017/data_afp/leo2-mepo/Call_Arity_SestoftGC_data/prob_308__3244432_1 ) ; }
diff --git a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p
index 6c35270fd..22c1d1dd1 100644
--- a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p
+++ b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --uf-ho --finite-model-find
+% COMMAND-LINE: --finite-model-find
 % EXPECT: % SZS status Satisfiable for bug_freeVar_BDD_General_data_270
 
 thf(ty_n_t__Nat__Onat, type,
diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
index 21405dfdb..7c9de4c49 100644
--- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
+++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --uf-ho --finite-model-find -q --decision=justification-old
+; COMMAND-LINE: --finite-model-find -q --decision=justification-old
 ; EXPECT: sat
 
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort qML_mu 0)
 (declare-sort qML_i 0)
diff --git a/test/regress/regress1/ho/fta0328.lfho.p b/test/regress/regress1/ho/fta0328.lfho.p
index c33b43ca5..f67c6db58 100644
--- a/test/regress/regress1/ho/fta0328.lfho.p
+++ b/test/regress/regress1/ho/fta0328.lfho.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --uf-ho --finite-model-find
+% COMMAND-LINE:  --finite-model-find
 % EXPECT: % SZS status CounterSatisfiable for fta0328.lfho
 
 % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/.isabelle/contrib/e-2.0-2/x86_64-darwin/eprover --auto-schedule --tstp-in --tstp-out --silent --cpu-limit=2 --proof-object=1 /Users/blanchette/hgs/matryoshka/papers/2019-TACAS-ehoh/eval/judgment_day/judgment_day_lifting_32/fta/prob_804__4064966_1 ) ; }
diff --git a/test/regress/regress1/ho/hoa0102.smt2 b/test/regress/regress1/ho/hoa0102.smt2
index 6be063783..c5840e6a9 100644
--- a/test/regress/regress1/ho/hoa0102.smt2
+++ b/test/regress/regress1/ho/hoa0102.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --uf-ho --full-saturate-quant
+; COMMAND-LINE:  --full-saturate-quant
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort Com$ 0)
 (declare-sort Glb$ 0)
diff --git a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2
index d536e51a1..d15095123 100644
--- a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2
+++ b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE:  --uf-ho --ho-elim
+; COMMAND-LINE:  --ho-elim
 ; EXPECT: unsat
 
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort num 0)
 (declare-fun agent_THFTYPE_i () $$unsorted)
diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2
index 9852150d9..a13aa2bae 100644
--- a/test/regress/regress1/ho/issue4065-no-rep.smt2
+++ b/test/regress/regress1/ho/issue4065-no-rep.smt2
@@ -1,7 +1,6 @@
-(set-logic AUFBV)
+(set-logic HO_AUFBV)
 (set-info :status unsat)
 (set-option :fmf-bound-int true)
-(set-option :uf-ho true)
 (declare-fun _substvar_20_ () Bool)
 (declare-sort S4 0)
 (assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true)))
diff --git a/test/regress/regress1/ho/issue4092-sinf.smt2 b/test/regress/regress1/ho/issue4092-sinf.smt2
index d3066c282..83a3e08b9 100644
--- a/test/regress/regress1/ho/issue4092-sinf.smt2
+++ b/test/regress/regress1/ho/issue4092-sinf.smt2
@@ -1,10 +1,9 @@
-; COMMAND-LINE: --uf-ho --sort-inference
+; COMMAND-LINE: --sort-inference
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-option :sort-inference true)
-(set-option :uf-ho true)
 (set-info :status sat)
-(declare-fun a ( Int ) Int) 
-(declare-fun b ( Int ) Int)  
-(assert (and (distinct 0 (b 5)) (distinct a b ))) 
-(check-sat) 
+(declare-fun a ( Int ) Int)
+(declare-fun b ( Int ) Int)
+(assert (and (distinct 0 (b 5)) (distinct a b )))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue4134-sinf.smt2 b/test/regress/regress1/ho/issue4134-sinf.smt2
index 60a754aad..0003bc91e 100644
--- a/test/regress/regress1/ho/issue4134-sinf.smt2
+++ b/test/regress/regress1/ho/issue4134-sinf.smt2
@@ -1,7 +1,6 @@
-; COMMAND-LINE: --uf-ho --sort-inference
+; COMMAND-LINE: --sort-inference
 ; EXPECT: sat
-(set-logic ALL)
-(set-option :uf-ho true)
+(set-logic HO_ALL)
 (set-option :sort-inference true)
 (set-info :status sat)
 (declare-fun a () Int)
diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
index 313ff68a1..6a8feba5c 100644
--- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models --ho-elim
+; COMMAND-LINE: --no-check-unsat-cores --no-produce-models --ho-elim
 ; EXPECT: unsat
 
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 (declare-sort mu 0)
 (declare-fun meq_ind (mu mu $$unsorted) Bool)
diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
index 6743e00d4..3f02e56fd 100644
--- a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
@@ -1,8 +1,7 @@
-; COMMAND-LINE:  --uf-ho --finite-model-find --no-check-models
+; COMMAND-LINE:  --finite-model-find --no-check-models
 ; EXPECT: sat
 
-
-(set-logic ALL)
+(set-logic HO_ALL)
 (declare-sort $$unsorted 0)
 
 (declare-fun mvalid ((-> $$unsorted Bool)) Bool)
diff --git a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p
index baabd675a..4068cc42e 100644
--- a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p
+++ b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --finite-model-find
+% COMMAND-LINE:   --finite-model-find
 % EXPECT: % SZS status GaveUp for soundness_fmf_SYO362^5-delta
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress1/ho/store-ax-min.p b/test/regress/regress1/ho/store-ax-min.p
index d67eb8dad..d000a17d0 100644
--- a/test/regress/regress1/ho/store-ax-min.p
+++ b/test/regress/regress1/ho/store-ax-min.p
@@ -1,5 +1,5 @@
-% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim-store-ax
-% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim
+% COMMAND-LINE: --full-saturate-quant --ho-elim-store-ax
+% COMMAND-LINE: --full-saturate-quant --ho-elim
 % EXPECT: % SZS status Theorem for store-ax-min
 
 thf(a, type, (a: $i)).
diff --git a/test/regress/regress1/quantifiers/issue3724-quant.smt2 b/test/regress/regress1/quantifiers/issue3724-quant.smt2
index 6dd874fbf..32e82a8b5 100644
--- a/test/regress/regress1/quantifiers/issue3724-quant.smt2
+++ b/test/regress/regress1/quantifiers/issue3724-quant.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --uf-ho
+; COMMAND-LINE:
 ; EXPECT: unknown
-(set-logic ALL)
+(set-logic HO_ALL)
 (assert
 (forall ((BOUND_VARIABLE_313 Bool) (BOUND_VARIABLE_314 (-> Int Bool)) (BOUND_VARIABLE_315 (-> Int Int)) (BOUND_VARIABLE_316 Int) (BOUND_VARIABLE_317 (-> Int Bool)) (BOUND_VARIABLE_318 Int)) (! (not (and (not (and (= (ite (and (not (= BOUND_VARIABLE_318 0)) (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))) (ite (BOUND_VARIABLE_317 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9))))))) BOUND_VARIABLE_316 0) 0) 0) (not (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))))) true)) :pattern (true)))
 )
diff --git a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
index 03bbd9469..9cb5cdac3 100644
--- a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
+++ b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
@@ -1,9 +1,9 @@
-(set-logic ALL)
+; COMMAND-LINE:
+(set-logic HO_ALL)
 (set-option :ag-miniscope-quant true)
 (set-option :conjecture-gen true)
 (set-option :int-wf-ind true)
 (set-option :sygus-inference true)
-(set-option :uf-ho true)
 (set-info :status unsat)
 (declare-fun a () Real)
 (declare-fun b () Real)
diff --git a/test/regress/regress1/sygus/eval-uc.sy b/test/regress/regress1/sygus/eval-uc.sy
index e2bf9d144..e007eec51 100644
--- a/test/regress/regress1/sygus/eval-uc.sy
+++ b/test/regress/regress1/sygus/eval-uc.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
-(set-logic ALL)
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic HO_ALL)
 (declare-sort S 0)
 (declare-var f Bool)
 (declare-var u (-> S Bool))
@@ -9,7 +9,7 @@
 (define-fun init ((f Bool) (u (-> S Bool))) Bool (and f (forall ((x S)) (not (u x)))))
 (define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and (not new_f) (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x)))))))
 ;(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and new_f (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x)))))))
-(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not 
+(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not
 (u x)) (not f))))))
 (define-fun inv ((f Bool) (u (-> S Bool))) Bool (forall ((x S)) (inv_matrix f u x)))
 (constraint (=> (and (inv f u) (trans f u new_f new_u)) (inv new_f new_u)))
diff --git a/test/regress/regress1/sygus/ho-sygus.sy b/test/regress/regress1/sygus/ho-sygus.sy
index 893c2034e..d46d8ecde 100644
--- a/test/regress/regress1/sygus/ho-sygus.sy
+++ b/test/regress/regress1/sygus/ho-sygus.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
-(set-logic ALL)
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic HO_ALL)
 (synth-fun f ((y (-> Int Int)) (z Int)) Int)
 (declare-var z (-> Int Int))
 (constraint (= (f z 0) (z 1)))
diff --git a/test/regress/regress1/sygus/issue3507.smt2 b/test/regress/regress1/sygus/issue3507.smt2
index c8700f37b..1bbcb2984 100644
--- a/test/regress/regress1/sygus/issue3507.smt2
+++ b/test/regress/regress1/sygus/issue3507.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --uf-ho --quiet
-(set-logic ALL)
+; COMMAND-LINE: --sygus-inference --quiet
+(set-logic HO_ALL)
 (declare-fun f (Int) Bool)
 (declare-fun g (Int) Bool)
 (assert (and (distinct f g) (g 0)))
diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
index bc882fc8a..711afb2d8 100644
--- a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
+++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho
-(set-logic ALL)
+; COMMAND-LINE: --sygus-inference --fmf-bound
+(set-logic HO_ALL)
 (declare-fun a () (_ BitVec 1))
 (assert (bvsgt (bvsmod a a) #b0))
 (check-sat)
diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy
index 2e10a0c71..cb1ae2721 100644
--- a/test/regress/regress1/sygus/list_recursor.sy
+++ b/test/regress/regress1/sygus/list_recursor.sy
@@ -1,23 +1,23 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
 
-(set-logic ALL)
+(set-logic HO_ALL)
 
 (declare-datatype List ((cons (head Int) (tail List)) (nil)))
 
 (define-fun-rec List_rec ((x Int) (y (-> Int List Int Int)) (l List)) Int
-  (ite ((_ is nil) l) x 
+  (ite ((_ is nil) l) x
                       (y (head l) (tail l) (List_rec x y (tail l)))))
 
 (synth-fun f () Int
   ((I Int))
   ((I Int  (0 1 (+ I I)))))
-   
+
 (synth-fun g ((x Int) (y List) (z Int)) Int
   ((I Int) (L List))
   ((I Int  (x z (+ I I) (head L) 0 1))
    (L List (y (tail y)))))
-   
+
 
 (constraint (= (List_rec f g (cons 0 (cons 1 nil))) 2))
 (constraint (= (List_rec f g (cons 0 (cons 0 nil))) 2))
diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy
index 7e1cd80b3..c74ce79b7 100644
--- a/test/regress/regress1/sygus/sygus-uf-ex.sy
+++ b/test/regress/regress1/sygus/sygus-uf-ex.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
-(set-logic ALL)
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic HO_ALL)
 
 (declare-var uf (-> Int Int))
 
diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/sygus/uf-abduct.smt2
index 690e57290..bfcfe39fd 100644
--- a/test/regress/regress1/sygus/uf-abduct.smt2
+++ b/test/regress/regress1/sygus/uf-abduct.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --produce-abducts --uf-ho
+; COMMAND-LINE: --produce-abducts
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
-(set-logic UFLIA)
+(set-logic HO_UFLIA)
 (declare-fun f (Int) Int)
 (declare-fun a () Int)
 (assert (and (<= 0 a) (< a 4)))
diff --git a/test/regress/regress2/ho/auth0068.smt2 b/test/regress/regress2/ho/auth0068.smt2
index eb0bb5d36..fc788a15c 100644
--- a/test/regress/regress2/ho/auth0068.smt2
+++ b/test/regress/regress2/ho/auth0068.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort Msg$ 0)
 (declare-sort Nat$ 0)
diff --git a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p
index a62a2080a..bf58b95d8 100644
--- a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p
+++ b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --full-saturate-quant --ho-elim
+% COMMAND-LINE:  --full-saturate-quant --ho-elim
 % EXPECT: % SZS status Theorem for bug_instfalse_SEU882^5
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress2/ho/fta0409.smt2 b/test/regress/regress2/ho/fta0409.smt2
index 51ac5f2da..5516c804a 100644
--- a/test/regress/regress2/ho/fta0409.smt2
+++ b/test/regress/regress2/ho/fta0409.smt2
@@ -1,6 +1,5 @@
-; COMMAND-LINE: --uf-ho
 ; EXPECT: unsat
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort Nat$ 0)
 (declare-sort Complex$ 0)
diff --git a/test/regress/regress2/ho/involved_parsing_ALG248^3.p b/test/regress/regress2/ho/involved_parsing_ALG248^3.p
index d0577dd1f..47a89143d 100644
--- a/test/regress/regress2/ho/involved_parsing_ALG248^3.p
+++ b/test/regress/regress2/ho/involved_parsing_ALG248^3.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE:  --uf-ho --ho-elim
+% COMMAND-LINE:  --ho-elim
 % EXPECT: % SZS status Theorem for involved_parsing_ALG248^3
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p
index 37c7a02e8..5f87519d1 100644
--- a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p
+++ b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim
+% COMMAND-LINE: --full-saturate-quant --ho-elim
 % EXPECT: % SZS status Theorem for partial_app_interpreted_SWW474^2
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress3/ho/SYO362^5.p b/test/regress/regress3/ho/SYO362^5.p
index b9537fd0e..41fe3d541 100644
--- a/test/regress/regress3/ho/SYO362^5.p
+++ b/test/regress/regress3/ho/SYO362^5.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim --decision=justification-old
+% COMMAND-LINE: --full-saturate-quant --ho-elim --decision=justification-old
 % EXPECT: % SZS status Theorem for SYO362^5
 
 thf(cK,type,(
diff --git a/test/regress/regress3/issue4170.smt2 b/test/regress/regress3/issue4170.smt2
index 0dee146c0..25e0c7f8d 100644
--- a/test/regress/regress3/issue4170.smt2
+++ b/test/regress/regress3/issue4170.smt2
@@ -1,6 +1,5 @@
-(set-logic ALL)
+(set-logic HO_ALL)
 (set-option :sygus-inference true)
-(set-option :uf-ho true)
 (set-option :sygus-ext-rew false)
 (set-info :status sat)
 (declare-fun a (Int) Int)