diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-17 13:38:27 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-17 13:38:27 -0400 |
| commit | 8d5eb49d38371a2c682642d21d6b7aa151a9aa51 (patch) | |
| tree | e019578aa97a563e6c39b5b09ab3da56fb936f31 | |
| parent | 129b483eac716eef7c9de110a8600db417077ad2 (diff) | |
Fix fix. There are no unsat cores in 1.4
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6e046444d..6964e6069 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -421,7 +421,6 @@ command returns [CVC4::Command* cmd = NULL] 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(); } } ) @@ -450,7 +449,6 @@ 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(); } |