From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 1 Dec 2021 00:11:54 +0000 (-0600)
Subject: Define sort undeclared (#7714)
X-Git-Tag: cvc5-1.0.0~749
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ca4a8043609a4e65adb9fcbcd79ecd8cd6e93a4;p=cvc5.git

Define sort undeclared (#7714)

Fixes cvc5/cvc5-projects#369.

Now gives:

(error "Parse Error: proj-369.smt2:3.22: Symbol 'Bool' previously declared as a type

  (define-sort _s0 (Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
                    ^
")
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dbc65d90f..bdc5b32d4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -248,7 +248,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
     { PARSER_STATE->checkUserSymbol(name); }
-    LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
+    LPAREN_TOK symbolList[names,CHECK_UNDECLARED,SYM_SORT] RPAREN_TOK
     { PARSER_STATE->pushScope();
       for(std::vector<std::string>::const_iterator i = names.begin(),
             iend = names.end();