Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

13 files changed, 343 insertions, 672 deletions

diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 6dfd14157..11c3dc081 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -101,59 +101,8 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
         Debug("pf::ee") << "Getting explanation for ROW guard: "
                         << indexOne << " != " << indexTwo << std::endl;
 
-
         eq::EqProof* childProof = new eq::EqProof;
         d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof);
-
-        // It could be that the guard condition is a constant disequality. In this case,
-        // we need to change it to a different format.
-        if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
-          // The proof has two children, explaining why each index is a (different) constant.
-          Assert(childProof->d_children.size() == 2);
-
-          Node constantOne, constantTwo;
-          // Each subproof explains why one of the indices is constant.
-
-          if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantOne = childProof->d_children[0]->d_node;
-          } else {
-            Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
-            if ((childProof->d_children[0]->d_node[0] == indexOne) ||
-                (childProof->d_children[0]->d_node[0] == indexTwo)) {
-              constantOne = childProof->d_children[0]->d_node[1];
-            } else {
-              constantOne = childProof->d_children[0]->d_node[0];
-            }
-          }
-
-          if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantTwo = childProof->d_children[1]->d_node;
-          } else {
-            Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
-            if ((childProof->d_children[1]->d_node[0] == indexOne) ||
-                (childProof->d_children[1]->d_node[0] == indexTwo)) {
-              constantTwo = childProof->d_children[1]->d_node[1];
-            } else {
-              constantTwo = childProof->d_children[1]->d_node[0];
-            }
-          }
-
-          eq::EqProof* constantDisequalityProof = new eq::EqProof;
-          constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
-          constantDisequalityProof->d_node =
-            NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
-
-          // Middle is where we need to insert the new disequality
-          std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin();
-          ++middle;
-
-          childProof->d_children.insert(middle, constantDisequalityProof);
-
-          childProof->d_id = theory::eq::MERGED_THROUGH_TRANS;
-          childProof->d_node =
-            NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate();
-        }
-
         proof->d_children.push_back(childProof);
       } else {
         // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 28a08630e..6add1b55f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -829,8 +829,7 @@ void TheoryArrays::propagate(Effort e)
 
 
 Node TheoryArrays::explain(TNode literal) {
-  Node explanation = explain(literal, NULL);
-  return explanation;
+  return explain(literal, NULL);
 }
 
 Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
@@ -1395,7 +1394,6 @@ void TheoryArrays::check(Effort e) {
         break;
     default:
       Unreachable();
-      break;
     }
   }
 
@@ -2233,7 +2231,6 @@ bool TheoryArrays::dischargeLemmas()
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
   eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
-
   if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b), proof);
   } else {
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index dc5520411..fdc36ce72 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -41,7 +41,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
           continue;
         }
         Node signature = computeSignature(assertions[i][j]);
-        storeSignature(signature, assertions[i][j]);
+        storeSignature(signature, assertions[i][j]); 
         Debug("bv-abstraction") << "   assertion: " << assertions[i][j] <<"\n";
         Debug("bv-abstraction") << "   signature: " << signature <<"\n";
       }
@@ -52,7 +52,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
   for (unsigned i = 0; i < assertions.size(); ++i) {
     if (assertions[i].getKind() == kind::OR &&
         assertions[i][0].getKind() == kind::AND) {
-      std::vector<Node> new_children;
+      std::vector<Node> new_children; 
       for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) {
         if (hasSignature(assertions[i][j])) {
           new_children.push_back(abstractSignatures(assertions[i][j]));
@@ -60,10 +60,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
           new_children.push_back(assertions[i][j]);
         }
       }
-      new_assertions.push_back(utils::mkNode(kind::OR, new_children));
+      new_assertions.push_back(utils::mkNode(kind::OR, new_children)); 
     } else {
       // assertions that are not changed
-      new_assertions.push_back(assertions[i]);
+      new_assertions.push_back(assertions[i]); 
     }
   }
 
@@ -71,21 +71,21 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, st
     skolemizeArguments(new_assertions);
   }
 
-
+  
   // if we are using the eager solver reverse the abstraction
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     if (d_funcToSignature.size() == 0) {
       // we did not change anything
       return false;
     }
-    NodeNodeMap seen;
+    NodeNodeMap seen; 
     for (unsigned i = 0; i < new_assertions.size(); ++i) {
-      new_assertions[i] = reverseAbstraction(new_assertions[i], seen);
+      new_assertions[i] = reverseAbstraction(new_assertions[i], seen); 
     }
     // we undo the abstraction functions so the logic is QF_BV still
-    return true;
+    return true; 
   }
-
+  
   // return true if we have created new function symbols for the problem
   return d_funcToSignature.size() != 0;
 }
@@ -99,7 +99,7 @@ bool AbstractionModule::isConjunctionOfAtoms(TNode node) {
 bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) {
   if (seen.find(node)!= seen.end())
     return true;
-
+  
   if (!node.getType().isBitVector()) {
     return (node.getKind() == kind::AND || utils::isBVPredicate(node));
   }
@@ -120,30 +120,30 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) {
 
   if (seen.find(assertion) != seen.end())
     return seen[assertion];
-
+  
   if (isAbstraction(assertion)) {
     Node interp =  getInterpretation(assertion);
     seen[assertion] = interp;
-    Assert (interp.getType() == assertion.getType());
+    Assert (interp.getType() == assertion.getType()); 
     return interp;
   }
 
   if (assertion.getNumChildren() == 0) {
     seen[assertion] = assertion;
-    return assertion;
+    return assertion; 
   }
-
+  
   NodeBuilder<> result(assertion.getKind());
   if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
-    result << assertion.getOperator();
+    result << assertion.getOperator(); 
   }
 
   for (unsigned i = 0; i < assertion.getNumChildren(); ++i) {
-    result << reverseAbstraction(assertion[i], seen);
+    result << reverseAbstraction(assertion[i], seen); 
   }
   Node res = result;
   seen[assertion] = res;
-  return res;
+  return res; 
 }
 
 void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
@@ -151,7 +151,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
     TNode assertion = assertions[i];
     if (assertion.getKind() != kind::OR)
       continue;
-
+    
     bool is_skolemizable = true;
     for (unsigned k = 0; k < assertion.getNumChildren(); ++k) {
       if (assertion[k].getKind() != kind::EQUAL ||
@@ -191,54 +191,54 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) {
       NodeBuilder<> skolem_func (kind::APPLY_UF);
       skolem_func << func;
       std::vector<Node> skolem_args;
-
+        
       for (unsigned j = 0; j < args.getArity(); ++j) {
         bool all_same = true;
         for (unsigned k = 1; k < args.getNumEntries(); ++k) {
           if ( args.getEntry(k)[j] != args.getEntry(0)[j])
-            all_same = false;
+            all_same = false; 
         }
-        Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j]));
+        Node new_arg = all_same ? (Node)args.getEntry(0)[j] : utils::mkVar(utils::getSize(args.getEntry(0)[j])); 
         skolem_args.push_back(new_arg);
-        skolem_func << new_arg;
+        skolem_func << new_arg; 
       }
+      
 
-
-      Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u));
-
+      Node skolem_func_eq1 = utils::mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); 
+      
       // enumerate arguments assignments
-      std::vector<Node> or_assignments;
+      std::vector<Node> or_assignments; 
       for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) {
         NodeBuilder<> arg_assignment(kind::AND);
         ArgsVec& args =  *it;
         for (unsigned k = 0; k < args.size(); ++k) {
           Node eq = utils::mkNode(kind::EQUAL, args[k], skolem_args[k]);
-          arg_assignment << eq;
+          arg_assignment << eq; 
         }
         or_assignments.push_back(arg_assignment);
       }
-
+      
       Node new_func_def = utils::mkNode(kind::AND, skolem_func_eq1, utils::mkNode(kind::OR, or_assignments));
-      assertion_builder << new_func_def;
+      assertion_builder << new_func_def; 
     }
     Node new_assertion = assertion_builder;
     Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " << assertions[i] << " => \n";
-    Debug("bv-abstraction-dbg") << "    " << new_assertion;
+    Debug("bv-abstraction-dbg") << "    " << new_assertion; 
     assertions[i] = new_assertion;
   }
 }
 
 void AbstractionModule::storeSignature(Node signature, TNode assertion) {
   if(d_signatures.find(signature) == d_signatures.end()) {
-    d_signatures[signature] = 0;
+    d_signatures[signature] = 0; 
   }
-  d_signatures[signature] = d_signatures[signature] + 1;
-  d_assertionToSignature[assertion] = signature;
+  d_signatures[signature] = d_signatures[signature] + 1; 
+  d_assertionToSignature[assertion] = signature; 
 }
 
 Node AbstractionModule::computeSignature(TNode node) {
-  resetSignatureIndex();
-  NodeNodeMap cache;
+  resetSignatureIndex(); 
+  NodeNodeMap cache; 
   Node sig = computeSignatureRec(node, cache);
   return sig;
 }
@@ -247,17 +247,17 @@ Node AbstractionModule::getSignatureSkolem(TNode node) {
   Assert (node.getKind() == kind::VARIABLE);
   unsigned bitwidth = utils::getSize(node);
   if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) {
-    d_signatureSkolems[bitwidth] = vector<Node>();
+    d_signatureSkolems[bitwidth] = vector<Node>(); 
   }
-
+  
   vector<Node>& skolems = d_signatureSkolems[bitwidth];
   // get the index of bv variables of this size
-  unsigned index = getBitwidthIndex(bitwidth);
+  unsigned index = getBitwidthIndex(bitwidth); 
   Assert (skolems.size() + 1 >= index );
   if (skolems.size() == index) {
     ostringstream os;
     os << "sig_" <<bitwidth <<"_" << index;
-    NodeManager* nm = NodeManager::currentNM();
+    NodeManager* nm = NodeManager::currentNM(); 
     skolems.push_back(nm->mkSkolem(os.str(), nm->mkBitVectorType(bitwidth), "skolem for computing signatures"));
   }
   ++(d_signatureIndices[bitwidth]);
@@ -268,12 +268,12 @@ unsigned AbstractionModule::getBitwidthIndex(unsigned bitwidth) {
   if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) {
     d_signatureIndices[bitwidth] = 0;
   }
-  return d_signatureIndices[bitwidth];
+  return d_signatureIndices[bitwidth]; 
 }
 
 void AbstractionModule::resetSignatureIndex() {
   for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) {
-    it->second = 0;
+    it->second = 0; 
   }
 }
 
@@ -282,24 +282,24 @@ bool AbstractionModule::hasSignature(Node node) {
 }
 
 Node AbstractionModule::getGeneralizedSignature(Node node) {
-  NodeNodeMap::const_iterator it = d_assertionToSignature.find(node);
+  NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); 
   Assert (it != d_assertionToSignature.end());
-  Node generalized_signature = getGeneralization(it->second);
-  return generalized_signature;
+  Node generalized_signature = getGeneralization(it->second); 
+  return generalized_signature; 
 }
 
 Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
   if (cache.find(node) != cache.end()) {
-    return cache.find(node)->second;
+    return cache.find(node)->second; 
   }
-
+  
   if (node.getNumChildren() == 0) {
     if (node.getKind() == kind::CONST_BITVECTOR)
       return node;
 
     Node sig = getSignatureSkolem(node);
-    cache[node] = sig;
-    return sig;
+    cache[node] = sig; 
+    return sig; 
   }
 
   NodeBuilder<> builder(node.getKind());
@@ -308,30 +308,30 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) {
   }
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
     Node converted = computeSignatureRec(node[i], cache);
-    builder << converted;
+    builder << converted; 
   }
   Node result = builder;
   cache[node] = result;
-  return result;
+  return result; 
 }
 
-/**
+/** 
  * Returns 0, if the two are equal,
  * 1 if s is a generalization of t
  * 2 if t is a generalization of s
  * -1 if the two cannot be unified
  *
- * @param s
- * @param t
- *
- * @return
+ * @param s 
+ * @param t 
+ * 
+ * @return 
  */
 int AbstractionModule::comparePatterns(TNode s, TNode t) {
   if (s.getKind() == kind::SKOLEM &&
       t.getKind() == kind::SKOLEM) {
     return 0;
   }
-
+  
   if (s.getKind() == kind::CONST_BITVECTOR &&
       t.getKind() == kind::CONST_BITVECTOR) {
     if (s == t) {
@@ -350,7 +350,7 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) {
       t.getKind() == kind::SKOLEM) {
     return 2;
   }
-
+  
   if (s.getNumChildren() != t.getNumChildren() ||
       s.getKind() != t.getKind())
     return -1;
@@ -370,26 +370,26 @@ int AbstractionModule::comparePatterns(TNode s, TNode t) {
 }
 
 TNode AbstractionModule::getGeneralization(TNode term) {
-  NodeNodeMap::iterator it = d_sigToGeneralization.find(term);
+  NodeNodeMap::iterator it = d_sigToGeneralization.find(term); 
   // if not in the map we add it
   if (it == d_sigToGeneralization.end()) {
     d_sigToGeneralization[term] = term;
-    return term;
+    return term; 
   }
-  // doesn't have a generalization
+  // doesn't have a generalization 
   if (it->second == term)
     return term;
-
+  
   TNode generalization = getGeneralization(it->second);
   Assert (generalization != term);
   d_sigToGeneralization[term] = generalization;
-  return generalization;
+  return generalization; 
 }
 
 void AbstractionModule::storeGeneralization(TNode s, TNode t) {
   Assert (s == getGeneralization(s));
   Assert (t == getGeneralization(t));
-  d_sigToGeneralization[s] = t;
+  d_sigToGeneralization[s] = t; 
 }
 
 void AbstractionModule::finalizeSignatures() {
@@ -402,29 +402,29 @@ void AbstractionModule::finalizeSignatures() {
     for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) {
       TNode t = getGeneralization(tt->first);
       TNode s = getGeneralization(ss->first);
-
+      
       if (t != s) {
         int status = comparePatterns(s, t);
-        Assert (status);
+        Assert (status); 
         if (status < 0)
           continue;
         if (status == 1) {
-          storeGeneralization(t, s);
+          storeGeneralization(t, s); 
         } else {
-          storeGeneralization(s, t);
+          storeGeneralization(s, t); 
         }
       }
     }
   }
   // keep only most general signatures
   for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
-    TNode sig = it->first;
+    TNode sig = it->first; 
     TNode gen = getGeneralization(sig);
     if (sig != gen) {
-      Assert (d_signatures.find(gen) != d_signatures.end());
+      Assert (d_signatures.find(gen) != d_signatures.end()); 
       // update the count
       d_signatures[gen]+= d_signatures[sig];
-      d_signatures.erase(it++);
+      d_signatures.erase(it++); 
     } else {
       ++it;
     }
@@ -434,12 +434,12 @@ void AbstractionModule::finalizeSignatures() {
   // remove signatures that are not frequent enough
   for (SignatureMap::iterator it = d_signatures.begin(); it != d_signatures.end(); ) {
     if (it->second <= 7) {
-      d_signatures.erase(it++);
+      d_signatures.erase(it++); 
     } else {
       ++it;
     }
   }
-
+  
   for (SignatureMap::const_iterator it = d_signatures.begin(); it != d_signatures.end(); ++it) {
     TNode signature = it->first;
     // we already processed this signature
@@ -451,31 +451,31 @@ void AbstractionModule::finalizeSignatures() {
     collectArgumentTypes(signature, arg_types, seen);
     Assert (signature.getType().isBoolean());
     // make function return a bitvector of size 1
-    //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u));
+    //Node bv_function = utils::mkNode(kind::ITE, signature, utils::mkConst(1, 1u), utils::mkConst(1, 0u)); 
     TypeNode range = NodeManager::currentNM()->mkBitVectorType(1);
-
+    
     TypeNode abs_type = nm->mkFunctionType(arg_types, range);
     Node abs_func = nm->mkSkolem("abs_$$", abs_type, "abstraction function for bv theory");
     Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n";
 
     // NOTE: signature expression type is BOOLEAN
     d_signatureToFunc[signature] = abs_func;
-    d_funcToSignature[abs_func] = signature;
+    d_funcToSignature[abs_func] = signature; 
   }
 
   d_statistics.d_numFunctionsAbstracted.setData(d_signatureToFunc.size());
-
+  
   Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " << d_signatureToFunc.size() << " signatures. \n";
 }
 
 void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) {
   if (seen.find(sig) != seen.end())
     return;
-
+  
   if (sig.getKind() == kind::SKOLEM) {
     types.push_back(sig.getType());
-    seen.insert(sig);
-    return;
+    seen.insert(sig); 
+    return; 
   }
 
   for (unsigned i = 0; i < sig.getNumChildren(); ++i) {
@@ -487,36 +487,36 @@ void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& t
 void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector<Node>& args, TNodeSet& seen) {
   if (seen.find(node)!= seen.end())
     return;
-
+  
   if (node.getKind() == kind::VARIABLE ||
       node.getKind() == kind::CONST_BITVECTOR) {
     // a constant in the node can either map to an argument of the abstraction
-    // or can be hard-coded and part of the abstraction
+    // or can be hard-coded and part of the abstraction 
     if (signature.getKind() == kind::SKOLEM) {
       args.push_back(node);
       seen.insert(node);
     } else {
-      Assert (signature.getKind() == kind::CONST_BITVECTOR);
+      Assert (signature.getKind() == kind::CONST_BITVECTOR); 
     }
-    //
-    return;
+    // 
+    return; 
   }
   Assert (node.getKind() == signature.getKind() &&
-          node.getNumChildren() == signature.getNumChildren());
+          node.getNumChildren() == signature.getNumChildren()); 
 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-    collectArguments(node[i], signature[i], args, seen);
-    seen.insert(node);
+    collectArguments(node[i], signature[i], args, seen); 
+    seen.insert(node); 
   }
 }
 
 
 Node AbstractionModule::abstractSignatures(TNode assertion) {
-  Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n";
+  Debug("bv-abstraction") << "AbstractionModule::abstractSignatures "<< assertion <<"\n"; 
   // assume the assertion has been fully abstracted
   Node signature = getGeneralizedSignature(assertion);
-
-  Debug("bv-abstraction") << "   with sig "<< signature <<"\n";
+  
+  Debug("bv-abstraction") << "   with sig "<< signature <<"\n"; 
   NodeNodeMap::iterator it = d_signatureToFunc.find(signature);
   if (it!= d_signatureToFunc.end()) {
     std::vector<Node> args;
@@ -527,16 +527,16 @@ Node AbstractionModule::abstractSignatures(TNode assertion) {
     collectArguments(assertion, signature, args, seen);
     std::vector<TNode> real_args;
     for (unsigned i = 1; i < args.size(); ++i) {
-      real_args.push_back(args[i]);
+      real_args.push_back(args[i]); 
     }
-    d_argsTable.addEntry(func, real_args);
-    Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args),
+    d_argsTable.addEntry(func, real_args); 
+    Node result = utils::mkNode(kind::EQUAL, utils::mkNode(kind::APPLY_UF, args), 
                                 utils::mkConst(1, 1u));
-    Debug("bv-abstraction") << "=>   "<< result << "\n";
-    Assert (result.getType() == assertion.getType());
-    return result;
+    Debug("bv-abstraction") << "=>   "<< result << "\n"; 
+    Assert (result.getType() == assertion.getType()); 
+    return result; 
   }
-  return assertion;
+  return assertion; 
 }
 
 bool AbstractionModule::isAbstraction(TNode node) {
@@ -557,11 +557,11 @@ bool AbstractionModule::isAbstraction(TNode node) {
   if (constant != utils::mkConst(1, 1u))
     return false;
 
-  TNode func_symbol = func.getOperator();
+  TNode func_symbol = func.getOperator(); 
   if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end())
     return false;
 
-  return true;
+  return true; 
 }
 
 Node AbstractionModule::getInterpretation(TNode node) {
@@ -571,51 +571,51 @@ Node AbstractionModule::getInterpretation(TNode node) {
   Assert (constant.getKind() == kind::CONST_BITVECTOR &&
           apply.getKind() == kind::APPLY_UF);
 
-  Node func = apply.getOperator();
+  Node func = apply.getOperator(); 
   Assert (d_funcToSignature.find(func) != d_funcToSignature.end());
-
+  
   Node sig = d_funcToSignature[func];
-
+  
   // substitute arguments in signature
   TNodeTNodeMap seen;
   unsigned index = 0;
   Node result = substituteArguments(sig, apply, index, seen);
-  Assert (result.getType().isBoolean());
+  Assert (result.getType().isBoolean()); 
   Assert (index == apply.getNumChildren());
   // Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n";
   // Debug("bv-abstraction") << "    => " << result << "\n";
-  return result;
+  return result; 
 }
 
 Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) {
   if (seen.find(signature) != seen.end()) {
-    return seen[signature];
+    return seen[signature]; 
   }
-
+  
   if (signature.getKind() == kind::SKOLEM) {
     // return corresponding argument and increment counter
     seen[signature] = apply[index];
-    return apply[index++];
+    return apply[index++]; 
   }
 
   if (signature.getNumChildren() == 0) {
     Assert (signature.getKind() != kind::VARIABLE &&
-            signature.getKind() != kind::SKOLEM);
+            signature.getKind() != kind::SKOLEM); 
     seen[signature] = signature;
-    return signature;
+    return signature; 
   }
-
+  
   NodeBuilder<> builder(signature.getKind());
   if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
     builder << signature.getOperator();
   }
