Merged bit-vector and uf proof branch.

33 files changed, 470 insertions, 262 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 508a4b323..cbcccd734 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -26,9 +26,10 @@
 #include "smt_util/command.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "proof/theory_proof.h"
+#include "proof/proof_manager.h"
 #include "theory/valuation.h"
 
-
 using namespace std;
 
 namespace CVC4 {
@@ -54,27 +55,28 @@ const bool d_solveWrite2 = false;
 
 TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
                            OutputChannel& out, Valuation valuation,
-                           const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals),
-      d_numRow("theory::arrays::number of Row lemmas", 0),
-      d_numExt("theory::arrays::number of Ext lemmas", 0),
-      d_numProp("theory::arrays::number of propagations", 0),
-      d_numExplain("theory::arrays::number of explanations", 0),
-      d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
-      d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
-      d_numGetModelValSplits("theory::arrays::number of getModelVal splits", 0),
-      d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
-      d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
-      d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
-      d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
+                           const LogicInfo& logicInfo, SmtGlobals* globals,
+                           std::string name)
+  : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, globals, name),
+      d_numRow(name + "theory::arrays::number of Row lemmas", 0),
+      d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
+      d_numProp(name + "theory::arrays::number of propagations", 0),
+      d_numExplain(name + "theory::arrays::number of explanations", 0),
+      d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear", 0),
+      d_numSharedArrayVarSplits(name + "theory::arrays::number of shared array var splits", 0),
+      d_numGetModelValSplits(name + "theory::arrays::number of getModelVal splits", 0),
+      d_numGetModelValConflicts(name + "theory::arrays::number of getModelVal conflicts", 0),
+      d_numSetModelValSplits(name + "theory::arrays::number of setModelVal splits", 0),
+      d_numSetModelValConflicts(name + "theory::arrays::number of setModelVal conflicts", 0),
+      d_ppEqualityEngine(u, name + "theory::arrays::TheoryArraysPP" , true),
       d_ppFacts(u),
       //      d_ppCache(u),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_isPreRegistered(c),
-      d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
+      d_mayEqualEqualityEngine(c, name + "theory::arrays::TheoryArraysMayEqual", true),
       d_notify(*this),
-      d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
+      d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true),
       d_conflict(c, false),
       d_backtracker(c),
       d_infoMap(c, &d_backtracker),
@@ -1385,7 +1387,8 @@ void TheoryArrays::check(Effort e) {
           weakEquivBuildCond(r[0], r[1], conjunctions);
           weakEquivBuildCond(r2[0], r[1], conjunctions);
           lemma = mkAnd(conjunctions, true);
-          d_out->lemma(lemma, false, false, true);
+          // LSH FIXME: which kind of arrays lemma is this
+          d_out->lemma(lemma, RULE_INVALID, false, false, true);
           d_readTableContext->pop();
           return;
         }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index f1b02d99e..88d83bfb9 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -128,7 +128,7 @@ class TheoryArrays : public Theory {
 
   TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out,
                Valuation valuation, const LogicInfo& logicInfo,
-               SmtGlobals* globals);
+               SmtGlobals* globals, std::string name = ""); 
   ~TheoryArrays();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index 0990c2f29..bc022a02d 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -253,17 +253,17 @@ void DefaultAndBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   
   Assert(node.getKind() == kind::BITVECTOR_AND &&
          bits.size() == 0);
-  
-  for(unsigned j = 0; j < utils::getSize(node); ++j) {
-    std::vector<T> and_j; 
-    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-      std::vector<T> current;
-      bb->bbTerm(node[i], current);
-      and_j.push_back(current[j]); 
-      Assert(utils::getSize(node) == current.size());
+
+  bb->bbTerm(node[0], bits);
+  std::vector<T> current;
+  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+    bb->bbTerm(node[j], current);
+    for (unsigned i = 0; i < utils::getSize(node); ++i) {
+      bits[i] = mkAnd(bits[i], current[i]);
     }
-    bits.push_back(mkAnd(and_j)); 
+    current.clear();
   }
+  Assert (bits.size() == utils::getSize(node));
 }
 
 template <class T>
@@ -272,17 +272,17 @@ void DefaultOrBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
 
   Assert(node.getKind() == kind::BITVECTOR_OR &&
          bits.size() == 0);
-  
-  for(unsigned j = 0; j < utils::getSize(node); ++j) {
-    std::vector<T> or_j;
-    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-      std::vector<T> current;
-      bb->bbTerm(node[i], current);
-      or_j.push_back(current[j]); 
-      Assert(utils::getSize(node) == current.size());
+
+  bb->bbTerm(node[0], bits);
+  std::vector<T> current;
+  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+    bb->bbTerm(node[j], current);
+    for (unsigned i = 0; i < utils::getSize(node); ++i) {
+      bits[i] = mkOr(bits[i], current[i]);
     }
-    bits.push_back(mkOr(or_j)); 
+    current.clear();
   }
+  Assert (bits.size() == utils::getSize(node));
 }
 
 template <class T>
@@ -291,20 +291,17 @@ void DefaultXorBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
 
   Assert(node.getKind() == kind::BITVECTOR_XOR &&
          bits.size() == 0);
