Fix fix. There are no unsat cores in 1.4
authorKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 17 Sep 2014 17:38:27 +0000 (13:38 -0400)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 17 Sep 2014 17:38:27 +0000 (13:38 -0400)
src/parser/smt2/Smt2.g

index 6e046444d708ab6fb72e03fcdd423cdb114771e2..6964e60693ae328f9da46344f20e7f5e3e208228 100644 (file)
@@ -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();
         }