-
+  
   for (unsigned i = 0; i < signature.getNumChildren(); ++i) {
     Node child = substituteArguments(signature[i], apply, index, seen);
-    builder << child;
+    builder << child; 
   }
 
-  Node result = builder;
+  Node result = builder; 
   seen[signature]= result;
 
   return result;
@@ -625,20 +625,20 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
   if (Dump.isOn("bv-abstraction")) {
     NodeNodeMap seen;
     Node c = reverseAbstraction(conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
+    Dump("bv-abstraction") << PushCommand(); 
     Dump("bv-abstraction") << AssertCommand(c.toExpr());
     Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
+    Dump("bv-abstraction") << PopCommand(); 
   }
 
-  Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n";
+  Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; 
   if (conflict.getKind() != kind::AND)
-    return conflict;
+    return conflict; 
 
   std::vector<Node> conjuncts;
   for (unsigned i = 0; i < conflict.getNumChildren(); ++i)
     conjuncts.push_back(conflict[i]);
-
+  
   theory::SubstitutionMap subst(new context::Context());
   for (unsigned i = 0; i < conjuncts.size(); ++i) {
     TNode conjunct = conjuncts[i];
@@ -658,12 +658,12 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
       } else {
         continue;
       }
-
+      
       Assert (!subst.hasSubstitution(s));
       Assert (!t.isNull() &&
               !s.isNull() &&
               s!= t);
-      subst.addSubstitution(s, t);
+      subst.addSubstitution(s, t); 
 
       for (unsigned k = 0; k < conjuncts.size(); k++) {
         conjuncts[k] = subst.apply(conjuncts[k]);
@@ -671,28 +671,28 @@ Node AbstractionModule::simplifyConflict(TNode conflict) {
     }
   }
   Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts));
-
+  
   Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n";
   Debug("bv-abstraction") << "   => " << new_conflict <<"\n";
 
   if (Dump.isOn("bv-abstraction")) {
-
+    
     NodeNodeMap seen;
     Node nc = reverseAbstraction(new_conflict, seen);
-    Dump("bv-abstraction") << PushCommand();
+    Dump("bv-abstraction") << PushCommand(); 
     Dump("bv-abstraction") << AssertCommand(nc.toExpr());
     Dump("bv-abstraction") << CheckSatCommand();
-    Dump("bv-abstraction") << PopCommand();
+    Dump("bv-abstraction") << PopCommand(); 
   }
-
-  return new_conflict;
+  
+  return new_conflict; 
 }
 
 
 void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instantiations,
                               const std::vector<TNode> functions) {
   // print header
-  Debug("bv-abstraction-dbg") <<"[ ";
+  Debug("bv-abstraction-dbg") <<"[ "; 
   for (unsigned i = 0; i < functions.size(); ++i) {
     for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) {
       Debug("bv-abstraction-dgb") << functions[i][j] <<" ";
@@ -706,16 +706,16 @@ void DebugPrintInstantiations(const std::vector< std::vector<ArgsVec> >& instant
     const std::vector<ArgsVec>& inst = instantiations[i];
     for (unsigned j = 0; j < inst.size(); ++j) {
       for (unsigned k = 0; k < inst[j].size(); ++k) {
-        Debug("bv-abstraction-dbg") << inst[j][k] << " ";
+        Debug("bv-abstraction-dbg") << inst[j][k] << " "; 
       }
-      Debug("bv-abstraction-dbg") << " || ";
+      Debug("bv-abstraction-dbg") << " || "; 
     }
     Debug("bv-abstraction-dbg") <<"]\n";
   }
 }
 
 void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& lemmas) {
-  Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n";
+  Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; 
   std::vector<TNode> functions;
 
   // collect abstract functions
@@ -737,11 +737,11 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
   // if (functions.size() >= 3) {
   //   // dump conflict
   //   NodeNodeMap seen;
-  //   Node reversed = reverseAbstraction(conflict, seen);
-  //   std::cout << "CONFLICT " << reversed << "\n";
+  //   Node reversed = reverseAbstraction(conflict, seen); 
+  //   std::cout << "CONFLICT " << reversed << "\n"; 
   // }
 
-
+  
   if (functions.size() == 0 || functions.size() > options::bvNumFunc()) {
     return;
   }
@@ -751,31 +751,31 @@ void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& le
   SubstitutionMap skolem_subst(new context::Context());
   SubstitutionMap reverse_skolem(new context::Context());
   makeFreshSkolems(conflict, skolem_subst, reverse_skolem);
-
+  
   Node skolemized_conflict = skolem_subst.apply(conflict);
   for (unsigned i = 0; i < functions.size(); ++i) {
     functions[i] = skolem_subst.apply(functions[i]);
   }
 
-  conflict = skolem_subst.apply(conflict);
+  conflict = skolem_subst.apply(conflict); 
 
   LemmaInstantiatior inst(functions, d_argsTable, conflict);
   std::vector<Node> new_lemmas;
-  inst.generateInstantiations(new_lemmas);
+  inst.generateInstantiations(new_lemmas); 
   for (unsigned i = 0; i < new_lemmas.size(); ++i) {
     TNode lemma = reverse_skolem.apply(new_lemmas[i]);
     if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) {
       lemmas.push_back(lemma);
-      Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n";
+      Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; 
       storeLemma(lemma);
 
       if (Dump.isOn("bv-abstraction")) {
         NodeNodeMap seen;
         Node l = reverseAbstraction(lemma, seen);
-        Dump("bv-abstraction") << PushCommand();
+        Dump("bv-abstraction") << PushCommand(); 
         Dump("bv-abstraction") << AssertCommand(l.toExpr());
         Dump("bv-abstraction") << CheckSatCommand();
-        Dump("bv-abstraction") << PopCommand();
+        Dump("bv-abstraction") << PopCommand(); 
       }
     }
   }
