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/uf | |
| parent | e3f06d67aec4c423530002562e556f265f249123 (diff) | |
A few proof bugs fixed
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
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()]; |