Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).

1 files changed, 6 insertions, 1 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 0f9cfa710..2d8c4178a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -204,7 +204,7 @@ void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
   Debug("cores") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
   d_deps[Node::fromExpr(formula)]; // empty vector of deps
-  if(inUnsatCore || options::dumpUnsatCores()) {
+  if(inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) {
     Debug("cores") << "adding to input core forms: " << formula << std::endl;
     d_inputCoreFormulas.insert(formula);
   }
@@ -221,6 +221,11 @@ void ProofManager::addDependence(TNode n, TNode dep) {
   }
 }
 
+void ProofManager::addUnsatCore(Expr formula) {
+  Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end());
+  d_outputCoreFormulas.insert(formula);
+}
+
 void ProofManager::setLogic(const LogicInfo& logic) {
   d_logic = logic;
 }