@@ -787,18 +787,18 @@ int AbstractionModule::LemmaInstantiatior::next(int val, int index) {
   return -1;
 }
 
-/**
+/** 
  * Assumes the stack without top is consistent, and checks that the
  * full stack is consistent
- *
- * @param stack
- *
- * @return
+ * 
+ * @param stack 
+ * 
+ * @return 
  */
 bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stack) {
   if (stack.empty())
     return true;
-
+  
   unsigned current = stack.size() - 1;
   TNode func = d_functions[current];
   ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator());
@@ -807,12 +807,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
   for (unsigned k = 0; k < args.size(); ++k) {
     TNode s = func[k];
     TNode t = args[k];
-
+      
     TNode s0 = s;
     while (d_subst.hasSubstitution(s0)) {
       s0 = d_subst.getSubstitution(s0);
     }
-
+    
     TNode t0 = t;
     while (d_subst.hasSubstitution(t0)) {
       t0 = d_subst.getSubstitution(t0);
@@ -824,7 +824,7 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
       else
         continue;
     }
-
+      
     if(s0.getMetaKind() == kind::metakind::VARIABLE &&
        t0.isConst()) {
       d_subst.addSubstitution(s0, t0);
@@ -839,12 +839,12 @@ bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stac
 
     Assert (s0.getMetaKind() == kind::metakind::VARIABLE &&
             t0.getMetaKind() == kind::metakind::VARIABLE);
-
+      
     if (s0 != t0) {
       d_subst.addSubstitution(s0, t0);
     }
   }
-  return true;
+  return true; 
 }
 
 bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
@@ -854,13 +854,13 @@ bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) {
 void AbstractionModule::LemmaInstantiatior::mkLemma() {
   Node lemma = d_subst.apply(d_conflict);
   // Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n";
-  d_lemmas.push_back(lemma);
+  d_lemmas.push_back(lemma); 
 }
 
 void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
   if (!isConsistent(stack))
     return;
-
+  
   if (accept(stack)) {
     mkLemma();
     return;
@@ -871,7 +871,7 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
     d_ctx->push();
     stack.push_back(x);
     backtrack(stack);
-
+    
     d_ctx->pop();
     stack.pop_back();
     x = next(x, stack.size());
@@ -880,13 +880,13 @@ void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) {
 
 
 void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<Node>& lemmas) {
-  Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations ";
+  Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; 
 
   std::vector<int> stack;
   backtrack(stack);
-  Assert (d_ctx->getLevel() == 0);
-  Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n";
-  lemmas.swap(d_lemmas);
+  Assert (d_ctx->getLevel() == 0); 
+  Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; 
+  lemmas.swap(d_lemmas); 
 }
 
 void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) {
@@ -910,7 +910,7 @@ void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, Subst
 void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) {
   Assert (fresh_args.size() == 0);
   Assert (func.getKind() == kind::APPLY_UF);
-  TNodeNodeMap d_map;
+  TNodeNodeMap d_map; 
   for (unsigned i = 0; i < func.getNumChildren(); ++i) {
     TNode arg = func[i];
     if (arg.isConst()) {
@@ -918,9 +918,9 @@ void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args)
       continue;
     }
     Assert (arg.getMetaKind() == kind::metakind::VARIABLE);
-    TNodeNodeMap::iterator it = d_map.find(arg);
+    TNodeNodeMap::iterator it = d_map.find(arg); 
     if (it != d_map.end()) {
-      fresh_args.push_back(it->second);
+      fresh_args.push_back(it->second); 
     } else {
       Node skolem = utils::mkVar(utils::getSize(arg));
       d_map[arg] = skolem;
@@ -947,7 +947,7 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect
     Debug("bv-abstraction-dbg") <<"\n";
   }
 
-
+  
   SubstitutionMap subst(new context::Context());
 
   for (unsigned i = 0; i < ss.size(); ++i) {
@@ -982,10 +982,10 @@ Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vect
     Assert (s0 != t0);
     subst.addSubstitution(s0, t0);
   }
-
+  
   Node res = subst.apply(conflict);
-  Debug("bv-abstraction-dbg") << "  Lemma: " << res <<"\n";
-  return res;
+  Debug("bv-abstraction-dbg") << "  Lemma: " << res <<"\n"; 
+  return res; 
 }
 
 void AbstractionModule::storeLemma(TNode lemma) {
@@ -996,7 +996,7 @@ void AbstractionModule::storeLemma(TNode lemma) {
       atom = atom.getKind() == kind::NOT ? atom[0] : atom;
       Assert (atom.getKind() != kind::NOT);
       Assert (utils::isBVPredicate(atom));
-      d_lemmaAtoms.insert(atom);
+      d_lemmaAtoms.insert(atom); 
     }
   } else {
     lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma;
@@ -1009,9 +1009,9 @@ void AbstractionModule::storeLemma(TNode lemma) {
 bool AbstractionModule::isLemmaAtom(TNode node) const {
   Assert (node.getType().isBoolean());
   node = node.getKind() == kind::NOT? node[0] : node;
-
+  
   return d_inputAtoms.find(node) == d_inputAtoms.end() &&
-    d_lemmaAtoms.find(node) != d_lemmaAtoms.end();
+    d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); 
 }
 
 void AbstractionModule::addInputAtom(TNode atom) {
@@ -1022,31 +1022,31 @@ void AbstractionModule::addInputAtom(TNode atom) {
 
 void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) {
   Assert (args.size() == d_arity);
-  d_data.push_back(args);
+  d_data.push_back(args); 
 }
 
 void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) {
   if (d_data.find(signature) == d_data.end()) {
-    d_data[signature] = ArgsTableEntry(args.size());
+    d_data[signature] = ArgsTableEntry(args.size()); 
   }
   ArgsTableEntry& entry = d_data[signature];
-  entry.addArguments(args);
+  entry.addArguments(args); 
 }
 
 
 bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const {
-  return d_data.find(signature) != d_data.end();
+  return d_data.find(signature) != d_data.end(); 
 }
 
 AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) {
   Assert (hasEntry(signature));
-  return d_data.find(signature)->second;
+  return d_data.find(signature)->second; 
 }
 
