diff options
author | Guy <katz911@gmail.com> | 2016-07-06 16:41:33 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-06 16:41:33 -0700 |
commit | f9899f4ffc081369f419b8572a5aa397fbaa428a (patch) | |
tree | 2d48cf1e799e3336229ce34d0344ca3733a54a45 /src/theory/arrays | |
parent | e3f06d67aec4c423530002562e556f265f249123 (diff) |
A few proof bugs fixed
Diffstat (limited to 'src/theory/arrays')
-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; |