11 files changed, 260 insertions, 126 deletions

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 5e4616628..5f49ab3ab 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -65,12 +65,12 @@ private:
       }
     }
 
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
       if (t1.getKind() == kind::CONST_BOOLEAN) {
-        return d_acm.propagate(t1.iffNode(t2));
+        d_acm.propagate(t1.iffNode(t2));
       } else {
-        return d_acm.propagate(t1.eqNode(t2));
+        d_acm.propagate(t1.eqNode(t2));
       }
     }
    };
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 3ae0146c1..54d20d478 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -266,10 +266,9 @@ class TheoryArrays : public Theory {
       return true;
     }
 
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_arrays.conflict(t1, t2);
-      return false;
     }
   };
 
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 98678a9b4..afb4a8b4a 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -29,7 +29,7 @@ using namespace CVC4::theory::bv::utils;
 
 EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
-    d_notify(bv),
+    d_notify(*this),
     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV")
 {
   if (d_useEqualityEngine) {
@@ -127,34 +127,41 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory:
 bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
   BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
   if (value) {
-    return d_bv->storePropagation(equality, TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(equality);
   } else {
-    return d_bv->storePropagation(equality.notNode(), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(equality.notNode());
   }
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
   BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
   if (value) {
-    return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(predicate);
   } else {
-    return d_bv->storePropagation(predicate.notNode(), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(predicate.notNode());
   }
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
   Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
   if (value) {
-    return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(t1.eqNode(t2));
   } else {
-    return d_bv->storePropagation(t1.eqNode(t2).notNode(), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(t1.eqNode(t2).notNode());
   }
 }
 
-bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-  if (Theory::theoryOf(t1) == THEORY_BOOL) {
-    return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY);
-  }
-  return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+  d_solver.conflict(t1, t2);
+}
+
+bool EqualitySolver::storePropagation(TNode literal) {
+  return d_bv->storePropagation(literal, TheoryBV::SUB_EQUALITY);
 }
+  
+void EqualitySolver::conflict(TNode a, TNode b) {
+  std::vector<TNode> assumptions;
+  d_equalityEngine.explainEquality(a, b, true, assumptions);
+  d_bv->setConflict(mkAnd(assumptions));
+}
+
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index 356d12a06..d4239ff13 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -32,14 +32,14 @@ class EqualitySolver : public SubtheorySolver {
   // NotifyClass: handles call-back from congruence closure module
 
   class NotifyClass : public eq::EqualityEngineNotify {
-    TheoryBV* d_bv;
+    EqualitySolver& d_solver;
 
   public:
-    NotifyClass(TheoryBV* bv): d_bv(bv) {}
+    NotifyClass(EqualitySolver& solver): d_solver(solver) {}
     bool eqNotifyTriggerEquality(TNode equality, bool value);
     bool eqNotifyTriggerPredicate(TNode predicate, bool value);
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2);
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
 };
 
 
@@ -49,6 +49,12 @@ class EqualitySolver : public SubtheorySolver {
   /** Equality engine */
   eq::EqualityEngine d_equalityEngine;
 
+  /** Store a propagation to the bv solver */
+  bool storePropagation(TNode literal);
+  
+  /** Store a conflict from merging two constants */
+  void conflict(TNode a, TNode b);
+
 public:
 
   EqualitySolver(context::Context* c, TheoryBV* bv);
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 1a38d7332..fccd2e6bc 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -92,9 +92,8 @@ private:
       return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
     }
 
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       d_sharedTerms.conflict(t1, t2, true);
-      return false;
     }
   };
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a7b13dc2f..0be232bfa 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -763,13 +763,17 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
       d_factsAsserted = true;      
     } else {
       Assert(toTheoryId == THEORY_SAT_SOLVER);
-      // Enqueue for propagation to the SAT solver
-      d_propagatedLiterals.push_back(assertion);
       // Check for propositional conflict
       bool value;
-      if (d_propEngine->hasValue(assertion, value) && !value) {
-        d_inConflict = true;
-      }
+      if (d_propEngine->hasValue(assertion, value)) {
+        if (!value) {
+          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << std::endl;
+          d_inConflict = true;
+        } else {
+          return;
+        }
+      } 
+      d_propagatedLiterals.push_back(assertion);
     }
     return;
   }
@@ -994,7 +998,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
 
 Node TheoryEngine::getExplanation(TNode node) {
-  Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl;
+  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current proagation index = " << d_propagationMapTimestamp << std::endl;
 
   bool polarity = node.getKind() != kind::NOT;
   TNode atom = polarity ? node : node[0];
@@ -1165,8 +1169,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     } else {
       explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
     }