-AbstractionModule::Statistics::Statistics(const std::string& name)
-  : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
-  , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0)
-  , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime")
+AbstractionModule::Statistics::Statistics()
+  : d_numFunctionsAbstracted("theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
+  , d_numArgsSkolemized("theory::bv::AbstractioModule::NumArgsSkolemized", 0)
+  , d_abstractionTime("theory::bv::AbstractioModule::AbstractionTime")
 {
   smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
   smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 5d48b926e..5d580f6ce 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -38,11 +38,11 @@ class AbstractionModule {
     IntStat d_numFunctionsAbstracted;
     IntStat d_numArgsSkolemized;
     TimerStat d_abstractionTime;
-    Statistics(const std::string& name);
+    Statistics();
     ~Statistics();
   };
 
-
+  
   class ArgsTableEntry {
     std::vector<ArgsVec> d_data;
     unsigned d_arity;
@@ -61,11 +61,11 @@ class AbstractionModule {
     unsigned getArity() { return d_arity; }
     unsigned getNumEntries() { return d_data.size(); }
     ArgsVec& getEntry(unsigned i ) { Assert (i < d_data.size()); return d_data[i]; }
-  };
+  }; 
 
   class ArgsTable {
     __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction > d_data;
-    bool hasEntry(TNode signature) const;
+    bool hasEntry(TNode signature) const; 
   public:
     typedef __gnu_cxx::hash_map<TNode, ArgsTableEntry, TNodeHashFunction >::iterator iterator;
     ArgsTable() {}
@@ -75,12 +75,12 @@ class AbstractionModule {
     iterator end() { return d_data.end(); }
   };
 
-  /**
+  /** 
    * Checks if one pattern is a generalization of the other
-   *
-   * @param s
-   * @param t
-   *
+   * 
+   * @param s 
+   * @param t 
+   * 
    * @return 1 if s :> t, 2 if s <: t, 0 if they equivalent and -1 if they are incomparable
    */
   static int comparePatterns(TNode s, TNode t);
@@ -93,7 +93,7 @@ class AbstractionModule {
     theory::SubstitutionMap d_subst;
     TNode d_conflict;
     std::vector<Node> d_lemmas;
-
+    
     void backtrack(std::vector<int>& stack);
     int next(int val, int index);
     bool isConsistent(const std::vector<int>& stack);
@@ -108,7 +108,7 @@ class AbstractionModule {
       , d_conflict(conflict)
       , d_lemmas()
     {
-      Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n";
+      Debug("bv-abstraction-gen") << "LemmaInstantiator conflict:" << conflict << "\n"; 
       // initializing the search space
       for (unsigned i = 0; i < functions.size(); ++i) {
         TNode func_op = functions[i].getOperator();
@@ -118,31 +118,31 @@ class AbstractionModule {
       }
     }
 
-    void generateInstantiations(std::vector<Node>& lemmas);
-
+    void generateInstantiations(std::vector<Node>& lemmas); 
+    
   };
-
+  
   typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
   typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
   typedef __gnu_cxx::hash_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
   typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeNodeMap;
   typedef __gnu_cxx::hash_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-  typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap;
+  typedef __gnu_cxx::hash_map<unsigned, Node> IntNodeMap; 
   typedef __gnu_cxx::hash_map<unsigned, unsigned> IndexMap;
   typedef __gnu_cxx::hash_map<unsigned, std::vector<Node> > SkolemMap;
   typedef __gnu_cxx::hash_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
-
-  ArgsTable d_argsTable;
+  
+  ArgsTable d_argsTable; 
 
   // mapping between signature and uninterpreted function symbol used to
   // abstract the signature
   NodeNodeMap d_signatureToFunc;
-  NodeNodeMap d_funcToSignature;
+  NodeNodeMap d_funcToSignature; 
 
-  NodeNodeMap d_assertionToSignature;
+  NodeNodeMap d_assertionToSignature; 
   SignatureMap d_signatures;
-  NodeNodeMap d_sigToGeneralization;
+  NodeNodeMap d_sigToGeneralization; 
   TNodeSet d_skolems;
 
   // skolems maps
@@ -165,7 +165,7 @@ class AbstractionModule {
   Node getGeneralizedSignature(Node node);
   Node getSignatureSkolem(TNode node);
 
-  unsigned getBitwidthIndex(unsigned bitwidth);
+  unsigned getBitwidthIndex(unsigned bitwidth); 
   void resetSignatureIndex();
   Node computeSignatureRec(TNode, NodeNodeMap&);
   void storeSignature(Node signature, TNode assertion);
@@ -175,14 +175,14 @@ class AbstractionModule {
 
   // crazy instantiation methods
   void generateInstantiations(unsigned current,
-                              std::vector<ArgsTableEntry>& matches,
+                              std::vector<ArgsTableEntry>& matches, 
                               std::vector<std::vector<ArgsVec> >& instantiations,
                               std::vector<std::vector<ArgsVec> >& new_instantiations);
 
   Node tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict);
   void makeFreshArgs(TNode func, std::vector<Node>& fresh_args);
   void makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map);
-
+  
   void skolemizeArguments(std::vector<Node>& assertions);
   Node reverseAbstraction(Node assertion, NodeNodeMap& seen);
 
@@ -192,9 +192,9 @@ class AbstractionModule {
   void storeLemma(TNode lemma);
 
   Statistics d_statistics;
-
+  
 public:
-  AbstractionModule(const std::string& name)
+  AbstractionModule()
     : d_argsTable()
     , d_signatureToFunc()
     , d_funcToSignature()
@@ -207,34 +207,34 @@ public:
     , d_addedLemmas()
     , d_lemmaAtoms()
     , d_inputAtoms()
-    , d_statistics(name)
+    , d_statistics()
   {}
-  /**
+  /** 
    * returns true if there are new uninterepreted functions symbols in the output
-   *
-   * @param assertions
-   * @param new_assertions
-   *
-   * @return
+   * 
+   * @param assertions 
+   * @param new_assertions 
+   * 
+   * @return 
    */
   bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-  /**
-   * Returns true if the node represents an abstraction predicate.
-   *
-   * @param node
-   *
-   * @return
+  /** 
+   * Returns true if the node represents an abstraction predicate. 
+   * 
+   * @param node 
+   * 
+   * @return 
    */
   bool isAbstraction(TNode node);
-  /**
-   * Returns the interpretation of the abstraction predicate.
-   *
-   * @param node
-   *
-   * @return
+  /** 
+   * Returns the interpretation of the abstraction predicate. 
+   * 
+   * @param node 
+   * 
+   * @return 
    */
   Node getInterpretation(TNode node);
-  Node simplifyConflict(TNode conflict);
+  Node simplifyConflict(TNode conflict); 
   void generalizeConflict(TNode conflict, std::vector<Node>& lemmas);
   void addInputAtom(TNode atom);
   bool isLemmaAtom(TNode node) const;
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 6c6c13ee8..b7619c4bb 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -37,9 +37,9 @@ namespace bv {
 
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
-    d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")),
+    d_bitblaster(new TLazyBitblaster(c, bv, "lazy")),
     d_bitblastQueue(c),
-    d_statistics(bv->getFullInstanceName()),
+    d_statistics(),
     d_validModelCache(c, true),
     d_lemmaAtomsQueue(c),
     d_useSatPropagation(options::bitvectorPropagate()),
@@ -55,9 +55,9 @@ BitblastSolver::~BitblastSolver() {
   delete d_bitblaster;
 }
 
-BitblastSolver::Statistics::Statistics(const std::string &instanceName)
-  : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0)
-  , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+BitblastSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
+  , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
@@ -68,8 +68,8 @@ BitblastSolver::Statistics::~Statistics() {
 }
 
 void BitblastSolver::setAbstraction(AbstractionModule* abs) {
-  d_abstractionModule = abs;
-  d_bitblaster->setAbstraction(abs);
+  d_abstractionModule = abs; 
+  d_bitblaster->setAbstraction(abs); 
 }
 
 void BitblastSolver::preRegister(TNode node) {
@@ -117,7 +117,7 @@ void BitblastSolver::bitblastQueue() {
 
 bool BitblastSolver::check(Theory::Effort e) {
   Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); 
 
   ++(d_statistics.d_numCallstoCheck);
 
@@ -135,10 +135,10 @@ bool BitblastSolver::check(Theory::Effort e) {
       // skip atoms that are the result of abstraction lemmas
       if (d_abstractionModule->isLemmaAtom(fact)) {
         d_lemmaAtomsQueue.push_back(fact);
-        continue;
+        continue; 
       }
     }
-
+    
     if (!d_bv->inConflict() &&
         (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
@@ -183,7 +183,7 @@ bool BitblastSolver::check(Theory::Effort e) {
   if (options::bvAbstraction() &&
       e == Theory::EFFORT_FULL &&
       d_lemmaAtomsQueue.size()) {
-
+    
     // bit-blast lemma atoms
     while(!d_lemmaAtomsQueue.empty()) {
       TNode lemma_atom = d_lemmaAtomsQueue.front();
@@ -199,7 +199,7 @@ bool BitblastSolver::check(Theory::Effort e) {
         return false;
       }
     }
-
+    
     Assert(!d_bv->inConflict());
     bool ok = d_bitblaster->solve();
     if (!ok) {
@@ -210,9 +210,9 @@ bool BitblastSolver::check(Theory::Effort e) {
       ++(d_statistics.d_numBBLemmas);
       return false;
     }
-
+    
   }
-
+  
 
   return true;
 }
@@ -228,9 +228,9 @@ void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
 Node BitblastSolver::getModelValue(TNode node)
 {
   if (d_bv->d_invalidateModelCache.get()) {
-    d_bitblaster->invalidateModelCache();
+    d_bitblaster->invalidateModelCache(); 
   }
-  d_bv->d_invalidateModelCache.set(false);
+  d_bv->d_invalidateModelCache.set(false); 
   Node val = d_bitblaster->getTermModel(node, true);
   return val;
 }
@@ -241,9 +241,9 @@ void BitblastSolver::setConflict(TNode conflict) {
   Node final_conflict = conflict;
   if (options::bitvectorQuickXplain() &&
       conflict.getKind() == kind::AND) {
-    // std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
+    // std::cout << "Original conflict " << conflict.getNumChildren() << "\n"; 
     final_conflict = d_quickXplain->minimizeConflict(conflict);
-    //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
+    //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n"; 
   }
   d_bv->setConflict(final_conflict);
 }
@@ -256,3 +256,4 @@ void BitblastSolver::setProofLog( BitVectorProof * bvp ) {
 }/* namespace CVC4::theory::bv */
 }/* namespace CVC4::theory */
 }/* namespace CVC4 */
+
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index fe16d2702..e9300138b 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -37,7 +37,7 @@ class BitblastSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     IntStat d_numBBLemmas;
-    Statistics(const std::string &instanceName);
+    Statistics();
     ~Statistics();
   };
   /** Bitblaster */
@@ -71,8 +71,8 @@ public:
   Node getModelValue(TNode node);
   bool isComplete() { return true; }
   void bitblastQueue();
-  void setAbstraction(AbstractionModule* module);
-  uint64_t computeAtomWeight(TNode atom);
+  void setAbstraction(AbstractionModule* module); 
+  uint64_t computeAtomWeight(TNode atom); 
   void setProofLog( BitVectorProof * bvp );
 };
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index fec93e033..f5b2175f3 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -42,16 +42,14 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
-                   OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, std::string name)
-  : Theory(THEORY_BV, c, u, out, valuation, logicInfo, name),
+TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo)
+  : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
     d_subtheories(),
     d_subtheoryMap(),
-    d_statistics(getFullInstanceName()),
+    d_statistics(),
     d_staticLearnCache(),
     d_BVDivByZero(),
     d_BVRemByZero(),
@@ -64,7 +62,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c),
     d_eagerSolver(NULL),
-    d_abstractionModule(new AbstractionModule(getFullInstanceName())),
+    d_abstractionModule(new AbstractionModule()),
     d_isCoreTheory(false),
     d_calledPreregister(false)
 {
@@ -121,14 +119,14 @@ void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) {
   getOutputChannel().spendResource(ammount);
 }
 
-TheoryBV::Statistics::Statistics(const std::string &name):
-  d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"),
-  d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0),
-  d_solveTimer(name + "theory::bv::solveTimer"),
-  d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0),
-  d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0),
-  d_weightComputationTimer(name + "theory::bv::weightComputationTimer"),
-  d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0)
+TheoryBV::Statistics::Statistics():
+  d_avgConflictSize("theory::bv::AvgBVConflictSize"),
+  d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
+  d_solveTimer("theory::bv::solveTimer"),
+  d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
+  d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0),
+  d_weightComputationTimer("theory::bv::weightComputationTimer"),
+  d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
@@ -236,7 +234,7 @@ void TheoryBV::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
         for (unsigned i = 0; i < args1.getNumChildren(); ++i) {
           eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
         }
