squash-merge from proof branch

1 files changed, 290 insertions, 26 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 0ac5096d2..53347c365 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -42,7 +42,6 @@ EqualityEngine::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&constantTermsCount);
 }
 
-
 /**
  * Data used in the BFS search through the equality graph.
  */
@@ -157,7 +156,7 @@ void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
 }
 
 void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
-  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << "). reason: " << candidate.reason << std::endl;
   if (back) {
     d_propagationQueue.push_back(candidate);
   } else {
@@ -920,7 +919,7 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const {
 }
 
 void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const {
-  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
 
   // The terms must be there already
   Assert(hasTerm(t1) && hasTerm(t2));;
@@ -933,13 +932,83 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
     // Get the explanation
     getExplanation(t1Id, t2Id, equalities, eqp);
   } else {
+    if (eqp) {
+      eqp->d_id = eq::MERGED_THROUGH_TRANS;
+      eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode();
+    }
+
     // Get the reason for this disequality
     EqualityPair pair(t1Id, t2Id);
     Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end(), "Don't ask for stuff I didn't notify you about");
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
+
     for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
-      getExplanation(toExplain.first, toExplain.second, equalities, eqp);
+    }
+
+    for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
+
+      EqualityPair toExplain = d_deducedDisequalityReasons[i];
+      EqProof* eqpc = NULL;
+
+      // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
+      if (eqp && toExplain.first != toExplain.second) {
+        eqpc = new EqProof;
+      }
+
+      // Some edges have the form ((a == b) == false). Translate this into (not (a == b)).
+      // Assert(d_nodes[toExplain.first] != NodeManager::currentNM()->mkConst(false));
+
+      getExplanation(toExplain.first, toExplain.second, equalities, eqpc);
+
+      // if (eqpc) {
+      //   eqp->d_children.push_back(eqpc);
+      // }
+
+      if (eqpc) {
+        Debug("pf::ee") << "Child proof is:" << std::endl;
+        eqpc->debug_print("pf::ee", 1);
+
+        if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) {
+          std::vector<EqProof *> orderedChildren;
+          bool nullCongruenceFound = false;
+          for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
+            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) {
+
+              // For now, assume there can only be one null congruence child
+              Assert(!nullCongruenceFound);
+              nullCongruenceFound = true;
+
+              Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl;
+              orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]);
+              orderedChildren.push_back(eqpc->d_children[i]->d_children[1]);
+            } else {
+              orderedChildren.push_back(eqpc->d_children[i]);
+            }
+          }
+
+          if (nullCongruenceFound) {
+            eqpc->d_children = orderedChildren;
+            Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl;
+            eqpc->debug_print("pf::ee", 1);
+          }
+        }
+
+        eqp->d_children.push_back(eqpc);
+      }
+    }
+
+    if (eqp) {
+      if(eqp->d_children.size() == 1) {
+        // The transitivity proof has just one child. Simplify.
+        EqProof* temp = eqp->d_children[0];
+        eqp->d_children.clear();
+        *eqp = *temp;
+        delete temp;
+      }
+
+      Debug("pf::ee") << "Disequality explanation final proof: " << std::endl;
+      eqp->debug_print("pf::ee", 1);
     }
   }
 }
@@ -972,7 +1041,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
   // If the nodes are the same, we're done
   if (t1Id == t2Id){
     if( eqp ) {
-      eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
+      if ((d_nodes[t1Id].getKind() == kind::BUILTIN) && (d_nodes[t1Id].getConst<Kind>() == kind::SELECT)) {
+        std::vector<Node> no_children;
+        eqp->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, no_children);
+      } else {
+        eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
+      }
     }
     return;
   }
@@ -1019,7 +1093,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
           Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
 