-  
-  for(unsigned j = 0; j < utils::getSize(node); ++j) {
-    std::vector<T> first;
-    bb->bbTerm(node[0], first); 
-    T bitj = first[j];
-    
-    for (unsigned i = 1; i < node.getNumChildren(); ++i) {
-      std::vector<T> current;
-      bb->bbTerm(node[i], current);
-      bitj = mkXor(bitj, current[j]);
-      Assert(utils::getSize(node) == current.size());
+
+  bb->bbTerm(node[0], bits);
+  std::vector<T> current;
+  for(unsigned j = 1; j < node.getNumChildren(); ++j) {
+    bb->bbTerm(node[j], current);
+    for (unsigned i = 0; i < utils::getSize(node); ++i) {
+      bits[i] = mkXor(bits[i], current[i]);
     }
-    bits.push_back(bitj); 
+    current.clear();
   }
+  Assert (bits.size() == utils::getSize(node));
 }
 
 template <class T>
diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h
index a236c69e8..adaed31c1 100644
--- a/src/theory/bv/bitblast_utils.h
+++ b/src/theory/bv/bitblast_utils.h
@@ -221,7 +221,7 @@ inline void shiftAddMultiplier(const std::vector<T>&a, const std::vector<T>&b, s
   T carry_in = mkFalse<T>();
   T carry_out;
     for(unsigned j = 0; j < res.size() -k; ++j) {
-      T aj = mkAnd(a[j], b[k]);
+      T aj = mkAnd(b[k], a[j]);
       carry_out = mkOr(mkAnd(res[j+k], aj),
                        mkAnd( mkXor(res[j+k], aj), carry_in));
       res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in);
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index ec76bb4f6..66eea0997 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -85,6 +85,8 @@ protected:
   TermDefMap d_termCache;
   ModelCache d_modelCache;
 
+  BitVectorProof * d_bvp;
+
   void initAtomBBStrategies();
   void initTermBBStrategies();
 protected:
@@ -105,7 +107,7 @@ public:
 
   bool hasBBTerm(TNode node) const;
   void getBBTerm(TNode node, Bits& bits) const;
-  void storeBBTerm(TNode term, const Bits& bits);
+  virtual void storeBBTerm(TNode term, const Bits& bits);
   /**
    * Return a constant representing the value of a in the  model.
    * If fullModel is true set unconstrained bits to 0. If not return
@@ -171,7 +173,9 @@ public:
   void bbAtom(TNode node);
   Node getBBAtom(TNode atom) const;
   void storeBBAtom(TNode atom, Node atom_bb);
-  bool hasBBAtom(TNode atom) const;
+  void storeBBTerm(TNode node, const Bits& bits);
+  bool hasBBAtom(TNode atom) const; 
+
   TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
   ~TLazyBitblaster() throw();
   /**
@@ -201,6 +205,7 @@ public:
    * constants to equivalence classes that don't already have them
    */
   void collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog( BitVectorProof * bvp );
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
@@ -277,9 +282,12 @@ public:
   bool hasBBAtom(TNode atom) const;
   void bbFormula(TNode formula);
   void storeBBAtom(TNode atom, Node atom_bb);
+  void storeBBTerm(TNode node, const Bits& bits);
+
   bool assertToSat(TNode node, bool propagate = true);
   bool solve();
   void collectModelInfo(TheoryModel* m, bool fullModel);
+  void setProofLog( BitVectorProof * bvp );
 };
 
 class BitblastingRegistrar: public prop::Registrar {
@@ -406,6 +414,7 @@ template <class T>
 TBitblaster<T>::TBitblaster()
   : d_termCache()
   , d_modelCache()
+  , d_bvp( NULL )
 {
   initAtomBBStrategies();
   initTermBBStrategies(); 
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 66b1c4182..2af8d04d6 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -16,6 +16,7 @@
 
 #include "options/bv_options.h"
 #include "theory/bv/bitblaster_template.h"
+#include "proof/bitvector_proof.h"
 #include "theory/bv/bv_eager_solver.h"
 
 using namespace std;
@@ -54,6 +55,12 @@ void EagerBitblastSolver::initialize() {
     d_aigBitblaster = new AigBitblaster();
   } else {
     d_bitblaster = new EagerBitblaster(d_bv);
+    THEORY_PROOF(
+      if( d_bvp ){
+        d_bitblaster->setProofLog( d_bvp );
+        d_bvp->setBitblaster(d_bitblaster);
+      }
+    );
   }
 }
 
@@ -112,3 +119,7 @@ void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
   AlwaysAssert(!d_useAig && d_bitblaster);
   d_bitblaster->collectModelInfo(m, fullModel); 
 }
+
+void EagerBitblastSolver::setProofLog( BitVectorProof * bvp ) {
+  d_bvp = bvp;
+}
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index ff13867cc..cfc84dae1 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -39,7 +39,9 @@ class EagerBitblastSolver {
   EagerBitblaster* d_bitblaster;
   AigBitblaster* d_aigBitblaster;
   bool d_useAig;
-  TheoryBV* d_bv;
+
+  TheoryBV* d_bv; 
+  BitVectorProof * d_bvp;
 
 public:
   EagerBitblastSolver(theory::bv::TheoryBV* bv);
@@ -53,6 +55,7 @@ public:
   bool isInitialized();
   void initialize();
   void collectModelInfo(theory::TheoryModel* m, bool fullModel);
+  void setProofLog( BitVectorProof * bvp );
 };
 
 }
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 9a314fd6a..402dd6be3 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -74,6 +74,8 @@ protected:
 
   /** The bit-vector theory */
   TheoryBV* d_bv;
+  /** proof log */
+  BitVectorProof * d_bvp;
   AssertionQueue d_assertionQueue;
   context::CDO<uint32_t>  d_assertionIndex;
 public:
@@ -102,6 +104,7 @@ public:
     return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
+  virtual void setProofLog( BitVectorProof * bvp ) {}
   AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); }
   AssertionQueue::const_iterator assertionsEnd() { return d_assertionQueue.end(); }
 };
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 9f8cb580c..e7630bb3f 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -24,6 +24,8 @@
 #include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "proof/proof_manager.h"
+#include "proof/bitvector_proof.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -44,7 +46,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
     d_abstractionModule(NULL),
     d_quickCheck(options::bitvectorQuickXplain() ? new BVQuickCheck("bb", bv) : NULL),
     d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("bb", d_quickCheck) :  NULL)
-{}
+{
+}
 
 BitblastSolver::~BitblastSolver() {
   delete d_quickXplain;
@@ -232,40 +235,6 @@ Node BitblastSolver::getModelValue(TNode node)
   return val;
 }
 
