1 files changed, 37 insertions, 6 deletions
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index 77c8e80b4..61823c143 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -549,10 +549,17 @@ std::string EqualityEngine<NotifyClass>::edgesToString(EqualityEdgeId edgeId) co
 }
 
 template <typename NotifyClass>
-void EqualityEngine<NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
-  Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
-
-  Assert(getRepresentative(t1) == getRepresentative(t2));
+void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
+  Debug("equality") << "EqualityEngine::explainEquality(" << t1 << "," << t2 << ")" << std::endl;
+
+  Assert(getRepresentative(t1) == getRepresentative(t2),
+         "Cannot explain an equality, because the two terms are not equal!\n"
+         "The representative of %s\n"
+         "                   is %s\n"
+         "The representative of %s\n"
+         "                   is %s",
+         t1.toString().c_str(), getRepresentative(t1).toString().c_str(),
+         t2.toString().c_str(), getRepresentative(t2).toString().c_str());
 
   // Get the explanation
   EqualityNodeId t1Id = getNodeId(t1);
@@ -561,6 +568,28 @@ void EqualityEngine<NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector
 }
 
 template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
+  Debug("equality") << "EqualityEngine::explainDisequality(" << t1 << "," << t2 << ")" << std::endl;
+
+  Node equality = t1.eqNode(t2);
+
+  Assert(getRepresentative(equality) == getRepresentative(d_false),
+         "Cannot explain the dis-equality, because the two terms are not dis-equal!\n"
+         "The representative of %s\n"
+         "                   is %s\n"
+         "The representative of %s\n"
+         "                   is %s",
+         equality.toString().c_str(), getRepresentative(equality).toString().c_str(),
+         d_false.toString().c_str(), getRepresentative(d_false).toString().c_str());
+
+  // Get the explanation 
+  EqualityNodeId equalityId = getNodeId(equality);
+  EqualityNodeId falseId = getNodeId(d_false);
+  getExplanation(equalityId, falseId, equalities);
+}
+
+
+template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const {
 
   Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
@@ -672,12 +701,12 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t
   // Get the information about t1
   EqualityNodeId t1Id = getNodeId(t1);
   EqualityNodeId t1classId = getEqualityNode(t1Id).getFind();
-  TriggerId t1TriggerId = d_nodeTriggers[t1Id];
+  TriggerId t1TriggerId = d_nodeTriggers[t1classId];
 
   // Get the information about t2
   EqualityNodeId t2Id = getNodeId(t2);
   EqualityNodeId t2classId = getEqualityNode(t2Id).getFind();
-  TriggerId t2TriggerId = d_nodeTriggers[t2Id];
+  TriggerId t2TriggerId = d_nodeTriggers[t2classId];
 
   Debug("equality") << "EqualityEngine::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl;
 
@@ -836,6 +865,7 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   Node equality1 = t1.eqNode(t2);
   addTerm(equality1);
   if (getEqualityNode(equality1).getFind() == getEqualityNode(d_false).getFind()) {
+    d_context->pop();
     return true;
   }
 
@@ -843,6 +873,7 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   Node equality2 = t2.eqNode(t1);
   addTerm(equality2);
   if (getEqualityNode(equality2).getFind() == getEqualityNode(d_false).getFind()) {
+    d_context->pop();
     return true;
   }