From 21f9e53792ba5f94594fccb7bef880aa77b266cb Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Sun, 27 May 2012 16:59:01 +0000
Subject: [PATCH] some reordering to keep invariants

---
 src/theory/uf/equality_engine.cpp | 30 +++++++++++++++++++-----------
 1 file changed, 19 insertions(+), 11 deletions(-)

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 72966d0b3..5093e5a7b 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -414,17 +414,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         trigger.classId = class1Id;
         // If they became the same, call the trigger
         if (otherTrigger.classId == class1Id) {
-          const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[currentTrigger];
-          if (triggerInfo.trigger.getKind() == kind::EQUAL && !triggerInfo.polarity) {
-            TNode equality = triggerInfo.trigger;
-            EqualityNodeId original = getNodeId(equality);
-            d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId));
-            if (!storePropagatedDisequality(equality[0], equality[1], 1)) {
-              // Go to the next trigger
-              currentTrigger = trigger.nextTrigger;
-              continue;
-            }
-          }
           // Id of the real trigger is half the internal one
           triggersFired.push_back(currentTrigger);
         }
@@ -492,6 +481,25 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
     
   // Now merge the lists
   class1.merge<true>(class2);
+
+  // Go through the triggers and store the dis-equalities
+  unsigned i = 0, j = 0;
+  for (; i < triggersFired.size();) {
+    const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggersFired[i]];
+    if (triggerInfo.trigger.getKind() == kind::EQUAL && !triggerInfo.polarity) {
+      TNode equality = triggerInfo.trigger;
+      EqualityNodeId original = getNodeId(equality);
+      d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId));
+      if (!storePropagatedDisequality(equality[0], equality[1], 1)) {
+        // Already notified, go to the next trigger
+        ++ i;
+        continue;
+      }
+    }
+    // Copy
+    triggersFired[j++] = triggersFired[i++];
+  }
+  triggersFired.resize(j);
   
   // Notify the trigger term merges
   TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
-- 
2.30.2