Merge pull request #82 from CVC4/master_for_merge

Squash-merge from the proof branch

16 files changed, 527 insertions, 128 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 55f013f8c..16412c05b 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -44,16 +44,16 @@ Info::~Info() {
   in_stores->deleteSelf();
 }
 
-ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b)
+ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix)
     : ct(c), bck(b), info_map(),
-      d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
-      d_avgIndexListLength("theory::arrays::avgIndexListLength"),
-      d_avgStoresListLength("theory::arrays::avgStoresListLength"),
-      d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
-      d_listsCount("theory::arrays::listsCount",0),
-      d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
-      d_maxList("theory::arrays::maxList",0),
-      d_tableSize("theory::arrays::infoTableSize", info_map) {
+      d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"),
+      d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"),
+      d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"),
+      d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"),
+      d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0),
+      d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0),
+      d_maxList(statisticsPrefix + "theory::arrays::maxList",0),
+      d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) {
   emptyList = new(true) CTNodeList(ct);
   emptyInfo = new Info(ct, bck);
   smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
@@ -208,7 +208,7 @@ void ArrayInfo::setNonLinear(const TNode a) {
   } else {
     (*it).second->isNonLinear = true;
   }
-  
+
 }
 
 void ArrayInfo::setRIntro1Applied(const TNode a) {
@@ -222,7 +222,7 @@ void ArrayInfo::setRIntro1Applied(const TNode a) {
   } else {
     (*it).second->rIntro1Applied = true;
   }
-  
+
 }
 
 void ArrayInfo::setModelRep(const TNode a, const TNode b) {
@@ -236,7 +236,7 @@ void ArrayInfo::setModelRep(const TNode a, const TNode b) {
   } else {
     (*it).second->modelRep = b;
   }
-  
+
 }
 
 void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 319864c34..04b9cffb1 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -155,7 +155,8 @@ public:
   currentStatisticsRegistry()->registerStat(&d_maxList);
   currentStatisticsRegistry()->registerStat(&d_tableSize);
   }*/
-  ArrayInfo(context::Context* c, Backtracker<TNode>* b);
+
+  ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix = "");
 
   ~ArrayInfo();
 
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index d5f313ca1..be16d684d 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -54,6 +54,11 @@ typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
 typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule
 
+operator PARTIAL_SELECT_0 0:2 "partial array select, for internal use only"
+operator PARTIAL_SELECT_1 0:2 "partial array select, for internal use only"
+typerule PARTIAL_SELECT_0 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule
+typerule PARTIAL_SELECT_1 ::CVC4::theory::arrays::ArrayPartialSelectTypeRule
+
 # store operations that are ordered (by index) over a store-all are constant
 construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 631785437..fcde18b66 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,13 +21,14 @@
 #include "expr/kind.h"
 #include "options/arrays_options.h"
 #include "options/smt_options.h"
+#include "proof/array_proof.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
 #include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.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;
@@ -78,7 +79,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
       d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true),
       d_conflict(c, false),
       d_backtracker(c),
-      d_infoMap(c, &d_backtracker),
+      d_infoMap(c, &d_backtracker, name),
       d_mergeQueue(c),
       d_mergeInProgress(false),
       d_RowQueue(c),
@@ -383,21 +384,27 @@ bool TheoryArrays::propagate(TNode literal)
 }/* TheoryArrays::propagate(TNode) */
 
 
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
   //eq::EqProof * eqp = new eq::EqProof;
-  eq::EqProof * eqp = NULL;
+  // eq::EqProof * eqp = 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, proof);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof);
   }
-  if( eqp ){
-    Debug("array-pf") << " Proof is : " << std::endl;
-    eqp->debug_print("array-pf");
+  if(proof){
+    Debug("pf::array") << " Proof is : " << std::endl;
+    proof->debug_print("pf::array");
   }
+
+  Debug("pf::array") << "Array: explain( " << literal << " ):" << std::endl << "\t";
+  for (unsigned i = 0; i < assumptions.size(); ++i) {
+    Debug("pf::array") << assumptions[i] << " ";
+  }
+  Debug("pf::array") << std::endl;
 }
 
 TNode TheoryArrays::weakEquivGetRep(TNode node) {
@@ -597,7 +604,7 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
         }
       }
     }
-  }  
+  }
 }
 
 /**
@@ -787,6 +794,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     else {
       d_equalityEngine.addTerm(node);
     }
+
     break;
   }
   // Invariant: preregistered terms are exactly the terms in the equality engine
@@ -807,12 +815,16 @@ void TheoryArrays::propagate(Effort e)
 }
 
 
-Node TheoryArrays::explain(TNode literal)
+Node TheoryArrays::explain(TNode literal) {
+  return explain(literal, NULL);
+}
+
+Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
 {
   ++d_numExplain;
   Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
-  explain(literal, assumptions);
+  explain(literal, assumptions, proof);
   return mkAnd(assumptions);
 }
 
@@ -1230,7 +1242,11 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
       makeEqual = false;
     }
   }
+
+  Debug("pf::array") << "Pregistering a Skolem" << std::endl;
   preRegisterTermInternal(skolem);
+  Debug("pf::array") << "Pregistering a Skolem DONE" << std::endl;
+
   if (makeEqual) {
     Node d = skolem.eqNode(ref);
     Debug("arrays-model-based") << "Asserting skolem equality " << d << endl;
@@ -1239,6 +1255,8 @@ Node TheoryArrays::getSkolem(TNode ref, const string& name, const TypeNode& type
     d_skolemAssertions.push_back(d);
     d_skolemIndex = d_skolemIndex + 1;
   }
+
+  Debug("pf::array") << "getSkolem DONE" << std::endl;
   return skolem;
 }
 
@@ -1293,28 +1311,76 @@ void TheoryArrays::check(Effort e) {
 
           // Apply ArrDiseq Rule if diseq is between arrays
           if(fact[0][0].getType().isArray() && !d_conflict) {
+            if (d_conflict) { Debug("pf::array") << "Entering the skolemization branch" << std::endl; }
+
             NodeManager* nm = NodeManager::currentNM();
             TypeNode indexType = fact[0][0].getType()[0];
-            TNode k = getSkolem(fact,"array_ext_index", indexType, "an extensional lemma index variable from the theory of arrays", false);
+
+            TNode k;
+            // k is the skolem for this disequality.
+            if (!d_proofsEnabled) {
+              Debug("pf::array") << "Check: kind::NOT: array theory making a skolem" << std::endl;
+
+              // If not in replay mode, generate a fresh skolem variable
+              k = getSkolem(fact,
+                            "array_ext_index",
+                            indexType,
+                            "an extensional lemma index variable from the theory of arrays",
+                            false);
+
+              // Register this skolem for the proof replay phase
+              PROOF(ProofManager::getSkolemizationManager()->registerSkolem(fact, k));
+            } else {
+              if (!ProofManager::getSkolemizationManager()->hasSkolem(fact)) {
+                // In the solution pass we didn't need this skolem. Therefore, we don't need it
+                // in this reply pass, either.
+                break;
+              }
+
+              // Reuse the same skolem as in the solution pass
+              k = ProofManager::getSkolemizationManager()->getSkolem(fact);
+              Debug("pf::array") << "Skolem = " << k << std::endl;
+            }
 
             Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
             Node eq = ak.eqNode(bk);
             Node lemma = fact[0].orNode(eq.notNode());
+
+            // In solve mode we don't care if ak and bk are registered. If they aren't, they'll be registered
+            // when we output the lemma. However, in replay need the lemma to be propagated, and so we
+            // preregister manually.
+            if (d_proofsEnabled) {
+              if (!d_equalityEngine.hasTerm(ak)) { preRegisterTermInternal(ak); }
+              if (!d_equalityEngine.hasTerm(bk)) { preRegisterTermInternal(bk); }
+            }
+
             if (options::arraysPropagate() > 0 && d_equalityEngine.hasTerm(ak) && d_equalityEngine.hasTerm(bk)) {
               // Propagate witness disequality - might produce a conflict
               d_permRef.push_back(lemma);
-              d_equalityEngine.assertEquality(eq, false, lemma, eq::MERGED_ARRAYS_EXT);
+              Debug("pf::array") << "Asserting to the equality engine:" << std::endl
+                                 << "\teq = " << eq << std::endl
+                                 << "\treason = " << fact << std::endl;
+
+              d_equalityEngine.assertEquality(eq, false, fact, eq::MERGED_ARRAYS_EXT);
               ++d_numProp;
             }
-            Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
-            d_out->lemma(lemma);
-            ++d_numExt;
+
+            if (!d_proofsEnabled) {
+              // If this is the solution pass, generate the lemma. Otherwise, don't generate it -
+              // as this is the lemma that we're reproving...
+              Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n";
+              d_out->lemma(lemma);
+              ++d_numExt;
+            }
+          } else {
+            Debug("pf::array") << "Check: kind::NOT: array theory NOT making a skolem" << std::endl;
+            d_modelConstraints.push_back(fact);
           }
         }
         break;
-      default:
-        Unreachable();
+    default:
+      Unreachable();
     }
   }
 
@@ -1389,8 +1455,10 @@ void TheoryArrays::check(Effort e) {
           weakEquivBuildCond(r2[0], r[1], conjunctions);
           lemma = mkAnd(conjunctions, true);
           // LSH FIXME: which kind of arrays lemma is this
+          Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n";
           d_out->lemma(lemma, RULE_INVALID, false, false, true);
           d_readTableContext->pop();
+          Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
           return;
         }
       }
@@ -1401,7 +1469,7 @@ void TheoryArrays::check(Effort e) {
 
   if(!options::arraysEagerLemmas() && fullEffort(e) && !d_conflict && !options::arraysWeakEquivalence()) {
     // generate the lemmas on the worklist
-    Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+    Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
     while (d_RowQueue.size() > 0 && !d_conflict) {
       if (dischargeLemmas()) {
         break;
@@ -1865,6 +1933,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 
 void TheoryArrays::propagate(RowLemmaType lem)
 {
+  Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
+                     << options::arraysPropagate() << std::endl;
+
   TNode a = lem.first;
   TNode b = lem.second;
   TNode i = lem.third;
@@ -1919,6 +1990,8 @@ void TheoryArrays::propagate(RowLemmaType lem)
 
 void TheoryArrays::queueRowLemma(RowLemmaType lem)
 {
+  Debug("pf::array") << "Array solver: queue row lemma called" << std::endl;
+
   if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
     return;
   }
@@ -1958,14 +2031,20 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   // Prefer equality between indexes so as not to introduce new read terms
   if (options::arraysEagerIndexSplitting() && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
-    Node i_eq_j = d_valuation.ensureLiteral(i.eqNode(j));
+    Node i_eq_j;
+    if (!d_proofsEnabled) {
+      i_eq_j = d_valuation.ensureLiteral(i.eqNode(j)); // TODO: think about this
+    } else {
+      i_eq_j = i.eqNode(j);
+    }
+
     getOutputChannel().requirePhase(i_eq_j, true);
     d_decisionRequests.push(i_eq_j);
   }
 
   // TODO: maybe add triggers here
 
-  if (options::arraysEagerLemmas() || bothExist) {
+  if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) {
 
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
     Node aj2 = Rewriter::rewrite(aj);
@@ -2137,14 +2216,20 @@ 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));
+    d_conflictNode = explain(a.iffNode(b), proof);
   } else {
-    d_conflictNode = explain(a.eqNode(b));
+    d_conflictNode = explain(a.eqNode(b), proof);
   }
+
   if (!d_inCheckModel) {
-    d_out->conflict(d_conflictNode);
+    if (proof) { proof->debug_print("pf::array"); }
+    ProofArray* proof_array = d_proofsEnabled ? new ProofArray( proof ) : NULL;
+    d_out->conflict(d_conflictNode, proof_array);
   }
+
   d_conflict = true;
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index eba6c000e..2f69c52f9 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,
-               std::string instanceName = "");
+               std::string name = "");
   ~TheoryArrays();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
@@ -183,7 +183,7 @@ class TheoryArrays : public Theory {
   bool propagate(TNode literal);
 
   /** Explain why this literal is true by adding assumptions */
-  void explain(TNode literal, std::vector<TNode>& assumptions);
+  void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof);
 
   /** For debugging only- checks invariants about when things are preregistered*/
   context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
@@ -195,6 +195,7 @@ class TheoryArrays : public Theory {
 
   void preRegisterTerm(TNode n);
   void propagate(Effort e);
+  Node explain(TNode n, eq::EqProof *proof);
   Node explain(TNode n);
 
   /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 70e1c1a5b..a5d0eac69 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -214,6 +214,15 @@ struct ArraysProperties {
   }
 };/* struct ArraysProperties */
 
+
+struct ArrayPartialSelectTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::PARTIAL_SELECT_0 || n.getKind() == kind::PARTIAL_SELECT_1);
+    return nodeManager->integerType();
+  }
+};/* struct ArrayPartialSelectTypeRule */
+
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 77e75091d..ed76dbb80 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -99,7 +99,7 @@ void EagerBitblaster::bbAtom(TNode node) {
   // 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); 
+  AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   storeBBAtom(node, atom_bb);
   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
@@ -108,7 +108,7 @@ void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
   if( d_bvp ){
     d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
   }
-  d_bbAtoms.insert(atom); 
+  d_bbAtoms.insert(atom);
 }
 
 void EagerBitblaster::storeBBTerm(TNode node, const Bits& bits) {
@@ -140,13 +140,13 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
 void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
   Assert(bits.size() == 0);
   for (unsigned i = 0; i < utils::getSize(var); ++i) {
-    bits.push_back(utils::mkBitOf(var, i)); 
+    bits.push_back(utils::mkBitOf(var, i));
   }
-  d_variables.insert(var); 
+  d_variables.insert(var);
 }
 
 Node EagerBitblaster::getBBAtom(TNode node) const {
-  return node; 
+  return node;
 }
 
 
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index ca21e98c4..c8c2d62f3 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -9,9 +9,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Bitblaster for the lazy bv solver. 
+ ** \brief Bitblaster for the lazy bv solver.
  **
- ** Bitblaster for the lazy bv solver. 
+ ** Bitblaster for the lazy bv solver.
  **/
 
 #include "bitblaster_template.h"
@@ -123,11 +123,11 @@ void TLazyBitblaster::bbAtom(TNode node) {
       }
       atom_bb = utils::mkAnd(atoms);
     }
-    Assert (!atom_bb.isNull()); 
+    Assert (!atom_bb.isNull());
     Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
     storeBBAtom(node, atom_bb);
     d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
-    return; 
+    return;
   }
 
   // the bitblasted definition of the atom
@@ -138,7 +138,7 @@ void TLazyBitblaster::bbAtom(TNode node) {
   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);
@@ -150,7 +150,7 @@ void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
   if( d_bvp != NULL ){
     d_bvp->registerAtomBB(atom.toExpr(), atom_bb.toExpr());
   }
-  d_bbAtoms.insert(atom); 
+  d_bbAtoms.insert(atom);
 }
 
 void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
@@ -160,16 +160,16 @@ void TLazyBitblaster::storeBBTerm(TNode node, const Bits& bits) {
 
 
 bool TLazyBitblaster::hasBBAtom(TNode atom) const {
-  return d_bbAtoms.find(atom) != d_bbAtoms.end(); 
+  return d_bbAtoms.find(atom) != d_bbAtoms.end();
 }
 
 
 void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
   Assert(bits.size() == 0);
   for (unsigned i = 0; i < utils::getSize(var); ++i) {
-    bits.push_back(utils::mkBitOf(var, i)); 
+    bits.push_back(utils::mkBitOf(var, i));
   }
-  d_variables.insert(var); 
+  d_variables.insert(var);
 }
 
 uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
@@ -182,7 +182,7 @@ uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
 
 // cnf conversion ensures the atom represents itself
 Node TLazyBitblaster::getBBAtom(TNode node) const {
-  return node; 
+  return node;
 }
 
 void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
@@ -220,9 +220,9 @@ void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
     for (unsigned i = 0; i < literal_explanation.size(); ++i) {
       explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
     }
-    return; 
+    return;
   }
-  
+
   std::vector<prop::SatLiteral> literal_explanation;
   d_satSolver->explain(lit, literal_explanation);
   for (unsigned i = 0; i < literal_explanation.size(); ++i) {
@@ -285,7 +285,7 @@ bool TLazyBitblaster::solve() {
     }
   }
   Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
-  d_satSolverFullModel.set(true); 
+  d_satSolverFullModel.set(true);
   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
@@ -357,11 +357,11 @@ bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
       d_lazyBB->d_explanations->insert(lit, literal_explanation);
     } else {
       // we propagated it at a lower level
-      return true; 
+      return true;
     }
   }
   ++(d_lazyBB->d_statistics.d_numBitblastingPropagations);
-  TNode atom = d_cnf->getNode(lit); 
+  TNode atom = d_cnf->getNode(lit);
   return d_bv->storePropagation(atom, SUB_BITBLAST);
 }
 
@@ -398,13 +398,13 @@ EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) {
   if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
 
   if (!d_satSolverFullModel.get())
-    return theory::EQUALITY_UNKNOWN; 
-  
+    return theory::EQUALITY_UNKNOWN;
+
   // Check if cache is valid (invalidated in check and pops)
   if (d_bv->d_invalidateModelCache.get()) {
-    invalidateModelCache(); 
+    invalidateModelCache();
   }
-  d_bv->d_invalidateModelCache.set(false); 
+  d_bv->d_invalidateModelCache.set(false);
 
   Node a_value = getTermModel(a, true);
   Node b_value = getTermModel(b, true);
@@ -414,10 +414,10 @@ EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) {
 
   if (a_value == b_value) {
     Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n";
-    return theory::EQUALITY_TRUE_IN_MODEL; 
+    return theory::EQUALITY_TRUE_IN_MODEL;
   }
   Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n";
-  return theory::EQUALITY_FALSE_IN_MODEL; 
+  return theory::EQUALITY_FALSE_IN_MODEL;
 }
 
 
