summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-10-06 14:47:54 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2014-10-06 14:47:54 -0400
commit6970ed001a5704b1b79bb3775adce70f8c3b9778 (patch)
treebb2d0bcd051352b7f1c601d29e6e5fbc1736445d /src/parser
parent1d9d1933a32df3a0b1deeef5adab019fad4f74d0 (diff)
Clear out decls/defs with RESET command.
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 81e022c82..151e2ecb6 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -697,7 +697,9 @@ mainCommand[CVC4::Command*& cmd]
{ UNSUPPORTED("POPTO_SCOPE command"); }
| RESET_TOK
- { cmd = new ResetCommand(); }
+ { cmd = new ResetCommand();
+ PARSER_STATE->reset();
+ }
// Datatypes can be mututally-recursive if they're in the same
// definition block, separated by a comma. So we parse everything
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback