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.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bdc5b32d404d14d4ceb24c5d75874be9b5982cb9..5924ecde6c708026aa101a1cb8379431543305f4 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -444,10 +444,9 @@ command [std::unique_ptr<cvc5::Command>* 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 e52f2ac63ab3e6b4d84fca5f1a08ed02cb6d99af..2478bd2766157c37505372a63dc34fc73b572282 100644 (file)
--- 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 (file)
index 0000000..b46cf34
--- /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)