-// Node BitblastSolver::getModelValueRec(TNode node)
-// {
-//   Node val;
-//   if (node.isConst()) {
-//     return node;
-//   }
-//   NodeMap::iterator it = d_modelCache.find(node);
-//   if (it != d_modelCache.end()) {
-//     val = (*it).second;
-//     Debug("bitvector-model") << node << " => (cached) " << val <<"\n";
-//     return val;
-//   }
-//   if (d_bv->isLeaf(node)) {
-//     val = d_bitblaster->getVarValue(node);
-//     if (val == Node()) {
-//       // If no value in model, just set to 0
-//       val = utils::mkConst(utils::getSize(node), (unsigned)0);
-//     }
-//   } else {
-//     NodeBuilder<> valBuilder(node.getKind());
-//     if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-//       valBuilder << node.getOperator();
-//     }
-//     for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-//       valBuilder << getModelValueRec(node[i]);
-//     }
-//     val = valBuilder;
-//     val = Rewriter::rewrite(val);
-//   }
-//   Assert(val.isConst());
-//   d_modelCache[node] = val;
-//   Debug("bitvector-model") << node << " => " << val <<"\n";
-//   return val;
-// }
 
 
 void BitblastSolver::setConflict(TNode conflict) {
@@ -279,6 +248,12 @@ void BitblastSolver::setConflict(TNode conflict) {
   d_bv->setConflict(final_conflict);
 }
 
+void BitblastSolver::setProofLog( BitVectorProof * bvp ) {
+  d_bitblaster->setProofLog( bvp );
+  bvp->setBitblaster(d_bitblaster);
+}
+
 }/* namespace CVC4::theory::bv */
 }/* namespace CVC4::theory */
 }/* namespace CVC4 */
+
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 0e066eefb..c69069109 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -73,8 +73,9 @@ public:
   void bitblastQueue();
   void setAbstraction(AbstractionModule* module); 
   uint64_t computeAtomWeight(TNode atom); 
+  void setProofLog( BitVectorProof * bvp );
 };
 
-}
-}
-}
+} /* namespace CVC4::theory::bv */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 000abe62b..2e4f06c38 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -19,16 +19,13 @@
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
+#include "proof/bitvector_proof.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -46,13 +43,19 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
 
-  d_satSolver = prop::SatSolverFactory::createMinisat(
-      d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar,
-                                           d_nullContext, d_bv->globals());
-
+  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext,
+                                                      smtStatisticsRegistry(),
+                                                      "EagerBitblaster");
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
+                                           d_bitblastingRegistrar,
+                                           d_nullContext,
+                                           d_bv->globals(),
+                                           options::proof(),
+                                           "EagerBitblaster");
+  
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
+  d_bvp = NULL;
 }
 
 EagerBitblaster::~EagerBitblaster() {
@@ -85,21 +88,34 @@ void EagerBitblaster::bbAtom(TNode node) {
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
-      Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
-      normalized;
+    d_atomBBStrategies[normalized.getKind()](normalized, this) :
+    normalized;
+
+  if (!options::proof()) {
+    atom_bb = Rewriter::rewrite(atom_bb);
+  }
+
   // asserting that the atom is true iff the definition holds
   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
 
-  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
-  storeBBAtom(node, atom_definition);
+  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); 
+  storeBBAtom(node, atom_bb);
   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
 
 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
-  // no need to store the definition for the lazy bit-blaster
-  d_bbAtoms.insert(atom);
+  if( d_bvp ){
+    d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
+  }
+  d_bbAtoms.insert(atom); 
 }
 
+void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
+  if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
+  d_termCache.insert(std::make_pair(node, bits));
+}
+
+
 bool EagerBitblaster::hasBBAtom(TNode atom) const {
   return d_bbAtoms.find(atom) != d_bbAtoms.end();
 }
@@ -211,6 +227,12 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   }
 }
 
+void EagerBitblaster::setProofLog( BitVectorProof * bvp ) {
+  d_bvp = bvp;
+  d_satSolver->setProofLog(bvp);
+  bvp->initCnfProof(d_cnfStream, d_nullContext);
+}
+
 bool EagerBitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 34a9418dd..9268e2152 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -25,7 +25,9 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
-#include "theory_bv_utils.h"
+#include "proof/bitvector_proof.h"
+#include "proof/proof_manager.h"
+#include "theory/bv/theory_bv_utils.h"
 
 namespace CVC4 {
 namespace theory {
@@ -51,8 +53,12 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
       c, smtStatisticsRegistry(), name);
   d_nullRegistrar = new prop::NullRegistrar();
   d_nullContext = new context::Context();
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
-                                           d_nullContext, d_bv->globals());
+  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
+                                           d_nullRegistrar,
+                                           d_nullContext,
+                                           d_bv->globals(),
+                                           options::proof(),
+                                           "LazyBitblaster");
 
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
@@ -127,8 +133,12 @@ void TLazyBitblaster::bbAtom(TNode node) {
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
-    Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
-    normalized;
+                 d_atomBBStrategies[normalized.getKind()](normalized, this) : normalized;
+
+  if (!options::proof()) {
+    atom_bb = Rewriter::rewrite(atom_bb);
+  }
+      
   // asserting that the atom is true iff the definition holds
   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
   storeBBAtom(node, atom_bb);
@@ -136,10 +146,19 @@ void TLazyBitblaster::bbAtom(TNode node) {
 }
 
 void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
-  // no need to store the definition for the lazy bit-blaster
+  // No need to store the definition for the lazy bit-blaster (unless proofs are enabled).
+  if( d_bvp != NULL ){
+    d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
+  }
   d_bbAtoms.insert(atom); 
 }
 
+void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
+  if( d_bvp ){ d_bvp->registerTermBB(node.toExpr()); }
+  d_termCache.insert(std::make_pair(node, bits));
+}
+
+
 bool TLazyBitblaster::hasBBAtom(TNode atom) const {
   return d_bbAtoms.find(atom) != d_bbAtoms.end(); 
 }
@@ -483,6 +502,12 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   }
 }
 
+void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
+  d_bvp = bvp;
+  d_satSolver->setProofLog( bvp );
+  bvp->initCnfProof(d_cnfStream, d_nullContext);
+}
+
 void TLazyBitblaster::clearSolver() {
   Assert (d_ctx->getLevel() == 0);
   delete d_satSolver;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4acd1b847..8f7e975cd 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -30,6 +30,8 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "proof/theory_proof.h"
+#include "proof/proof_manager.h"
 #include "theory/valuation.h"
 
 using namespace CVC4::context;
@@ -363,7 +365,6 @@ void TheoryBV::checkForLemma(TNode fact) {
   }
 }
 
