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 dbc65d90f96e784a44fedb4ff71597657b9e301b..bdc5b32d404d14d4ceb24c5d75874be9b5982cb9 100644 (file)
--- 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();