diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 7 |
1 files changed, 3 insertions, 4 deletions
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<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) { |