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

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5b90ca14f861358f3bfec97ba2ac6f905fa19866..8f51c6d0d9ddc296deb4cb9317625169c555249b 100644 (file)
--- 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 36f2abdd203ba74046f03e109dfcb80be4d0f704..4c3c7b6bd4e03c5b00726303d4249ae222666ccd 100644 (file)
--- 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 730852d4ac9080d6c7ae05b69dcfa662cc8b12b6..90caa1fb18b411c0c5d2a5049c25ef69ee9933b0 100644 (file)
--- 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).");