-    Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially");
     Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << std::endl;
+    Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially");
     // Mark the explanation
     NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
     explanationVector.push_back(newExplain);
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 1f45b7827..25645c472 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -91,6 +91,9 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 , d_triggerDatabaseSize(context, 0)
 , d_triggerTermSetUpdatesSize(context, 0)
 , d_deducedDisequalitiesSize(context, 0)
+, d_deducedDisequalityReasonsSize(context, 0)
+, d_propagatedDisequalities(context)
+, d_name(name)
 {
   init();
 }
@@ -109,6 +112,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 , d_triggerDatabaseSize(context, 0)
 , d_triggerTermSetUpdatesSize(context, 0)
 , d_deducedDisequalitiesSize(context, 0)
+, d_deducedDisequalityReasonsSize(context, 0)
+, d_propagatedDisequalities(context)
 , d_name(name)
 {
   init();
@@ -388,16 +393,21 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
           // Same tags, notify
           EqualityNodeId aSharedId = aTriggerTerms.triggers[a_i++];
           EqualityNodeId bSharedId = bTriggerTerms.triggers[b_i++];
-          d_deducedDisequalityReasons.push_back(EqualityPair(aSharedId, a));
-          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) 
-          Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl;
-          if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) {
-            break;
+          // Propagate
+          if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId)) {
+            // Store a proof if not there already
+            if (!hasPropagatedDisequality(aSharedId, bSharedId)) {
+              d_deducedDisequalityReasons.push_back(EqualityPair(aSharedId, a));
+              d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b));
+              d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId));
+            }
+            // Store the propagation
+            storePropagatedDisequality(aTag, aSharedId, bSharedId);
+            // Notify
+            Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl;
+            if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) {
+              break;
+            }
           }
           // Pop the next tags
           aTag = Theory::setPop(aTags);
@@ -431,6 +441,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   bool class1isConstant = d_isConstant[class1Id];
   bool class2isConstant = d_isConstant[class2Id];
   Assert(class1isConstant || !class2isConstant, "Should always merge into constants");
+  Assert(!class1isConstant || !class2isConstant, "Don't merge constants");
 
   // Trigger set of class 1
   TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
@@ -548,36 +559,6 @@ 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 (class1isConstant && 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();) {
-    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);
   
   // Go through the trigger term disequalities and propagate
   if (!propagateTriggerTermDisequalities(class1OnlyTags, class1triggerRef, class2disequalitiesToNotify)) {
@@ -627,7 +608,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 && !constantMerge) {
+          if (d_performNotify) {
             EqualityNodeId tag2id = class2triggers.triggers[i2++];
             if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
               return false;
@@ -704,7 +685,9 @@ void EqualityEngine::backtrack() {
       // Get the ids of the merged classes
       Equality& eq = d_assertedEqualities[i];
       // Undo the merge
-      undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs);
+      if (eq.lhs != null_id) {
+        undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs);
+      }
     }
 
     d_assertedEqualities.resize(d_assertedEqualitiesCount);
@@ -778,14 +761,13 @@ void EqualityEngine::backtrack() {
   if (d_deducedDisequalities.size() > d_deducedDisequalitiesSize) {
     for(int i = d_deducedDisequalities.size() - 1, i_end = (int)d_deducedDisequalitiesSize; i >= i_end; -- i) {
       EqualityPair pair = d_deducedDisequalities[i];
-      DisequalityReasonRef reason = d_disequalityReasonsMap[pair];
+      Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end());
       // Remove from the map
       d_disequalityReasonsMap.erase(pair);
       std::swap(pair.first, pair.second);
       d_disequalityReasonsMap.erase(pair);
-      // Resize the reasons vector
-      d_deducedDisequalityReasons.resize(reason.mergesStart);
     }
+    d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize);
     d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
   }
 }
@@ -859,7 +841,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
   // We can only explain the nodes that got merged
 #ifdef CVC4_ASSERTIONS
-  bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind();
+  bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind()
+                  || (d_done && isConstant(t1Id) && isConstant(t2Id));
+  
   if (!canExplain) {
     Warning() << "Can't explain equality:" << std::endl;
     Warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl;
@@ -954,7 +938,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Assert(isConstant(eq.b));
               getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities);
               Debug("equality") << pop;
-            
+              // If the constants were merged, we're in trouble
+              Assert(getEqualityNode(eq.a).getFind() != getEqualityNode(eq.b).getFind());
+
               break;
             }
             default:
