merge from arrays-clark branch

25 files changed, 2236 insertions, 1473 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1c6287c4a..3b29cbcd1 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -345,6 +345,11 @@ void TheoryArith::addSharedTerm(TNode n){
 }
 
 Node TheoryArith::ppRewrite(TNode atom) {
+
+  if (!atom.getType().isBoolean()) {
+    return atom;
+  }
+
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
   Node a = d_pbSubstitutions.apply(atom);
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 50ded8758..cd6c38a7f 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -139,6 +139,20 @@ void ArrayInfo::addInStore(const TNode a, const TNode b){
 };
 
 
+void ArrayInfo::setNonLinear(const TNode a) {
+  Assert(a.getType().isArray());
+  Info* temp_info;
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_info = new Info(ct, bck);
+    temp_info->isNonLinear = true;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->isNonLinear = true;
+  }
+  
+}
+
 
 /**
  * Returns the information associated with TNode a
@@ -152,6 +166,15 @@ const Info* ArrayInfo::getInfo(const TNode a) const{
   return emptyInfo;
 }
 
+const bool ArrayInfo::isNonLinear(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end())
+      return (*it).second->isNonLinear;
+  return false;
+}
+
 List<TNode>* ArrayInfo::getIndices(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
   if(it!= info_map.end()) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index d1c435b48..3eae369ca 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -55,9 +55,10 @@ namespace theory {
 namespace arrays {
 
 typedef context::CDList<TNode> CTNodeList;
+typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
 
-struct TNodeQuadHashFunction {
-  size_t operator()(const quad<CVC4::TNode, CVC4::TNode, CVC4::TNode, CVC4::TNode>& q ) const {
+struct RowLemmaTypeHashFunction {
+  size_t operator()(const RowLemmaType& q ) const {
     TNode n1 = q.first;
     TNode n2 = q.second;
     TNode n3 = q.third;
@@ -66,7 +67,7 @@ struct TNodeQuadHashFunction {
         n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
 
   }
-};/* struct TNodeQuadHashFunction */
+};/* struct RowLemmaTypeHashFunction */
 
 void printList (CTNodeList* list);
 void printList( List<TNode>* list);
@@ -81,11 +82,12 @@ bool inList(const CTNodeList* l, const TNode el);
 
 class Info {
 public:
+  context::CDO<bool> isNonLinear;
   List<TNode>* indices;
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck) {
+  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false) {
     indices = new List<TNode>(bck);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
@@ -228,6 +230,7 @@ public:
   void addStore(const Node a, const TNode st);
   void addInStore(const TNode a, const TNode st);
 
+  void setNonLinear(const TNode a);
 
   /**
    * Returns the information associated with TNode a
@@ -235,6 +238,8 @@ public:
 
   const Info* getInfo(const TNode a) const;
 
+  const bool isNonLinear(const TNode a) const;
+
   List<TNode>* getIndices(const TNode a) const;
 
   const CTNodeList* getStores(const TNode a) const;
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 2f4bc7313..06240a315 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -7,7 +7,7 @@
 theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
 typechecker "theory/arrays/theory_arrays_type_rules.h"
 
-properties polite stable-infinite
+properties polite stable-infinite parametric
 properties check propagate presolve
 
 rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
@@ -24,7 +24,11 @@ operator SELECT 2 "array select"
 # store a i e  is  a[i] <= e
 operator STORE 3 "array store"
 
+# used internally by array theory
+operator ARR_TABLE_FUN 4 "array table function"
+
 typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
 typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
+typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
 
 endtheory
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 03a9d7a4c..718483143 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,45 +23,87 @@
 #include <map>
 #include "theory/rewriter.h"
 #include "expr/command.h"
+#include "theory/uf/equality_engine_impl.h"
+
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arrays;
 
 
-TheoryArrays::TheoryArrays(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) :
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+
+// These are the options that produce the best empirical results on QF_AX benchmarks.
+// Use static configuration of options for now
+const bool d_ccStore = false;
+const bool d_useArrTable = false;
+const bool d_eagerLemmas = true;
+const bool d_propagateLemmas = false;
+const bool d_preprocess = true;
+const bool d_solveWrite = true;
+const bool d_useNonLinearOpt = true;
+
+
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
   Theory(THEORY_ARRAY, c, u, out, valuation),
-  d_ccChannel(this),
-  d_cc(c, &d_ccChannel),
-  d_unionFind(c),
-  d_backtracker(c),
-  d_infoMap(c,&d_backtracker),
-  d_disequalities(c),
-  d_equalities(c),
-  d_prop_queue(c),
-  d_atoms(),
-  d_explanations(c),
-  d_conflict(),
   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_checkTimer("theory::arrays::checkTime"),
-  d_donePreregister(false)
+  d_ppNotify(),
+  d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"),
+  d_ppFacts(u),
+  //  d_ppCache(u),  
+  d_literalsToPropagate(c),
+  d_literalsToPropagateIndex(c, 0),
+  d_mayEqualNotify(),
+  d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"),
+  d_notify(*this),
+  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"),
+  d_conflict(c, false),
+  d_backtracker(c),
+  d_infoMap(c, &d_backtracker),
+  d_mergeQueue(c),
+  d_mergeInProgress(false),
+  d_RowQueue(u),
+  d_RowAlreadyAdded(u),
+  d_sharedArrays(c),
+  d_sharedTerms(c, false),
+  d_reads(c),
+  d_permRef(c)
 {
-  //d_backtracker = new Backtracker<TNode>(c);
-  //d_infoMap = ArrayInfo(c, d_backtracker);
-
   StatisticsRegistry::registerStat(&d_numRow);
   StatisticsRegistry::registerStat(&d_numExt);
   StatisticsRegistry::registerStat(&d_numProp);
   StatisticsRegistry::registerStat(&d_numExplain);
+  StatisticsRegistry::registerStat(&d_numNonLinear);
+  StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits);
   StatisticsRegistry::registerStat(&d_checkTimer);
 
+  d_true = NodeManager::currentNM()->mkConst<bool>(true);
+  d_false = NodeManager::currentNM()->mkConst<bool>(false);
+
+  d_ppEqualityEngine.addTerm(d_true);
+  d_ppEqualityEngine.addTerm(d_false);
+  d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false);
+
+  d_equalityEngine.addTerm(d_true);
+  d_equalityEngine.addTerm(d_false);
+  d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
 
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine.addFunctionKind(kind::SELECT);
+  if (d_ccStore) {
+    d_equalityEngine.addFunctionKind(kind::STORE);
+  }
+  d_equalityEngine.addFunctionKind(kind::EQUAL);
+  if (d_useArrTable) {
+    d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
+  }
 }
 
 
@@ -71,159 +113,27 @@ TheoryArrays::~TheoryArrays() {
   StatisticsRegistry::unregisterStat(&d_numExt);
   StatisticsRegistry::unregisterStat(&d_numProp);
   StatisticsRegistry::unregisterStat(&d_numExplain);
+  StatisticsRegistry::unregisterStat(&d_numNonLinear);
+  StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits);
   StatisticsRegistry::unregisterStat(&d_checkTimer);
 
 }
 
 
-void TheoryArrays::addSharedTerm(TNode t) {
-  Trace("arrays") << "Arrays::addSharedTerm(): "
-                  << t << endl;
-}
-
-
-void TheoryArrays::notifyEq(TNode lhs, TNode rhs) {
-}
-
-void TheoryArrays::notifyCongruent(TNode a, TNode b) {
-  Trace("arrays") << "Arrays::notifyCongruent(): "
-       << a << " = " << b << endl;
-  if(!d_conflict.isNull()) {
-    return;
-  }
-  merge(a,b);
-}
-
-
-void TheoryArrays::check(Effort e) {
-  TimerStat::CodeTimer codeTimer(d_checkTimer);
-
-  if(!d_donePreregister ) {
-    // only start looking for lemmas after preregister on all input terms
-    // has been called
-   return;
-  }
-
-  Trace("arrays") <<"Arrays::start check ";
-  while(!done()) {
-    Node assertion = get();
-    Trace("arrays") << "Arrays::check(): " << assertion << endl;
-
-    switch(assertion.getKind()) {
-    case kind::EQUAL:
-    case kind::IFF:
-      d_cc.addEquality(assertion);
-      if(!d_conflict.isNull()) {
-        // addEquality can cause a notify congruent which calls merge
-        // which can lead to a conflict
-        Node conflict = constructConflict(d_conflict);
-        d_conflict = Node::null();
-        d_out->conflict(conflict);
-        return;
-      }
-      merge(assertion[0], assertion[1]);
-      break;
-    case kind::NOT:
-    {
-      Assert(assertion[0].getKind() == kind::EQUAL ||
-         assertion[0].getKind() == kind::IFF );
-      Node a = assertion[0][0];
-      Node b = assertion[0][1];
-      addDiseq(assertion[0]);
-
-      d_cc.addTerm(a);
-      d_cc.addTerm(b);
-
-      if(!d_conflict.isNull()) {
-        // we got notified through notifyCongruent which called merge
-        // after addTerm since we weren't watching a or b before
-        Node conflict = constructConflict(d_conflict);
-        d_conflict = Node::null();
-        d_out->conflict(conflict);
-        return;
-      }
-      else if(find(a) == find(b)) {
-        Node conflict = constructConflict(assertion[0]);
-        d_conflict = Node::null();
-        d_out->conflict(conflict);
-        return;
-        }
-      Assert(!d_cc.areCongruent(a,b));
-      if(a.getType().isArray()) {
-        queueExtLemma(a, b);
-      }
-      break;
-    }
-    default:
-      Unhandled(assertion.getKind());
-    }
-
-  }
-
-  if(fullEffort(e)) {
-    // generate the lemmas on the worklist
-    //while(!d_RowQueue.empty() || ! d_extQueue.empty()) {
-    dischargeLemmas();
-    Trace("arrays-lem")<<"Arrays::discharged lemmas "<<d_RowQueue.size()<<"\n";
-    //}
-  }
-  Trace("arrays") << "Arrays::check(): done" << endl;
-}
-
-Node TheoryArrays::getValue(TNode n) {
-  NodeManager* nodeManager = NodeManager::currentNM();
-
-  switch(n.getKind()) {
+/////////////////////////////////////////////////////////////////////////////
+// PREPROCESSING
+/////////////////////////////////////////////////////////////////////////////
 
-  case kind::VARIABLE:
-    Unhandled(kind::VARIABLE);
-
-  case kind::EQUAL: // 2 args
-    return nodeManager->
-      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
-
-  default:
-    Unhandled(n.getKind());
-  }
-}
-
-Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  switch(in.getKind()) {
-    case kind::EQUAL:
-    {
-      d_staticFactManager.addEq(in);
-      if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
-        outSubstitutions.addSubstitution(in[0], in[1]);
-        return PP_ASSERT_STATUS_SOLVED;
-      }
-      if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
-        outSubstitutions.addSubstitution(in[1], in[0]);
-        return PP_ASSERT_STATUS_SOLVED;
-      }
-      break;
-    }
-    case kind::NOT:
-    {
-      Assert(in[0].getKind() == kind::EQUAL ||
-             in[0].getKind() == kind::IFF );
-      Node a = in[0][0];
-      Node b = in[0][1];
-      d_staticFactManager.addDiseq(in[0]);
-      break;
-    }
-    default:
-      break;
-  }
-  return PP_ASSERT_STATUS_UNSOLVED;
-}
 
-Node TheoryArrays::preprocessTerm(TNode term) {
+Node TheoryArrays::ppRewrite(TNode term) {
+  if (!d_preprocess) return term;
   switch (term.getKind()) {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
       if (term[0].getKind() == kind::STORE &&
-          d_staticFactManager.areDiseq(term[0][1], term[1])) {
+          (d_ppEqualityEngine.areDisequal(term[0][1], term[1]) ||
+           (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
         return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
       }
       break;
@@ -233,7 +143,8 @@ Node TheoryArrays::preprocessTerm(TNode term) {
       //    IF i != j and j comes before i in the ordering
       if (term[0].getKind() == kind::STORE &&
           (term[1] < term[0][1]) &&
-          d_staticFactManager.areDiseq(term[1], term[0][1])) {
+          (d_ppEqualityEngine.areDisequal(term[1], term[0][1]) ||
+           (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
         Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
         Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
         return outer;
@@ -241,6 +152,7 @@ Node TheoryArrays::preprocessTerm(TNode term) {
       break;
     }
     case kind::EQUAL: {
+      if (!d_solveWrite) break;
       if (term[0].getKind() == kind::STORE ||
           term[1].getKind() == kind::STORE) {
         TNode left = term[0];
@@ -295,7 +207,8 @@ Node TheoryArrays::preprocessTerm(TNode term) {
                 NodeBuilder<> hyp(kind::AND);
                 for (j = leftWrites - 1; j > i; --j) {
                   index_j = write_j[1];
-                  if (d_staticFactManager.areDiseq(index_i, index_j)) {
+                  if (d_ppEqualityEngine.areDisequal(index_i, index_j) ||
+                      (index_i.isConst() && index_j.isConst() && index_i != index_j)) {
                     continue;
                   }
                   Node hyp2(index_i.getType() == nm->booleanType()? 
@@ -338,7 +251,7 @@ Node TheoryArrays::preprocessTerm(TNode term) {
           Node l = left;
           Node tmp;
           NodeBuilder<> nb(kind::AND);
-          while (right.getKind() == STORE) {
+          while (right.getKind() == kind::STORE) {
             tmp = nm->mkNode(kind::SELECT, l, right[1]);
             nb << tmp.eqNode(right[2]);
             tmp = nm->mkNode(kind::SELECT, right[0], right[1]);
@@ -357,699 +270,683 @@ Node TheoryArrays::preprocessTerm(TNode term) {
   return term;
 }
 
-Node TheoryArrays::recursivePreprocessTerm(TNode term) {
-  unsigned nc = term.getNumChildren();
-  if (nc == 0 ||
-      (theoryOf(term) != theory::THEORY_ARRAY &&
-       term.getType() != NodeManager::currentNM()->booleanType())) {
-    return term;
-  }
-  NodeMap::iterator find = d_ppCache.find(term);
-  if (find != d_ppCache.end()) {
-    return (*find).second;
-  }
-  NodeBuilder<> newNode(term.getKind());
-  unsigned i;
-  for (i = 0; i < nc; ++i) {
-    newNode << recursivePreprocessTerm(term[i]);
-  }
-  Node newTerm = Rewriter::rewrite(newNode);
-  Node newTerm2 = preprocessTerm(newTerm);
-  if (newTerm != newTerm2) {
-    newTerm = recursivePreprocessTerm(Rewriter::rewrite(newTerm2));
-  }
-  d_ppCache[term] = newTerm;
-  return newTerm;
-}
 
-Node TheoryArrays::ppRewrite(TNode atom) {
-  if (d_donePreregister) return atom;
-  Assert(atom.getKind() == kind::EQUAL, "expected EQUAL, got %s", atom.toString().c_str());
-  return recursivePreprocessTerm(atom);
+Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+  switch(in.getKind()) {
+    case kind::EQUAL:
+    {
+      d_ppFacts.push_back(in);
+      d_ppEqualityEngine.addEquality(in[0], in[1], in);
+      if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
+        outSubstitutions.addSubstitution(in[0], in[1]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) {
+        outSubstitutions.addSubstitution(in[1], in[0]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      break;
+    }
+    case kind::NOT:
+    {
+      d_ppFacts.push_back(in);
+      Assert(in[0].getKind() == kind::EQUAL ||
+             in[0].getKind() == kind::IFF );
+      Node a = in[0][0];
+      Node b = in[0][1];
+      d_ppEqualityEngine.addDisequality(a, b, in);
+      break;
+    }
+    default:
+      break;
+  }
+  return PP_ASSERT_STATUS_UNSOLVED;
 }
 
 
-void TheoryArrays::merge(TNode a, TNode b) {
-  Assert(d_conflict.isNull());
+/////////////////////////////////////////////////////////////////////////////
+// T-PROPAGATION / REGISTRATION
+/////////////////////////////////////////////////////////////////////////////
 
-  Trace("arrays-merge")<<"Arrays::merge() " << a <<" and " <<b <<endl;
 
-  /*
-   * take care of the congruence closure part
-   */
+bool TheoryArrays::propagate(TNode literal)
+{
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal  << ")" << std::endl;
 
-  // make "a" the one with shorter diseqList
-  CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
-  CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl;
+    return false;
+  }
 
-  if(deq_ia != d_disequalities.end()) {
-    if(deq_ib == d_disequalities.end() ||
-       (*deq_ia).second->size() > (*deq_ib).second->size()) {
-      TNode tmp = a;
-      a = b;
-      b = tmp;
+  // See if the literal has been asserted already
+  Node normalized = Rewriter::rewrite(literal);
+  bool satValue = false;
+  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
+
+  // If asserted, we're done or in conflict
+  if (isAsserted) {
+    if (!satValue) {
+      Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+      std::vector<TNode> assumptions;
+      Node negatedLiteral;
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+        assumptions.push_back(negatedLiteral);
+      }
+      explain(literal, assumptions);
+      d_conflictNode = mkAnd(assumptions);
+      d_conflict = true;
+      return false;
     }
+    // Propagate even if already known in SAT - could be a new equation between shared terms
+    // (terms that weren't shared when the literal was asserted!)
   }
-  a = find(a);
-  b = find(b);
 
-  if( a == b) {
-    return;
-  }
+  // Nothing, just enqueue it for propagation and mark it as asserted already
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+  d_literalsToPropagate.push_back(literal);
 
+  return true;
+}/* TheoryArrays::propagate(TNode) */
 
-  // b becomes the canon of a
-  setCanon(a, b);
-
-  deq_ia = d_disequalities.find(a);
-  map<TNode, TNode> alreadyDiseqs;
-  if(deq_ia != d_disequalities.end()) {
-    /*
-     * Collecting the disequalities of b, no need to check for conflicts
-     * since the representative of b does not change and we check all the things
-     * in a's class when we look at the diseq list of find(a)
-     */
-
-    CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
-    if(deq_ib != d_disequalities.end()) {
-      CTNodeListAlloc* deq = (*deq_ib).second;
-      for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) {
-        TNode deqn = *j;
-        TNode s = deqn[0];
-        TNode t = deqn[1];
-        TNode sp = find(s);
-        TNode tp = find(t);
-        Assert(sp == b || tp == b);
-        if(sp == b) {
-          alreadyDiseqs[tp] = deqn;
-        } else {
-          alreadyDiseqs[sp] = deqn;
-        }
-      }
-    }
 
-    /*
-     * Looking for conflicts in the a disequality list. Note
-     * that at this point a and b are already merged. Also has
-     * the side effect that it adds them to the list of b (which
-     * became the canonical representative)
-     */
-
-    CTNodeListAlloc* deqa = (*deq_ia).second;
-    for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) {
-      TNode deqn = (*i);
-      Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF);
-      TNode s = deqn[0];
-      TNode t = deqn[1];
-      TNode sp = find(s);
-      TNode tp = find(t);
-
-      if(find(s) == find(t)) {
-        d_conflict = deqn;
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+    case kind::EQUAL:
+      lhs = literal[0];
+      rhs = literal[1];
+      break;
+    case kind::SELECT:
+      lhs = literal;
+      rhs = d_true;
+      break;
+    case kind::NOT:
+      if (literal[0].getKind() == kind::EQUAL) {
+        // Disequalities
+        d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
         return;
-      }
-      Assert( sp == b || tp == b);
-
-      // make sure not to add duplicates
-
-      if(sp == b) {
-        if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
-          appendToDiseqList(b, deqn);
-          alreadyDiseqs[tp] = deqn;
-        }
       } else {
-        if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
-          appendToDiseqList(b, deqn);
-          alreadyDiseqs[sp] = deqn;
-        }
+        // Predicates
+        lhs = literal[0];
+        rhs = d_false;
+        break;
       }
