1 files changed, 11 insertions, 0 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index aae11ae51..dd7e94f03 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -228,6 +228,17 @@ void SatProofManager::endResChain(Node conclusion,
                        << children[0] << "\n";
     return;
   }
+  // whether trivial cycle
+  for (const Node& child : children)
+  {
+    if (conclusion == child)
+    {
+      Trace("sat-proof")
+          << "SatProofManager::endResChain: no-op. The conclusion "
+          << conclusion << " is equal to a premise\n";
+      return;
+    }
+  }
   if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion))
   {
     Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of "