(proof-new) Fix true explanations of propagations in pf equality engine (#5338)

This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.

1 files changed, 13 insertions, 2 deletions

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 184584aa9..18cdcf902 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -408,9 +408,20 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc,
       scopeAssumps.push_back(a);
     }
   }
-  // scope the proof constructed above, and connect the formula with the proof
-  // minimize the assumptions
+  // Scope the proof constructed above, and connect the formula with the proof
+  // minimize the assumptions.
   pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
+  // If we have no assumptions, and are proving an explanation for propagation
+  if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP)
+  {
+    // Must add "true" as an explicit argument. This is to ensure that the
+    // propagation F from true proves (=> true F) instead of F, since this is
+    // the form required by TrustNodeKind::PROP_EXP. We do not ensure closed or
+    // minimize here, since we already ensured the proof was closed above, and
+    // we do not want to minimize, or else "true" would be omitted.
+    scopeAssumps.push_back(nm->mkConst(true));
+    pf = d_pnm->mkScope(pf, scopeAssumps, false);
+  }
   exp = nm->mkAnd(scopeAssumps);
   // Make the lemma or conflict node. This must exactly match the conclusion
   // of SCOPE below.