From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sat, 23 Aug 2014 05:13:49 +0000 (-0400)
Subject: Some fixes for dump- and get-unsat-core.
X-Git-Tag: cvc5-1.0.0~6653
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba9a2a34e37f856774662b50a09b3a1d3b9ae89f;p=cvc5.git

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

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).");