-
 void TheoryBV::check(Effort e)
 {
   if (done() && !fullEffort(e)) {
@@ -706,6 +707,7 @@ Node TheoryBV::explain(TNode node) {
   // return the explanation
   Node explanation = utils::mkAnd(assumptions);
   Debug("bitvector::explain") << "TheoryBV::explain(" << node << ") => " << explanation << std::endl;
+  Debug("bitvector::explain") << "TheoryBV::explain done. \n"; 
   return explanation;
 }
 
@@ -796,6 +798,16 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
   return changed;
 }
 
+void TheoryBV::setProofLog( BitVectorProof * bvp ) {
+  if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
+    d_eagerSolver->setProofLog( bvp );
+  }else{
+    for( unsigned i=0; i< d_subtheories.size(); i++ ){
+      d_subtheories[i]->setProofLog( bvp );
+    }
+  }
+}
+
 void TheoryBV::setConflict(Node conflict) {
   if (options::bvAbstraction()) {
     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index e7e4d464f..27138abfc 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -87,7 +87,10 @@ public:
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
   void presolve();
-  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
+
+  bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
+  
+  void setProofLog( BitVectorProof * bvp );
 
 private:
 
@@ -209,11 +212,10 @@ private:
 
   void sendConflict();
 
-  void lemma(TNode node) { d_out->lemma(node); d_lemmasAdded = true; }
+  void lemma(TNode node) { d_out->lemma(node, RULE_CONFLICT); d_lemmasAdded = true; }
 
   void checkForLemma(TNode node); 
 
- 
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
   friend class EagerBitblaster;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 676df5dde..185985b3b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -276,7 +276,8 @@ bool RewriteRule<ReflexivityEq>::applies(TNode node) {
 template<> inline
 Node RewriteRule<ReflexivityEq>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
-  return node[1].eqNode(node[0]);
+  Node res = node[1].eqNode(node[0]);
+  return res;
 }
 
 }
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index cd173a6dd..d5d6c39dd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -325,7 +325,8 @@ Node RewriteRule<XnorEliminate>::apply(TNode node) {
   TNode a = node[0];
   TNode b = node[1]; 
   Node xorNode = utils::mkNode(kind::BITVECTOR_XOR, a, b);
-  return utils::mkNode(kind::BITVECTOR_NOT, xorNode); 
+  Node result = utils::mkNode(kind::BITVECTOR_NOT, xorNode);
+  return result;
 }
 
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 3bf390ded..4d3b676c9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -379,8 +379,8 @@ Node RewriteRule<XorZero>::apply(TNode node) {
       children.push_back(node[i]); 
     }
   }
-
-  return utils::mkNode(kind::BITVECTOR_XOR, children); 
+  Node res = utils::mkNode(kind::BITVECTOR_XOR, children); 
+  return res;
 }
 
 
@@ -488,7 +488,7 @@ bool RewriteRule<NotIdemp>::applies(TNode node) {
 
 template<> inline
 Node RewriteRule<NotIdemp>::apply(TNode node) {
-  Debug("bv-rewrite") << "RewriteRule<XorIdemp>(" << node << ")" << std::endl;
+  Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl;
   return node[0][0];
 }
 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index ba8074fbb..993be309b 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -51,11 +51,11 @@ inline unsigned getSize(TNode node) {
   return node.getType().getBitVectorSize();
 }
 
-// this seems to behave strangely
-inline const Integer& getBit(TNode node, unsigned i) {
-  Assert (0); 
-  Assert (node.getKind() == kind::CONST_BITVECTOR);
-  return node.getConst<BitVector>().extract(i, i).getValue();
+inline const bool getBit(TNode node, unsigned i) {
+  Assert (i < utils::getSize(node) && 
+          node.getKind() == kind::CONST_BITVECTOR);
+  Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
+  return (bit == 1u); 
 }
 
 inline Node mkTrue() {
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 2491aef3a..d5c12457a 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -22,6 +22,7 @@
 #include "base/cvc4_assert.h"
 #include "smt/logic_exception.h"
 #include "theory/interrupted.h"
+#include "proof/proof_manager.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
@@ -99,8 +100,10 @@ public:
    * assigned false), or else a literal by itself (in the case of a
    * unit conflict) which is assigned TRUE (and T-conflicting) in the
    * current assignment.
+   * @param pf - a proof of the conflict. This is only non-null if proofs
+   * are enabled. 
    */
-  virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
+  virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Propagate a theory literal.
@@ -115,16 +118,31 @@ public:
    * been detected.  (This requests a split.)
    *
    * @param n - a theory lemma valid at decision level 0
+   * @param rule - the proof rule for this lemma
    * @param removable - whether the lemma can be removed at any point
    * @param preprocess - whether to apply more aggressive preprocessing
    * @param sendAtoms - whether to ensure atoms are sent to the theory
    * @return the "status" of the lemma, including user level at which
    * the lemma resides; the lemma will be removed when this user level pops
    */
-  virtual LemmaStatus lemma(TNode n, bool removable = false,
-                            bool preprocess = false, bool sendAtoms = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0;
+  virtual LemmaStatus lemma(TNode n, ProofRule rule,
+                            bool removable = false,
+                            bool preprocess = false,
+                            bool sendAtoms = false)
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
+
+  /**
+   * Variant of the lemma function that does not require providing a proof rule.
+   */
+  virtual LemmaStatus lemma(TNode n, 
+                            bool removable = false,
+                            bool preprocess = false,
+                            bool sendAtoms = false)
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+    return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms);
+  }
 
+  
   /**
    * Request a split on a new theory atom.  This is equivalent to
    * calling lemma({OR n (NOT n)}).
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index c98429dd2..d89724cbd 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -40,7 +40,9 @@ static CVC4_THREADLOCAL(std::hash_set<Node, NodeHashFunction>*) s_rewriteStack =
 
 class RewriterInitializer {
   static RewriterInitializer s_rewriterInitializer;
-  RewriterInitializer() { Rewriter::init(); }
+  RewriterInitializer() {
+    Rewriter::init();
+  }
   ~RewriterInitializer() { Rewriter::shutdown(); }
 };/* class RewriterInitializer */
 
@@ -190,7 +192,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
       // Incorporate the children if necessary
       if (rewriteStackTop.node.getNumChildren() > 0) {
-        rewriteStackTop.node = rewriteStackTop.builder;
+        Node rewritten = rewriteStackTop.builder;
+        rewriteStackTop.node = rewritten;
         rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node);
       }
 
@@ -208,7 +211,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
           Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end());
           s_rewriteStack->insert(response.node);
 #endif
-          rewriteStackTop.node = rewriteTo(newTheoryId, response.node);
+          Node rewritten = rewriteTo(newTheoryId, response.node);
+          rewriteStackTop.node = rewritten;
 #ifdef CVC4_ASSERTIONS
           s_rewriteStack->erase(response.node);
 #endif
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9e946f8d7..45c9b1936 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -50,8 +50,9 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
 
 Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
                OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
-               SmtGlobals* globals) throw()
+               SmtGlobals* globals, std::string name) throw()
     : d_id(id)
+    , d_instanceName(name)
     , d_satContext(satContext)
     , d_userContext(userContext)
     , d_logicInfo(logicInfo)
@@ -60,12 +61,12 @@ Theory::Theory(TheoryId id, context::Context* satContext, context::UserContext*
     , d_sharedTermsIndex(satContext, 0)
     , d_careGraph(NULL)
     , d_quantEngine(NULL)
-    , d_checkTime(statName(id, "checkTime"))
-    , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
+    , d_checkTime(getFullInstanceName() + "::checkTime")
+    , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime")
     , d_sharedTerms(satContext)
     , d_out(&out)
     , d_valuation(valuation)
-    , d_proofEnabled(false)
+    , d_proofsEnabled(false)
     , d_globals(globals)
 {
   smtStatisticsRegistry()->registerStat(&d_checkTime);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index f7d9ee6a0..2c3c66d8b 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -149,6 +149,11 @@ private:
    */
   TheoryId d_id;
 
+  /** Name of this theory instance. Along with the TheoryId this should provide
+   * an unique string identifier for each instance of a Theory class. We need
+   * this to ensure unique statistics names over multiple theory instances. */
+  std::string d_instanceName;
+  
   /**
    * The SAT search context for the Theory.
    */
@@ -204,12 +209,6 @@ protected:
   /** time spent in theory combination */
   TimerStat d_computeCareGraphTime;
 
-  static std::string statName(TheoryId id, const char* statName) {
-    std::stringstream ss;
-    ss << "theory<" << id << ">::" << statName;
-    return ss.str();
-  }
-
   /**
    * The only method to add suff to the care graph.
    */
@@ -247,7 +246,7 @@ protected:
    */
   Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext,
          OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
-         SmtGlobals* globals) throw();
+         SmtGlobals* globals, std::string name = "") throw(); // taking : No default.
 
   /**
    * This is called at shutdown time by the TheoryEngine, just before
@@ -272,6 +271,12 @@ protected:
   Valuation d_valuation;
 
   /**
+   * Whether proofs are enabled
+   *
+   */
+  bool d_proofsEnabled;
+  
+  /**
    * Returns the next assertion in the assertFact() queue.
    *
    * @return the next assertion in the assertFact() queue
@@ -290,12 +295,6 @@ protected:
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
-  /**
-   * Whether proofs are enabled
-   *
-   */
-  bool d_proofEnabled;
-
   SmtGlobals* d_globals;
 
 public:
@@ -416,6 +415,13 @@ public:
     return d_id;
   }
 
+  std::string getFullInstanceName() const {
+    std::stringstream ss;
+    ss << "theory<" << d_id << ">" << d_instanceName;
+    return ss.str();
+  }
+
+  
   /**
    * Get the SAT context associated to this Theory.
    */
@@ -855,7 +861,11 @@ public:
    */
   virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
 
-
+  /**
+   * Turn on proof-production mode.
+   */
+  void produceProofs() { d_proofsEnabled = true; }
+  
   /** Returns a pointer to the globals copy the theory is using. */
   SmtGlobals* globals() { return d_globals; }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 25eac2ed4..be2a89dbc 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -27,7 +27,7 @@
 #include "options/options.h"
 #include "options/quantifiers_options.h"
 #include "proof/proof_manager.h"
-#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
 #include "smt/logic_exception.h"
 #include "smt_util/ite_removal.h"
 #include "smt_util/lemma_output_channel.h"
@@ -54,8 +54,6 @@ using namespace CVC4::theory;
 namespace CVC4 {
 
 void TheoryEngine::finishInit() {
-  PROOF (ProofManager::initTheoryProof(); );
-
   // initialize the quantifiers engine
   d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
 
@@ -157,6 +155,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
+  PROOF (ProofManager::currentPM()->initTheoryProofEngine(d_globals); );
+
   d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
 
   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
@@ -377,7 +377,7 @@ void TheoryEngine::check(Theory::Effort effort) {
           printAssertions("theory::assertions::fulleffort");
         }
       }
-        
+
       // Note that we've discharged all the facts
       d_factsAsserted = false;
 
@@ -414,7 +414,7 @@ void TheoryEngine::check(Theory::Effort effort) {
         // must build model at this point
         d_curr_model_builder->buildModel(d_curr_model, true);
       }
-	  Trace("theory::assertions-model") << endl;
+    Trace("theory::assertions-model") << endl;
       if (Trace.isOn("theory::assertions-model")) {
         printAssertions("theory::assertions-model");
       }
@@ -486,7 +486,7 @@ void TheoryEngine::combineTheories() {
 
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-    lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory);
+    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, 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) {
@@ -1371,7 +1371,12 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
   }
 }
 
-theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
+theory::LemmaStatus TheoryEngine::lemma(TNode node,
+                                        ProofRule rule,
+                                        bool negated,
+                                        bool removable,
+                                        bool preprocess,
+                                        theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
   // spendResource();
 
@@ -1420,10 +1425,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
   }
 
   // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, RULE_INVALID, node);
+  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
     additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
