From: Guy <guy@Guy-X260>
Date: Fri, 16 Sep 2016 23:26:30 +0000 (-0700)
Subject: Handling a corner case where a ROW's guard is a constant disequality.
X-Git-Tag: cvc5-1.0.0~6028^2~44
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e68cfe050946d1ed9544dffcbd5e75be0e6f22f;p=cvc5.git

Handling a corner case where a ROW's guard is a constant disequality.
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
---

diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 8dd7fe782..9cba0592e 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -107,7 +107,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
 
         // It could be that the guard condition is a constant disequality. In this case,
         // we need to change it to a different format.
-        if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS) {
+        if (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS && childProof->d_children.size() != 0) {
           // The proof has two children, explaining why each index is a (different) constant.
           Assert(childProof->d_children.size() == 2);
 
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f98ad556f..5d929a708 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -987,7 +987,14 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
     }
 
     if (eqp) {
-      if(eqp->d_children.size() == 1) {
+      if (eqp->d_children.size() == 0) {
+        // Corner case where this is actually a disequality between two constants
+        Debug("pf::ee") << "Encountered a constant disequality (not a transitivity proof): "
+                        << eqp->d_node << std::endl;
+        Assert(eqp->d_node[0][0].isConst());
+        Assert(eqp->d_node[0][1].isConst());
+        eqp->d_id = MERGED_THROUGH_CONSTANTS;
+      } else if (eqp->d_children.size() == 1) {
         // The transitivity proof has just one child. Simplify.
         EqProof* temp = eqp->d_children[0];
         eqp->d_children.clear();