Merged bit-vector and uf proof branch.

1 files changed, 13 insertions, 1 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4acd1b847..8f7e975cd 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -30,6 +30,8 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "proof/theory_proof.h"
+#include "proof/proof_manager.h"
 #include "theory/valuation.h"
 
 using namespace CVC4::context;
@@ -363,7 +365,6 @@ void TheoryBV::checkForLemma(TNode fact) {
   }
 }
 
-
 void TheoryBV::check(Effort e)
 {
   if (done() && !fullEffort(e)) {
@@ -706,6 +707,7 @@ Node TheoryBV::explain(TNode node) {
   // return the explanation
   Node explanation = utils::mkAnd(assumptions);
   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
+  Debug("bitvector::explain") << "TheoryBV::explain done. \n"; 
   return explanation;
 }
 
@@ -796,6 +798,16 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
   return changed;
 }
 
+void TheoryBV::setProofLog( BitVectorProof * bvp ) {
+  if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
+    d_eagerSolver->setProofLog( bvp );
+  }else{
+    for( unsigned i=0; i< d_subtheories.size(); i++ ){
+      d_subtheories[i]->setProofLog( bvp );
+    }
+  }
+}
+
 void TheoryBV::setConflict(Node conflict) {
   if (options::bvAbstraction()) {
     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);