3 files changed, 27 insertions, 8 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1962c6433..c66031265 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -788,6 +788,13 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_stats = new SmtEngineStatistics();
   d_stats->d_resourceUnitsUsed.setData(
       d_private->getResourceManager()->getResourceUsage());
+
+  // The ProofManager is constructed before any other proof objects such as
+  // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
+  // initialized in TheoryEngine and PropEngine respectively. 
+  Assert(d_proofManager == NULL);
+  PROOF( d_proofManager = new ProofManager(); ); 
+  
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, d_userContext,
@@ -798,6 +805,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   // Add the theories
   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
     TheoryConstructor::addTheory(d_theoryEngine, id);
+    //register with proof engine if applicable
+    THEORY_PROOF(ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); );
   }
 
   // global push/pop around everything, to ensure proper destruction
@@ -817,9 +826,6 @@ void SmtEngine::finishInit() {
   // ensure that our heuristics are properly set up
   setDefaults();
 
-  Assert(d_proofManager == NULL);
-  PROOF( d_proofManager = new ProofManager(); );
-
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
   d_decisionEngine->init();   // enable appropriate strategies
 
@@ -857,7 +863,7 @@ void SmtEngine::finishInit() {
   }
   d_dumpCommands.clear();
 
-  PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); );
+  PROOF( ProofManager::currentPM()->setLogic(d_logic); );
 }
 
 void SmtEngine::finalOptionsAreSet() {
@@ -3515,6 +3521,14 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
   dumpAssertions("post-definition-expansion", d_assertions);
 
+  // save the assertions now
+  THEORY_PROOF
+    (
+     for (unsigned i = 0; i < d_assertions.size(); ++i) {
+       ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
+     }
+     );
+  
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   if( options::ceGuidedInst() ){
@@ -3936,7 +3950,8 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
   PROOF(
     if( inInput ){
       // n is an input assertion
-      ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore);
+      if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores())
+        ProofManager::currentPM()->addCoreAssertion(n.toExpr());
     }else{
       // n is the result of an unknown preprocessing step, add it to dependency map to null
       ProofManager::currentPM()->addDependence(n, Node::null());
@@ -4724,7 +4739,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptExcepti
     throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.");
   }
 
-  d_proofManager->getProof(this);// just to trigger core creation
+  d_proofManager->traceUnsatCore();// just to trigger core creation
   return UnsatCore(this, d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
 #else /* IS_PROOFS_BUILD */
   throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index c4747d724..14adcc536 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -64,11 +64,12 @@ void SmtEngine::checkProof() {
   Chat() << "checking proof..." << endl;
 
   if( !(d_logic.isPure(theory::THEORY_BOOL) ||
+        d_logic.isPure(theory::THEORY_BV) ||
 	(d_logic.isPure(theory::THEORY_UF) &&
 	 ! d_logic.hasCardinalityConstraints())) ||
       d_logic.isQuantified()) {
     // no checking for these yet
-    Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl;
+    Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl;
     return;
   }
 
@@ -91,7 +92,7 @@ void SmtEngine::checkProof() {
   a.use_nested_app = false;
   a.compile_lib = false;
   init();
-  check_file(pfFile, args());
+  check_file(pfFile, a);
   close(fd);
 
 #else /* IS_PROOFS_BUILD */
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 83da5a159..c4ec15371 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -23,6 +23,8 @@
 #include "base/output.h"
 #include "base/tls.h"
 #include "expr/node_manager.h"
+#include "proof/proof.h"
+#include "proof/proof_manager.h"
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "util/configuration_private.h"
@@ -44,6 +46,7 @@ inline bool smtEngineInScope() {
   return s_smtEngine_current != NULL;
 }
 
+// FIXME: Maybe move into SmtScope?
 inline ProofManager* currentProofManager() {
 #if IS_PROOFS_BUILD
   Assert(options::proof() || options::unsatCores());