@@ -1136,21 +1122,36 @@ void EqualityEngine::propagate() {
     // Add the actual equality to the equality graph
     addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
 
-    // One more equality added
-    d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+    // If constants are being merged we're done 
+    if (d_isConstant[t1classId] && d_isConstant[t2classId]) {
+      // When merging constants we are inconsistent, hence done
+      d_done = true;
+      // But in order to keep invariants (edges = 2*equalities) we put an equalities in
+      // Note that we can explain this merge as we have a graph edge
+      d_assertedEqualities.push_back(Equality(null_id, null_id));
+      d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+      // Notify
+      if (d_performNotify) {
+        d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], d_nodes[t2classId]);
+      }
+      // Empty the queue and exit
+      continue;
+    }
 
     // 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[t1classId]) || d_isConstant[t2classId]) {
       Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t2classId, t1classId));
+      d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
       if (!merge(node2, node1, triggers)) {
         d_done = true;
       }
     } else {
       Debug("equality") << d_name << "::eq::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t1classId, t2classId));
-      if (!merge(node1, node2, triggers)) {
+      d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+    if (!merge(node1, node2, triggers)) {
         d_done = true;
       }
     }
@@ -1159,10 +1160,30 @@ void EqualityEngine::propagate() {
     if (d_performNotify && !d_done) {
       for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
         const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]];
-        // Notify the trigger and exit if it fails
         if (triggerInfo.trigger.getKind() == kind::EQUAL) {
-          if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) {
-            d_done = true;
+          // Special treatment for disequalities
+          if (!triggerInfo.polarity) {
+            // Store that we are propagating a diseauality
+            TNode equality = triggerInfo.trigger;
+            EqualityNodeId original = getNodeId(equality);
+            TNode lhs = equality[0];
+            TNode rhs = equality[1];
+            EqualityNodeId lhsId = getNodeId(lhs);
+            EqualityNodeId rhsId = getNodeId(rhs);
+            if (!hasPropagatedDisequality(THEORY_BOOL, lhsId, rhsId)) {
+              if (!hasPropagatedDisequality(lhsId, rhsId)) {
+                d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId));
+              }
+              storePropagatedDisequality(THEORY_BOOL, lhsId, rhsId);
+              if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) {
+                d_done = true;
+              }
+            }
+          } else {
+            // Equalities are simple
+            if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) {
+              d_done = true;
+            }
           }
         } else {
           if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity)) {
@@ -1211,6 +1232,11 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
   EqualityNodeId t1Id = getNodeId(t1);
   EqualityNodeId t2Id = getNodeId(t2);
 
+  // If we propagated this disequality we're true
+  if (hasPropagatedDisequality(t1Id, t2Id)) {
+    return true;
+  }
+
   // Get equivalence classes
   EqualityNodeId t1ClassId = getEqualityNode(t1Id).getFind();
   EqualityNodeId t2ClassId = getEqualityNode(t2Id).getFind();
@@ -1223,7 +1249,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
     if (ensureProof) {
       nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, t1ClassId));
       nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId));
-      storePropagatedDisequality(t1, t2, 2);
+      nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
     }
     return true;
   }
@@ -1234,7 +1260,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
     if (getEqualityNode(eq).getFind() == getEqualityNode(d_falseId).getFind()) {
       if (ensureProof) {
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(getNodeId(eq), d_falseId));
-        storePropagatedDisequality(t1, t2, 1);
+        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       return true;
     }
@@ -1246,7 +1272,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
     if (getEqualityNode(eq).getFind() == getEqualityNode(d_false).getFind()) {
       if (ensureProof) {
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(getNodeId(eq), d_falseId));
-        storePropagatedDisequality(t1, t2, 1);
+        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       return true;
     }
@@ -1264,7 +1290,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.a, t1ClassId));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.b, t2ClassId));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
-        storePropagatedDisequality(t1, t2, 5);
+        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       return true;
     }
@@ -1282,7 +1308,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.a, t2ClassId));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(original.b, t1ClassId));
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
-        storePropagatedDisequality(t1, t2, 5);
+        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
       return true;
     }
@@ -1302,7 +1328,9 @@ size_t EqualityEngine::getSize(TNode t)
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
   Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
+
   Assert(tag != THEORY_LAST);
