From e5516d91b82f93f74fb24523bdab12763e65c419 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 18 May 2020 21:44:54 -0700
Subject: Fix detection of cyclic proofs

---
 src/expr/proof_node.cpp | 5 +++++
 1 file changed, 5 insertions(+)

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());
         }
       }
-- 
cgit v1.2.3