summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-05-17 08:51:36 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-05-17 08:51:36 -0400
commit5ad796d0ddaa9c6f2ad98d2680babb7776a5f9b0 (patch)
treee7e21978833558a8f91e18fc543a5f4c72e4386a /src/parser
parent24cb86db0716875b14d86af27354e13898899b6c (diff)
Fixed "success" response to (push N) / (pop N) with N > 1.
Thanks to David Cok for reporting this issue.
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/smt2/Smt2.g8
1 files 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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback