Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.

http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5

5 files changed, 180 insertions, 129 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 5093e5a7b..4cd54a2bf 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -62,14 +62,14 @@ void EqualityEngine::init() {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
+  d_triggerDatabaseAllocatedSize = 100000;
+  d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
+
   addTerm(d_true);
   addTerm(d_false);
 
   d_trueId = getNodeId(d_true);
   d_falseId = getNodeId(d_false);  
-
-  d_triggerDatabaseAllocatedSize = 100000;
-  d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
 } 
 
 EqualityEngine::~EqualityEngine() throw(AssertionException) {
@@ -114,7 +114,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 }
 
 void EqualityEngine::enqueue(const MergeCandidate& candidate) {
-    d_propagationQueue.push(candidate);
+  Debug("equality") << "EqualityEngine::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
+  d_propagationQueue.push(candidate);
 }
 
 EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) {
@@ -144,7 +145,15 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
     if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) {
       if (t1ClassId != t2ClassId) {
         Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl;
+        Assert(d_nodes[funId].getKind() == kind::EQUAL);
         enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+        // Also enqueue the symmetric one
+        TNode eq = d_nodes[funId];
+        Node symmetricEq = eq[1].eqNode(eq[0]);
+        if (hasTerm(symmetricEq)) {
+          EqualityNodeId symmFunId = getNodeId(symmetricEq);
+          enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));              
+        }
       }
     }
   } else {
@@ -154,8 +163,8 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
   }
 
   // Add to the use lists
-  d_equalityNodes[t1ClassId].usedIn<USE_LIST_FUNCTIONS>(funId, d_useListNodes);
-  d_equalityNodes[t2ClassId].usedIn<USE_LIST_FUNCTIONS>(funId, d_useListNodes);
+  d_equalityNodes[t1].usedIn(funId, d_useListNodes);
+  d_equalityNodes[t2].usedIn(funId, d_useListNodes);
 
   // Return the new id
   Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
@@ -238,6 +247,20 @@ void EqualityEngine::addTerm(TNode t) {
     // We set this here as this only applies to actual terms, not the
     // intermediate application terms
     d_isBoolean[result] = true;
+  } else if (t.isConst()) {
+    // Non-Boolean constants are trigger terms for all tags
+    EqualityNodeId tId = getNodeId(t);
+    d_newSetTags = 0;
+    d_newSetTriggersSize = THEORY_LAST;
+    for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
+      d_newSetTags = Theory::setInsert(currentTheory, d_newSetTags);
+      d_newSetTriggers[currentTheory] = tId;
+    } 
+    // Add it to the list for backtracking
+    d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
+    d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+    // Mark the the new set as a trigger 
+    d_nodeIndividualTrigger[tId] = newTriggerTermSet();
   }
 
   propagate();
@@ -319,15 +342,20 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
     assertEqualityInternal(eq, d_false, reason);
     propagate();    
     assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason);
-    propagate();
+    propagate();    
   
     if (d_done) {
       return;
     }
   
-    // If we are adding a disequality, notify of the shared term representatives
+    // If both have constant representatives, we don't notify anyone
     EqualityNodeId a = getNodeId(eq[0]);
     EqualityNodeId b = getNodeId(eq[1]);
+    if (isConstant(a) && isConstant(b)) {
+      return;
+    }    
+    
+    // If we are adding a disequality, notify of the shared term representatives
     EqualityNodeId eqId = getNodeId(eq);
     TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[a];
     TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[b];
@@ -356,6 +384,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
           d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b));
           d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId));
           storePropagatedDisequality(d_nodes[aSharedId], d_nodes[bSharedId], 3);
