3 files changed, 15 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d591c29de..95f4b1a67 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2630,8 +2630,8 @@ CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
 TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
 
-HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->';
-HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda';
+HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
+HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';
 
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 91260d1db..9ca2194f4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -315,6 +315,12 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
   return d_logic.isTheoryEnabled(theory);
 }
 
+bool Smt2::isHoEnabled() const
+{
+  return getLogic().isHigherOrder()
+         && d_solver->getExprManager()->getOptions().getUfHo();
+}
+
 bool Smt2::logicIsSet() {
   return d_logicSet;
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 35d088601..af1e36795 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -98,6 +98,13 @@ class Smt2 : public Parser
 
   bool isTheoryEnabled(theory::TheoryId theory) const;
 
+  /**
+   * Checks if higher-order support is enabled.
+   *
+   * @return true if higher-order support is enabled, false otherwise
+   */
+  bool isHoEnabled() const;
+
   bool logicIsSet() override;
 
   /**