From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 4 Aug 2021 20:08:06 +0000 (-0300)
Subject: Improve error messages for UF catching higher-order (#6982)
X-Git-Tag: cvc5-1.0.0~1405
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b054414bad62166603865c8af007fee897b536d;p=cvc5.git

Improve error messages for UF catching higher-order (#6982)

Addresses #6979.
---

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f1adde143..4224ec854 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -217,7 +217,8 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
   {
     if( !options::ufHo() ){
       std::stringstream ss;
-      ss << "Partial function applications are not supported in default mode, try --uf-ho.";
+      ss << "Partial function applications are only supported with "
+            "higher-order logic. Try adding the logic prefix HO_.";
       throw LogicException(ss.str());
     }
     Node ret = d_ho->ppRewrite(node);
@@ -236,7 +237,9 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
     {
       std::stringstream ss;
       ss << "UF received an application whose operator has higher-order type "
-         << node << ", which is not supported by default, try --uf-ho";
+         << node
+         << ", which is only supported with higher-order logic. Try adding the "
+            "logic prefix HO_.";
       throw LogicException(ss.str());
     }
   }