Merging proof branch

46 files changed, 2639 insertions, 847 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index a3580989c..cfa4982ca 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -96,10 +96,14 @@ libcvc4_la_SOURCES = \
 	proof/skolemization_manager.h \
 	proof/theory_proof.cpp \
 	proof/theory_proof.h \
+	proof/lemma_proof.cpp \
+	proof/lemma_proof.h \
 	proof/uf_proof.cpp \
 	proof/uf_proof.h \
 	proof/unsat_core.cpp \
 	proof/unsat_core.h \
+	proof/proof_output_channel.cpp \
+	proof/proof_output_channel.h \
 	prop/cnf_stream.cpp \
 	prop/cnf_stream.h \
 	prop/prop_engine.cpp \
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 643932781..e8a18481b 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -10,7 +10,7 @@
 # Step 4: Generate X_options.h from X_options.sed
 # Step 5: Generate X_options.cpp from X_options.sed.
 #   This stage also waits for X_options.h as otherwise it cannot compile.
-# 
+#
 
 OPTIONS_SRC_FILES = \
 	arith_options \
@@ -424,4 +424,3 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed
 # directories that are cleaned first.  Without this rule, "distclean"
 # fails.
 %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@"
-
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index a1287b667..b9907aac9 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -830,4 +830,8 @@ void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
   // Nothing to do here at this point.
 }
 
+void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+  // Nothing to do here at this point.
+}
+
 } /* CVC4  namespace */
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 788e4bd86..810d41155 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -74,6 +74,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
 };
 
 
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 8aba8dce9..aee236677 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -81,14 +81,29 @@ inline static bool match(TNode n1, TNode n2) {
 
 void ProofArray::setRowMergeTag(unsigned tag) {
   d_reasonRow = tag;
+  d_proofPrinter.d_row = tag;
 }
 
 void ProofArray::setRow1MergeTag(unsigned tag) {
   d_reasonRow1 = tag;
+  d_proofPrinter.d_row1 = tag;
 }
 
 void ProofArray::setExtMergeTag(unsigned tag) {
   d_reasonExt = tag;
+  d_proofPrinter.d_ext = tag;
+}
+
+unsigned ProofArray::getRowMergeTag() const {
+  return d_reasonRow;
+}
+
+unsigned ProofArray::getRow1MergeTag() const {
+  return d_reasonRow1;
+}
+
+unsigned ProofArray::getExtMergeTag() const {
+  return d_reasonExt;
 }
 
 void ProofArray::toStream(std::ostream& out) {
@@ -101,7 +116,7 @@ void ProofArray::toStream(std::ostream& out) {
 
 void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) {
   Debug("pf::array") << "Printing array proof in LFSC : " << std::endl;
-  pf->debug_print("pf::array");
+  pf->debug_print("pf::array", 0, &d_proofPrinter);
   Debug("pf::array") << std::endl;
   toStreamRecLFSC( out, tp, pf, 0, map );
   Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
@@ -114,7 +129,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                                  const LetMap& map) {
 
   Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
-  pf->debug_print("pf::array");
+  pf->debug_print("pf::array", 0, &d_proofPrinter);
   Debug("pf::array") << std::endl;
 
   if(tb == 0) {
@@ -150,7 +165,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                pf->d_children[i + count]->d_node.isNull();
              ++count) {
           Debug("pf::array") << "Found a congruence: " << std::endl;
-          pf->d_children[i+count]->debug_print("pf::array");
+          pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter);
           congruenceClosures.push_back(pf->d_children[i+count]);
         }
 
@@ -220,48 +235,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         ++i;
       }
     }
-    Assert(neg >= 0);
+
+    bool disequalityFound = (neg >= 0);
+    if (!disequalityFound) {
+      Debug("pf::array") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
+      Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
+      Assert(pf->d_node.getKind() == kind::EQUAL);
+      Assert(pf->d_node.getNumChildren() == 2);
+      Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+    }
 
     Node n1;
     std::stringstream ss, ss2;
     //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
     Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
-    if(pf->d_children.size() > 2) {
+    if(!disequalityFound || pf->d_children.size() > 2) {
       n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
     } else {
       n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
       Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
     }
 
-    Node n2 = pf->d_children[neg]->d_node;
-    Assert(n2.getKind() == kind::NOT);
-    Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
-    Debug("mgdx") << "n2 is " << n2 << std::endl;
-    Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
-    Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
-
-    if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
-    if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
-
-    if (pf->d_children[neg]->d_id == d_reasonExt) {
-      // The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
-
-      //      	    (clausify_false (contra _ .gl2 (or_elim_1 _ _ .gl1 FIXME))))))) (\ .glemc6
-
-      out << "(clausify_false (contra _ ";
-      out << ss.str();
-
-      toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+    out << "(clausify_false (contra _ ";
 
-      out << " ";
-      out << ss2.str();
-      out << "))";
+    if (disequalityFound) {
+      Node n2 = pf->d_children[neg]->d_node;
+      Assert(n2.getKind() == kind::NOT);
+      Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
+      Debug("mgdx") << "n2 is " << n2 << std::endl;
+      Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
+      Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
 
-    } else {
-      // The negative node is, e.g., a pure equality
-      out << "(clausify_false (contra _ ";
+      if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
+      if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
 
-      if(n2[0].getKind() == kind::APPLY_UF) {
+      if ((pf->d_children[neg]->d_id == d_reasonExt) ||
+          (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) {
+        // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
+        out << ss.str();
+        out << " ";
+        toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+        out << ss2.str();
+      } else if (n2[0].getKind() == kind::APPLY_UF) {
         out << "(trans _ _ _ _ ";
         out << "(symm _ _ _ ";
         out << ss.str();
@@ -276,16 +291,27 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         Debug("pf::array") << "ArrayProof::toStream: getLitName( " << n2[0] << " ) = " <<
           ProofManager::getLitName(n2[0]) << std::endl;
 
-        out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
+        out << " " << ProofManager::getLitName(n2[0]);
       }
+    } else {
+      Node n2 = pf->d_node;
+      Assert(n2.getKind() == kind::EQUAL);
+      Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+
+      out << ss.str();
+      out << " ";
+      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
+                                                                          n1[0].toExpr(),
+                                                                          n1[1].toExpr());
     }
 
+    out << "))" << std::endl;
     return Node();
   }
 
   if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
     Debug("mgd") << "\nok, looking at congruence:\n";
-    pf->debug_print("mgd");
+    pf->debug_print("mgd", 0, &d_proofPrinter);
     std::stack<const theory::eq::EqProof*> stk;
     for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
       Assert(!pf2->d_node.isNull());
@@ -315,7 +341,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
 
     Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
-    pf2->debug_print("mgd");
+    pf2->debug_print("mgd", 0, &d_proofPrinter);
     // Temp
     Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl;
     Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl;
@@ -332,7 +358,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       Debug("mgd") << "SIDE IS 1\n";
       if(!match(pf2->d_node, n1[1])) {
         Debug("mgd") << "IN BAD CASE, our first subproof is\n";
-        pf2->d_children[0]->debug_print("mgd");
+        pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter);
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -546,6 +572,20 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     return pf->d_node;
   }
 
+  else if (pf->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
+    Debug("pf::array") << "Proof for: " << pf->d_node << std::endl;
+    Assert(pf->d_node.getKind() == kind::NOT);
+    Node n = pf->d_node[0];
+    Assert(n.getKind() == kind::EQUAL);
+    Assert(n.getNumChildren() == 2);
+    Assert(n[0].isConst() && n[1].isConst());
+
+    ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out,
+                                                                        n[0].toExpr(),
+                                                                        n[1].toExpr());
+    return pf->d_node;
+  }
+
   else if (pf->d_id == theory::eq::MERGED_THROUGH_TRANS) {
     bool firstNeg = false;
     bool secondNeg = false;
@@ -554,7 +594,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Assert(pf->d_children.size() >= 2);
     std::stringstream ss;
     Debug("mgd") << "\ndoing trans proof[[\n";
-    pf->debug_print("mgd");
+    pf->debug_print("mgd", 0, &d_proofPrinter);
     Debug("mgd") << "\n";
     Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
     Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
@@ -772,7 +812,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
           Warning() << "\n\ntrans proof failure at step " << i << "\n\n";
           Warning() << "0 proves " << n1 << "\n";
           Warning() << "1 proves " << n2 << "\n\n";
-          pf->debug_print("mgdx",0);
+          pf->debug_print("mgdx", 0, &d_proofPrinter);
           //toStreamRec(Warning.getStream(), pf, 0);
           Warning() << "\n\n";
           Unreachable();
@@ -931,6 +971,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       t4 = pf->d_children[0]->d_node[0][side][0][2];
       ret = pf->d_node;
 
+      // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
+      bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]);
+
       Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
 
       Assert(pf->d_children.size() == 1);
@@ -939,28 +982,31 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
       Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
 
+      if (swap) {
+        out << "(symm _ _ _ ";
+      }
+
       out << "(negativerow _ _ ";
-      tp->printTerm(t1.toExpr(), out, map);
+      tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map);
       out << " ";
-      tp->printTerm(t2.toExpr(), out, map);
+      tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map);
       out << " ";
       tp->printTerm(t3.toExpr(), out, map);
       out << " ";
       tp->printTerm(t4.toExpr(), out, map);
       out << " ";
 
-
-      // if (subproof[0][1] == t3) {
-      Debug("pf::array") << "Dont need symmetry!" << std::endl;
-      out << ss.str();
-      // } else {
-      //   Debug("pf::array") << "Need symmetry!" << std::endl;
-      //   out << "(negsymm _ _ _ " << ss.str() << ")";
-      // }
+      if (side != 0) {
+        out << "(negsymm _ _ _ " << ss.str() << ")";
+      } else {
+        out << ss.str();
+      }
 
       out << ")";
 
-      // Unreachable();
+      if (swap) {
+        out << ") ";
+      }
 
       return ret;
     }
@@ -1071,13 +1117,12 @@ void ArrayProof::registerTerm(Expr term) {
 }
 
 std::string ArrayProof::skolemToLiteral(Expr skolem) {
+  Debug("pf::array") << "ArrayProof::skolemToLiteral( " << skolem << ")" << std::endl;
   Assert(d_skolemToLiteral.find(skolem) != d_skolemToLiteral.end());
   return d_skolemToLiteral[skolem];
 }
 
 void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
-  Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedTerm: term = " << term << std::endl;
-
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY);
 
   if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) {
@@ -1154,7 +1199,21 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& m
 void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
   Assert (type.isArray() || type.isSort());
-  os << type <<" ";
+  if (type.isArray()){
+    ArrayType array_type(type);
+
+    Debug("pf::array") << "LFSCArrayProof::printOwnedSort: type is an array. Index type: "
+                       << array_type.getIndexType()
+                       << ", element type: " << array_type.getConstituentType() << std::endl;
+
+    os << "(Array ";
+    printSort(array_type.getIndexType(), os);
+    os << " ";
+    printSort(array_type.getConstituentType(), os);
+    os << ")";
+  } else {
+    os << type <<" ";
+  }
 }
 
 void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
@@ -1169,8 +1228,6 @@ void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostrea
 
 void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
   // declaring the sorts
-  Debug("pf::array") << "Arrays declaring sorts..." << std::endl;
-
   for (TypeSet::const_iterator it = d_sorts.begin(); it != d_sorts.end(); ++it) {
     if (!ProofManager::currentPM()->wasPrinted(*it)) {
       os << "(% " << *it << " sort\n";
@@ -1229,6 +1286,7 @@ void LFSCArrayProof::printTermDeclarations(std::ostream& os, std::ostream& paren
 void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
   Debug("pf::array") << "Array: print deferred declarations called" << std::endl;
 
+  unsigned count = 1;
   for (ExprSet::const_iterator it = d_skolemDeclarations.begin(); it != d_skolemDeclarations.end(); ++it) {
     Expr term = *it;
     Node equality = ProofManager::getSkolemizationManager()->getDisequality(*it);
@@ -1237,7 +1295,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
                        << "It is a witness for: " << equality << std::endl;
 
     std::ostringstream newSkolemLiteral;
-    newSkolemLiteral << ".sl" << d_skolemToLiteral.size();
+    newSkolemLiteral << ".sl" << count++;
     std::string skolemLiteral = newSkolemLiteral.str();
 
     d_skolemToLiteral[*it] = skolemLiteral;
@@ -1251,13 +1309,12 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
     Node array_two = equality[0][1];
 
     LetMap map;
-
     os << "(ext _ _ ";
     printTerm(array_one.toExpr(), os, map);
     os << " ";
     printTerm(array_two.toExpr(), os, map);
     os << " (\\ ";
-    printTerm(*it, os, map);
+    os << ProofManager::sanitize(*it);
     os << " (\\ ";
     os << skolemLiteral.c_str();
     os << "\n";
@@ -1266,4 +1323,8 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
   }
 }
 
+void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+    // Nothing to do here at this point.
+}
+
 } /* CVC4  namespace */
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index fb25c9433..076ba7381 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -30,6 +30,32 @@ namespace CVC4 {
 //proof object outputted by TheoryARRAY
 class ProofArray : public Proof {
 private:
+  class ArrayProofPrinter : public theory::eq::EqProof::PrettyPrinter {
+  public:
+    ArrayProofPrinter() : d_row(0), d_row1(0), d_ext(0) {
+    }
+
+    std::string printTag(unsigned tag) {
+      if (tag == theory::eq::MERGED_THROUGH_CONGRUENCE) return "Congruence";
+      if (tag == theory::eq::MERGED_THROUGH_EQUALITY) return "Pure Equality";
+      if (tag == theory::eq::MERGED_THROUGH_REFLEXIVITY) return "Reflexivity";
+      if (tag == theory::eq::MERGED_THROUGH_CONSTANTS) return "Constants";
+      if (tag == theory::eq::MERGED_THROUGH_TRANS) return "Transitivity";
+
+      if (tag == d_row) return "Read Over Write";
+      if (tag == d_row1) return "Read Over Write (1)";
+      if (tag == d_ext) return "Extensionality";
+
+      std::ostringstream result;
+      result << tag;
+      return result.str();
+    }
+
+    unsigned d_row;
+    unsigned d_row1;
+    unsigned d_ext;
+  };
+
   Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
                        theory::eq::EqProof* pf,
                        unsigned tb,
@@ -41,6 +67,8 @@ private:
   unsigned d_reasonRow1;
   /** Merge tag for EXT applications */
   unsigned d_reasonExt;
+
+  ArrayProofPrinter d_proofPrinter;
 public:
   ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {}
   //it is simply an equality engine proof
@@ -53,6 +81,10 @@ public:
   void setRowMergeTag(unsigned tag);
   void setRow1MergeTag(unsigned tag);
   void setExtMergeTag(unsigned tag);
+
+  unsigned getRowMergeTag() const;
+  unsigned getRow1MergeTag() const;
+  unsigned getExtMergeTag() const;
 };
 
 namespace theory {
@@ -91,6 +123,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
 };
 
 
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index b63782226..479266db4 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -15,9 +15,11 @@
 
 **/
 
-#include "proof/bitvector_proof.h"
 #include "options/bv_options.h"
+#include "proof/array_proof.h"
+#include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
+#include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof_implementation.h"
 #include "prop/bvminisat/bvminisat.h"
@@ -80,20 +82,40 @@ BVSatProof* BitVectorProof::getSatProof() {
 }
 
 void BitVectorProof::registerTermBB(Expr term) {
+  Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl;
+
   if (d_seenBBTerms.find(term) != d_seenBBTerms.end())
     return;
 
   d_seenBBTerms.insert(term);
   d_bbTerms.push_back(term);
+
+  // If this term gets used in the final proof, we will want to register it. However,
+  // we don't know this at this point; and when the theory proof engine sees it, if it belongs
+  // to another theory, it won't register it with this proof. So, we need to tell the
+  // engine to inform us.
+
+  if (theory::Theory::theoryOf(term) != theory::THEORY_BV) {
+    Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl;
+    d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV);
+  }
 }
 
 void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
+  Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl;
+
   Expr def = atom.iffExpr(atom_bb);
-   d_bbAtoms.insert(std::make_pair(atom, def));
+  d_bbAtoms.insert(std::make_pair(atom, def));
   registerTerm(atom);
+
+  // Register the atom's terms for bitblasting
+  registerTermBB(atom[0]);
+  registerTermBB(atom[1]);
 }
 
 void BitVectorProof::registerTerm(Expr term) {
+  Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl;
+
   d_usedBB.insert(term);
 
   if (Theory::isLeafOf(term, theory::THEORY_BV) &&
@@ -101,6 +123,11 @@ void BitVectorProof::registerTerm(Expr term) {
     d_declarations.insert(term);
   }
 
+  Debug("pf::bv") << "Going to register children: " << std::endl;
+  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+    Debug("pf::bv") << "\t" << term[i] << std::endl;
+  }
+
   // don't care about parametric operators for bv?
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
      d_proofEngine->registerTerm(term[i]);
@@ -108,6 +135,7 @@ void BitVectorProof::registerTerm(Expr term) {
 }
 
 std::string BitVectorProof::getBBTermName(Expr expr) {
+  Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl;
   std::ostringstream os;
   os << "bt"<< expr.getId();
   return os.str();
@@ -122,6 +150,8 @@ void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit lit) {
 }
 
 void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) {
+  Debug("pf::bv") << "BitVectorProof::endBVConflict called" << std::endl;
+
   std::vector<Expr> expr_confl;
   for (int i = 0; i < confl.size(); ++i) {
     prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]);
@@ -129,6 +159,7 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl
     Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
     expr_confl.push_back(expr_lit);
   }
+
   Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl);
   Debug("pf::bv") << "Make conflict for " << conflict << std::endl;
 
@@ -144,25 +175,99 @@ void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl
   ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl);
   d_bbConflictMap[conflict] = clause_id;
   d_resolutionProof->endResChain(clause_id);
-  Debug("pf::bv") << "BitVectorProof::endBVConflict id"<<clause_id<< " => " << conflict << "\n";
+  Debug("pf::bv") << "BitVectorProof::endBVConflict id" <<clause_id<< " => " << conflict << "\n";
   d_isAssumptionConflict = false;
 }
 
 void BitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) {
+
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     Debug("pf::bv") << "Construct full proof." << std::endl;
     d_resolutionProof->constructProof();
     return;
   }
-  for(unsigned i = 0; i < conflicts.size(); ++i) {
+
+  for (unsigned i = 0; i < conflicts.size(); ++i) {
     Expr confl = conflicts[i];
-    Debug("pf::bv") << "Finalize conflict " << confl << std::endl;
-    //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end());
-    if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){
+    Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl;
+
+    // Special case: if the conflict has a (true) or a (not false) in it, it is trivial...
+    bool ignoreConflict = false;
+    if ((confl.isConst() && confl.getConst<bool>()) ||
+        (confl.getKind() == kind::NOT && confl[0].isConst() && !confl[0].getConst<bool>())) {
+      ignoreConflict = true;
+    } else if (confl.getKind() == kind::OR) {
+      for (unsigned k = 0; k < confl.getNumChildren(); ++k) {
+        if ((confl[k].isConst() && confl[k].getConst<bool>()) ||
+            (confl[k].getKind() == kind::NOT && confl[k][0].isConst() && !confl[k][0].getConst<bool>())) {
+          ignoreConflict = true;
+        }
+      }
+    }
+    if (ignoreConflict) {
+      Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" << std::endl;
+      continue;
+    }
+
+    if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) {
       ClauseId id = d_bbConflictMap[confl];
       d_resolutionProof->collectClauses(id);
-    }else{
-      Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl;
+    } else {
+      // There is no exact match for our conflict, but maybe it is a subset of another conflict
+      ExprToClauseId::const_iterator it;
+      bool matchFound = false;
+      for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+        Expr possibleMatch = it->first;
+        if (possibleMatch.getKind() != kind::OR) {
+          // This is a single-node conflict. If this node is in the conflict we're trying to prove,
+          // we have a match.
+          for (unsigned k = 0; k < confl.getNumChildren(); ++k) {
+            if (confl[k] == possibleMatch) {
+              matchFound = true;
+              d_resolutionProof->collectClauses(it->second);
+              break;
+            }
+          }
+        } else {
+          if (possibleMatch.getNumChildren() > confl.getNumChildren())
+            continue;
+
+          unsigned k = 0;
+          bool matching = true;
+          for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) {
+            // j is the index in possibleMatch
+            // k is the index in confl
+            while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) {
+              ++k;
+            }
+            if (k == confl.getNumChildren()) {
+              // We couldn't find a match for possibleMatch[j], so not a match
+              matching = false;
+              break;
+            }
+          }
+
+          if (matching) {
+            Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl;
+            d_resolutionProof->collectClauses(it->second);
+            matchFound = true;
+            break;
+          }
+        }
+      }
+
+      if (!matchFound) {
+        Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl
+                        << "Dumping existing conflicts:" << std::endl;
+
+        i = 0;
+        for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+          ++i;
+          Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
+        }
+
+        Unreachable();
+      }
     }
   }
 }
@@ -238,11 +343,25 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa
     printBitOf(term, os, map);
     return;
   }
-  case kind::VARIABLE:
+
+  case kind::VARIABLE: {
+    os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")";
+    return;
+  }
+
   case kind::SKOLEM: {
-    os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")";
+
+    // TODO: we need to distinguish between "real" skolems (e.g. from array) and "fake" skolems,
+    // like ITE terms. Is there a more elegant way?
+
+    if (ProofManager::getSkolemizationManager()->isSkolem(term)) {
+      os << ProofManager::sanitize(term);
+    } else {
+      os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")";
+    }
     return;
   }
+
   default:
     Unreachable();
   }
@@ -258,14 +377,7 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& m
                   << ", var = " << var << std::endl;
 
   os << "(bitof ";
-  if (var.getKind() == kind::VARIABLE || var.getKind() == kind::SKOLEM) {
-    // If var is "simple", we can just sanitize and print
-    os << ProofManager::sanitize(var);
-  } else {
-    // If var is "complex", it can belong to another theory. Therefore, dispatch again.
-    d_proofEngine->printBoundTerm(var, os, map);
-  }
-
+  os << d_exprToVariableName[var];
   os << " " << bit << ")";
 }
 
@@ -349,14 +461,16 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co
 
 void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl;
-
   Assert (type.isBitVector());
   unsigned width = utils::getSize(type);
   os << "(BitVec "<<width<<")";
 }
 
 void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+  Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl;
   Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
