1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 481493e13..22e3d0507 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -85,6 +85,8 @@ private:
 
   Statistics d_statistics;
 
+  context::CDO<bool> d_lemmasAdded;
+  
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
@@ -97,6 +99,8 @@ private:
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
+
+  
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.
@@ -147,7 +151,9 @@ private:
 
   void sendConflict();
 
-  void lemma(TNode node) { d_out->lemma(node); }
+  void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; }
+
+  void checkForLemma(TNode node); 
   
   friend class Bitblaster;
   friend class BitblastSolver;