+
           // We notify even if the it's already been sent (they are not 
           // disequal at assertion, and we need to notify for each tag) 
           if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) {
@@ -383,7 +412,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
 
   Assert(triggersFired.empty());
-
+  
   ++ d_stats.mergesCount;
 
   EqualityNodeId class1Id = class1.getFind();
@@ -391,6 +420,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   // Check for constant merges
   bool isConstant = d_isConstant[class1Id];
+  Assert(isConstant || !d_isConstant[class2Id]);
 
   // Update class2 representative information
   Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl;
@@ -438,13 +468,13 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
  
       // Go through the uselist and check for congruences
-      UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>();
+      UseListNodeId currentUseId = currentNode.getUseList();
       while (currentUseId != null_uselist_id) {
         // Get the node of the use list
         UseListNode& useNode = d_useListNodes[currentUseId];
         // Get the function application
         EqualityNodeId funId = useNode.getApplicationId();
-        Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
+        Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
         const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
         // Check if there is an application with find arguments
         EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
@@ -460,11 +490,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           // There is no representative, so we can add one, we remove this when backtracking
           storeApplicationLookup(funNormalized, funId);
           // Now, if we're constant and it's an equality, check if the other guy is also a constant
-          if (isConstant && funNormalized.isEquality) {
-            if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) {
-              // both constants
-              if (funNormalized.a != funNormalized.b) {
-                enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+          if (funNormalized.isEquality) {
+            if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) {
+              Assert(d_nodes[funId].getKind() == kind::EQUAL);
+              enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+              // Also enqueue the symmetric one
+              TNode eq = d_nodes[funId];
+              Node symmetricEq = eq[1].eqNode(eq[0]);
+              if (hasTerm(symmetricEq)) {
+                EqualityNodeId symmFunId = getNodeId(symmetricEq);
+                enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));              
               }
             }
           }          
@@ -482,6 +517,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   // Now merge the lists
   class1.merge<true>(class2);
 
+  // Notify of the constants merge
+  bool constantMerge = false;
+  if (isConstant && d_isConstant[class2Id]) {
+    constantMerge = true;
+    if (d_performNotify) {
+      if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) {
+        return false;
+      }
+    }
+  }
+
   // Go through the triggers and store the dis-equalities
   unsigned i = 0, j = 0;
   for (; i < triggersFired.size();) {
@@ -543,7 +589,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           // copy tag1 
           EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
           // since they are both tagged notify of merge
-          if (d_performNotify) {
+          if (d_performNotify && !constantMerge) {
             EqualityNodeId tag2id = class2triggers.triggers[i2++];
             if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
               return false;
@@ -566,15 +612,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
     }	
   }
 
-  // Notify of the constants merge
-  if (isConstant && d_isConstant[class2Id]) {
-    if (d_performNotify) {
-      if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) {
-        return false;
-      }
-    }
-  }
-
   // Everything fine
   return true;
 }
@@ -680,12 +717,12 @@ void EqualityEngine::backtrack() {
       Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl;
       d_nodeIds.erase(d_nodes[i]);
 
-      const FunctionApplication& app = d_applications[i].normalized;
+      const FunctionApplication& app = d_applications[i].original;
       if (app.isApplication()) {
         // Remove b from use-list
-        getEqualityNode(app.b).removeTopFromUseList<USE_LIST_FUNCTIONS>(d_useListNodes);
+        getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
         // Remove a from use-list
-        getEqualityNode(app.a).removeTopFromUseList<USE_LIST_FUNCTIONS>(d_useListNodes);
+        getEqualityNode(app.a).removeTopFromUseList(d_useListNodes);
       }
     }
 
@@ -818,8 +855,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
     // Go through the equality edges of this node
     EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
-    Debug("equality") << "EqualityEngine::getExplanation(): edgesId =  " << currentEdge << std::endl;
-    Debug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
+    if (Debug.isOn("equality")) {
+      Debug("equality") << "EqualityEngine::getExplanation(): edgesId =  " << currentEdge << std::endl;
+      Debug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
+    }
 
     while (currentEdge != null_edge) {
       // Get the edge
@@ -871,8 +910,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               
               Debug("equality") << push;
               // Explain why a is a constant
+              Assert(isConstant(eq.a));
               getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities);
               // Explain why b is a constant
+              Assert(isConstant(eq.b));
               getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities);
               Debug("equality") << pop;
             
