diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-07-16 23:23:05 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-16 21:23:05 -0500 |
| commit | 2ee5a2bcf5fd7aaf72d44553ebb85edd76fd06c8 (patch) | |
| tree | f76a2ba702f37733603de02af29011639b7bd7c7 | |
| parent | 70353e7a7bdb5863edda8f2cabf6807d8f084525 (diff) | |
Fix EqProof to ProofNode conversion (#4760)
A wrong change slipped away during the cleaning of the module. This commit fixes the conversion.
| -rw-r--r-- | src/theory/uf/eq_proof.cpp | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 70edbd0dd..c7a834b19 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -997,7 +997,6 @@ Node EqProof::addToProof( if (childProof->d_id == MERGED_THROUGH_CONGRUENCE && childProof->d_node.isNull()) { - CVC4_UNUSED bool addedChild = false; Trace("eqproof-conv") << "EqProof::addToProof: child proof " << i << " is fake cong step. Fold it.\n"; Assert(childProof->d_children.size() == 2); @@ -1008,12 +1007,11 @@ Node EqProof::addToProof( Trace("eqproof-conv") << "EqProof::addToProof: recurse on child " << j << "\n" << push; - Node child = - childProof->d_children[j]->addToProof(p, visited, assumptions); + children.push_back( + childProof->d_children[j]->addToProof(p, visited, assumptions)); Trace("eqproof-conv") << pop; } Trace("eqproof-conv") << pop; - Assert(addedChild); continue; } Trace("eqproof-conv") |