From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 17 Sep 2014 16:21:39 +0000 (-0400)
Subject: Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.
X-Git-Tag: cvc5-1.0.0~6509^2~31
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=129b483eac716eef7c9de110a8600db417077ad2;p=cvc5.git

Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e05ffaebe..6e046444d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -420,6 +420,8 @@ command returns [CVC4::Command* cmd = NULL]
     | { if(PARSER_STATE->strictModeEnabled()) {
           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH.  Maybe you want (push 1)?");
         } else {
+          PARSER_STATE->pushScope();
+          PARSER_STATE->pushUnsatCoreNameScope();
           cmd = new PushCommand();
         }
       } )
@@ -448,6 +450,8 @@ command returns [CVC4::Command* cmd = NULL]
     | { if(PARSER_STATE->strictModeEnabled()) {
           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP.  Maybe you want (pop 1)?");
         } else {
+          PARSER_STATE->popUnsatCoreNameScope();
+          PARSER_STATE->popScope();
           cmd = new PopCommand();
         }
       } )