projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 30f9183) | patch
Define sort undeclared (#7714)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Dec 2021 00:11:54 +0000 (18:11 -0600)
committerGitHub <noreply@github.com>
Wed, 1 Dec 2021 00:11:54 +0000 (00:11 +0000)
commit0ca4a8043609a4e65adb9fcbcd79ecd8cd6e93a4
tree8e7af7f8adeb3e8dbcd3b236728ebc5e6f504b32tree
parent30f91833dea7f31156dafa401d17522b7fd87bc7commit | diff
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 diff | blob | history