+    case kind::CONST_BOOLEAN:
+      // we get to explain true = false, since we set false to be the trigger of this
+      lhs = d_true;
+      rhs = d_false;
+      break;
+    default:
+      Unreachable();
+  }
+  d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
 
+
+  /**
+   * Stores in d_infoMap the following information for each term a of type array:
+   *
+   *    - all i, such that there exists a term a[i] or a = store(b i v)
+   *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
+   *      position i due to the implicit axiom store(b i v)[i] = v )
+   *
+   *    - all the stores a is congruent to (this information is context dependent)
+   *
+   *    - all store terms of the form store (a i v) (i.e. in which a appears
+   *      directly; this is invariant because no new store terms are created)
+   *
+   * Note: completeness depends on having pre-register called on all the input
+   *       terms before starting to instantiate lemmas.
+   */
+void TheoryArrays::preRegisterTerm(TNode node)
+{
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
+
+  switch (node.getKind()) {
+  case kind::EQUAL:
+    // Add the terms
+    //    d_equalityEngine.addTerm(node[0]);
+    //    d_equalityEngine.addTerm(node[1]);
+    d_equalityEngine.addTerm(node);
+    // Add the trigger for equality
+    d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+    d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+    break;
+  case kind::SELECT:
+    // Reads
+    d_equalityEngine.addTerm(node);
+    // Maybe it's a predicate
+    // TODO: remove this or keep it if we allow Boolean elements in arrays.
+    if (node.getType().isBoolean()) {
+      // Get triggered for both equal and dis-equal
+      d_equalityEngine.addTriggerEquality(node, d_true, node);
+      d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
     }
-  }
 
-  // TODO: check for equality propagations
-  // a and b are find(a) and find(b) here
-  checkPropagations(a,b);
+    d_infoMap.addIndex(node[0], node[1]);
+    checkRowForIndex(node[1], d_equalityEngine.getRepresentative(node[0]));
+    d_reads.push_back(node);
+    break;
 
-  if(a.getType().isArray()) {
-    checkRowLemmas(a,b);
-    checkRowLemmas(b,a);
-    // note the change in order, merge info adds the list of
-    // the 2nd argument to the first
-    d_infoMap.mergeInfo(b, a);
-  }
+  case kind::STORE: {
+    d_equalityEngine.addTriggerTerm(node);
 
+    TNode a = node[0];
+    TNode i = node[1];
+    TNode v = node[2];
 
-}
+    d_mayEqualEqualityEngine.addEquality(node, node[0], d_true);
 
+    NodeManager* nm = NodeManager::currentNM();
+    Node ni = nm->mkNode(kind::SELECT, node, i);
+    if (!d_equalityEngine.hasTerm(ni)) {
+      preRegisterTerm(ni);
+    }
 
-void TheoryArrays::checkPropagations(TNode a, TNode b) {
-  EqLists::const_iterator ita = d_equalities.find(a);
-  EqLists::const_iterator itb = d_equalities.find(b);
+    // Apply RIntro1 Rule
+    d_equalityEngine.addEquality(ni, v, d_true);
 
-  if(ita != d_equalities.end()) {
-    if(itb!= d_equalities.end()) {
-      // because b is the canonical representative
-      List<TNode>* eqsa = (*ita).second;
-      List<TNode>* eqsb = (*itb).second;
+    d_infoMap.addStore(node, node);
+    d_infoMap.addInStore(a, node);
 
-      for(List<TNode>::const_iterator it = eqsa->begin(); it!= eqsa->end(); ++it) {
-        Node eq = *it;
-        Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF);
-        if(find(eq[0])== find(eq[1])) {
-          d_prop_queue.push_back(eq);
-        }
-      }
-     eqsb->concat(eqsa);
+    checkStore(node);
+    break;
+  }
+  default:
+    // Variables etc
+    if (node.getType().isArray()) {
+      d_equalityEngine.addTriggerTerm(node);
     }
     else {
-      List<TNode>* eqsb = new List<TNode>(&d_backtracker);
-      List<TNode>* eqsa = (*ita).second;
-      d_equalities.insert(b, eqsb);
-      eqsb->concat(eqsa);
+      d_equalityEngine.addTerm(node);
     }
-  } else {
-    List<TNode>* eqsb = new List<TNode>(&d_backtracker);
-    d_equalities.insert(b, eqsb);
-    List<TNode>* eqsa = new List<TNode>(&d_backtracker);
-    d_equalities.insert(a, eqsa);
-    eqsb->concat(eqsa);
+    break;
   }
 }
 
 
-bool TheoryArrays::isNonLinear(TNode a) {
-  Assert(a.getType().isArray());
-  const CTNodeList* inst = d_infoMap.getInStores(find(a));
-  if(inst->size()<=1) {
-    return false;
-  }
-  return true;
-}
-
-bool TheoryArrays::isAxiom(TNode t1, TNode t2) {
-  Trace("arrays-axiom")<<"Arrays::isAxiom start "<<t1<<" = "<<t2<<"\n";
-  if(t1.getKind() == kind::SELECT) {
-    TNode a = t1[0];
-    TNode i = t1[1];
-
-    if(a.getKind() == kind::STORE) {
-      TNode b = a[0];
-      TNode j = a[1];
-      TNode v = a[2];
-      if(i == j && v == t2) {
-        Trace("arrays-axiom")<<"Arrays::isAxiom true\n";
-        return true;
+void TheoryArrays::propagate(Effort e)
+{
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
+  if (!d_conflict) {
+    for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+      TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+      Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
+      bool satValue;
+      Node normalized = Rewriter::rewrite(literal);
+      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
+        d_out->propagate(literal);
+      } else {
+        Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
+        Node negatedLiteral;
+        std::vector<TNode> assumptions;
+        if (normalized != d_false) {
+          negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+          assumptions.push_back(negatedLiteral);
+        }
+        explain(literal, assumptions);
+        d_conflictNode = mkAnd(assumptions);
+        d_conflict = true;
+        break;
       }
     }
   }
-  return false;
+
 }
 
 
-Node TheoryArrays::constructConflict(TNode diseq) {
-  Trace("arrays") << "arrays: begin constructConflict()" << endl;
-  Trace("arrays") << "arrays:   using diseq == " << diseq << endl;
+Node TheoryArrays::explain(TNode literal)
+{
+  ++d_numExplain;
+  Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
+  std::vector<TNode> assumptions;
+  explain(literal, assumptions);
+  return mkAnd(assumptions);
+}
+
 
-  // returns the reason the two terms are equal
-  Node explanation = d_cc.explain(diseq[0], diseq[1]);
+/////////////////////////////////////////////////////////////////////////////
+// SHARING
+/////////////////////////////////////////////////////////////////////////////
 
-  NodeBuilder<> nb(kind::AND);
 
-  if(explanation.getKind() == kind::EQUAL ||
-     explanation.getKind() == kind::IFF) {
-    // if the explanation is only one literal
-    if(!isAxiom(explanation[0], explanation[1]) &&
-       !isAxiom(explanation[1], explanation[0])) {
-      nb<<explanation;
-    }
+void TheoryArrays::addSharedTerm(TNode t) {
+  Debug("arrays::sharing") << spaces(getContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
+  d_equalityEngine.addTriggerTerm(t);
+  if (t.getType().isArray()) {
+    d_sharedArrays.insert(t,true);
   }
   else {
-    Assert(explanation.getKind() == kind::AND);
-    for(TNode::iterator i  = TNode(explanation).begin();
-        i != TNode(explanation).end(); i++) {
-      if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
-        nb<<*i;
-      }
-    }
+    d_sharedTerms = true;
   }
-
-  nb<<diseq.notNode();
-  Node conflict = nb;
-  Trace("arrays") << "conflict constructed : " << conflict << endl;
-  return conflict;
 }
 
-/*
-void TheoryArrays::addAtom(TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL);
-
-  TNode lhs = eq[0];
-  TNode rhs = eq[1];
-
-  appendToAtomList(find(lhs), rhs);
-  appendToAtomList(find(rhs), lhs);
-}
 
-void TheoryArrays::appendToAtomList(TNode a, TNode b) {
-  Assert(find(a) == a);
-
-  NodeTNodesMap::const_iterator it = d_atoms.find(a);
-  if(it != d_atoms.end()) {
-    (*it).second->push_back(b);
+EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
+  Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
+  if (d_equalityEngine.areEqual(a, b)) {
+    // The terms are implied to be equal
+    return EQUALITY_TRUE;
   }
-  else {
-   CTNodeList* list = new (true)CTNodeList(getContext());
-   list->push_back(b);
-   d_atoms[a] = list;
+  if (d_equalityEngine.areDisequal(a, b)) {
+    // The terms are implied to be dis-equal
+    return EQUALITY_FALSE;
   }
-
+  //TODO: can we be more precise sometimes?
+  return EQUALITY_UNKNOWN;
 }
-*/
 
-void TheoryArrays::addEq(TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-  TNode a = eq[0];
-  TNode b = eq[1];
-
-  // don't need to say find(a) because due to the structure of the lists it gets
-  // automatically added
-  appendToEqList(a, eq);
-  appendToEqList(b, eq);
-
-}
 
-void TheoryArrays::appendToEqList(TNode n, TNode eq) {
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-
-  EqLists::const_iterator it = d_equalities.find(n);
-  if(it == d_equalities.end()) {
-    List<TNode>* eqs = new List<TNode>(&d_backtracker);
-    eqs->append(eq);
-    d_equalities.insert(n, eqs);
-  } else {
-    List<TNode>* eqs = (*it).second;
-    eqs->append(eq);
+void TheoryArrays::computeCareGraph()
+{
+  if (d_sharedArrays.size() > 0) {
+    context::CDHashMap<TNode, bool, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+    for (; it1 != iend; ++it1) {
+      for (it2 = it1, ++it2; it2 != iend; ++it2) {
+        EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first);
+        if (eqStatusArr != EQUALITY_UNKNOWN) {
+          continue;
+        }
+        Assert(d_valuation.getEqualityStatus((*it1).first, (*it2).first) == EQUALITY_UNKNOWN);
+        addCarePair((*it1).first, (*it2).first);
+        ++d_numSharedArrayVarSplits;
+        return;
+      }
+    }
   }
-}
+  if (d_sharedTerms) {
 
-void TheoryArrays::addDiseq(TNode diseq) {
-  Assert(diseq.getKind() == kind::EQUAL ||
-         diseq.getKind() == kind::IFF);
-  TNode a = diseq[0];
-  TNode b = diseq[1];
+    vector< pair<TNode, TNode> > currentPairs;
 
-  appendToDiseqList(find(a), diseq);
-  appendToDiseqList(find(b), diseq);
+    // Go through the read terms and see if there are any to split on
+    unsigned size = d_reads.size();
+    for (unsigned i = 0; i < size; ++ i) {
+      TNode r1 = d_reads[i];
 
-}
+      for (unsigned j = i + 1; j < size; ++ j) {
+        TNode r2 = d_reads[j];
 
-void TheoryArrays::appendToDiseqList(TNode of, TNode eq) {
-  Trace("arrays") << "appending " << eq << endl
-              << "  to diseq list of " << of << endl;
-  Assert(eq.getKind() == kind::EQUAL ||
-         eq.getKind() == kind::IFF);
-
-  CNodeTNodesMap::iterator deq_i = d_disequalities.find(of);
-  CTNodeListAlloc* deq;
-  if(deq_i == d_disequalities.end()) {
-    deq = new(getContext()->getCMM()) CTNodeListAlloc(true, getContext(), false,
-                                             ContextMemoryAllocator<TNode>(getContext()->getCMM()));
-    d_disequalities.insertDataFromContextMemory(of, deq);
-  } else {
-    deq = (*deq_i).second;
-  }
+        Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checking reads " << r1 << " and " << r2 << std::endl;
 
-  deq->push_back(eq);
-}
+        // If the terms are already known to be equal, we are also in good shape
+        if (d_equalityEngine.areEqual(r1, r2)) {
+          Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equal, skipping" << std::endl;
+          continue;
+        }
 
+        if (r1[0] != r2[0]) {
+          // If arrays are known to be disequal, or cannot become equal, we can continue
+          if (d_equalityEngine.areDisequal(r1[0], r2[0]) ||
+              (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0]))) {
+            Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
+            continue;
+          }
+        }
 
-/**
- * Iterates through the indices of a and stores of b and checks if any new
- * Row lemmas need to be instantiated.
- */
-bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) {
-  Assert(a.getType().isArray());
-  Assert(b.getType().isArray());
+        TNode x = r1[1];
+        TNode y = r2[1];
 
-  if(d_RowAlreadyAdded.count(make_quad(a, b, i, j)) != 0 ||
-     d_RowAlreadyAdded.count(make_quad(b, a, i, j)) != 0 ) {
-    return true;
-  }
+        EqualityStatus eqStatus = getEqualityStatus(x, y);
 
-  return false;
-}
+        if (eqStatus != EQUALITY_UNKNOWN) {
+          Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): equality status known, skipping" << std::endl;
+          continue;
+        }
 
-bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) {
-  NodeManager* nm = NodeManager::currentNM();
-  Node aj = nm->mkNode(kind::SELECT, a, j);
-  Node bj = nm->mkNode(kind::SELECT, b, j);
+        if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+          Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
+          continue;
+        }
 
-  if(find(i) == find(j) || find(aj) == find(bj)) {
-    Trace("arrays") << "isRedundantInContext valid "
-                    << a << " " << b << " " << i << " " << j << endl;
-    checkRowForIndex(j, b); // why am i doing this?
-    checkRowForIndex(i, a);
-    return true;
-  }
-  Trace("arrays") << "isRedundantInContext " << a << endl
-                  << "isRedundantInContext " << b << endl
-                  << "isRedundantInContext " << i << endl
-                  << "isRedundantInContext " << j << endl;
-  Node ieqj = i.eqNode(j);
-  Node literal1 = Rewriter::rewrite(ieqj);
-  bool hasValue1, satValue1;
-  Node ff = nm->mkConst<bool>(false);
-  Node tt = nm->mkConst<bool>(true);
-  if (literal1 == ff) {
-    hasValue1 = true;
-    satValue1 = false;
-  } else if (literal1 == tt) {
-    hasValue1 = true;
-    satValue1 = true;
-  } else {
-    hasValue1 = (d_valuation.isSatLiteral(literal1) && d_valuation.hasSatValue(literal1, satValue1));
-  }
-  if (hasValue1) {
-    if (satValue1) {
-      Trace("arrays") << "isRedundantInContext returning, hasValue1 && satValue1" << endl;
-      return true;
-    }
-    Node ajeqbj = aj.eqNode(bj);
-    Node literal2 = Rewriter::rewrite(ajeqbj);
-    bool hasValue2, satValue2;
-    if (literal2 == ff) {
-      hasValue2 = true;
-      satValue2 = false;
-    } else if (literal2 == tt) {
-      hasValue2 = true;
-      satValue2 = true;
-    } else {
-      hasValue2 = (d_valuation.isSatLiteral(literal2) && d_valuation.hasSatValue(literal2, satValue2));
-    }
-    if (hasValue2) {
-      if (satValue2) {
-        Trace("arrays") << "isRedundantInContext returning, hasValue2 && satValue2" << endl;
-        return true;
+        // Get representative trigger terms
+        TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x);
+        TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y);
+
+        EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
+        switch (eqStatusDomain) {
+          case EQUALITY_FALSE_AND_PROPAGATED:
+          case EQUALITY_FALSE:
+            continue;
+            break;
+          case EQUALITY_TRUE_AND_PROPAGATED:
+          case EQUALITY_TRUE:
+            // Should have been propagated to us
+            Assert(false);
+            continue;
+            break;
+          case EQUALITY_FALSE_IN_MODEL:
+            Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model, skipping" << std::endl;
+            continue;
+            break;
+          default:
+            break;
+        }
+
+        // Otherwise, add this pair
+        Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl;
+        addCarePair(x_shared, y_shared);
       }
-      // conflict
-      Assert(!satValue1 && !satValue2);
-      Assert(literal1.getKind() == kind::EQUAL && literal2.getKind() == kind::EQUAL);
-      NodeBuilder<2> nb(kind::AND);
-      //literal1 = areDisequal(literal1[0], literal1[1]);
-      //literal2 = areDisequal(literal2[0], literal2[1]);
-      Assert(!literal1.isNull() && !literal2.isNull());
-      nb << literal1.notNode() << literal2.notNode();
-      literal1 = nb;
-      d_conflict = Node::null();
-      d_out->conflict(literal1);
-      Trace("arrays") << "TheoryArrays::isRedundantInContext() "
-                      << "conflict via lemma: " << literal1 << endl;
-      return true;
     }
   }
-  if(alreadyAddedRow(a, b, i, j)) {
-    Trace("arrays") << "isRedundantInContext already added "
-                    << a << " " << b << " " << i << " " << j << endl;
-    return true;
-  }
-  return false;
 }
 
-TNode TheoryArrays::areDisequal(TNode a, TNode b) {
-  Trace("arrays-prop") << "Arrays::areDisequal " << a << " " << b << "\n";
-
-  a = find(a);
-  b = find(b);
-
-  CNodeTNodesMap::const_iterator it = d_disequalities.find(a);
-  if(it!= d_disequalities.end()) {
-    CTNodeListAlloc::const_iterator i = (*it).second->begin();
-    for( ; i!= (*it).second->end(); i++) {
-      Trace("arrays-prop") << "   " << *i << "\n";
-      TNode s = (*i)[0];
-      TNode t = (*i)[1];
-
-      Assert(find(s) == a || find(t) == a);
-      TNode sp, tp;
-      if(find(t) == a) {
-        sp = find(t);
-        tp = find(s);
-      }
-      else {
-        sp = find(s);
-        tp = find(t);
-      }
 
-      if(tp == b) {
-        return *i;
-      }
+/////////////////////////////////////////////////////////////////////////////
+// MODEL GENERATION
+/////////////////////////////////////////////////////////////////////////////
 
-    }
-  }
-  Trace("arrays-prop") << "    not disequal \n";
-  return TNode::null();
-}
 
-bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) {
-  Trace("arrays-prop")<<"Arrays::propagateFromRow "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
+Node TheoryArrays::getValue(TNode n)
+{
+  // TODO: Implement this
+  NodeManager* nodeManager = NodeManager::currentNM();
 
-  NodeManager* nm = NodeManager::currentNM();
-  Node aj = nm->mkNode(kind::SELECT, a, j);
-  Node bj = nm->mkNode(kind::SELECT, b, j);
+  switch(n.getKind()) {
 
-  Node eq_aj_bj = nm->mkNode(kind::EQUAL,aj, bj);
-  Node eq_ij = nm->mkNode(kind::EQUAL, i, j);
-
-  // first check if the current context implies NOT (i = j)
-  // in which case we can propagate a[j] = b[j]
-  // FIXME: does i = j need to be a SAT literal or can we propagate anyway?
-
-  // if it does not have an atom we must add the lemma (do we?!)
-  if(d_atoms.count(eq_aj_bj) != 0 ||
-     d_atoms.count(nm->mkNode(kind::EQUAL, bj, aj))!=0) {
-    Node diseq = areDisequal(i, j);
-    // check if the current context implies that (NOT i = j)
-    if(diseq != TNode::null()) {
-      // if it's unassigned
-      Trace("arrays-prop")<<"satValue "<<d_valuation.getSatValue(eq_aj_bj).isNull();
-      if(d_valuation.getSatValue(eq_aj_bj).isNull()) {
-        d_out->propagate(eq_aj_bj);
-        ++d_numProp;
-        // save explanation
-        d_explanations.insert(eq_aj_bj,std::make_pair(eq_ij, diseq));
-        return true;
-      }
+  case kind::VARIABLE:
+    Unhandled(kind::VARIABLE);
 
-    }
-  }
+  case kind::EQUAL: // 2 args
+    return nodeManager->
+      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
 
-  // now check if the current context implies NOT a[j] = b[j]
-  // in which case we propagate i = j
+  default:
+    Unhandled(n.getKind());
+  }
+}
 
-  // we can't propagate if it does not have an atom
-  if(d_atoms.count(eq_ij) != 0 || d_atoms.count(nm->mkNode(kind::EQUAL, j, i))!= 0) {
 
-    Node diseq = areDisequal(aj, bj);
-    Assert(TNode::null() == Node::null());
+/////////////////////////////////////////////////////////////////////////////
+// NOTIFICATIONS
+/////////////////////////////////////////////////////////////////////////////
 
-    if(diseq != TNode::null()) {
-      if(d_valuation.getSatValue(eq_ij) == Node::null()) {
-        d_out->propagate(eq_ij);
-        ++d_numProp;
-        // save explanation
-        d_explanations.insert(eq_ij, std::make_pair(eq_aj_bj,diseq));
-        return true;
-      }
-    }
-  }
 
-  Trace("arrays-prop")<<"Arrays::propagateFromRow no prop \n";
-  return false;
+void TheoryArrays::presolve()
+{
+  Trace("arrays")<<"Presolving \n";
 }
 
-Node TheoryArrays::explain(TNode n) {
 
+/////////////////////////////////////////////////////////////////////////////
+// MAIN SOLVER
+/////////////////////////////////////////////////////////////////////////////
 
-  Trace("arrays")<<"Arrays::explain start for "<<n<<"\n";
-  ++d_numExplain;
-
-  Assert(n.getKind()==kind::EQUAL);
 
-  Node explanation = d_cc.explain(n[0], n[1]);
+void TheoryArrays::check(Effort e) {
+  TimerStat::CodeTimer codeTimer(d_checkTimer);
 
-  NodeBuilder<> nb(kind::AND);
+  while (!done() && !d_conflict) 
+  {
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+
+    Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
+
+    // If the assertion doesn't have a literal, it's a shared equality
+    Assert(assertion.isPreregistered ||
+           ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
+            (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
+             d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+
+    // Do the work
+    switch (fact.getKind()) {
+      case kind::EQUAL:
+        d_equalityEngine.addEquality(fact[0], fact[1], fact);
+        break;
+      case kind::SELECT:
+        d_equalityEngine.addPredicate(fact, true, fact);
+        break;
+      case kind::NOT:
+        if (fact[0].getKind() == kind::SELECT) {
+          d_equalityEngine.addPredicate(fact[0], false, fact);
+        } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) {
+          // Assert the dis-equality
+          d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+
+          // Apply ArrDiseq Rule if diseq is between arrays
+          if(fact[0][0].getType().isArray()) {
+            NodeManager* nm = NodeManager::currentNM();
+            TypeNode indexType = fact[0][0].getType()[0];
+            TNode k;
+            std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
+            if (it == d_diseqCache.end()) {
+              Node newk = nm->mkVar(indexType);
+	      Dump.declareVar(newk.toExpr(),
+                              "an extensional lemma index variable from the theory of arrays");
+              d_diseqCache[fact] = newk;
+              k = newk;
+            }
+            else {
+              k = (*it).second;
+            }
 
-  if(explanation.getKind() == kind::EQUAL ||
-     explanation.getKind() == kind::IFF) {
-    // if the explanation is only one literal
-    if(!isAxiom(explanation[0], explanation[1]) &&
-       !isAxiom(explanation[1], explanation[0])) {
-      nb<<explanation;
+            Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
+            Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
+            if (!d_equalityEngine.hasTerm(ak)) {
+              preRegisterTerm(ak);
+            }
+            if (!d_equalityEngine.hasTerm(bk)) {
+              preRegisterTerm(bk);
+            }
+            d_equalityEngine.addDisequality(ak, bk, fact);
+            Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n";
+            ++d_numExt;
+          }
+        }
+        break;
+      default:
+        Unreachable();
     }
   }
+
+  // If in conflict, output the conflict
+  if (d_conflict) {
+    Debug("arrays") << spaces(getContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
+    d_out->conflict(d_conflictNode);
+  }
   else {
-    Assert(explanation.getKind() == kind::AND);
-    for(TNode::iterator i  = TNode(explanation).begin();
-        i != TNode(explanation).end(); i++) {
-      if(!isAxiom((*i)[0], (*i)[1]) && !isAxiom((*i)[1], (*i)[0])) {
-        nb<<*i;
-      }
+    // Otherwise we propagate
+    propagate(e);
+
+    if(!d_eagerLemmas && fullEffort(e)) {
+      // generate the lemmas on the worklist
+      Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+      dischargeLemmas();
     }
   }
-  Node reason = nb;
-
-  return reason;
-
-  /*
-  context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator
-                                                    it = d_explanations.find(n);
-  Assert(it!= d_explanations.end());
-  TNode diseq = (*it).second.second;
-  TNode s = diseq[0];
-  TNode t = diseq[1];
 
-  TNode eq = (*it).second.first;
-  TNode a = eq[0];
-  TNode b = eq[1];
+  Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::check(): done" << endl;
+}
 
-  Assert ((find(a) == find(s) && find(b) == find(t)) ||
-          (find(a) == find(t) && find(b) == find(s)));
 
+Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
+{
+  Assert(conjunctions.size() > 0);
 
-  if(find(a) == find(t)) {
-    TNode temp = t;
-    t = s;
-    s = temp;
-  }
+  std::set<TNode> all;
+  std::set<TNode> explained;
 
-  // construct the explanation
+  unsigned i = 0;
+  TNode t;
+  for (; i < conjunctions.size(); ++i) {
+    t = conjunctions[i];
 
-  NodeBuilder<> nb(kind::AND);
-  Node explanation1 = d_cc.explain(a, s);
-  Node explanation2 = d_cc.explain(b, t);
+    // Remove true node - represents axiomatically true assertion
+    if (t == d_true) continue;
 
-  if(explanation1.getKind() == kind::AND) {
-    for(TNode::iterator i= TNode(explanation1).begin();
-        i!=TNode(explanation1).end(); ++i) {
-      nb << *i;
+    // Expand explanation resulting from propagating a ROW lemma
+    if (t.getKind() == kind::OR) {
+      if ((explained.find(t) == explained.end())) {
+        Assert(t[1].getKind() == kind::EQUAL);
+        d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions);
+        explained.insert(t);
+      }
+      continue;
     }
-  } else {
-    Assert(explanation1.getKind() == kind::EQUAL ||
-           explanation1.getKind() == kind::IFF);
-    nb << explanation1;
+    all.insert(t);
   }
 
-  if(explanation2.getKind() == kind::AND) {
-    for(TNode::iterator i= TNode(explanation2).begin();
-        i!=TNode(explanation2).end(); ++i) {
-      nb << *i;
-    }
-  } else {
-    Assert(explanation2.getKind() == kind::EQUAL ||
-           explanation2.getKind() == kind::IFF);
-    nb << explanation2;
+  Assert(all.size() > 0);
+  if (all.size() == 1) {
+    // All the same, or just one
+    return *(all.begin());
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
   }
 
-  nb << diseq;
-  Node reason = nb;
-  d_out->explanation(reason);
-  Trace("arrays")<<"explanation "<< reason<<" done \n";
-  */
+  return conjunction;
 }
 
-void TheoryArrays::checkRowLemmas(TNode a, TNode b) {
 
-  Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
-  if(Trace.isOn("arrays-crl"))
-    d_infoMap.getInfo(a)->print();
-  Trace("arrays-crl")<<"  ------------  and "<<b<<"\n";
-  if(Trace.isOn("arrays-crl"))
-    d_infoMap.getInfo(b)->print();
+void TheoryArrays::setNonLinear(TNode a)
+{
+  if (d_infoMap.isNonLinear(a)) return;
+
+  Trace("arrays") << spaces(getContext()->getLevel()) << "Arrays::setNonLinear (" << a << ")\n";
+  d_infoMap.setNonLinear(a);
+  ++d_numNonLinear;
 
   List<TNode>* i_a = d_infoMap.getIndices(a);
-  const CTNodeList* st_b = d_infoMap.getStores(b);
-  const CTNodeList* inst_b = d_infoMap.getInStores(b);
+  const CTNodeList* st_a = d_infoMap.getStores(a);
+  const CTNodeList* inst_a = d_infoMap.getInStores(a);
 
-  List<TNode>::const_iterator it = i_a->begin();
-  CTNodeList::const_iterator its;
+  CTNodeList::const_iterator it = st_a->begin();
 
-  for( ; it != i_a->end(); it++ ) {
-    TNode i = *it;
-    its = st_b->begin();
-    for ( ; its != st_b->end(); its++) {
-      TNode store = *its;
+  // Propagate non-linearity down chain of stores
+  for(; it!= st_a->end(); ++it) {
+    TNode store = *it;
+    Assert(store.getKind()==kind::STORE);
+    setNonLinear(store[0]);
+  }
+
+  // Instantiate ROW lemmas that were ignored before
+  List<TNode>::const_iterator itl = i_a->begin();
+  RowLemmaType lem;
+  for(; itl != i_a->end(); ++itl ) {
+    TNode i = *itl;
+    it = inst_a->begin();
+    for ( ; it !=inst_a->end(); ++it) {
+      TNode store = *it;
       Assert(store.getKind() == kind::STORE);
       TNode j = store[1];
       TNode c = store[0];
-
-      if(  !isRedundantRowLemma(store, c, j, i)){
-         //&&!propagateFromRow(store, c, j, i)) {
-        queueRowLemma(store, c, j, i);
-      }
+      lem = make_quad(store, c, j, i);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::setNonLinear ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(lem);
     }
-
   }
 
-  it = i_a->begin();
+}
 
-  for( ; it != i_a->end(); it++ ) {
-    TNode i = *it;
-    its = inst_b->begin();
-    for ( ; its !=inst_b->end(); its++) {
-      TNode store = *its;
-      Assert(store.getKind() == kind::STORE);
-      TNode j = store[1];
-      TNode c = store[0];
 
-      if (   isNonLinear(c)
-          &&!isRedundantRowLemma(store, c, j, i)){
-          //&&!propagateFromRow(store, c, j, i)) {
-        queueRowLemma(store, c, j, i);
+void TheoryArrays::mergeArrays(TNode a, TNode b)
+{
+  // Note: a is the new representative
+  Assert(a.getType().isArray() && b.getType().isArray());
+
+  if (d_mergeInProgress) {
+    // Nested call to mergeArrays, just push on the queue and return
+    d_mergeQueue.push(a.eqNode(b));
+    return;
+  }
+
+  d_mergeInProgress = true;
+
+  Node n;
+  while (true) {
+    if (d_useNonLinearOpt) {
+      bool aNL = d_infoMap.isNonLinear(a);
+      bool bNL = d_infoMap.isNonLinear(b);
+      if (aNL) {
+        if (bNL) {
+          // already both marked as non-linear - no need to do anything
+        }
+        else {
+          // Set b to be non-linear
+          setNonLinear(b);
+        }
       }
+      else {
+        if (bNL) {
+          // Set a to be non-linear
+          setNonLinear(a);
+        }
+        else {
+          // Check for new non-linear arrays
+          const CTNodeList* astores = d_infoMap.getStores(a);
+          const CTNodeList* bstores = d_infoMap.getStores(a);
+          Assert(astores->size() <= 1 && bstores->size() <= 1);
+          if (astores->size() > 0 && bstores->size() > 0) {
+            setNonLinear(a);
+            setNonLinear(b);
+          }
+        }
+      }
+    }
+
+    d_mayEqualEqualityEngine.addEquality(a, b, d_true);
 
+    checkRowLemmas(a,b);
+    checkRowLemmas(b,a);
+
+    // merge info adds the list of the 2nd argument to the first
+    d_infoMap.mergeInfo(a, b);
+
+    // If no more to do, break
+    if (d_conflict || d_mergeQueue.empty()) {
+      break;
     }
-  }
 
-  Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
+    // Otherwise, prepare for next iteration
+    n = d_mergeQueue.front();
+    a = n[0];
+    b = n[1];
+    d_mergeQueue.pop();
+  }
+  d_mergeInProgress = false;
 }
 
-/**
- * Adds a new Row lemma of the form i = j OR a[j] = b[j] if i and j are not the
- * same and a and b are also not identical.
- *
- */
-
-inline void TheoryArrays::addRowLemma(TNode a, TNode b, TNode i, TNode j) {
- Assert(a.getType().isArray());
- Assert(b.getType().isArray());
 
- // construct lemma
- NodeManager* nm = NodeManager::currentNM();
- Node aj = nm->mkNode(kind::SELECT, a, j);
- Node bj = nm->mkNode(kind::SELECT, b, j);
- Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
- Node eq2 = nm->mkNode(kind::EQUAL, i, j);
- Node lem = nm->mkNode(kind::OR, eq2, eq1);
+void TheoryArrays::checkStore(TNode a) {
+  Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
 
+  if(Trace.isOn("arrays-cri")) {
+    d_infoMap.getInfo(a)->print();
+  }
+  Assert(a.getType().isArray());
+  Assert(a.getKind()==kind::STORE);
+  TNode b = a[0];
+  TNode i = a[1];
 
+  TNode brep = d_equalityEngine.getRepresentative(b);
 
- Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
- d_RowAlreadyAdded.insert(make_quad(a,b,i,j));
- d_out->lemma(lem);
- ++d_numRow;
+  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(brep)) {
+    List<TNode>* js = d_infoMap.getIndices(brep);
+    List<TNode>::const_iterator it = js->begin();
 
+    RowLemmaType lem;
+    for(; it!= js->end(); ++it) {
+      TNode j = *it;
+      if (i == j) continue;
+      lem = make_quad(a,b,i,j);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
+      queueRowLemma(lem);
+    }
+  }
 }
 
 
-/**
- * Because a is now being read at position i check if new lemmas can be
- * instantiated for all store terms equal to a and all store terms of the form
- * store(a _ _ )
- */
-void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
+void TheoryArrays::checkRowForIndex(TNode i, TNode a)
+{
   Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
   Trace("arrays-cri")<<"                   index "<<i<<"\n";
 
@@ -1057,107 +954,207 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) {
     d_infoMap.getInfo(a)->print();
   }
   Assert(a.getType().isArray());
+  Assert(d_equalityEngine.getRepresentative(a) == a);
 
   const CTNodeList* stores = d_infoMap.getStores(a);
   const CTNodeList* instores = d_infoMap.getInStores(a);
   CTNodeList::const_iterator it = stores->begin();
+  RowLemmaType lem;
 
-  for(; it!= stores->end(); it++) {
+  for(; it!= stores->end(); ++it) {
     TNode store = *it;
     Assert(store.getKind()==kind::STORE);
     TNode j = store[1];
-    //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
-    if(!isRedundantRowLemma(store, store[0], j, i)) {
-      //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
-      queueRowLemma(store, store[0], j, i);
-    }
+    if (i == j) continue;
+    lem = make_quad(store, store[0], j, i);
+    Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n";
+    queueRowLemma(lem);
   }
 
-  it = instores->begin();
-  for(; it!= instores->end(); it++) {
-    TNode instore = *it;
-    Assert(instore.getKind()==kind::STORE);
-    TNode j = instore[1];
-    //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
-    if(!isRedundantRowLemma(instore, instore[0], j, i)) {
-      //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
-      queueRowLemma(instore, instore[0], j, i);
+  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(a)) {
+    it = instores->begin();
+    for(; it!= instores->end(); ++it) {
+      TNode instore = *it;
+      Assert(instore.getKind()==kind::STORE);
+      TNode j = instore[1];
+      if (i == j) continue;
+      lem = make_quad(instore, instore[0], j, i);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(lem);
     }
   }
-
 }
 
 
-void TheoryArrays::checkStore(TNode a) {
-  Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
-
-  if(Trace.isOn("arrays-cri")) {
+// a just became equal to b
+// look for new ROW lemmas
+void TheoryArrays::checkRowLemmas(TNode a, TNode b)
+{
+  Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
+  if(Trace.isOn("arrays-crl"))
     d_infoMap.getInfo(a)->print();
-  }
-  Assert(a.getType().isArray());
-  Assert(a.getKind()==kind::STORE);
-  TNode b = a[0];
-  TNode i = a[1];
+  Trace("arrays-crl")<<"  ------------  and "<<b<<"\n";
+  if(Trace.isOn("arrays-crl"))
+    d_infoMap.getInfo(b)->print();
 
-  List<TNode>* js = d_infoMap.getIndices(b);
-  List<TNode>::const_iterator it = js->begin();
+  List<TNode>* i_a = d_infoMap.getIndices(a);
+  const CTNodeList* st_b = d_infoMap.getStores(b);
+  const CTNodeList* inst_b = d_infoMap.getInStores(b);
+
+  List<TNode>::const_iterator it = i_a->begin();
+  CTNodeList::const_iterator its;
 
-  for(; it!= js->end(); it++) {
-    TNode j = *it;
+  RowLemmaType lem;
 
-    if(!isRedundantRowLemma(a, b, i, j)) {
-      //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n";
-      queueRowLemma(a,b,i,j);
+  for( ; it != i_a->end(); ++it ) {
+    TNode i = *it;
+    its = st_b->begin();
+    for ( ; its != st_b->end(); ++its) {
+      TNode store = *its;
+      Assert(store.getKind() == kind::STORE);
+      TNode j = store[1];
+      TNode c = store[0];
+      lem = make_quad(store, c, j, i);
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+      queueRowLemma(lem);
     }
   }
 
+  if (!d_useNonLinearOpt || d_infoMap.isNonLinear(b)) {
+    for(it = i_a->begin() ; it != i_a->end(); ++it ) {
+      TNode i = *it;
+      its = inst_b->begin();
+      for ( ; its !=inst_b->end(); ++its) {
+        TNode store = *its;
+        Assert(store.getKind() == kind::STORE);
+        TNode j = store[1];
+        TNode c = store[0];
+        lem = make_quad(store, c, j, i);
+        Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::checkRowLemmas ("<<store<<", "<<c<<", "<<j<<", "<<i<<")\n";
+        queueRowLemma(lem);
+      }
+    }
+  }
+  Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
-inline void TheoryArrays::queueExtLemma(TNode a, TNode b) {
+
+void TheoryArrays::queueRowLemma(RowLemmaType lem)
+{
+  if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
+    return;
+  }
+  TNode a = lem.first;
+  TNode b = lem.second;
+  TNode i = lem.third;
+  TNode j = lem.fourth;
   Assert(a.getType().isArray() && b.getType().isArray());
+  if (d_equalityEngine.areEqual(a,b) ||
+      d_equalityEngine.areEqual(i,j)) {
+    return;
+  }
 
-  d_extQueue.insert(make_pair(a,b));
-}
+  NodeManager* nm = NodeManager::currentNM();
 
-void TheoryArrays::queueRowLemma(TNode a, TNode b, TNode i, TNode j) {
-  Assert(a.getType().isArray() && b.getType().isArray());
-//if(!isRedundantInContext(a,b,i,j)) {
-  d_RowQueue.insert(make_quad(a, b, i, j));
-}
+  Node aj = nm->mkNode(kind::SELECT, a, j);
+  Node bj = nm->mkNode(kind::SELECT, b, j);
+  if (!d_equalityEngine.hasTerm(aj)) {
+    preRegisterTerm(aj);
+  }
+  if (!d_equalityEngine.hasTerm(bj)) {
+    preRegisterTerm(bj);
+  }
+
+  if (d_equalityEngine.areEqual(aj,bj)) {
+    return;
+  }
+
+  if (d_useArrTable) {
+    Node tableEntry = nm->mkNode(kind::ARR_TABLE_FUN, a, b, i, j);
+    if (d_equalityEngine.getSize(tableEntry) != 1) {
+      return;
+    }
+  }
 
-/**
-* Adds a new Ext lemma of the form
-*    a = b OR a[k]!=b[k], for a new variable k
-*/
+  //Propagation
+  if (d_propagateLemmas) {
+    if (d_equalityEngine.areDisequal(i,j)) {
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
+      Node reason = nm->mkNode(kind::OR, aj.eqNode(bj), i.eqNode(j));
+      d_permRef.push_back(reason);
+      d_equalityEngine.addEquality(aj, bj, reason);
+      ++d_numProp;
+      return;
+    }
+    if (d_equalityEngine.areDisequal(aj,bj)) {
+      Trace("arrays-lem") << spaces(getContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
+      Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj));
+      d_permRef.push_back(reason);
+      d_equalityEngine.addEquality(i, j, reason);
+      ++d_numProp;
+      return;
+    }
+  }
 
-inline void TheoryArrays::addExtLemma(TNode a, TNode b) {
- Assert(a.getType().isArray());
- Assert(b.getType().isArray());
+  // TODO: maybe add triggers here
 
- Trace("arrays-cle")<<"Arrays::checkExtLemmas "<<a<<" \n";
- Trace("arrays-cle")<<"                   and "<<b<<" \n";
+  if (d_eagerLemmas) {
+    Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
+    Node eq2 = nm->mkNode(kind::EQUAL, i, j);
+    Node lemma = nm->mkNode(kind::OR, eq2, eq1);
+    Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma<<"\n";
+    d_RowAlreadyAdded.insert(lem);
+    d_out->lemma(lemma);
+    ++d_numRow;
+  }
+  else {
+    d_RowQueue.push(lem);
+  }
+}
 
 
- if(   d_extAlreadyAdded.count(make_pair(a, b)) == 0
-    && d_extAlreadyAdded.count(make_pair(b, a)) == 0) {
+void TheoryArrays::dischargeLemmas()
+{
+  size_t sz = d_RowQueue.size();
+  for (unsigned count = 0; count < sz; ++count) {
+    RowLemmaType l = d_RowQueue.front();
+    d_RowQueue.pop();
+    if (d_RowAlreadyAdded.count(l) != 0) {
+      continue;
+    }
 
-   NodeManager* nm = NodeManager::currentNM();
-   TypeNode ixType = a.getType()[0];
-   Node k = nm->mkVar(ixType);
-   Dump.declareVar(k.toExpr(), "an extensional lemma index variable from the theory of arrays");
-   Node eq = nm->mkNode(kind::EQUAL, a, b);
-   Node ak = nm->mkNode(kind::SELECT, a, k);
-   Node bk = nm->mkNode(kind::SELECT, b, k);
-   Node neq = nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, ak, bk));
-   Node lem = nm->mkNode(kind::OR, eq, neq);
+    TNode a = l.first;
+    TNode b = l.second;
+    TNode i = l.third;
+    TNode j = l.fourth;
+    Assert(a.getType().isArray() && b.getType().isArray());
+
+    NodeManager* nm = NodeManager::currentNM();
+    Node aj = nm->mkNode(kind::SELECT, a, j);
+    Node bj = nm->mkNode(kind::SELECT, b, j);
+
+    // Check for redundant lemma
+    // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
+    if (d_equalityEngine.areEqual(i,j) ||
+        d_equalityEngine.areEqual(a,b) ||
+        d_equalityEngine.areEqual(aj,bj)) {
+      d_RowQueue.push(l);
+      continue;
+    }
 
-   Trace("arrays-lem")<<"Arrays::addExtLemma "<<lem<<"\n";
-   d_extAlreadyAdded.insert(make_pair(a,b));
-   d_out->lemma(lem);
-   ++d_numExt;
-   return;
- }
+    // construct lemma
+    Node eq1 = nm->mkNode(kind::EQUAL, aj, bj);
+    Node eq2 = nm->mkNode(kind::EQUAL, i, j);
+    Node lem = nm->mkNode(kind::OR, eq2, eq1);
 
- Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n";
+    Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";
+    d_RowAlreadyAdded.insert(l);
+    d_out->lemma(lem);
+    ++d_numRow;
+  }
 }
 
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index dcae47dc7..12dbd771d 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -2,7 +2,7 @@
 /*! \file theory_arrays.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: lianah
  ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
@@ -22,17 +22,12 @@
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 
 #include "theory/theory.h"
-#include "theory/arrays/union_find.h"
-#include "util/congruence_closure.h"
 #include "theory/arrays/array_info.h"
-#include "util/hash.h"
-#include "util/ntuple.h"
 #include "util/stats.h"
-#include "util/backtrackable.h"
-#include "theory/arrays/static_fact_manager.h"
-
-#include <iostream>
-#include <map>
+#include "theory/uf/equality_engine.h"
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
 
 namespace CVC4 {
 namespace theory {
@@ -87,417 +82,237 @@ namespace arrays {
  *  check. Ext lemmas are stored in a cache to prevent instantiating essentially
  *  the same lemma multiple times.
  */
-class TheoryArrays : public Theory {
 
-private:
+static inline std::string spaces(int level)
+{
+  std::string indentStr(level, ' ');
+  return indentStr;
+}
 
+class TheoryArrays : public Theory {
 
-  class CongruenceChannel {
-    TheoryArrays* d_arrays;
+  /////////////////////////////////////////////////////////////////////////////
+  // MISC
+  /////////////////////////////////////////////////////////////////////////////
 
-  public:
-    CongruenceChannel(TheoryArrays* arrays) : d_arrays(arrays) {}
-    void notifyCongruent(TNode a, TNode b) {
-      d_arrays->notifyCongruent(a, b);
-    }
-  }; /* class CongruenceChannel*/
-  friend class CongruenceChannel;
+  private:
 
-  /**
-   * Output channel connected to the congruence closure module.
-   */
-  CongruenceChannel d_ccChannel;
+  /** True node for predicates = true */
+  Node d_true;
 
-  /**
-   * Instance of the congruence closure module.
-   */
-  CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_1
-                                 (kind::SELECT)> d_cc;
+  /** True node for predicates = false */
+  Node d_false;
 
-  /**
-   * (Temporary) fact manager for preprocessing - eventually handle this with
-   * something more standard (like congruence closure module)
-   */
-  StaticFactManager d_staticFactManager;
+  // Statistics
 
-  /**
-   * Cache for proprocessing of atoms.
-   */
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-  NodeMap d_ppCache;
+  /** number of Row lemmas */
+  IntStat d_numRow;
+  /** number of Ext lemmas */
+  IntStat d_numExt;
+  /** number of propagations */
+  IntStat d_numProp;
+  /** number of explanations */
+  IntStat d_numExplain;
+  /** calls to non-linear */
+  IntStat d_numNonLinear;
+  /** splits on array variables */
+  IntStat d_numSharedArrayVarSplits;
+  /** time spent in check() */
+  TimerStat d_checkTimer;
 
-  /**
-   * Union find for storing the equalities.
-   */
+  public:
 
-  UnionFind<Node, NodeHashFunction> d_unionFind;
+  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
+  ~TheoryArrays();
 
-  Backtracker<TNode> d_backtracker;
+  std::string identify() const { return std::string("TheoryArrays"); }
 
+  /////////////////////////////////////////////////////////////////////////////
+  // PREPROCESSING
+  /////////////////////////////////////////////////////////////////////////////
 
-  /**
-   * Context dependent map from a congruence class canonical representative of
-   * type array to an Info pointer that keeps track of information useful to axiom
-   * instantiation
-   */
+  private:
 
-  ArrayInfo d_infoMap;
+  // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
+  class PPNotifyClass {
+  public:
+    bool notify(TNode propagation) { return true; }
+    void notify(TNode t1, TNode t2) { }
+  };
 
-  /**
-   * Received a notification from the congruence closure algorithm that the two
-   * nodes a and b have become congruent.
-   */
+  /** The notify class for d_ppEqualityEngine */
+  PPNotifyClass d_ppNotify;
 
-  void notifyCongruent(TNode a, TNode b);
+  /** Equaltity engine */
+  uf::EqualityEngine<PPNotifyClass> d_ppEqualityEngine;
 
+  // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine
+  context::CDList<Node> d_ppFacts;
 
-  typedef context::CDChunkList<TNode> CTNodeListAlloc;
-  typedef context::CDHashMap<Node, CTNodeListAlloc*, NodeHashFunction> CNodeTNodesMap;
-  typedef context::CDHashMap<TNode, List<TNode>*, TNodeHashFunction > EqLists;
+  Node preprocessTerm(TNode term);
+  Node recursivePreprocessTerm(TNode term);
 
+  public:
 
-  typedef __gnu_cxx::hash_map<TNode, CTNodeList*, TNodeHashFunction> NodeTNodesMap;
-  /**
-   * List of all disequalities this theory has seen. Maintains the invariant that
-   * if a is in the disequality list of b, then b is in that of a. FIXME? make non context dep map
-   * */
-  CNodeTNodesMap d_disequalities;
-  EqLists d_equalities;
-  context::CDList<TNode> d_prop_queue;
+  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  Node ppRewrite(TNode atom);
 
-  void checkPropagations(TNode a, TNode b);
+  /////////////////////////////////////////////////////////////////////////////
+  // T-PROPAGATION / REGISTRATION
+  /////////////////////////////////////////////////////////////////////////////
 
-  /** List of all atoms the SAT solver knows about and are candidates for
-   *  propagation. */
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_atoms;
+  private:
 
-  /** List of disequalities needed to construct explanations for propagated
-   * row lemmas */
+  /** Literals to propagate */
+  context::CDList<Node> d_literalsToPropagate;
 
-  context::CDHashMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction> d_explanations;
+  /** Index of the next literal to propagate */
+  context::CDO<unsigned> d_literalsToPropagateIndex;
 
-  /**
-   * stores the conflicting disequality (still need to call construct
-   * conflict to get the actual explanation)
-   */
-  Node d_conflict;
+  /** Should be called to propagate the literal.  */
+  bool propagate(TNode literal);
 
-  typedef context::CDList< quad<TNode, TNode, TNode, TNode > > QuadCDList;
+  /** Explain why this literal is true by adding assumptions */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
 
+  public:
 
-  /**
-   * Ext lemma workslist that stores extensionality lemmas that still need to be added
-   */
-  std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extQueue;
+  void preRegisterTerm(TNode n);
+  void propagate(Effort e);
+  Node explain(TNode n);
 
-  /**
-   * Row Lemma worklist, stores lemmas that can still be added to the SAT solver
-   * to be emptied during full effort check
-   */
-  std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowQueue;
+  /////////////////////////////////////////////////////////////////////////////
+  // SHARING
+  /////////////////////////////////////////////////////////////////////////////
 
-  /**
-   * Extensionality lemma cache which stores the array pair (a,b) for which
-   * a lemma of the form (a = b OR a[k]!= b[k]) has been added to the SAT solver.
-   */
-  std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> d_extAlreadyAdded;
+  private:
 
-  /**
-   * Read-over-write lemma cache storing a quadruple (a,b,i,j) for which a
-   * the lemma (i = j OR a[j] = b[j]) has been added to the SAT solver. Needed
-   * to prevent infinite recursion in addRowLemma.
-   */
-  std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > d_RowAlreadyAdded;
+  class MayEqualNotifyClass {
+  public:
+    bool notify(TNode propagation) { return true; }
+    void notify(TNode t1, TNode t2) { }
+  };
 
-  /*
-   * Congruence helper methods
-   */
+  /** The notify class for d_mayEqualEqualityEngine */
+  MayEqualNotifyClass d_mayEqualNotify;
 
-  void addDiseq(TNode diseq);
-  void addEq(TNode eq);
+  /** Equaltity engine for determining if two arrays might be equal */
+  uf::EqualityEngine<MayEqualNotifyClass> d_mayEqualEqualityEngine;
 
-  void appendToDiseqList(TNode of, TNode eq);
-  void appendToEqList(TNode a, TNode b);
-  Node constructConflict(TNode diseq);
+  public:
 
-  /**
-   * Merges two congruence classes in the internal union-find and checks for a
-   * conflict.
-   */
+  void addSharedTerm(TNode t);
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+  void computeCareGraph();
+  bool isShared(TNode t)
+    { return (d_sharedArrays.find(t) != d_sharedArrays.end()); }
 
-  void merge(TNode a, TNode b);
-  inline TNode find(TNode a);
-  inline TNode debugFind(TNode a) const;
 
-  inline void setCanon(TNode a, TNode b);
+  /////////////////////////////////////////////////////////////////////////////
+  // MODEL GENERATION
+  /////////////////////////////////////////////////////////////////////////////
 
-  void queueRowLemma(TNode a, TNode b, TNode i, TNode j);
-  inline void queueExtLemma(TNode a, TNode b);
+  private:
+  public:
 
-  /**
-   * Adds a Row lemma of the form:
-   *    i = j OR a[j] = b[j]
-   */
-  void addRowLemma(TNode a, TNode b, TNode i, TNode j);
+  Node getValue(TNode n);
 
-  /**
-   * Adds a new Ext lemma of the form
-   *    a = b OR a[k]!=b[k], for a new variable k
-   */
-  void addExtLemma(TNode a, TNode b);
+  /////////////////////////////////////////////////////////////////////////////
+  // NOTIFICATIONS
+  /////////////////////////////////////////////////////////////////////////////
 
-  /**
-   * Because Row1 axioms of the form (store a i v) [i] = v are not added as
-   * explicitly but are kept track of internally, is axiom recognizez an axiom
-   * of the above form given the two terms in the equality.
-   */
-  bool isAxiom(TNode lhs, TNode rhs);
+  private:
+  public:
 
+  void presolve();
+  void shutdown() { }
 
-  bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j);
-  bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j);
+  /////////////////////////////////////////////////////////////////////////////
+  // MAIN SOLVER
+  /////////////////////////////////////////////////////////////////////////////
 
+  public:
 
+  void check(Effort e);
 
-  bool alreadyAddedRow(TNode a, TNode b, TNode i, TNode j) {
-    //Trace("arrays-lem")<<"alreadyAddedRow check for "<<a<<" "<<b<<" "<<i<<" "<<j<<"\n";
-    std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it = d_RowAlreadyAdded.begin();
-    a = find(a);
-    b = find(b);
-    i = find(i);
-    j = find(j);
+  private:
 
-    for( ; it!= d_RowAlreadyAdded.end(); it++) {
+  // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+  class NotifyClass {
+    TheoryArrays& d_arrays;
+  public:
+    NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
 
-      TNode a_ = find((*it).first);
-      TNode b_ = find((*it).second);
-      TNode i_ = find((*it).third);
-      TNode j_ = find((*it).fourth);
-      if( a == a_ && b == b_ && i==i_ && j==j_) {
-        //Trace("arrays-lem")<<"alreadyAddedRow found "<<a_<<" "<<b_<<" "<<i_<<" "<<j_<<"\n";
-        return true;
-      }
+    bool notify(TNode propagation) {
+      Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+      // Just forward to arrays
+      return d_arrays.propagate(propagation);
     }
-    return false;
-  }
-
-
-  bool isNonLinear(TNode n);
-
-  /**
-   * Checks if any new Row lemmas need to be generated after merging arrays a
-   * and b; called after setCanon.
-   */
-  void checkRowLemmas(TNode a, TNode b);
-
-  /**
-   * Called after a new select term a[i] is created to check whether new Row
-   * lemmas need to be instantiated.
-   */
-  void checkRowForIndex(TNode i, TNode a);
-
-  void checkStore(TNode a);
-  /**
-   * Lemma helper functions to prevent changing the list we are iterating through.
-   */
 
-  void insertInQuadQueue(std::set<quad<TNode, TNode, TNode, TNode> >& queue, TNode a, TNode b, TNode i, TNode j){
-    if(i != j) {
-      queue.insert(make_quad(a,b,i,j));
-    }
-  }
-
-  void dischargeLemmas() {
-    // we need to swap the temporary lists because adding a lemma calls preregister
-    // which might modify the d_RowQueue we would be iterating through
-    std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction > temp_Row;
-    temp_Row.swap(d_RowQueue);
-
-    std::hash_set<quad<TNode, TNode, TNode, TNode>, TNodeQuadHashFunction >::const_iterator it1 = temp_Row.begin();
-    for( ; it1!= temp_Row.end(); it1++) {
-      if(!isRedundantInContext((*it1).first, (*it1).second, (*it1).third, (*it1).fourth)) {
-        addRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
-      }
-      else {
-        // add it to queue may be needed later
-        queueRowLemma((*it1).first, (*it1).second, (*it1).third, (*it1).fourth);
+    void notify(TNode t1, TNode t2) {
+      Debug("arrays") << spaces(d_arrays.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+      if (t1.getType().isArray()) {
+        d_arrays.mergeArrays(t1, t2);
+        if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
+          return;
+        }
       }
+      // Propagate equality between shared terms
+      Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+      d_arrays.propagate(equality);
     }
+  };
 
-    std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction>  temp_ext;
-    temp_ext.swap(d_extQueue);
 
-    std::hash_set<std::pair<TNode, TNode>, TNodePairHashFunction> ::const_iterator it2 = temp_ext.begin();
-    for(; it2 != temp_ext.end(); it2++) {
-      addExtLemma((*it2).first, (*it2).second);
-    }
-  }
+  /** The notify class for d_equalityEngine */
+  NotifyClass d_notify;
 
-  /** Checks if instead of adding a lemma of the form i = j OR  a[j] = b[j]
-   * we can propagate either i = j or NOT a[j] = b[j] and does the propagation.
-   * Returns whether it did propagate.
-   */
-  bool propagateFromRow(TNode a, TNode b, TNode i, TNode j);
+  /** Equaltity engine */
+  uf::EqualityEngine<NotifyClass> d_equalityEngine;
 
-  TNode areDisequal(TNode a, TNode b);
-
-
-
-  /*
-   * === STATISTICS ===
-   */
+  // Are we in conflict?
+  context::CDO<bool> d_conflict;
 
-  /** number of Row lemmas */
-  IntStat d_numRow;
-  /** number of Ext lemmas */
-  IntStat d_numExt;
-
-  /** number of propagations */
-  IntStat d_numProp;
-  IntStat d_numExplain;
-  /** time spent in check() */
-  TimerStat d_checkTimer;
-
-  bool d_donePreregister;
-
-  Node preprocessTerm(TNode term);
-  Node recursivePreprocessTerm(TNode term);
-
-public:
-  TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
-  ~TheoryArrays();
+  /** The conflict node */
+  Node d_conflictNode;
 
   /**
-   * Stores in d_infoMap the following information for each term a of type array:
-   *
-   *    - all i, such that there exists a term a[i] or a = store(b i v)
-   *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
-   *      position i due to the implicit axiom store(b i v)[i] = v )
-   *
-   *    - all the stores a is congruent to (this information is context dependent)
-   *
-   *    - all store terms of the form store (a i v) (i.e. in which a appears
-   *      directly; this is invariant because no new store terms are created)
-   *
-   * Note: completeness depends on having pre-register called on all the input
-   *       terms before starting to instantiate lemmas.
+   * Context dependent map from a congruence class canonical representative of
+   * type array to an Info pointer that keeps track of information useful to axiom
+   * instantiation
    */
-  void preRegisterTerm(TNode n) {
-    //TimerStat::CodeTimer codeTimer(d_preregisterTimer);
-    Trace("arrays-preregister")<<"Arrays::preRegisterTerm "<<n<<"\n";
-    //TODO: check non-linear arrays with an AlwaysAssert!!!
-    //if(n.getType().isArray())
-
-    switch(n.getKind()) {
-    case kind::EQUAL:
-      // stores the seen atoms for propagation
-      Trace("arrays-preregister")<<"atom "<<n<<"\n";
-      d_atoms.insert(n);
-      // add to proper equality lists
-      addEq(n);
-      break;
-    case kind::SELECT:
-      //Trace("arrays-preregister")<<"at level "<<getContext()->getLevel()<<"\n";
-      d_infoMap.addIndex(n[0], n[1]);
-      checkRowForIndex(n[1], find(n[0]));
-      //Trace("arrays-preregister")<<"n[0] \n";
-      //d_infoMap.getInfo(n[0])->print();
-      //Trace("arrays-preregister")<<"find(n[0]) \n";
-      //d_infoMap.getInfo(find(n[0]))->print();
-      break;
-
-    case kind::STORE:
-    {
-      // this should always be called at level0 since we do not create new store terms
-      TNode a = n[0];
-      TNode i = n[1];
-      TNode v = n[2];
-
-      NodeManager* nm = NodeManager::currentNM();
-      Node ni = nm->mkNode(kind::SELECT, n, i);
-      Node eq = nm->mkNode(kind::EQUAL, ni, v);
-
-      d_cc.addEquality(eq);
-
-      d_infoMap.addIndex(n, i);
-      d_infoMap.addStore(n, n);
-      d_infoMap.addInStore(a, n);
-
-      checkStore(n);
-
-      break;
-    }
-    default:
-      Trace("darrays")<<"Arrays::preRegisterTerm non-array term. \n";
-    }
-  }
 
-  //void registerTerm(TNode n) {
-  //  Trace("arrays-register")<<"Arrays::registerTerm "<<n<<"\n";
-  //}
+  Backtracker<TNode> d_backtracker;
+  ArrayInfo d_infoMap;
 
-  void presolve() {
-    Trace("arrays")<<"Presolving \n";
-    d_donePreregister = true;
-  }
+  context::CDQueue<Node> d_mergeQueue;
 
-  void addSharedTerm(TNode t);
-  void notifyEq(TNode lhs, TNode rhs);
-  void check(Effort e);
+  bool d_mergeInProgress;
 
-  void propagate(Effort e) {
+  typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
 
-    // Trace("arrays-prop")<<"Propagating \n";
+  context::CDQueue<RowLemmaType> d_RowQueue;
+  context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
 
-    // context::CDList<TNode>::const_iterator it = d_prop_queue.begin();
-    /*
-    for(; it!= d_prop_queue.end(); it++) {
-      TNode eq = *it;
-      if(d_valuation.getSatValue(eq).isNull()) {
-        //FIXME remove already propagated literals?
-        d_out->propagate(eq);
-        ++d_numProp;
-      }
-    }*/
-    //d_prop_queue.deleteSelf();
-    /*
-    __gnu_cxx::hash_set<TNode, TNodeHashFunction>::const_iterator it = d_atoms.begin();
-
-    for(; it!= d_atoms.end(); it++) {
-      TNode eq = *it;
-      Assert(eq.getKind()==kind::EQUAL);
-      Trace("arrays-prop")<<"value of "<<eq<<" ";
-      Trace("arrays-prop")<<d_valuation.getSatValue(eq);
-      if(find(eq[0]) == find(eq[1])) {
-        Trace("arrays-prop")<<" eq \n";
-        ++d_numProp;
-      }
-    }
-    */
+  context::CDHashMap<TNode, bool, TNodeHashFunction> d_sharedArrays;
+  context::CDO<bool> d_sharedTerms;
+  context::CDList<TNode> d_reads;
+  std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
 
-  }
-  Node explain(TNode n);
+  // List of nodes that need permanent references in this context
+  context::CDList<Node> d_permRef;
 
-  Node getValue(TNode n);
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
-  void shutdown() { }
-  std::string identify() const { return std::string("TheoryArrays"); }
+  Node mkAnd(std::vector<TNode>& conjunctions);
+  void setNonLinear(TNode a);
+  void mergeArrays(TNode a, TNode b);
+  void checkStore(TNode a);
+  void checkRowForIndex(TNode i, TNode a);
+  void checkRowLemmas(TNode a, TNode b);
+  void queueRowLemma(RowLemmaType lem);
+  void dischargeLemmas();
 
 };/* class TheoryArrays */
 
-inline void TheoryArrays::setCanon(TNode a, TNode b) {
-  d_unionFind.setCanon(a, b);
-}
-
-inline TNode TheoryArrays::find(TNode a) {
-  return d_unionFind.find(a);
-}
-
-inline TNode TheoryArrays::debugFind(TNode a) const {
-  return d_unionFind.debugFind(a);
-}
-
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index f3a19ff02..627f34a30 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -36,11 +36,22 @@ public:
     Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
     switch (node.getKind()) {
       case kind::SELECT: {
-        // select(store(a,i,v),i) = v
         TNode store = node[0];
-        if (store.getKind() == kind::STORE &&
-            store[1] == node[1]) {
-          return RewriteResponse(REWRITE_DONE, store[2]);
+        if (store.getKind() == kind::STORE) {
+          // select(store(a,i,v),j)
+          Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1]));
+          if (eqRewritten.getKind() == kind::CONST_BOOLEAN) {
+            bool value = eqRewritten.getConst<bool>();
+            if (value) {
+              // select(store(a,i,v),i) = v
+              return RewriteResponse(REWRITE_DONE, store[2]);
+            }
+            else {
+              // select(store(a,i,v),j) = select(a,j) if i /= j
+              Node newNode = NodeManager::currentNM()->mkNode(kind::SELECT, store[0], node[1]);
+              return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+            }
+          }
         }
         break;
       }
@@ -53,11 +64,25 @@ public:
             value[1] == node[1]) {
           return RewriteResponse(REWRITE_DONE, store);
         }
-        // store(store(a,i,v),i,w) = store(a,i,w)
-        if (store.getKind() == kind::STORE &&
-            store[1] == node[1]) {
-          Node newNode = NodeManager::currentNM()->mkNode(kind::STORE, store[0], store[1], value);
-          return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+        if (store.getKind() == kind::STORE) {
+          // store(store(a,i,v),j,w)
+          Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1]));
+          if (eqRewritten.getKind() == kind::CONST_BOOLEAN) {
+            bool val = eqRewritten.getConst<bool>();
+            NodeManager* nm = NodeManager::currentNM();
+            if (val) {
+              // store(store(a,i,v),i,w) = store(a,i,w)
+              Node newNode = nm->mkNode(kind::STORE, store[0], store[1], value);
+              return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+            }
+            else if (node[1] < store[1]) {
+              // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
+              //    IF i != j and j comes before i in the ordering
+              Node newNode = nm->mkNode(kind::STORE, store[0], node[1], value);
+              newNode = nm->mkNode(kind::STORE, newNode, store[1], store[2]);
+              return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+            }
+          }
         }
         break;
       }
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index fd9e7cb2f..fabff0aab 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -65,6 +65,32 @@ struct ArrayStoreTypeRule {
   }
 };/* struct ArrayStoreTypeRule */
 
+struct ArrayTableFunTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::ARR_TABLE_FUN);
+    TypeNode arrayType = n[0].getType(check);
+    if( check ) {
+      if(!arrayType.isArray()) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 0 is non-array");
+      }
+      TypeNode arrType2 = n[1].getType(check);
+      if(!arrayType.isArray()) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 1 is non-array");
+      }
+      TypeNode indexType = n[2].getType(check);
+      if(arrayType.getArrayIndexType() != indexType) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 2 does not match type of array");
+      }
+      indexType = n[3].getType(check);
+      if(arrayType.getArrayIndexType() != indexType) {
+        throw TypeCheckingExceptionPrivate(n, "array table fun arg 3 does not match type of array");
+      }
+    }
+    return arrayType.getArrayIndexType();
+  }
+};/* struct ArrayStoreTypeRule */
+
 struct CardinalityComputer {
   inline static Cardinality computeCardinality(TypeNode type) {
     Assert(type.getKind() == kind::ARRAY_TYPE);
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index edaf8c154..b579122e5 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -338,7 +338,7 @@ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Assert (node.getKind() == kind::VARIABLE);
+  //  Assert (node.getKind() == kind::VARIABLE);
   Assert(bits.size() == 0);
   
   for (unsigned i = 0; i < utils::getSize(node); ++i) {
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index f5c43688a..2f4ac1324 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -83,6 +83,9 @@ void Bitblaster::bbAtom(TNode node) {
     return; 
   }
 
+  // make sure it is marked as an atom
+  addAtom(node); 
+
   BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
@@ -298,12 +301,14 @@ void Bitblaster::initAtomBBStrategies() {
 }
 
 void Bitblaster::initTermBBStrategies() {
+  // Changed this to DefaultVarBB because any foreign kind should be treated as a variable
+  // TODO: check this is OK
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
-    d_termBBStrategies[i] = UndefinedTermBBStrategy; 
+    d_termBBStrategies[i] = DefaultVarBB;
   }
   
   /// setting default bb strategies for terms:
-  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
+  //  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
   d_termBBStrategies [ kind::CONST_BITVECTOR ]        = DefaultConstBB;
   d_termBBStrategies [ kind::BITVECTOR_NOT ]          = DefaultNotBB;
   d_termBBStrategies [ kind::BITVECTOR_CONCAT ]       = DefaultConcatBB;
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
index 647e4fe9f..2422da0b7 100644
--- a/src/theory/bv/bv_sat.h
+++ b/src/theory/bv/bv_sat.h
@@ -82,7 +82,9 @@ class Bitblaster {
                                                        currently asserted by the DPLL SAT solver. */
 
   /// helper methods
+  public:
   bool          hasBBAtom(TNode node);    
+  private:
   bool          hasBBTerm(TNode node); 
   void          getBBTerm(TNode node, Bits& bits);
 
@@ -101,6 +103,7 @@ class Bitblaster {
   Node bbOptimize(TNode node); 
   
   void bbAtom(TNode node);
+  void addAtom(TNode atom); 
   // division is bitblasted in terms of constraints
   // so it needs to use private bitblaster interface
   void bbUdiv(TNode node, Bits& bits);
@@ -116,7 +119,7 @@ public:
   bool solve(bool quick_solve = false);
   void bitblast(TNode node);
   void getConflict(std::vector<TNode>& conflict); 
-  void addAtom(TNode atom); 
+
   bool getPropagations(std::vector<TNode>& propagations);
   void explainPropagation(TNode atom, std::vector<Node>& explanation);
 private:
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 429e5ff19..a3f4364ba 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -20,8 +20,8 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/valuation.h"
-
 #include "theory/bv/bv_sat.h"
+#include "theory/uf/equality_engine_impl.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -31,16 +31,67 @@ using namespace CVC4::context;
 using namespace std;
 using namespace CVC4::theory::bv::utils;
 
+
+const bool d_useEqualityEngine = true;
+const bool d_useSatPropagation = true;
+
+
 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
   : Theory(THEORY_BV, c, u, out, valuation),
     d_context(c),
     d_assertions(c),
     d_bitblaster(new Bitblaster(c) ),
     d_statistics(),
-    d_alreadyPropagatedSet(c)
-   {
+    d_alreadyPropagatedSet(c),
+    d_notify(*this),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+    d_conflict(c, false),
+    d_literalsToPropagate(c),
+    d_literalsToPropagateIndex(c, 0),
+    d_toBitBlast(c)
+  {
     d_true = utils::mkTrue();
+    d_false = utils::mkFalse();
+
+    if (d_useEqualityEngine) {
+      d_equalityEngine.addTerm(d_true);
+      d_equalityEngine.addTerm(d_false);
+      d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+
+      // The kinds we are treating as function application in congruence
+      d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
+      d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
+      d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+
+    }
   }
+
 TheoryBV::~TheoryBV() {
   delete d_bitblaster; 
 }
@@ -68,32 +119,99 @@ void TheoryBV::preRegisterTerm(TNode node) {
       node.getKind() == kind::BITVECTOR_SLT ||
       node.getKind() == kind::BITVECTOR_SLE) {
     d_bitblaster->bitblast(node);
-    d_bitblaster->addAtom(node); 
   }
+
+  if (d_useEqualityEngine) {
+    switch (node.getKind()) {
+      case kind::EQUAL:
+        // Add the terms
+        d_equalityEngine.addTerm(node);
+        // Add the trigger for equality
+        d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+        d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+        break;
+      default:
+        d_equalityEngine.addTerm(node);
+        break;
+    }
+  }
+
 }
 
-void TheoryBV::check(Effort e) {
-  BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
+void TheoryBV::check(Effort e)
+{
+  BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; 
   BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
-  while (!done()) {
-    TNode assertion = get();
-    // make sure we do not assert things we propagated
-    if (!hasBeenPropagated(assertion)) {
-      BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n";
-      bool ok = d_bitblaster->assertToSat(assertion, true);
+  while (!done() && !d_conflict) {
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+
+    BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; 
+
+    // If the assertion doesn't have a literal, it's a shared equality
+    bool shared = !assertion.isPreregistered;
+    Assert(!d_useEqualityEngine || !shared ||
+           ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
+            (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
+             d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+
+    // Notify the Equality Engine
+    switch (fact.getKind()) {
+      case kind::EQUAL:
+        if (d_useEqualityEngine) {
+          d_equalityEngine.addEquality(fact[0], fact[1], fact);
+        }
+        if (shared && !d_bitblaster->hasBBAtom(fact)) {
+          d_bitblaster->bitblast(fact);
+        }
+        break;
+      case kind::NOT:
+        if (fact[0].getKind() == kind::EQUAL) {
+          // Assert the dis-equality
+          if (d_useEqualityEngine) {
+            d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+          }
+          if (shared && !d_bitblaster->hasBBAtom(fact[0])) {
+            d_bitblaster->bitblast(fact[0]);
+          }
+        } else {
+          if (d_useEqualityEngine) {
+            d_equalityEngine.addPredicate(fact[0], false, fact);
+          }
+          break;
+        }
+        break;
+      default:
+        if (d_useEqualityEngine) {
+          d_equalityEngine.addPredicate(fact, true, fact);
+        }
+        break;
+    }
+
+    // make sure we do not assert things we propagated 
+    if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) {
+      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
       if (!ok) {
         std::vector<TNode> conflictAtoms;
         d_bitblaster->getConflict(conflictAtoms);
         d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
-        Node conflict = mkConjunction(conflictAtoms);
-        d_out->conflict(conflict);
-        BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
-        return;
+        d_conflict = true;
+        d_conflictNode = mkConjunction(conflictAtoms);
+        break;
       }
     }
   }
 
+  // If in conflict, output the conflict
+  if (d_conflict) {
+    Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
+    d_out->conflict(d_conflictNode);
+    return;
+  }
+
   if (e == EFFORT_FULL) {
+
+    Assert(done() && !d_conflict);
     BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
     // in standard effort we only do boolean constraint propagation 
     bool ok = d_bitblaster->solve(false);
@@ -127,12 +245,36 @@ Node TheoryBV::getValue(TNode n) {
   }
 }
 
-bool TheoryBV::hasBeenPropagated(TNode node) {
-  return d_alreadyPropagatedSet.count(node); 
-}
 
 void TheoryBV::propagate(Effort e) {
-  BVDebug("bitvector") << "TheoryBV::propagate() \n";
+  BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
+
+  if (d_conflict) {
+    return;
+  }
+
+  // get new propagations from the equality engine
+  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+    TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+    BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
+    bool satValue;
+    Node normalized = Rewriter::rewrite(literal);
+    if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
+      d_out->propagate(literal);
+    } else {
+      Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
+      Node negatedLiteral;
+      std::vector<TNode> assumptions;
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+        assumptions.push_back(negatedLiteral);
+      }
+      explain(literal, assumptions);
+      d_conflictNode = mkAnd(assumptions);
+      d_conflict = true;
+      return;
+    }
+  }
 
   // get new propagations from the sat solver
   std::vector<TNode> propagations; 
@@ -142,6 +284,10 @@ void TheoryBV::propagate(Effort e) {
   for (unsigned i = 0; i < propagations.size(); ++ i) {
     TNode node = propagations[i];
     BVDebug("bitvector") << "TheoryBV::propagate    " << node <<" \n";
+    if (!d_valuation.isSatLiteral(node)) {
+      // TODO: maybe propagate shared terms too?
+      continue;
+    }
     if (d_valuation.getSatValue(node) == Node::null()) {
       vector<Node> explanation;
       d_bitblaster->explainPropagation(node, explanation);
@@ -162,21 +308,21 @@ void TheoryBV::propagate(Effort e) {
 
 }
 
-Node TheoryBV::explain(TNode n) {
-  BVDebug("bitvector") << "TheoryBV::explain node " <<  n <<"\n";
-  std::vector<Node> explanation;
-  d_bitblaster->explainPropagation(n, explanation);
-  Node exp;
+// Node TheoryBV::explain(TNode n) {
+//   BVDebug("bitvector") << "TheoryBV::explain node " <<  n <<"\n";
+//   std::vector<Node> explanation;
+//   d_bitblaster->explainPropagation(n, explanation);
+//   Node exp;
 
-  if (explanation.size() == 0) {
-    return utils::mkTrue(); 
-  }
+//   if (explanation.size() == 0) {
+//     return utils::mkTrue(); 
+//   }
   
-  exp = utils::mkAnd(explanation);
+//   exp = utils::mkAnd(explanation);
   
-  BVDebug("bitvector") << "TheoryBV::explain with " <<  exp <<"\n";
-  return exp;
-}
+//   BVDebug("bitvector") << "TheoryBV::explain with " <<  exp <<"\n";
+//   return exp;
+// }
 
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
@@ -203,3 +349,108 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
   }
   return PP_ASSERT_STATUS_UNSOLVED;
 }
+
+
+bool TheoryBV::propagate(TNode literal)
+{
+  Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal  << ")" << std::endl;
+
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
+    return false;
+  }
+
+  // See if the literal has been asserted already
+  Node normalized = Rewriter::rewrite(literal);
+  bool satValue = false;
+  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
+
+  // If asserted, we might be in conflict
+  if (isAsserted) {
+    if (!satValue) {
+      Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+      std::vector<TNode> assumptions;
+      Node negatedLiteral;
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+        assumptions.push_back(negatedLiteral);
+      }
+      explain(literal, assumptions);
+      d_conflictNode = mkAnd(assumptions);
+      d_conflict = true;
+      return false;
+    }
+    // Propagate even if already known in SAT - could be a new equation between shared terms
+    // (terms that weren't shared when the literal was asserted!)
+  }
+
+  // Nothing, just enqueue it for propagation and mark it as asserted already
+  Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+  d_literalsToPropagate.push_back(literal);
+
+  return true;
+}/* TheoryBV::propagate(TNode) */
+
+
+void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+    case kind::EQUAL:
+      lhs = literal[0];
+      rhs = literal[1];
+      break;
+    case kind::NOT:
+      if (literal[0].getKind() == kind::EQUAL) {
+        // Disequalities
+        d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
+        return;
+      } else {
+        // Predicates
+        lhs = literal[0];
+        rhs = d_false;
+        break;
+      }
+    case kind::CONST_BOOLEAN:
+      // we get to explain true = false, since we set false to be the trigger of this
+      lhs = d_true;
+      rhs = d_false;
+      break;
+    default:
+      Unreachable();
+  }
+  d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
+
+
+Node TheoryBV::explain(TNode node) {
+  BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+  std::vector<TNode> assumptions;
+  explain(node, assumptions);
+  return mkAnd(assumptions);
+}
+
+
+void TheoryBV::addSharedTerm(TNode t) {
+  Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+  if (d_useEqualityEngine) {
+    d_equalityEngine.addTriggerTerm(t);
+  }
+}
+
+
+EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
+{
+  if (d_useEqualityEngine) {
+    if (d_equalityEngine.areEqual(a, b)) {
+      // The terms are implied to be equal
+      return EQUALITY_TRUE;
+    }
+    if (d_equalityEngine.areDisequal(a, b)) {
+      // The terms are implied to be dis-equal
+      return EQUALITY_FALSE;
+    }
+  }
+  return EQUALITY_UNKNOWN;
+}
+
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index d147c8bb5..940eaef56 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -27,6 +27,8 @@
 #include "context/cdhashset.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/stats.h"
+#include "theory/uf/equality_engine.h"
+#include "context/cdqueue.h"
 
 namespace BVMinisat {
 class SimpSolver; 
@@ -40,6 +42,12 @@ namespace bv {
 /// forward declarations 
 class Bitblaster;
 
+static inline std::string spaces(int level)
+{
+  std::string indentStr(level, ' ');
+  return indentStr;
+}
+
 class TheoryBV : public Theory {
 
 
@@ -54,11 +62,11 @@ private:
   /** Bitblaster */
   Bitblaster* d_bitblaster; 
   Node d_true;
-
+  Node d_false;
+    
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
 
-  bool hasBeenPropagated(TNode node); 
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
@@ -70,8 +78,6 @@ public:
 
   void check(Effort e);
 
-  void propagate(Effort e);
-
   Node explain(TNode n);
 
   Node getValue(TNode n);
@@ -93,6 +99,61 @@ private:
   
   Statistics d_statistics;
   
+  // Added by Clark
+  // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+  class NotifyClass {
+    TheoryBV& d_bv;
+  public:
+    NotifyClass(TheoryBV& uf): d_bv(uf) {}
+
+    bool notify(TNode propagation) {
+      Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+      // Just forward to bv
+      return d_bv.propagate(propagation);
+    }
+
+    void notify(TNode t1, TNode t2) {
+      Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+      // Propagate equality between shared terms
+      Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+      d_bv.propagate(t1.eqNode(t2));
+    }
+  };
+
+  /** The notify class for d_equalityEngine */
+  NotifyClass d_notify;
+
+  /** Equaltity engine */
+  uf::EqualityEngine<NotifyClass> d_equalityEngine;
+
+  // Are we in conflict?
+  context::CDO<bool> d_conflict;
+
+  /** The conflict node */
+  Node d_conflictNode;
+
+  /** Literals to propagate */
+  context::CDList<Node> d_literalsToPropagate;
+
+  /** Index of the next literal to propagate */
+  context::CDO<unsigned> d_literalsToPropagateIndex;
+
+  context::CDQueue<Node> d_toBitBlast;
+
+  /** Should be called to propagate the literal.  */
+  bool propagate(TNode literal);
+
+  /** Explain why this literal is true by adding assumptions */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+
+  void addSharedTerm(TNode t);
+
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+
+public:
+
+  void propagate(Effort e);
+  
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index cf8310e5a..530949de2 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -866,6 +866,9 @@ Node RewriteRule<UremPow2>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned power = utils::isPow2Const(node[1]) - 1;
+  if (power == 0) {
+    return utils::mkConst(utils::getSize(node), 0);
+  }
   Node extract = utils::mkExtract(a, power - 1, 0);
   Node zeros = utils::mkConst(utils::getSize(node) - power, 0);
   return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract); 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 8b5dd0499..38547ad99 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -344,6 +344,29 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) {
 }
 
 
+inline Node mkAnd(const std::vector<TNode>& conjunctions) {
+  Assert(conjunctions.size() > 0);
+
+  std::set<TNode> all;
+  all.insert(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}/* mkAnd() */
+
+
 // Turn a set into a string
 inline std::string setToString(const std::set<TNode>& nodeSet) {
   std::stringstream out;
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 1687f3480..24cbc165c 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -16,9 +16,43 @@
  **/
 
 #include "theory/shared_terms_database.h"
+#include "theory/uf/equality_engine_impl.h"
 
 using namespace CVC4;
-using namespace CVC4::theory;
+using namespace theory;
+
+SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context)
+  : ContextNotifyObj(context),
+    d_context(context), 
+    d_statSharedTerms("theory::shared_terms", 0),
+    d_addedSharedTermsSize(context, 0),
+    d_termsToTheories(context),
+    d_alreadyNotifiedMap(context),
+    d_sharedNotify(notify),
+    d_termToNotifyList(context),
+    d_allocatedNLSize(0),
+    d_allocatedNLNext(context, 0),
+    d_EENotify(*this),
+    d_equalityEngine(d_EENotify, context, "SharedTermsDatabase")
+{
+  StatisticsRegistry::registerStat(&d_statSharedTerms);
+  NodeManager* nm = NodeManager::currentNM();
+  d_true = nm->mkConst<bool>(true);
+  d_false = nm->mkConst<bool>(false);
+  d_equalityEngine.addTerm(d_true);
+  d_equalityEngine.addTerm(d_false);
+  d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+}
+
+
+SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
+{
+  StatisticsRegistry::unregisterStat(&d_statSharedTerms);
+  for (unsigned i = 0; i < d_allocatedNLSize; ++i) {
+    d_allocatedNL[i]->deleteSelf();
+  }
+}
+
 
 void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) {
   Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; 
@@ -30,6 +64,9 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo
     d_addedSharedTerms.push_back(atom);
     d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
     d_termsToTheories[search_pair] = theories;
+    if (!d_equalityEngine.hasTerm(term)) {
+      d_equalityEngine.addTriggerTerm(term);
+    }
   } else {
     Assert(theories != (*find).second);
     d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); 
@@ -79,6 +116,7 @@ Theory::Set SharedTermsDatabase::getTheoriesToNotify(TNode atom, TNode term) con
   return Theory::setDifference((*find).second, alreadyNotified);
 }
 
+
 Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const {
   // Get the theories that were already notified
   AlreadyNotifiedMap::iterator theoriesFind = d_alreadyNotifiedMap.find(term);
@@ -89,7 +127,191 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const {
   }
 }
 
+
+SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList()
+{
+  NotifyList* retval;
+  if (d_allocatedNLSize == d_allocatedNLNext) {
+    retval = new (true) NotifyList(d_context);
+    d_allocatedNL.push_back(retval);
+    d_allocatedNLNext = ++d_allocatedNLSize;
+  }
+  else {
+    retval = d_allocatedNL[d_allocatedNLNext];
+    d_allocatedNLNext = d_allocatedNLNext + 1;
+  }
+  Assert(retval->empty());
+  return retval;
+}
+
+
+void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b)
+{
+  // Note: a is the new representative
+
+  NotifyList* pnlLeft = NULL;
+  NotifyList* pnlRight = NULL;
+
+  TermToNotifyList::iterator it = d_termToNotifyList.find(a);
+  if (it == d_termToNotifyList.end()) {
+    pnlLeft = getNewNotifyList();
+    d_termToNotifyList[a] = pnlLeft;
+  }
+  else {
+    pnlLeft = (*it).second;
+  }
+  it = d_termToNotifyList.find(b);
+  if (it != d_termToNotifyList.end()) {
+    pnlRight = (*it).second;
+  }
+
+  // Get theories interested in EC for lhs
+  Theory::Set lhsSet = getNotifiedTheories(a);
+  Theory::Set rhsSet = getNotifiedTheories(b);
+  NotifyList::iterator nit;
+  TNode left, right;
+
+  for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
+
+    if (Theory::setContains(currentTheory, rhsSet)) {
+      right = b;
+    }
+    else if (pnlRight != NULL &&
+             ((nit = pnlRight->end()) != pnlRight->end())) {
+      right = (*nit).second;
+    }
+    else {
+      // no match for right: continue
+      continue;
+    }
+
+    if (Theory::setContains(currentTheory, lhsSet)) {
+      left = a;
+    }
+    else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) {
+      left = (*nit).second;
+    }
+    else {
+      // no match for left: insert right into left
+      (*pnlLeft)[currentTheory] = right;
+      continue;
+    }
+
+    // New shared equality: notify the client
+
+    // TODO: add propagation of disequalities?
+
+    // Normalize the equality
+    Node equality = left.eqNode(right);
+    Node normalized = Rewriter::rewriteEquality(currentTheory, equality);
+    if (normalized.getKind() != kind::CONST_BOOLEAN) {
+      // Notify client
+      d_sharedNotify.notify(normalized, equality, currentTheory);
+    } else {
+      Assert(equality.getConst<bool>());
+    }
+  }
+
+}
+  
+
 void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
-  d_alreadyNotifiedMap[term] = Theory::setUnion(theories, d_alreadyNotifiedMap[term]);
+  Theory::Set alreadyNotified = d_alreadyNotifiedMap[term];
+  Theory::Set newlyNotified = Theory::setDifference(theories, alreadyNotified);
+  if (newlyNotified != 0) {
+    TNode rep = d_equalityEngine.getRepresentative(term);
+    if (rep != term) {
+      TermToNotifyList::iterator it = d_termToNotifyList.find(rep);
+      Assert(it != d_termToNotifyList.end());
+      NotifyList* pnl = (*it).second;
+      for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) {
+        if (Theory::setContains(theory, newlyNotified) &&
+            pnl->find(theory) == pnl->end()) {
+          (*pnl)[theory] = term;
+        }
+      }
+    }
+  }
+  d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified);
+}
+
+
+bool SharedTermsDatabase::areEqual(TNode a, TNode b) {
+  return d_equalityEngine.areEqual(a,b);
+}
+
+
+bool SharedTermsDatabase::areDisequal(TNode a, TNode b) {
+  return d_equalityEngine.areDisequal(a,b);
+}
+
+
+void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason)
+{
+  bool negated = literal.getKind() == kind::NOT;
+  TNode atom = negated ? literal[0] : literal;
+  if (negated) {
+    Assert(!d_equalityEngine.areDisequal(atom[0], atom[1]));
+    d_equalityEngine.addDisequality(atom[0], atom[1], reason);
+  }
+  else {
+    Assert(!d_equalityEngine.areEqual(atom[0], atom[1]));
+    d_equalityEngine.addEquality(atom[0], atom[1], reason);
+  }
 }
 
+
+static Node mkAnd(const std::vector<TNode>& conjunctions) {
+  Assert(conjunctions.size() > 0);
+
+  std::set<TNode> all;
+  all.insert(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}/* mkAnd() */
+
+
+Node SharedTermsDatabase::explain(TNode literal)
+{
+  std::vector<TNode> assumptions;
+  explain(literal, assumptions);
+  return mkAnd(assumptions);
+}
+
+
+void SharedTermsDatabase::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+    case kind::EQUAL:
+      lhs = literal[0];
+      rhs = literal[1];
+      break;
+    case kind::NOT:
+      if (literal[0].getKind() == kind::EQUAL) {
+        // Disequalities
+        d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
+        return;
+      }
+    case kind::CONST_BOOLEAN:
+      // we get to explain true = false, since we set false to be the trigger of this
+      lhs = d_true;
+      rhs = d_false;
+      break;
+    default:
+      Unreachable();
+  }
+  d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 2efd121a0..6af7fd41f 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -20,6 +20,7 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "util/stats.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 
@@ -34,6 +35,10 @@ public:
 
 private:
 
+  Node d_true;
+
+  Node d_false;
+
   /** The context */
   context::Context* d_context;
   
@@ -59,26 +64,72 @@ private:
   /** Map from term to theories that have already been notified about the shared term */
   AlreadyNotifiedMap d_alreadyNotifiedMap;
 
+public:
+  /** Class for notifications about new shared term equalities */
+  class SharedTermsNotifyClass {
+    public:
+      SharedTermsNotifyClass() {}
+      virtual ~SharedTermsNotifyClass() {}
+      virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0;
+  };
+
+private:
+  // Instance of class to send shared term notifications to
+  SharedTermsNotifyClass& d_sharedNotify;
+
+  // Type for list of theory, node pairs: theory is theory to be notified,
+  // node is the representative for this equivalence class known to the
+  // theory that will be notified
+  typedef context::CDHashMap<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList;
+  typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> TermToNotifyList;
+
+  // Map from terms (only valid for reps) to their notify lists
+  // Note that theory, term pairs only need to be in the notify list if the
+  // representative term is not a valid shared term for the theory.
+  TermToNotifyList d_termToNotifyList;
+
+  // List of allocated NotifyList* objects
+  std::vector<NotifyList*> d_allocatedNL;
+
+  // Total number of allocated NotifyList* objects
+  unsigned d_allocatedNLSize;
+
+  // Size of portion of d_allocatedNL that is currently in use
+  context::CDO<unsigned> d_allocatedNLNext;
+
   /** This method removes all the un-necessary stuff from the maps */
   void backtrack();
 
-public:
+  // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
+  class EENotifyClass {
+    SharedTermsDatabase& d_sharedTerms;
+  public:
+    EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
+    bool notify(TNode propagation) { return true; }    // Not used
+    void notify(TNode t1, TNode t2) {
+      d_sharedTerms.mergeSharedTerms(t1, t2);
+    }
+  };
 
-  SharedTermsDatabase(context::Context* context)
-  : ContextNotifyObj(context),
-    d_context(context), 
-    d_statSharedTerms("theory::shared_terms", 0),
-    d_addedSharedTermsSize(context, 0),
-    d_termsToTheories(context),
-    d_alreadyNotifiedMap(context) 
-  {
-    StatisticsRegistry::registerStat(&d_statSharedTerms);
-  }
+  /** The notify class for d_equalityEngine */
+  EENotifyClass d_EENotify;
 
-  ~SharedTermsDatabase() throw(AssertionException)
-  {
-    StatisticsRegistry::unregisterStat(&d_statSharedTerms);
-  }
+  /** Equaltity engine */
+  theory::uf::EqualityEngine<EENotifyClass> d_equalityEngine;
+
+  /** Attach a new notify list to an equivalence class representative */
+  NotifyList* getNewNotifyList();
+
+  /** Method called by equalityEngine when a becomes equal to b */
+  void mergeSharedTerms(TNode a, TNode b);
+
+  /** Internal explanation method */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+
+public:
+
+  SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context);
+  ~SharedTermsDatabase() throw(AssertionException);
   
   /**
    * Add a shared term to the database. The shared term is a subterm of the atom and 
@@ -116,6 +167,18 @@ public:
    */
   void markNotified(TNode term, theory::Theory::Set theories);
    