+  Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
+
   if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) {
     std::ostringstream lemma_paren;
     for (unsigned i = 0; i < lemma.size(); ++i) {
@@ -377,7 +491,7 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os
       // print corresponding literal in bv sat solver
       prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
       os << pm->getAtomName(bb_var, "bb");
-      os <<"(\\unit"<<bb_var<<"\n";
+      os <<"(\\ unit"<<bb_var<<"\n";
       lemma_paren <<")";
     }
     Expr lem = utils::mkOr(lemma);
@@ -386,11 +500,120 @@ void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::os
     d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren);
     os <<lemma_paren.str();
   } else {
-    Unreachable(); // If we were to reach here, we would crash because BV replay is currently not supported
-                   // in TheoryProof::printTheoryLemmaProof()
 
-    Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl;
-    BitVectorProof::printTheoryLemmaProof( lemma, os, paren );
+    Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching sub-conflict..."
+                    << std::endl;
+
+    bool matching;
+
+    ExprToClauseId::const_iterator it;
+    unsigned i = 0;
+    for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+      // Our conflict is sorted, and the records are also sorted.
+      ++i;
+      Expr possibleMatch = it->first;
+
+      if (possibleMatch.getKind() != kind::OR) {
+        // This is a single-node conflict. If this node is in the conflict we're trying to prove,
+        // we have a match.
+        matching = false;
+
+        for (unsigned k = 0; k < conflict.getNumChildren(); ++k) {
+          if (conflict[k] == possibleMatch) {
+            matching = true;
+            break;
+          }
+        }
+      } else {
+        if (possibleMatch.getNumChildren() > conflict.getNumChildren())
+          continue;
+
+        unsigned k = 0;
+
+        matching = true;
+        for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) {
+          // j is the index in possibleMatch
+          // k is the index in conflict
+          while (k < conflict.getNumChildren() && conflict[k] != possibleMatch[j]) {
+            ++k;
+          }
+          if (k == conflict.getNumChildren()) {
+            // We couldn't find a match for possibleMatch[j], so not a match
+            matching = false;
+            break;
+          }
+        }
+      }
+
+      if (matching) {
+        Debug("pf::bv") << "Found a match with conflict #" << i << ": " << std::endl << possibleMatch << std::endl;
+        // The rest is just a copy of the usual handling, if a precise match is found.
+        // We only use the literals that appear in the matching conflict, though, and not in the
+        // original lemma - as these may not have even been bit blasted!
+        std::ostringstream lemma_paren;
+
+        if (possibleMatch.getKind() == kind::OR) {
+          for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) {
+            Expr lit = possibleMatch[i];
+
+            if (lit.getKind() == kind::NOT) {
+              os << "(intro_assump_t _ _ _ ";
+            } else {
+              os << "(intro_assump_f _ _ _ ";
+            }
+            lemma_paren <<")";
+            // print corresponding literal in main sat solver
+            ProofManager* pm = ProofManager::currentPM();
+            CnfProof* cnf = pm->getCnfProof();
+            prop::SatLiteral main_lit = cnf->getLiteral(lit);
+            os << pm->getLitName(main_lit);
+            os <<" ";
+            // print corresponding literal in bv sat solver
+            prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
+            os << pm->getAtomName(bb_var, "bb");
+            os <<"(\\ unit"<<bb_var<<"\n";
+            lemma_paren <<")";
+          }
+        } else {
+          // The conflict only consists of one node, either positive or negative.
+          Expr lit = possibleMatch;
+          if (lit.getKind() == kind::NOT) {
+            os << "(intro_assump_t _ _ _ ";
+          } else {
+            os << "(intro_assump_f _ _ _ ";
+          }
+          lemma_paren <<")";
+          // print corresponding literal in main sat solver
+          ProofManager* pm = ProofManager::currentPM();
+          CnfProof* cnf = pm->getCnfProof();
+          prop::SatLiteral main_lit = cnf->getLiteral(lit);
+          os << pm->getLitName(main_lit);
+          os <<" ";
+          // print corresponding literal in bv sat solver
+          prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable();
+          os << pm->getAtomName(bb_var, "bb");
+          os <<"(\\ unit"<<bb_var<<"\n";
+          lemma_paren <<")";
+        }
+
+        ClauseId lemma_id = it->second;
+        d_resolutionProof->printAssumptionsResolution(lemma_id, os, lemma_paren);
+        os <<lemma_paren.str();
+
+        return;
+      }
+    }
+
+    Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl
+                    << "Dumping existing conflicts:" << std::endl;
+
+    i = 0;
+    for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) {
+      ++i;
+      Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl;
+    }
+
+    Unreachable();
   }
 }
 
@@ -402,7 +625,13 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p
   ExprSet::const_iterator it = d_declarations.begin();
   ExprSet::const_iterator end = d_declarations.end();
   for (; it != end; ++it) {
-    os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n";
+    if ((it->isVariable() || it->isConst()) && !ProofManager::getSkolemizationManager()->isSkolem(*it)) {
+      d_exprToVariableName[*it] = ProofManager::sanitize(*it);
+    } else {
+      d_exprToVariableName[*it] = assignAlias(*it);
+    }
+
+    os << "(% " << d_exprToVariableName[*it] <<" var_bv" << "\n";
     paren <<")";
   }
 }
@@ -411,15 +640,43 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea
   // Nothing to do here at this point.
 }
 
+void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+  // Print "trust" statements to bind complex bv variables to their associated terms
+
+  ExprToString::const_iterator it = d_assignedAliases.begin();
+  ExprToString::const_iterator end = d_assignedAliases.end();
+
+  for (; it != end; ++it) {
+    Debug("pf::bv") << "Printing aliasing declaration for: " << *it << std::endl;
+    std::stringstream declaration;
+    declaration << ".fbvd" << d_aliasToBindDeclaration.size();
+    d_aliasToBindDeclaration[it->second] = declaration.str();
+
+    os << "(th_let_pf _ ";
+
+    os << "(trust_f ";
+    os << "(= (BitVec " << utils::getSize(it->first) << ") ";
+    os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") ";
+    LetMap emptyMap;
+    d_proofEngine->printBoundTerm(it->first, os, emptyMap);
+    os << ")) ";
+    os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n";
+    paren << "))";
+  }
+
+  os << "\n";
+}
+
 void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   // TODO: once we have the operator elimination rules remove those that we
   // eliminated
   Assert (term.getType().isBitVector());
   Kind kind = term.getKind();
 
-  if (Theory::isLeafOf(term, theory::THEORY_BV) &&
-      !term.isConst()) {
-    os << "(bv_bbl_var "<<utils::getSize(term) << " " << ProofManager::sanitize(term) <<" _ )";
+  if (Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) {
+    // A term is a leaf if it has no children, or if it belongs to another theory
+    os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term];
+    os << " _ )";
     return;
   }
 
@@ -448,37 +705,60 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   case kind::BITVECTOR_PLUS :
   case kind::BITVECTOR_SUB :
   case kind::BITVECTOR_CONCAT : {
-    for (unsigned i =0; i < term.getNumChildren() - 1; ++i) {
+    Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
+
+    for (int i = term.getNumChildren() - 1; i > 0; --i) {
       os <<"(bv_bbl_"<< utils::toLFSCKind(kind);
+
+      if (i > 1) {
+        // This is not the inner-most operation; only child i+1 can be aliased
+        if (hasAlias(term[i])) {os << "_alias_2";}
+      } else {
+        // This is the inner-most operation; both children can be aliased
+        if (hasAlias(term[i-1]) || hasAlias(term[i])) {os << "_alias";}
+        if (hasAlias(term[i-1])) {os << "_1";}
+        if (hasAlias(term[i])) {os << "_2";}
+      }
+
       if (kind == kind::BITVECTOR_CONCAT) {
-        os << " " << utils::getSize(term) <<" _ ";
+        os << " " << utils::getSize(term) << " _";
       }
-      os <<" _ _ _ _ _ _ ";
+      os << " _ _ _ _ _ _ ";
     }
-    os << getBBTermName(term[0]) <<" ";
+
+    if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
+    os << getBBTermName(term[0]) << " ";
 
     for (unsigned i = 1; i < term.getNumChildren(); ++i) {
+      if (hasAlias(term[i])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[i]]] << " ";}
       os << getBBTermName(term[i]);
       os << ") ";
     }
     return;
   }
+
   case kind::BITVECTOR_NEG :
   case kind::BITVECTOR_NOT :
   case kind::BITVECTOR_ROTATE_LEFT :
   case kind::BITVECTOR_ROTATE_RIGHT : {
-    os <<"(bv_bbl_"<<utils::toLFSCKind(kind);
-    os <<" _ _ _ _ ";
+    os << "(bv_bbl_"<<utils::toLFSCKind(kind);
+    os << " _ _ _ _ ";
     os << getBBTermName(term[0]);
-    os <<")";
+    os << ")";
     return;
   }
   case kind::BITVECTOR_EXTRACT : {
-    os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
-    os << utils::getSize(term) << " ";
+    os <<"(bv_bbl_"<<utils::toLFSCKind(kind);
+
+    if (hasAlias(term[0])) {os << "_alias";};
+
+    os << " " << utils::getSize(term) << " ";
     os << utils::getExtractHigh(term) << " ";
     os << utils::getExtractLow(term) << " ";
     os << " _ _ _ _ ";
+
+    if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
+
     os << getBBTermName(term[0]);
     os <<")";
     return;
@@ -486,7 +766,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   case kind::BITVECTOR_REPEAT :
   case kind::BITVECTOR_ZERO_EXTEND :
   case kind::BITVECTOR_SIGN_EXTEND : {
-    os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
+    os <<"(bv_bbl_" <<utils::toLFSCKind(kind) << (hasAlias(term[0]) ? "_alias " : " ");
     os << utils::getSize(term) <<" ";
     if (term.getKind() == kind::BITVECTOR_REPEAT) {
       unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
@@ -501,7 +781,9 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
       unsigned amount = term.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
       os << amount;
     }
+
     os <<" _ _ _ _ ";
+    if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
     os << getBBTermName(term[0]);
     os <<")";
     return;
@@ -539,7 +821,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   }
 }
 
-void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) {
+void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) {
   Kind kind = atom.getKind();
   switch(kind) {
   case kind::BITVECTOR_ULT :
@@ -550,11 +832,28 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) {
   case kind::BITVECTOR_SLE :
   case kind::BITVECTOR_SGT :
   case kind::BITVECTOR_SGE :
-  case kind::EQUAL:
-    {
-    os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind());
+  case kind::EQUAL: {
+    Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
+
+    os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind());
+
+    if (hasAlias(atom[0]) || hasAlias(atom[1])) {os << "_alias";}
+    if (hasAlias(atom[0])) {os << "_1";}
+    if (hasAlias(atom[1])) {os << "_2";}
+
+    if (swap) {os << "_swap";}
+
     os << " _ _ _ _ _ _ ";
-    os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")";
+
+    if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";}
+    os << getBBTermName(atom[0]);
+
+    os << " ";
+
+    if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";}
+    os << getBBTermName(atom[1]);
+
+    os << ")";
     return;
   }
   default:
@@ -562,19 +861,53 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) {
   }
 }
 
+void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) {
+  Assert(atom.getKind() == kind::EQUAL);
+
+  os << "(bv_bbl_=_false";
+  os << " _ _ _ _ _ _ ";
+  if (hasAlias(atom[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[0]]] << " ";}
+  os << getBBTermName(atom[0]);
+
+  os << " ";
+
+  if (hasAlias(atom[1])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[atom[1]]] << " ";}
+  os << getBBTermName(atom[1]);
+
+  os << ")";
+}
 
 void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) {
   // bit-blast terms
+  {
+    Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl;
+    std::vector<Expr>::const_iterator it = d_bbTerms.begin();
+    std::vector<Expr>::const_iterator end = d_bbTerms.end();
+
+    Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
+
+    for (; it != end; ++it) {
+      if (d_usedBB.find(*it) == d_usedBB.end()) {
+        Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl;
+      } else {
+        Debug("pf::bv") << "\t" << *it << std::endl;
+      }
+    }
+
+    Debug("pf::bv") << std::endl;
+  }
+
   std::vector<Expr>::const_iterator it = d_bbTerms.begin();
   std::vector<Expr>::const_iterator end = d_bbTerms.end();
   for (; it != end; ++it) {
     if (d_usedBB.find(*it) == d_usedBB.end() &&
         options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER)
       continue;
-    os <<"(decl_bblast _ _ _ ";
+
+    os << "(decl_bblast _ _ _ ";
     printTermBitblasting(*it, os);
-    os << "(\\ "<< getBBTermName(*it);
-    paren <<"\n))";
+    os << "(\\ "<< getBBTermName(*it) << "\n";
+    paren << "))";
   }
   // bit-blast atoms
   ExprToExpr::const_iterator ait = d_bbAtoms.begin();
@@ -589,7 +922,35 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
       bool val = ait->first.getConst<bool>();
       os << "(iff_symm " << (val ? "true" : "false" ) << ")";
     } else {
-      printAtomBitblasting(ait->first, os);
+      Assert(ait->first == ait->second[0]);
+
+      bool swap = false;
+      if (ait->first.getKind() == kind::EQUAL) {
+        Expr bitwiseEquivalence = ait->second[1];
+        if ((bitwiseEquivalence.getKind() == kind::CONST_BOOLEAN) && !bitwiseEquivalence.getConst<bool>()) {
+          printAtomBitblastingToFalse(ait->first, os);
+        } else {
+          if (bitwiseEquivalence.getKind() != kind::AND) {
+            // Just one bit
+            if (bitwiseEquivalence.getNumChildren() > 0 && bitwiseEquivalence[0].getKind() == kind::BITVECTOR_BITOF) {
+              swap = (ait->first[1] == bitwiseEquivalence[0][0]);
+            }
+          } else {
+            // Multiple bits
+            if (bitwiseEquivalence[0].getNumChildren() > 0 &&
+                bitwiseEquivalence[0][0].getKind() == kind::BITVECTOR_BITOF) {
+              swap = (ait->first[1] == bitwiseEquivalence[0][0][0]);
+            } else if (bitwiseEquivalence[0].getNumChildren() > 0 &&
+                       bitwiseEquivalence[0][1].getKind() == kind::BITVECTOR_BITOF) {
+              swap = (ait->first[0] == bitwiseEquivalence[0][1][0]);
+            }
+          }
+
+          printAtomBitblasting(ait->first, os, swap);
+        }
+      } else {
+        printAtomBitblasting(ait->first, os, swap);
+      }
     }
 
     os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n";
@@ -606,25 +967,53 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
                                         used_lemmas);
   Assert (used_lemmas.empty());
 
+  IdToSatClause::iterator it2;
+  Debug("pf::bv") << std::endl << "BV Used inputs: " << std::endl;
+  for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
+    Debug("pf::bv") << "\t input = " << *(it2->second) << std::endl;
+  }
+  Debug("pf::bv") << std::endl;
+
   // print mapping between theory atoms and internal SAT variables
-  os << ";; BB atom mapping\n";
+  os << std::endl << ";; BB atom mapping\n" << std::endl;
+
+  std::set<Node> atoms;
+  d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
 
-  NodeSet atoms;
-  d_cnfProof->collectAtomsForClauses(used_inputs,atoms);
+  std::set<Node>::iterator atomIt;
+  Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl;
+  for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
+    Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl;
+  }
+  Debug("pf::bv") << std::endl;
 
   // first print bit-blasting
   printBitblasting(os, paren);
 
   // print CNF conversion proof for bit-blasted facts
   d_cnfProof->printAtomMapping(atoms, os, paren);
-  os << ";; Bit-blasting definitional clauses \n";
+  os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
   for (IdToSatClause::iterator it = used_inputs.begin();
        it != used_inputs.end(); ++it) {
     d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren);
   }
 
-  os << ";; Bit-blasting learned clauses \n";
+  os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl;
   d_resolutionProof->printResolutions(os, paren);
 }
 
+std::string LFSCBitVectorProof::assignAlias(Expr expr) {
+  static unsigned counter = 0;
+  Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end());
+  std::stringstream ss;
+  ss << "fbv" << counter++;
+  Debug("pf::bv") << "assignAlias( " << expr << ") = " << ss.str() << std::endl;
+  d_assignedAliases[expr] = ss.str();
+  return ss.str();
+}
+
+bool LFSCBitVectorProof::hasAlias(Expr expr) {
+  return d_assignedAliases.find(expr) != d_assignedAliases.end();
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4a1f4015d..4e5e98541 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -60,6 +60,7 @@ typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
 typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
 typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId;
 typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr;
+typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString;
 
 class BitVectorProof : public TheoryProof {
 protected:
@@ -108,7 +109,8 @@ public:
   virtual void registerTerm(Expr term);
 
   virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
-  virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0;
+  virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0;
+  virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0;
 
   virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
   virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0;
@@ -123,6 +125,12 @@ class LFSCBitVectorProof: public BitVectorProof {
   void printPredicate(Expr term, std::ostream& os, const LetMap& map);
   void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map);
   void printBitOf(Expr term, std::ostream& os, const LetMap& map);
+
+  ExprToString d_exprToVariableName;
+  ExprToString d_assignedAliases;
+  std::map<std::string, std::string> d_aliasToBindDeclaration;
+  std::string assignAlias(Expr expr);
+  bool hasAlias(Expr expr);
 public:
   LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
     :BitVectorProof(bv, proofEngine)
@@ -130,11 +138,13 @@ public:
   virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
   virtual void printTermBitblasting(Expr term, std::ostream& os);
-  virtual void printAtomBitblasting(Expr term, std::ostream& os);
+  virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
+  virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printBitblasting(std::ostream& os, std::ostream& paren);
   virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
 };
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 19e9cbac9..abe48e3cd 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -19,6 +19,7 @@
 
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
+#include "proof/proof_utils.h"
 #include "proof/theory_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
@@ -32,7 +33,6 @@ CnfProof::CnfProof(prop::CnfStream* stream,
   : d_cnfStream(stream)
   , d_clauseToAssertion(ctx)
   , d_assertionToProofRule(ctx)
-  , d_clauseIdToOwnerTheory(ctx)
   , d_currentAssertionStack()
   , d_currentDefinitionStack()
   , d_clauseToDefinition(ctx)
@@ -103,7 +103,6 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) {
 
   setClauseAssertion(clause, current_assertion);
   setClauseDefinition(clause, current_expr);
-  registerExplanationLemma(clause);
 }
 
 void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
@@ -143,16 +142,15 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) {
   d_assertionToProofRule.insert(assertion, reason);
 }
 
-void CnfProof::registerExplanationLemma(ClauseId clauseId) {
-  d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory());
+LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) {
+  Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end());
+  return d_lemmaToProofRecipe[lemma];
 }
 
-theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) {
-  Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end());
-  return d_clauseIdToOwnerTheory[clause];
+bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) {
+  return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end();
 }
 
-
 void CnfProof::setCnfDependence(Node from, Node to) {
   Debug("proof:cnf") << "CnfProof::setCnfDependence "
                      << "from " << from  << std::endl
@@ -183,12 +181,10 @@ Node CnfProof::getCurrentAssertion() {
   return d_currentAssertionStack.back();
 }
 
-void CnfProof::setExplainerTheory(theory::TheoryId theory) {
-  d_explainerTheory = theory;
-}
-
-theory::TheoryId CnfProof::getExplainerTheory() {
-  return d_explainerTheory;
+void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) {
+  Assert(proofRecipe);
+  Assert(proofRecipe->getNumSteps() > 0);
+  d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe;
 }
 
 void CnfProof::pushCurrentDefinition(Node definition) {
@@ -212,22 +208,19 @@ Node CnfProof::getCurrentDefinition() {
   return d_currentDefinitionStack.back();
 }
 
-
 Node CnfProof::getAtom(prop::SatVariable var) {
   prop::SatLiteral lit (var);
   Node node = d_cnfStream->getNode(lit);
   return node;
 }
 
-
 void CnfProof::collectAtoms(const prop::SatClause* clause,
-                            NodeSet& atoms) {
+                            std::set<Node>& atoms) {
   for (unsigned i = 0; i < clause->size(); ++i) {
     prop::SatLiteral lit = clause->operator[](i);
     prop::SatVariable var = lit.getSatVariable();
     TNode atom = getAtom(var);
     if (atoms.find(atom) == atoms.end()) {
-      Assert (atoms.find(atom) == atoms.end());
       atoms.insert(atom);
     }
   }
@@ -237,14 +230,75 @@ prop::SatLiteral CnfProof::getLiteral(TNode atom) {
   return d_cnfStream->getLiteral(atom);
 }
 
+bool CnfProof::hasLiteral(TNode atom) {
+  return d_cnfStream->hasLiteral(atom);
+}
+
+void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) {
+  d_cnfStream->ensureLiteral(atom, noPreregistration);
+}
+
 void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses,
-                                       NodeSet& atom_map) {
+                                      std::set<Node>& atoms) {
   IdToSatClause::const_iterator it = clauses.begin();
   for (; it != clauses.end(); ++it) {
     const prop::SatClause* clause = it->second;
-    collectAtoms(clause, atom_map);
+    collectAtoms(clause, atoms);
   }
+}
+
+void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
+                                                std::set<Node>& atoms,
+                                                NodePairSet& rewrites) {
+  IdToSatClause::const_iterator it = lemmaClauses.begin();
+  for (; it != lemmaClauses.end(); ++it) {
+    const prop::SatClause* clause = it->second;
+
+    // TODO: just calculate the map from ID to recipe once,
+    // instead of redoing this over and over again
+    std::vector<Expr> clause_expr;
+    std::set<Node> clause_expr_nodes;
+    for(unsigned i = 0; i < clause->size(); ++i) {
+      prop::SatLiteral lit = (*clause)[i];
+      Node node = getAtom(lit.getSatVariable());
+      Expr atom = node.toExpr();
+      if (atom.isConst()) {
+        Assert (atom == utils::mkTrue());
+        continue;
+      }
+      clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
+    }
+
+    LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes);
 
+    for (unsigned i = 0; i < recipe.getNumSteps(); ++i) {
+      const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i);
+      Node atom = proofStep->getLiteral();
+
+      if (atom == Node()) {
+        // The last proof step always has the empty node as its target...
+        continue;
+      }
+
+      if (atom.getKind() == kind::NOT) {
+        atom = atom[0];
+      }
+
+      atoms.insert(atom);
+    }
+
+    LemmaProofRecipe::RewriteIterator rewriteIt;
+    for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) {
+      rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second));
+
+      // The unrewritten terms also need to have literals, so insert them into atoms
+      Node rewritten = rewriteIt->first;
+      if (rewritten.getKind() == kind::NOT) {
+        rewritten = rewritten[0];
+      }
+      atoms.insert(rewritten);
+    }
+  }
 }
 
 void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
@@ -263,13 +317,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
   }
 }
 
-void LFSCCnfProof::printAtomMapping(const NodeSet& atoms,
+void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
                                     std::ostream& os,
                                     std::ostream& paren) {
-  NodeSet::const_iterator it = atoms.begin();
-  NodeSet::const_iterator end = atoms.end();
+  std::set<Node>::const_iterator it = atoms.begin();
+  std::set<Node>::const_iterator end = atoms.end();
 
-  for (;it != end;  ++it) {
+  for (;it != end; ++it) {
     os << "(decl_atom ";
     Node atom = *it;
     prop::SatVariable var = getLiteral(atom).getSatVariable();
@@ -277,8 +331,8 @@ void LFSCCnfProof::printAtomMapping(const NodeSet& atoms,
     LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
     pe->printLetTerm(atom.toExpr(), os);
 
-    os << " (\\ " << ProofManager::getVarName(var, d_name)
-       << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
+    os << " (\\ " << ProofManager::getVarName(var, d_name);
+    os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
     paren << ")))";
   }
 }
@@ -304,6 +358,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
                                           const prop::SatClause* clause,
                                           std::ostream& os,
                                           std::ostream& paren) {
+  Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting "
+                  << std::endl;
+
   os << "(satlem _ _ ";
   std::ostringstream clause_paren;
   printClause(*clause, os, clause_paren);
@@ -336,6 +393,10 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
   // and prints the proof of the top-level formula
   bool is_input = printProofTopLevel(base_assertion, os_base);
 
+  if (is_input) {
+    Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl;
+  }
+
   //get base assertion with polarity
   bool base_pol = base_assertion.getKind()!=kind::NOT;
   base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion;
@@ -564,6 +625,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
       if( !pols[0] || num_nots_1==1 ){
         os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") ";
       }else{
+        Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl;
         os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
       }
       Assert( elimNum!=0 );
@@ -662,6 +724,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
 
   os << ")" << clause_paren.str()
      << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
+
   paren << "))";
 }
 
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index a21cb1c0e..62036ced0 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -27,6 +27,7 @@
 
 #include "context/cdhashmap.h"
 #include "proof/clause_id.h"
+#include "proof/lemma_proof.h"
 #include "proof/sat_proof.h"
 #include "util/proof.h"
 
@@ -43,7 +44,9 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
 
 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
 typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
-typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory;
+typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe;
+typedef std::pair<Node, Node> NodePair;
+typedef std::set<NodePair> NodePairSet;
 
 class CnfProof {
 protected:
@@ -55,11 +58,8 @@ protected:
   /** Map from assertion to reason for adding assertion  **/
   NodeToProofRule d_assertionToProofRule;
 
-  /** Map from assertion to the theory that added this assertion  **/
-  ClauseIdToTheory d_clauseIdToOwnerTheory;
-
-  /** The last theory to explain a lemma **/
-  theory::TheoryId d_explainerTheory;
+  /** Map from lemma to the recipe for proving it **/
+  LemmaToRecipe d_lemmaToProofRecipe;
 
   /** Top of stack is assertion currently being converted to CNF **/
   std::vector<Node> d_currentAssertionStack;
@@ -91,10 +91,16 @@ public:
 
   Node getAtom(prop::SatVariable var);
   prop::SatLiteral getLiteral(TNode node);
+  bool hasLiteral(TNode node);
+  void ensureLiteral(TNode node, bool noPreregistration = false);
+
   void collectAtoms(const prop::SatClause* clause,
-                    NodeSet& atoms);
+                    std::set<Node>& atoms);
   void collectAtomsForClauses(const IdToSatClause& clauses,
-                               NodeSet& atoms);
+                              std::set<Node>& atoms);
+  void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
+                                        std::set<Node>& atoms,
+                                        NodePairSet& rewrites);
   void collectAssertionsForClauses(const IdToSatClause& clauses,
                                    NodeSet& assertions);
 
