Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

22 files changed, 434 insertions, 1849 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index b9907aac9..a1287b667 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -830,8 +830,4 @@ 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 810d41155..788e4bd86 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -74,7 +74,6 @@ 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 aee236677..8aba8dce9 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -81,29 +81,14 @@ 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) {
@@ -116,7 +101,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", 0, &d_proofPrinter);
+  pf->debug_print("pf::array");
   Debug("pf::array") << std::endl;
   toStreamRecLFSC( out, tp, pf, 0, map );
   Debug("pf::array") << "Printing array proof in LFSC DONE" << std::endl;
@@ -129,7 +114,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", 0, &d_proofPrinter);
+  pf->debug_print("pf::array");
   Debug("pf::array") << std::endl;
 
   if(tb == 0) {
@@ -165,7 +150,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", 0, &d_proofPrinter);
+          pf->d_children[i+count]->debug_print("pf::array");
           congruenceClosures.push_back(pf->d_children[i+count]);
         }
 
@@ -235,48 +220,48 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         ++i;
       }
     }
-
-    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());
-    }
+    Assert(neg >= 0);
 
     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(!disequalityFound || pf->d_children.size() > 2) {
+    if(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;
     }
 
-    out << "(clausify_false (contra _ ";
+    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 (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;
+    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].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.
 
-      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) {
+      //      	    (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 << " ";
+      out << ss2.str();
+      out << "))";
+
+    } else {
+      // The negative node is, e.g., a pure equality
+      out << "(clausify_false (contra _ ";
+
+      if(n2[0].getKind() == kind::APPLY_UF) {
         out << "(trans _ _ _ _ ";
         out << "(symm _ _ _ ";
         out << ss.str();
@@ -291,27 +276,16 @@ 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]);
+        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();
   }
 
   if (pf->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE) {
     Debug("mgd") << "\nok, looking at congruence:\n";
-    pf->debug_print("mgd", 0, &d_proofPrinter);
+    pf->debug_print("mgd");
     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());
@@ -341,7 +315,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
 
     Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
-    pf2->debug_print("mgd", 0, &d_proofPrinter);
+    pf2->debug_print("mgd");
     // 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;
@@ -358,7 +332,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", 0, &d_proofPrinter);
+        pf2->d_children[0]->debug_print("mgd");
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -572,20 +546,6 @@ 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;
@@ -594,7 +554,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", 0, &d_proofPrinter);
+    pf->debug_print("mgd");
     Debug("mgd") << "\n";
     Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
     Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
@@ -812,7 +772,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, &d_proofPrinter);
+          pf->debug_print("mgdx",0);
           //toStreamRec(Warning.getStream(), pf, 0);
           Warning() << "\n\n";
           Unreachable();
@@ -971,9 +931,6 @@ 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);
@@ -982,31 +939,28 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
       Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
 
-      if (swap) {
-        out << "(symm _ _ _ ";
-      }
-
       out << "(negativerow _ _ ";
-      tp->printTerm(swap ? t2.toExpr() : t1.toExpr(), out, map);
+      tp->printTerm(t1.toExpr(), out, map);
       out << " ";
-      tp->printTerm(swap ? t1.toExpr() : t2.toExpr(), out, map);
+      tp->printTerm(t2.toExpr(), out, map);
       out << " ";
       tp->printTerm(t3.toExpr(), out, map);
       out << " ";
       tp->printTerm(t4.toExpr(), out, map);
       out << " ";
 
-      if (side != 0) {
-        out << "(negsymm _ _ _ " << ss.str() << ")";
-      } else {
-        out << ss.str();
-      }
+
+      // 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() << ")";
+      // }
 
       out << ")";
 
-      if (swap) {
-        out << ") ";
-      }
+      // Unreachable();
 
       return ret;
     }
@@ -1117,12 +1071,13 @@ 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) {
@@ -1199,21 +1154,7 @@ 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());
-  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 <<" ";
-  }
+  os << type <<" ";
 }
 
 void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
@@ -1228,6 +1169,8 @@ 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";
@@ -1286,7 +1229,6 @@ 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);
@@ -1295,7 +1237,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
                        << "It is a witness for: " << equality << std::endl;
 
     std::ostringstream newSkolemLiteral;
