diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 9110b9660..c1a9df887 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -305,8 +305,11 @@ command [std::unique_ptr<CVC4::Command>* cmd] t = PARSER_STATE->mkFlatFunctionType(sorts, t); } if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot " - "be declared in logic "); + PARSER_STATE->parseError( + "Functions (of non-zero arity) cannot " + "be declared in logic " + + PARSER_STATE->getLogic().getLogicString() + + " unless option --uf-ho is used."); } // we allow overloading for function declarations if (PARSER_STATE->sygus_v1()) @@ -1283,8 +1286,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { Type t; if(sorts.size() > 1) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) " - "cannot be declared in logic "); + PARSER_STATE->parseError( + "Functions (of non-zero arity) cannot " + "be declared in logic " + + PARSER_STATE->getLogic().getLogicString() + + " unless option --uf-ho is used"); } // must flatten Type range = sorts.back(); @@ -1310,8 +1316,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] { Type t = EXPR_MANAGER->booleanType(); if(sorts.size() > 0) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseErrorLogic("Predicates (of non-zero arity) " - "cannot be declared in logic "); + PARSER_STATE->parseError( + "Functions (of non-zero arity) cannot " + "be declared in logic " + + PARSER_STATE->getLogic().getLogicString() + + " unless option --uf-ho is used"); } t = EXPR_MANAGER->mkFunctionType(sorts, t); } |