Fix detection of cyclic proofsstringsPfFixCycleDetect

1 files changed, 5 insertions, 0 deletions

diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
index de9be6a71..d22091f17 100644
--- a/src/expr/proof_node.cpp
+++ b/src/expr/proof_node.cpp
@@ -93,6 +93,11 @@ void ProofNode::getFreeAssumptionsMap(
         {
           Assert(std::find(visit.begin(), visit.end(), cp.get()) == visit.end())
               << "ProofNode::getFreeAssumptions: cyclic proof!";
+        }
+        // The following loop cannot be merged with the loop above because the
+        // same subproof
+        for (const std::shared_ptr<ProofNode>& cp : cur->d_children)
+        {
           visit.push_back(cp.get());
         }
       }