+  bool isShared(TNode term) const {
+    return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
+  }
+
+  bool areEqual(TNode a, TNode b);
+
+  bool areDisequal(TNode a, TNode b);
+
+  void processSharedLiteral(TNode literal, TNode reason);
+
+  Node explain(TNode literal);
+
   /**
    * This method gets called on backtracks from the context manager.
    */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 6460533e2..afd311bf2 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -60,7 +60,7 @@ void Theory::computeCareGraph() {
         // We don't care about the terms of different types
         continue;
       }
-      switch (getEqualityStatus(a, b)) {
+      switch (d_valuation.getEqualityStatus(a, b)) {
       case EQUALITY_TRUE_AND_PROPAGATED:
       case EQUALITY_FALSE_AND_PROPAGATED:
   	// If we know about it, we should have propagated it, so we can skip
diff --git a/src/theory/theory.h b/src/theory/theory.h
index a8d34eab3..28fdc8cbe 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -281,7 +281,7 @@ public:
       id = kindToTheoryId(typeNode.getKind());
     }
     if (id == THEORY_BUILTIN) {
-      Trace("theory") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
+      Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
       return s_uninterpretedSortOwner;
     }
     return id;
@@ -637,7 +637,7 @@ public:
 
   /** a - b  */
   static inline Set setDifference(Set a, Set b) {
-    return ((~b) & AllTheories) & a;
+    return (~b) & a;
   }
 
   static inline std::string setToString(theory::Theory::Set theorySet) {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a3ff4d90b..1bb830aa8 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -43,15 +43,17 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_context(context),
   d_userContext(userContext),
   d_activeTheories(context, 0),
-  d_sharedTerms(context),
-  d_atomPreprocessingCache(),
+  d_notify(*this),
+  d_sharedTerms(d_notify, context),
+  d_ppCache(),
   d_possiblePropagations(),
   d_hasPropagated(context),
   d_inConflict(context, false),
   d_sharedTermsExist(context, false),
   d_hasShutDown(false),
   d_incomplete(context, false),
-  d_sharedAssertions(context),
+  d_sharedLiteralsIn(context),
+  d_assertedLiteralsOut(context),
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
   d_decisionRequests(context),
@@ -118,8 +120,8 @@ void TheoryEngine::check(Theory::Effort effort) {
   // Do the checking
   try {
 
-    // Clear any leftover propagated equalities
-    d_propagatedEqualities.clear();
+    // Clear any leftover propagated shared literals
+    d_propagatedSharedLiterals.clear();
 
     // Mark the output channel unused (if this is FULL_EFFORT, and nothing
     // is done by the theories, no additional check will be needed)
@@ -173,10 +175,10 @@ void TheoryEngine::check(Theory::Effort effort) {
       // We are still satisfiable, propagate as much as possible
       propagate(effort);
 
-      // If we have any propagated equalities, we enqueue them to the theories and re-check
-      if (d_propagatedEqualities.size() > 0) {
-        Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl;
-        assertSharedEqualities();
+      // If we have any propagated shared literals, we enqueue them to the theories and re-check
+      if (d_propagatedSharedLiterals.size() > 0) {
+        Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl;
+        outputSharedLiterals();
         continue;
       }
 
@@ -191,12 +193,12 @@ void TheoryEngine::check(Theory::Effort effort) {
         // Do the combination
         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl;
         combineTheories();
-        // If we have any propagated equalities, we enqueue them to the theories and re-check
-        if (d_propagatedEqualities.size() > 0) {
-          Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared equalities" << std::endl;
-          assertSharedEqualities();
+        // If we have any propagated shared literals, we enqueue them to the theories and re-check
+        if (d_propagatedSharedLiterals.size() > 0) {
+          Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl;
+          outputSharedLiterals();
         } else {
-          // No propagated equalities, we're either sat, or there are lemmas added
+          // No propagated shared literals, we're either sat, or there are lemmas added
           break;
         }
       } else {
@@ -204,8 +206,8 @@ void TheoryEngine::check(Theory::Effort effort) {
       }
     }
 
-    // Clear any leftover propagated equalities
-    d_propagatedEqualities.clear();
+    // Clear any leftover propagated shared literals
+    d_propagatedSharedLiterals.clear();
 
     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl;
 
@@ -214,15 +216,15 @@ void TheoryEngine::check(Theory::Effort effort) {
   }
 }
 
-void TheoryEngine::assertSharedEqualities() {
-  // Assert all the shared equalities
-  for (unsigned i = 0; i < d_propagatedEqualities.size(); ++ i) {
-    const SharedEquality& eq = d_propagatedEqualities[i];
+void TheoryEngine::outputSharedLiterals() {
+  // Assert all the shared literals
+  for (unsigned i = 0; i < d_propagatedSharedLiterals.size(); ++ i) {
+    const SharedLiteral& eq = d_propagatedSharedLiterals[i];
     // Check if the theory already got this one
-    if (d_sharedAssertions.find(eq.toAssert) == d_sharedAssertions.end()) {
-      Debug("sharing") << "TheoryEngine::assertSharedEqualities(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl;
-      Debug("sharing") << "TheoryEngine::assertSharedEqualities(): orignal " << eq.toExplain.node << " from " << eq.toExplain.theory << std::endl;
-      d_sharedAssertions[eq.toAssert] = eq.toExplain;
+    if (d_assertedLiteralsOut.find(eq.toAssert) == d_assertedLiteralsOut.end()) {
+      Debug("sharing") << "TheoryEngine::outputSharedLiterals(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl;
+      Debug("sharing") << "TheoryEngine::outputSharedLiterals(): orignal " << eq.toExplain << std::endl;
+      d_assertedLiteralsOut[eq.toAssert] = eq.toExplain;
       if (eq.toAssert.theory == theory::THEORY_LAST) {
         d_propagatedLiterals.push_back(eq.toAssert.node);
       } else {
@@ -231,7 +233,7 @@ void TheoryEngine::assertSharedEqualities() {
     }
   }
   // Clear the equalities
-  d_propagatedEqualities.clear();
+  d_propagatedSharedLiterals.clear();
 }
 
 
@@ -260,40 +262,44 @@ void TheoryEngine::combineTheories() {
 
     Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl;
 
+    if (d_sharedTerms.areEqual(carePair.a, carePair.b) ||
+        d_sharedTerms.areDisequal(carePair.a, carePair.b)) {
+      continue;
+    }
+
+    if (carePair.a.isConst() && carePair.b.isConst()) {
+      // TODO: equality engine should auto-detect these as disequal
+      d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), NodeManager::currentNM()->mkConst<bool>(true));
+      continue;
+    }
+
     Node equality = carePair.a.eqNode(carePair.b);
     Node normalizedEquality = Rewriter::rewrite(equality);
     bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN;
-
-    // If the node has a literal, it has been asserted so we should just check it
     bool value;
     if (isTrivial || (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value))) {
+      // Missed propagation!
       Debug("sharing") << "TheoryEngine::combineTheories(): has a literal or is trivial" << std::endl;
-
+      
       if (isTrivial) {
-	// if the equality is trivial, we assert it back to the theory saying the sat solver should explain
         value = normalizedEquality.getConst<bool>();
+        normalizedEquality = NodeManager::currentNM()->mkConst<bool>(true);
       }
-
-      // Normalize the equality to the theory that requested it
-      Node toAssert = Rewriter::rewriteEquality(carePair.theory, equality);
-
-      if (value) {
-        SharedEquality sharedEquality(toAssert, normalizedEquality, theory::THEORY_LAST, carePair.theory);
-        if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) {
-          d_propagatedEqualities.push_back(sharedEquality);
-        }
-      } else {
-        SharedEquality sharedEquality(toAssert.notNode(), normalizedEquality.notNode(), theory::THEORY_LAST, carePair.theory);
-        if (d_sharedAssertions.find(sharedEquality.toAssert) == d_sharedAssertions.end()) {
-          d_propagatedEqualities.push_back(sharedEquality);
-        }
+      else {
+        d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST;
+        if (!value) normalizedEquality = normalizedEquality.notNode();
       }
-    } else {
-       Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
-
-       // There is no value, so we need to split on it
-       lemma(equality.orNode(equality.notNode()), false, false);
+      if (!value) {
+        equality = equality.notNode();
+      }
+      d_sharedTerms.processSharedLiteral(equality, normalizedEquality);
+      continue;
     }
+
+    // There is no value, so we need to split on it
+    Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
+    lemma(equality.orNode(equality.notNode()), false, false);
+
   }
 }
 
@@ -493,6 +499,43 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
   return solveStatus;
 }
 
+// Recursively traverse a term and call the theory rewriter on its sub-terms
+Node TheoryEngine::ppTheoryRewrite(TNode term)
+{
+  NodeMap::iterator find = d_ppCache.find(term);
+  if (find != d_ppCache.end()) {
+    return (*find).second;
+  }
+  unsigned nc = term.getNumChildren();
+  if (nc == 0) {
+    return theoryOf(term)->ppRewrite(term);
+  }
+  Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
+  NodeBuilder<> newNode(term.getKind());
+  if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    newNode << term.getOperator();
+  }
+  unsigned i;
+  for (i = 0; i < nc; ++i) {
+    newNode << ppTheoryRewrite(term[i]);
+  }
+  Node newTerm = Rewriter::rewrite(newNode);
+  Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm);
+  if (newTerm != newTerm2) {
+    newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
+  }
+  d_ppCache[term] = newTerm;
+  Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm << "}" << endl;
+  return newTerm;
+}
+
+
+void TheoryEngine::preprocessStart()
+{
+  d_ppCache.clear();
+}
+
+
 struct preprocess_stack_element {
   TNode node;
   bool children_added;
@@ -518,15 +561,15 @@ Node TheoryEngine::preprocess(TNode assertion) {
     Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl;
 
     // If node already in the cache we're done, pop from the stack
-    NodeMap::iterator find = d_atomPreprocessingCache.find(current);
-    if (find != d_atomPreprocessingCache.end()) {
+    NodeMap::iterator find = d_ppCache.find(current);
+    if (find != d_ppCache.end()) {
       toVisit.pop_back();
       continue;
     }
 
-    // If this is an atom, we preprocess it with the theory
+    // If this is an atom, we preprocess its terms with the theory ppRewriter
     if (Theory::theoryOf(current) != THEORY_BOOL) {
-      d_atomPreprocessingCache[current] = theoryOf(current)->ppRewrite(current);
+      d_ppCache[current] = ppTheoryRewrite(current);
       continue;
     }
 
@@ -538,13 +581,13 @@ Node TheoryEngine::preprocess(TNode assertion) {
         builder << current.getOperator();
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
-        Assert(d_atomPreprocessingCache.find(current[i]) != d_atomPreprocessingCache.end());
-        builder << d_atomPreprocessingCache[current[i]];
+        Assert(d_ppCache.find(current[i]) != d_ppCache.end());
+        builder << d_ppCache[current[i]];
       }
       // Mark the substitution and continue
       Node result = builder;
       Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl;
-      d_atomPreprocessingCache[current] = result;
+      d_ppCache[current] = result;
       toVisit.pop_back();
     } else {
       // Mark that we have added the children if any
@@ -553,59 +596,94 @@ Node TheoryEngine::preprocess(TNode assertion) {
         // We need to add the children
         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
           TNode childNode = *child_it;
-          NodeMap::iterator childFind = d_atomPreprocessingCache.find(childNode);
-          if (childFind == d_atomPreprocessingCache.end()) {
+          NodeMap::iterator childFind = d_ppCache.find(childNode);
+          if (childFind == d_ppCache.end()) {
             toVisit.push_back(childNode);
           }
         }
       } else {
         // No children, so we're done
         Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl;
-        d_atomPreprocessingCache[current] = current;
+        d_ppCache[current] = current;
         toVisit.pop_back();
       }
     }
   }
 
   // Return the substituted version
-  return d_atomPreprocessingCache[assertion];
+  return d_ppCache[assertion];
 }
 
 void TheoryEngine::assertFact(TNode node)
 {
   Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
+  Trace("theory::assertFact") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 
   d_propEngine->checkTime();
 
   // Get the atom
-  TNode atom = node.getKind() == kind::NOT ? node[0] : node;
-
-  // Assert the fact to the appropriate theory and mark it active
+  bool negated = node.getKind() == kind::NOT;
+  TNode atom = negated ? node[0] : node;
   Theory* theory = theoryOf(atom);
-  theory->assertFact(node, true);
-  markActive(Theory::setInsert(theory->getId()));
 
-  // If any shared terms, notify the theories
-  if (d_sharedTerms.hasSharedTerms(atom)) {
-    SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
-    SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
-    for (; it != it_end; ++ it) {
-      TNode term = *it;
-      Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
-      for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) {
-        if (Theory::setContains(theory, theories)) {
-          theoryOf(theory)->addSharedTermInternal(term);
+  //TODO: there is probably a bug here if shared terms start to exist after some asseritons have been processed
+  if (d_sharedTermsExist) {
+
+    // If any shared terms, notify the theories
+    if (d_sharedTerms.hasSharedTerms(atom)) {
+      SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
+      SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
+      for (; it != it_end; ++ it) {
+        TNode term = *it;
+        Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
+        for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
+          if (Theory::setContains(id, theories)) {
+            theoryOf(id)->addSharedTermInternal(term);
+          }
         }
+        d_sharedTerms.markNotified(term, theories);
+        markActive(theories);
+      }
+    }
+
+    if (atom.getKind() == kind::EQUAL &&
+        d_sharedTerms.isShared(atom[0]) &&
+        d_sharedTerms.isShared(atom[1])) {
+      Debug("sharing") << "TheoryEngine::assertFact: asserting shared node: " << node << std::endl;
+      // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain
+      if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) ||
+          ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) {
+        Debug("sharing") << "TheoryEngine::assertFact: sharedLiteral already known(" << node << ")" << std::endl;
+        return;
+      }
+      d_sharedLiteralsIn[node] = THEORY_LAST;
+      d_sharedTerms.processSharedLiteral(node, node);
+      if (d_propagatedSharedLiterals.size() > 0) {
+        Debug("theory") << "TheoryEngine::assertFact: distributing shared literals" << std::endl;
+        outputSharedLiterals();
+      }
+      // TODO: have processSharedLiteral propagate disequalities?
+      if (node.getKind() == kind::EQUAL) {
+        // Don't have to assert it - this will be taken care of by processSharedLiteral
+        Assert(isActive(theory->getId()));
+        return;
       }
-      d_sharedTerms.markNotified(term, theories);
-      markActive(theories);
+    }
+    // If theory didn't already get this literal, add to the map
+    NodeTheoryPair ntp(node, theory->getId());
+    if (d_assertedLiteralsOut.find(ntp) == d_assertedLiteralsOut.end()) {
+      d_assertedLiteralsOut[ntp] = Node();
     }
   }
+
+  // Assert the fact to the appropriate theory and mark it active
+  theory->assertFact(node, true);
+  markActive(Theory::setInsert(theory->getId()));
 }
 
 void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 
-  Debug("theory") << "EngineOutputChannel::propagate(" << literal << ", " << theory << ")" << std::endl;
+  Debug("theory") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << std::endl;
 
   d_propEngine->checkTime();
 
@@ -617,58 +695,51 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
     d_hasPropagated.insert(literal);
   }
 
-  TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+  bool negated = (literal.getKind() == kind::NOT);
+  TNode atom = negated ? literal[0] : literal;
+  bool value;
 
-  if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL) {
-    // If not an equality it must be a SAT literal so we enlist it, and it can only
-    // be propagated by the theory that owns it, as it is the only one that got
-    // a preregister call with it.
+  if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL ||
+      !d_sharedTerms.isShared(atom[0]) || !d_sharedTerms.isShared(atom[1])) {
+    // If not an equality or if an equality between terms that are not both shared,
+    // it must be a SAT literal so we enqueue it
     Assert(d_propEngine->isSatLiteral(literal));
-    d_propagatedLiterals.push_back(literal);
+    if (d_propEngine->hasValue(literal, value)) {
+      // if we are propagting something that already has a sat value we better be the same
+      Debug("theory") << "literal " << literal << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
+      Assert(value);
+    } else {
+      d_propagatedLiterals.push_back(literal);
+    }
   } else {
-    // Otherwise it might be a shared-term (dis-)equality
+    // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain
+    if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) ||
+        ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) {
+      Debug("sharing") << "TheoryEngine::propagate: sharedLiteral already known(" << literal << ")" << std::endl;
+      return;
+    }
+
+    // Otherwise it is a shared-term (dis-)equality
     Node normalizedLiteral = Rewriter::rewrite(literal);
     if (d_propEngine->isSatLiteral(normalizedLiteral)) {
-      // If there is a literal, just enqueue it, same as above
-      bool value;
+      // If there is a literal, propagate it to SAT
       if (d_propEngine->hasValue(normalizedLiteral, value)) {
         // if we are propagting something that already has a sat value we better be the same
-        Debug("theory") << "literal " << literal << " (" << normalizedLiteral << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
+        Debug("theory") << "literal " << literal << ", normalized = " << normalizedLiteral << ", propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
         Assert(value);
       } else {
-        SharedEquality sharedEquality(normalizedLiteral, literal, theory, theory::THEORY_LAST);
-        d_propagatedEqualities.push_back(sharedEquality);
-      }
-    }
-    // Otherwise, we assert it to all interested theories
-    Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]);
-    Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(atom[1]);
-    // Now notify the theories
-    if (Theory::setIntersection(lhsNotified, rhsNotified) != 0) {
-      bool negated = literal.getKind() == kind::NOT;
-      for (TheoryId currentTheory = theory::THEORY_FIRST; currentTheory != theory::THEORY_LAST; ++ currentTheory) {
-        if (currentTheory == theory) {
-          // Don't reassert to the same theory
-          continue;
-        }
-        // Assert if theory is interested in both terms
-        if (Theory::setContains(currentTheory, lhsNotified) && Theory::setContains(currentTheory, rhsNotified)) {
-          // Normalize the equality
-          Node equality = Rewriter::rewriteEquality(currentTheory, atom);
-          if (equality.getKind() != kind::CONST_BOOLEAN) {
-            // The assertion
-            Node assertion = negated ? equality.notNode() : equality;
-            // Remember it to assert later
-            d_propagatedEqualities.push_back(SharedEquality(assertion, literal, theory, currentTheory));
-          } else {
-            Assert(negated || equality.getConst<bool>());
-          }
-        }
+        SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST);
+        d_propagatedSharedLiterals.push_back(sharedLiteral);
       }
     }