@@ -121,11 +127,9 @@ public:
   void popCurrentDefinition();
   Node getCurrentDefinition();
 
-  void setExplainerTheory(theory::TheoryId theory);
-  theory::TheoryId getExplainerTheory();
-  theory::TheoryId getOwnerTheory(ClauseId clause);
-
-  void registerExplanationLemma(ClauseId clauseId);
+  void setProofRecipe(LemmaProofRecipe* proofRecipe);
+  LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
+  bool haveProofRecipe(const std::set<Node> &lemma);
 
   // accessors for the leaf assertions that are being converted to CNF
   bool isAssertion(Node node);
@@ -134,7 +138,7 @@ public:
   Node getAssertionForClause(ClauseId clause);
 
   /** Virtual methods for printing things **/
-  virtual void printAtomMapping(const NodeSet& atoms,
+  virtual void printAtomMapping(const std::set<Node>& atoms,
                                 std::ostream& os,
                                 std::ostream& paren) = 0;
 
@@ -161,7 +165,7 @@ public:
   {}
   ~LFSCCnfProof() {}
 
-  void printAtomMapping(const NodeSet& atoms,
+  void printAtomMapping(const std::set<Node>& atoms,
                         std::ostream& os,
                         std::ostream& paren);
 
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp
new file mode 100644
index 000000000..a12a516cf
--- /dev/null
+++ b/src/proof/lemma_proof.cpp
@@ -0,0 +1,193 @@
+/*********************                                                        */
+/*! \file lemma_proof.h
+** \verbatim
+**
+** \brief A class for recoding the steps required in order to prove a theory lemma.
+**
+** A class for recoding the steps required in order to prove a theory lemma.
+**
+**/
+
+#include "proof/lemma_proof.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+LemmaProofRecipe::ProofStep::ProofStep(theory::TheoryId theory, Node literalToProve) :
+  d_theory(theory), d_literalToProve(literalToProve) {
+}
+
+theory::TheoryId LemmaProofRecipe::ProofStep::getTheory() const {
+  return d_theory;
+}
+
+Node LemmaProofRecipe::ProofStep::getLiteral() const {
+  return d_literalToProve;
+}
+
+void LemmaProofRecipe::ProofStep::addAssertion(const Node& assertion) {
+  d_assertions.insert(assertion);
+}
+
+std::set<Node> LemmaProofRecipe::ProofStep::getAssertions() const {
+  return d_assertions;
+}
+
+void LemmaProofRecipe::addStep(ProofStep& proofStep) {
+  std::list<ProofStep>::iterator existingFirstStep = d_proofSteps.begin();
+  d_proofSteps.push_front(proofStep);
+}
+
+std::set<Node> LemmaProofRecipe::getMissingAssertionsForStep(unsigned index) const {
+  Assert(index < d_proofSteps.size());
+
+  std::set<Node> existingAssertions = getBaseAssertions();
+
+  std::list<ProofStep>::const_iterator step = d_proofSteps.begin();
+  while (index != 0) {
+    existingAssertions.insert(step->getLiteral().negate());
+    ++step;
+    --index;
+  }
+
+  std::set<Node> neededAssertions = step->getAssertions();
+
+  std::set<Node> result;
+  std::set_difference(neededAssertions.begin(), neededAssertions.end(),
+                      existingAssertions.begin(), existingAssertions.end(),
+                      std::inserter(result, result.begin()));
+  return result;
+}
+
+void LemmaProofRecipe::dump(const char *tag) const {
+
+  if (d_proofSteps.size() == 1) {
+    Debug(tag) << std::endl << "[Simple lemma]" << std::endl << std::endl;
+  }
+
+  unsigned count = 1;
+  Debug(tag) << "Base assertions:" << std::endl;
+  for (std::set<Node>::iterator baseIt = d_baseAssertions.begin();
+       baseIt != d_baseAssertions.end();
+       ++baseIt) {
+    Debug(tag) << "\t#" << count << ": " << "\t" << *baseIt << std::endl;
+    ++count;
+  }
+
+  Debug(tag) << std::endl << std::endl << "Proof steps:" << std::endl;
+
+  count = 1;
+  for (std::list<ProofStep>::const_iterator step = d_proofSteps.begin(); step != d_proofSteps.end(); ++step) {
+    Debug(tag) << "\tStep #" << count << ": " << "\t[" << step->getTheory() << "] ";
+    if (step->getLiteral() == Node()) {
+      Debug(tag) << "Contradiction";
+    } else {
+      Debug(tag) << step->getLiteral();
+    }
+
+    Debug(tag) << std::endl;
+
+    std::set<Node> missingAssertions = getMissingAssertionsForStep(count - 1);
+    for (std::set<Node>::const_iterator it = missingAssertions.begin(); it != missingAssertions.end(); ++it) {
+      Debug(tag) << "\t\t\tMissing assertion for step: " << *it << std::endl;
+    }
+
+    Debug(tag) << std::endl;
+    ++count;
+  }
+
+  if (!d_assertionToExplanation.empty()) {
+    Debug(tag) << std::endl << "Rewrites used:" << std::endl;
+    count = 1;
+    for (std::map<Node, Node>::const_iterator rewrite = d_assertionToExplanation.begin();
+         rewrite != d_assertionToExplanation.end();
+         ++rewrite) {
+      Debug(tag) << "\tRewrite #" << count << ":" << std::endl
+                 << "\t\t" << rewrite->first
+                 << std::endl << "\t\trewritten into" << std::endl
+                 << "\t\t" << rewrite->second
+                 << std::endl << std::endl;
+      ++count;
+    }
+  }
+}
+
+void LemmaProofRecipe::addBaseAssertion(Node baseAssertion) {
+  d_baseAssertions.insert(baseAssertion);
+}
+
+std::set<Node> LemmaProofRecipe::getBaseAssertions() const {
+  return d_baseAssertions;
+}
+
+theory::TheoryId LemmaProofRecipe::getTheory() const {
+  Assert(d_proofSteps.size() > 0);
+  return d_proofSteps.back().getTheory();
+}
+
+void LemmaProofRecipe::addRewriteRule(Node assertion, Node explanation) {
+  if (d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end()) {
+    Assert(d_assertionToExplanation[assertion] == explanation);
+  }
+
+  d_assertionToExplanation[assertion] = explanation;
+}
+
+bool LemmaProofRecipe::wasRewritten(Node assertion) const {
+  return d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end();
+}
+
+Node LemmaProofRecipe::getExplanation(Node assertion) const {
+  Assert(d_assertionToExplanation.find(assertion) != d_assertionToExplanation.end());
+  return d_assertionToExplanation.find(assertion)->second;
+}
+
+LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteBegin() const {
+  return d_assertionToExplanation.begin();
+}
+
+LemmaProofRecipe::RewriteIterator LemmaProofRecipe::rewriteEnd() const {
+  return d_assertionToExplanation.end();
+}
+
+bool LemmaProofRecipe::operator<(const LemmaProofRecipe& other) const {
+    return d_baseAssertions < other.d_baseAssertions;
+  }
+
+bool LemmaProofRecipe::simpleLemma() const {
+  return d_proofSteps.size() == 1;
+}
+
+bool LemmaProofRecipe::compositeLemma() const {
+  return !simpleLemma();
+}
+
+const LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) const {
+  Assert(index < d_proofSteps.size());
+
+  std::list<ProofStep>::const_iterator it = d_proofSteps.begin();
+  while (index != 0) {
+    ++it;
+    --index;
+  }
+
+  return &(*it);
+}
+
+LemmaProofRecipe::ProofStep* LemmaProofRecipe::getStep(unsigned index) {
+  Assert(index < d_proofSteps.size());
+
+  std::list<ProofStep>::iterator it = d_proofSteps.begin();
+  while (index != 0) {
+    ++it;
+    --index;
+  }
+
+  return &(*it);
+}
+
+unsigned LemmaProofRecipe::getNumSteps() const {
+  return d_proofSteps.size();
+}
+
+} /* namespace CVC4 */
diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h
new file mode 100644
index 000000000..e96ff5337
--- /dev/null
+++ b/src/proof/lemma_proof.h
@@ -0,0 +1,79 @@
+/*********************                                                        */
+/*! \file lemma_proof.h
+** \verbatim
+**
+** \brief A class for recoding the steps required in order to prove a theory lemma.
+**
+** A class for recoding the steps required in order to prove a theory lemma.
+**
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__LEMMA_PROOF_H
+#define __CVC4__LEMMA_PROOF_H
+
+#include "expr/expr.h"
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+#include "util/proof.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class LemmaProofRecipe {
+public:
+  class ProofStep {
+  public:
+    ProofStep(theory::TheoryId theory, Node literalToProve);
+    theory::TheoryId getTheory() const;
+    Node getLiteral() const;
+    void addAssertion(const Node& assertion);
+    std::set<Node> getAssertions() const;
+
+  private:
+    theory::TheoryId d_theory;
+    Node d_literalToProve;
+    std::set<Node> d_assertions;
+  };
+
+  //* The lemma assertions and owner */
+  void addBaseAssertion(Node baseAssertion);
+  std::set<Node> getBaseAssertions() const;
+  theory::TheoryId getTheory() const;
+
+  //* Rewrite rules */
+  typedef std::map<Node, Node>::const_iterator RewriteIterator;
+  RewriteIterator rewriteBegin() const;
+  RewriteIterator rewriteEnd() const;
+
+  void addRewriteRule(Node assertion, Node explanation);
+  bool wasRewritten(Node assertion) const;
+  Node getExplanation(Node assertion) const;
+
+  //* Proof Steps */
+  void addStep(ProofStep& proofStep);
+  const ProofStep* getStep(unsigned index) const;
+  ProofStep* getStep(unsigned index);
+  unsigned getNumSteps() const;
+  std::set<Node> getMissingAssertionsForStep(unsigned index) const;
+  bool simpleLemma() const;
+  bool compositeLemma() const;
+
+  void dump(const char *tag) const;
+  bool operator<(const LemmaProofRecipe& other) const;
+
+private:
+  //* The list of assertions for this lemma */
+  std::set<Node> d_baseAssertions;
+
+  //* The various steps needed to derive the empty clause */
+  std::list<ProofStep> d_proofSteps;
+
+  //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */
+  std::map<Node, Node> d_assertionToExplanation;
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__LEMMA_PROOF_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index a3689d746..5ce8b523f 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -200,7 +200,6 @@ std::string ProofManager::getLitName(prop::SatLiteral lit,
   return append(prefix+".l", lit.toInt());
 }
 
-
 std::string ProofManager::getPreprocessedAssertionName(Node node,
                                                        const std::string& prefix) {
   node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node;
@@ -217,9 +216,15 @@ std::string ProofManager::getAtomName(TNode atom,
   Assert(!lit.isNegated());
   return getAtomName(lit.getSatVariable(), prefix);
 }
+
 std::string ProofManager::getLitName(TNode lit,
                                      const std::string& prefix) {
-  return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
+  std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
+  if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) {
+    return currentPM()->d_rewriteFilters[litName];
+  }
+
+  return litName;
 }
 
 std::string ProofManager::sanitize(TNode node) {
@@ -331,6 +336,9 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine,
 {}
 
 void LFSCProof::toStream(std::ostream& out) {
+
+  Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
+
   d_satProof->constructProof();
 
   // collecting leaf clauses in resolution proof
@@ -384,8 +392,37 @@ void LFSCProof::toStream(std::ostream& out) {
   for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
     Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
 
-  NodeSet atoms;
+  std::set<Node> atoms;
+  NodePairSet rewrites;
   // collects the atoms in the clauses
+  d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
+
+  if (!rewrites.empty()) {
+    Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
+    NodePairSet::const_iterator rewriteIt;
+    for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
+      Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
+    }
+    Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
+  } else {
+    Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
+  }
+
+  // The derived/unrewritten atoms may not have CNF literals required later on.
+  // If they don't, add them.
+  std::set<Node>::const_iterator it;
+  for (it = atoms.begin(); it != atoms.end(); ++it) {
+    Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
+    if (!d_cnfProof->hasLiteral(*it)) {
+      // For arithmetic: these literals are not normalized, causing an error in Arith.
+      if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
+        d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
+      } else {
+        d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
+      }
+    }
+  }
+
   d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
   d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
 
@@ -393,38 +430,23 @@ void LFSCProof::toStream(std::ostream& out) {
   for (NodeSet::const_iterator it = used_assertions.begin();
        it != used_assertions.end(); ++it) {
     utils::collectAtoms(*it, atoms);
+    // utils::collectAtoms(*it, newAtoms);
   }
 
-  NodeSet::iterator atomIt;
-  Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << std::endl;
+  std::set<Node>::iterator atomIt;
+  Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
+                  << std::endl << std::endl;
   for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
     Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
-
-    if (Debug.isOn("proof:pm")) {
-      // std::cout << NodeManager::currentNM();
-      Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl;
-      for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) {
-        Debug("proof:pm") << "   " << *it << std::endl;
-      }
-
-      Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl;
-      for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) {
-        Debug("proof:pm") << "   " << *it << std::endl;
-      }
-    }
   }
-
   smt::SmtScope scope(d_smtEngine);
   std::ostringstream paren;
   out << "(check\n";
   out << " ;; Declarations\n";
 
   // declare the theory atoms
-  NodeSet::const_iterator it = atoms.begin();
-  NodeSet::const_iterator end = atoms.end();
-
   Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
-  for(; it != end; ++it) {
+  for(it = atoms.begin(); it != atoms.end(); ++it) {
     Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
     d_theoryProof->registerTerm((*it).toExpr());
   }
@@ -444,9 +466,15 @@ void LFSCProof::toStream(std::ostream& out) {
   out << "(: (holds cln)\n\n";
 
   // Have the theory proofs print deferred declarations, e.g. for skolem variables.
-  out << " ;; Printing deferred declarations \n";
+  out << " ;; Printing deferred declarations \n\n";
   d_theoryProof->printDeferredDeclarations(out, paren);
 
+  out << " ;; Printing aliasing declarations \n\n";
+  d_theoryProof->printAliasingDeclarations(out, paren);
+
+  out << " ;; Rewrites for Lemmas \n";
+  d_theoryProof->printLemmaRewrites(rewrites, out, paren);
+
   // print trust that input assertions are their preprocessed form
   printPreprocessedAssertions(used_assertions, out, paren);
 
@@ -464,10 +492,6 @@ void LFSCProof::toStream(std::ostream& out) {
 
   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
 
-  // FIXME: for now assume all theory lemmas are in CNF form so
-  // distinguish between them and inputs
-  // print theory lemmas for resolution proof
-
   Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
   d_theoryProof->printTheoryLemmas(used_lemmas, out, paren);
   Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
@@ -496,6 +520,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
   NodeSet::const_iterator it = assertions.begin();
   NodeSet::const_iterator end = assertions.end();
 
+  Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl;
+
   for (; it != end; ++it) {
     os << "(th_let_pf _ ";
 
@@ -506,7 +532,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
     os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
     paren << "))";
-
   }
 
   os << "\n";
@@ -568,6 +593,14 @@ void ProofManager::markPrinted(const Type& type) {
   d_printedTypes.insert(type);
 }
 
+void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) {
+  d_rewriteFilters[original] = substitute;
+}
+
+void ProofManager::clearRewriteFilters() {
+  d_rewriteFilters.clear();
+}
+
 std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
   switch(k) {
   case RULE_GIVEN:
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c74aac237..c6454b652 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -34,6 +34,8 @@
 
 namespace CVC4 {
 
+class SmtGlobals;
+
 // forward declarations
 namespace Minisat {
   class Solver;
@@ -136,6 +138,8 @@ class ProofManager {
 
   std::set<Type> d_printedTypes;
 
+  std::map<std::string, std::string> d_rewriteFilters;
+
 protected:
   LogicInfo d_logic;
 
@@ -224,6 +228,9 @@ public:
   void markPrinted(const Type& type);
   bool wasPrinted(const Type& type) const;
 
+  void addRewriteFilter(const std::string &original, const std::string &substitute);
+  void clearRewriteFilters();
+
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
new file mode 100644
index 000000000..6d729db1f
--- /dev/null
+++ b/src/proof/proof_output_channel.cpp
@@ -0,0 +1,82 @@
+/*********************                                                        */
+/*! \file proof_output_channel.cpp
+** \verbatim
+** \brief [[ Add one-line brief description here ]]
+**
+** [[ Add lengthier description here ]]
+** \todo document this file
+**/
+
+#include "base/cvc4_assert.h"
+#include "proof_output_channel.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/valuation.h"
+
+namespace CVC4 {
+
+ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
+
+void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() {
+  Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
+  Assert(d_conflict.isNull());
+  Assert(!n.isNull());
+  d_conflict = n;
+  Assert(pf != NULL);
+  d_proof = pf;
+}
+
+bool ProofOutputChannel::propagate(TNode x) throw() {
+  Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl;
+  d_propagations.insert(x);
+  return true;
+}
+
+theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) throw() {
+  Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl;
+  d_lemma = n;
+  return theory::LemmaStatus(TNode::null(), 0);
+}
+
+theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) throw() {
+  AlwaysAssert(false);
+  return theory::LemmaStatus(TNode::null(), 0);
+}
+
+void ProofOutputChannel::requirePhase(TNode n, bool b) throw() {
+  Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl;
+  Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
+}
+
+bool ProofOutputChannel::flipDecision() throw() {
+  Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl;
+  AlwaysAssert(false);
+  return false;
+}
+
+void ProofOutputChannel::setIncomplete() throw() {
+  Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl;
+  AlwaysAssert(false);
+}
+
+
+MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory)
+  : d_theory(theory)
+  , d_visited() {
+}
+
+bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
+  return d_visited.find(current) != d_visited.end();
+}
+
+void MyPreRegisterVisitor::visit(TNode current, TNode parent) {
+  d_theory->preRegisterTerm(current);
+  d_visited.insert(current);
+}
+
+void MyPreRegisterVisitor::start(TNode node) {
+}
+
+void MyPreRegisterVisitor::done(TNode node) {
+}
+
+} /* namespace CVC4 */
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
new file mode 100644
index 000000000..b85af5fb5
--- /dev/null
+++ b/src/proof/proof_output_channel.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file proof_output_channel.h
+ ** \verbatim
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
+#define __CVC4__PROOF_OUTPUT_CHANNEL_H
+
+#include "theory/output_channel.h"
+
+namespace CVC4 {
+
+class ProofOutputChannel : public theory::OutputChannel {
+public:
+  Node d_conflict;
+  Proof* d_proof;
+  Node d_lemma;
+  std::set<Node> d_propagations;
+
+  ProofOutputChannel();
+
+  virtual ~ProofOutputChannel() throw() {}
+
+  void conflict(TNode n, Proof* pf) throw();
+  bool propagate(TNode x) throw();
+  theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw();
+  theory::LemmaStatus splitLemma(TNode, bool) throw();
+  void requirePhase(TNode n, bool b) throw();
+  bool flipDecision() throw();
+  void setIncomplete() throw();
+};/* class ProofOutputChannel */
+
+class MyPreRegisterVisitor {
+  theory::Theory* d_theory;
+  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
+public:
+  typedef void return_type;
+  MyPreRegisterVisitor(theory::Theory* theory);
+  bool alreadyVisited(TNode current, TNode parent);
+  void visit(TNode current, TNode parent);
+  void start(TNode node);
+  void done(TNode node);
+}; /* class MyPreRegisterVisitor */
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */
diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp
index 5b04c281d..fe0d42242 100644
--- a/src/proof/proof_utils.cpp
+++ b/src/proof/proof_utils.cpp
@@ -21,14 +21,14 @@
 namespace CVC4 {
 namespace utils {
 
-void collectAtoms(TNode node, CVC4::NodeSet& seen) {
+void collectAtoms(TNode node, std::set<Node>& seen) {
   if (seen.find(node) != seen.end())
     return;
   if (theory::Theory::theoryOf(node) != theory::THEORY_BOOL || node.isVar()) {
       seen.insert(node);
       return;
   }
-  
+
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     collectAtoms(node[i], seen);
   }
@@ -47,23 +47,23 @@ std::string toLFSCKind(Kind kind) {
 
     // bit-vector kinds
   case kind::BITVECTOR_AND :
-    return "bvand"; 
+    return "bvand";
   case kind::BITVECTOR_OR :
-    return "bvor"; 
+    return "bvor";
   case kind::BITVECTOR_XOR :
-    return "bvxor"; 
+    return "bvxor";
   case kind::BITVECTOR_NAND :
-    return "bvnand"; 
+    return "bvnand";
   case kind::BITVECTOR_NOR :
-    return "bvnor"; 
+    return "bvnor";
   case kind::BITVECTOR_XNOR :
-    return "bvxnor"; 
+    return "bvxnor";
   case kind::BITVECTOR_COMP :
-    return "bvcomp"; 
+    return "bvcomp";
   case kind::BITVECTOR_MULT :
     return "bvmul";
   case kind::BITVECTOR_PLUS :
-    return "bvadd"; 
+    return "bvadd";
   case kind::BITVECTOR_SUB :
     return "bvsub";
   case kind::BITVECTOR_UDIV :
@@ -71,49 +71,49 @@ std::string toLFSCKind(Kind kind) {
     return "bvudiv";
   case kind::BITVECTOR_UREM :
   case kind::BITVECTOR_UREM_TOTAL :
-    return "bvurem"; 
+    return "bvurem";
   case kind::BITVECTOR_SDIV :
-    return "bvsdiv"; 
+    return "bvsdiv";
   case kind::BITVECTOR_SREM :
     return "bvsrem";
   case kind::BITVECTOR_SMOD :
-    return "bvsmod"; 
+    return "bvsmod";
   case kind::BITVECTOR_SHL :
-    return "bvshl"; 
+    return "bvshl";
   case kind::BITVECTOR_LSHR :
     return "bvlshr";
   case kind::BITVECTOR_ASHR :
     return "bvashr";
   case kind::BITVECTOR_CONCAT :
-    return "concat"; 
+    return "concat";
   case kind::BITVECTOR_NEG :
-    return "bvneg"; 
+    return "bvneg";
   case kind::BITVECTOR_NOT :
-    return "bvnot"; 
+    return "bvnot";
   case kind::BITVECTOR_ROTATE_LEFT :
-    return "rotate_left"; 
+    return "rotate_left";
   case kind::BITVECTOR_ROTATE_RIGHT :
     return "rotate_right";
   case kind::BITVECTOR_ULT :
-    return "bvult"; 
+    return "bvult";
   case kind::BITVECTOR_ULE :
-    return "bvule"; 
+    return "bvule";
   case kind::BITVECTOR_UGT :
     return "bvugt";
   case kind::BITVECTOR_UGE :
     return "bvuge";
   case kind::BITVECTOR_SLT :
-    return "bvslt"; 
+    return "bvslt";
   case kind::BITVECTOR_SLE :
-    return "bvsle"; 
+    return "bvsle";
   case kind::BITVECTOR_SGT :
-    return "bvsgt"; 
+    return "bvsgt";
   case kind::BITVECTOR_SGE :
-    return "bvsge"; 
+    return "bvsge";
   case kind::BITVECTOR_EXTRACT :
-    return "extract"; 
+    return "extract";
   case kind::BITVECTOR_REPEAT :
-    return "repeat"; 
+    return "repeat";
   case kind::BITVECTOR_ZERO_EXTEND :
     return "zero_extend";
   case kind::BITVECTOR_SIGN_EXTEND :
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index da10c33a0..8c734c892 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -17,7 +17,7 @@
 
 #include "cvc4_private.h"
 
-#pragma once 
+#pragma once
 
 #include <set>
 #include <vector>
@@ -29,6 +29,9 @@ namespace CVC4 {
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 
+typedef std::pair<Node, Node> NodePair;
+typedef std::set<NodePair> NodePairSet;
+
 namespace utils {
 
 std::string toLFSCKind(Kind kind);
@@ -42,7 +45,7 @@ inline unsigned getExtractLow(Expr node) {
 }
 
 inline unsigned getSize(Type type) {
-  BitVectorType bv(type); 
+  BitVectorType bv(type);
   return bv.getSize();
 }
 
@@ -60,8 +63,8 @@ inline Expr mkFalse() {
   return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false);
 }
 inline BitVector mkBitVectorOnes(unsigned size) {
-  Assert(size > 0); 
-  return BitVector(1, Integer(1)).signExtend(size - 1); 
+  Assert(size > 0);
+  return BitVector(1, Integer(1)).signExtend(size - 1);
 }
 
 inline Expr mkExpr(Kind k , Expr expr) {
@@ -73,16 +76,16 @@ inline Expr mkExpr(Kind k , Expr e1, Expr e2) {
 inline Expr mkExpr(Kind k , std::vector<Expr>& children) {
   return NodeManager::currentNM()->toExprManager()->mkExpr(k, children);
 }
-  
-  
+
+
 inline Expr mkOnes(unsigned size) {
-  BitVector val = mkBitVectorOnes(size); 
-  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); 
+  BitVector val = mkBitVectorOnes(size);
+  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
 }
 
 inline Expr mkConst(unsigned size, unsigned int value) {
   BitVector val(size, value);
-  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val); 
+  return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
 }
 
 inline Expr mkConst(const BitVector& value) {
@@ -92,14 +95,14 @@ inline Expr mkConst(const BitVector& value) {
 inline Expr mkOr(const std::vector<Expr>& nodes) {
   std::set<Expr> all;
   all.insert(nodes.begin(), nodes.end());
-  Assert(all.size() != 0 ); 
+  Assert(all.size() != 0 );
 
   if (all.size() == 1) {
     // All the same, or just one
     return nodes[0];
   }
-  
-  
+
+
   NodeBuilder<> disjunction(kind::OR);
   std::set<Expr>::const_iterator it = all.begin();
   std::set<Expr>::const_iterator it_end = all.end();
@@ -109,23 +112,23 @@ inline Expr mkOr(const std::vector<Expr>& nodes) {
   }
 
   Node res = disjunction;
-  return res.toExpr(); 
+  return res.toExpr();
 }/* mkOr() */
 
-                 
+
 inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
   std::set<Expr> all;
   all.insert(conjunctions.begin(), conjunctions.end());
 
   if (all.size() == 0) {
-    return mkTrue(); 
+    return mkTrue();
   }
-  
+
   if (all.size() == 1) {
     // All the same, or just one
     return conjunctions[0];
   }
-  
+
 
   NodeBuilder<> conjunction(kind::AND);
   std::set<Expr>::const_iterator it = all.begin();
@@ -135,7 +138,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
     ++ it;
   }
 
-  Node res = conjunction; 
+  Node res = conjunction;
   return res.toExpr();
 }/* mkAnd() */
 
@@ -144,14 +147,14 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
   all.insert(children.begin(), children.end());
 
   if (all.size() == 0) {
-    return mkTrue(); 
+    return mkTrue();
   }
-  
+
   if (all.size() == 1) {
     // All the same, or just one
     return children[0];
   }
-  
+
 
   NodeBuilder<> res(kind);
   std::set<Expr>::const_iterator it = all.begin();
@@ -165,13 +168,13 @@ inline Expr mkSortedExpr(Kind kind, const std::vector<Expr>& children) {
 }/* mkSortedNode() */
 
 inline const bool getBit(Expr expr, unsigned i) {
-  Assert (i < utils::getSize(expr) && 
-          expr.isConst()); 
+  Assert (i < utils::getSize(expr) &&
+          expr.isConst());
   Integer bit = expr.getConst<BitVector>().extract(i, i).getValue();
-  return (bit == 1u); 
+  return (bit == 1u);
 }
 
-void collectAtoms(TNode node, NodeSet& seen);
+void collectAtoms(TNode node, std::set<Node>& seen);
 
 
 }
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 4f3330ef7..1e01e4dce 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -543,12 +543,9 @@ ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause,
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
       d_lemmaClauses.insert(newId);
-      Debug("pf::sat")
-          << "TSatProof::registerClause registering a new lemma clause: "
-          << newId << " = " << *buildClause(newId)
-          << ". Explainer theory: " << d_cnfProof->getExplainerTheory()
-          << std::endl;
-      d_cnfProof->registerExplanationLemma(newId);
+      Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: "
+                       << newId << " = " << *buildClause(newId)
+                       << std::endl;
     }
   }
 
@@ -579,12 +576,10 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit,
     }
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
-                          "lemma (UNIT CLAUSE): "
-                       << lit << ". Explainer theory: "
-                       << d_cnfProof->getExplainerTheory() << std::endl;
+      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): "
+                       << lit
+                       << std::endl;
       d_lemmaClauses.insert(newId);
-      d_cnfProof->registerExplanationLemma(newId);
     }
   }
   ClauseId id = d_unitId[toInt(lit)];
@@ -842,7 +837,7 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) {
   // clause allocator.  So reload reason ptr each time.
   const typename Solver::TClause& initial_reason = getClause(reason_ref);
   size_t current_reason_size = initial_reason.size();
-  for (int i = 0; i < current_reason_size; i++) {
+  for (size_t i = 0; i < current_reason_size; i++) {
     const typename Solver::TClause& current_reason = getClause(reason_ref);
     current_reason_size = current_reason.size();
     typename Solver::TLit l = current_reason[i];
@@ -904,7 +899,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
   // Here, the call to resolveUnit() can reallocate memory in the
   // clause allocator.  So reload conflict ptr each time.
   size_t conflict_size = getClause(conflict_ref).size();
-  for (int i = 0; i < conflict_size; ++i) {
+  for (size_t i = 0; i < conflict_size; ++i) {
     const typename Solver::TClause& conflict = getClause(conflict_ref);
     typename Solver::TLit lit = conflict[i];
     ClauseId res_id = resolveUnit(~lit);
@@ -1106,12 +1101,12 @@ void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
   }
 
   if (id == this->d_emptyClauseId) {
-    out << "(\\empty empty)";
+    out <<"(\\ empty empty)";
     return;
   }
 
-  out << "(\\" << this->clauseName(id) << "\n";  // bind to lemma name
-  paren << "))";  // closing parethesis for lemma binding and satlem
+  out << "(\\ " << this->clauseName(id) << "\n";   // bind to lemma name
+  paren << "))";                            // closing parethesis for lemma binding and satlem
 }
 
 /// LFSCSatProof class
diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h
index de510e514..b026e21c2 100644
--- a/src/proof/skolemization_manager.h
+++ b/src/proof/skolemization_manager.h
@@ -37,7 +37,6 @@ public:
   Node getSkolem(Node disequality);
   Node getDisequality(Node skolem);
   bool isSkolem(Node skolem);
-
   void clear();
 
   std::hash_map<Node, Node, NodeHashFunction>::const_iterator begin();
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 088275b3f..eaf21846b 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -25,6 +25,7 @@
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
+#include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof.h"
 #include "proof/uf_proof.h"
@@ -48,74 +49,6 @@ namespace CVC4 {
 unsigned CVC4::LetCount::counter = 0;
 static unsigned LET_COUNT = 1;
 
-//for proof replay
-class ProofOutputChannel : public theory::OutputChannel {
-public:
-  Node d_conflict;
-  Proof* d_proof;
-  Node d_lemma;
-
-  ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
-  virtual ~ProofOutputChannel() throw() {}
-
-  void conflict(TNode n, Proof* pf) throw() {
-    Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl;
-    Assert(d_conflict.isNull());
-    Assert(!n.isNull());
-    d_conflict = n;
-    Assert(pf != NULL);
-    d_proof = pf;
-  }
-  bool propagate(TNode x) throw() {
-    Trace("theory-proof-debug") << "got a propagation: " << x << std::endl;
-    return true;
-  }
-  theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() {
-    Trace("theory-proof-debug") << "new lemma: " << n << std::endl;
-    d_lemma = n;
-    return theory::LemmaStatus(TNode::null(), 0);
-  }
-  theory::LemmaStatus splitLemma(TNode, bool) throw() {
-    AlwaysAssert(false);
-    return theory::LemmaStatus(TNode::null(), 0);
-  }
-  void requirePhase(TNode n, bool b) throw() {
-    Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl;
-    Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl;
-  }
-  bool flipDecision() throw() {
-    Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl;
-    AlwaysAssert(false);
-    return false;
-  }
-  void setIncomplete() throw() {
-    Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl;
-    AlwaysAssert(false);
-  }
-};/* class ProofOutputChannel */
-
-//for proof replay
-class MyPreRegisterVisitor {
-  theory::Theory* d_theory;
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
-public:
-  typedef void return_type;
-  MyPreRegisterVisitor(theory::Theory* theory)
-  : d_theory(theory)
-  , d_visited()
-  {}
-  bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); }
-  void visit(TNode current, TNode parent) {
-    if(theory::Theory::theoryOf(current) == d_theory->getId()) {
-      //Trace("theory-proof-debug") << "preregister " << current << std::endl;
-      d_theory->preRegisterTerm(current);
-      d_visited.insert(current);
-    }
-  }
-  void start(TNode node) { }
-  void done(TNode node) { }
-}; /* class MyPreRegisterVisitor */
-
 TheoryProofEngine::TheoryProofEngine()
   : d_registrationCache()
   , d_theoryProofTable()
@@ -131,13 +64,12 @@ TheoryProofEngine::~TheoryProofEngine() {
   }
 }
 
-
 void TheoryProofEngine::registerTheory(theory::Theory* th) {
-  if( th ){
+  if (th) {
     theory::TheoryId id = th->getId();
     if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) {
 
-      Trace("theory-proof-debug") << "; register theory " << id << std::endl;
+      Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl;
 
       if (id == theory::THEORY_UF) {
         d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this);
@@ -167,19 +99,42 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
 }
 
 TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
+  // The UF theory handles queries for the Builtin theory.
+  if (id == theory::THEORY_BUILTIN) {
+    Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl;
+    id = theory::THEORY_UF;
+  }
+
   Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end());
   return d_theoryProofTable[id];
 }
 
+void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) {
+  d_exprToTheoryIds[term].insert(id);
+}
+
+void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+  LetMap emptyMap;
+
+  os << "(trust_f (not (= _ ";
+  printBoundTerm(c1, os, emptyMap);
+  os << " ";
+  printBoundTerm(c2, os, emptyMap);
+  os << ")))";
+}
+
 void TheoryProofEngine::registerTerm(Expr term) {
+  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl;
+
   if (d_registrationCache.count(term)) {
     return;
   }
-  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl;
+
+  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl;
 
   theory::TheoryId theory_id = theory::Theory::theoryOf(term);
 
-  Debug("pf::tp") << "Term's theory: " << theory_id << std::endl;
+  Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl;
 
   // don't need to register boolean terms
   if (theory_id == theory::THEORY_BUILTIN ||
@@ -193,32 +148,38 @@ void TheoryProofEngine::registerTerm(Expr term) {
 
   if (!supportedTheory(theory_id)) return;
 
+  // Register the term with its owner theory
   getTheoryProof(theory_id)->registerTerm(term);
+
+  // A special case: the array theory needs to know of every skolem, even if
+  // it belongs to another theory (e.g., a BV skolem)
+  if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) {
+    Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl;
+    getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term);
+  }
+
   d_registrationCache.insert(term);
 }
 
-theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) {
+theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* clause) {
   ProofManager* pm = ProofManager::currentPM();
 
-  Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )"
-                     << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+  std::set<Node> nodes;
+  for(unsigned i = 0; i < clause->size(); ++i) {
+    prop::SatLiteral lit = (*clause)[i];
+    Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+    Expr atom = node.toExpr();
+    if (atom.isConst()) {
+      Assert (atom == utils::mkTrue());
+      continue;
+    }
 
-  if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) {
-    Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. "
-                       << "Returning THEORY_ARITH" << std::endl;
-    return theory::THEORY_ARITH;
+    nodes.insert(lit.isNegated() ? node.notNode() : node);
   }
 
-  return pm->getCnfProof()->getOwnerTheory(id);
-
-  // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF;
-  // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV;
-  // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY;
-  // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV;
-
-  // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl;
-
-  // Unreachable();
+  // Ensure that the lemma is in the database.
+  Assert (pm->getCnfProof()->haveProofRecipe(nodes));
+  return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
 }
 
 void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
@@ -272,8 +233,6 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
 
 void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) {
   theory::TheoryId theory_id = theory::Theory::theoryOf(term);
-  Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term
-                     << ", theory_id = " << theory_id << std::endl;
 
   // boolean terms and ITEs are special because they
   // are common to all theories
@@ -315,6 +274,29 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) {
   Unreachable();
 }
 
+void LFSCTheoryProofEngine::performExtraRegistrations() {
+  ExprToTheoryIds::const_iterator it;
+  for (it = d_exprToTheoryIds.begin(); it != d_exprToTheoryIds.end(); ++it) {
+    if (d_registrationCache.count(it->first)) { // Only register if the term appeared
+      TheoryIdSet::const_iterator theoryIt;
+      for (theoryIt = it->second.begin(); theoryIt != it->second.end(); ++theoryIt) {
+        Debug("pf::tp") << "\tExtra registration of term " << it->first
+                        << " with theory: " << *theoryIt << std::endl;
+        Assert(supportedTheory(*theoryIt));
+        getTheoryProof(*theoryIt)->registerTerm(it->first);
+      }
+    }
+  }
+}
+
+void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) {
+  TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+  TheoryProofTable::const_iterator end = d_theoryProofTable.end();
+  for (; it != end; ++it) {
+    it->second->treatBoolsAsFormulas(value);
+  }
+}
+
 void LFSCTheoryProofEngine::registerTermsFromAssertions() {
   ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
   ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
@@ -322,6 +304,8 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() {
   for(; it != end; ++it) {
     registerTerm(*it);
   }
+
+  performExtraRegistrations();
 }
 
 void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
@@ -333,17 +317,43 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
 
   for (; it != end; ++it) {
     Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
-    // FIXME: merge this with counter
-    os << "(% A" << counter++ << " (th_holds ";
+    std::ostringstream name;
+    name << "A" << counter++;
+    os << "(% " << name.str() << " (th_holds ";
     printLetTerm(*it,  os);
     os << ")\n";
     paren << ")";
   }
-  //store map between assertion and counter
-  // ProofManager::currentPM()->setAssertion( *it );
+
   Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl;
 }
 
+void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren) {
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl;
+
+  NodePairSet::const_iterator it;
+
+  for (it = rewrites.begin(); it != rewrites.end(); ++it) {
+    Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl;
+
+    std::ostringstream rewriteRule;
+    rewriteRule << ".lrr" << d_assertionToRewrite.size();
+
+    LetMap emptyMap;
+    os << "(th_let_pf _ (trust_f (iff ";
+    printBoundTerm(it->second.toExpr(), os, emptyMap);
+    os << " ";
+    printBoundTerm(it->first.toExpr(), os, emptyMap);
+    os << ")) (\\ " << rewriteRule.str() << "\n";
+
+    d_assertionToRewrite[it->first] = rewriteRule.str();
+    Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl;
+    paren << "))";
+  }
+
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl << std::endl;
+}
+
 void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl;
 
@@ -378,55 +388,148 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost
   }
 }
 
-void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
-                                              std::ostream& os,
-                                              std::ostream& paren) {
-  os << " ;; Theory Lemmas \n";
-  ProofManager* pm = ProofManager::currentPM();
-  IdToSatClause::const_iterator it = lemmas.begin();
-  IdToSatClause::const_iterator end = lemmas.end();
-
-  Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl;
+void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl;
 
+  TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+  TheoryProofTable::const_iterator end = d_theoryProofTable.end();
   for (; it != end; ++it) {
-    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl;
-    ClauseId id = it->first;
-    Debug("pf::tp") << "\tLemma = " << id
-                       << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+    it->second->printAliasingDeclarations(os, paren);
   }
-  it = lemmas.begin();
+}
 
-  // BitVector theory is special case: must know all
-  // conflicts needed ahead of time for resolution
-  // proof lemmas
-  std::vector<Expr> bv_lemmas;
-  for (; it != end; ++it) {
+void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
+  Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl;
+
+  ProofManager* pm = ProofManager::currentPM();
+  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
     ClauseId id = it->first;
+    Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl;
     const prop::SatClause* clause = it->second;
+    std::set<Node> nodes;
+    for(unsigned i = 0; i < clause->size(); ++i) {
+      prop::SatLiteral lit = (*clause)[i];
+      Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+      if (node.isConst()) {
+        Assert (node.toExpr() == utils::mkTrue());
+        continue;
+      }
+      nodes.insert(lit.isNegated() ? node.notNode() : node);
+    }
+
+    LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes);
+    recipe.dump("pf::dumpLemmas");
+  }
 
-    theory::TheoryId theory_id = getTheoryForLemma(id);
-    if (theory_id != theory::THEORY_BV) continue;
+  Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl << std::endl;
+}
+
+// TODO: this function should be moved into the BV prover.
+void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) {
+  // BitVector theory is special case: must know all conflicts needed
+  // ahead of time for resolution proof lemmas
+  std::vector<Expr> bv_lemmas;
+
+  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+    const prop::SatClause* clause = it->second;
 
     std::vector<Expr> conflict;
+    std::set<Node> conflictNodes;
     for(unsigned i = 0; i < clause->size(); ++i) {
       prop::SatLiteral lit = (*clause)[i];
-      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+      Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable());
+      Expr atom = node.toExpr();
+
+      // The literals (true) and (not false) are omitted from conflicts
       if (atom.isConst()) {
         Assert (atom == utils::mkTrue() ||
                 (atom == utils::mkFalse() && lit.isNegated()));
         continue;
       }
+
       Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
       conflict.push_back(expr_lit);
+      conflictNodes.insert(lit.isNegated() ? node.notNode() : node);
+    }
+
+    LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes);
+
+    unsigned numberOfSteps = recipe.getNumSteps();
+
+    prop::SatClause currentClause = *clause;
+    std::vector<Expr> currentClauseExpr = conflict;
+
+    for (unsigned i = 0; i < numberOfSteps; ++i) {
+      const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+      if (currentStep->getTheory() != theory::THEORY_BV) {
+        continue;
+      }
+
+      // If any rewrites took place, we need to update the conflict clause accordingly
+      std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+      std::map<Node, Node> explanationToMissingAssertion;
+      std::set<Node>::iterator assertionIt;
+      for (assertionIt = missingAssertions.begin();
+           assertionIt != missingAssertions.end();
+           ++assertionIt) {
+        Node negated = (*assertionIt).negate();
+        explanationToMissingAssertion[recipe.getExplanation(negated)] = negated;
+      }
+
+      currentClause = *clause;
+      currentClauseExpr = conflict;
+
+      for (unsigned j = 0; j < i; ++j) {
+        // Literals already used in previous steps need to be negated
+        Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+
+        // If this literal is the result of a rewrite, we need to translate it
+        if (explanationToMissingAssertion.find(previousLiteralNode) !=
+            explanationToMissingAssertion.end()) {
+          previousLiteralNode = explanationToMissingAssertion[previousLiteralNode];
+        }
+
+        Node previousLiteralNodeNegated = previousLiteralNode.negate();
+        prop::SatLiteral previousLiteralNegated =
+          ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+
+        currentClause.push_back(previousLiteralNegated);
+        currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+      }
+
+      // If we're in the final step, the last literal is Null and should not be added.
+      // Otherwise, the current literal does NOT need to be negated
+      Node currentLiteralNode = currentStep->getLiteral();
+
+      if (currentLiteralNode != Node()) {
+        prop::SatLiteral currentLiteral =
+          ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+        currentClause.push_back(currentLiteral);
+        currentClauseExpr.push_back(currentLiteralNode.toExpr());
+      }
+
+      bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, currentClauseExpr));
     }
-    bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict));
   }
-  // FIXME: ugly, move into bit-vector proof by adding lemma
-  // queue inside each theory_proof
+
   BitVectorProof* bv = ProofManager::getBitVectorProof();
   bv->finalizeConflicts(bv_lemmas);
-
   bv->printResolutionProof(os, paren);
+}
+
+void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
+                                              std::ostream& os,
+                                              std::ostream& paren) {
+  os << " ;; Theory Lemmas \n";
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl;
+
+  if (Debug.isOn("pf::dumpLemmas")) {
+    dumpTheoryLemmas(lemmas);
+  }
+
+  finalizeBvConflicts(lemmas, os, paren);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     Assert (lemmas.size() == 1);
@@ -434,54 +537,247 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
     return;
   }
 
-  it = lemmas.begin();
-
+  ProofManager* pm = ProofManager::currentPM();
   Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl;
 
-  for (; it != end; ++it) {
-    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl;
-
-    // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl;
+  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
     ClauseId id = it->first;
-    Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
     const prop::SatClause* clause = it->second;
-    // printing clause as it appears in resolution proof
-    os << "(satlem _ _ ";
-    std::ostringstream clause_paren;
 
-    Debug("pf::tp") << "CnfProof printing clause..." << std::endl;
-    pm->getCnfProof()->printClause(*clause, os, clause_paren);
-    Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl;
+    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = "
+                    << id << std::endl;
 
     std::vector<Expr> clause_expr;
+    std::set<Node> clause_expr_nodes;
     for(unsigned i = 0; i < clause->size(); ++i) {
       prop::SatLiteral lit = (*clause)[i];
-      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+      Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+      Expr atom = node.toExpr();
       if (atom.isConst()) {
         Assert (atom == utils::mkTrue());
         continue;
       }
       Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
       clause_expr.push_back(expr_lit);
+      clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
     }
 
-    Debug("pf::tp") << "Expression printing done!" << std::endl;
-
-    // query appropriate theory for proof of clause
-    theory::TheoryId theory_id = getTheoryForLemma(id);
-    Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
-    Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl;
-    getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
-    Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
-    // os << " (clausify_false trust)";
-    os << clause_paren.str();
-    os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
-    paren << "))";
+    LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes);
+
+    if (recipe.simpleLemma()) {
+      // In a simple lemma, there will be no propositional resolution in the end
+
+      Debug("pf::tp") << "Simple lemma" << std::endl;
+      // Printing the clause as it appears in resolution proof
+      os << "(satlem _ _ ";
+      std::ostringstream clause_paren;
+      pm->getCnfProof()->printClause(*clause, os, clause_paren);
+
+      // Find and handle missing assertions, due to rewrites
+      std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(0);
+      if (!missingAssertions.empty()) {
+        Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl;
+      }
+
+      std::set<Node>::const_iterator missingAssertion;
+      for (missingAssertion = missingAssertions.begin();
+           missingAssertion != missingAssertions.end();
+           ++missingAssertion) {
+
+        Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+        Assert(recipe.wasRewritten(missingAssertion->negate()));
+        Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+        Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+        // We have a missing assertion.
+        //     rewriteIt->first is the assertion after the rewrite (the explanation),
+        //     rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+        bool found = false;
+        unsigned k;
+        for (k = 0; k < clause_expr.size(); ++k) {
+          if (clause_expr[k] == explanation.toExpr()) {
+            found = true;
+            break;
+          }
+        }
+
+        Assert(found);
+        Debug("pf::tp") << "Replacing theory assertion "
+                        << clause_expr[k]
+                        << " with "
+                        << *missingAssertion
+                        << std::endl;
+
+        clause_expr[k] = missingAssertion->toExpr();
+
+        std::ostringstream rewritten;
+        rewritten << "(or_elim_1 _ _ ";
+        rewritten << "(not_not_intro _ ";
+        rewritten << pm->getLitName(explanation);
+        rewritten << ") (iff_elim_1 _ _ ";
+        rewritten << d_assertionToRewrite[missingAssertion->negate()];
+        rewritten << "))";
+
+        Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+                        << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+                        << std::endl << std::endl;
+
+        pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+      }
+
+      // Query the appropriate theory for a proof of this clause
+      theory::TheoryId theory_id = getTheoryForLemma(clause);
+      Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
+      getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
+
+      // Turn rewrite filter OFF
+      pm->clearRewriteFilters();
+
+      Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+      os << clause_paren.str();
+      os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
+      paren << "))";
+    } else { // This is a composite lemma
+
+      unsigned numberOfSteps = recipe.getNumSteps();
+      prop::SatClause currentClause = *clause;
+      std::vector<Expr> currentClauseExpr = clause_expr;
+
+      for (unsigned i = 0; i < numberOfSteps; ++i) {
+        const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+        currentClause = *clause;
+        currentClauseExpr = clause_expr;
+
+        for (unsigned j = 0; j < i; ++j) {
+          // Literals already used in previous steps need to be negated
+          Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+          Node previousLiteralNodeNegated = previousLiteralNode.negate();
+          prop::SatLiteral previousLiteralNegated =
+            ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+          currentClause.push_back(previousLiteralNegated);
+          currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+        }
+
+        // If the current literal is NULL, can ignore (final step)
+        // Otherwise, the current literal does NOT need to be negated
+        Node currentLiteralNode = currentStep->getLiteral();
+        if (currentLiteralNode != Node()) {
+          prop::SatLiteral currentLiteral =
+            ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+          currentClause.push_back(currentLiteral);
+          currentClauseExpr.push_back(currentLiteralNode.toExpr());
+        }
+
+        os << "(satlem _ _ ";
+        std::ostringstream clause_paren;
+
+        pm->getCnfProof()->printClause(currentClause, os, clause_paren);
+
+        // query appropriate theory for proof of clause
+        theory::TheoryId theory_id = currentStep->getTheory();
+        Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
+
+        std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+        if (!missingAssertions.empty()) {
+          Debug("pf::tp") << "Have missing assertions for this step!" << std::endl;
+        }
+
+        // Turn rewrite filter ON
+        std::set<Node>::const_iterator missingAssertion;
+        for (missingAssertion = missingAssertions.begin();
+             missingAssertion != missingAssertions.end();
+             ++missingAssertion) {
+
+          Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+
+          Assert(recipe.wasRewritten(missingAssertion->negate()));
+          Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+
+          Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+          // We have a missing assertion.
+          //     rewriteIt->first is the assertion after the rewrite (the explanation),
+          //     rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+          bool found = false;
+          unsigned k;
+          for (k = 0; k < currentClauseExpr.size(); ++k) {
+            if (currentClauseExpr[k] == explanation.toExpr()) {
+              found = true;
+              break;
+            }
+          }
+
+          Assert(found);
+
+          Debug("pf::tp") << "Replacing theory assertion "
+                          << currentClauseExpr[k]
+                          << " with "
+                          << *missingAssertion
+                          << std::endl;
+
+          currentClauseExpr[k] = missingAssertion->toExpr();
+
+          std::ostringstream rewritten;
+          rewritten << "(or_elim_1 _ _ ";
+          rewritten << "(not_not_intro _ ";
+          rewritten << pm->getLitName(explanation);
+          rewritten << ") (iff_elim_1 _ _ ";
+          rewritten << d_assertionToRewrite[missingAssertion->negate()];
+          rewritten << "))";
+
+          Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+                          << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+                          << std::endl << std::endl;
+
+          pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+        }
+
+        getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren);
+
+        // Turn rewrite filter OFF
+        pm->clearRewriteFilters();
+
+        Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+        os << clause_paren.str();
+        os << "( \\ " << pm->getLemmaClauseName(id) << "s" << i <<"\n";
+        paren << "))";
+      }
+
+      Assert(numberOfSteps >= 2);
+
+      os << "(satlem_simplify _ _ _ ";
+      for (unsigned i = 0; i < numberOfSteps - 1; ++i) {
+        // Resolve step i with step i + 1
+        if (recipe.getStep(i)->getLiteral().getKind() == kind::NOT) {
+          os << "(Q _ _ ";
+        } else {
+          os << "(R _ _ ";
+        }
+
+        os << pm->getLemmaClauseName(id) << "s" << i;
+        os << " ";
+      }
+
+      os << pm->getLemmaClauseName(id) << "s" << numberOfSteps - 1 << " ";
+
+      prop::SatLiteral v;
+      for (int i = numberOfSteps - 2; i >= 0; --i) {
+        v = ProofManager::currentPM()->getCnfProof()->getLiteral(recipe.getStep(i)->getLiteral());
+        os << ProofManager::getVarName(v.getSatVariable(), "") << ") ";
+      }
+
+      os << "( \\ " << pm->getLemmaClauseName(id) << "\n";
+      paren << "))";
+    }
   }
 }
 
 void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) {
-  // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
 
   LetMap::const_iterator it = map.find(term);
   if (it != map.end()) {
@@ -597,19 +893,21 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Let
 }
 
 void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
-  //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
-  Assert( d_theory!=NULL );
+  // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
+  Assert(d_theory!=NULL);
+
   context::UserContext fakeContext;
   ProofOutputChannel oc;
   theory::Valuation v(NULL);
   //make new copy of theory
   theory::Theory* th;
-  Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
-  if(d_theory->getId()==theory::THEORY_UF) {
+  Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
+
+  if (d_theory->getId()==theory::THEORY_UF) {
     th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
                                   ProofManager::currentPM()->getLogicInfo(),
                                   "replay::");
-  } else if(d_theory->getId()==theory::THEORY_ARRAY) {
+  } else if (d_theory->getId()==theory::THEORY_ARRAY) {
     th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
                                           ProofManager::currentPM()->getLogicInfo(),
                                           "replay::");
@@ -714,7 +1012,10 @@ void BooleanProof::registerTerm(Expr term) {
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {
-    os << "(p_app " << ProofManager::sanitize(term) <<")";
+    if (d_treatBoolsAsFormulas)
+      os << "(p_app " << ProofManager::sanitize(term) <<")";
+    else
+      os << ProofManager::sanitize(term);
     return;
   }
 
@@ -753,7 +1054,10 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap&
     return;
 
   case kind::CONST_BOOLEAN:
-    os << (term.getConst<bool>() ? "true" : "false");
+    if (d_treatBoolsAsFormulas)
+      os << (term.getConst<bool>() ? "true" : "false");
+    else
+      os << (term.getConst<bool>() ? "t_true" : "t_false");
     return;
 
   default:
@@ -786,6 +1090,10 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream&
   // Nothing to do here at this point.
 }
 
+void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+  // Nothing to do here at this point.
+}
+
 void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                              std::ostream& os,
                                              std::ostream& paren) {
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 54c86f3f3..c8c776ec9 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -27,6 +27,7 @@
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "util/proof.h"
+#include "proof/proof_utils.h"
 
 namespace CVC4 {
 
@@ -90,10 +91,14 @@ class TheoryProof;
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
 
+typedef std::set<theory::TheoryId> TheoryIdSet;
+typedef std::map<Expr, TheoryIdSet> ExprToTheoryIds;
+
 class TheoryProofEngine {
 protected:
   ExprSet d_registrationCache;
   TheoryProofTable d_theoryProofTable;
+  ExprToTheoryIds d_exprToTheoryIds;
 
   /**
    * Returns whether the theory is currently supported in proof
@@ -148,6 +153,14 @@ public:
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
 
   /**
+   * Print aliasing declarations.
+   *
+   * @param os
+   * @param paren closing parenthesis
+   */
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+
+  /**
    * Print proofs of all the theory lemmas (must prove
    * actual clause used in resolution proof).
    *
@@ -171,8 +184,14 @@ public:
    */
   void registerTheory(theory::Theory* theory);
 
-  theory::TheoryId getTheoryForLemma(ClauseId id);
+  theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
   TheoryProof* getTheoryProof(theory::TheoryId id);
+
+  void markTermForFutureRegistration(Expr term, theory::TheoryId id);
+
+  void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+
+  virtual void treatBoolsAsFormulas(bool value) {};
 };
 
 class LFSCTheoryProofEngine : public TheoryProofEngine {
@@ -190,11 +209,25 @@ public:
   virtual void printLetTerm(Expr term, std::ostream& os);
   virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printAssertions(std::ostream& os, std::ostream& paren);
+  virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTheoryLemmas(const IdToSatClause& lemmas,
                                  std::ostream& os,
                                  std::ostream& paren);
   virtual void printSort(Type type, std::ostream& os);
+
+  void performExtraRegistrations();
+
+  void treatBoolsAsFormulas(bool value);
+
+private:
+  static void dumpTheoryLemmas(const IdToSatClause& lemmas);
+
+  // TODO: this function should be moved into the BV prover.
+  void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren);
+
+  std::map<Node, std::string> d_assertionToRewrite;
 };
 
 class TheoryProof {
@@ -270,11 +303,20 @@ public:
    */
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
   /**
+   * Print any aliasing declarations.
+   *
+   * @param os
+   * @param paren
+   */
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+  /**
    * Register a term of this theory that appears in the proof.
    *
    * @param term
    */
   virtual void registerTerm(Expr term) = 0;
+
+  virtual void treatBoolsAsFormulas(bool value) {}
 };
 
 class BooleanProof : public TheoryProof {
@@ -292,12 +334,13 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
 };
 
 class LFSCBooleanProof : public BooleanProof {
 public:
   LFSCBooleanProof(TheoryProofEngine* proofEngine)
-    : BooleanProof(proofEngine)
+    : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
   {}
   virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
@@ -305,6 +348,14 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+
+  void treatBoolsAsFormulas(bool value) {
+    d_treatBoolsAsFormulas = value;
+  }
+
+private:
+  bool d_treatBoolsAsFormulas;
 };
 
 } /* CVC4 namespace */
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 32ca122b0..bc409901c 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -86,7 +86,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
   pf->debug_print("pf::uf");
   Debug("pf::uf") << std::endl;
 
-  if(tb == 0) {
+  if (tb == 0) {
+    // Special case: false was an input, so the proof is just "false".
+    if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY &&
+        pf->d_node == NodeManager::currentNM()->mkConst(false)) {
+      out << "(clausify_false ";
+      out << ProofManager::getLitName(NodeManager::currentNM()->mkConst(false).notNode());
+      out << ")" << std::endl;
+      return Node();
+    }
+
     Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
     Assert(!pf->d_node.isNull());
     Assert(pf->d_children.size() >= 2);
@@ -190,42 +199,71 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
         ++i;
       }
     }
-    Assert(neg >= 0);
+
+    bool disequalityFound = (neg >= 0);
+    if (!disequalityFound) {
+      Debug("pf::uf") << "A disequality was NOT found. UNSAT due to merged constants" << std::endl;
+      Debug("pf::uf") << "Proof for: " << pf->d_node << std::endl;
+      Assert(pf->d_node.getKind() == kind::EQUAL);
+      Assert(pf->d_node.getNumChildren() == 2);
+      Assert (pf->d_node[0].isConst() && pf->d_node[1].isConst());
+    }
 
     Node n1;
     std::stringstream ss;
-    //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
     Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
-    if(pf->d_children.size() > 2) {
+
+    if(!disequalityFound || subTrans.d_children.size() >= 2) {
       n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
     } else {
       n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
       Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
     }
 
-    Node n2 = pf->d_children[neg]->d_node;
-    Assert(n2.getKind() == kind::NOT);
-    out << "(clausify_false (contra _ ";
     Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
-    Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
 
-    if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
-    if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
+    out << "(clausify_false (contra _ ";
+
+    if (disequalityFound) {
+      Node n2 = pf->d_children[neg]->d_node;
+      Assert(n2.getKind() == kind::NOT);
+      Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
 
-    if(n2[0].getKind() == kind::APPLY_UF) {
-      out << "(trans _ _ _ _ ";
-      out << "(symm _ _ _ ";
-      out << ss.str();
-      out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
-    } else {
-      Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
-      if(n1[1] == n2[0][0]) {
-        out << "(symm _ _ _ " << ss.str() << ")";
+      if (n2[0].getNumChildren() > 0) { Debug("pf::uf") << "\nn2[0]: " << n2[0][0] << std::endl; }
+      if (n1.getNumChildren() > 1) { Debug("pf::uf") << "n1[1]: " << n1[1] << std::endl; }
+
+      if(n2[0].getKind() == kind::APPLY_UF) {
+        out << "(trans _ _ _ _ ";
+
+        if (n1[0] == n2[0]) {
+          out << "(symm _ _ _ ";
+          out << ss.str();
+          out << ") ";
+        } else {
+          Assert(n1[1] == n2[0]);
+          out << ss.str();
+        }
+        out << "(pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
       } else {
-        out << ss.str();
+        Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
+        if(n1[1] == n2[0][0]) {
+          out << "(symm _ _ _ " << ss.str() << ")";
+        } else {
+          out << ss.str();
+        }
+        out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
       }
-      out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
+    } else {
+      Node n2 = pf->d_node;
+      Assert(n2.getKind() == kind::EQUAL);
+      Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+
+      out << ss.str();
+      out << " ";
+      ProofManager::getTheoryProofEngine()->printConstantDisequalityProof(out, n1[0].toExpr(), n1[1].toExpr());
+      out << "))" << std::endl;
     }
+
     return Node();
   }
 
@@ -584,10 +622,10 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) {
         // n1 is an equality/iff, but n2 is a predicate
         if(n1[0] == n2) {
-          n1 = n1[1];
+          n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true));
           ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
         } else if(n1[1] == n2) {
-          n1 = n1[0];
+          n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true));
           ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
         } else {
           Unreachable();
@@ -595,16 +633,16 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) {
         // n2 is an equality/iff, but n1 is a predicate
         if(n2[0] == n1) {
-          n1 = n2[1];
+          n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true));
           ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
         } else if(n2[1] == n1) {
-          n1 = n2[0];
+          n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true));
           ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
         } else {
           Unreachable();
         }
       } else {
-        // Both n1 and n2 are prediacates. Don't know what to do...
+        // Both n1 and n2 are predicates. Don't know what to do...
         Unreachable();
       }
 
@@ -667,6 +705,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map)
   }
 
   Assert (term.getKind() == kind::APPLY_UF);
+  d_proofEngine->treatBoolsAsFormulas(false);
 
   if(term.getType().isBoolean()) {
     os << "(p_app ";
@@ -683,6 +722,7 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map)
   if(term.getType().isBoolean()) {
     os << ")";
   }
+  d_proofEngine->treatBoolsAsFormulas(true);
 }
 
 void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
@@ -714,6 +754,8 @@ void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
 
 void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
   // declaring the terms
+  Debug("pf::uf") << "LFSCUFProof::printTermDeclarations called" << std::endl;
+
   for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
     Expr term = *it;
 
@@ -729,7 +771,8 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
       os << "(arrow";
       for (unsigned i = 0; i < args.size(); i++) {
         Type arg_type = args[i];
-        os << " " << arg_type;
+        os << " ";
+        d_proofEngine->printSort(arg_type, os);
         if (i < args.size() - 2) {
           os << " (arrow";
           fparen << ")";
@@ -742,10 +785,16 @@ void LFSCUFProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
     }
     paren << ")";
   }
+
+  Debug("pf::uf") << "LFSCUFProof::printTermDeclarations done" << std::endl;
 }
 
 void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
   // Nothing to do here at this point.
 }
 
+void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+  // Nothing to do here at this point.
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index e359eaebd..0a23267d8 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -69,6 +69,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
 };
 
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index aa1fc9587..eda736b8a 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -120,7 +120,7 @@ bool CnfStream::hasLiteral(TNode n) const {
   return find != d_nodeToLiteralMap.end();
 }
 
-void TseitinCnfStream::ensureLiteral(TNode n) {
+void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
   // These are not removable and have no proof ID
   d_removable = false;
 
@@ -163,7 +163,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
     d_literalToNodeMap.insert_safe(~lit, n.notNode());
   } else {
     // We have a theory atom or variable.
-    lit = convertAtom(n);
+    lit = convertAtom(n, noPreregistration);
   }
 
   Assert(hasLiteral(n) && getNode(lit) == n);
@@ -232,7 +232,7 @@ void CnfStream::setProof(CnfProof* proof) {
   d_cnfProof = proof;
 }
 
-SatLiteral CnfStream::convertAtom(TNode node) {
+SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
   Assert(!hasLiteral(node), "atom already mapped!");
@@ -247,7 +247,7 @@ SatLiteral CnfStream::convertAtom(TNode node) {
   } else {
     theoryLiteral = true;
     canEliminate = false;
-    preRegister = true;
+    preRegister = !noPreregistration;
   }
 
   // Make a new literal (variables are not considered theory literals)
@@ -258,7 +258,11 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
 SatLiteral CnfStream::getLiteral(TNode node) {
   Assert(!node.isNull(), "CnfStream: can't getLiteral() of null node");
-  Assert(d_nodeToLiteralMap.contains(node), "Literal not in the CNF Cache: %s\n", node.toString().c_str());
+
+  Assert(d_nodeToLiteralMap.contains(node),
+         "Literal not in the CNF Cache: %s\n",
+         node.toString().c_str());
+
   SatLiteral literal = d_nodeToLiteralMap[node];
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;
@@ -675,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node,
                                         bool negated,
                                         ProofRule proof_id,
                                         TNode from,
-                                        theory::TheoryId ownerTheory) {
+                                        LemmaProofRecipe* proofRecipe) {
   Debug("cnf") << "convertAndAssert(" << node
                << ", removable = " << (removable ? "true" : "false")
                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
@@ -685,7 +689,12 @@ void TseitinCnfStream::convertAndAssert(TNode node,
       Node assertion = negated ? node.notNode() : (Node)node;
       Node from_assertion = negated? from.notNode() : (Node) from;
 
-      d_cnfProof->setExplainerTheory(ownerTheory);
+      if (proofRecipe) {
+        Debug("pf::sat") << "TseitinCnfStream::convertAndAssert: setting proof recipe" << std::endl;
+        proofRecipe->dump("pf::sat");
+        d_cnfProof->setProofRecipe(proofRecipe);
+      }
+
       if (proof_id != RULE_INVALID) {
         d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
         d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index cf9d519a7..6cc10d878 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -36,6 +36,9 @@
 #include "smt_util/lemma_channels.h"
 
 namespace CVC4 {
+
+class LemmaProofRecipe;
+
 namespace prop {
 
 class PropEngine;
@@ -174,7 +177,7 @@ protected:
    * structure in this expression.  Assumed to not be in the
    * translation cache.
    */
-  SatLiteral convertAtom(TNode node);
+  SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
 
 public:
 
@@ -207,14 +210,10 @@ public:
    * @param node node to convert and assert
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
-   * @param ownerTheory indicates the theory that should invoked to prove the formula.
+   * @param proofRecipe contains the proof recipe for proving this node
    */
-  virtual void convertAndAssert(TNode node,
-                                bool removable,
-                                bool negated,
-                                ProofRule proof_id,
-                                TNode from = TNode::null(),
-                                theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0;
+  virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0;
+
   /**
    * Get the node that is represented by the given SatLiteral.
    * @param literal the literal from the sat solver
@@ -235,7 +234,7 @@ public:
    * this is like a "convert-but-don't-assert" version of
    * convertAndAssert().
    */
-  virtual void ensureLiteral(TNode n) = 0;
+  virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
@@ -284,7 +283,7 @@ public:
    */
   void convertAndAssert(TNode node, bool removable,
                         bool negated, ProofRule rule, TNode from = TNode::null(),
-                        theory::TheoryId ownerTheory = theory::THEORY_LAST);
+                        LemmaProofRecipe* proofRecipe = NULL);
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -337,7 +336,7 @@ private:
    */
   SatLiteral toCNF(TNode node, bool negated = false);
 
-  void ensureLiteral(TNode n);
+  void ensureLiteral(TNode n, bool noPreregistration = false);
 
 };/* class TseitinCnfStream */
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 411b89514..d898b66a2 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -232,6 +232,8 @@ CRef Solver::reason(Var x) {
     vec<Lit> explanation;
     MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
+    Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl;
+
     // Sort the literals by trail index level
     lemma_lt lt(*this);
     sort(explanation, lt);
@@ -266,6 +268,12 @@ CRef Solver::reason(Var x) {
     }
     explanation.shrink(i - j);
 
+    Debug("pf::sat") << "Solver::reason: explanation = " ;
+    for (int i = 0; i < explanation.size(); ++i) {
+      Debug("pf::sat") << explanation[i] << " ";
+    }
+    Debug("pf::sat") << std::endl;
+
     // We need an explanation clause so we add a fake literal
     if (j == 1) {
       // Add not TRUE to the clause
@@ -276,6 +284,7 @@ CRef Solver::reason(Var x) {
     CRef real_reason = ca.alloc(explLevel, explanation, true);
     // FIXME: at some point will need more information about where this explanation
     // came from (ie. the theory/sharing)
+    Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
     PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
            ProofManager::getCnfProof()->registerConvertedClause(id, true);
            // no need to pop current assertion as this is not converted to cnf
@@ -336,6 +345,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
     // If we are in solve or decision level > 0
     if (minisat_busy || decisionLevel() > 0) {
+      Debug("pf::sat") << "Add clause adding a new lemma: ";
+      for (int k = 0; k < ps.size(); ++k) {
+        Debug("pf::sat") << ps[k] << " ";
+      }
+      Debug("pf::sat") << std::endl;
+
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
@@ -1666,6 +1681,13 @@ CRef Solver::updateLemmas() {
     {
       // The current lemma
       vec<Lit>& lemma = lemmas[i];
+
+      Debug("pf::sat") << "Solver::updateLemmas: working on lemma: ";
+      for (int k = 0; k < lemma.size(); ++k) {
+        Debug("pf::sat") << lemma[k] << " ";
+      }
+      Debug("pf::sat") << std::endl;
+
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
         Assert (! PROOF_ON());
@@ -1725,6 +1747,7 @@ CRef Solver::updateLemmas() {
          TNode cnf_assertion = lemmas_cnf_assertion[i].first;
          TNode cnf_def = lemmas_cnf_assertion[i].second;
 
+         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
@@ -1741,6 +1764,7 @@ CRef Solver::updateLemmas() {
          Node cnf_assertion = lemmas_cnf_assertion[i].first;
          Node cnf_def = lemmas_cnf_assertion[i].second;
 
+         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index bfbf9da6f..ff726e299 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   // FIXME: This relies on the invariant that when ok() is false
   // the SAT solver does not add the clause (which is what Minisat currently does)
   if (!ok()) {
-    return ClauseIdUndef; 
+    return ClauseIdUndef;
   }
   d_minisat->addClause(minisat_clause, removable, clause_id);
   PROOF( Assert (clause_id != ClauseIdError););
@@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() {
 }
 
 bool MinisatSatSolver::ok() const {
-  return d_minisat->okay(); 
+  return d_minisat->okay();
 }
 
 void MinisatSatSolver::interrupt() {
@@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const
   return true;
 }
 
-void MinisatSatSolver::requirePhase(SatLiteral lit) { 
+void MinisatSatSolver::requirePhase(SatLiteral lit) {
   Assert(!d_minisat->rnd_pol);
   Debug("minisat") << "requirePhase(" << lit << ")" << " " <<  lit.getSatVariable() << " " << lit.isNegated() << std::endl;
   SatVariable v = lit.getSatVariable();
   d_minisat->freezePolarity(v, lit.isNegated());
 }
 
-bool MinisatSatSolver::flipDecision() { 
+bool MinisatSatSolver::flipDecision() {
   Debug("minisat") << "flipDecision()" << std::endl;
   return d_minisat->flipDecision();
 }
 
-bool MinisatSatSolver::isDecision(SatVariable decn) const { 
-  return d_minisat->isDecision( decn ); 
+bool MinisatSatSolver::isDecision(SatVariable decn) const {
+  return d_minisat->isDecision( decn );
 }
 
 /** Incremental interface */
@@ -291,7 +291,7 @@ namespace CVC4 {
 template<>
 prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
   return prop::MinisatSatSolver::toSatLiteral(lit);
-} 
+}
 
 template<>
 void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
@@ -300,5 +300,3 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause&
 }
 
 } /* namespace CVC4 */
-
-
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 54cf4c457..eb607e901 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -132,13 +132,13 @@ void PropEngine::assertFormula(TNode node) {
 void PropEngine::assertLemma(TNode node, bool negated,
                              bool removable,
                              ProofRule rule,
-                             theory::TheoryId ownerTheory,
+                             LemmaProofRecipe* proofRecipe,
                              TNode from) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
   // Assert as (possibly) removable
-  d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory);
+  d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe);
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index b9ce7ca7e..c02015931 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -37,6 +37,7 @@ namespace CVC4 {
 class ResourceManager;
 class DecisionEngine;
 class TheoryEngine;
+class LemmaProofRecipe;
 
 namespace theory {
   class TheoryRegistrar;
@@ -134,7 +135,7 @@ public:
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, TNode from = TNode::null());
+  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, LemmaProofRecipe* proofRecipe, TNode from = TNode::null());
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 4a4515eb9..6e8f1fbbf 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -99,29 +99,34 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode);
-  Node explanationNode = theoryExplanation.node;
-  theory::TheoryId explainerTheory = theoryExplanation.theory;
+  LemmaProofRecipe* proofRecipe = NULL;
+  PROOF(proofRecipe = new LemmaProofRecipe;);
+
+  Node theoryExplanation = d_theoryEngine->getExplanationAndRecipe(lNode, proofRecipe);
 
   PROOF({
-      ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode);
-      ProofManager::getCnfProof()->setExplainerTheory(explainerTheory);
+      ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation);
+      ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
+
+      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting lemma recipe to: "
+                       << std::endl;
+      proofRecipe->dump("pf::sat");
 
-      Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: "
-                        << explainerTheory << std::endl;
+      delete proofRecipe;
+      proofRecipe = NULL;
     });
 
-  Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl;
-  if (explanationNode.getKind() == kind::AND) {
-    Node::const_iterator it = explanationNode.begin();
-    Node::const_iterator it_end = explanationNode.end();
+  Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
+  if (theoryExplanation.getKind() == kind::AND) {
+    Node::const_iterator it = theoryExplanation.begin();
+    Node::const_iterator it_end = theoryExplanation.end();
     explanation.push_back(l);
     for (; it != it_end; ++ it) {
       explanation.push_back(~d_cnfStream->getLiteral(*it));
     }
   } else {
     explanation.push_back(l);
-    explanation.push_back(~d_cnfStream->getLiteral(explanationNode));
+    explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
   }
 }
 
@@ -175,7 +180,9 @@ void TheoryProxy::notifyRestart() {
           if(lemmaCount % 1 == 0) {
             Debug("shared") << "=) " << asNode << std::endl;
           }
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST);
+
+          LemmaProofRecipe* noProofRecipe = NULL;
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, noProofRecipe);
         } else {
           Debug("shared") << "=(" << asNode << std::endl;
         }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8f282b413..63afb0b72 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -990,7 +990,7 @@ public:
           Trace("smt-qe-debug") << "   return : " << ret << std::endl;
           //recursive (for nested quantification)
           ret = replaceQuantifiersWithInstantiations( reti, insts, visited );
-        }     
+        }
       }else if( n.getNumChildren()>0 ){
         bool childChanged = false;
         std::vector< Node > children;
@@ -1723,14 +1723,14 @@ void SmtEngine::setDefaults() {
     //must have finite model finding on
     options::finiteModelFind.set( true );
   }
-  
+
   //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
   if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
     if( !options::instWhenStrictInterleave.wasSetByUser() ){
       options::instWhenStrictInterleave.set( false );
     }
   }
-  
+
   //local theory extensions
   if( options::localTheoryExt() ){
     if( !options::instMaxLevel.wasSetByUser() ){
@@ -1803,8 +1803,8 @@ void SmtEngine::setDefaults() {
   //apply counterexample guided instantiation options
   if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){
     if( !options::ceGuidedInst.wasSetByUser() ){
-      options::ceGuidedInst.set( true ); 
-    } 
+      options::ceGuidedInst.set( true );
+    }
   }
   if( options::ceGuidedInst() ){
     //counterexample-guided instantiation for sygus
@@ -1845,7 +1845,7 @@ void SmtEngine::setDefaults() {
   }
   //counterexample-guided instantiation for non-sygus
   // enable if any quantifiers with arithmetic or datatypes
-  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || 
+  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) ||
       options::cbqiAll() ){
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
@@ -3858,7 +3858,7 @@ void SmtEnginePrivate::processAssertions() {
        ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr());
      }
      );
-  
+
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   if( options::ceGuidedInst() ){
@@ -4240,7 +4240,7 @@ void SmtEnginePrivate::processAssertions() {
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl;
   dumpAssertions("post-everything", d_assertions);
-  
+
 
   //set instantiation level of everything to zero
   if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
@@ -4434,18 +4434,18 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx
     //possibly run quantifier elimination to make formula into single invocation
     if( conj[1].getKind()==kind::EXISTS ){
       Node conj_se = conj[1][1];
-      
+
       Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
       quantifiers::SingleInvocationPartition sip( kind::APPLY );
       sip.init( conj_se );
       Trace("smt-synth") << "...finished, got:" << std::endl;
       sip.debugPrint("smt-synth");
-      
+
       if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){
         //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f.
-        //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), 
+        //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ),
         //  and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f.  We invoke synthesis solver on this result.
-      
+
         //create new smt engine to do quantifier elimination
         SmtEngine smt_qe( d_exprManager );
         smt_qe.setLogic(getLogicInfo());
@@ -4480,11 +4480,11 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx
         Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() );
         Assert( !qe_vars.empty() );
         conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs );
-        
+
         Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl;
         Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false );
         Trace("smt-synth") << "Result : " << qe_res << std::endl;
-        
+
         //create single invocation conjecture
         Node qe_res_n = Node::fromExpr( qe_res );
         qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() );
@@ -4498,7 +4498,7 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx
       }
     }
   }
-  
+
   return checkSatisfiability( e_check, true, false );
 }
 
@@ -5125,7 +5125,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
     Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
   }
   Trace("smt-qe") << "Do quantifier elimination " << e << std::endl;
-  Node n_e = Node::fromExpr( e );  
+  Node n_e = Node::fromExpr( e );
   if( n_e.getKind()!=kind::EXISTS ){
     throw ModalException("Expecting an existentially quantified formula as argument to get-qe.");
   }
@@ -5152,7 +5152,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
       InternalError(ss.str().c_str());
     }
     //get the instantiations for all quantified formulas
-    std::map< Node, std::vector< Node > > insts;    
+    std::map< Node, std::vector< Node > > insts;
     d_theoryEngine->getInstantiations( insts );
     //find the quantified formula that corresponds to the input
     Node top_q;
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 5634a4651..808f5162c 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -63,14 +63,21 @@ void SmtEngine::checkProof() {
 
   Chat() << "checking proof..." << endl;
 
-  if ( !(d_logic.isPure(theory::THEORY_BOOL) ||
-           d_logic.isPure(theory::THEORY_BV) ||
-           d_logic.isPure(theory::THEORY_ARRAY) ||
-           (d_logic.isPure(theory::THEORY_UF) &&
-            ! d_logic.hasCardinalityConstraints())) ||
-       d_logic.isQuantified()) {
-    // no checking for these yet
-    Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl;
+  std::string logicString = d_logic.getLogicString();
+
+  if (!(
+        // Pure logics
+        logicString == "QF_UF" ||
+        logicString == "QF_AX" ||
+        logicString == "QF_BV" ||
+        // Non-pure logics
+        logicString == "QF_AUF" ||
+        logicString == "QF_UFBV" ||
+        logicString == "QF_ABV" ||
+        logicString == "QF_AUFBV"
+        )) {
+    // This logic is not yet supported
+    Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" << endl;
     return;
   }
 
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 11c3dc081..6dfd14157 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -101,8 +101,59 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
         Debug("pf::ee") << "Getting explanation for ROW guard: "
                         << indexOne << " != " << indexTwo << std::endl;
 
+
         eq::EqProof* childProof = new eq::EqProof;
         d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof);
+
+        // It could be that the guard condition is a constant disequality. In this case,
+        // we need to change it to a different format.
+        if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
+          // The proof has two children, explaining why each index is a (different) constant.
+          Assert(childProof->d_children.size() == 2);
+
+          Node constantOne, constantTwo;
+          // Each subproof explains why one of the indices is constant.
+
+          if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+            constantOne = childProof->d_children[0]->d_node;
+          } else {
+            Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
+            if ((childProof->d_children[0]->d_node[0] == indexOne) ||
+                (childProof->d_children[0]->d_node[0] == indexTwo)) {
+              constantOne = childProof->d_children[0]->d_node[1];
+            } else {
+              constantOne = childProof->d_children[0]->d_node[0];
+            }
+          }
+
+          if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+            constantTwo = childProof->d_children[1]->d_node;
+          } else {
+            Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
+            if ((childProof->d_children[1]->d_node[0] == indexOne) ||
+                (childProof->d_children[1]->d_node[0] == indexTwo)) {
+              constantTwo = childProof->d_children[1]->d_node[1];
+            } else {
+              constantTwo = childProof->d_children[1]->d_node[0];
+            }
+          }
+
+          eq::EqProof* constantDisequalityProof = new eq::EqProof;
+          constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
+          constantDisequalityProof->d_node =
+            NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
+
+          // Middle is where we need to insert the new disequality
+          std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin();
+          ++middle;
+
+          childProof->d_children.insert(middle, constantDisequalityProof);
+
+          childProof->d_id = theory::eq::MERGED_THROUGH_TRANS;
+          childProof->d_node =
+            NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate();
+        }
+
         proof->d_children.push_back(childProof);
       } else {
         // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 6add1b55f..28a08630e 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -829,7 +829,8 @@ void TheoryArrays::propagate(Effort e)
 
 
 Node TheoryArrays::explain(TNode literal) {
-  return explain(literal, NULL);
+  Node explanation = explain(literal, NULL);
+  return explanation;
 }
 
 Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
@@ -1394,6 +1395,7 @@ void TheoryArrays::check(Effort e) {
         break;
     default:
       Unreachable();
+      break;
     }
   }
 
@@ -2231,6 +2233,7 @@ bool TheoryArrays::dischargeLemmas()
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
   eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
+
   if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b), proof);
   } else {
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index fdc36ce72..dc5520411 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -41,7 +41,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
           continue;
         }
         Node signature = computeSignature(assertions[i][j]);
-        storeSignature(signature, assertions[i][j]); 
+        storeSignature(signature, assertions[i][j]);
         Debug("bv-abstraction") << "   assertion: " << assertions[i][j] <<"\n";
         Debug("bv-abstraction") << "   signature: " << signature <<"\n";
       }
@@ -52,7 +52,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
   for (unsigned i = 0; i < assertions.size(); ++i) {
     if (assertions[i].getKind() == kind::OR &&
         assertions[i][0].getKind() == kind::AND) {
-      std::vector<Node> new_children; 
+      std::vector<Node> new_children;
       for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) {
         if (hasSignature(assertions[i][j])) {
           new_children.push_back(abstractSignatures(assertions[i][j]));
@@ -60,10 +60,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
           new_children.push_back(assertions[i][j]);
         }
       }
-      new_assertions.push_back(utils::mkNode(kind::OR, new_children)); 
+      new_assertions.push_back(utils::mkNode(kind::OR, new_children));
     } else {
       // assertions that are not changed
-      new_assertions.push_back(assertions[i]); 
+      new_assertions.push_back(assertions[i]);
     }
   }
 
@@ -71,21 +71,21 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
     skolemizeArguments(new_assertions);
   }
 
-  
+
   // if we are using the eager solver reverse the abstraction
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     if (d_funcToSignature.size() == 0) {
       // we did not change anything
       return false;
     }
-    NodeNodeMap seen; 
+    NodeNodeMap seen;
     for (unsigned i = 0; i < new_assertions.size(); ++i) {
-      new_assertions[i] = reverseAbstraction(new_assertions[i], seen); 
+      new_assertions[i] = reverseAbstraction(new_assertions[i], seen);
     }
     // we undo the abstraction functions so the logic is QF_BV still
-    return true; 
+    return true;
   }
-  
+
   // return true if we have created new function symbols for the problem
   return d_funcToSignature.size() != 0;
 }
@@ -99,7 +99,7 @@ bool AbstractionModule::isConjunctionOfAtoms(TNode node) {
 bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) {
   if (seen.find(node)!= seen.end())
     return true;
-  
+
   if (!node.getType().isBitVector()) {
     return (node.getKind() == kind::AND || utils::isBVPredicate(node));
   }
@@ -120,30 +120,30 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) {
 
   if (seen.find(assertion) != seen.end())
     return seen[assertion];
-  
+
   if (isAbstraction(assertion)) {
     Node interp =  getInterpretation(assertion);
     seen[assertion] = interp;
-    Assert (interp.getType() == assertion.getType()); 
+    Assert (interp.getType() == assertion.getType());
     return interp;
   }
 
   if (assertion.getNumChildren() == 0) {
     seen[assertion] = assertion;
-    return assertion; 
+    return assertion;
   }
-  
+
   NodeBuilder<> result(assertion.getKind());
   if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    result << assertion.getOperator(); 
+    result << assertion.getOperator();
   }
 
   for (unsigned i = 0; i < assertion.getNumChildren(); ++i) {
-    result << reverseAbstraction(assertion[i], seen); 
+    result << reverseAbstraction(assertion[i], seen);
   }
   Node res = result;
   seen[assertion] = res;
-  return res; 
+  return res;
 }
 
 void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
@@ -151,7 +151,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
     TNode assertion = assertions[i];
     if (assertion.getKind() != kind::OR)
       continue;
-    
+
     bool is_skolemizable = true;
     for (unsigned k = 0; k < assertion.getNumChildren(); ++k) {
       if (assertion[k].getKind() != kind::EQUAL ||
@@ -191,54 +191,54 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
       NodeBuilder<> skolem_func (kind::APPLY_UF);
       skolem_func << func;
       std::vector<Node> skolem_args;
-        
+
       for (unsigned j = 0; j < args.getArity(); ++j) {
         bool all_same = true;
         for (unsigned k = 1; k < args.getNumEntries(); ++k) {
           if ( args.getEntry(k)[j] != args.getEntry(0)[j])
-            all_same = false; 
+            all_same = false;
         }
-        Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); 
+        Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j]));
         skolem_args.push_back(new_arg);
-        skolem_func << new_arg; 
+        skolem_func << new_arg;
       }
-      
 
-      Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); 
-      
+
+      Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u));
+
       // enumerate arguments assignments
-      std::vector<Node> or_assignments; 
+      std::vector<Node> or_assignments;
       for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) {
         NodeBuilder<> arg_assignment(kind::AND);
         ArgsVec& args =  *it;
         for (unsigned k = 0; k < args.size(); ++k) {
           Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]);
-          arg_assignment << eq; 
+          arg_assignment << eq;
         }
         or_assignments.push_back(arg_assignment);
       }
-      
+
       Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments));
-      assertion_builder << new_func_def; 
+      assertion_builder << new_func_def;
     }
     Node new_assertion = assertion_builder;
     Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n";
-    Debug("bv-abstraction-dbg") << "    " << new_assertion; 
+    Debug("bv-abstraction-dbg") << "    " << new_assertion;
     assertions[i] = new_assertion;
   }
 }
 
 void AbstractionModule::storeSignature(Node signature, TNode assertion) {
   if(d_signatures.find(signature) == d_signatures.end()) {
-    d_signatures[signature] = 0; 
+    d_signatures[signature] = 0;
   }
-  d_signatures[signature] = d_signatures[signature] + 1; 
-  d_assertionToSignature[assertion] = signature; 
+  d_signatures[signature] = d_signatures[signature] + 1;
+  d_assertionToSignature[assertion] = signature;
 }
 
 Node AbstractionModule::computeSignature(TNode node) {
-  resetSignatureIndex(); 
-  NodeNodeMap cache; 
+  resetSignatureIndex();
+  NodeNodeMap cache;
   Node sig = computeSignatureRec(node, cache);
   return sig;
 }
@@ -247,17 +247,17 @@ Node AbstractionModule::getSignatureSkolem(TNode node) {
   Assert (node.getKind() == kind::VARIABLE);
   unsigned bitwidth = utils::getSize(node);
   if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) {
-    d_signatureSkolems[bitwidth] = vector<Node>(); 
+    d_signatureSkolems[bitwidth] = vector<Node>();
   }
-  
+
   vector<Node>& skolems = d_signatureSkolems[bitwidth];
   // get the index of bv variables of this size
-  unsigned index = getBitwidthIndex(bitwidth); 
+  unsigned index = getBitwidthIndex(bitwidth);
   Assert (skolems.size() + 1 >= index );
   if (skolems.size() == index) {
     ostringstream os;
     os << "sig_" <<bitwidth <<"_" << index;
-    NodeManager* nm = NodeManager::currentNM(); 
+    NodeManager* nm = NodeManager::currentNM();
     skolems.push_back(nm->mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures"));
   }
   ++(d_signatureIndices[bitwidth]);
@@ -268,12 +268,12 @@ unsigned AbstractionModule::getBitwidthIndex(unsigned bitwidth) {
   if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) {
     d_signatureIndices[bitwidth] = 0;
   }
-  return d_signatureIndices[bitwidth]; 
+  return d_signatureIndices[bitwidth];
 }
 
 void AbstractionModule::resetSignatureIndex() {
   for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) {
-    it->second = 0; 
+    it->second = 0;
   }
 }
 
@@ -282,24 +282,24 @@ bool AbstractionModule::hasSignature(Node node) {
 }
 
 Node AbstractionModule::getGeneralizedSignature(Node node) {
-  NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); 
+  NodeNodeMap::const_iterator it = d_assertionToSignature.find(node);
   Assert (it != d_assertionToSignature.end());
-  Node generalized_signature = getGeneralization(it->second); 
-  return generalized_signature; 
+  Node generalized_signature = getGeneralization(it->second);
+  return generalized_signature;
 }
 
 Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
   if (cache.find(node) != cache.end()) {
-    return cache.find(node)->second; 
+    return cache.find(node)->second;
   }
-  
+
   if (node.getNumChildren() == 0) {
     if (node.getKind() == kind::CONST_BITVECTOR)
       return node;
 
     Node sig = getSignatureSkolem(node);
-    cache[node] = sig; 
-    return sig; 
+    cache[node] = sig;
+    return sig;
   }
 
   NodeBuilder<> builder(node.getKind());
@@ -308,30 +308,30 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
   }
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     Node converted = computeSignatureRec(node[i], cache);
-    builder << converted; 
+    builder << converted;
   }
   Node result = builder;
   cache[node] = result;
-  return result; 
+  return result;
 }
 
-/** 
+/**
  * Returns 0, if the two are equal,
  * 1 if s is a generalization of t
  * 2 if t is a generalization of s
  * -1 if the two cannot be unified
  *
- * @param s 
- * @param t 
- * 
- * @return 
+ * @param s
+ * @param t
+ *
+ * @return
  */
 int AbstractionModule::comparePatterns(TNode s, TNode t) {
   if (s.getKind() == kind::SKOLEM &&
       t.getKind() == kind::SKOLEM) {
     return 0;
   }
-  
+
   if (s.getKind() == kind::CONST_BITVECTOR &&
       t.getKind() == kind::CONST_BITVECTOR) {
     if (s == t) {
@@ -350,7 +350,7 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) {
       t.getKind() == kind::SKOLEM) {
     return 2;
   }
-  
+
   if (s.getNumChildren() != t.getNumChildren() ||
       s.getKind() != t.getKind())
     return -1;
@@ -370,26 +370,26 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) {
 }
 
 TNode AbstractionModule::getGeneralization(TNode term) {
-  NodeNodeMap::iterator it = d_sigToGeneralization.find(term); 
+  NodeNodeMap::iterator it = d_sigToGeneralization.find(term);
   // if not in the map we add it
   if (it == d_sigToGeneralization.end()) {
     d_sigToGeneralization[term] = term;
-    return term; 
+    return term;
   }
-  // doesn't have a generalization 
+  // doesn't have a generalization
   if (it->second == term)
     return term;
-  
+
   TNode generalization = getGeneralization(it->second);
   Assert (generalization != term);
   d_sigToGeneralization[term] = generalization;
-  return generalization; 
+  return generalization;
 }
 
 void AbstractionModule::storeGeneralization(TNode s, TNode t) {
   Assert (s == getGeneralization(s));
   Assert (t == getGeneralization(t));
-  d_sigToGeneralization[s] = t; 
+  d_sigToGeneralization[s] = t;
 }
 
 void AbstractionModule::finalizeSignatures() {
@@ -402,29 +402,29 @@ void AbstractionModule::finalizeSignatures() {
     for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) {
       TNode t = getGeneralization(tt->first);
       TNode s = getGeneralization(ss->first);
-      
+
       if (t != s) {
         int status = comparePatterns(s, t);
-        Assert (status); 
+        Assert (status);
         if (status < 0)
           continue;
         if (status == 1) {
-          storeGeneralization(t, s); 
+          storeGeneralization(t, s);
         } else {
-          storeGeneralization(s, t); 
+          storeGeneralization(s, t);
         }
       }
     }
   }
   // keep only most general signatures
   for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
-    TNode sig = it->first; 
+    TNode sig = it->first;
     TNode gen = getGeneralization(sig);
     if (sig != gen) {
-      Assert (d_signatures.find(gen) != d_signatures.end()); 
+      Assert (d_signatures.find(gen) != d_signatures.end());
       // update the count
       d_signatures[gen]+= d_signatures[sig];
-      d_signatures.erase(it++); 
+      d_signatures.erase(it++);
     } else {
       ++it;
     }
@@ -434,12 +434,12 @@ void AbstractionModule::finalizeSignatures() {
   // remove signatures that are not frequent enough
   for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
     if (it->second <= 7) {
-      d_signatures.erase(it++); 
+      d_signatures.erase(it++);
     } else {
       ++it;
     }
   }
-  
+
   for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) {
     TNode signature = it->first;
     // we already processed this signature
@@ -451,31 +451,31 @@ void AbstractionModule::finalizeSignatures() {
     collectArgumentTypes(signature, arg_types, seen);
     Assert (signature.getType().isBoolean());
     // make function return a bitvector of size 1
-    //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); 
+    //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u));
     TypeNode range = NodeManager::currentNM()->mkBitVectorType(1);
-    
+
     TypeNode abs_type = nm->mkFunctionType(arg_types, range);
     Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory");
     Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n";
 
     // NOTE: signature expression type is BOOLEAN
     d_signatureToFunc[signature] = abs_func;
-    d_funcToSignature[abs_func] = signature; 
+    d_funcToSignature[abs_func] = signature;
   }
 
   d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size());
-  
+
   Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n";
 }
 
 void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) {
   if (seen.find(sig) != seen.end())
     return;
-  
+
   if (sig.getKind() == kind::SKOLEM) {
     types.push_back(sig.getType());
-    seen.insert(sig); 
-    return; 
+    seen.insert(sig);
+    return;
   }
 
   for (unsigned i = 0; i < sig.getNumChildren(); ++i) {
@@ -487,36 +487,36 @@ void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& t
 void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector<Node>& args, TNodeSet& seen) {
   if (seen.find(node)!= seen.end())
     return;
-  
+
   if (node.getKind() == kind::VARIABLE ||
       node.getKind() == kind::CONST_BITVECTOR) {
     // a constant in the node can either map to an argument of the abstraction
-    // or can be hard-coded and part of the abstraction 
+    // or can be hard-coded and part of the abstraction
     if (signature.getKind() == kind::SKOLEM) {
       args.push_back(node);
       seen.insert(node);
     } else {
-      Assert (signature.getKind() == kind::CONST_BITVECTOR); 
+      Assert (signature.getKind() == kind::CONST_BITVECTOR);
     }
-    // 
-    return; 
+    //
+    return;
   }
   Assert (node.getKind() == signature.getKind() &&
-          node.getNumChildren() == signature.getNumChildren()); 
+          node.getNumChildren() == signature.getNumChildren());
 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-    collectArguments(node[i], signature[i], args, seen); 
-    seen.insert(node); 
+    collectArguments(node[i], signature[i], args, seen);
+    seen.insert(node);
   }
 }
 
 
 Node AbstractionModule::abstractSignatures(TNode assertion) {
-  Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; 
+  Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n";
   // assume the assertion has been fully abstracted
   Node signature = getGeneralizedSignature(assertion);
-  
-  Debug("bv-abstraction") << "   with sig "<< signature <<"\n"; 
+
+  Debug("bv-abstraction") << "   with sig "<< signature <<"\n";
   NodeNodeMap::iterator it = d_signatureToFunc.find(signature);
   if (it!= d_signatureToFunc.end()) {
     std::vector<Node> args;
@@ -527,16 +527,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) {
     collectArguments(assertion, signature, args, seen);
     std::vector<TNode> real_args;
     for (unsigned i = 1; i < args.size(); ++i) {
-      real_args.push_back(args[i]); 
+      real_args.push_back(args[i]);
     }
-    d_argsTable.addEntry(func, real_args); 
-    Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), 
+    d_argsTable.addEntry(func, real_args);
+    Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args),
                                 utils::mkConst(1, 1u));
-    Debug("bv-abstraction") << "=>   "<< result << "\n"; 
-    Assert (result.getType() == assertion.getType()); 
-    return result; 
+    Debug("bv-abstraction") << "=>   "<< result << "\n";
+    Assert (result.getType() == assertion.getType());
+    return result;
   }
-  return assertion; 
+  return assertion;
 }
 
 bool AbstractionModule::isAbstraction(TNode node) {
@@ -557,11 +557,11 @@ bool AbstractionModule::isAbstraction(TNode node) {
   if (constant != utils::mkConst(1, 1u))
     return false;
 
-  TNode func_symbol = func.getOperator(); 
+  TNode func_symbol = func.getOperator();
   if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end())
     return false;
 
-  return true; 
+  return true;
 }
 
 Node AbstractionModule::getInterpretation(TNode node) {
@@ -571,51 +571,51 @@ Node AbstractionModule::getInterpretation(TNode node) {
   Assert (constant.getKind() == kind::CONST_BITVECTOR &&
           apply.getKind() == kind::APPLY_UF);
 
-  Node func = apply.getOperator(); 
+  Node func = apply.getOperator();
   Assert (d_funcToSignature.find(func) != d_funcToSignature.end());
-  
+
   Node sig = d_funcToSignature[func];
-  
+
   // substitute arguments in signature
   TNodeTNodeMap seen;
   unsigned index = 0;
   Node result = substituteArguments(sig, apply, index, seen);
-  Assert (result.getType().isBoolean()); 
+  Assert (result.getType().isBoolean());
   Assert (index == apply.getNumChildren());
   // Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n";
   // Debug("bv-abstraction") << "    => " << result << "\n";
-  return result; 
+  return result;
 }
 
 Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) {
   if (seen.find(signature) != seen.end()) {
-    return seen[signature]; 
+    return seen[signature];
   }
-  
+
   if (signature.getKind() == kind::SKOLEM) {
     // return corresponding argument and increment counter
     seen[signature] = apply[index];
-    return apply[index++]; 
+    return apply[index++];
   }
 
   if (signature.getNumChildren() == 0) {
     Assert (signature.getKind() != kind::VARIABLE &&
-            signature.getKind() != kind::SKOLEM); 
+            signature.getKind() != kind::SKOLEM);
     seen[signature] = signature;
-    return signature; 
+    return signature;
   }
-  
+
   NodeBuilder<> builder(signature.getKind());
   if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
     builder << signature.getOperator();
   }
-  
+
   for (unsigned i = 0; i < signature.getNumChildren(); ++i) {
     Node child = substituteArguments(signature[i], apply, index, seen);
-    builder << child; 
+    builder << child;
   }
 
-  Node result = builder; 
+  Node result = builder;
   seen[signature]= result;
 
   return result;
@@ -625,20 +625,20 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
   if (Dump.isOn("bv-abstraction")) {
     NodeNodeMap seen;
     Node c = reverseAbstraction(conflict, seen);
-    Dump("bv-abstraction") << PushCommand(); 
+    Dump("bv-abstraction") << PushCommand();
     Dump("bv-abstraction") << AssertCommand(c.toExpr());
     Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand(); 
+    Dump("bv-abstraction") << PopCommand();
   }
 
-  Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; 
+  Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
   if (conflict.getKind() != kind::AND)
-    return conflict; 
+    return conflict;
 
   std::vector<Node> conjuncts;
   for (unsigned i = 0; i < conflict.getNumChildren(); ++i)
     conjuncts.push_back(conflict[i]);
-  
+
   theory::SubstitutionMap subst(new context::Context());
   for (unsigned i = 0; i < conjuncts.size(); ++i) {
     TNode conjunct = conjuncts[i];
@@ -658,12 +658,12 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
       } else {
         continue;
       }
-      
+
       Assert (!subst.hasSubstitution(s));
       Assert (!t.isNull() &&
               !s.isNull() &&
               s!= t);
-      subst.addSubstitution(s, t); 
+      subst.addSubstitution(s, t);
 
       for (unsigned k = 0; k < conjuncts.size(); k++) {
         conjuncts[k] = subst.apply(conjuncts[k]);
@@ -671,28 +671,28 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
     }
   }
   Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts));
-  
+
   Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
   Debug("bv-abstraction") << "   => " << new_conflict <<"\n";
 
   if (Dump.isOn("bv-abstraction")) {
-    
+
     NodeNodeMap seen;
     Node nc = reverseAbstraction(new_conflict, seen);
-    Dump("bv-abstraction") << PushCommand(); 
+    Dump("bv-abstraction") << PushCommand();
     Dump("bv-abstraction") << AssertCommand(nc.toExpr());
     Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand(); 
+    Dump("bv-abstraction") << PopCommand();
   }
-  
-  return new_conflict; 
+
+  return new_conflict;
 }
 
 
 void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instantiations,
                               const std::vector<TNode> functions) {
   // print header
-  Debug("bv-abstraction-dbg") <<"[ "; 
+  Debug("bv-abstraction-dbg") <<"[ ";
   for (unsigned i = 0; i < functions.size(); ++i) {
     for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) {
       Debug("bv-abstraction-dgb") << functions[i][j] <<" ";
@@ -706,16 +706,16 @@ void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instant
     const std::vector<ArgsVec>& inst = instantiations[i];
     for (unsigned j = 0; j < inst.size(); ++j) {
       for (unsigned k = 0; k < inst[j].size(); ++k) {
-        Debug("bv-abstraction-dbg") << inst[j][k] << " "; 
+        Debug("bv-abstraction-dbg") << inst[j][k] << " ";
       }
-      Debug("bv-abstraction-dbg") << " || "; 
+      Debug("bv-abstraction-dbg") << " || ";
     }
     Debug("bv-abstraction-dbg") <<"]\n";
   }
 }
 
 void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& lemmas) {
-  Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; 
+  Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n";
   std::vector<TNode> functions;
 
   // collect abstract functions
@@ -737,11 +737,11 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
   // if (functions.size() >= 3) {
   //   // dump conflict
   //   NodeNodeMap seen;
-  //   Node reversed = reverseAbstraction(conflict, seen); 
-  //   std::cout << "CONFLICT " << reversed << "\n"; 
+  //   Node reversed = reverseAbstraction(conflict, seen);
+  //   std::cout << "CONFLICT " << reversed << "\n";
   // }
 
-  
+
   if (functions.size() == 0 || functions.size() > options::bvNumFunc()) {
     return;
   }
@@ -751,31 +751,31 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
   SubstitutionMap skolem_subst(new context::Context());
   SubstitutionMap reverse_skolem(new context::Context());
   makeFreshSkolems(conflict, skolem_subst, reverse_skolem);
-  
+
   Node skolemized_conflict = skolem_subst.apply(conflict);
   for (unsigned i = 0; i < functions.size(); ++i) {
     functions[i] = skolem_subst.apply(functions[i]);
   }
 
-  conflict = skolem_subst.apply(conflict); 
+  conflict = skolem_subst.apply(conflict);
 
   LemmaInstantiatior inst(functions, d_argsTable, conflict);
   std::vector<Node> new_lemmas;
-  inst.generateInstantiations(new_lemmas); 
+  inst.generateInstantiations(new_lemmas);
   for (unsigned i = 0; i < new_lemmas.size(); ++i) {
     TNode lemma = reverse_skolem.apply(new_lemmas[i]);
     if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) {
       lemmas.push_back(lemma);
-      Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; 
+      Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
       storeLemma(lemma);
 
       if (Dump.isOn("bv-abstraction")) {
         NodeNodeMap seen;
         Node l = reverseAbstraction(lemma, seen);
-        Dump("bv-abstraction") << PushCommand(); 
+        Dump("bv-abstraction") << PushCommand();
         Dump("bv-abstraction") << AssertCommand(l.toExpr());
         Dump("bv-abstraction") << CheckSatCommand();
-        Dump("bv-abstraction") << PopCommand(); 
+        Dump("bv-abstraction") << PopCommand();
       }
     }
   }
@@ -787,18 +787,18 @@ int AbstractionModule::LemmaInstantiatior::next(int val, int index) {
   return -1;
 }
 
-/** 
+/**
  * Assumes the stack without top is consistent, and checks that the
  * full stack is consistent
- * 
- * @param stack 
- * 
- * @return 
+ *
+ * @param stack
+ *
+ * @return
  */
 bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stack) {
   if (stack.empty())
     return true;
-  
+
   unsigned current = stack.size() - 1;
   TNode func = d_functions[current];
   ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator());
@@ -807,12 +807,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
   for (unsigned k = 0; k < args.size(); ++k) {
     TNode s = func[k];
     TNode t = args[k];
-      
+
     TNode s0 = s;
     while (d_subst.hasSubstitution(s0)) {
       s0 = d_subst.getSubstitution(s0);
     }
-    
+
     TNode t0 = t;
     while (d_subst.hasSubstitution(t0)) {
       t0 = d_subst.getSubstitution(t0);
@@ -824,7 +824,7 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
       else
         continue;
     }
-      
+
     if(s0.getMetaKind() == kind::metakind::VARIABLE &&
        t0.isConst()) {
       d_subst.addSubstitution(s0, t0);
@@ -839,12 +839,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
 
     Assert (s0.getMetaKind() == kind::metakind::VARIABLE &&
             t0.getMetaKind() == kind::metakind::VARIABLE);
-      
+
     if (s0 != t0) {
       d_subst.addSubstitution(s0, t0);
     }
   }
-  return true; 
+  return true;
 }
 
 bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
@@ -854,13 +854,13 @@ bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
 void AbstractionModule::LemmaInstantiatior::mkLemma() {
   Node lemma = d_subst.apply(d_conflict);
   // Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n";
-  d_lemmas.push_back(lemma); 
+  d_lemmas.push_back(lemma);
 }
 
 void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
   if (!isConsistent(stack))
     return;
-  
+
   if (accept(stack)) {
     mkLemma();
     return;
@@ -871,7 +871,7 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
     d_ctx->push();
     stack.push_back(x);
     backtrack(stack);
-    
+
     d_ctx->pop();
     stack.pop_back();
     x = next(x, stack.size());
@@ -880,13 +880,13 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
 
 
 void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<Node>& lemmas) {
-  Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; 
+  Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations ";
 
   std::vector<int> stack;
   backtrack(stack);
-  Assert (d_ctx->getLevel() == 0); 
-  Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; 
-  lemmas.swap(d_lemmas); 
+  Assert (d_ctx->getLevel() == 0);
+  Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n";
+  lemmas.swap(d_lemmas);
 }
 
 void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) {
@@ -910,7 +910,7 @@ void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, Subst
 void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) {
   Assert (fresh_args.size() == 0);
   Assert (func.getKind() == kind::APPLY_UF);
-  TNodeNodeMap d_map; 
+  TNodeNodeMap d_map;
   for (unsigned i = 0; i < func.getNumChildren(); ++i) {
     TNode arg = func[i];
     if (arg.isConst()) {
@@ -918,9 +918,9 @@ void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args)
       continue;
     }
     Assert (arg.getMetaKind() == kind::metakind::VARIABLE);
-    TNodeNodeMap::iterator it = d_map.find(arg); 
+    TNodeNodeMap::iterator it = d_map.find(arg);
     if (it != d_map.end()) {
-      fresh_args.push_back(it->second); 
+      fresh_args.push_back(it->second);
     } else {
       Node skolem = utils::mkVar(utils::getSize(arg));
       d_map[arg] = skolem;
@@ -947,7 +947,7 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect
     Debug("bv-abstraction-dbg") <<"\n";
   }
 
-  
+
   SubstitutionMap subst(new context::Context());
 
   for (unsigned i = 0; i < ss.size(); ++i) {
@@ -982,10 +982,10 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect
     Assert (s0 != t0);
     subst.addSubstitution(s0, t0);
   }
-  
+
   Node res = subst.apply(conflict);
-  Debug("bv-abstraction-dbg") << "  Lemma: " << res <<"\n"; 
-  return res; 
+  Debug("bv-abstraction-dbg") << "  Lemma: " << res <<"\n";
+  return res;
 }
 
 void AbstractionModule::storeLemma(TNode lemma) {
@@ -996,7 +996,7 @@ void AbstractionModule::storeLemma(TNode lemma) {
       atom = atom.getKind() == kind::NOT ? atom[0] : atom;
       Assert (atom.getKind() != kind::NOT);
       Assert (utils::isBVPredicate(atom));
-      d_lemmaAtoms.insert(atom); 
+      d_lemmaAtoms.insert(atom);
     }
   } else {
     lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma;
@@ -1009,9 +1009,9 @@ void AbstractionModule::storeLemma(TNode lemma) {
 bool AbstractionModule::isLemmaAtom(TNode node) const {
   Assert (node.getType().isBoolean());
   node = node.getKind() == kind::NOT? node[0] : node;
-  
+
   return d_inputAtoms.find(node) == d_inputAtoms.end() &&
-    d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); 
+    d_lemmaAtoms.find(node) != d_lemmaAtoms.end();
 }
 
 void AbstractionModule::addInputAtom(TNode atom) {
@@ -1022,31 +1022,31 @@ void AbstractionModule::addInputAtom(TNode atom) {
 
 void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) {
   Assert (args.size() == d_arity);
-  d_data.push_back(args); 
+  d_data.push_back(args);
 }
 
 void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) {
   if (d_data.find(signature) == d_data.end()) {
-    d_data[signature] = ArgsTableEntry(args.size()); 
+    d_data[signature] = ArgsTableEntry(args.size());
   }
   ArgsTableEntry& entry = d_data[signature];
-  entry.addArguments(args); 
+  entry.addArguments(args);
 }
 
 
 bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const {
-  return d_data.find(signature) != d_data.end(); 
+  return d_data.find(signature) != d_data.end();
 }
 
 AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) {
   Assert (hasEntry(signature));
-  return d_data.find(signature)->second; 
+  return d_data.find(signature)->second;
 }
 
-AbstractionModule::Statistics::Statistics()
-  : d_numFunctionsAbstracted("theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
-  , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0)
-  , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime")
+AbstractionModule::Statistics::Statistics(const std::string& name)
+  : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
+  , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0)
+  , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime")
 {
   smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
   smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 5d580f6ce..5d48b926e 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -38,11 +38,11 @@ class AbstractionModule {
     IntStat d_numFunctionsAbstracted;
     IntStat d_numArgsSkolemized;
     TimerStat d_abstractionTime;
-    Statistics();
+    Statistics(const std::string& name);
     ~Statistics();
   };
 
-  
+
   class ArgsTableEntry {
     std::vector<ArgsVec> d_data;
     unsigned d_arity;
@@ -61,11 +61,11 @@ class AbstractionModule {
     unsigned getArity() { return d_arity; }
     unsigned getNumEntries() { return d_data.size(); }
     ArgsVec& getEntry(unsigned i ) { Assert (i < d_data.size()); return d_data[i]; }
-  }; 
+  };
 
   class ArgsTable {
     __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
-    bool hasEntry(TNode signature) const; 
+    bool hasEntry(TNode signature) const;
   public:
     typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
     ArgsTable() {}
@@ -75,12 +75,12 @@ class AbstractionModule {
     iterator end() { return d_data.end(); }
   };
 
-  /** 
+  /**
    * Checks if one pattern is a generalization of the other
-   * 
-   * @param s 
-   * @param t 
-   * 
+   *
+   * @param s
+   * @param t
+   *
    * @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable
    */
   static int comparePatterns(TNode s, TNode t);
@@ -93,7 +93,7 @@ class AbstractionModule {
     theory::SubstitutionMap d_subst;
     TNode d_conflict;
     std::vector<Node> d_lemmas;
-    
+
     void backtrack(std::vector<int>& stack);
     int next(int val, int index);
     bool isConsistent(const std::vector<int>& stack);
@@ -108,7 +108,7 @@ class AbstractionModule {
       , d_conflict(conflict)
       , d_lemmas()
     {
-      Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n"; 
+      Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n";
       // initializing the search space
       for (unsigned i = 0; i < functions.size(); ++i) {
         TNode func_op = functions[i].getOperator();
@@ -118,31 +118,31 @@ class AbstractionModule {
       }
     }
 
-    void generateInstantiations(std::vector<Node>& lemmas); 
-    
+    void generateInstantiations(std::vector<Node>& lemmas);
+
   };
-  
+
   typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
   typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
   typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
   typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap; 
+  typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap;
   typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap;
   typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap;
   typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
-  
-  ArgsTable d_argsTable; 
+
+  ArgsTable d_argsTable;
 
   // mapping between signature and uninterpreted function symbol used to
   // abstract the signature
   NodeNodeMap d_signatureToFunc;
-  NodeNodeMap d_funcToSignature; 
+  NodeNodeMap d_funcToSignature;
 
-  NodeNodeMap d_assertionToSignature; 
+  NodeNodeMap d_assertionToSignature;
   SignatureMap d_signatures;
-  NodeNodeMap d_sigToGeneralization; 
+  NodeNodeMap d_sigToGeneralization;
   TNodeSet d_skolems;
 
   // skolems maps
@@ -165,7 +165,7 @@ class AbstractionModule {
   Node getGeneralizedSignature(Node node);
   Node getSignatureSkolem(TNode node);
 
-  unsigned getBitwidthIndex(unsigned bitwidth); 
+  unsigned getBitwidthIndex(unsigned bitwidth);
   void resetSignatureIndex();
   Node computeSignatureRec(TNode, NodeNodeMap&);
   void storeSignature(Node signature, TNode assertion);
@@ -175,14 +175,14 @@ class AbstractionModule {
 
   // crazy instantiation methods
   void generateInstantiations(unsigned current,
-                              std::vector<ArgsTableEntry>& matches, 
+                              std::vector<ArgsTableEntry>& matches,
                               std::vector<std::vector<ArgsVec> >& instantiations,
                               std::vector<std::vector<ArgsVec> >& new_instantiations);
 
   Node tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict);
   void makeFreshArgs(TNode func, std::vector<Node>& fresh_args);
   void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map);
-  
+
   void skolemizeArguments(std::vector<Node>& assertions);
   Node reverseAbstraction(Node assertion, NodeNodeMap& seen);
 
@@ -192,9 +192,9 @@ class AbstractionModule {
   void storeLemma(TNode lemma);
 
   Statistics d_statistics;
-  
+
 public:
-  AbstractionModule()
+  AbstractionModule(const std::string& name)
     : d_argsTable()
     , d_signatureToFunc()
     , d_funcToSignature()
@@ -207,34 +207,34 @@ public:
     , d_addedLemmas()
     , d_lemmaAtoms()
     , d_inputAtoms()
-    , d_statistics()
+    , d_statistics(name)
   {}
-  /** 
+  /**
    * returns true if there are new uninterepreted functions symbols in the output
-   * 
-   * @param assertions 
-   * @param new_assertions 
-   * 
-   * @return 
+   *
+   * @param assertions
+   * @param new_assertions
+   *
+   * @return
    */
   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-  /** 
-   * Returns true if the node represents an abstraction predicate. 
-   * 
-   * @param node 
-   * 
-   * @return 
+  /**
+   * Returns true if the node represents an abstraction predicate.
+   *
+   * @param node
+   *
+   * @return
    */
   bool isAbstraction(TNode node);
-  /** 
-   * Returns the interpretation of the abstraction predicate. 
-   * 
-   * @param node 
-   * 
-   * @return 
+  /**
+   * Returns the interpretation of the abstraction predicate.
+   *
+   * @param node
+   *
+   * @return
    */
   Node getInterpretation(TNode node);
-  Node simplifyConflict(TNode conflict); 
+  Node simplifyConflict(TNode conflict);
   void generalizeConflict(TNode conflict, std::vector<Node>& lemmas);
   void addInputAtom(TNode atom);
   bool isLemmaAtom(TNode node) const;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index b7619c4bb..6c6c13ee8 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -37,9 +37,9 @@ namespace bv {
 
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
-    d_bitblaster(new TLazyBitblaster(c, bv, "lazy")),
+    d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")),
     d_bitblastQueue(c),
-    d_statistics(),
+    d_statistics(bv->getFullInstanceName()),
     d_validModelCache(c, true),
     d_lemmaAtomsQueue(c),
     d_useSatPropagation(options::bitvectorPropagate()),
@@ -55,9 +55,9 @@ BitblastSolver::~BitblastSolver() {
   delete d_bitblaster;
 }
 
-BitblastSolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
-  , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+BitblastSolver::Statistics::Statistics(const std::string &instanceName)
+  : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0)
+  , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
@@ -68,8 +68,8 @@ BitblastSolver::Statistics::~Statistics() {
 }
 
 void BitblastSolver::setAbstraction(AbstractionModule* abs) {
-  d_abstractionModule = abs; 
-  d_bitblaster->setAbstraction(abs); 
+  d_abstractionModule = abs;
+  d_bitblaster->setAbstraction(abs);
 }
 
 void BitblastSolver::preRegister(TNode node) {
@@ -117,7 +117,7 @@ void BitblastSolver::bitblastQueue() {
 
 bool BitblastSolver::check(Theory::Effort e) {
   Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); 
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
 
   ++(d_statistics.d_numCallstoCheck);
 
@@ -135,10 +135,10 @@ bool BitblastSolver::check(Theory::Effort e) {
       // skip atoms that are the result of abstraction lemmas
       if (d_abstractionModule->isLemmaAtom(fact)) {
         d_lemmaAtomsQueue.push_back(fact);
-        continue; 
+        continue;
       }
     }
-    
+
     if (!d_bv->inConflict() &&
         (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
@@ -183,7 +183,7 @@ bool BitblastSolver::check(Theory::Effort e) {
   if (options::bvAbstraction() &&
       e == Theory::EFFORT_FULL &&
       d_lemmaAtomsQueue.size()) {
-    
+
     // bit-blast lemma atoms
     while(!d_lemmaAtomsQueue.empty()) {
       TNode lemma_atom = d_lemmaAtomsQueue.front();
@@ -199,7 +199,7 @@ bool BitblastSolver::check(Theory::Effort e) {
         return false;
       }
     }
-    
+
     Assert(!d_bv->inConflict());
     bool ok = d_bitblaster->solve();
     if (!ok) {
@@ -210,9 +210,9 @@ bool BitblastSolver::check(Theory::Effort e) {
       ++(d_statistics.d_numBBLemmas);
       return false;
     }
-    
+
   }
-  
+
 
   return true;
 }
@@ -228,9 +228,9 @@ void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
 Node BitblastSolver::getModelValue(TNode node)
 {
   if (d_bv->d_invalidateModelCache.get()) {
-    d_bitblaster->invalidateModelCache(); 
+    d_bitblaster->invalidateModelCache();
   }
-  d_bv->d_invalidateModelCache.set(false); 
+  d_bv->d_invalidateModelCache.set(false);
   Node val = d_bitblaster->getTermModel(node, true);
   return val;
 }
@@ -241,9 +241,9 @@ void BitblastSolver::setConflict(TNode conflict) {
   Node final_conflict = conflict;
   if (options::bitvectorQuickXplain() &&
       conflict.getKind() == kind::AND) {
-    // std::cout << "Original conflict " << conflict.getNumChildren() << "\n"; 
+    // std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
     final_conflict = d_quickXplain->minimizeConflict(conflict);
-    //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n"; 
+    //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
   }
   d_bv->setConflict(final_conflict);
 }
@@ -256,4 +256,3 @@ void BitblastSolver::setProofLog( BitVectorProof * bvp ) {
 }/* 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 e9300138b..fe16d2702 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -37,7 +37,7 @@ class BitblastSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     IntStat d_numBBLemmas;
-    Statistics();
+    Statistics(const std::string &instanceName);
     ~Statistics();
   };
   /** Bitblaster */
@@ -71,8 +71,8 @@ public:
   Node getModelValue(TNode node);
   bool isComplete() { return true; }
   void bitblastQueue();
-  void setAbstraction(AbstractionModule* module); 
-  uint64_t computeAtomWeight(TNode atom); 
+  void setAbstraction(AbstractionModule* module);
+  uint64_t computeAtomWeight(TNode atom);
   void setProofLog( BitVectorProof * bvp );
 };
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index f5b2175f3..fec93e033 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -42,14 +42,16 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
-  : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
+                   OutputChannel& out, Valuation valuation,
+                   const LogicInfo& logicInfo, std::string name)
+  : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
     d_subtheories(),
     d_subtheoryMap(),
-    d_statistics(),
+    d_statistics(getFullInstanceName()),
     d_staticLearnCache(),
     d_BVDivByZero(),
     d_BVRemByZero(),
@@ -62,7 +64,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c),
     d_eagerSolver(NULL),
-    d_abstractionModule(new AbstractionModule()),
+    d_abstractionModule(new AbstractionModule(getFullInstanceName())),
     d_isCoreTheory(false),
     d_calledPreregister(false)
 {
@@ -119,14 +121,14 @@ void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) {
   getOutputChannel().spendResource(ammount);
 }
 
-TheoryBV::Statistics::Statistics():
-  d_avgConflictSize("theory::bv::AvgBVConflictSize"),
-  d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
-  d_solveTimer("theory::bv::solveTimer"),
-  d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
-  d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0),
-  d_weightComputationTimer("theory::bv::weightComputationTimer"),
-  d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
+TheoryBV::Statistics::Statistics(const std::string &name):
+  d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"),
+  d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0),
+  d_solveTimer(name + "theory::bv::solveTimer"),
+  d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0),
+  d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0),
+  d_weightComputationTimer(name + "theory::bv::weightComputationTimer"),
+  d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
@@ -234,7 +236,7 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
         for (unsigned i = 0; i < args1.getNumChildren(); ++i) {
           eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
         }
-        
+
         Node args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs);
         Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
         Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
@@ -276,9 +278,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 
     // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     //   // Ackermanize UF if using eager bit-blasting
-    //   Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); 
+    //   Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
     //   node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
-    //   return node; 
+    //   return node;
     // } else {
       Node divByZero = getBVDivByZero(node.getKind(), width);
       Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
@@ -327,7 +329,7 @@ void TheoryBV::sendConflict() {
   if (d_conflictNode.isNull()) {
     return;
   } else {
-    Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+    Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
     d_out->conflict(d_conflictNode);
     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     d_conflictNode = Node::null();
@@ -703,7 +705,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"; 
+  Debug("bitvector::explain") << "TheoryBV::explain done. \n";
   return explanation;
 }
 
@@ -723,7 +725,7 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
     return EQUALITY_UNKNOWN;
-  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); 
+  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 7f0494dc1..ba2a4fc2a 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -56,7 +56,8 @@ class TheoryBV : public Theory {
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo);
+           Valuation valuation, const LogicInfo& logicInfo,
+           std::string name = "");
 
   ~TheoryBV();
 
@@ -88,8 +89,8 @@ public:
 
   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:
@@ -100,10 +101,10 @@ private:
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;
     IntStat     d_numCallsToCheckFullEffort;
-    IntStat     d_numCallsToCheckStandardEffort; 
+    IntStat     d_numCallsToCheckStandardEffort;
     TimerStat   d_weightComputationTimer;
     IntStat     d_numMultSlice;
-    Statistics();
+    Statistics(const std::string &name);
     ~Statistics();
   };
 
@@ -121,12 +122,12 @@ private:
    */
   Node getBVDivByZero(Kind k, unsigned width);
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
   void collectFunctionSymbols(TNode term, TNodeSet& seen);
   void storeFunction(TNode func, TNode term);
   typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_staticLearnCache;
-  
+
   /**
    * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
@@ -142,7 +143,7 @@ private:
   CVC4::theory::SubstitutionMap d_funcToSkolem;
 
   context::CDO<bool> d_lemmasAdded;
-  
+
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
@@ -165,17 +166,17 @@ private:
   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
   PropagatedMap d_propagatedBy;
 
-  EagerBitblastSolver* d_eagerSolver; 
+  EagerBitblastSolver* d_eagerSolver;
   AbstractionModule* d_abstractionModule;
   bool d_isCoreTheory;
   bool d_calledPreregister;
-  
+
   bool wasPropagatedBySubtheory(TNode literal) const {
-    return d_propagatedBy.find(literal) != d_propagatedBy.end(); 
+    return d_propagatedBy.find(literal) != d_propagatedBy.end();
   }
-  
+
   SubTheory getPropagatingSubtheory(TNode literal) const {
-    Assert(wasPropagatedBySubtheory(literal)); 
+    Assert(wasPropagatedBySubtheory(literal));
     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
     return (*find).second;
   }
@@ -191,7 +192,7 @@ private:
   void addSharedTerm(TNode t);
 
   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
-  
+
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   Node getModelValue(TNode var);
@@ -212,7 +213,7 @@ private:
 
   void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
 
-  void checkForLemma(TNode node); 
+  void checkForLemma(TNode node);
 
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1ab4c228b..618fda4c0 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,6 +26,8 @@
 #include "options/bv_options.h"
 #include "options/options.h"
 #include "options/quantifiers_options.h"
+#include "proof/cnf_proof.h"
+#include "proof/lemma_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
 #include "smt/ite_removal.h"
@@ -53,6 +55,104 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
+inline void flattenAnd(Node n, std::vector<TNode>& out){
+  Assert(n.getKind() == kind::AND);
+  for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
+    Node curr = *i;
+    if(curr.getKind() == kind::AND){
+      flattenAnd(curr, out);
+    }else{
+      out.push_back(curr);
+    }
+  }
+}
+
+inline Node flattenAnd(Node n){
+  std::vector<TNode> out;
+  flattenAnd(n, out);
+  return NodeManager::currentNM()->mkNode(kind::AND, out);
+}
+
+theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
+                                                             ProofRule rule,
+                                                             bool removable,
+                                                             bool preprocess,
+                                                             bool sendAtoms)
+  throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl;
+  ++ d_statistics.lemmas;
+  d_engine->d_outputChannelUsed = true;
+
+  LemmaProofRecipe* proofRecipe = NULL;
+  PROOF({
+      // Theory lemmas have one step that proves the empty clause
+      proofRecipe = new LemmaProofRecipe;
+
+      Node emptyNode;
+      LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode);
+
+      Node rewritten;
+      if (lemma.getKind() == kind::OR) {
+        for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
+          rewritten = theory::Rewriter::rewrite(lemma[i]);
+          if (rewritten != lemma[i]) {
+            proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate());
+          }
+          proofStep.addAssertion(lemma[i]);
+          proofRecipe->addBaseAssertion(rewritten);
+        }
+      } else {
+        rewritten = theory::Rewriter::rewrite(lemma);
+        if (rewritten != lemma) {
+          proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate());
+        }
+        proofStep.addAssertion(lemma);
+        proofRecipe->addBaseAssertion(rewritten);
+      }
+      proofRecipe->addStep(proofStep);
+    });
+
+  theory::LemmaStatus result = d_engine->lemma(lemma,
+                                               rule,
+                                               false,
+                                               removable,
+                                               preprocess,
+                                               sendAtoms ? d_theory : theory::THEORY_LAST,
+                                               proofRecipe);
+  PROOF(delete proofRecipe;);
+  return result;
+}
+
+theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable)
+  throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
+  ++ d_statistics.lemmas;
+  d_engine->d_outputChannelUsed = true;
+
+
+  LemmaProofRecipe* proofRecipe = NULL;
+  Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl;
+  theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe);
+  return result;
+}
+
+bool TheoryEngine::EngineOutputChannel::propagate(TNode literal)
+  throw(AssertionException, UnsafeInterruptException) {
+  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
+  ++ d_statistics.propagations;
+  d_engine->d_outputChannelUsed = true;
+  return d_engine->propagate(literal, d_theory);
+}
+
+void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
+  throw(AssertionException, UnsafeInterruptException) {
+  Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
+  Assert (pf == NULL); // Theory shouldn't be producing proofs yet
+  ++ d_statistics.conflicts;
+  d_engine->d_outputChannelUsed = true;
+  d_engine->conflict(conflictNode, d_theory);
+}
+
 void TheoryEngine::finishInit() {
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
@@ -497,7 +597,10 @@ void TheoryEngine::combineTheories() {
 
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, carePair.theory);
+
+    LemmaProofRecipe* proofRecipe = NULL;
+    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe);
+
     // This code is supposed to force preference to follow what the theory models already have
     // but it doesn't seem to make a big difference - need to explore more -Clark
     // if (true) {
@@ -963,7 +1066,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the
 
 void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
 
-  Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl;
+  Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
 
   Assert(toTheoryId != fromTheoryId);
   if(toTheoryId != THEORY_SAT_SOLVER &&
@@ -1176,6 +1279,23 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
     }
   } else {
+    // We could be propagating a unit-clause lemma. In this case, we need to provide a
+    // recipe.
+    // TODO: Consider putting this someplace else? This is the only refence to the proof
+    // manager in this class.
+
+    PROOF({
+        LemmaProofRecipe proofRecipe;
+        proofRecipe.addBaseAssertion(literal);
+
+        Node emptyNode;
+        LemmaProofRecipe::ProofStep proofStep(theory, emptyNode);
+        proofStep.addAssertion(literal);
+        proofRecipe.addStep(proofStep);
+
+        ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
+      });
+
     // Just send off to the SAT solver
     Assert(d_propEngine->isSatLiteral(literal));
     assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
@@ -1270,7 +1390,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
   return conjunction;
 }
 
-NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) {
+Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
 
   bool polarity = node.getKind() != kind::NOT;
@@ -1278,32 +1398,90 @@ NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) {
 
   // If we're not in shared mode, explanations are simple
   if (!d_logicInfo.isSharingEnabled()) {
+    Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
+                             << " Responsible theory is: "
+                             << theoryOf(atom)->getId() << std::endl;
+
     Node explanation = theoryOf(atom)->explain(node);
     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
-    return NodeTheoryPair(explanation, theoryOf(atom)->getId());
+    PROOF({
+        if(proofRecipe) {
+          Node emptyNode;
+          LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode);
+          proofStep.addAssertion(node);
+          proofRecipe->addBaseAssertion(node);
+
+          if (explanation.getKind() == kind::AND) {
+            // If the explanation is a conjunction, the recipe for the corresponding lemma is
+            // the negation of its conjuncts.
+            Node flat = flattenAnd(explanation);
+            for (unsigned i = 0; i < flat.getNumChildren(); ++i) {
+              if (flat[i].isConst() && flat[i].getConst<bool>()) {
+                ++ i;
+                continue;
+              }
+              if (flat[i].getKind() == kind::NOT &&
+                  flat[i][0].isConst() && !flat[i][0].getConst<bool>()) {
+                ++ i;
+                continue;
+              }
+              Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
+                                       << flat[i].negate() << std::endl;
+              proofStep.addAssertion(flat[i].negate());
+              proofRecipe->addBaseAssertion(flat[i].negate());
+            }
+          } else {
+            // The recipe for proving it is by negating it. "True" is not an acceptable reason.
+            if (!((explanation.isConst() && explanation.getConst<bool>()) ||
+                  (explanation.getKind() == kind::NOT &&
+                   explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
+              proofStep.addAssertion(explanation.negate());
+              proofRecipe->addBaseAssertion(explanation.negate());
+            }
+          }
+
+          proofRecipe->addStep(proofStep);
+        }
+      });
+
+    return explanation;
   }
 
+  Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
+
   // Initial thing to explain
   NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
   Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
 
   NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
+  Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
+                           << nodeExplainerPair.node
+                           << " is theory: " << nodeExplainerPair.theory << std::endl;
   TheoryId explainer = nodeExplainerPair.theory;
 
   // Create the workplace for explanations
   std::vector<NodeTheoryPair> explanationVector;
   explanationVector.push_back(d_propagationMap[toExplain]);
   // Process the explanation
-  getExplanation(explanationVector);
+  if (proofRecipe) {
+    Node emptyNode;
+    LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode);
+    proofStep.addAssertion(node);
+    proofRecipe->addStep(proofStep);
+    proofRecipe->addBaseAssertion(node);
+  }
+
+  getExplanation(explanationVector, proofRecipe);
   Node explanation = mkExplanation(explanationVector);
 
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
 
-  return NodeTheoryPair(explanation, explainer);
+  return explanation;
 }
 
 Node TheoryEngine::getExplanation(TNode node) {
-  return getExplanationAndExplainer(node).node;
+  LemmaProofRecipe *dontCareRecipe = NULL;
+  return getExplanationAndRecipe(node, dontCareRecipe);
 }
 
 struct AtomsCollect {
@@ -1406,7 +1584,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         bool removable,
                                         bool preprocess,
                                         theory::TheoryId atomsTo,
-                                        theory::TheoryId ownerTheory) {
+                                        LemmaProofRecipe* proofRecipe) {
   // For resource-limiting (also does a time check).
   // spendResource();
 
@@ -1456,10 +1634,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, ownerTheory, node);
+  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node);
   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
     additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
-    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node);
+    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1493,22 +1671,69 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
                         << CheckSatCommand(conflict.toExpr());
   }
 
+  LemmaProofRecipe* proofRecipe = NULL;
+  PROOF({
+      proofRecipe = new LemmaProofRecipe;
+      Node emptyNode;
+      LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
+
+      if (conflict.getKind() == kind::AND) {
+        for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
+          proofStep.addAssertion(conflict[i].negate());
+        }
+      } else {
+        proofStep.addAssertion(conflict.negate());
+      }
+
+      proofRecipe->addStep(proofStep);
+    });
+
   // In the multiple-theories case, we need to reconstruct the conflict
   if (d_logicInfo.isSharingEnabled()) {
     // Create the workplace for explanations
     std::vector<NodeTheoryPair> explanationVector;
     explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
+
     // Process the explanation
-    getExplanation(explanationVector);
+    getExplanation(explanationVector, proofRecipe);
     Node fullConflict = mkExplanation(explanationVector);
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
-    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
+    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+
   } else {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
-    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
+    PROOF({
+        if (conflict.getKind() == kind::AND) {
+          // If the conflict is a conjunction, the corresponding lemma is derived by negating
+          // its conjuncts.
+          for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
+            if (conflict[i].isConst() && conflict[i].getConst<bool>()) {
+              ++ i;
+              continue;
+            }
+            if (conflict[i].getKind() == kind::NOT &&
+                conflict[i][0].isConst() && !conflict[i][0].getConst<bool>()) {
+              ++ i;
+              continue;
+            }
+            proofRecipe->getStep(0)->addAssertion(conflict[i].negate());
+            proofRecipe->addBaseAssertion(conflict[i].negate());
+          }
+        } else {
+          proofRecipe->getStep(0)->addAssertion(conflict.negate());
+          proofRecipe->addBaseAssertion(conflict.negate());
+        }
+      });
+
+    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
   }
+
+  PROOF({
+      delete proofRecipe;
+      proofRecipe = NULL;
+    });
 }
 
 void TheoryEngine::staticInitializeBVOptions(const std::vector<Node>& assertions) {
@@ -1660,19 +1885,21 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   return result;
 }
 
-void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector)
-{
+void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
   Assert(explanationVector.size() > 0);
 
   unsigned i = 0; // Index of the current literal we are processing
   unsigned j = 0; // Index of the last literal we are keeping
 
-  while (i < explanationVector.size()) {
+  std::set<Node> inputAssertions;
+  PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions(););
 
+  while (i < explanationVector.size()) {
     // Get the current literal to explain
     NodeTheoryPair toExplain = explanationVector[i];
 
-    Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
+    Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
+
 
     // If a true constant or a negation of a false constant we can ignore it
     if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
@@ -1686,6 +1913,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
 
     // If from the SAT solver, keep it
     if (toExplain.theory == THEORY_SAT_SOLVER) {
+      Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
       explanationVector[j++] = explanationVector[i++];
       continue;
     }
@@ -1704,10 +1932,26 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     // See if it was sent to the theory by another theory
     PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
     if (find != d_propagationMap.end()) {
+      Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
+                               << theoryOf((*find).second.theory)->getId() << ")" << std::endl;
       // There is some propagation, check if its a timely one
       if ((*find).second.timestamp < toExplain.timestamp) {
+        Debug("theory::explain") << "\tRelevant timetsamp, pushing "
+                                 << (*find).second.node << "to index = " << explanationVector.size() << std::endl;
         explanationVector.push_back((*find).second);
-        ++ i;
+        ++i;
+
+        PROOF({
+            if (toExplain.node != (*find).second.node) {
+              Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node
+                                   << ", toExplain = " << (*find).second.node << std::endl;
+
+              if (proofRecipe) {
+                proofRecipe->addRewriteRule(toExplain.node, (*find).second.node);
+              }
+            }
+          })
+
         continue;
       }
     }
@@ -1716,21 +1960,61 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     Node explanation;
     if (toExplain.theory == THEORY_BUILTIN) {
       explanation = d_sharedTerms.explain(toExplain.node);
+      Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
     } else {
       explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
+      Debug("theory::explain") << "\tTerm was propagated by owner theory: "
+                               << theoryOf(toExplain.theory)->getId()
+                               << ". Explanation: " << explanation << std::endl;
     }
+
     Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
     Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
     // Mark the explanation
     NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
     explanationVector.push_back(newExplain);
+
     ++ i;
+
+    PROOF({
+        if (proofRecipe) {
+          // If we're expanding the target node of the explanation (this is the first expansion...),
+          // we don't want to add it as a separate proof step. It is already part of the assertions.
+          if (inputAssertions.find(toExplain.node) == inputAssertions.end()) {
+            LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node);
+            if (explanation.getKind() == kind::AND) {
+              Node flat = flattenAnd(explanation);
+              for (unsigned k = 0; k < flat.getNumChildren(); ++ k) {
+                // If a true constant or a negation of a false constant we can ignore it
+                if (! ((flat[k].isConst() && flat[k].getConst<bool>()) ||
+                       (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst<bool>()))) {
+                  proofStep.addAssertion(flat[k].negate());
+                }
+              }
+            } else {
+             if (! ((explanation.isConst() && explanation.getConst<bool>()) ||
+                    (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
+               proofStep.addAssertion(explanation.negate());
+             }
+            }
+            proofRecipe->addStep(proofStep);
+          }
+        }
+      });
   }
 
   // Keep only the relevant literals
   explanationVector.resize(j);
-}
 
+  PROOF({
+      if (proofRecipe) {
+        // The remaining literals are the base of the proof
+        for (unsigned k = 0; k < explanationVector.size(); ++k) {
+          proofRecipe->addBaseAssertion(explanationVector[k].node.negate());
+        }
+      }
+    });
+}
 
 void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
 {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index db94edd7c..53c4aac77 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -50,6 +50,7 @@
 namespace CVC4 {
 
 class ResourceManager;
+class LemmaProofRecipe;
 
 /**
  * A pair of a theory and a node. This is used to mark the flow of
@@ -270,46 +271,18 @@ class TheoryEngine {
       }
     }
 
-    void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) {
-      Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
-      Assert(pf == NULL); // theory shouldn't be producing proofs yet
-      ++ d_statistics.conflicts;
-      d_engine->d_outputChannelUsed = true;
-      d_engine->conflict(conflictNode, d_theory);
-    }
+    void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException);
 
-    bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) {
-      Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
-      ++ d_statistics.propagations;
-      d_engine->d_outputChannelUsed = true;
-      return d_engine->propagate(literal, d_theory);
-    }
+    bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException);
 
     theory::LemmaStatus lemma(TNode lemma,
                               ProofRule rule,
                               bool removable = false,
                               bool preprocess = false,
                               bool sendAtoms = false)
-      throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
-      Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
-      ++ d_statistics.lemmas;
-      d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST, d_theory);
-    }
+      throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException);
 
-    /*theory::LemmaStatus preservedLemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) {
-      Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::preservedLemma(" << lemma << ")" << std::endl;
-      ++ d_statistics.lemmas;
-      d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, false, removable, preprocess, d_theory);
-    }*/
-
-    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
-      Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::splitLemma(" << lemma << ")" << std::endl;
-      ++ d_statistics.lemmas;
-      d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory);
-    }
+    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException);
 
     void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       NodeManager* curr = NodeManager::currentNM();
@@ -456,7 +429,7 @@ class TheoryEngine {
                             bool removable,
                             bool preprocess,
                             theory::TheoryId atomsTo,
-                            theory::TheoryId ownerTheory);
+                            LemmaProofRecipe* proofRecipe);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
@@ -606,9 +579,10 @@ private:
    * asking relevant theories to explain the propagations. Initially
    * the explanation vector should contain only the element (node, theory)
    * where the node is the one to be explained, and the theory is the
-   * theory that sent the literal.
+   * theory that sent the literal. The lemmaProofRecipe will contain a list
+   * of the explanation steps required to produce the original node.
    */
-  void getExplanation(std::vector<NodeTheoryPair>& explanationVector);
+  void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
 
 public:
 
@@ -730,7 +704,7 @@ public:
    * Returns an explanation of the node propagated to the SAT solver and the theory
    * that propagated it.
    */
-  NodeTheoryPair getExplanationAndExplainer(TNode node);
+  Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
 
   /**
    * collect model info
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 9b429765e..25b12f75f 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -964,12 +964,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
           std::vector<EqProof *> orderedChildren;
           bool nullCongruenceFound = false;
           for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
-            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) {
-
-              // For now, assume there can only be one null congruence child
-              Assert(!nullCongruenceFound);
+            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
+                eqpc->d_children[i]->d_node.isNull()) {
               nullCongruenceFound = true;
-
               Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl;
               orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]);
               orderedChildren.push_back(eqpc->d_children[i]->d_children[1]);
@@ -1192,6 +1189,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
                 getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
                 if( eqpc ) {
                   eqpc->d_children.push_back( eqpcc );
+
+                  Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl;
+                  eqpc->debug_print("pf::ee", 1);
                 }
               }
 
@@ -1605,6 +1605,7 @@ void EqualityEngine::propagate() {
 }
 
 void EqualityEngine::debugPrintGraph() const {
+  Debug("equality::graph") << std::endl << "Dumping graph" << std::endl;
   for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
 
     Debug("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
@@ -1618,6 +1619,7 @@ void EqualityEngine::debugPrintGraph() const {
 
     Debug("equality::graph") << std::endl;
   }
+  Debug("equality::graph") << std::endl;
 }
 
 bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
@@ -2209,9 +2211,15 @@ bool EqClassIterator::isFinished() const {
   return d_current == null_id;
 }
 
-void EqProof::debug_print( const char * c, unsigned tb ) const{
-  for( unsigned i=0; i<tb; i++ ) { Debug( c ) << "  "; }
-  Debug( c ) << d_id << "(";
+void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const {
+  for(unsigned i=0; i<tb; i++) { Debug( c ) << "  "; }
+
+  if (prettyPrinter)
+    Debug( c ) << prettyPrinter->printTag(d_id);
+  else
+    Debug( c ) << d_id;
+
+  Debug( c ) << "(";
   if( !d_children.empty() || !d_node.isNull() ){
     if( !d_node.isNull() ){
       Debug( c ) << std::endl;
@@ -2221,7 +2229,7 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{
     for( unsigned i=0; i<d_children.size(); i++ ){
       if( i>0 || !d_node.isNull() ) Debug( c ) << ",";
       Debug( c ) << std::endl;
-      d_children[i]->debug_print( c, tb+1 );
+      d_children[i]->debug_print( c, tb+1, prettyPrinter );
     }
   }
   Debug( c ) << ")" << std::endl;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index f30f1e8a0..843e7ce7f 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -902,11 +902,17 @@ public:
 class EqProof
 {
 public:
+  class PrettyPrinter {
+  public:
+    virtual ~PrettyPrinter() {}
+    virtual std::string printTag(unsigned tag) = 0;
+  };
+
   EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
   unsigned d_id;
   Node d_node;
   std::vector< EqProof * > d_children;
-  void debug_print( const char * c, unsigned tb = 0 ) const;
+  void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const;
 };/* class EqProof */
 
 } // Namespace eq
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index d1685bdd1..9c461f57b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -502,7 +502,7 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
 void TheoryUF::computeCareGraph() {
 
   if (d_sharedTerms.size() > 0) {
-    //use term indexing 
+    //use term indexing
     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
     std::map< Node, quantifiers::TermArgTrie > index;
     std::map< Node, unsigned > arity;
@@ -533,6 +533,7 @@ void TheoryUF::computeCareGraph() {
 
 void TheoryUF::conflict(TNode a, TNode b) {
   eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
+
   if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b),pf);
   } else {