1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index afa9f4b4f..3d151cfb1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -31,6 +31,14 @@
 #include "util/hash.h"
 #include "util/statistics_registry.h"
 
+// Forward declarations, needed because the BV theory and the BV Proof classes
+// are cyclically dependent
+namespace CVC4 {
+namespace proof {
+class BitVectorProof;
+}
+}  // namespace CVC4
+
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -104,7 +112,7 @@ public:
 
   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
 
-  void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp);
+  void setProofLog(proof::BitVectorProof* bvp);
 
  private: