From 6b054414bad62166603865c8af007fee897b536d Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 4 Aug 2021 17:08:06 -0300 Subject: [PATCH] Improve error messages for UF catching higher-order (#6982) Addresses #6979. --- src/theory/uf/theory_uf.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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& 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& 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()); } } -- 2.30.2