-    newSkolemLiteral << ".sl" << count++;
+    newSkolemLiteral << ".sl" << d_skolemToLiteral.size();
     std::string skolemLiteral = newSkolemLiteral.str();
 
     d_skolemToLiteral[*it] = skolemLiteral;
@@ -1309,12 +1251,13 @@ 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 << " (\\ ";
-    os << ProofManager::sanitize(*it);
+    printTerm(*it, os, map);
     os << " (\\ ";
     os << skolemLiteral.c_str();
     os << "\n";
@@ -1323,8 +1266,4 @@ 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 076ba7381..fb25c9433 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -30,32 +30,6 @@ 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,
@@ -67,8 +41,6 @@ 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
@@ -81,10 +53,6 @@ public:
   void setRowMergeTag(unsigned tag);
   void setRow1MergeTag(unsigned tag);
   void setExtMergeTag(unsigned tag);
-
-  unsigned getRowMergeTag() const;
-  unsigned getRow1MergeTag() const;
-  unsigned getExtMergeTag() const;
 };
 
 namespace theory {
@@ -123,7 +91,6 @@ 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 479266db4..b63782226 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -15,11 +15,9 @@
 
 **/
 
-#include "options/bv_options.h"
-#include "proof/array_proof.h"
 #include "proof/bitvector_proof.h"
+#include "options/bv_options.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"
@@ -82,40 +80,20 @@ 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) &&
@@ -123,11 +101,6 @@ 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]);
@@ -135,7 +108,6 @@ 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();
@@ -150,8 +122,6 @@ 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]);
@@ -159,7 +129,6 @@ 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;
 
@@ -175,99 +144,25 @@ 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 #" << 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()) {
+    Debug("pf::bv") << "Finalize conflict " << confl << std::endl;
+    //Assert (d_bbConflictMap.find(confl) != d_bbConflictMap.end());
+    if(d_bbConflictMap.find(confl) != d_bbConflictMap.end()){
       ClauseId id = d_bbConflictMap[confl];
       d_resolutionProof->collectClauses(id);
-    } 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();
-      }
+    }else{
+      Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl;
     }
   }
 }
@@ -343,25 +238,11 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa
     printBitOf(term, os, map);
     return;
   }
-
-  case kind::VARIABLE: {
-    os << "(a_var_bv " << utils::getSize(term)<< " " << ProofManager::sanitize(term) << ")";
-    return;
-  }
-
+  case kind::VARIABLE:
   case kind::SKOLEM: {
-
-    // 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) << ")";
-    }
+    os << "(a_var_bv " << utils::getSize(term)<<" " << ProofManager::sanitize(term) <<")";
     return;
   }
-
   default:
     Unreachable();
   }
@@ -377,7 +258,14 @@ void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& m
                   << ", var = " << var << std::endl;
 
   os << "(bitof ";
-  os << d_exprToVariableName[var];
+  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 << " " << bit << ")";
 }
 
@@ -461,16 +349,14 @@ 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) {
@@ -491,7 +377,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);
@@ -500,120 +386,11 @@ 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") << "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();
+    Debug("pf::bv") << std::endl << "; Print non-bitblast theory conflict " << conflict << std::endl;
+    BitVectorProof::printTheoryLemmaProof( lemma, os, paren );
   }
 }
 
@@ -625,13 +402,7 @@ 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) {
-    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";
+    os << "(% " << ProofManager::sanitize(*it) <<" var_bv\n";
     paren <<")";
   }
 }