-    d_propEngine->assertLemma(additionalLemmas[i], false, removable, RULE_INVALID, node);
+    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1467,11 +1472,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     Node fullConflict = mkExplanation(explanationVector);
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
-    lemma(fullConflict, true, true, false, THEORY_LAST);
+    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
   } else {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
-    lemma(conflict, true, true, false, THEORY_LAST);
+    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
   }
 }
 
@@ -1483,27 +1488,27 @@ void TheoryEngine::staticInitializeBVOptions(const std::vector<Node>& assertions
     if (options::produceModels())
       throw ModalException("Slicer does not currently support model generation. Use --bv-eq-slicer=off");
     useSlicer = true;
-    
+
   } else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_OFF) {
     return;
-    
+
   } else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_AUTO) {
     if (options::incrementalSolving() ||
         options::produceModels())
       return;
 
-    useSlicer = true; 
+    useSlicer = true;
     bv::utils::TNodeBoolMap cache;
     for (unsigned i = 0; i < assertions.size(); ++i) {
-      useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache); 
+      useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache);
     }
   }
-  
+
   if (useSlicer) {
-    bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; 
+    bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
     bv_theory->enableCoreTheorySlicer();
   }
-  
+
 }
 
 void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
@@ -1511,12 +1516,12 @@ void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<N
 }
 
 bool  TheoryEngine::ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
-  bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; 
-  return bv_theory->applyAbstraction(assertions, new_assertions); 
+  bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
+  return bv_theory->applyAbstraction(assertions, new_assertions);
 }
 
 void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) {
-  bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; 
+  bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
   bv_theory->mkAckermanizationAsssertions(assertions);
 }
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7cb15ca97..0bf00c079 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -269,8 +269,9 @@ class TheoryEngine {
       }
     }
 
-    void conflict(TNode conflictNode) 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);
@@ -283,18 +284,23 @@ class TheoryEngine {
       return d_engine->propagate(literal, d_theory);
     }
 
-    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false, bool sendAtoms = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) {
+    theory::LemmaStatus lemma(TNode lemma,
+                              ProofRule rule,
+                              bool removable = false,
+                              bool preprocess = false,
+                              bool sendAtoms = false)
+      throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, false, removable, preprocess, sendAtoms ? d_theory : theory::THEORY_LAST);
+      return d_engine->lemma(lemma, rule, false, removable, preprocess, sendAtoms ? d_theory: theory::THEORY_LAST);
     }
 
     theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, false, removable, false, d_theory);
+      return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
     }
 
     void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
@@ -304,7 +310,7 @@ class TheoryEngine {
                                         "A boolean variable asserted to be true to force a restart");
       Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl;
       ++ d_statistics.restartDemands;
-      lemma(restartVar, true);
+      lemma(restartVar, RULE_INVALID, true);
     }
 
     void requirePhase(TNode n, bool phase)
@@ -436,7 +442,12 @@ class TheoryEngine {
    * @param removable can the lemma be remove (restrictions apply)
    * @param needAtoms if not THEORY_LAST, then
    */
-  theory::LemmaStatus lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo);
+  theory::LemmaStatus lemma(TNode node,
+                            ProofRule rule,
+                            bool negated,
+                            bool removable,
+                            bool preprocess,
+                            theory::TheoryId atomsTo);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index f0b616d62..6247833f8 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -71,7 +71,7 @@ public:
 
   void safePoint(uint64_t ammount)  throw(Interrupted, AssertionException) {}
 
-  void conflict(TNode n)
+  void conflict(TNode n, Proof* pf = NULL)
     throw(AssertionException, UnsafeInterruptException) {
     push(CONFLICT, n);
   }
@@ -87,7 +87,10 @@ public:
     push(PROPAGATE_AS_DECISION, n);
   }
 
-  LemmaStatus lemma(TNode n, bool removable, bool preprocess, bool sendAtoms) throw(AssertionException, UnsafeInterruptException) {
+  LemmaStatus lemma(TNode n, ProofRule rule,
+                    bool removable = false,
+                    bool preprocess = false,
+                    bool sendAtoms = false) throw(AssertionException, UnsafeInterruptException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 828d53144..8df323992 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -314,10 +314,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
       // How many children are not constants yet
       d_subtermsToEvaluate[result] = t.getNumChildren();
       for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
-	if (isConstant(getNodeId(t[i]))) {
-	  Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl;
-	  subtermEvaluates(result);
-	}
+        if (isConstant(getNodeId(t[i]))) {
+          Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl;
+          subtermEvaluates(result);
+        }
       }
     }
   } else {
@@ -335,7 +335,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
   } else if (d_constantsAreTriggers && d_isConstant[result]) {
     // Non-Boolean constants are trigger terms for all tags
     EqualityNodeId tId = getNodeId(t);
-    // Setup the new set 
+    // Setup the new set
     Theory::Set newSetTags = 0;
     EqualityNodeId newSetTriggers[THEORY_LAST];
     unsigned newSetTriggersSize = THEORY_LAST;
@@ -629,12 +629,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
         const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
         // If it's interpreted and we can interpret
-	if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) {
-	  // Get the actual term id
-	  TNode term = d_nodes[funId];
-	  subtermEvaluates(getNodeId(term));
-	}
-	// Check if there is an application with find arguments
+  if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) {
+    // Get the actual term id
+    TNode term = d_nodes[funId];
+    subtermEvaluates(getNodeId(term));
+  }
+  // Check if there is an application with find arguments
         EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
         EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
         FunctionApplication funNormalized(fun.type, aNormalized, bNormalized);
@@ -972,7 +972,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
   // If the nodes are the same, we're done
   if (t1Id == t2Id){
     if( eqp ) {
-      eqp->d_node = d_nodes[t1Id];
+      eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
     }
     return;
   }
@@ -1029,6 +1029,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
 
             Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
+            Debug("equality") << d_name << "                     in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
 
             EqProof * eqpc = NULL;
             //make child proof if a proof is being constructed
@@ -1051,6 +1052,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
                 eqpc->d_children.push_back( eqpc2 );
