In a ROW guard proof, if the transitivity proof does not have a disequality, we can deduce that it is a constant-disequality proof and process it accordingly

1 files changed, 10 insertions, 3 deletions

diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 9cba0592e..5ecccdd53 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -107,7 +107,14 @@ 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 && childProof->d_children.size() != 0) {
+        bool haveNegChild = false;
+        for (unsigned i = 0; i < childProof->d_children.size(); ++i) {
+          if (childProof->d_children[i]->d_node.getKind() == kind::NOT)
+            haveNegChild = true;
+        }
+
+        if ((childProof->d_children.size() != 0) &&
+            (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS || !haveNegChild)) {
           // The proof has two children, explaining why each index is a (different) constant.
           Assert(childProof->d_children.size() == 2);
 
@@ -117,7 +124,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
           if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
             constantOne = childProof->d_children[0]->d_node;
           } else {
-            Assert(childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
+            Assert(childProof->d_children[0]->d_node.getKind() == kind::EQUAL);
             if ((childProof->d_children[0]->d_node[0] == indexOne) ||
                 (childProof->d_children[0]->d_node[0] == indexTwo)) {
               constantOne = childProof->d_children[0]->d_node[1];
@@ -129,7 +136,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
           if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
             constantTwo = childProof->d_children[1]->d_node;
           } else {
-            Assert(childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_EQUALITY);
+            Assert(childProof->d_children[1]->d_node.getKind() == kind::EQUAL);
             if ((childProof->d_children[1]->d_node[0] == indexOne) ||
                 (childProof->d_children[1]->d_node[0] == indexTwo)) {
               constantTwo = childProof->d_children[1]->d_node[1];