Some fixes for dump- and get-unsat-core.

3 files changed, 8 insertions, 1 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5b90ca14f..8f51c6d0d 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -134,6 +134,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     } else if( d_options[options::dumpInstantiations] &&
                res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetInstantiationsCommand();
+    } else if( d_options[options::dumpUnsatCores] &&
+               res.asSatisfiabilityResult() == Result::UNSAT ) {
+      g = new GetUnsatCoreCommand();
     }
     if( g ){
       //set no time limit during dumping if applicable
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 36f2abdd2..4c3c7b6bd 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -374,6 +374,10 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
         Command* gi = new GetInstantiationsCommand();
         status = doCommandSingleton(gi);
+      } else if( d_options[options::dumpUnsatCores] &&
+                 d_result.asSatisfiabilityResult() == Result::UNSAT ) {
+        Command* guc = new GetUnsatCoreCommand();
+        status = doCommandSingleton(guc);
       }
     }
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 730852d4a..90caa1fb1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3968,7 +3968,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
     throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.");
   }
 
-  delete d_proofManager->getProof(this);// just to trigger core creation
+  d_proofManager->getProof(this);// just to trigger core creation
   return UnsatCore(d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
 #else /* CVC4_PROOF */
   throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");