+    // Assert to interested theories
+    Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl;
+    d_sharedLiteralsIn[literal] = theory;
+    d_sharedTerms.processSharedLiteral(literal, literal);
   }
 }
 
+
 void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) {
   Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl;
 
@@ -681,6 +752,14 @@ void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) {
 
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   Assert(a.getType() == b.getType());
+  if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
+    if (d_sharedTerms.areEqual(a,b)) {
+      return EQUALITY_TRUE_AND_PROPAGATED;
+    }
+    else if (d_sharedTerms.areDisequal(a,b)) {
+      return EQUALITY_FALSE_AND_PROPAGATED;
+    }
+  }
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
@@ -695,29 +774,26 @@ Node TheoryEngine::getExplanation(TNode node) {
   Theory* theory;
 
   //This is true if atom is a shared assertion
-  bool sharedAssertion = false;
+  bool sharedLiteral = false;
 
-  SharedAssertionsMap::iterator find;
+  AssertedLiteralsOutMap::iterator find;
   // "find" will have a value when sharedAssertion is true
   if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) {
-    find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
-    sharedAssertion = (find != d_sharedAssertions.end());
+    find = d_assertedLiteralsOut.find(NodeTheoryPair(node, theory::THEORY_LAST));
+    sharedLiteral = (find != d_assertedLiteralsOut.end());
   }
 
   // Get the explanation