@@ -640,43 +411,15 @@ 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()) {
-    // 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 << " _ )";
+  if (Theory::isLeafOf(term, theory::THEORY_BV) &&
+      !term.isConst()) {
+    os << "(bv_bbl_var "<<utils::getSize(term) << " " << ProofManager::sanitize(term) <<" _ )";
     return;
   }
 
@@ -705,60 +448,37 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   case kind::BITVECTOR_PLUS :
   case kind::BITVECTOR_SUB :
   case kind::BITVECTOR_CONCAT : {
-    Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl;
-
-    for (int i = term.getNumChildren() - 1; i > 0; --i) {
+    for (unsigned i =0; i < term.getNumChildren() - 1; ++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 <<" _ _ _ _ _ _ ";
     }
-
-    if (hasAlias(term[0])) {os << "_ " << d_aliasToBindDeclaration[d_assignedAliases[term[0]]] << " ";}
-    os << getBBTermName(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);
-
-    if (hasAlias(term[0])) {os << "_alias";};
-
-    os << " " << utils::getSize(term) << " ";
+    os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
+    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;
@@ -766,7 +486,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) << (hasAlias(term[0]) ? "_alias " : " ");
+    os <<"(bv_bbl_"<<utils::toLFSCKind(kind) <<" ";
     os << utils::getSize(term) <<" ";
     if (term.getKind() == kind::BITVECTOR_REPEAT) {
       unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount;
@@ -781,9 +501,7 @@ 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;
@@ -821,7 +539,7 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) {
   }
 }
 
-void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) {
+void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os) {
   Kind kind = atom.getKind();
   switch(kind) {
   case kind::BITVECTOR_ULT :
@@ -832,28 +550,11 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool
   case kind::BITVECTOR_SLE :
   case kind::BITVECTOR_SGT :
   case kind::BITVECTOR_SGE :
-  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";}
-
+  case kind::EQUAL:
+    {
+    os <<"(bv_bbl_" << utils::toLFSCKind(atom.getKind());
     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 << ")";
+    os << getBBTermName(atom[0])<<" " << getBBTermName(atom[1]) <<")";
     return;
   }
   default:
@@ -861,53 +562,19 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool
   }
 }
 
-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) << "\n";
-    paren << "))";
+    os << "(\\ "<< getBBTermName(*it);
+    paren <<"\n))";
   }
   // bit-blast atoms
   ExprToExpr::const_iterator ait = d_bbAtoms.begin();
@@ -922,35 +589,7 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
       bool val = ait->first.getConst<bool>();
       os << "(iff_symm " << (val ? "true" : "false" ) << ")";
     } else {
-      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);
-      }
+      printAtomBitblasting(ait->first, os);
     }
 
     os <<"(\\ " << ProofManager::getPreprocessedAssertionName(ait->second) <<"\n";
@@ -967,53 +606,25 @@ 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 << std::endl << ";; BB atom mapping\n" << std::endl;
-
-  std::set<Node> atoms;
-  d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
+  os << ";; BB atom mapping\n";
 
-  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;
+  NodeSet atoms;
+  d_cnfProof->collectAtomsForClauses(used_inputs,atoms);
 
   // first print bit-blasting
   printBitblasting(os, paren);
 
   // print CNF conversion proof for bit-blasted facts
   d_cnfProof->printAtomMapping(atoms, os, paren);
-  os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
+  os << ";; Bit-blasting definitional clauses \n";
   for (IdToSatClause::iterator it = used_inputs.begin();
        it != used_inputs.end(); ++it) {
     d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren);
   }
 
-  os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl;
+  os << ";; Bit-blasting learned clauses \n";
   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 4e5e98541..4a1f4015d 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -60,7 +60,6 @@ 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:
@@ -109,8 +108,7 @@ public:
   virtual void registerTerm(Expr term);
 
   virtual void printTermBitblasting(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 printAtomBitblasting(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;
@@ -125,12 +123,6 @@ 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)
@@ -138,13 +130,11 @@ 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, bool swap);
-  virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
+  virtual void printAtomBitblasting(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 abe48e3cd..19e9cbac9 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -19,7 +19,6 @@
 
 #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"
@@ -33,6 +32,7 @@ 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,6 +103,7 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) {
 
   setClauseAssertion(clause, current_assertion);
   setClauseDefinition(clause, current_expr);
+  registerExplanationLemma(clause);
 }
 
 void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
@@ -142,15 +143,16 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) {
   d_assertionToProofRule.insert(assertion, reason);
 }
 
-LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) {
-  Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end());
-  return d_lemmaToProofRecipe[lemma];
+void CnfProof::registerExplanationLemma(ClauseId clauseId) {
+  d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory());
 }
 
-bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) {
-  return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end();
+theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) {
+  Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end());
+  return d_clauseIdToOwnerTheory[clause];
 }
 
