From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 24 Mar 2022 16:57:53 +0000 (-0500)
Subject: Fix a couple of parse error messages for sygus (#8381)
X-Git-Tag: cvc5-1.0.0~188
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3aff5d5f720d4c45c4dbb3a316be3399a3dea044;p=cvc5.git

Fix a couple of parse error messages for sygus (#8381)
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8edb39107..ac7392b86 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -281,8 +281,8 @@ command [std::unique_ptr<cvc5::Command>* cmd]
       // we allow overloading for function declarations
       if( PARSER_STATE->sygus() )
       {
-        PARSER_STATE->parseErrorLogic("declare-fun are not allowed in sygus "
-                                      "version 2.0");
+        PARSER_STATE->parseError("declare-fun are not allowed in sygus "
+                                 "version 2.0");
       }
       else
       {
@@ -780,8 +780,8 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
     { // allow overloading here
       if( PARSER_STATE->sygus() )
       {
-        PARSER_STATE->parseErrorLogic("declare-const is not allowed in sygus "
-                                      "version 2.0");
+        PARSER_STATE->parseError("declare-const is not allowed in sygus "
+                                 "version 2.0");
       }
       api::Term c =
           PARSER_STATE->bindVar(name, t, true);