From 0ca4a8043609a4e65adb9fcbcd79ecd8cd6e93a4 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 30 Nov 2021 18:11:54 -0600
Subject: [PATCH] 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)
                    ^
")
---
 src/parser/smt2/Smt2.g | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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();
-- 
2.30.2