projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ca4a80) | patch
Remove spurious assertion in parser (#7713)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Dec 2021 00:40:33 +0000 (18:40 -0600)
committerGitHub <noreply@github.com>
Wed, 1 Dec 2021 00:40:33 +0000 (00:40 +0000)
commit08f42b62bb83a0d858862c832be70e38003b5dad
treef4858aca751a7da36169febeb2aa61456734149dtree
parent0ca4a8043609a4e65adb9fcbcd79ecd8cd6e93a4commit | diff
Remove spurious assertion in parser (#7713)

When global declarations are true, we do not push/pop the context of the symbol manager. This removes a spurious assertion that checked whether a pop in this case was greater than the actual context level of the symbol manager.

Fixes cvc5/cvc5-projects#370.
src/parser/smt2/Smt2.g diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/parser/proj-issue370-push-pop-global.smt2 [new file with mode: 0644] blob