Merged bit-vector and uf proof branch.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 9a314fd6a..402dd6be3 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -74,6 +74,8 @@ protected:
 
   /** The bit-vector theory */
   TheoryBV* d_bv;
+  /** proof log */
+  BitVectorProof * d_bvp;
   AssertionQueue d_assertionQueue;
   context::CDO<uint32_t>  d_assertionIndex;
 public:
@@ -102,6 +104,7 @@ public:
     return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
+  virtual void setProofLog( BitVectorProof * bvp ) {}
   AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); }
   AssertionQueue::const_iterator assertionsEnd() { return d_assertionQueue.end(); }
 };