diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-08-04 17:08:06 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-04 20:08:06 +0000 |
commit | 6b054414bad62166603865c8af007fee897b536d (patch) | |
tree | f7014201402fe03c71fd56a357ba69acf8b24072 /src | |
parent | ad59051f029507a6c49411b71b9c67467a53660d (diff) |
Improve error messages for UF catching higher-order (#6982)
Addresses #6979.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 7 |
1 files 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<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()); } } |