[proof-new] Catch trivial cycles in SAT proof generation (#5853)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from

       l1 v l2   ~l1 v l3   ~l2 v l3
(ok) ------------------------------
                  l3
in which l3 = l1 v l2, to

         l1 v l2   ~l1 v l3   ~l2 v l3
(bad) ------------------------------
               l3 v l3
              ---------
                 l3
This commit now catches the trivial cycle before it's generated.

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 "