-          std::vector< EqProof * > eqp_trans;
+          std::vector<EqProof *> eqp_trans;
 
           // Reconstruct the path
           do {
@@ -1029,11 +1103,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
 
             Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
+            Debug("equality") << d_name << "                     targetNode = " << d_nodes[edgeNode] << std::endl;
             Debug("equality") << d_name << "                     in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
+            Debug("equality") << d_name << "                     reason type = " << reasonType << std::endl;
 
-            EqProof * eqpc = NULL;
-            //make child proof if a proof is being constructed
-            if( eqp ){
+            EqProof* eqpc = NULL;
+            // Make child proof if a proof is being constructed
+            if (eqp) {
               eqpc = new EqProof;
               eqpc->d_id = reasonType;
             }
@@ -1044,26 +1120,60 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Debug("equality") << d_name << "::eq::getExplanation(): due to congruence, going deeper" << std::endl;
               const FunctionApplication& f1 = d_applications[currentNode].original;
               const FunctionApplication& f2 = d_applications[edgeNode].original;
+
+              Debug("pf::ee") << "We need to prove two equalities:" << std::endl;
+              Debug("pf::ee") << "\tLHS: " << d_nodes[f1.a] << " = " << d_nodes[f2.a] << std::endl;
+              Debug("pf::ee") << "\tRHS: " << d_nodes[f1.b] << " = " << d_nodes[f2.b] << std::endl;
+
               Debug("equality") << push;
+              Debug("equality") << "Explaining left hand side equalities" << std::endl;
               EqProof * eqpc1 = eqpc ? new EqProof : NULL;
               getExplanation(f1.a, f2.a, equalities, eqpc1);
+              Debug("equality") << "Explaining right hand side equalities" << std::endl;
               EqProof * eqpc2 = eqpc ? new EqProof : NULL;
               getExplanation(f1.b, f2.b, equalities, eqpc2);
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
                 eqpc->d_children.push_back( eqpc2 );
-                Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl;
+                Debug("pf::ee") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl;
                 if( d_nodes[currentNode].getKind()==kind::EQUAL ){
                   //leave node null for now
                   eqpc->d_node = Node::null();
                 }else{
-                  Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl;
+                  Debug("pf::ee") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl;
                   if(d_nodes[f1.a].getKind() == kind::APPLY_UF ||
                      d_nodes[f1.a].getKind() == kind::SELECT ||
                      d_nodes[f1.a].getKind() == kind::STORE) {
                     eqpc->d_node = d_nodes[f1.a];
                   } else {
-                    eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]);
+
+                    Debug("pf::ee") << "f1.a is: " << d_nodes[f1.a]
+                                    << ". kind is: " << d_nodes[f1.a].getKind() << std::endl;
+
+                    if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) {
+                      Debug("pf::ee") << "f1.a getConst<kind> is: " << d_nodes[f1.a].getConst<Kind>() << std::endl;
+
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]);
+                      // The first child is a PARTIAL_SELECT_0. Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
+                      Debug("pf::ee") << "eqpc->d_children[0]->d_node.getKind() == " << eqpc->d_children[0]->d_node.getKind() << std::endl;
+                      Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0);
+                      Assert(eqpc->d_children[0]->d_children.size() == 0);
+
+                      Debug("pf::ee") << "Dumping the equality proof before:" << std::endl;
+                      eqpc->debug_print("pf::ee", 1);
+
+                      eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, d_nodes[f1.b]);
+
+                      Debug("pf::ee") << "Dumping the equality proof after:" << std::endl;
+                      eqpc->debug_print("pf::ee", 1);
+
+                      //eqpc->d_children[0]->d_node.append(d_nodes[f1.b]);
+                    } else {
+                      eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF,
+                                                                      ProofManager::currentPM()->mkOp(d_nodes[f1.a]),
+                                                                      d_nodes[f1.b]);
+                    }
+                    Debug("pf::ee") << "New d_node is: " << eqpc->d_node << std::endl;
                   }
                 }
               }
@@ -1114,16 +1224,162 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
               break;
             }
