From: Morgan Deters Date: Fri, 17 May 2013 12:51:36 +0000 (-0400) Subject: Fixed "success" response to (push N) / (pop N) with N > 1. X-Git-Tag: cvc5-1.0.0~7287^2~33^2~25 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3a34a4827c4188db9bd0274b34d4188aee00fff2;p=cvc5.git Fixed "success" response to (push N) / (pop N) with N > 1. Thanks to David Cok for reporting this issue. --- 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; }