@@ -426,9 +426,9 @@ bool TLazyBitblaster::isSharedTerm(TNode node) {
 }
 
 bool TLazyBitblaster::hasValue(TNode a) {
-  Assert (hasBBTerm(a)); 
+  Assert (hasBBTerm(a));
   Bits bits;
-  getBBTerm(a, bits); 
+  getBBTerm(a, bits);
   for (int i = bits.size() -1; i >= 0; --i) {
     prop::SatValue bit_value;
     if (d_cnfStream->hasLiteral(bits[i])) {
@@ -456,7 +456,7 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   if (!hasBBTerm(a)) {
     return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
   }
-  
+
   Bits bits;
   getBBTerm(a, bits);
   Integer value(0);
@@ -486,13 +486,13 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
     // not actually a leaf of the bit-vector theory
     if (d_variables.find(var) == d_variables.end())
       continue;
-    
-    Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); 
+
+    Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
     // only shared terms could not have been bit-blasted
     Assert (hasBBTerm(var) || isSharedTerm(var));
-    
+
     Node const_value = getModelFromSatSolver(var, fullModel);
-    Assert (const_value.isNull() || const_value.isConst()); 
+    Assert (const_value.isNull() || const_value.isConst());
     if(const_value != Node()) {
       Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
                                << var << " "
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 89cba3ae4..8cfd5159e 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -122,7 +122,7 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const {
 
 bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value)
 {
-  Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;
+  Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << "," << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;
 
   if (d_inConflict) {
     return false;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c988c9120..b95b4f5a3 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -277,7 +277,7 @@ protected:
    *
    */
   bool d_proofsEnabled;
-  
+
   /**
    * Returns the next assertion in the assertFact() queue.
    *
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8228861be..045af0864 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -198,6 +198,7 @@ void TheoryEngine::interrupt() throw(ModalException) {
 
 void TheoryEngine::preRegister(TNode preprocessed) {
 
+  Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl;
   if(Dump.isOn("missed-t-propagations")) {
     d_possiblePropagations.push_back(preprocessed);
   }
@@ -425,7 +426,7 @@ void TheoryEngine::check(Theory::Effort effort) {
     }
 
     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
-    Debug("theory") << ", need check = " << needCheck() << endl;
+    Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 
     if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) {
       AlwaysAssert(d_masterEqualityEngine->consistent());
@@ -490,7 +491,7 @@ void TheoryEngine::combineTheories() {
 
     // We need to split on it
     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-    lemma(equality.orNode(equality.notNode()), RULE_INVALID, false, false, false, carePair.theory);
+    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) {
@@ -1263,8 +1264,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
   return conjunction;
 }
 
-
-Node TheoryEngine::getExplanation(TNode node) {
+NodeTheoryPair TheoryEngine::getExplanationAndExplainer(TNode node) {
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
 
   bool polarity = node.getKind() != kind::NOT;
@@ -1274,12 +1274,16 @@ Node TheoryEngine::getExplanation(TNode node) {
   if (!d_logicInfo.isSharingEnabled()) {
     Node explanation = theoryOf(atom)->explain(node);
     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
-    return explanation;
+    return NodeTheoryPair(explanation, theoryOf(atom)->getId());
   }
 
   // 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];
+  TheoryId explainer = nodeExplainerPair.theory;
+
   // Create the workplace for explanations
   std::vector<NodeTheoryPair> explanationVector;
   explanationVector.push_back(d_propagationMap[toExplain]);
@@ -1289,7 +1293,11 @@ Node TheoryEngine::getExplanation(TNode node) {
 
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
 
-  return explanation;
+  return NodeTheoryPair(explanation, explainer);
+}
+
+Node TheoryEngine::getExplanation(TNode node) {
+  return getExplanationAndExplainer(node).node;
 }
 
 struct AtomsCollect {
@@ -1391,7 +1399,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         bool negated,
                                         bool removable,
                                         bool preprocess,
-                                        theory::TheoryId atomsTo) {
+                                        theory::TheoryId atomsTo,
+                                        theory::TheoryId ownerTheory) {
   // For resource-limiting (also does a time check).
   // spendResource();
 
@@ -1417,12 +1426,13 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
     d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
   }
 
+  std::vector<Node> additionalLemmas;
+  IteSkolemMap iteSkolemMap;
+
   // Run theory preprocessing, maybe
   Node ppNode = preprocess ? this->preprocess(node) : Node(node);
 
   // Remove the ITEs
-  std::vector<Node> additionalLemmas;
-  IteSkolemMap iteSkolemMap;
   additionalLemmas.push_back(ppNode);
   d_iteRemover.run(additionalLemmas, iteSkolemMap);
   additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
@@ -1440,10 +1450,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, 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, node);
+    d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, ownerTheory, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
@@ -1487,11 +1497,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, RULE_CONFLICT, true, true, false, THEORY_LAST);
+    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
   } else {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
-    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
+    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST, theoryId);
   }
 }
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 05ecc0e91..21d0905e5 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -59,7 +59,7 @@ struct NodeTheoryPair {
   Node node;
   theory::TheoryId theory;
   size_t timestamp;
-  NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp)
+  NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0)
   : node(node), theory(theory), timestamp(timestamp) {}
   NodeTheoryPair()
   : theory(theory::THEORY_LAST) {}
@@ -263,7 +263,7 @@ class TheoryEngine {
     {
     }
 
-      void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
+    void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
       spendResource(ammount);
       if (d_engine->d_interrupted) {
         throw theory::Interrupted();
@@ -294,14 +294,14 @@ class TheoryEngine {
       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);
+      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) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
-      return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
+      return d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory, d_theory);
     }
 
     void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
@@ -448,7 +448,8 @@ class TheoryEngine {
                             bool negated,
                             bool removable,
                             bool preprocess,
-                            theory::TheoryId atomsTo);
+                            theory::TheoryId atomsTo,
+                            theory::TheoryId ownerTheory);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
@@ -719,6 +720,12 @@ public:
   Node getExplanation(TNode node);
 
   /**
+   * Returns an explanation of the node propagated to the SAT solver and the theory
+   * that propagated it.
+   */
+  NodeTheoryPair getExplanationAndExplainer(TNode node);
+
+  /**
    * collect model info
    */
   void collectModelInfo( theory::TheoryModel* m, bool fullModel );
@@ -783,8 +790,8 @@ public:
    */
   void printSynthSolution( std::ostream& out );
 
-  /** 
-   * Get instantiations 
+  /**
+   * Get instantiations
    */
   void getInstantiations( std::map< Node, std::vector< Node > >& insts );
 
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 0ac5096d2..53347c365 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -42,7 +42,6 @@ EqualityEngine::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&constantTermsCount);
 }
 
-
 /**
  * Data used in the BFS search through the equality graph.
  */
@@ -157,7 +156,7 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
 }
 
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
-  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl;
   if (back) {
     d_propagationQueue.push_back(candidate);
   } else {
@@ -920,7 +919,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const {
 }
 
 void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const {
-  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
 
   // The terms must be there already
   Assert(hasTerm(t1) && hasTerm(t2));;
@@ -933,13 +932,83 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
     // Get the explanation
     getExplanation(t1Id, t2Id, equalities, eqp);
   } else {
+    if (eqp) {
+      eqp->d_id = eq::MERGED_THROUGH_TRANS;
+      eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode();
+    }
+
     // Get the reason for this disequality
     EqualityPair pair(t1Id, t2Id);
     Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about");
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
+
     for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
-      getExplanation(toExplain.first, toExplain.second, equalities, eqp);
+    }
+
+    for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
+
+      EqualityPair toExplain = d_deducedDisequalityReasons[i];
+      EqProof* eqpc = NULL;
+
+      // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
+      if (eqp && toExplain.first != toExplain.second) {
+        eqpc = new EqProof;
+      }
+
+      // Some edges have the form ((a == b) == false). Translate this into (not (a == b)).
+      // Assert(d_nodes[toExplain.first] != NodeManager::currentNM()->mkConst(false));
+
+      getExplanation(toExplain.first, toExplain.second, equalities, eqpc);
+
+      // if (eqpc) {
+      //   eqp->d_children.push_back(eqpc);
+      // }
+
+      if (eqpc) {
+        Debug("pf::ee") << "Child proof is:" << std::endl;
+        eqpc->debug_print("pf::ee", 1);
+
+        if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) {
+          std::vector<EqProof *> orderedChildren;
+          bool nullCongruenceFound = false;
+          for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
+            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) {
+
+              // For now, assume there can only be one null congruence child
+              Assert(!nullCongruenceFound);
+              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]);
+            } else {
+              orderedChildren.push_back(eqpc->d_children[i]);
+            }
+          }
+
+          if (nullCongruenceFound) {
+            eqpc->d_children = orderedChildren;
+            Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl;
+            eqpc->debug_print("pf::ee", 1);
+          }
+        }
+
+        eqp->d_children.push_back(eqpc);
+      }
+    }
+
+    if (eqp) {
+      if(eqp->d_children.size() == 1) {
+        // The transitivity proof has just one child. Simplify.
+        EqProof* temp = eqp->d_children[0];
+        eqp->d_children.clear();
+        *eqp = *temp;
+        delete temp;
+      }
+
+      Debug("pf::ee") << "Disequality explanation final proof: " << std::endl;
+      eqp->debug_print("pf::ee", 1);
     }
   }
 }
