From 08f42b62bb83a0d858862c832be70e38003b5dad Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Nov 2021 18:40:33 -0600 Subject: 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 | 7 +++---- test/regress/CMakeLists.txt | 1 + test/regress/regress0/parser/proj-issue370-push-pop-global.smt2 | 6 ++++++ 3 files changed, 10 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/parser/proj-issue370-push-pop-global.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bdc5b32d4..5924ecde6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -444,10 +444,9 @@ command [std::unique_ptr* cmd] } ( k=INTEGER_LITERAL { unsigned num = AntlrInput::tokenToUnsigned(k); - if(num > PARSER_STATE->scopeLevel()) { - PARSER_STATE->parseError("Attempted to pop above the top stack " - "frame."); - } + // we don't compare num to PARSER_STATE->scopeLevel() here, since + // when global declarations is true, the scope level of the parser + // is not indicative of the context level. if(num == 0) { cmd->reset(new EmptyCommand()); } else if(num == 1) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e52f2ac63..2478bd276 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -803,6 +803,7 @@ set(regress_0_tests regress0/parser/linear_arithmetic_err3.smt2 regress0/parser/named-attr-error.smt2 regress0/parser/named-attr.smt2 + regress0/parser/proj-issue370-push-pop-global.smt2 regress0/parser/quoted-define-fun.smt2 regress0/parser/shadow_fun_symbol_all.smt2 regress0/parser/shadow_fun_symbol_nirat.smt2 diff --git a/test/regress/regress0/parser/proj-issue370-push-pop-global.smt2 b/test/regress/regress0/parser/proj-issue370-push-pop-global.smt2 new file mode 100644 index 000000000..b46cf3445 --- /dev/null +++ b/test/regress/regress0/parser/proj-issue370-push-pop-global.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: -i +; EXIT: 0 +(set-option :global-declarations true) +(set-logic ALL) +(push 2) +(pop 2) -- cgit v1.2.3