+
 void CnfProof::setCnfDependence(Node from, Node to) {
   Debug("proof:cnf") << "CnfProof::setCnfDependence "
                      << "from " << from  << std::endl
@@ -181,10 +183,12 @@ Node CnfProof::getCurrentAssertion() {
   return d_currentAssertionStack.back();
 }
 
-void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) {
-  Assert(proofRecipe);
-  Assert(proofRecipe->getNumSteps() > 0);
-  d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe;
+void CnfProof::setExplainerTheory(theory::TheoryId theory) {
+  d_explainerTheory = theory;
+}
+
+theory::TheoryId CnfProof::getExplainerTheory() {
+  return d_explainerTheory;
 }
 
 void CnfProof::pushCurrentDefinition(Node definition) {
@@ -208,19 +212,22 @@ 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,
-                            std::set<Node>& atoms) {
+                            NodeSet& 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);
     }
   }
@@ -230,75 +237,14 @@ 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,
-                                      std::set<Node>& atoms) {
+                                       NodeSet& atom_map) {
   IdToSatClause::const_iterator it = clauses.begin();
   for (; it != clauses.end(); ++it) {
     const prop::SatClause* clause = it->second;
-    collectAtoms(clause, atoms);
+    collectAtoms(clause, atom_map);
   }
-}
-
-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,
@@ -317,13 +263,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
   }
 }
 
-void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
+void LFSCCnfProof::printAtomMapping(const NodeSet& atoms,
                                     std::ostream& os,
                                     std::ostream& paren) {
-  std::set<Node>::const_iterator it = atoms.begin();
-  std::set<Node>::const_iterator end = atoms.end();
+  NodeSet::const_iterator it = atoms.begin();
+  NodeSet::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();
@@ -331,8 +277,8 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
     LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
     pe->printLetTerm(atom.toExpr(), os);
 
-    os << " (\\ " << ProofManager::getVarName(var, d_name);
-    os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
+    os << " (\\ " << ProofManager::getVarName(var, d_name)
+       << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
     paren << ")))";
   }
 }
@@ -358,9 +304,6 @@ 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);
@@ -393,10 +336,6 @@ 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;
@@ -625,7 +564,6 @@ 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 );
@@ -724,7 +662,6 @@ 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 62036ced0..a21cb1c0e 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -27,7 +27,6 @@
 
 #include "context/cdhashmap.h"
 #include "proof/clause_id.h"
-#include "proof/lemma_proof.h"
 #include "proof/sat_proof.h"
 #include "util/proof.h"
 
@@ -44,9 +43,7 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet;
 
 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
 typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
-typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe;
-typedef std::pair<Node, Node> NodePair;
-typedef std::set<NodePair> NodePairSet;
+typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory;
 
 class CnfProof {
 protected:
@@ -58,8 +55,11 @@ protected:
   /** Map from assertion to reason for adding assertion  **/
   NodeToProofRule d_assertionToProofRule;
 
-  /** Map from lemma to the recipe for proving it **/
-  LemmaToRecipe d_lemmaToProofRecipe;
+  /** Map from assertion to the theory that added this assertion  **/
+  ClauseIdToTheory d_clauseIdToOwnerTheory;
+
+  /** The last theory to explain a lemma **/
+  theory::TheoryId d_explainerTheory;
 
   /** Top of stack is assertion currently being converted to CNF **/
   std::vector<Node> d_currentAssertionStack;
@@ -91,16 +91,10 @@ 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,
-                    std::set<Node>& atoms);
+                    NodeSet& atoms);
   void collectAtomsForClauses(const IdToSatClause& clauses,
-                              std::set<Node>& atoms);
-  void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
-                                        std::set<Node>& atoms,
-                                        NodePairSet& rewrites);
+                               NodeSet& atoms);
   void collectAssertionsForClauses(const IdToSatClause& clauses,
                                    NodeSet& assertions);
 
@@ -127,9 +121,11 @@ public:
   void popCurrentDefinition();
   Node getCurrentDefinition();
 
-  void setProofRecipe(LemmaProofRecipe* proofRecipe);
-  LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
-  bool haveProofRecipe(const std::set<Node> &lemma);
+  void setExplainerTheory(theory::TheoryId theory);
+  theory::TheoryId getExplainerTheory();
+  theory::TheoryId getOwnerTheory(ClauseId clause);
+
+  void registerExplanationLemma(ClauseId clauseId);
 
   // accessors for the leaf assertions that are being converted to CNF
   bool isAssertion(Node node);
@@ -138,7 +134,7 @@ public:
   Node getAssertionForClause(ClauseId clause);
 
   /** Virtual methods for printing things **/