@@ -1062,7 +1103,7 @@ void EqualityEngine::propagate() {
 
     // Depending on the merge preference (such as size, or being a constant), merge them
     std::vector<TriggerId> triggers;
-    if (node2.getSize() > node1.getSize() || d_isConstant[t2classId]) {
+    if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) {
       Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t2classId, t1classId));
       if (!merge(node2, node1, triggers)) {
@@ -1222,7 +1263,7 @@ size_t EqualityEngine::getSize(TNode t)
 
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
-  Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
+  Debug("equality::trigger") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
   Assert(tag != THEORY_LAST);
 
   if (d_done) {
@@ -1243,12 +1284,71 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
     // If the term already is in the equivalence class that a tagged representative, just notify
     if (d_performNotify) {
       EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
-      if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
+      if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
         d_done = true;
       }
     }
   } else {
 
+    // Check for disequalities by going through the equivalence class looking for equalities in the
+    // uselists that have been asserted to false. All the representatives appearing on the other
+    // side of such disequalities, that have the tag on, are put in a set.
+    std::set<EqualityNodeId> disequalSet;
+    EqualityNodeId currentId = classId;
+    do {
+      // Current node
+      EqualityNode& currentNode = getEqualityNode(currentId);
+      // Go through the uselist and look for disequalities
+      UseListNodeId currentUseId = currentNode.getUseList();
+      while (!d_done && currentUseId != null_uselist_id) {
+        // Get the normalized equality
+        UseListNode& useNode = d_useListNodes[currentUseId];
+        EqualityNodeId funId = useNode.getApplicationId();
+        const FunctionApplication& fun = d_applications[useNode.getApplicationId()].original;
+        // Check for asserted disequalities
+        if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) {
+          // Get the other equality member
+          EqualityNodeId toCompare = fun.b;
+          if (toCompare == currentId) {
+            toCompare = fun.a;
+          }
+          // Representative of the other member
+          EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind();
+          Assert(toCompareRep != classId);
+          // Get the trigger set
+          TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep];
+          // Only notify if we're not both constants
+          if ((!d_isConstant[classId] || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) {
+            TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef);
+            if (Theory::setContains(tag, toCompareTriggerSet.tags)) {
+              // Get the tag representative
+              EqualityNodeId tagRep = toCompareTriggerSet.getTrigger(tag);
+              // Propagate the disequality if not already done
+              if (!disequalSet.count(tagRep) && d_performNotify) {
+                // Mark as propagated
+                disequalSet.insert(tagRep);
+                // Store the propagation
+                d_deducedDisequalityReasons.push_back(EqualityPair(eqNodeId, currentId));
+                d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep));
+                d_deducedDisequalityReasons.push_back(EqualityPair(funId, d_falseId));
+                storePropagatedDisequality(t, d_nodes[tagRep], 3);
+                // We don't check if it's been propagated already, as we need one per tag
+                if (d_performNotify) {
+                  if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[tagRep], false)) {
+                    d_done = true;
+                  }
+                }
+              }
+            }
+          }
+        }
+        // Go to the next one in the use list
+        currentUseId = useNode.getNext();
+      }
+      // Next in equivalence class
+      currentId = currentNode.getNext();
+    } while (!d_done && currentId != classId);
+
     // Setup the data for the new set
     if (triggerSetRef != null_set_id) {
       // Get the existing set
@@ -1322,7 +1422,7 @@ void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
       // Get the current node
       EqualityNode& currentNode = getEqualityNode(currentId);
       // Go through the use-list
-      UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>();
+      UseListNodeId currentUseId = currentNode.getUseList();
       while (currentUseId != null_uselist_id) {
         // Get the node of the use list
         UseListNode& useNode = d_useListNodes[currentUseId];
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 5ff8ee4dc..f40c79df3 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -345,6 +345,13 @@ private:
   std::vector<bool> d_isConstant;
 
   /**
+   * Returns true if it's a constant
+   */
+  bool isConstant(EqualityNodeId id) const {
+    return d_isConstant[getEqualityNode(id).getFind()];
+  }
+
+  /**
    * Map from ids to wheather they are Boolean.
    */
   std::vector<bool> d_isBoolean;
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 0baf70fcf..056ee0b84 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -94,8 +94,9 @@ struct MergeCandidate {
   EqualityNodeId t1Id, t2Id;
   MergeReasonType type;
   TNode reason;
-  MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason):
-    t1Id(x), t2Id(y), type(type), reason(reason) {}
+  MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason)
+  : t1Id(x), t2Id(y), type(type), reason(reason) 
+  {}
 };
 
 /**
@@ -145,15 +146,6 @@ public:
   }
 };
 
-/** Main types of uselists */
-enum UseListType {
-  /** Use list of functions where the term appears in */
-  USE_LIST_FUNCTIONS,
-  /** Use list of asserted disequalities */
-  USE_LIST_DISEQUALITIES
-};
-
-
 /**
  * Main class for representing nodes in the equivalence class. The 
  * nodes are a circular list, with the representative carrying the
@@ -178,9 +170,6 @@ private:
   /** The use list of this node */
   UseListNodeId d_useList;
 
-  /** The list of asserted disequalities that this node appears in */
-  UseListNodeId d_diseqList;
-
 public:
 
   /**
@@ -191,15 +180,13 @@ public:
   , d_findId(nodeId) 
   , d_nextId(nodeId)
   , d_useList(null_uselist_id)
-  , d_diseqList(null_uselist_id)
   {}
 
   /**
    * Returns the requested uselist.
    */
-  template<UseListType type>
   UseListNodeId getUseList() const {
-    return type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
+    return d_useList;
   }
 
   /**
@@ -244,22 +231,20 @@ public:
    * Note that this node is used in a function application funId, or
    * a negatively asserted equality (dis-equality) with funId. 
    */
-  template<UseListType type, typename memory_class>
+  template<typename memory_class>
   void usedIn(EqualityNodeId funId, memory_class& memory) {
-    UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
     UseListNodeId newUseId = memory.size();
-    memory.push_back(UseListNode(funId, useList));
-    useList = newUseId;
+    memory.push_back(UseListNode(funId, d_useList));
+    d_useList = newUseId;
   }
 
   /**
    * For backtracking: remove the first element from the uselist and pop the memory.
    */
