diff options
Diffstat (limited to 'src/theory/arrays/array_proof_reconstruction.cpp')
-rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp index 6dfd14157..8dd7fe782 100644 --- a/src/theory/arrays/array_proof_reconstruction.cpp +++ b/src/theory/arrays/array_proof_reconstruction.cpp @@ -60,7 +60,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, // or ((a[i]:=t)[k] == a[k]) because (i != k). if (proof) { - if (a.getNumChildren() == 2) { + if (a.getKind() == kind::SELECT) { // 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 @@ -156,7 +156,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, proof->d_children.push_back(childProof); } else { - // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), + // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]), Node indexOne = a; Node indexTwo = b; |