+  Assert(tag != THEORY_BOOL, "This one is used internally, bummer");
 
   if (d_done) {
     return;
@@ -1453,38 +1481,84 @@ EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet() {
   return newTriggerSetRef;
 }
 
-bool EqualityEngine::storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const {
+bool EqualityEngine::hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const {
+  EqualityPair eq(lhsId, rhsId);
+  bool propagated = d_propagatedDisequalities.find(eq) != d_propagatedDisequalities.end();
+#ifdef CVC4_ASSERTIONS
+  bool stored = d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end();
+  Assert(propagated == stored, "These two should be in sync");
+#endif
+  Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (propagated ? "true" : "false") << std::endl;
+  return propagated;
+}
+
+bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const {
 
-  Assert(reasonsCount > 0);
+  EqualityPair eq(lhsId, rhsId);
 
+  PropagatedDisequalitiesMap::const_iterator it = d_propagatedDisequalities.find(eq);
+  if (it == d_propagatedDisequalities.end()) {
+    Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end(), "Why do we have a proof if not propagated");
+    Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => false" << std::endl;
+    return false;
+  }
+  Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end(), "We propagated but there is no proof");
+  bool result = Theory::setContains(tag, (*it).second);
+  Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl;
+  return result;
+}
 
-  EqualityNodeId lhsId = getNodeId(lhs);
-  EqualityNodeId rhsId = getNodeId(rhs);
 
-  // We are semantically const, just remembering stuff for later
-  EqualityEngine* nonConst = const_cast<EqualityEngine*>(this);
+void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) {
 
-  Assert(d_deducedDisequalityReasons.size() >= reasonsCount);
-  DisequalityReasonRef ref(d_deducedDisequalityReasons.size() - reasonsCount, d_deducedDisequalityReasons.size());
+  Assert(!hasPropagatedDisequality(tag, lhsId, rhsId), "Check before you store it");
+  Assert(lhsId != rhsId, "Wow, wtf!");
 
-#ifdef CVC4_ASSERTIONS
-  for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) {
-    Assert(getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind());
+  Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ")" << std::endl;
+
+  EqualityPair pair1(lhsId, rhsId);
+  EqualityPair pair2(rhsId, lhsId);
+
+  // Store the fact that we've propagated this already
+  Theory::Set notified = 0;
+  PropagatedDisequalitiesMap::const_iterator find = d_propagatedDisequalities.find(pair1);
+  if (find == d_propagatedDisequalities.end()) {
+    notified = Theory::setInsert(tag);
+  } else {
+    notified = Theory::setInsert(tag, (*find).second);
   }
+  d_propagatedDisequalities[pair1] = notified;
+  d_propagatedDisequalities[pair2] = notified;
+
+  // Store the proof if provided
+  if (d_deducedDisequalityReasons.size() > d_deducedDisequalityReasonsSize) {
+    Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << "): storing proof" << std::endl;
+    Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end(), "There can't be a proof if you're adding a new one");
+    DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size());
+#ifdef CVC4_ASSERTIONS
+    // Check that the reasons are valid
+    for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) {
+      Assert(getEqualityNode(d_deducedDisequalityReasons[i].first).getFind() == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind());
+    }
 #endif
+    if (Debug.isOn("equality::disequality")) {
+      for (unsigned i = ref.mergesStart; i < ref.mergesEnd; ++ i) {
+        TNode lhs = d_nodes[d_deducedDisequalityReasons[i].first];
+        TNode rhs = d_nodes[d_deducedDisequalityReasons[i].second];
+        Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(): because " << lhs << " == " << rhs << std::endl;
+      }
 
-  EqualityPair pair(lhsId, rhsId);
-  DisequalityReasonsMap::const_iterator find = d_disequalityReasonsMap.find(pair);
-  if (find == d_disequalityReasonsMap.end()) {
-    nonConst->d_disequalityReasonsMap[pair] = ref;
-    nonConst->d_deducedDisequalities.push_back(pair);
-    nonConst->d_deducedDisequalitiesSize = d_deducedDisequalities.size();
-    std::swap(pair.first, pair.second);
-    nonConst->d_disequalityReasonsMap[pair] = ref;
-    return true;
+    }
+
+    // Store for backtracking
+    d_deducedDisequalities.push_back(pair1);
+    d_deducedDisequalitiesSize = d_deducedDisequalities.size();
+    d_deducedDisequalityReasonsSize = d_deducedDisequalityReasons.size();
+    // Store the proof reference
+    d_disequalityReasonsMap[pair1] = ref;
+    d_disequalityReasonsMap[pair2] = ref;
   } else {
-    nonConst->d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
-    return false;
+    Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end(), "You must provide a proof initially");
   }
 }
 
@@ -1583,21 +1657,32 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger
     // Figure out who we are comparing to in the original equality
     EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b;
     EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a;