+            case MERGED_ARRAYS_EXT:
+
+              Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_EXT" << std::endl;
+
+              if (eqpc) {
+                Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+                Node b = d_nodes[currentNode];
+
+                // GK: todo: here we assume that a=b is an assertion. We should probably call explain()
+                // recursively, to explain this.
+
+                if (a == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = b.notNode();
+                } else if (b == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = a.notNode();
+                } else {
+                  eqpc->d_node = a.eqNode(b);
+                }
+
+                EqProof* eqpc1 = new EqProof;
+                eqpc1->d_node = d_equalityEdges[currentEdge].getReason();
+                eqpc->d_children.push_back( eqpc1 );
+
+                eqpc1->debug_print("pf::ee", 1);
+                eqpc->debug_print("pf::ee", 1);
+              }
+
+              // We push the reason into "equalities" because that's what the theory of arrays expects.
+              equalities.push_back(d_equalityEdges[currentEdge].getReason());
+              break;
+
+            case MERGED_ARRAYS_ROW: {
+              Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_ROW" << std::endl;
+
+              // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
+              // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
+              // or ((a[i]:=t)[k] == a[k]) because (i != k).
+
+              if (eqpc) {
+                if (d_nodes[currentNode].getNumChildren() == 2) {
+                  // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k).
+
+                  // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be
+                  // false in the first case and true in the second case.
+                  bool currentNodeIsUnchangedArray;
+
+                  Assert(d_nodes[currentNode].getNumChildren() == 2);
+                  Assert(d_nodes[edgeNode].getNumChildren() == 2);
+
+                  if (d_nodes[currentNode][0].getKind() == kind::VARIABLE ||
+                      d_nodes[currentNode][0].getKind() == kind::SKOLEM) {
+                    currentNodeIsUnchangedArray = true;
+                  } else if (d_nodes[edgeNode][0].getKind() == kind::VARIABLE ||
+                             d_nodes[edgeNode][0].getKind() == kind::SKOLEM) {
+                    currentNodeIsUnchangedArray = false;
+                  } else {
+                    Assert(d_nodes[currentNode][0].getKind() == kind::STORE);
+                    Assert(d_nodes[edgeNode][0].getKind() == kind::STORE);
+
+                    if (d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]) {
+                      currentNodeIsUnchangedArray = false;
+                    } else if (d_nodes[edgeNode][0][0] == d_nodes[currentNode][0]) {
+                      currentNodeIsUnchangedArray = true;
+                    } else {
+                      Unreachable();
+                    }
+                  }
+
+                  Node indexOne =
+                    currentNodeIsUnchangedArray ? d_nodes[currentNode][1] : d_nodes[currentNode][0][1];
+                  Node indexTwo =
+                    currentNodeIsUnchangedArray ? d_nodes[edgeNode][0][1] : d_nodes[edgeNode][1];
+
+                  // Some assertions to ensure that the theory of arrays behaves as expected
+                  Assert(d_nodes[currentNode][1] == d_nodes[edgeNode][1]);
+                  if (currentNodeIsUnchangedArray) {
+                    Assert(d_nodes[currentNode][0] == d_nodes[edgeNode][0][0]);
+                  } else {
+                    Assert(d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]);
+                  }
+
+                  Debug("pf::ee") << "Getting explanation for ROW guard: "
+                                     << indexOne << " != " << indexTwo << std::endl;
+
+                  EqProof* eqpcc = eqpc ? new EqProof : NULL;
+                  explainEquality(indexOne, indexTwo, false, equalities, eqpcc);
+
+                  Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl;
+                  Debug("pf::ee") << "And the explanation of their disequality is: " << std::endl;
+                  eqpcc->debug_print("pf::ee", 1);
+                  eqpc->d_children.push_back(eqpcc);
+                } else {
+                  // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
+
+                  Debug("pf::ee") << "In the new case of ROW!" << std::endl;
+
+                  Node indexOne = d_nodes[currentNode];
+                  Node indexTwo = d_nodes[edgeNode];
+
+                  Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl;
+                  Debug("pf::ee") << "The reason for the edge is: " << d_equalityEdges[currentEdge].getReason()
+                                     << std::endl;
+
+                  Assert(d_equalityEdges[currentEdge].getReason().getNumChildren() == 2);
+                  Node reason = d_equalityEdges[currentEdge].getReason()[1];
+                  Debug("pf::ee") << "Getting explanation for ROW guard: " << reason << std::endl;
+
+                  EqProof* eqpcc = eqpc ? new EqProof : NULL;
+                  explainEquality(reason[0], reason[1], false, equalities, eqpcc);
+
+                  if (eqpc) {
+                    Debug("pf::ee") << "The guard's explanation is: " << std::endl;
+                    eqpcc->debug_print("pf::ee", 1);
+                    eqpc->d_children.push_back(eqpcc);
+                  }
+                }
+
+                Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+                Node b = d_nodes[currentNode];
+
+                if (a == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = b.notNode();
+                } else if (b == NodeManager::currentNM()->mkConst(false)) {
+                  eqpc->d_node = a.notNode();
+                } else {
+                  eqpc->d_node = a.eqNode(b);
+                }
+              }
+
+              // We push the reason into "equalities" because that's what the theory of arrays expects.
+              equalities.push_back(d_equalityEdges[currentEdge].getReason());
+              break;
+            }
+
             default: {
               // Construct the equality
               Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
-              if( eqpc ){
-                if(reasonType == MERGED_THROUGH_EQUALITY) {
+              Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl;
+
+              if (eqpc) {
+                if (reasonType == MERGED_THROUGH_EQUALITY) {
                   eqpc->d_node = d_equalityEdges[currentEdge].getReason();
                 } else {
-                  // theory-specific proof rule
-                  eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]);
-                  Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl;
+                  // The LFSC translator prefers (not (= a b)) over (= (a==b) false)
+
+                  Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+                  Node b = d_nodes[currentNode];
+
+                  if (a == NodeManager::currentNM()->mkConst(false)) {
+                    eqpc->d_node = b.notNode();
+                  } else if (b == NodeManager::currentNM()->mkConst(false)) {
+                    eqpc->d_node = a.notNode();
+                  } else {
+                    eqpc->d_node = a.eqNode(b);
+                  }
+                  Debug("pf::ee") << "theory eq : " << eqpc->d_node << std::endl;
                 }
                 eqpc->d_id = reasonType;
               }
@@ -1137,7 +1393,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             currentIndex = bfsQueue[currentIndex].previousIndex;
 
             //---from Morgan---
-            if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
+            if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
               if(eqpc->d_node.isNull()) {
                 Assert(eqpc->d_children.size() == 1);
                 EqProof *p = eqpc;
@@ -1149,11 +1405,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             }
             //---end from Morgan---
 
-            eqp_trans.push_back( eqpc );
-
+            eqp_trans.push_back(eqpc);
           } while (currentEdge != null_id);
 
