[proof-new] Fix bug in expansion of MACRO_RESOLUTION (#5845)

Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which a crowding literal occurs in an OR node that represents a single-literal clause subsequent to the last clause that includes the crowding literal. This was leading to the clause that eliminates the crowding literal not being found. The commit fixes this issue by excluding single-literal clauses from those that can introduce crowding literals (which was already marked as necessary but not properly enforced).

1 files changed, 12 insertions, 3 deletions

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index a57a6d920..4b1a05e0f 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -156,6 +156,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
     {
       Node crowdLit = clauseLits[i];
       crowding.insert(crowdLit);
+      Trace("smt-proof-pp-debug2") << "crowding lit " << crowdLit << "\n";
       // found crowding lit, now get its last inclusion position, which is the
       // position of the last resolution link that introduces the crowding
       // literal. Note that this position has to be *before* the last link, as a
@@ -164,11 +165,19 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
       for (j = children.size() - 1; j > 0; --j)
       {
         // notice that only non-unit clauses may be introducing the crowding
-        // literal, so we don't need to differentiate unit from non-unit
+        // literal, so we only care about non-unit OR nodes. We check then
+        // against the kind and whether the whole OR node occurs as a pivot of
+        // the respective resolution
         if (children[j - 1].getKind() != kind::OR)
         {
           continue;
         }
+        uint64_t pivotIndex = 2 * (j - 1);
+        if (args[pivotIndex] == children[j - 1]
+            || args[pivotIndex].notNode() == children[j - 1])
+        {
+          continue;
+        }
         if (std::find(children[j - 1].begin(), children[j - 1].end(), crowdLit)
             != children[j - 1].end())
         {
@@ -177,7 +186,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
       }
       Assert(j > 0);
       lastInclusion.emplace_back(crowdLit, j - 1);
-      Trace("smt-proof-pp-debug2") << "crowding lit " << crowdLit << "\n";
+
       Trace("smt-proof-pp-debug2") << "last inc " << j - 1 << "\n";
       // get elimination position, starting from the following link as the last
       // inclusion one. The result is the last (in the chain, but first from
@@ -210,7 +219,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits(
           break;
         }
       }
-      Assert(j < children.size());
+      AlwaysAssert(j < children.size());
     }
   }
   Assert(!lastInclusion.empty());