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

80 files changed, 229 insertions, 222 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index f6592a931..d96e94d43 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -109,8 +109,8 @@ api::Term Parser::getExpressionForNameAndType(const std::string& name,
   if(expr.isNull()) {
     // the variable is overloaded, try with type if the type exists
     if(!t.isNull()) {
-      // if we decide later to support annotations for function types, this will update to 
-      // separate t into ( argument types, return type )
+      // if we decide later to support annotations for function types, this will
+      // update to separate t into ( argument types, return type )
       expr = getOverloadedConstantForType(name, t);
       if(expr.isNull()) {
         parseError("Cannot get overloaded constant for type ascription.");
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8add1c698..4b04c77b7 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -303,9 +303,10 @@ public:
   virtual api::Term getExpressionForName(const std::string& name);
 
   /**
-   * Returns the expression that name should be interpreted as, based on the current binding.
+   * Returns the expression that name should be interpreted as, based on the
+   * current binding.
    *
-   * This is the same as above but where the name has been type cast to t. 
+   * This is the same as above but where the name has been type cast to t.
    */
   virtual api::Term getExpressionForNameAndType(const std::string& name,
                                                 api::Sort t);
@@ -331,9 +332,9 @@ public:
    * This is a generalization of ExprManager::operatorToKind that also
    * handles variables whose types are "function-like", i.e. where
    * checkFunctionLike(fun) returns true.
-   * 
+   *
    * For examples of the latter, this function returns
-   *   APPLY_UF if fun has function type, 
+   *   APPLY_UF if fun has function type,
    *   APPLY_CONSTRUCTOR if fun has constructor type.
    */
   api::Kind getKindForFunction(api::Term fun);
@@ -379,7 +380,7 @@ public:
 
   /**
    * Checks whether the given expression is function-like, i.e.
-   * it expects arguments. This is checked by looking at the type 
+   * it expects arguments. This is checked by looking at the type
    * of fun. Examples of function types are function, constructor,
    * selector, tester.
    * @param fun the expression to check
@@ -443,11 +444,12 @@ public:
   std::vector<api::Term> bindBoundVars(const std::vector<std::string> names,
                                        const api::Sort& type);
 
-  /** Create a new variable definition (e.g., from a let binding). 
+  /** Create a new variable definition (e.g., from a let binding).
    * levelZero is set if the binding must be done at level 0.
    * If a symbol with name already exists,
    *  then if doOverload is true, we create overloaded operators.
-   *  else if doOverload is false, the existing expression is shadowed by the new expression.
+   *  else if doOverload is false, the existing expression is shadowed by the
+   * new expression.
    */
   void defineVar(const std::string& name,
                  const api::Term& val,
@@ -648,9 +650,10 @@ public:
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
-  /** Is fun a function (or function-like thing)? 
-  * Currently this means its type is either a function, constructor, tester, or selector.
-  */
+  /** Is fun a function (or function-like thing)?
+   * Currently this means its type is either a function, constructor, tester, or
+   * selector.
+   */
   bool isFunctionLike(api::Term fun);
 
   /** Is the symbol bound to a predicate? */
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index e4f46326f..1f25e00dd 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -143,7 +143,8 @@ ParserBuilder& ParserBuilder::withIncludeFile(bool flag) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) {
+ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic)
+{
   d_logicIsForced = true;
   d_forcedLogic = logic;
   return *this;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 5961de587..56aebdcf7 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -315,10 +315,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
   return d_logic.isTheoryEnabled(theory);
 }
 
-bool Smt2::isHoEnabled() const
-{
-  return getLogic().isHigherOrder() && options::getUfHo(d_solver->getOptions());
-}
+bool Smt2::isHoEnabled() const { return d_logic.isHigherOrder(); }
 
 bool Smt2::logicIsSet() {
   return d_logicSet;
@@ -505,8 +502,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
   d_logicSet = true;
   d_logic = name;
 
-  // if sygus is enabled, we must enable UF, datatypes, integer arithmetic and
-  // higher-order
+  // if sygus is enabled, we must enable UF, datatypes, and integer arithmetic
   if(sygus()) {
     if (!d_logic.isQuantified())
     {
@@ -772,7 +768,7 @@ void Smt2::checkLogicAllowsFunctions()
     parseError(
         "Functions (of non-zero arity) cannot "
         "be declared in logic "
-        + d_logic.getLogicString() + " unless option --uf-ho is used");
+        + d_logic.getLogicString() + ". Try adding the prefix HO_.");
   }
 }
 
@@ -1012,8 +1008,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       }
     }
   }
-  // Second phase: apply the arguments to the parse op
-  const Options& opts = d_solver->getOptions();
   // handle special cases
   if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull())
   {
@@ -1102,17 +1096,17 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   }
   else if (isBuiltinOperator)
   {
-    if (!options::getUfHo(opts)
-        && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!isHoEnabled() && (kind == api::EQUAL || kind == api::DISTINCT))
     {
-      // need --uf-ho if these operators are applied over function args
+      // need hol if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
            ++i)
       {
         if ((*i).getSort().isFunction())
         {
           parseError(
-              "Cannot apply equalty to functions unless --uf-ho is set.");
+              "Cannot apply equalty to functions unless logic is prefixed by "
+              "HO_.");
         }
       }
     }
