From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 17 Jul 2020 02:23:05 +0000 (-0300)
Subject: Fix EqProof to ProofNode conversion (#4760)
X-Git-Tag: cvc5-1.0.0~3095
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ee5a2bcf5fd7aaf72d44553ebb85edd76fd06c8;p=cvc5.git

Fix EqProof to ProofNode conversion (#4760)

A wrong change slipped away during the cleaning of the module. This commit fixes the conversion.
---

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")