[parser] [hol] Fix parser check for allowing functions when HOL is enabled (#6790)

Fixes #6526

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 282b72974c4230352875ad5f6e3d999f559e3889..8c011aecefe8e99e9ec6487c04fcad2b0d95992b 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -764,12 +764,13 @@ void Smt2::checkLogicAllowsFreeSorts()
 
 void Smt2::checkLogicAllowsFunctions()
 {
-  if (!d_logic.isTheoryEnabled(theory::THEORY_UF))
+  if (!d_logic.isTheoryEnabled(theory::THEORY_UF) && !isHoEnabled())
   {
     parseError(
         "Functions (of non-zero arity) cannot "
         "be declared in logic "
-        + d_logic.getLogicString() + ". Try adding the prefix HO_.");
+        + d_logic.getLogicString()
+        + ". Try including UF or adding the prefix HO_.");
   }
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6706ed4f68688a04c1c6edb41c315d0f07077dbd..53e050191a8b76672866c3a5543307034e574759 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -632,6 +632,7 @@ set(regress_0_tests
   regress0/ho/issue4477.smt2
   regress0/ho/issue4990-care-graph.smt2
   regress0/ho/issue5233-part1-usort-owner.smt2
+  regress0/ho/issue6526.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/match-middle.smt2

diff --git a/test/regress/regress0/ho/issue6526.smt2 b/test/regress/regress0/ho/issue6526.smt2
new file mode 100644 (file)
index 0000000..07dfbc0
--- /dev/null
+++ b/test/regress/regress0/ho/issue6526.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE:
+; EXPECT: sat
+(set-logic HO_NIA)
+(declare-fun x (Int) Bool)
+(check-sat)
\ No newline at end of file