-  virtual void printAtomMapping(const std::set<Node>& atoms,
+  virtual void printAtomMapping(const NodeSet& atoms,
                                 std::ostream& os,
                                 std::ostream& paren) = 0;
 
@@ -165,7 +161,7 @@ public:
   {}
   ~LFSCCnfProof() {}
 
-  void printAtomMapping(const std::set<Node>& atoms,
+  void printAtomMapping(const NodeSet& atoms,
                         std::ostream& os,
                         std::ostream& paren);
 
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp
deleted file mode 100644
index a12a516cf..000000000
--- a/src/proof/lemma_proof.cpp
+++ /dev/null
@@ -1,193 +0,0 @@
-/*********************                                                        */
-/*! \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
deleted file mode 100644
index e96ff5337..000000000
--- a/src/proof/lemma_proof.h
+++ /dev/null
@@ -1,79 +0,0 @@
-/*********************                                                        */
-/*! \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 5ce8b523f..a3689d746 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -200,6 +200,7 @@ 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;
@@ -216,15 +217,9 @@ std::string ProofManager::getAtomName(TNode atom,
   Assert(!lit.isNegated());
   return getAtomName(lit.getSatVariable(), prefix);
 }
-
 std::string ProofManager::getLitName(TNode lit,
                                      const std::string& 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;
+  return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix);
 }
 
 std::string ProofManager::sanitize(TNode node) {
@@ -336,9 +331,6 @@ 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
@@ -392,37 +384,8 @@ void LFSCProof::toStream(std::ostream& out) {
   for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
     Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
 
-  std::set<Node> atoms;
-  NodePairSet rewrites;
+  NodeSet atoms;
   // 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);
 
@@ -430,23 +393,38 @@ 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);
   }
 
-  std::set<Node>::iterator atomIt;
-  Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
-                  << std::endl << std::endl;
+  NodeSet::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 = atoms.begin(); it != atoms.end(); ++it) {
+  for(; it != end; ++it) {
     Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
     d_theoryProof->registerTerm((*it).toExpr());
   }
@@ -466,15 +444,9 @@ 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\n";
+  out << " ;; Printing deferred declarations \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);
 
@@ -492,6 +464,10 @@ 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;
@@ -520,8 +496,6 @@ 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 _ ";
 
@@ -532,6 +506,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
     os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
     paren << "))";
+
   }
 
   os << "\n";
@@ -593,14 +568,6 @@ 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 c6454b652..c74aac237 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -34,8 +34,6 @@
 
 namespace CVC4 {
 
-class SmtGlobals;
-
 // forward declarations
 namespace Minisat {
   class Solver;
@@ -138,8 +136,6 @@ class ProofManager {
 
   std::set<Type> d_printedTypes;
 
-  std::map<std::string, std::string> d_rewriteFilters;
-
 protected:
   LogicInfo d_logic;
 
@@ -228,9 +224,6 @@ 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
deleted file mode 100644
index 6d729db1f..000000000
--- a/src/proof/proof_output_channel.cpp
+++ /dev/null
@@ -1,82 +0,0 @@
-/*********************                                                        */
-/*! \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
deleted file mode 100644
index b85af5fb5..000000000
--- a/src/proof/proof_output_channel.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/*********************                                                        */
-/*! \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 fe0d42242..5b04c281d 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, std::set<Node>& seen) {
+void collectAtoms(TNode node, CVC4::NodeSet& 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 8c734c892..da10c33a0 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,9 +29,6 @@ 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);
@@ -45,7 +42,7 @@ inline unsigned getExtractLow(Expr node) {
 }
 
 inline unsigned getSize(Type type) {
-  BitVectorType bv(type);
+  BitVectorType bv(type); 
   return bv.getSize();
 }
 
@@ -63,8 +60,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) {
@@ -76,16 +73,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) {
@@ -95,14 +92,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();
@@ -112,23 +109,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();
@@ -138,7 +135,7 @@ inline Expr mkAnd(const std::vector<Expr>& conjunctions) {
     ++ it;
   }
 
-  Node res = conjunction;
+  Node res = conjunction; 
   return res.toExpr();
 }/* mkAnd() */
 
@@ -147,14 +144,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();
@@ -168,13 +165,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, std::set<Node>& seen);
+void collectAtoms(TNode node, NodeSet& seen);
 
 
 }
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 1e01e4dce..4f3330ef7 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -543,9 +543,12 @@ 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)
-                       << std::endl;
+      Debug("pf::sat")
+          << "TSatProof::registerClause registering a new lemma clause: "
+          << newId << " = " << *buildClause(newId)
+          << ". Explainer theory: " << d_cnfProof->getExplainerTheory()
+          << std::endl;
+      d_cnfProof->registerExplanationLemma(newId);
     }
   }
 
