From 2ee5a2bcf5fd7aaf72d44553ebb85edd76fd06c8 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 16 Jul 2020 23:23:05 -0300 Subject: [PATCH] Fix EqProof to ProofNode conversion (#4760) A wrong change slipped away during the cleaning of the module. This commit fixes the conversion. --- src/theory/uf/eq_proof.cpp | 6 ++---- 1 file 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") -- 2.30.2