@@ -972,7 +1041,12 @@ 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 = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
+      if ((d_nodes[t1Id].getKind() == kind::BUILTIN) && (d_nodes[t1Id].getConst<Kind>() == kind::SELECT)) {
+        std::vector<Node> no_children;
+        eqp->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, no_children);
+      } else {
+        eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
+      }
     }
     return;
   }
@@ -1019,7 +1093,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
           Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
 
-          std::vector< EqProof * > eqp_trans;
+          std::vector<EqProof *> eqp_trans;
 
           // Reconstruct the path
           do {
@@ -1029,11 +1103,13 @@ 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 << "                     targetNode = " << d_nodes[edgeNode] << std::endl;
             Debug("equality") << d_name << "                     in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
+            Debug("equality") << d_name << "                     reason type = " << reasonType << std::endl;
 
-            EqProof * eqpc = NULL;
-            //make child proof if a proof is being constructed
-            if( eqp ){
+            EqProof* eqpc = NULL;
+            // Make child proof if a proof is being constructed
+            if (eqp) {
               eqpc = new EqProof;
               eqpc->d_id = reasonType;
             }
@@ -1044,26 +1120,60 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl;
               const FunctionApplication& f1 = d_applications[currentNode].original;
               const FunctionApplication& f2 = d_applications[edgeNode].original;
+
+              Debug("pf::ee") << "We need to prove two equalities:" << std::endl;
+              Debug("pf::ee") << "\tLHS: " << d_nodes[f1.a] << " = " << d_nodes[f2.a] << std::endl;
+              Debug("pf::ee") << "\tRHS: " << d_nodes[f1.b] << " = " << d_nodes[f2.b] << std::endl;
+
               Debug("equality") << push;
+              Debug("equality") << "Explaining left hand side equalities" << std::endl;
               EqProof * eqpc1 = eqpc ? new EqProof : NULL;
               getExplanation(f1.a, f2.a, equalities, eqpc1);
+              Debug("equality") << "Explaining right hand side equalities" << std::endl;
               EqProof * eqpc2 = eqpc ? new EqProof : NULL;
               getExplanation(f1.b, f2.b, equalities, eqpc2);
               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;
+                Debug("pf::ee") << "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;
+                  Debug("pf::ee") << 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("pf::ee") << "f1.a is: " << d_nodes[f1.a]
+                                    << ". kind is: " << d_nodes[f1.a].getKind() << std::endl;
+
+                    if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) {
+                      Debug("pf::ee") << "f1.a getConst<kind> is: " << d_nodes[f1.a].getConst<Kind>() << std::endl;
+
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]);
+                      // The first child is a PARTIAL_SELECT_0. Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
+                      Debug("pf::ee") << "eqpc->d_children[0]->d_node.getKind() == " << eqpc->d_children[0]->d_node.getKind() << std::endl;
+                      Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0);
+                      Assert(eqpc->d_children[0]->d_children.size() == 0);
+
+                      Debug("pf::ee") << "Dumping the equality proof before:" << std::endl;
+                      eqpc->debug_print("pf::ee", 1);
+
+                      eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, d_nodes[f1.b]);
+
+                      Debug("pf::ee") << "Dumping the equality proof after:" << std::endl;
+                      eqpc->debug_print("pf::ee", 1);
+
+                      //eqpc->d_children[0]->d_node.append(d_nodes[f1.b]);
+                    } else {
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF,
+                                                                      ProofManager::currentPM()->mkOp(d_nodes[f1.a]),
+                                                                      d_nodes[f1.b]);
+                    }
+                    Debug("pf::ee") << "New d_node is: " << eqpc->d_node << std::endl;
                   }
                 }
               }
@@ -1114,16 +1224,162 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
               break;
             }
