From 8f14d8b4eeaf5b2d1b7bb30173ca85197b7166be Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 21:51:42 -0600
Subject: [PATCH] Improve error for higher-order logic (#8207)

Makes the error more informative when a higher-order function variable is encountered.
Fixes cvc5/cvc5-projects#450.
---
 src/theory/uf/theory_uf.cpp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9058a57f3..e22698bc0 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -221,7 +221,15 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
     if (!isHol)
     {
       std::stringstream ss;
-      ss << "Partial function applications are only supported with "
+      if (k == kind::HO_APPLY)
+      {
+        ss << "Partial function applications";
+      }
+      else
+      {
+        ss << "Function variables";
+      }
+      ss << " are only supported with "
             "higher-order logic. Try adding the logic prefix HO_.";
       throw LogicException(ss.str());
     }
-- 
2.30.2