-          if(eqp) {
+          if (eqp) {
             if(eqp_trans.size() == 1) {
               *eqp = *eqp_trans[0];
               delete eqp_trans[0];
@@ -1162,6 +1417,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
               eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
             }
+
+            eqp->debug_print("pf::ee", 1);
           }
 
           // Done
@@ -1508,7 +1765,7 @@ void EqualityEngine::debugPrintGraph() const {
     EqualityEdgeId edgeId = d_equalityGraph[nodeId];
     while (edgeId != null_edge) {
       const EqualityEdge& edge = d_equalityEdges[edgeId];
-      Debug("equality::graph") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
+      Debug("equality::graph") << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
       edgeId = edge.getNext();
     }
 
@@ -1517,17 +1774,19 @@ void EqualityEngine::debugPrintGraph() const {
 }
 
 bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
-  Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")";
 
   Assert(hasTerm(t1));
   Assert(hasTerm(t2));
 
-  return getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+  bool result = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+  Debug("equality") << (result ? "\t(YES)" : "\t(NO)") << std::endl;
+  return result;
 }
 
 bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
 {
-  Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")";
 
   // Add the terms
   Assert(hasTerm(t1));
@@ -1539,6 +1798,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
 
   // If we propagated this disequality we're true
   if (hasPropagatedDisequality(t1Id, t2Id)) {
+    Debug("equality") << "\t(YES)" << std::endl;
     return true;
   }
 
@@ -1556,6 +1816,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
       nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId));
       nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
     }
+    Debug("equality") << "\t(YES)" << std::endl;
     return true;
   }
 
@@ -1571,6 +1832,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
+      Debug("equality") << "\t(YES)" << std::endl;
       return true;
     }
   }
@@ -1587,11 +1849,13 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
         nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, original.b));
         nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
       }
+      Debug("equality") << "\t(YES)" << std::endl;
       return true;
     }
   }
 
   // Couldn't deduce dis-equalityReturn whether the terms are disequal
+  Debug("equality") << "\t(NO)" << std::endl;
   return false;
 }
 
@@ -2103,7 +2367,7 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{
       d_children[i]->debug_print( c, tb+1 );
     }
   }
-  Debug( c ) << ")";
+  Debug( c ) << ")" << std::endl;
 }