+            case MERGED_ARRAYS_EXT:
+
+              Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_EXT" << std::endl;
+
+              if (eqpc) {
+                Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+                Node b = d_nodes[currentNode];
+
+                // GK: todo: here we assume that a=b is an assertion. We should probably call explain()
+                // recursively, to explain this.
+
+                if (a == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = b.notNode();
+                } else if (b == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = a.notNode();
+                } else {
+                  eqpc->d_node = a.eqNode(b);
+                }
+
+                EqProof* eqpc1 = new EqProof;
+                eqpc1->d_node = d_equalityEdges[currentEdge].getReason();
+                eqpc->d_children.push_back( eqpc1 );
+
+                eqpc1->debug_print("pf::ee", 1);
+                eqpc->debug_print("pf::ee", 1);
+              }
+
+              // We push the reason into "equalities" because that's what the theory of arrays expects.
+              equalities.push_back(d_equalityEdges[currentEdge].getReason());
+              break;
+
+            case MERGED_ARRAYS_ROW: {
+              Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_ROW" << std::endl;
+
+              // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
+              // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
+              // or ((a[i]:=t)[k] == a[k]) because (i != k).
+
+              if (eqpc) {
+                if (d_nodes[currentNode].getNumChildren() == 2) {
+                  // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k).
+
+                  // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be
+                  // false in the first case and true in the second case.
+                  bool currentNodeIsUnchangedArray;
+
+                  Assert(d_nodes[currentNode].getNumChildren() == 2);
+                  Assert(d_nodes[edgeNode].getNumChildren() == 2);
+
+                  if (d_nodes[currentNode][0].getKind() == kind::VARIABLE ||
+                      d_nodes[currentNode][0].getKind() == kind::SKOLEM) {
+                    currentNodeIsUnchangedArray = true;
+                  } else if (d_nodes[edgeNode][0].getKind() == kind::VARIABLE ||
+                             d_nodes[edgeNode][0].getKind() == kind::SKOLEM) {
+                    currentNodeIsUnchangedArray = false;
+                  } else {
+                    Assert(d_nodes[currentNode][0].getKind() == kind::STORE);
+                    Assert(d_nodes[edgeNode][0].getKind() == kind::STORE);
+
+                    if (d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]) {
+                      currentNodeIsUnchangedArray = false;
+                    } else if (d_nodes[edgeNode][0][0] == d_nodes[currentNode][0]) {
+                      currentNodeIsUnchangedArray = true;
+                    } else {
+                      Unreachable();
+                    }
+                  }
+
+                  Node indexOne =
+                    currentNodeIsUnchangedArray ? d_nodes[currentNode][1] : d_nodes[currentNode][0][1];
+                  Node indexTwo =
+                    currentNodeIsUnchangedArray ? d_nodes[edgeNode][0][1] : d_nodes[edgeNode][1];
+
+                  // Some assertions to ensure that the theory of arrays behaves as expected
+                  Assert(d_nodes[currentNode][1] == d_nodes[edgeNode][1]);
+                  if (currentNodeIsUnchangedArray) {
+                    Assert(d_nodes[currentNode][0] == d_nodes[edgeNode][0][0]);
+                  } else {
+                    Assert(d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]);
+                  }
+
+                  Debug("pf::ee") << "Getting explanation for ROW guard: "
+                                     << indexOne << " != " << indexTwo << std::endl;
+
+                  EqProof* eqpcc = eqpc ? new EqProof : NULL;
+                  explainEquality(indexOne, indexTwo, false, equalities, eqpcc);
+
+                  Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl;
+                  Debug("pf::ee") << "And the explanation of their disequality is: " << std::endl;
+                  eqpcc->debug_print("pf::ee", 1);
+                  eqpc->d_children.push_back(eqpcc);
+                } else {
+                  // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
+
+                  Debug("pf::ee") << "In the new case of ROW!" << std::endl;
+
+                  Node indexOne = d_nodes[currentNode];
+                  Node indexTwo = d_nodes[edgeNode];
+
+                  Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl;
+                  Debug("pf::ee") << "The reason for the edge is: " << d_equalityEdges[currentEdge].getReason()
+                                     << std::endl;
+
+                  Assert(d_equalityEdges[currentEdge].getReason().getNumChildren() == 2);
+                  Node reason = d_equalityEdges[currentEdge].getReason()[1];
+                  Debug("pf::ee") << "Getting explanation for ROW guard: " << reason << std::endl;
+
+                  EqProof* eqpcc = eqpc ? new EqProof : NULL;
+                  explainEquality(reason[0], reason[1], false, equalities, eqpcc);
+
+                  if (eqpc) {
+                    Debug("pf::ee") << "The guard's explanation is: " << std::endl;
+                    eqpcc->debug_print("pf::ee", 1);
+                    eqpc->d_children.push_back(eqpcc);
+                  }
+                }
+
+                Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+                Node b = d_nodes[currentNode];
+
+                if (a == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = b.notNode();
+                } else if (b == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = a.notNode();
+                } else {
+                  eqpc->d_node = a.eqNode(b);
+                }
+              }
+
+              // We push the reason into "equalities" because that's what the theory of arrays expects.
+              equalities.push_back(d_equalityEdges[currentEdge].getReason());
+              break;
+            }
+
             default: {
               // Construct the equality
               Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
-              if( eqpc ){
-                if(reasonType == MERGED_THROUGH_EQUALITY) {
+              Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl;
+
+              if (eqpc) {
+                if (reasonType == MERGED_THROUGH_EQUALITY) {
                   eqpc->d_node = d_equalityEdges[currentEdge].getReason();
                 } 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;
+                  // The LFSC translator prefers (not (= a b)) over (= (a==b) false)
+
+                  Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+                  Node b = d_nodes[currentNode];
+
+                  if (a == NodeManager::currentNM()->mkConst(false)) {
+                    eqpc->d_node = b.notNode();
+                  } else if (b == NodeManager::currentNM()->mkConst(false)) {
+                    eqpc->d_node = a.notNode();
+                  } else {
+                    eqpc->d_node = a.eqNode(b);
+                  }
+                  Debug("pf::ee") << "theory eq : " << eqpc->d_node << std::endl;
                 }
                 eqpc->d_id = reasonType;
               }
@@ -1137,7 +1393,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             currentIndex = bfsQueue[currentIndex].previousIndex;
 
             //---from Morgan---
-            if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
+            if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
               if(eqpc->d_node.isNull()) {
                 Assert(eqpc->d_children.size() == 1);
                 EqProof *p = eqpc;
@@ -1149,11 +1405,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             }
             //---end from Morgan---
 
-            eqp_trans.push_back( eqpc );
-
+            eqp_trans.push_back(eqpc);
           } while (currentEdge != null_id);
 
-          if(eqp) {
+          if (eqp) {
             if(eqp_trans.size() == 1) {
               *eqp = *eqp_trans[0];
               delete eqp_trans[0];
@@ -1162,6 +1417,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               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]);
             }
+
+            eqp->debug_print("pf::ee", 1);
           }
 
           // Done
