Merged bit-vector and uf proof branch.

16 files changed, 169 insertions, 107 deletions

diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index 0990c2f29..bc022a02d 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -253,17 +253,17 @@ void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   
   Assert(node.getKind() == kind::BITVECTOR_AND &&
          bits.size() == 0);
-  
-  for(unsigned j = 0; j < utils::getSize(node); ++j) {
-    std::vector<T> and_j; 
-    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-      std::vector<T> current;
-      bb->bbTerm(node[i], current);
-      and_j.push_back(current[j]); 
-      Assert(utils::getSize(node) == current.size());
+
+  bb->bbTerm(node[0], bits);
+  std::vector<T> current;
+  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+    bb->bbTerm(node[j], current);
+    for (unsigned i = 0; i < utils::getSize(node); ++i) {
+      bits[i] = mkAnd(bits[i], current[i]);
     }
-    bits.push_back(mkAnd(and_j)); 
+    current.clear();
   }
+  Assert (bits.size() == utils::getSize(node));
 }
 
 template <class T>
@@ -272,17 +272,17 @@ void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
 
   Assert(node.getKind() == kind::BITVECTOR_OR &&
          bits.size() == 0);
-  
-  for(unsigned j = 0; j < utils::getSize(node); ++j) {
-    std::vector<T> or_j;
-    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-      std::vector<T> current;
-      bb->bbTerm(node[i], current);
-      or_j.push_back(current[j]); 
-      Assert(utils::getSize(node) == current.size());
+
+  bb->bbTerm(node[0], bits);
+  std::vector<T> current;
+  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+    bb->bbTerm(node[j], current);
+    for (unsigned i = 0; i < utils::getSize(node); ++i) {
+      bits[i] = mkOr(bits[i], current[i]);
     }
-    bits.push_back(mkOr(or_j)); 
+    current.clear();
   }
+  Assert (bits.size() == utils::getSize(node));
 }
 
 template <class T>
@@ -291,20 +291,17 @@ void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
 
   Assert(node.getKind() == kind::BITVECTOR_XOR &&
          bits.size() == 0);
-  
-  for(unsigned j = 0; j < utils::getSize(node); ++j) {
-    std::vector<T> first;
-    bb->bbTerm(node[0], first); 
-    T bitj = first[j];
-    
-    for (unsigned i = 1; i < node.getNumChildren(); ++i) {
-      std::vector<T> current;
-      bb->bbTerm(node[i], current);
-      bitj = mkXor(bitj, current[j]);
-      Assert(utils::getSize(node) == current.size());
+
+  bb->bbTerm(node[0], bits);
+  std::vector<T> current;
+  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+    bb->bbTerm(node[j], current);
+    for (unsigned i = 0; i < utils::getSize(node); ++i) {
+      bits[i] = mkXor(bits[i], current[i]);
     }
-    bits.push_back(bitj); 
+    current.clear();
   }
+  Assert (bits.size() == utils::getSize(node));
 }
 
 template <class T>
diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h
index a236c69e8..adaed31c1 100644
--- a/src/theory/bv/bitblast_utils.h
+++ b/src/theory/bv/bitblast_utils.h
@@ -221,7 +221,7 @@ inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, s
   T carry_in = mkFalse<T>();
   T carry_out;
     for(unsigned j = 0; j < res.size() -k; ++j) {
-      T aj = mkAnd(a[j], b[k]);
+      T aj = mkAnd(b[k], a[j]);
       carry_out = mkOr(mkAnd(res[j+k], aj),
                        mkAnd( mkXor(res[j+k], aj), carry_in));
       res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index ec76bb4f6..66eea0997 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -85,6 +85,8 @@ protected:
   TermDefMap d_termCache;
   ModelCache d_modelCache;
 
+  BitVectorProof * d_bvp;
+
   void initAtomBBStrategies();
   void initTermBBStrategies();
 protected:
@@ -105,7 +107,7 @@ public:
 
   bool hasBBTerm(TNode node) const;
   void getBBTerm(TNode node, Bits& bits) const;
-  void storeBBTerm(TNode term, const Bits& bits);
+  virtual void storeBBTerm(TNode term, const Bits& bits);
   /**
    * Return a constant representing the value of a in the  model.
    * If fullModel is true set unconstrained bits to 0. If not return
@@ -171,7 +173,9 @@ public:
   void bbAtom(TNode node);
   Node getBBAtom(TNode atom) const;
   void storeBBAtom(TNode atom, Node atom_bb);
-  bool hasBBAtom(TNode atom) const;
+  void storeBBTerm(TNode node, const Bits& bits);
+  bool hasBBAtom(TNode atom) const; 
+
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
   ~TLazyBitblaster() throw();
   /**
@@ -201,6 +205,7 @@ public:
    * constants to equivalence classes that don't already have them
    */
   void collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog( BitVectorProof * bvp );
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
@@ -277,9 +282,12 @@ public:
   bool hasBBAtom(TNode atom) const;
   void bbFormula(TNode formula);
   void storeBBAtom(TNode atom, Node atom_bb);
+  void storeBBTerm(TNode node, const Bits& bits);
+
   bool assertToSat(TNode node, bool propagate = true);
   bool solve();
   void collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog( BitVectorProof * bvp );
 };
 
 class BitblastingRegistrar: public prop::Registrar {
@@ -406,6 +414,7 @@ template <class T>
 TBitblaster<T>::TBitblaster()
   : d_termCache()
   , d_modelCache()
+  , d_bvp( NULL )
 {
   initAtomBBStrategies();
   initTermBBStrategies(); 
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 66b1c4182..2af8d04d6 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -16,6 +16,7 @@
 
 #include "options/bv_options.h"
 #include "theory/bv/bitblaster_template.h"
+#include "proof/bitvector_proof.h"
 #include "theory/bv/bv_eager_solver.h"
 
 using namespace std;
@@ -54,6 +55,12 @@ void EagerBitblastSolver::initialize() {
     d_aigBitblaster = new AigBitblaster();
   } else {
     d_bitblaster = new EagerBitblaster(d_bv);
+    THEORY_PROOF(
+      if( d_bvp ){
+        d_bitblaster->setProofLog( d_bvp );
+        d_bvp->setBitblaster(d_bitblaster);
+      }
+    );
   }
 }
 
@@ -112,3 +119,7 @@ void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
   AlwaysAssert(!d_useAig && d_bitblaster);
   d_bitblaster->collectModelInfo(m, fullModel); 
 }
+
+void EagerBitblastSolver::setProofLog( BitVectorProof * bvp ) {
+  d_bvp = bvp;
+}
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index ff13867cc..cfc84dae1 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -39,7 +39,9 @@ class EagerBitblastSolver {
   EagerBitblaster* d_bitblaster;
   AigBitblaster* d_aigBitblaster;
   bool d_useAig;
-  TheoryBV* d_bv;
+
+  TheoryBV* d_bv; 
+  BitVectorProof * d_bvp;
 
 public:
   EagerBitblastSolver(theory::bv::TheoryBV* bv);
@@ -53,6 +55,7 @@ public:
   bool isInitialized();
   void initialize();
   void collectModelInfo(theory::TheoryModel* m, bool fullModel);
+  void setProofLog( BitVectorProof * bvp );
 };
 
 }
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(); }
 };
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 9f8cb580c..e7630bb3f 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -24,6 +24,8 @@
 #include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "proof/proof_manager.h"
+#include "proof/bitvector_proof.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -44,7 +46,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
     d_abstractionModule(NULL),
     d_quickCheck(options::bitvectorQuickXplain() ? new BVQuickCheck("bb", bv) : NULL),
     d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("bb", d_quickCheck) :  NULL)
-{}
+{
+}
 
 BitblastSolver::~BitblastSolver() {
   delete d_quickXplain;
@@ -232,40 +235,6 @@ Node BitblastSolver::getModelValue(TNode node)
   return val;
 }
 
-// Node BitblastSolver::getModelValueRec(TNode node)
-// {
-//   Node val;
-//   if (node.isConst()) {
-//     return node;
-//   }
-//   NodeMap::iterator it = d_modelCache.find(node);
-//   if (it != d_modelCache.end()) {
-//     val = (*it).second;
-//     Debug("bitvector-model") << node << " => (cached) " << val <<"\n";
-//     return val;
-//   }
-//   if (d_bv->isLeaf(node)) {
-//     val = d_bitblaster->getVarValue(node);
-//     if (val == Node()) {
-//       // If no value in model, just set to 0
-//       val = utils::mkConst(utils::getSize(node), (unsigned)0);
-//     }
-//   } else {
-//     NodeBuilder<> valBuilder(node.getKind());
-//     if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-//       valBuilder << node.getOperator();
-//     }
-//     for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-//       valBuilder << getModelValueRec(node[i]);
-//     }
-//     val = valBuilder;
-//     val = Rewriter::rewrite(val);
-//   }
-//   Assert(val.isConst());
-//   d_modelCache[node] = val;
-//   Debug("bitvector-model") << node << " => " << val <<"\n";
-//   return val;
-// }
 
 
 void BitblastSolver::setConflict(TNode conflict) {
@@ -279,6 +248,12 @@ void BitblastSolver::setConflict(TNode conflict) {
   d_bv->setConflict(final_conflict);
 }
 
+void BitblastSolver::setProofLog( BitVectorProof * bvp ) {
+  d_bitblaster->setProofLog( bvp );
+  bvp->setBitblaster(d_bitblaster);
+}
+
 }/* namespace CVC4::theory::bv */
 }/* namespace CVC4::theory */
 }/* namespace CVC4 */
