[proof-new] Fixing resolution proof checker (#5262)

Previously the binary resolution checker was:

- Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument.
- Not producing false the remaining set of literals after resolution was empty.

This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening).

Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>

1 files changed, 1 insertions, 1 deletions

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index c7dd288af..b2d33a61d 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -548,7 +548,7 @@ void ProofCnfStream::convertPropagation(theory::TrustNode trn)
     d_proof.addStep(clauseExp,
                     PfRule::RESOLUTION,
                     {clauseAndNeg, clauseImpliesElim},
-                    {proven[0]});
+                    {nm->mkConst(true), proven[0]});
   }
   else
   {