-  if(sharedAssertion){
-    theory = theoryOf((*find).second.theory);
-    explanation = theory->explain((*find).second.node);
+  if(sharedLiteral) {
+    explanation = explain(ExplainTask((*find).second, SHARED_LITERAL_OUT));
   } else {
     theory = theoryOf(atom);
     explanation = theory->explain(node);
-  }
 
-  // Explain any shared equalities that might be in the explanation
-  if (d_sharedTermsExist) {
-    NodeBuilder<> nb(kind::AND);
-    explainEqualities(theory->getId(), explanation, nb);
-    explanation = nb;
+    // Explain any shared equalities that might be in the explanation
+    if (d_sharedTermsExist) {
+      explanation = explain(ExplainTask(explanation, THEORY_EXPLANATION, theory->getId()));
+    }
   }
 
   Assert(!explanation.isNull());
@@ -730,6 +806,114 @@ Node TheoryEngine::getExplanation(TNode node) {
   return explanation;
 }
 
+Node TheoryEngine::explain(ExplainTask toExplain)
+{
+  Debug("theory") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl;
+
+  std::set<TNode> satAssertions;
+  std::deque<ExplainTask> explainQueue;
+  // TODO: benchmark whether this helps
+  std::hash_set<ExplainTask, ExplainTaskHashFunction> explained;
+  bool value;
+
+  // No need to explain "true"
+  explained.insert(ExplainTask(NodeManager::currentNM()->mkConst<bool>(true), SHARED_DATABASE_EXPLANATION));
+
+  while (true) {
+
+    Debug("theory-explain") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl;
+
+    if (explained.find(toExplain) == explained.end()) {
+
+      explained.insert(toExplain);
+
+      if (toExplain.node.getKind() == kind::AND) {
+        for (unsigned i = 0, i_end = toExplain.node.getNumChildren(); i != i_end; ++ i) {
+          explainQueue.push_back(ExplainTask(toExplain.node[i], toExplain.kind, toExplain.theory));
+        }
+      }
+      else {
+
+        switch (toExplain.kind) {
+
+          // toExplain.node contains a shared literal sent out from theory engine (before being rewritten)
+          case SHARED_LITERAL_OUT: {
+            // Shortcut - see if this came directly from a theory
+            SharedLiteralsInMap::iterator it = d_sharedLiteralsIn.find(toExplain.node);
+            if (it != d_sharedLiteralsIn.end()) {
+              TheoryId id = (*it).second;
+              if (id == theory::THEORY_LAST) {
+                Assert(d_propEngine->isSatLiteral(toExplain.node));
+                Assert(d_propEngine->hasValue(toExplain.node, value) && value);
+                satAssertions.insert(toExplain.node);
+                break;
+              }
+              explainQueue.push_back(ExplainTask(theoryOf((*it).second)->explain(toExplain.node), THEORY_EXPLANATION, (*it).second));
+            }
+            // Otherwise, get explanation from shared terms database
+            else {
+              explainQueue.push_back(ExplainTask(d_sharedTerms.explain(toExplain.node), SHARED_DATABASE_EXPLANATION));
+            }
+            break;
+          }
+
+            // toExplain.node contains explanation from theory, toExplain.theory contains theory that produced explanation
+          case THEORY_EXPLANATION: {
+            AssertedLiteralsOutMap::iterator find = d_assertedLiteralsOut.find(NodeTheoryPair(toExplain.node, toExplain.theory));
+            if (find == d_assertedLiteralsOut.end() || (*find).second.isNull()) {
+              Assert(d_propEngine->isSatLiteral(toExplain.node));
+              Assert(d_propEngine->hasValue(toExplain.node, value) && value);
+              satAssertions.insert(toExplain.node);
+            }
+            else {
+              explainQueue.push_back(ExplainTask((*find).second, SHARED_LITERAL_OUT));
+            }
+            break;
+          }
+
+            // toExplain.node contains an explanation from the shared terms database
+            // Each literal in the explanation should be in the d_sharedLiteralsIn map
+          case SHARED_DATABASE_EXPLANATION: {
+            Assert(d_sharedLiteralsIn.find(toExplain.node) != d_sharedLiteralsIn.end());
+            TheoryId id = d_sharedLiteralsIn[toExplain.node];
+            if (id == theory::THEORY_LAST) {
+              Assert(d_propEngine->isSatLiteral(toExplain.node));
+              Assert(d_propEngine->hasValue(toExplain.node, value) && value);
+              satAssertions.insert(toExplain.node);
+            }
+            else {
+              explainQueue.push_back(ExplainTask(theoryOf(id)->explain(toExplain.node), THEORY_EXPLANATION, id));
+            }
+            break;
+          }        
+          default:
+            Unreachable();
+        }
+      }
+    }
+
+    if (explainQueue.empty()) break;
+
+    toExplain = explainQueue.front();
+    explainQueue.pop_front();
+  }
+
+  Assert(satAssertions.size() > 0);
+  if (satAssertions.size() == 1) {
+    return *(satAssertions.begin());
+  }
+
+  // Now build the explanation
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = satAssertions.begin();
+  std::set<TNode>::const_iterator it_end = satAssertions.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+  return conjunction;
+}
+
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
   // Mark that we are in conflict
@@ -742,9 +926,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 
   if (d_sharedTermsExist) {
     // In the multiple-theories case, we need to reconstruct the conflict
-    NodeBuilder<> nb(kind::AND);
-    explainEqualities(theoryId, conflict, nb);
-    Node fullConflict = nb;
+    Node fullConflict = explain(ExplainTask(conflict, THEORY_EXPLANATION, theoryId));
     Assert(properConflict(fullConflict));
     Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl;
     lemma(fullConflict, true, false);
@@ -754,47 +936,3 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     lemma(conflict, true, false);
   }
 }