-
+        
         Node args_eq = eqs.size() == 1 ? eqs[0] : nm->mkNode(kind::AND, eqs);
         Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
         Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
@@ -278,9 +276,9 @@ Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
 
     // if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     //   // Ackermanize UF if using eager bit-blasting
-    //   Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num);
+    //   Node ackerman_var = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_ACKERMANIZE_UDIV : kind::BITVECTOR_ACKERMANIZE_UREM, num); 
     //   node = nm->mkNode(kind::ITE, den_eq_0, ackerman_var, divTotalNumDen);
-    //   return node;
+    //   return node; 
     // } else {
       Node divByZero = getBVDivByZero(node.getKind(), width);
       Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
@@ -329,7 +327,7 @@ void TheoryBV::sendConflict() {
   if (d_conflictNode.isNull()) {
     return;
   } else {
-    Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
+    Debug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
     d_out->conflict(d_conflictNode);
     d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
     d_conflictNode = Node::null();
@@ -705,7 +703,7 @@ Node TheoryBV::explain(TNode node) {
   // return the explanation
   Node explanation = utils::mkAnd(assumptions);
   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
-  Debug("bitvector::explain") << "TheoryBV::explain done. \n";
+  Debug("bitvector::explain") << "TheoryBV::explain done. \n"; 
   return explanation;
 }
 
@@ -725,7 +723,7 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
     return EQUALITY_UNKNOWN;
-  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+  Assert (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); 
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ba2a4fc2a..7f0494dc1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -56,8 +56,7 @@ class TheoryBV : public Theory {
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
-           Valuation valuation, const LogicInfo& logicInfo,
-           std::string name = "");
+           Valuation valuation, const LogicInfo& logicInfo);
 
   ~TheoryBV();
 
@@ -89,8 +88,8 @@ public:
 
   void presolve();
 
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
-
+  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  
   void setProofLog( BitVectorProof * bvp );
 
 private:
@@ -101,10 +100,10 @@ private:
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;
     IntStat     d_numCallsToCheckFullEffort;
-    IntStat     d_numCallsToCheckStandardEffort;
+    IntStat     d_numCallsToCheckStandardEffort; 
     TimerStat   d_weightComputationTimer;
     IntStat     d_numMultSlice;
-    Statistics(const std::string &name);
+    Statistics();
     ~Statistics();
   };
 
@@ -122,12 +121,12 @@ private:
    */
   Node getBVDivByZero(Kind k, unsigned width);
 
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; 
   void collectFunctionSymbols(TNode term, TNodeSet& seen);
   void storeFunction(TNode func, TNode term);
   typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
   NodeSet d_staticLearnCache;
