1 files changed, 5 insertions, 3 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 0342288fe..82efbab0f 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -69,7 +69,10 @@ class TheoryProof;
 class UFProof;
 class ArithProof;
 class ArrayProof;
-class BitVectorProof;
+
+namespace proof {
+class ResolutionBitVectorProof;
+}
 
 template <class Solver> class LFSCSatProof;
 typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
@@ -77,7 +80,6 @@ typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
 class LFSCCnfProof;
 class LFSCTheoryProofEngine;
 class LFSCUFProof;
-class LFSCBitVectorProof;
 class LFSCRewriterProof;
 
 namespace prop {
@@ -189,7 +191,7 @@ public:
   static TheoryProofEngine* getTheoryProofEngine();
   static TheoryProof* getTheoryProof( theory::TheoryId id );
   static UFProof* getUfProof();
-  static BitVectorProof* getBitVectorProof();
+  static proof::ResolutionBitVectorProof* getBitVectorProof();
   static ArrayProof* getArrayProof();
   static ArithProof* getArithProof();