@@ -1155,9 +1149,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!options::getUfHo(opts))
+        if (!isHoEnabled())
         {
-          parseError("Cannot partially apply functions unless --uf-ho is set.");
+          parseError(
+              "Cannot partially apply functions unless logic is prefixed by "
+              "HO_.");
         }
         Debug("parser") << "Partial application of " << args[0];
         Debug("parser") << " : #argTypes = " << arity;
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 5f078cab7..c96fbf07d 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -194,7 +194,11 @@ parseCommand returns [cvc5::Command* cmd = NULL]
         cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
       }
     ) RPAREN_TOK DOT_TOK
-  | THF_TOK LPAREN_TOK nameN[name] COMMA_TOK
+  | THF_TOK
+    {
+      PARSER_STATE->setHol();
+    }
+    LPAREN_TOK nameN[name] COMMA_TOK
     // Supported THF formulas: either a logic formula or a typing atom (i.e. we
     // ignore subtyping and logic sequents). Also, only TH0
     ( TYPE_TOK COMMA_TOK thfAtomTyping[cmd]
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 764e83361..91fcc7a12 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -25,6 +25,7 @@
 #include "options/options_public.h"
 #include "parser/parser.h"
 #include "smt/command.h"
+#include "theory/logic_info.h"
 
 // ANTLR defines these, which is really bad!
 #undef true
@@ -37,7 +38,10 @@ Tptp::Tptp(api::Solver* solver,
            SymbolManager* sm,
            bool strictMode,
            bool parseOnly)
-    : Parser(solver, sm, strictMode, parseOnly), d_cnf(false), d_fof(false)
+    : Parser(solver, sm, strictMode, parseOnly),
+      d_cnf(false),
+      d_fof(false),
+      d_hol(false)
 {
   addTheory(Tptp::THEORY_CORE);
 
@@ -312,21 +316,18 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     isBuiltinKind = true;
   }
   Assert(kind != api::NULL_EXPR);
-  const Options& opts = d_solver->getOptions();
   // Second phase: apply parse op to the arguments
   if (isBuiltinKind)
   {
-    if (!options::getUfHo(opts)
-        && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!hol() && (kind == api::EQUAL || kind == api::DISTINCT))
     {
-      // need --uf-ho if these operators are applied over function args
+      // need hol if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
            ++i)
       {
         if ((*i).getSort().isFunction())
         {
-          parseError(
-              "Cannot apply equalty to functions unless --uf-ho is set.");
+          parseError("Cannot apply equalty to functions unless THF.");
         }
       }
     }
@@ -364,9 +365,9 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!options::getUfHo(opts))
+        if (!hol())
         {
-          parseError("Cannot partially apply functions unless --uf-ho is set.");
+          parseError("Cannot partially apply functions unless THF.");
         }
         Debug("parser") << "Partial application of " << args[0];
         Debug("parser") << " : #argTypes = " << arity;
@@ -438,6 +439,17 @@ api::Term Tptp::mkDecimal(
   return d_solver->mkReal(ss.str());
 }
 