+                Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl;
+                if( d_nodes[currentNode].getKind()==kind::EQUAL ){
+                  //leave node null for now
+                  eqpc->d_node = Node::null();
+                }else{
+                  Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl;
+                  if(d_nodes[f1.a].getKind() == kind::APPLY_UF ||
+                     d_nodes[f1.a].getKind() == kind::SELECT ||
+                     d_nodes[f1.a].getKind() == kind::STORE) {
+                    eqpc->d_node = d_nodes[f1.a];
+                  } else {
+                    eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]);
+                  }
+                }
               }
               Debug("equality") << pop;
               break;
@@ -1103,13 +1118,14 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               // Construct the equality
               Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
               if( eqpc ){
-                if( reasonType==MERGED_THROUGH_EQUALITY ){
+                if(reasonType == MERGED_THROUGH_EQUALITY) {
                   eqpc->d_node = d_equalityEdges[currentEdge].getReason();
-                }else{
-                  //theory-specific proof rule : TODO
-                  eqpc->d_id = reasonType;
-                  //eqpc->d_node = d_equalityEdges[currentEdge].getNodeId();
+                } else {
+                  // theory-specific proof rule
+                  eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]);
+                  Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl;
                 }
+                eqpc->d_id = reasonType;
               }
               equalities.push_back(d_equalityEdges[currentEdge].getReason());
               break;
@@ -1120,13 +1136,32 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             currentEdge = bfsQueue[currentIndex].edgeId;
             currentIndex = bfsQueue[currentIndex].previousIndex;
 
+            //---from Morgan---
+            if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
+              if(eqpc->d_node.isNull()) {
+                Assert(eqpc->d_children.size() == 1);
+                EqProof *p = eqpc;
+                eqpc = p->d_children[0];
+                delete p;
+              } else {
+                Assert(eqpc->d_children.empty());
+              }
+            }
+            //---end from Morgan---
+
             eqp_trans.push_back( eqpc );
 
           } while (currentEdge != null_id);
 
-          if( eqp ){
-            eqp->d_id = MERGED_THROUGH_TRANS;
-            eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
+          if(eqp) {
+            if(eqp_trans.size() == 1) {
+              *eqp = *eqp_trans[0];
+              delete eqp_trans[0];
+            } else {
+              eqp->d_id = MERGED_THROUGH_TRANS;
+              eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
+              eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
+            }
           }
 
           // Done
@@ -2057,8 +2092,7 @@ bool EqClassIterator::isFinished() const {
   return d_current == null_id;
 }
 
-
-void EqProof::debug_print( const char * c, unsigned tb ){
+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() ){
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 87074aebc..9cfa16adf 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -879,8 +879,8 @@ public:
   MergeReasonType d_id;
   Node d_node;
   std::vector< EqProof * > d_children;
-  void debug_print( const char * c, unsigned tb = 0 );
-};
+  void debug_print( const char * c, unsigned tb = 0 ) const;
+};/* class EqProof */
 
 } // Namespace eq
 } // Namespace theory
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index f0b50b778..888fa140f 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -21,6 +21,9 @@ typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRul
 operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature"
 typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule
 
+parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application"
+typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule
+
 operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
 typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule
 
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index d5e18ed14..4f7a2667c 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -167,7 +167,8 @@ void SymmetryBreaker::Template::reset() {
   d_reps.clear();
 }
 
-SymmetryBreaker::SymmetryBreaker(context::Context* context) :
+SymmetryBreaker::SymmetryBreaker(context::Context* context,
+                                 std::string name) :
   ContextNotifyObj(context),
   d_assertionsToRerun(context),
   d_rerunningAssertions(false),
@@ -178,7 +179,10 @@ SymmetryBreaker::SymmetryBreaker(context::Context* context) :
   d_template(),
   d_normalizationCache(),
   d_termEqs(),