+
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 0e066eefb..c69069109 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -73,8 +73,9 @@ public:
   void bitblastQueue();
   void setAbstraction(AbstractionModule* module); 
   uint64_t computeAtomWeight(TNode atom); 
+  void setProofLog( BitVectorProof * bvp );
 };
 
-}
-}
-}
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 000abe62b..2e4f06c38 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -19,16 +19,13 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
+#include "proof/bitvector_proof.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -46,13 +43,19 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
 
-  d_satSolver = prop::SatSolverFactory::createMinisat(
-      d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
-                                           d_nullContext, d_bv->globals());
-
+  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext,
+                                                      smtStatisticsRegistry(),
+                                                      "EagerBitblaster");
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
+                                           d_bitblastingRegistrar,
+                                           d_nullContext,
+                                           d_bv->globals(),
+                                           options::proof(),
+                                           "EagerBitblaster");
+  
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
+  d_bvp = NULL;
 }
 
 EagerBitblaster::~EagerBitblaster() {
@@ -85,21 +88,34 @@ void EagerBitblaster::bbAtom(TNode node) {
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
-      Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
-      normalized;
+    d_atomBBStrategies[normalized.getKind()](normalized, this) :
+    normalized;
+
+  if (!options::proof()) {
+    atom_bb = Rewriter::rewrite(atom_bb);
+  }
+
   // asserting that the atom is true iff the definition holds
   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
 
-  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
-  storeBBAtom(node, atom_definition);
+  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); 
+  storeBBAtom(node, atom_bb);
   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
 
 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
-  // no need to store the definition for the lazy bit-blaster
-  d_bbAtoms.insert(atom);
+  if( d_bvp ){
+    d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
+  }
+  d_bbAtoms.insert(atom); 
 }
 
+void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
+  if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
+  d_termCache.insert(std::make_pair(node, bits));
+}
+
+
 bool EagerBitblaster::hasBBAtom(TNode atom) const {
   return d_bbAtoms.find(atom) != d_bbAtoms.end();
 }
@@ -211,6 +227,12 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   }
 }
 
+void EagerBitblaster::setProofLog( BitVectorProof * bvp ) {
+  d_bvp = bvp;
+  d_satSolver->setProofLog(bvp);
+  bvp->initCnfProof(d_cnfStream, d_nullContext);
+}
+
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 34a9418dd..9268e2152 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -25,7 +25,9 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
-#include "theory_bv_utils.h"
+#include "proof/bitvector_proof.h"
+#include "proof/proof_manager.h"
+#include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
 namespace theory {
@@ -51,8 +53,12 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
       c, smtStatisticsRegistry(), name);
   d_nullRegistrar = new prop::NullRegistrar();
   d_nullContext = new context::Context();
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
-                                           d_nullContext, d_bv->globals());
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
+                                           d_nullRegistrar,
+                                           d_nullContext,
+                                           d_bv->globals(),
+                                           options::proof(),
+                                           "LazyBitblaster");
 
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
@@ -127,8 +133,12 @@ void TLazyBitblaster::bbAtom(TNode node) {
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
-    Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
-    normalized;
+                 d_atomBBStrategies[normalized.getKind()](normalized, this) : normalized;
+
+  if (!options::proof()) {
+    atom_bb = Rewriter::rewrite(atom_bb);
+  }
+      
   // asserting that the atom is true iff the definition holds
   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
   storeBBAtom(node, atom_bb);
@@ -136,10 +146,19 @@ void TLazyBitblaster::bbAtom(TNode node) {
 }
 
 void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
-  // no need to store the definition for the lazy bit-blaster
+  // No need to store the definition for the lazy bit-blaster (unless proofs are enabled).
+  if( d_bvp != NULL ){
+    d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
+  }
   d_bbAtoms.insert(atom); 
 }
 