-
-void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuilder<>& builder) {
-  Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl;
-  if (literals.getKind() == kind::AND) {
-    for (unsigned i = 0, i_end = literals.getNumChildren(); i != i_end; ++ i) {
-      TNode literal = literals[i];
-      TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
-      if (atom.getKind() == kind::EQUAL) {
-        explainEquality(theoryId, literal, builder);
-      } else if(literal.getKind() == kind::AND){
-        explainEqualities(theoryId, literal, builder);
-      } else {
-        builder << literal;
-      }
-    }
-  } else {
-    TNode atom = literals.getKind() == kind::NOT ? literals[0] : literals;
-    if (atom.getKind() == kind::EQUAL) {
-      explainEquality(theoryId, literals, builder);
-    } else {
-      builder << literals;
-    }
-  }
-}
-
-void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder) {
-  Assert(eqLiteral.getKind() == kind::EQUAL || (eqLiteral.getKind() == kind::NOT && eqLiteral[0].getKind() == kind::EQUAL));
-
-  SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId));
-  if (find == d_sharedAssertions.end()) {
-    // Not a shared assertion, just add it since it must be SAT literal
-    builder << Rewriter::rewrite(eqLiteral);
-  } else {
-    TheoryId explainingTheory = (*find).second.theory;
-    if (explainingTheory == theory::THEORY_LAST) {
-      // If the theory is from the SAT solver, just take the normalized one
-      builder << (*find).second.node;
-    } else {
-      // Explain it using the theory that propagated it
-      Node explanation = theoryOf(explainingTheory)->explain((*find).second.node);
-      explainEqualities(explainingTheory, explanation, builder);
-    }
-  }
-}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 5712b1502..dd642a865 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -98,6 +98,21 @@ class TheoryEngine {
    */
   context::CDO<theory::Theory::Set> d_activeTheories;
 
+  // NotifyClass: template helper class for Shared Terms Database
+  class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass {
+    TheoryEngine& d_theoryEngine;
+  public:
+    NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {}
+    ~NotifyClass() {}
+
+    void notify(TNode literal, TNode original, theory::TheoryId theory) {
+      d_theoryEngine.propagateSharedLiteral(literal, original, theory);
+    }
+  };
+
+  // Instance of NotifyClass
+  NotifyClass d_notify;
+
   /**
    * The database of shared terms.
    */
@@ -106,9 +121,9 @@ class TheoryEngine {
   typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
 
   /**
-   * Cache from proprocessing of atoms.
+  * Cache for theory-preprocessing of assertions
    */
-  NodeMap d_atomPreprocessingCache;
+  NodeMap d_ppCache;
 
   /**
    * Used for "missed-t-propagations" dumping mode only.  A set of all
@@ -296,32 +311,55 @@ class TheoryEngine {
     return theory::Theory::setContains(theory, d_activeTheories);
   }
 
-  struct SharedEquality {
+  struct SharedLiteral {
     /** The node/theory pair for the assertion */
+    /** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */
     NodeTheoryPair toAssert;
-    /** This is the node/theory pair that we will use to explain it */
-    NodeTheoryPair toExplain;
+    /** This is the node that we will use to explain it */
+    Node toExplain;
 
-    SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory)
+    SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory)
     : toAssert(assertion, receivingTheory),