+    if (getEqualityNode(toCompare).getFind() == getEqualityNode(myCompare).getFind()) {
+      // We're propagating a != a, which means we're inconsistent, just bail and let it go into
+      // a regular conflict
+      return !d_done;
+    }
     // Go through the tags, and add the disequalities
     TheoryId currentTag;
     while (!d_done && ((currentTag = Theory::setPop(commonTags)) != THEORY_LAST)) {
       // Get the tag representative
       EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag);
       EqualityNodeId myRep = triggerSet.getTrigger(currentTag);
-      // Store the propagation
-      d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep));
-      d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep));
-      d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId));
-      storePropagatedDisequality(d_nodes[myRep], 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(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) {
-          d_done = true;
+      // Propagate
+      if (!hasPropagatedDisequality(currentTag, myRep, tagRep)) {
+        // Construct the proof if not there already
+        if (!hasPropagatedDisequality(myRep, tagRep)) {
+          d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep));
+          d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep));
+          d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId));
+        }
+        // Store the propagation
+        storePropagatedDisequality(currentTag, myRep, tagRep);
+        // Notify
+        if (d_performNotify) {
+          if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) {
+            d_done = true;
+          }
         }
       }
     }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index ac6f458e9..8cf159cd7 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -78,12 +78,13 @@ public:
   virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0;
 
   /**
-   * Notifies about the merge of two constant terms.
+   * Notifies about the merge of two constant terms. After this, all work is suspended and all you 
+   * can do is ask for explanations.
    *
    * @param t1 a constant term
    * @param t2 a constnat term
    */
-  virtual bool eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
+  virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
 };
 
 /**
@@ -95,7 +96,7 @@ public:
   bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
   bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
   bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
-  bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { return true; }
+  void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
 };
 
 
@@ -521,9 +522,31 @@ private:
   std::vector<EqualityPair> d_deducedDisequalityReasons;
 
   /**
-   * Stores a propagated disequality for explanation purpooses and remembers the reasons.
+   * Size of the memory for disequality reasons.
    */
-  bool storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const;
+  context::CDO<size_t> d_deducedDisequalityReasonsSize;
+
+  /**
+   * Map from equalities to the tags that have received the notification.
+   */
+  typedef context::CDHashMap<EqualityPair, Theory::Set, EqualityPairHashFunction> PropagatedDisequalitiesMap;
+  PropagatedDisequalitiesMap d_propagatedDisequalities;
+
+  /**
+   * Has this equality been propagated to anyone.
+   */
+  bool hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const;
+
+  /**
+   * Has this equality been propagated to the tag owner.
+   */
+  bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const;
+
+  /**
+   * Stores a propagated disequality for explanation purpooses and remembers the reasons. The
+   * reasons should be pushed on the reasons vector.
+   */
+  void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId);
   
   /**
    * An equality tagged with a set of tags.
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 0d35d57d8..eceead38a 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -72,10 +72,9 @@ public:
       }
     }
 
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
       d_uf.conflict(t1, t2);
-      return false;
     }
   };
 
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index bdcaaa2d0..bec83183a 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -13,6 +13,7 @@ MAKEFLAGS = -k
 TESTS =	\
 	bug00.smt \
 	bug338.smt2 \
+	bug347.smt \
 	try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \
 	diseqprop.01.smt \
 	wchains010ue.delta01.smt \
diff --git a/test/regress/regress0/aufbv/bug347.smt b/test/regress/regress0/aufbv/bug347.smt
new file mode 100644
index 000000000..f467cd4b3
--- /dev/null
+++ b/test/regress/regress0/aufbv/bug347.smt
@@ -0,0 +1,11 @@
+(benchmark B_
+  :status sat
+  :category { unknown }
+  :logic QF_AUFBV
+  :extrafuns ((delete_0_val_1 BitVec[32]))
+  :extrafuns ((delete_0_curr_6 BitVec[32]))
+  :extrafuns ((arr_next_13 Array[32:32]))
+  :extrafuns ((arr_next_14 Array[32:32]))
+  :extrafuns ((delete_0_head_1 BitVec[32]))
+  :formula (and (= bv0[32] (ite (= bv0[32] delete_0_head_1) (select arr_next_14 delete_0_curr_6) delete_0_curr_6)) (= arr_next_14 arr_next_13) (= bv1[32] (select arr_next_13 bv1[32])) (= delete_0_curr_6 (ite (= bv0[32] delete_0_val_1) bv0[32] bv1[32])))
+)