-  d_termEqsOnly() {
+  d_termEqsOnly(),
+  d_name(name),
+  d_stats(d_name)
+{
 }
 
 class SBGuard {
@@ -461,7 +465,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
   Debug("ufsymm") << "UFSYMM =====================================================" << endl
                   << "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
   if(!d_permutations.empty()) {
-    { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer);
+    { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer);
       // normalize d_phi
 
       for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
@@ -476,12 +480,12 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
     for(Permutations::iterator i = d_permutations.begin();
         i != d_permutations.end();
         ++i) {
-      ++d_permutationSetsConsidered;
+      ++(d_stats.d_permutationSetsConsidered);
       const Permutation& p = *i;
       Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl;
       size_t n = p.size() - 1;
       if(invariantByPermutations(p)) {
-        ++d_permutationSetsInvariant;
+        ++(d_stats.d_permutationSetsInvariant);
         selectTerms(p);
         set<Node> cts;
         while(!d_terms.empty() && cts.size() <= n) {
@@ -539,11 +543,11 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
             Node d;
             if(disj.getNumChildren() > 1) {
               d = disj;
-              ++d_clauses;
+              ++(d_stats.d_clauses);
             } else {
               d = disj[0];
               disj.clear();
-              ++d_units;
+              ++(d_stats.d_units);
             }
             if(Debug.isOn("ufsymm")) {
               Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl;
@@ -569,7 +573,7 @@ void SymmetryBreaker::guessPermutations() {
 }
 
 bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
-  TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer);
+  TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer);
 
   // use d_phi
   Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl;
@@ -681,7 +685,7 @@ static bool isSubset(const T1& s, const T2& t) {
 }
 
 void SymmetryBreaker::selectTerms(const Permutation& p) {
-  TimerStat::CodeTimer codeTimer(d_selectTermsTimer);
+  TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer);
 
   // use d_phi, put into d_terms
   Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl;
@@ -733,6 +737,35 @@ void SymmetryBreaker::selectTerms(const Permutation& p) {
   }
 }
 
+SymmetryBreaker::Statistics::Statistics(std::string name)
+  : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
+  , d_units(name + "theory::uf::symmetry_breaker::units", 0)
+  , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
+  , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
+  , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
+  , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
+  , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
+{
+  smtStatisticsRegistry()->registerStat(&d_clauses);
+  smtStatisticsRegistry()->registerStat(&d_units);
+  smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
+  smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
+  smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
+  smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
+  smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
+}
+
+SymmetryBreaker::Statistics::~Statistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_clauses);
+  smtStatisticsRegistry()->unregisterStat(&d_units);
+  smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
+  smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
+  smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
+  smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
+}
+
 SymmetryBreaker::Terms::iterator
 SymmetryBreaker::selectMostPromisingTerm(Terms& terms) {
   // use d_phi
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 763ced650..5523c1c0d 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -128,35 +128,30 @@ private:
   Node normInternal(TNode phi, size_t level);
   Node norm(TNode n);
 
+  std::string d_name;
+  
   // === STATISTICS ===
   /** number of new clauses that come from the SymmetryBreaker */
-  KEEP_STATISTIC(IntStat,
-                 d_clauses,
-                 "theory::uf::symmetry_breaker::clauses", 0);
-  /** number of new clauses that come from the SymmetryBreaker */
-  KEEP_STATISTIC(IntStat,
-                 d_units,
-                 "theory::uf::symmetry_breaker::units", 0);
-  /** number of potential permutation sets we found */
-  KEEP_STATISTIC(IntStat,
-                 d_permutationSetsConsidered,
-                 "theory::uf::symmetry_breaker::permutationSetsConsidered", 0);
-  /** number of invariant permutation sets we found */
-  KEEP_STATISTIC(IntStat,
-                 d_permutationSetsInvariant,
-                 "theory::uf::symmetry_breaker::permutationSetsInvariant", 0);
-  /** time spent in invariantByPermutations() */
-  KEEP_STATISTIC(TimerStat,
-                 d_invariantByPermutationsTimer,
-                 "theory::uf::symmetry_breaker::timers::invariantByPermutations");
-  /** time spent in selectTerms() */
-  KEEP_STATISTIC(TimerStat,
-                 d_selectTermsTimer,
-                 "theory::uf::symmetry_breaker::timers::selectTerms");
-  /** time spent in initial round of normalization */
-  KEEP_STATISTIC(TimerStat,
-                 d_initNormalizationTimer,
-                 "theory::uf::symmetry_breaker::timers::initNormalization");
+  struct Statistics {
+    /** number of new clauses that come from the SymmetryBreaker */
+    IntStat d_clauses;
+    IntStat d_units;
+    /** number of potential permutation sets we found */
+    IntStat d_permutationSetsConsidered;
+    /** number of invariant permutation sets we found */
+    IntStat d_permutationSetsInvariant;
+    /** time spent in invariantByPermutations() */
+    TimerStat d_invariantByPermutationsTimer;
+    /** time spent in selectTerms() */
+    TimerStat d_selectTermsTimer;
+    /** time spent in initial round of normalization */
+    TimerStat d_initNormalizationTimer;
+
+    Statistics(std::string name);
+    ~Statistics();
+  };
+
+  Statistics d_stats;
 
 protected:
 
@@ -167,7 +162,7 @@ protected:
 
 public:
 
-  SymmetryBreaker(context::Context* context);
+  SymmetryBreaker(context::Context* context, std::string name = "");
   ~SymmetryBreaker() throw() {}
   void assertFormula(TNode phi);
   void apply(std::vector<Node>& newClauses);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e21b7ef7d..93a920f82 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -20,30 +20,34 @@
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
+#include "proof/uf_proof.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
 TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
                    OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals),
+                   const LogicInfo& logicInfo, SmtGlobals* globals, std::string name)
+    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name),
       d_notify(*this),
       /* The strong theory solver can be notified by EqualityEngine::init(),
        * so make sure it's initialized first. */
       d_thss(NULL),
-      d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
+      d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true),
       d_conflict(c, false),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_functionsTerms(c),
-      d_symb(u)
+      d_symb(u, name)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
@@ -204,27 +208,29 @@ Node TheoryUF::getNextDecisionRequest(){
   }
 }
 
-void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
+void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
-  eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp);
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
   }
-  //for now, just print debug
-  //TODO : send the proof outwards : d_out->conflict( lem, eqp );
-  if( eqp ){
-    eqp->debug_print("uf-pf");
+  if( pf ){
+    Debug("uf-pf") << std::endl;
+    pf->debug_print("uf-pf");
   }
 }
 
 Node TheoryUF::explain(TNode literal) {
+  return explain(literal, NULL);
+}
+
+Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
   Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
-  explain(literal, assumptions);
+  explain(literal, assumptions, pf);
   return mkAnd(assumptions);
 }
 
@@ -508,13 +514,14 @@ void TheoryUF::computeCareGraph() {
 }/* TheoryUF::computeCareGraph() */
 
 void TheoryUF::conflict(TNode a, TNode b) {
-  //TODO: create EqProof at this level if d_proofEnabled = true
+  eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
   if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b));
+    d_conflictNode = explain(a.iffNode(b),pf);
   } else {
-    d_conflictNode = explain(a.eqNode(b));
+    d_conflictNode = explain(a.eqNode(b),pf);
   }
-  d_out->conflict(d_conflictNode);
+  ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
+  d_out->conflict(d_conflictNode, puf);
   d_conflict = true;
 }
 
@@ -541,3 +548,8 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
     d_thss->assertDisequal(t1, t2, reason);
   }
 }
+
+
+} /* namespace CVC4::theory::uf */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index aff78f53d..bd0016be7 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -128,9 +128,15 @@ private:
 
   /**
    * Explain why this literal is true by adding assumptions
+   * with proof (if "pf" is non-NULL).
    */
-  void explain(TNode literal, std::vector<TNode>& assumptions);
+  void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf);
 
+  /**
+   * Explain a literal, with proof (if "pf" is non-NULL).
+   */
+  Node explain(TNode literal, eq::EqProof* pf);
+  
   /** Literals to propagate */
   context::CDList<Node> d_literalsToPropagate;
 
@@ -163,7 +169,7 @@ public:
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
   TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
            Valuation valuation, const LogicInfo& logicInfo,
-           SmtGlobals* globals);
+           SmtGlobals* globals, std::string name = "");
 
   ~TheoryUF();
 
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 6faab8517..05b95e9e1 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -107,6 +107,14 @@ public:
   }
 };/* class CardinalityConstraintTypeRule */
 
+class PartialTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    return n.getOperator().getType().getRangeType();
+  }
+};/* class PartialTypeRule */
+
 class CardinalityValueTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)