diff options
author | Guy <guy@Guy-X260> | 2016-09-16 16:26:30 -0700 |
---|---|---|
committer | Guy <guy@Guy-X260> | 2016-09-16 16:26:30 -0700 |
commit | 0e68cfe050946d1ed9544dffcbd5e75be0e6f22f (patch) | |
tree | 1c968358d3ff2f5bc592a89ca52d2c5f91fdb54f /src/theory/arrays | |
parent | 976ee5b66b7584b9fe46eab1facf5e5f857e723f (diff) |
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
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 2 |
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); |