+void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
+  if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
+  d_termCache.insert(std::make_pair(node, bits));
+}
+
+
 bool TLazyBitblaster::hasBBAtom(TNode atom) const {
   return d_bbAtoms.find(atom) != d_bbAtoms.end(); 
 }
@@ -483,6 +502,12 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   }
 }
 
+void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
+  d_bvp = bvp;
+  d_satSolver->setProofLog( bvp );
+  bvp->initCnfProof(d_cnfStream, d_nullContext);
+}
+
 void TLazyBitblaster::clearSolver() {
   Assert (d_ctx->getLevel() == 0);
   delete d_satSolver;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4acd1b847..8f7e975cd 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -30,6 +30,8 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "proof/theory_proof.h"
+#include "proof/proof_manager.h"
 #include "theory/valuation.h"
 
 using namespace CVC4::context;
@@ -363,7 +365,6 @@ void TheoryBV::checkForLemma(TNode fact) {
   }
 }
 
-
 void TheoryBV::check(Effort e)
 {
   if (done() && !fullEffort(e)) {
@@ -706,6 +707,7 @@ Node TheoryBV::explain(TNode node) {
   // return the explanation
   Node explanation = utils::mkAnd(assumptions);
   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
+  Debug("bitvector::explain") << "TheoryBV::explain done. \n"; 
   return explanation;
 }
 
@@ -796,6 +798,16 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
   return changed;
 }
 
+void TheoryBV::setProofLog( BitVectorProof * bvp ) {
+  if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
+    d_eagerSolver->setProofLog( bvp );
+  }else{
+    for( unsigned i=0; i< d_subtheories.size(); i++ ){
+      d_subtheories[i]->setProofLog( bvp );
+    }
+  }
+}
+
 void TheoryBV::setConflict(Node conflict) {
   if (options::bvAbstraction()) {
     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index e7e4d464f..27138abfc 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -87,7 +87,10 @@ public:
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
   void presolve();
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+
+  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  
+  void setProofLog( BitVectorProof * bvp );
 
 private:
 
@@ -209,11 +212,10 @@ private:
 
   void sendConflict();
 
-  void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; }
+  void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
 
   void checkForLemma(TNode node); 
 
- 
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
   friend class EagerBitblaster;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 676df5dde..185985b3b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -276,7 +276,8 @@ bool RewriteRule<ReflexivityEq>::applies(TNode node) {
 template<> inline
 Node RewriteRule<ReflexivityEq>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
-  return node[1].eqNode(node[0]);
+  Node res = node[1].eqNode(node[0]);
+  return res;
 }
 
 }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index cd173a6dd..d5d6c39dd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -325,7 +325,8 @@ Node RewriteRule<XnorEliminate>::apply(TNode node) {
   TNode a = node[0];
   TNode b = node[1]; 
   Node xorNode = utils::mkNode(kind::BITVECTOR_XOR, a, b);
-  return utils::mkNode(kind::BITVECTOR_NOT, xorNode); 
+  Node result = utils::mkNode(kind::BITVECTOR_NOT, xorNode);
+  return result;
 }
 
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 3bf390ded..4d3b676c9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -379,8 +379,8 @@ Node RewriteRule<XorZero>::apply(TNode node) {
       children.push_back(node[i]); 
     }
   }
-
-  return utils::mkNode(kind::BITVECTOR_XOR, children); 
+  Node res = utils::mkNode(kind::BITVECTOR_XOR, children); 
+  return res;
 }
 
 
@@ -488,7 +488,7 @@ bool RewriteRule<NotIdemp>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NotIdemp>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl;
   return node[0][0];
 }
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index ba8074fbb..993be309b 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -51,11 +51,11 @@ inline unsigned getSize(TNode node) {
   return node.getType().getBitVectorSize();
 }
 
-// this seems to behave strangely
-inline const Integer& getBit(TNode node, unsigned i) {
-  Assert (0); 
-  Assert (node.getKind() == kind::CONST_BITVECTOR);
-  return node.getConst<BitVector>().extract(i, i).getValue();
+inline const bool getBit(TNode node, unsigned i) {
+  Assert (i < utils::getSize(node) && 
+          node.getKind() == kind::CONST_BITVECTOR);
+  Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
+  return (bit == 1u); 
 }
 
 inline Node mkTrue() {