diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-17 12:21:39 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-17 12:24:15 -0400 |
| commit | 129b483eac716eef7c9de110a8600db417077ad2 (patch) | |
| tree | b943dde4fa18ea101700318b038dfc09230e7cd8 /src | |
| parent | 822cf47dbb9dc703b70aa9d384230c56e7afc285 (diff) | |
Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e05ffaebe..6e046444d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -420,6 +420,8 @@ command returns [CVC4::Command* cmd = NULL] | { if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH. Maybe you want (push 1)?"); } else { + PARSER_STATE->pushScope(); + PARSER_STATE->pushUnsatCoreNameScope(); cmd = new PushCommand(); } } ) @@ -448,6 +450,8 @@ command returns [CVC4::Command* cmd = NULL] | { if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP. Maybe you want (pop 1)?"); } else { + PARSER_STATE->popUnsatCoreNameScope(); + PARSER_STATE->popScope(); cmd = new PopCommand(); } } ) |