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 | |
| parent | e3f06d67aec4c423530002562e556f265f249123 (diff) | |
A few proof bugs fixed
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arrays/array_proof_reconstruction.cpp | 4 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 3 |
2 files changed, 3 insertions, 4 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; diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 25b12f75f..09d348584 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -393,7 +393,7 @@ const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) { - Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), pid = " << pid << std::endl; + Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2 << "), reason = " << reason << ", pid = " << pid << std::endl; if (d_done) { return; @@ -1204,7 +1204,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st Debug("equality") << d_name << "::eq::getExplanation(): adding: " << reason << std::endl; Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl; - Node a = d_nodes[currentNode]; Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()]; |