-  template<UseListType type, typename memory_class>
+  template<typename memory_class>
   void removeTopFromUseList(memory_class& memory) {
-    UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
-    Assert ((int) useList == (int)memory.size() - 1);
-    useList = memory.back().getNext();
+    Assert ((int) d_useList == (int)memory.size() - 1);
+    d_useList = memory.back().getNext();
     memory.pop_back();
   }
 };
@@ -288,7 +273,7 @@ struct FunctionApplication {
   FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id)
   : isEquality(isEquality), a(a), b(b) {}
   bool operator == (const FunctionApplication& other) const {
-    return a == other.a && b == other.b;
+    return isEquality == other.isEquality && a == other.a && b == other.b;
   }
   bool isApplication() const {
     return a != null_id && b != null_id;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ae8bdc8da..7583f8ee7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -70,16 +70,6 @@ void TheoryUF::check(Effort level) {
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
 
-    // If the assertion doesn't have a literal, it's a shared equality, so we set it up
-    if (!assertion.isPreregistered) {
-      Debug("uf") << "TheoryUF::check(): shared equality, setting up " << fact << std::endl;
-      if (fact.getKind() == kind::NOT) {
-        preRegisterTerm(fact[0]);
-      } else {
-        preRegisterTerm(fact);
-      }
-    }
-
     // Do the work
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
@@ -90,31 +80,8 @@ void TheoryUF::check(Effort level) {
     }
   }
 
-  // If in conflict, output the conflict
-  if (d_conflict) {
-    Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl;
-    d_out->conflict(d_conflictNode);
-  }
-
-  // Otherwise we propagate in order to detect a weird conflict like
-  // p, x = y
-  // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time
-  // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict
-  // until we go through the propagation list
-  propagate(level);
 }/* TheoryUF::check() */
 
-void TheoryUF::propagate(Effort level) {
-  Debug("uf") << "TheoryUF::propagate()" << std::endl;
-  if (!d_conflict) {
-    for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
-      TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-      Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
-      d_out->propagate(literal);
-    }
-  }
-}/* TheoryUF::propagate(Effort) */
-
 void TheoryUF::preRegisterTerm(TNode node) {
   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 
@@ -143,37 +110,18 @@ void TheoryUF::preRegisterTerm(TNode node) {
 }/* TheoryUF::preRegisterTerm() */
 
 bool TheoryUF::propagate(TNode literal) {
-  Debug("uf") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
-
+  Debug("uf::propagate") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("uf") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
     return false;
   }
-
-  // See if the literal has been asserted already
-  Node normalized = Rewriter::rewrite(literal);
-
-  // If asserted and is false, we're done or in conflict
-  // Note that even trivial equalities have a SAT value (i.e. 1 = 2 -> false)
-  bool satValue = false;
-  if (d_valuation.hasSatValue(normalized, satValue) && !satValue) {
-      Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
-      std::vector<TNode> assumptions;
-      Node negatedLiteral;
-      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 out
+  bool ok = d_out->propagate(literal);
+  if (!ok) {
+    d_conflict = true;
   }
-
-  // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("uf") << "TheoryUF::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
-  d_literalsToPropagate.push_back(literal);
-
-  return true;
+  return ok;
 }/* TheoryUF::propagate(TNode) */
 
 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
@@ -437,3 +385,13 @@ void TheoryUF::computeCareGraph() {
     }
   }
 }/* TheoryUF::computeCareGraph() */
+
+void TheoryUF::conflict(TNode a, TNode b) {
+  if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+    d_conflictNode = explain(a.iffNode(b));
+  } else {
+    d_conflictNode = explain(a.eqNode(b));
+  }
+  d_out->conflict(d_conflictNode);
+  d_conflict = true;
+}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 1dfcb86f0..0d35d57d8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -55,7 +55,7 @@ public:
     }
 
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         return d_uf.propagate(predicate);
       } else {
@@ -64,7 +64,7 @@ public:
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl;
+      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         return d_uf.propagate(t1.eqNode(t2));
       } else {
@@ -73,12 +73,9 @@ public:
     }
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
-      if (Theory::theoryOf(t1) == THEORY_BOOL) {
-        return d_uf.propagate(t1.iffNode(t2));
-      } else {
-        return d_uf.propagate(t1.eqNode(t2));
-      }
+      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+      d_uf.conflict(t1, t2);
+      return false;
     }
   };
 
@@ -119,13 +116,15 @@ private:
   /** Symmetry analyzer */
   SymmetryBreaker d_symb;
 
+  /** Conflict when merging two constants */
+  void conflict(TNode a, TNode b);
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
   TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
 
   void check(Effort);
-  void propagate(Effort);
   void preRegisterTerm(TNode term);
   Node explain(TNode n);
 
@@ -135,6 +134,8 @@ public:
   void addSharedTerm(TNode n);
   void computeCareGraph();
 
+  void propagate(Effort effort) {}
+
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   std::string identify() const {