1 files changed, 10 insertions, 6 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index cfad0a068..ee06fbfa0 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -22,12 +22,12 @@
 #include "options/proof_options.h"
 #include "proof/arith_proof.h"
 #include "proof/array_proof.h"
-#include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
+#include "proof/resolution_bitvector_proof.h"
 #include "proof/sat_proof.h"
 #include "proof/simplify_boolean_node.h"
 #include "proof/uf_proof.h"
@@ -46,6 +46,9 @@
 
 namespace CVC4 {
 
+using proof::LFSCBitVectorProof;
+using proof::ResolutionBitVectorProof;
+
 unsigned CVC4::ProofLetCount::counter = 0;
 static unsigned LET_COUNT = 1;
 
@@ -77,7 +80,8 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
       }
 
       if (id == theory::THEORY_BV) {
-        BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this);
+        auto bv_theory = static_cast<theory::bv::TheoryBV*>(th);
+        ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this);
         d_theoryProofTable[id] = bvp;
         return;
       }
@@ -102,9 +106,9 @@ void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) {
     theory::TheoryId id = th->getId();
     if (id == theory::THEORY_BV) {
       Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end());
-
-      BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id];
-      ((theory::bv::TheoryBV*)th)->setProofLog( bvp );
+      ResolutionBitVectorProof* bvp =
+          (ResolutionBitVectorProof*)d_theoryProofTable[id];
+      ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp);
       return;
     }
   }
@@ -529,7 +533,7 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std
     }
   }
 
-  BitVectorProof* bv = ProofManager::getBitVectorProof();
+  ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof();
   bv->finalizeConflicts(bv_lemmas);
   //  bv->printResolutionProof(os, paren, letMap);
 }