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

1 files changed, 1 insertions, 1 deletions

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);