+bool Tptp::hol() const { return d_hol; }
+void Tptp::setHol()
+{
+  if (d_hol)
+  {
+    return;
+  }
+  d_hol = true;
+  d_solver->setLogic("HO_UF");
+}
+
 void Tptp::forceLogic(const std::string& logic)
 {
   Parser::forceLogic(logic);
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 964c0bdfb..258394486 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -47,6 +47,9 @@ class Tptp : public Parser {
   bool fof() const { return d_fof; }
   void setFof(bool fof) { d_fof = fof; }
 
+  bool hol() const;
+  void setHol();
+
   void forceLogic(const std::string& logic) override;
 
   void addFreeVar(api::Term var);
@@ -209,6 +212,7 @@ class Tptp : public Parser {
 
   bool d_cnf; // in a cnf formula
   bool d_fof; // in an fof formula
+  bool d_hol;  // in a thf formula
 };/* class Tptp */
 
 
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 67c5c5647..cd05b84c4 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -271,11 +271,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // Set default options associated with strings-exp. We also set these options
   // if we are using eager string preprocessing, which may introduce quantified
   // formulas at preprocess time.
+  //
+  // We don't want to set this option when we are in logics that contain ALL.
   if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS))
   {
     // If the user explicitly set a logic that includes strings, but is not
     // the generic "ALL" logic, then enable stringsExp.
     opts.strings.stringExp = true;
+    Trace("smt") << "Turning stringExp on since logic does not have everything "
+                    "and string theory is enabled\n";
   }
   if (options::stringExp() || !options::stringLazyPreproc())
   {
@@ -753,7 +757,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // If in arrays, set the UF handler to arrays
-  if (logic.isTheoryEnabled(THEORY_ARRAYS) && !options::ufHo()
+  if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder()
       && !options::finiteModelFind()
       && (!logic.isQuantified()
           || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
@@ -890,7 +894,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     options::DecisionMode decMode =
         // anything that uses sygus uses internal
         usesSygus ? options::DecisionMode::INTERNAL :
-                  // ALL
+                  // ALL  or its supersets
             logic.hasEverything()
                 ? options::DecisionMode::JUSTIFICATION
                 : (  // QF_BV
@@ -922,7 +926,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                           : options::DecisionMode::INTERNAL);
 
     bool stoponly =
-        // ALL
+        // ALL or its supersets
         logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
             ? false
             : (  // QF_AUFLIA
@@ -986,8 +990,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE;
     }
   }
-  if (options::ufHo())
+  if (logic.isHigherOrder())
   {
+    opts.uf.ufHo = true;
     // if higher-order, then current variants of model-based instantiation
     // cannot be used
     if (options::mbqiMode() != options::MbqiMode::NONE)
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index ecebd27c9..05f8c7a9f 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -39,7 +39,7 @@ LogicInfo::LogicInfo()
       d_linear(false),
       d_differenceLogic(false),
       d_cardinalityConstraints(false),
-      d_higherOrder(true),
+      d_higherOrder(false),
       d_locked(false)
 {
   for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
@@ -117,13 +117,25 @@ bool LogicInfo::isHigherOrder() const
   return d_higherOrder;
 }
 
-/** Is this the all-inclusive logic? */
-bool LogicInfo::hasEverything() const {
-  PrettyCheckArgument(d_locked, *this,
+bool LogicInfo::hasEverything() const
+{
+  PrettyCheckArgument(d_locked,
+                      *this,
                       "This LogicInfo isn't locked yet, and cannot be queried");
-  LogicInfo everything;
-  everything.lock();
-  return *this == everything;
+  // A logic has everything if all theories are enabled as well as quantifiers
+  bool doesNotHaveEverything = !isQuantified();
+  for (TheoryId id = THEORY_FIRST; !doesNotHaveEverything && id < THEORY_LAST;
+       ++id)
+  {
+    // if not configured with symfpu, we allow THEORY_FP to be disabled and
+    // still *this to contain the ALL logic
+    if (!this->d_theories[id]
+        && (id != THEORY_FP || Configuration::isBuiltWithSymFPU()))
+    {
+      doesNotHaveEverything = true;
+    }
+  }
+  return !doesNotHaveEverything;
 }
 
 /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
@@ -275,17 +287,22 @@ std::string LogicInfo::getLogicString() const {
     LogicInfo qf_all_supported;
     qf_all_supported.disableQuantifiers();
     qf_all_supported.lock();
-    if(hasEverything()) {
-      d_logicString = "ALL";
-    } else if(*this == qf_all_supported) {
-      d_logicString = "QF_ALL";
-    } else {
+    stringstream ss;
+    if (isHigherOrder())
+    {
+      ss << "HO_";
+    }
+    if (!isQuantified())
+    {
+      ss << "QF_";
+    }
+    if (*this == qf_all_supported || hasEverything())
+    {
+      ss << "ALL";
+    }
+    else
+    {
       size_t seen = 0; // make sure we support all the active theories
-
-      stringstream ss;
-      if(!isQuantified()) {
-        ss << "QF_";
-      }
       if (d_theories[THEORY_SEP])
       {
         ss << "SEP_";
@@ -309,7 +326,7 @@ std::string LogicInfo::getLogicString() const {
       if(d_theories[THEORY_FP]) {
         ss << "FP";
         ++seen;
-      } 
+      }
       if(d_theories[THEORY_DATATYPES]) {
         ss << "DT";
         ++seen;
@@ -350,9 +367,8 @@ std::string LogicInfo::getLogicString() const {
       if(seen == 0) {
         ss << "SAT";
       }
-
-      d_logicString = ss.str();
     }
+    d_logicString = ss.str();
   }
   return d_logicString;
 }
@@ -374,6 +390,11 @@ void LogicInfo::setLogicString(std::string logicString)
   enableTheory(THEORY_BOOL);
 
   const char* p = logicString.c_str();
+  if (!strncmp(p, "HO_", 3))
+  {
+    enableHigherOrder();
+    p += 3;
+  }
   if(*p == '\0') {
     // propositional logic only; we're done.
   } else if(!strcmp(p, "QF_SAT")) {
@@ -384,14 +405,14 @@ void LogicInfo::setLogicString(std::string logicString)
     enableQuantifiers();
     p += 3;
   } else if(!strcmp(p, "QF_ALL")) {
-    // the "all theories included" logic, no quantifiers
-    enableEverything();
+    // the "all theories included" logic, no quantifiers.
+    enableEverything(d_higherOrder);
     disableQuantifiers();
     arithNonLinear();
     p += 6;
   } else if(!strcmp(p, "ALL")) {
-    // the "all theories included" logic, with quantifiers
-    enableEverything();
+    // the "all theories included" logic, with quantifiers.
+    enableEverything(d_higherOrder);
     enableQuantifiers();
     arithNonLinear();
     p += 3;
@@ -399,7 +420,7 @@ void LogicInfo::setLogicString(std::string logicString)
   else if (!strcmp(p, "HORN"))
   {
     // the HORN logic
-    enableEverything();
+    enableEverything(d_higherOrder);
     enableQuantifiers();
     arithNonLinear();
     p += 4;
@@ -541,9 +562,11 @@ void LogicInfo::setLogicString(std::string logicString)
   d_logicString = logicString;
 }
 
-void LogicInfo::enableEverything() {
+void LogicInfo::enableEverything(bool enableHigherOrder)
+{
   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
   *this = LogicInfo();
+  this->d_higherOrder = enableHigherOrder;
 }
 
 void LogicInfo::disableEverything() {
@@ -584,7 +607,6 @@ void LogicInfo::enableSygus()
   enableTheory(THEORY_UF);
   enableTheory(THEORY_DATATYPES);
   enableIntegers();
-  enableHigherOrder();
 }
 
 void LogicInfo::enableSeparationLogic()
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index 107093a5c..c6aa71ad0 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -120,7 +120,11 @@ public:
   /** Is this a quantified logic? */
   bool isQuantified() const;
 
-  /** Is this the all-inclusive logic? */
+  /** Is this a logic that includes the all-inclusive logic?
+   *
+   * @return Yields true if the logic corresponds to "ALL" or its super
+   * set including , such as "HO_ALL".
+   */
   bool hasEverything() const;
 
   /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
@@ -168,8 +172,11 @@ public:
   /**
    * Enable all functionality.  All theories, plus quantifiers, will be
    * enabled.
+   *
+   * @param enableHigherOrder Whether HOL should be enable together with the
+   * above.
    */
-  void enableEverything();
+  void enableEverything(bool enableHigherOrder = false);
 
   /**
    * Disable all functionality.  The result will be a LogicInfo with
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)