From 3a34a4827c4188db9bd0274b34d4188aee00fff2 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 08:51:36 -0400
Subject: [PATCH] Fixed "success" response to (push N) / (pop N) with N > 1.

Thanks to David Cok for reporting this issue.
---
 src/parser/smt2/Smt2.g | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8dcde2483..76708807f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -314,7 +314,9 @@ command returns [CVC4::Command* cmd = NULL]
           CommandSequence* seq = new CommandSequence();
           do {
             PARSER_STATE->pushScope();
-            seq->addCommand(new PushCommand());
+            Command* c = new PushCommand();
+            c->setMuted(n > 1);
+            seq->addCommand(c);
           } while(--n > 0);
           cmd = seq;
         }
@@ -337,7 +339,9 @@ command returns [CVC4::Command* cmd = NULL]
           CommandSequence* seq = new CommandSequence();
           do {
             PARSER_STATE->popScope();
-            seq->addCommand(new PopCommand());
+            Command* c = new PopCommand();
+            c->setMuted(n > 1);
+            seq->addCommand(c);
           } while(--n > 0);
           cmd = seq;
         }
-- 
2.30.2