-      toExplain(original, sendingTheory)
+      toExplain(original)
     { }
-  };/* struct SharedEquality */
+  };/* struct SharedLiteral */
 
   /**
-   * Map from equalities asserted to a theory, to the theory that can explain them.
+   * Map from nodes to theories.
    */
-  typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap;
+  typedef context::CDHashMap<Node, theory::TheoryId, NodeHashFunction> SharedLiteralsInMap;
 
   /**
-   * A map from asserted facts to where they came from (for explanations).
+   * All shared literals asserted to theory engine.
+   * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT).
    */
-  SharedAssertionsMap d_sharedAssertions;
+  SharedLiteralsInMap d_sharedLiteralsIn;
 
   /**
-   * Assert a shared equalities propagated by theories.
+   * Map from literals asserted by theory engine to literal that can explain
    */
-  void assertSharedEqualities();
+  typedef context::CDHashMap<NodeTheoryPair, Node, NodeTheoryPairHashFunction> AssertedLiteralsOutMap;
+
+  /**
+   * All literals asserted to theories from theory engine.
+   * Maps from literal/theory pair to literal that can explain this assertion.
+   */
+  AssertedLiteralsOutMap d_assertedLiteralsOut;
+
+  /**
+   * Shared literals queud up to be asserted to the individual theories.
+   */
+  std::vector<SharedLiteral> d_propagatedSharedLiterals;
+
+  void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory)
+  {
+    d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
+  }
+
+  /**
+   * Assert the shared literals that are queued up to the theories.
+   */
+  void outputSharedLiterals();
 
   /**
    * Literals that are propagated by the theory. Note that these are TNodes.
@@ -336,11 +374,6 @@ class TheoryEngine {
   context::CDO<unsigned> d_propagatedLiteralsIndex;
 
   /**
-   * Shared term equalities that should be asserted to the individual theories.
-   */
-  std::vector<SharedEquality> d_propagatedEqualities;
-
-  /**
    * Decisions that are requested via propagateAsDecision().  The theory
    * can only request decisions on nodes that have an assigned litearl in
    * the SAT solver and are hence referenced in the SAT solver (making the
@@ -466,6 +499,20 @@ public:
     return d_propEngine;
   }
 
+private:
+
+  /**
+   * Helper for preprocess
+   */
+  Node ppTheoryRewrite(TNode term);
+
+public:
+
+  /**
+   * Signal the start of a new round of assertion preprocessing
+   */
+  void preprocessStart();
+
   /**
    * Runs theory specific preprocesssing on the non-Boolean parts of
    * the formula.  This is only called on input assertions, after ITEs
@@ -519,15 +566,6 @@ public:
   void preRegister(TNode preprocessed);
 
   /**
-   * Call the theories to perform one last rewrite on the theory atoms
-   * if they wish. This last rewrite is only performed on the input atoms.
-   * At this point it is ensured that atoms do not contain any Boolean
-   * strucure, i.e. there is no ITE nodes in them.
-   *
-   */
-  Node preCheckRewrite(TNode node);
-
-  /**
    * Assert the formula to the appropriate theory.
    * @param node the assertion
    */
@@ -568,6 +606,7 @@ public:
 
   void getPropagatedLiterals(std::vector<TNode>& literals) {
     for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) {
+      Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl;
       literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]);
     }
   }
@@ -589,8 +628,40 @@ public:
   bool properPropagation(TNode lit) const;
   bool properExplanation(TNode node, TNode expl) const;
 
+  enum ExplainTaskKind {
+    // Literal sent out from the theory engine
+    SHARED_LITERAL_OUT,
+    // Explanation produced by a theory
+    THEORY_EXPLANATION,
+    // Explanation produced by the shared terms database
+    SHARED_DATABASE_EXPLANATION
+  };
+
+  struct ExplainTask {
+    Node node;
+    ExplainTaskKind kind;
+    theory::TheoryId theory;
+    ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) :
+      node(n), kind(k), theory(tid) {}
+    bool operator == (const ExplainTask& other) const {
+      return node == other.node && kind == other.kind && theory == other.theory;
+    }
+  };
+
+  struct ExplainTaskHashFunction {
+    size_t operator () (const ExplainTask& task) const {
+      size_t hash = 0;
+      hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node);
+      hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2);
+      hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2);
+      return hash;
+    }
+  };
+
   Node getExplanation(TNode node);
 
+  Node explain(ExplainTask toExplain);
+
   Node getValue(TNode node);
 
   /**
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index d8757926a..4eabf63de 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -558,6 +558,11 @@ private:
   /** The false node */
   Node d_false;
 
+  /**
+   * Adds an equality of terms t1 and t2 to the database.
+   */
+  void addEqualityInternal(TNode t1, TNode t2, TNode reason);
+
 public:
 
   /**
@@ -617,6 +622,11 @@ public:
   bool hasTerm(TNode t) const;
 
   /**
+   * Adds aa predicate t with given polarity
+   */
+  void addPredicate(TNode t, bool polarity, TNode reason);
+
+  /**
    * Adds an equality t1 = t2 to the database.
    */
   void addEquality(TNode t1, TNode t2, TNode reason);
@@ -693,6 +703,13 @@ public:
    * Check whether the two term are dis-equal.
    */
   bool areDisequal(TNode t1, TNode t2);
+
+  /**
+   * Return the number of nodes in the equivalence class contianing t
+   * Adds t if not already there.
+   */
+  size_t getSize(TNode t);
+
 };
 
 } // Namespace uf
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index dd1bf0cbc..be12e5f19 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -188,9 +188,9 @@ const EqualityNode& EqualityEngine<NotifyClass>::getEqualityNode(EqualityNodeId
 }
 
 template <typename NotifyClass>
-void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+void EqualityEngine<NotifyClass>::addEqualityInternal(TNode t1, TNode t2, TNode reason) {
 
-  Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << "EqualityEngine::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl;
 
   // Add the terms if they are not already in the database
   addTerm(t1);
@@ -200,19 +200,39 @@ void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason)
   EqualityNodeId t1Id = getNodeId(t1);
   EqualityNodeId t2Id = getNodeId(t2);
   enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
+
   propagate();
 }
 
 template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addPredicate(TNode t, bool polarity, TNode reason) {
+
+  Debug("equality") << "EqualityEngine::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
+
+  addEqualityInternal(t, polarity ? d_true : d_false, reason);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+
+  Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+
+  addEqualityInternal(t1, t2, reason);
+
+  Node equality = t1.eqNode(t2);
+  addEqualityInternal(equality, d_true, reason);
+}
+
+template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::addDisequality(TNode t1, TNode t2, TNode reason) {
 
   Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl;
 
   Node equality1 = t1.eqNode(t2);
-  addEquality(equality1, d_false, reason);
-
+  addEqualityInternal(equality1, d_false, reason);
+ 
   Node equality2 = t2.eqNode(t1);
-  addEquality(equality2, d_false, reason);
+  addEqualityInternal(equality2, d_false, reason);
 }
 
 
@@ -516,9 +536,6 @@ void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vecto
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms (they might not be there)
   addTerm(t1);
   addTerm(t2);
@@ -537,8 +554,6 @@ void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vecto
   EqualityNodeId t2Id = getNodeId(t2);
   getExplanation(t1Id, t2Id, equalities);
 
-  // Pop the possible extra information
-  d_context->pop();
 }
 
 template <typename NotifyClass>
@@ -548,9 +563,6 @@ void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::ve
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms
   addTerm(t1);
   addTerm(t2);
@@ -573,8 +585,6 @@ void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::ve
   EqualityNodeId falseId = getNodeId(d_false);
   getExplanation(equalityId, falseId, equalities);
 
-  // Pop the possible extra information
-  d_context->pop();
 }
 
 
@@ -722,6 +732,10 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t
     }
   }
 
+  if (Debug.isOn("equality::internal")) {
+    debugPrintGraph();
+  }
+
   Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
 }
 
@@ -809,17 +823,11 @@ bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2)
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms
   addTerm(t1);
   addTerm(t2);
   bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
 
-  // Pop the context (triggers new term removal)
-  d_context->pop();
-
   // Return whether the two terms are equal
   return equal;
 }
@@ -830,9 +838,6 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms
   addTerm(t1);
   addTerm(t2);
@@ -841,18 +846,22 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   Node equality = t1.eqNode(t2);
   addTerm(equality);
   if (getEqualityNode(equality).getFind() == getEqualityNode(d_false).getFind()) {
-    d_context->pop();
     return true;
   }
 
-  // Pop the context (triggers new term removal)
-  d_context->pop();
-
   // Return whether the terms are disequal
   return false;
 }
 
 template <typename NotifyClass>
+size_t EqualityEngine<NotifyClass>::getSize(TNode t)
+{
+  // Add the term
+  addTerm(t);
+  return getEqualityNode(getEqualityNode(t).getFind()).getSize();
+}
+
+template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::addTriggerTerm(TNode t) 
 {
   Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 4ac81bc74..f53918683 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -96,11 +96,11 @@ void TheoryUF::check(Effort level) {
       d_equalityEngine.addEquality(fact[0], fact[1], fact);
       break;
     case kind::APPLY_UF:
-      d_equalityEngine.addEquality(fact, d_true, fact);
+      d_equalityEngine.addPredicate(fact, true, fact);
       break;
     case kind::NOT:
       if (fact[0].getKind() == kind::APPLY_UF) {
-        d_equalityEngine.addEquality(fact[0], d_false, fact);
+        d_equalityEngine.addPredicate(fact[0], false, fact);
       } else {
         // Assert the dis-equality
         d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
@@ -132,24 +132,21 @@ void TheoryUF::propagate(Effort level) {
       TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
       Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
       bool satValue;
-      if (!d_valuation.hasSatValue(literal, satValue)) {
+      Node normalized = Rewriter::rewrite(literal);
+      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
         d_out->propagate(literal);
       } else {
-        if (!satValue) {
-          Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl;
-          Node negatedLiteral;
-          std::vector<TNode> assumptions;
-          if (literal != d_false) {
-            negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
-            assumptions.push_back(negatedLiteral);
-          }
-          explain(literal, assumptions);
-          d_conflictNode = mkAnd(assumptions);
-          d_conflict = true;
-          break;
-        } else {
-          Debug("uf") << "TheoryUF::propagate(): already asserted" << std::endl;
+        Debug("uf") << "TheoryUF::propagate(): in conflict, normalized = " << normalized << std::endl;
+        Node negatedLiteral;
+        std::vector<TNode> assumptions;
+        if (normalized != d_false) {
+          negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+          assumptions.push_back(negatedLiteral);
         }
+        explain(literal, assumptions);
+        d_conflictNode = mkAnd(assumptions);
+        d_conflict = true;
+        break;
       }
     }
   }
@@ -196,20 +193,18 @@ bool TheoryUF::propagate(TNode literal) {
   }
 
   // See if the literal has been asserted already
+  Node normalized = Rewriter::rewrite(literal);
   bool satValue = false;
-  bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue);
+  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
 
   // If asserted, we're done or in conflict
   if (isAsserted) {
-    if (satValue) {
-      Debug("uf") << "TheoryUF::propagate(" << literal << ") => already known" << std::endl;
-      return true;
-    } else {
-      Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl;
+    if (!satValue) {
+      Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
       std::vector<TNode> assumptions;
       Node negatedLiteral;
-      if (literal != d_false) {
-        negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
         assumptions.push_back(negatedLiteral);
       }
       explain(literal, assumptions);
@@ -217,6 +212,8 @@ bool TheoryUF::propagate(TNode literal) {
       d_conflict = true;
       return false;
     }
+    // Propagate even if already known in SAT - could be a new equation between shared terms
+    // (terms that weren't shared when the literal was asserted!)
   }
 
   // Nothing, just enqueue it for propagation and mark it as asserted already
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 627125a27..5eb4f0dc7 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -79,9 +79,9 @@ Node Valuation::getSatValue(TNode n) const {
 }
 
 bool Valuation::hasSatValue(TNode n, bool& value) const {
-  Node normalized = Rewriter::rewrite(n);
-  if (d_engine->getPropEngine()->isSatLiteral(normalized)) {
-    return d_engine->getPropEngine()->hasValue(normalized, value);
+  //  Node normalized = Rewriter::rewrite(n);
+  if (d_engine->getPropEngine()->isSatLiteral(n)) {
+    return d_engine->getPropEngine()->hasValue(n, value);
   } else {
     return false;
   }