diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 08:51:36 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-20 16:53:50 -0400 |
commit | 3a34a4827c4188db9bd0274b34d4188aee00fff2 (patch) | |
tree | 4f4819622c5f1bdb79c5f06b96be562da58afa37 /src/parser | |
parent | d4fb7022845f3ec595cff3fb1b6324e2364d25d3 (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.g | 8 |
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; } |