diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-17 12:24:50 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-17 12:24:50 -0400 |
| commit | 8c71dd4d6a68423bcf794dd6d6890d54d6d07e37 (patch) | |
| tree | 1d611c63dc2f4f9c5332032577dc690e98d405fc /src/parser | |
| parent | 944961607aa4a16c97d32e605c3f609ab66b4dc5 (diff) | |
| parent | 129b483eac716eef7c9de110a8600db417077ad2 (diff) | |
Merge branch '1.4.x'
Diffstat (limited to 'src/parser')
| -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 9f4b19c47..2efa7b55c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -428,6 +428,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(); } } ) @@ -458,6 +460,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(); } } ) |