@@ -1508,7 +1765,7 @@ void EqualityEngine::debugPrintGraph() const {
     EqualityEdgeId edgeId = d_equalityGraph[nodeId];
     while (edgeId != null_edge) {
       const EqualityEdge& edge = d_equalityEdges[edgeId];
-      Debug("equality::graph") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
+      Debug("equality::graph") << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
       edgeId = edge.getNext();
     }
 
@@ -1517,17 +1774,19 @@ void EqualityEngine::debugPrintGraph() const {
 }
 
 bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
-  Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")";
 
   Assert(hasTerm(t1));
   Assert(hasTerm(t2));
 
-  return getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+  bool result = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+  Debug("equality") << (result ? "\t(YES)" : "\t(NO)") << std::endl;
+  return result;
 }
 
 bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
 {
-  Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")";
 
   // Add the terms
   Assert(hasTerm(t1));
@@ -1539,6 +1798,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
 
   // If we propagated this disequality we're true
   if (hasPropagatedDisequality(t1Id, t2Id)) {
+    Debug("equality") << "\t(YES)" << std::endl;
     return true;
   }
 
@@ -1556,6 +1816,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId));
       nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
     }
+    Debug("equality") << "\t(YES)" << std::endl;
     return true;
   }
 
@@ -1571,6 +1832,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
+      Debug("equality") << "\t(YES)" << std::endl;
       return true;
     }
   }
@@ -1587,11 +1849,13 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
+      Debug("equality") << "\t(YES)" << std::endl;
       return true;
     }
   }
 
   // Couldn't deduce dis-equalityReturn whether the terms are disequal
+  Debug("equality") << "\t(NO)" << std::endl;
   return false;
 }
 
@@ -2103,7 +2367,7 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{
       d_children[i]->debug_print( c, tb+1 );
     }
   }
-  Debug( c ) << ")";
+  Debug( c ) << ")" << std::endl;
 }
 
 
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index fb1e73575..0c2c3e354 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -95,7 +95,16 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
   case MERGED_THROUGH_TRANS:
     out << "transitivity";
     break;
-  default:
+  case MERGED_ARRAYS_ROW:
+    out << "arrays ROW";
+    break;
+  case MERGED_ARRAYS_ROW1:
+    out << "arrays ROW1";
+    break;
+  case MERGED_ARRAYS_EXT:
+    out << "arrays EXT";
+    break;
+default:
     out << "[theory]";
     break;
   }
@@ -365,4 +374,3 @@ struct TriggerInfo {
 } // namespace eq
 } // namespace theory
 } // namespace CVC4
-
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ffb537734..b8e88a1a3 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -105,6 +105,8 @@ void TheoryUF::check(Effort level) {
     TNode fact = assertion.assertion;
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
+    Debug("uf") << "Term's theory: " << theory::Theory::theoryOf(fact.toExpr()) << std::endl;
+
     if (d_thss != NULL) {
       bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
       d_thss->assertNode(fact, isDecision);
@@ -219,9 +221,15 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro
     d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
   }
   if( pf ){
-    Debug("uf-pf") << std::endl;
-    pf->debug_print("uf-pf");
+    Debug("pf::uf") << std::endl;
+    pf->debug_print("pf::uf");
+  }
+
+  Debug("pf::uf") << "UF: explain( " << literal << " ):" << std::endl << "\t";
+  for (unsigned i = 0; i < assumptions.size(); ++i) {
+    Debug("pf::uf") << assumptions[i] << " ";
   }
+  Debug("pf::uf") << std::endl;
 }
 
 Node TheoryUF::explain(TNode literal) {
@@ -270,6 +278,7 @@ void TheoryUF::presolve() {
     for(vector<Node>::const_iterator i = newClauses.begin();
         i != newClauses.end();
         ++i) {
+      Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
       d_out->lemma(*i);
     }
   }
@@ -521,7 +530,7 @@ void TheoryUF::conflict(TNode a, TNode b) {
   } else {
     d_conflictNode = explain(a.eqNode(b),pf);
   }
-  ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
+  ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
   d_out->conflict(d_conflictNode, puf);
   d_conflict = true;
 }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index e29b923f9..863059525 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -136,7 +136,7 @@ private:
    * 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;