-
+  
   /**
    * Maps from bit-vector width to division-by-zero uninterpreted
    * function symbols.
@@ -143,7 +142,7 @@ private:
   CVC4::theory::SubstitutionMap d_funcToSkolem;
 
   context::CDO<bool> d_lemmasAdded;
-
+  
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
@@ -166,17 +165,17 @@ private:
   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
   PropagatedMap d_propagatedBy;
 
-  EagerBitblastSolver* d_eagerSolver;
+  EagerBitblastSolver* d_eagerSolver; 
   AbstractionModule* d_abstractionModule;
   bool d_isCoreTheory;
   bool d_calledPreregister;
-
+  
   bool wasPropagatedBySubtheory(TNode literal) const {
-    return d_propagatedBy.find(literal) != d_propagatedBy.end();
+    return d_propagatedBy.find(literal) != d_propagatedBy.end(); 
   }
-
+  
   SubTheory getPropagatingSubtheory(TNode literal) const {
-    Assert(wasPropagatedBySubtheory(literal));
+    Assert(wasPropagatedBySubtheory(literal)); 
     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
     return (*find).second;
   }
@@ -192,7 +191,7 @@ private:
   void addSharedTerm(TNode t);
 
   bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
-
+  
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   Node getModelValue(TNode var);
@@ -213,7 +212,7 @@ private:
 
   void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
 
-  void checkForLemma(TNode node);
+  void checkForLemma(TNode node); 
 
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 618fda4c0..1ab4c228b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,8 +26,6 @@
 #include "options/bv_options.h"
 #include "options/options.h"
 #include "options/quantifiers_options.h"
-#include "proof/cnf_proof.h"
-#include "proof/lemma_proof.h"
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
 #include "smt/ite_removal.h"
@@ -55,104 +53,6 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-inline void flattenAnd(Node n, std::vector<TNode>& out){
-  Assert(n.getKind() == kind::AND);
-  for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
-    Node curr = *i;
-    if(curr.getKind() == kind::AND){
-      flattenAnd(curr, out);
-    }else{
-      out.push_back(curr);
-    }
-  }
-}
-
-inline Node flattenAnd(Node n){
-  std::vector<TNode> out;
-  flattenAnd(n, out);
-  return NodeManager::currentNM()->mkNode(kind::AND, out);
-}
-
-theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma,
-                                                             ProofRule rule,
-                                                             bool removable,
-                                                             bool preprocess,
-                                                             bool sendAtoms)
-  throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl;
-  ++ d_statistics.lemmas;
-  d_engine->d_outputChannelUsed = true;
-
-  LemmaProofRecipe* proofRecipe = NULL;
-  PROOF({
-      // Theory lemmas have one step that proves the empty clause
-      proofRecipe = new LemmaProofRecipe;
-
-      Node emptyNode;
-      LemmaProofRecipe::ProofStep proofStep(d_theory, emptyNode);
-
-      Node rewritten;
-      if (lemma.getKind() == kind::OR) {
-        for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
-          rewritten = theory::Rewriter::rewrite(lemma[i]);
-          if (rewritten != lemma[i]) {
-            proofRecipe->addRewriteRule(lemma[i].negate(), rewritten.negate());
-          }
-          proofStep.addAssertion(lemma[i]);
-          proofRecipe->addBaseAssertion(rewritten);
-        }
-      } else {
-        rewritten = theory::Rewriter::rewrite(lemma);
-        if (rewritten != lemma) {
-          proofRecipe->addRewriteRule(lemma.negate(), rewritten.negate());
-        }
-        proofStep.addAssertion(lemma);
-        proofRecipe->addBaseAssertion(rewritten);
-      }
-      proofRecipe->addStep(proofStep);
-    });
-
-  theory::LemmaStatus result = d_engine->lemma(lemma,
-                                               rule,
-                                               false,
-                                               removable,
-                                               preprocess,
-                                               sendAtoms ? d_theory : theory::THEORY_LAST,
-                                               proofRecipe);
-  PROOF(delete proofRecipe;);
-  return result;
-}
-
-theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable)
-  throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
-  ++ d_statistics.lemmas;
-  d_engine->d_outputChannelUsed = true;
-
-
-  LemmaProofRecipe* proofRecipe = NULL;
-  Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl;
-  theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, proofRecipe);
-  return result;
-}
-
-bool TheoryEngine::EngineOutputChannel::propagate(TNode literal)
-  throw(AssertionException, UnsafeInterruptException) {
-  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
-  ++ d_statistics.propagations;
-  d_engine->d_outputChannelUsed = true;
-  return d_engine->propagate(literal, d_theory);
-}
-
-void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf)
-  throw(AssertionException, UnsafeInterruptException) {
-  Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
-  Assert (pf == NULL); // Theory shouldn't be producing proofs yet
-  ++ d_statistics.conflicts;
-  d_engine->d_outputChannelUsed = true;
-  d_engine->conflict(conflictNode, d_theory);
-}
-
 void TheoryEngine::finishInit() {
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
@@ -597,10 +497,7 @@ void TheoryEngine::combineTheories() {
 
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-
-    LemmaProofRecipe* proofRecipe = NULL;
-    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, proofRecipe);
-
+    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory, carePair.theory);
     // This code is supposed to force preference to follow what the theory models already have
     // but it doesn't seem to make a big difference - need to explore more -Clark
     // if (true) {
@@ -1066,7 +963,7 @@ bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, the
 
 void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
 
-  Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
+  Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl;
 
   Assert(toTheoryId != fromTheoryId);
   if(toTheoryId != THEORY_SAT_SOLVER &&
@@ -1279,23 +1176,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
     }
   } else {
-    // We could be propagating a unit-clause lemma. In this case, we need to provide a
-    // recipe.
-    // TODO: Consider putting this someplace else? This is the only refence to the proof
-    // manager in this class.
-
-    PROOF({
-        LemmaProofRecipe proofRecipe;
-        proofRecipe.addBaseAssertion(literal);
-
-        Node emptyNode;
-        LemmaProofRecipe::ProofStep proofStep(theory, emptyNode);
-        proofStep.addAssertion(literal);
-        proofRecipe.addStep(proofStep);
-
-        ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
-      });
-
     // Just send off to the SAT solver
     Assert(d_propEngine->isSatLiteral(literal));
     assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
@@ -1390,7 +1270,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
   return conjunction;
 }
 
-Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
+NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) {
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
 
   bool polarity = node.getKind() != kind::NOT;
@@ -1398,90 +1278,32 @@ Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRe
 
   // If we're not in shared mode, explanations are simple
   if (!d_logicInfo.isSharingEnabled()) {
-    Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
-                             << " Responsible theory is: "
-                             << theoryOf(atom)->getId() << std::endl;
-
     Node explanation = theoryOf(atom)->explain(node);
     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
-    PROOF({
-        if(proofRecipe) {
-          Node emptyNode;
-          LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode);
-          proofStep.addAssertion(node);
-          proofRecipe->addBaseAssertion(node);
-
-          if (explanation.getKind() == kind::AND) {
-            // If the explanation is a conjunction, the recipe for the corresponding lemma is
-            // the negation of its conjuncts.
-            Node flat = flattenAnd(explanation);
-            for (unsigned i = 0; i < flat.getNumChildren(); ++i) {
-              if (flat[i].isConst() && flat[i].getConst<bool>()) {
-                ++ i;
-                continue;
-              }
-              if (flat[i].getKind() == kind::NOT &&
-                  flat[i][0].isConst() && !flat[i][0].getConst<bool>()) {
-                ++ i;
-                continue;
-              }
-              Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
-                                       << flat[i].negate() << std::endl;
-              proofStep.addAssertion(flat[i].negate());
-              proofRecipe->addBaseAssertion(flat[i].negate());
-            }
-          } else {
-            // The recipe for proving it is by negating it. "True" is not an acceptable reason.
-            if (!((explanation.isConst() && explanation.getConst<bool>()) ||
-                  (explanation.getKind() == kind::NOT &&
-                   explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
-              proofStep.addAssertion(explanation.negate());
-              proofRecipe->addBaseAssertion(explanation.negate());
-            }
-          }
-
-          proofRecipe->addStep(proofStep);
-        }
-      });
-
-    return explanation;
+    return NodeTheoryPair(explanation, theoryOf(atom)->getId());
   }
 
-  Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
-
   // Initial thing to explain
   NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
   Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
 
   NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
-  Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
-                           << nodeExplainerPair.node
-                           << " is theory: " << nodeExplainerPair.theory << std::endl;
   TheoryId explainer = nodeExplainerPair.theory;
 
   // Create the workplace for explanations
   std::vector<NodeTheoryPair> explanationVector;
   explanationVector.push_back(d_propagationMap[toExplain]);
   // Process the explanation
-  if (proofRecipe) {
-    Node emptyNode;
-    LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode);
-    proofStep.addAssertion(node);
-    proofRecipe->addStep(proofStep);
-    proofRecipe->addBaseAssertion(node);
-  }
-
-  getExplanation(explanationVector, proofRecipe);
+  getExplanation(explanationVector);
   Node explanation = mkExplanation(explanationVector);
 
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
 
-  return explanation;
+  return NodeTheoryPair(explanation, explainer);
 }
 
 Node TheoryEngine::getExplanation(TNode node) {
-  LemmaProofRecipe *dontCareRecipe = NULL;
-  return getExplanationAndRecipe(node, dontCareRecipe);
+  return getExplanationAndExplainer(node).node;
 }
 
 struct AtomsCollect {
@@ -1584,7 +1406,7 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         bool removable,
                                         bool preprocess,
                                         theory::TheoryId atomsTo,
-                                        LemmaProofRecipe* proofRecipe) {
+                                        theory::TheoryId ownerTheory) {
   // For resource-limiting (also does a time check).
   // spendResource();
 
@@ -1634,10 +1456,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, proofRecipe, node);
+  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, ownerTheory, node);
   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
     additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
-    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, proofRecipe, node);
+    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1671,69 +1493,22 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
                         << CheckSatCommand(conflict.toExpr());
   }
 
-  LemmaProofRecipe* proofRecipe = NULL;
-  PROOF({
-      proofRecipe = new LemmaProofRecipe;
-      Node emptyNode;
-      LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
-
-      if (conflict.getKind() == kind::AND) {
-        for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
-          proofStep.addAssertion(conflict[i].negate());
-        }
-      } else {
-        proofStep.addAssertion(conflict.negate());
-      }
-
-      proofRecipe->addStep(proofStep);
-    });
-
   // In the multiple-theories case, we need to reconstruct the conflict
   if (d_logicInfo.isSharingEnabled()) {
     // Create the workplace for explanations
     std::vector<NodeTheoryPair> explanationVector;
     explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
-
     // Process the explanation
-    getExplanation(explanationVector, proofRecipe);
+    getExplanation(explanationVector);
     Node fullConflict = mkExplanation(explanationVector);
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
-    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
-
+    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
   } else {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
-    PROOF({
-        if (conflict.getKind() == kind::AND) {
-          // If the conflict is a conjunction, the corresponding lemma is derived by negating
-          // its conjuncts.
-          for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
-            if (conflict[i].isConst() && conflict[i].getConst<bool>()) {
-              ++ i;
-              continue;
-            }
-            if (conflict[i].getKind() == kind::NOT &&
-                conflict[i][0].isConst() && !conflict[i][0].getConst<bool>()) {
-              ++ i;
-              continue;
-            }
-            proofRecipe->getStep(0)->addAssertion(conflict[i].negate());
-            proofRecipe->addBaseAssertion(conflict[i].negate());
-          }
-        } else {
-          proofRecipe->getStep(0)->addAssertion(conflict.negate());
-          proofRecipe->addBaseAssertion(conflict.negate());
-        }
-      });
-
-    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, proofRecipe);
+    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
   }
-
-  PROOF({
-      delete proofRecipe;
-      proofRecipe = NULL;
-    });
 }
 
 void TheoryEngine::staticInitializeBVOptions(const std::vector<Node>& assertions) {
@@ -1885,21 +1660,19 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   return result;
 }
 
-void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
+void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector)
+{
   Assert(explanationVector.size() > 0);
 
   unsigned i = 0; // Index of the current literal we are processing
   unsigned j = 0; // Index of the last literal we are keeping
 
-  std::set<Node> inputAssertions;
-  PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions(););
-
   while (i < explanationVector.size()) {
+
     // Get the current literal to explain
     NodeTheoryPair toExplain = explanationVector[i];
 
-    Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
-
+    Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
 
     // If a true constant or a negation of a false constant we can ignore it
     if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
@@ -1913,7 +1686,6 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
 
     // If from the SAT solver, keep it
     if (toExplain.theory == THEORY_SAT_SOLVER) {
-      Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
       explanationVector[j++] = explanationVector[i++];
       continue;
     }
@@ -1932,26 +1704,10 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     // See if it was sent to the theory by another theory
     PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
     if (find != d_propagationMap.end()) {
-      Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
-                               << theoryOf((*find).second.theory)->getId() << ")" << std::endl;
       // There is some propagation, check if its a timely one
       if ((*find).second.timestamp < toExplain.timestamp) {
-        Debug("theory::explain") << "\tRelevant timetsamp, pushing "
-                                 << (*find).second.node << "to index = " << explanationVector.size() << std::endl;
         explanationVector.push_back((*find).second);
-        ++i;
-
-        PROOF({
-            if (toExplain.node != (*find).second.node) {
-              Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node
-                                   << ", toExplain = " << (*find).second.node << std::endl;
-
-              if (proofRecipe) {
-                proofRecipe->addRewriteRule(toExplain.node, (*find).second.node);
-              }
-            }
-          })
-
+        ++ i;
         continue;
       }
     }
@@ -1960,62 +1716,22 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     Node explanation;
     if (toExplain.theory == THEORY_BUILTIN) {
       explanation = d_sharedTerms.explain(toExplain.node);
-      Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
     } else {
       explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
-      Debug("theory::explain") << "\tTerm was propagated by owner theory: "
-                               << theoryOf(toExplain.theory)->getId()
-                               << ". Explanation: " << explanation << std::endl;
     }
-
     Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
     Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
     // Mark the explanation
     NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
     explanationVector.push_back(newExplain);
-
     ++ i;
-
-    PROOF({
-        if (proofRecipe) {
-          // If we're expanding the target node of the explanation (this is the first expansion...),
-          // we don't want to add it as a separate proof step. It is already part of the assertions.
-          if (inputAssertions.find(toExplain.node) == inputAssertions.end()) {
-            LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.node);
-            if (explanation.getKind() == kind::AND) {
-              Node flat = flattenAnd(explanation);
-              for (unsigned k = 0; k < flat.getNumChildren(); ++ k) {
-                // If a true constant or a negation of a false constant we can ignore it
-                if (! ((flat[k].isConst() && flat[k].getConst<bool>()) ||
-                       (flat[k].getKind() == kind::NOT && flat[k][0].isConst() && !flat[k][0].getConst<bool>()))) {
-                  proofStep.addAssertion(flat[k].negate());
-                }
-              }
-            } else {
-             if (! ((explanation.isConst() && explanation.getConst<bool>()) ||
-                    (explanation.getKind() == kind::NOT && explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
-               proofStep.addAssertion(explanation.negate());
-             }
-            }
-            proofRecipe->addStep(proofStep);
-          }
-        }
-      });
   }
 
   // Keep only the relevant literals
   explanationVector.resize(j);
-
-  PROOF({
-      if (proofRecipe) {
-        // The remaining literals are the base of the proof
-        for (unsigned k = 0; k < explanationVector.size(); ++k) {
-          proofRecipe->addBaseAssertion(explanationVector[k].node.negate());
-        }
-      }
-    });
 }
 
+
 void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
 {
   d_unconstrainedSimp->processAssertions(assertions);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 53c4aac77..db94edd7c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -50,7 +50,6 @@
 namespace CVC4 {
 
 class ResourceManager;
-class LemmaProofRecipe;
 
 /**
  * A pair of a theory and a node. This is used to mark the flow of
@@ -271,18 +270,46 @@ class TheoryEngine {
       }
     }
 
-    void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException);
+    void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) {
+      Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
+      Assert(pf == NULL); // theory shouldn't be producing proofs yet
+      ++ d_statistics.conflicts;
+      d_engine->d_outputChannelUsed = true;
+      d_engine->conflict(conflictNode, d_theory);
+    }
 
-    bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException);
+    bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) {
+      Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
+      ++ d_statistics.propagations;
+      d_engine->d_outputChannelUsed = true;
+      return d_engine->propagate(literal, d_theory);
+    }
 
     theory::LemmaStatus lemma(TNode lemma,
                               ProofRule rule,
                               bool removable = false,
                               bool preprocess = false,
                               bool sendAtoms = false)
-      throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException);
+      throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+      Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
+      ++ d_statistics.lemmas;
+      d_engine->d_outputChannelUsed = true;
+      return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST, d_theory);
+    }
 
-    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException);
+    /*theory::LemmaStatus preservedLemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) {
+      Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::preservedLemma(" << lemma << ")" << std::endl;
+      ++ d_statistics.lemmas;
+      d_engine->d_outputChannelUsed = true;
+      return d_engine->lemma(lemma, false, removable, preprocess, d_theory);
+    }*/
+
+    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+      Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::splitLemma(" << lemma << ")" << std::endl;
+      ++ d_statistics.lemmas;
+      d_engine->d_outputChannelUsed = true;
+      return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory);
+    }
 
     void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       NodeManager* curr = NodeManager::currentNM();