@@ -576,10 +579,12 @@ 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
-                       << std::endl;
+      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
+                          "lemma (UNIT CLAUSE): "
+                       << lit << ". Explainer theory: "
+                       << d_cnfProof->getExplainerTheory() << std::endl;
       d_lemmaClauses.insert(newId);
+      d_cnfProof->registerExplanationLemma(newId);
     }
   }
   ClauseId id = d_unitId[toInt(lit)];
@@ -837,7 +842,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 (size_t i = 0; i < current_reason_size; i++) {
+  for (int 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];
@@ -899,7 +904,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 (size_t i = 0; i < conflict_size; ++i) {
+  for (int 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);
@@ -1101,12 +1106,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 b026e21c2..de510e514 100644
--- a/src/proof/skolemization_manager.h
+++ b/src/proof/skolemization_manager.h
@@ -37,6 +37,7 @@ 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 eaf21846b..088275b3f 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -25,7 +25,6 @@
 #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"
@@ -49,6 +48,74 @@ 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()
@@ -64,12 +131,13 @@ 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("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl;
+      Trace("theory-proof-debug") << "; register theory " << id << std::endl;
 
       if (id == theory::THEORY_UF) {
         d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this);
@@ -99,42 +167,19 @@ 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( " << term << " ) = " << theory_id << std::endl;
+  Debug("pf::tp") << "Term's theory: " << theory_id << std::endl;
 
   // don't need to register boolean terms
   if (theory_id == theory::THEORY_BUILTIN ||
@@ -148,38 +193,32 @@ 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(const prop::SatClause* clause) {
+theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) {
   ProofManager* pm = ProofManager::currentPM();
 
-  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;
-    }
+  Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )"
+                     << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
 
-    nodes.insert(lit.isNegated() ? node.notNode() : node);
+  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;
   }
 
-  // Ensure that the lemma is in the database.
-  Assert (pm->getCnfProof()->haveProofRecipe(nodes));
-  return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
+  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();
 }
 
 void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
@@ -233,6 +272,8 @@ 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
@@ -274,29 +315,6 @@ 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();
@@ -304,8 +322,6 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() {
   for(; it != end; ++it) {
     registerTerm(*it);
   }
-
-  performExtraRegistrations();
 }
 
 void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
@@ -317,43 +333,17 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
 
   for (; it != end; ++it) {
     Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
-    std::ostringstream name;
-    name << "A" << counter++;
-    os << "(% " << name.str() << " (th_holds ";
+    // FIXME: merge this with counter
+    os << "(% A" << counter++ << " (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;
 
@@ -388,148 +378,55 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost
   }
 }
 
-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) {
-    it->second->printAliasingDeclarations(os, paren);
-  }
-}
+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();
 
-void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
-  Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl;
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl;
 
-  ProofManager* pm = ProofManager::currentPM();
-  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+  for (; it != end; ++it) {
+    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl;
     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");
+    Debug("pf::tp") << "\tLemma = " << id
+                       << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
   }
+  it = lemmas.begin();
 
-  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
+  // 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) {
+  for (; it != end; ++it) {
+    ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
 
+    theory::TheoryId theory_id = getTheoryForLemma(id);
+    if (theory_id != theory::THEORY_BV) continue;
+
     std::vector<Expr> conflict;
-    std::set<Node> conflictNodes;
     for(unsigned i = 0; i < clause->size(); ++i) {
       prop::SatLiteral lit = (*clause)[i];
-      Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable());
-      Expr atom = node.toExpr();
-
-      // The literals (true) and (not false) are omitted from conflicts
+      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
       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);
+  bv->printResolutionProof(os, paren);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     Assert (lemmas.size() == 1);
@@ -537,247 +434,54 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
     return;
   }
 
-  ProofManager* pm = ProofManager::currentPM();
+  it = lemmas.begin();
+
   Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl;
 
-  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+  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;
     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") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = "
-                    << id << std::endl;
+    Debug("pf::tp") << "CnfProof printing clause..." << std::endl;
+    pm->getCnfProof()->printClause(*clause, os, clause_paren);
+    Debug("pf::tp") << "CnfProof printing clause - Done!" << 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];
-      Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
-      Expr atom = node.toExpr();
+      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).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);
     }
 
-    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 << "))";
-    }
+    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 << "))";
   }
 }
 
 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()) {
@@ -893,21 +597,19 @@ 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("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
-
-  if (d_theory->getId()==theory::THEORY_UF) {
+  Trace("theory-proof-debug") << ";; 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::");
@@ -1012,10 +714,7 @@ void BooleanProof::registerTerm(Expr term) {
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {
-    if (d_treatBoolsAsFormulas)
-      os << "(p_app " << ProofManager::sanitize(term) <<")";
-    else
-      os << ProofManager::sanitize(term);
+    os << "(p_app " << ProofManager::sanitize(term) <<")";
     return;
   }
 
@@ -1054,10 +753,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap&
     return;
 
   case kind::CONST_BOOLEAN:
-    if (d_treatBoolsAsFormulas)
-      os << (term.getConst<bool>() ? "true" : "false");
-    else
-      os << (term.getConst<bool>() ? "t_true" : "t_false");
+    os << (term.getConst<bool>() ? "true" : "false");
     return;
 
   default:
@@ -1090,10 +786,6 @@ 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 c8c776ec9..54c86f3f3 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -27,7 +27,6 @@
 #include "proof/clause_id.h"
 #include "prop/sat_solver_types.h"
 #include "util/proof.h"
-#include "proof/proof_utils.h"
 
 namespace CVC4 {
 
@@ -91,14 +90,10 @@ 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
@@ -153,14 +148,6 @@ 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).
    *
@@ -184,14 +171,8 @@ public:
    */
   void registerTheory(theory::Theory* theory);
 
-  theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
+  theory::TheoryId getTheoryForLemma(ClauseId id);
   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 {
@@ -209,25 +190,11 @@ 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 {
@@ -303,20 +270,11 @@ 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 {
@@ -334,13 +292,12 @@ 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), d_treatBoolsAsFormulas(true)
+    : BooleanProof(proofEngine)
   {}
   virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
@@ -348,14 +305,6 @@ 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 bc409901c..32ca122b0 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -86,16 +86,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
   pf->debug_print("pf::uf");
   Debug("pf::uf") << std::endl;
 
-  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();
-    }
-
+  if(tb == 0) {
     Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
     Assert(!pf->d_node.isNull());
     Assert(pf->d_children.size() >= 2);
@@ -199,71 +190,42 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
         ++i;
       }
     }
-
-    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());
-    }
+    Assert(neg >= 0);
 
     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(!disequalityFound || subTrans.d_children.size() >= 2) {
+    if(pf->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;
     }
 
-    Debug("pf::uf") << "\nhave proven: " << 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 (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].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 (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 (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;
+    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() << ")";
       } 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() << ")";
-        } else {
-          out << ss.str();
-        }
-        out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
+        out << ss.str();
       }
-    } 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;
+      out << " " << ProofManager::getLitName(n2[0]) << "))" << std::endl;
     }
-
     return Node();
   }
 
@@ -622,10 +584,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].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n1[1];
           ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")";
         } else if(n1[1] == n2) {
-          n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n1[0];
           ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")";
         } else {
           Unreachable();
@@ -633,16 +595,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].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n2[1];
           ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")";
         } else if(n2[1] == n1) {
-          n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true));
+          n1 = n2[0];
           ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")";
         } else {
           Unreachable();
         }
       } else {
-        // Both n1 and n2 are predicates. Don't know what to do...
+        // Both n1 and n2 are prediacates. Don't know what to do...
         Unreachable();
       }
 
@@ -705,7 +667,6 @@ 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 ";
@@ -722,7 +683,6 @@ 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) {
@@ -754,8 +714,6 @@ 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;
 
@@ -771,8 +729,7 @@ 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 << " ";
-        d_proofEngine->printSort(arg_type, os);
+        os << " " << arg_type;
         if (i < args.size() - 2) {
           os << " (arrow";
           fparen << ")";
@@ -785,16 +742,10 @@ 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 0a23267d8..e359eaebd 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -69,7 +69,6 @@ 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);
 };