@@ -429,7 +456,7 @@ class TheoryEngine {
                             bool removable,
                             bool preprocess,
                             theory::TheoryId atomsTo,
-                            LemmaProofRecipe* proofRecipe);
+                            theory::TheoryId ownerTheory);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
@@ -579,10 +606,9 @@ private:
    * asking relevant theories to explain the propagations. Initially
    * the explanation vector should contain only the element (node, theory)
    * where the node is the one to be explained, and the theory is the
-   * theory that sent the literal. The lemmaProofRecipe will contain a list
-   * of the explanation steps required to produce the original node.
+   * theory that sent the literal.
    */
-  void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe);
+  void getExplanation(std::vector<NodeTheoryPair>& explanationVector);
 
 public:
 
@@ -704,7 +730,7 @@ public:
    * Returns an explanation of the node propagated to the SAT solver and the theory
    * that propagated it.
    */
-  Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe);
+  NodeTheoryPair getExplanationAndExplainer(TNode node);
 
   /**
    * collect model info
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 25b12f75f..9b429765e 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -964,9 +964,12 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
           std::vector<EqProof *> orderedChildren;
           bool nullCongruenceFound = false;
           for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
-            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
-                eqpc->d_children[i]->d_node.isNull()) {
+            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) {
+
+              // For now, assume there can only be one null congruence child
+              Assert(!nullCongruenceFound);
               nullCongruenceFound = true;
+
               Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl;
               orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]);
               orderedChildren.push_back(eqpc->d_children[i]->d_children[1]);
@@ -1189,9 +1192,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
                 getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
                 if( eqpc ) {
                   eqpc->d_children.push_back( eqpcc );
-
-                  Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl;
-                  eqpc->debug_print("pf::ee", 1);
                 }
               }
 
@@ -1605,7 +1605,6 @@ void EqualityEngine::propagate() {
 }
 
 void EqualityEngine::debugPrintGraph() const {
-  Debug("equality::graph") << std::endl << "Dumping graph" << std::endl;
   for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
 
     Debug("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
@@ -1619,7 +1618,6 @@ void EqualityEngine::debugPrintGraph() const {
 
     Debug("equality::graph") << std::endl;
   }
-  Debug("equality::graph") << std::endl;
 }
 
 bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
@@ -2211,15 +2209,9 @@ bool EqClassIterator::isFinished() const {
   return d_current == null_id;
 }
 
-void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const {
-  for(unsigned i=0; i<tb; i++) { Debug( c ) << "  "; }
-
-  if (prettyPrinter)
-    Debug( c ) << prettyPrinter->printTag(d_id);
-  else
-    Debug( c ) << d_id;
-
-  Debug( c ) << "(";
+void EqProof::debug_print( const char * c, unsigned tb ) const{
+  for( unsigned i=0; i<tb; i++ ) { Debug( c ) << "  "; }
+  Debug( c ) << d_id << "(";
   if( !d_children.empty() || !d_node.isNull() ){
     if( !d_node.isNull() ){
       Debug( c ) << std::endl;
@@ -2229,7 +2221,7 @@ void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrint
     for( unsigned i=0; i<d_children.size(); i++ ){
       if( i>0 || !d_node.isNull() ) Debug( c ) << ",";
       Debug( c ) << std::endl;
-      d_children[i]->debug_print( c, tb+1, prettyPrinter );
+      d_children[i]->debug_print( c, tb+1 );
     }
   }
   Debug( c ) << ")" << std::endl;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 843e7ce7f..f30f1e8a0 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -902,17 +902,11 @@ public:
 class EqProof
 {
 public:
-  class PrettyPrinter {
-  public:
-    virtual ~PrettyPrinter() {}
-    virtual std::string printTag(unsigned tag) = 0;
-  };
-
   EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
   unsigned d_id;
   Node d_node;
   std::vector< EqProof * > d_children;
-  void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const;
+  void debug_print( const char * c, unsigned tb = 0 ) const;
 };/* class EqProof */
 
 } // Namespace eq
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9c461f57b..d1685bdd1 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -502,7 +502,7 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
 void TheoryUF::computeCareGraph() {
 
   if (d_sharedTerms.size() > 0) {
-    //use term indexing
+    //use term indexing 
     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
     std::map< Node, quantifiers::TermArgTrie > index;
     std::map< Node, unsigned > arity;
@@ -533,7 +533,6 @@ void TheoryUF::computeCareGraph() {
 
 void TheoryUF::conflict(TNode a, TNode b) {
   eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
-
   if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b),pf);
   } else {