[proofs] [sat] [cores] Fix unsat cores based on the SAT proof (#8850)

The justifications for the theory lemmas (i.e., THEORY_LEMMA steps) sometimes was not being properly connected with the actual clause inserted into the SAT solver, leading to open proofs. The issue was triggered by a regression being added in ##8819, so we don't need to add one here.

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index aca1563167cf16554bddd26b42ca03780ecc1401..939e78f34f29e5b0650af93a7d2a89ee1a467b37 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -598,7 +598,8 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
   d_currPropagationProccessed = normalizeAndRegister(clauseExp);
   // consume steps if clausification being recorded. If we are not logging it,
   // we need to add the clause as a closed step to the proof so that the SAT
-  // proof does not have non-input formulas as assumptions.
+  // proof does not have non-input formulas as assumptions. That clause is the
+  // result of normalizeAndRegister, stored in d_currPropagationProccessed
   if (proofLogging)
   {
     const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
@@ -610,7 +611,10 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
   }
   else
   {
-    d_proof.addStep(clauseExp, PfRule::THEORY_LEMMA, {}, {clauseExp});
+    d_proof.addStep(d_currPropagationProccessed,
+                    PfRule::THEORY_LEMMA,
+                    {},
+                    {d_currPropagationProccessed});
   }
 }
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 1e72670640701832ce93b182432262c921a3c79b..91f1aaf7612d80cf6b3183564118b9a8e4a067d9 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -74,7 +74,9 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te)
       d_satSolver(nullptr),
       d_cnfStream(nullptr),
       d_pfCnfStream(nullptr),
-      d_theoryLemmaPg(d_env.getProofNodeManager(), d_env.getUserContext()),
+      d_theoryLemmaPg(d_env.getProofNodeManager(),
+                      d_env.getUserContext(),
+                      "PropEngine::ThLemmaPg"),
       d_ppm(nullptr),
       d_interrupted(false),
       d_assumptions(d_env.getUserContext())
@@ -240,7 +242,8 @@ void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
   if (isProofEnabled() && !d_env.isTheoryProofProducing()
       && !trn.getGenerator())
   {
-    d_theoryLemmaPg.addStep(node, PfRule::THEORY_LEMMA, {}, {node});
+    Node actualNode = negated ? node.notNode() : node;
+    d_theoryLemmaPg.addStep(actualNode, PfRule::THEORY_LEMMA, {}, {actualNode});
     trn = TrustNode::mkReplaceGenTrustNode(trn, &d_theoryLemmaPg);
   }
   assertInternal(node, negated, removable, false, trn.getGenerator());
@@ -337,7 +340,7 @@ bool PropEngine::isDecision(Node lit) const {
 
 std::vector<Node> PropEngine::getPropDecisions() const
 {
-  std::vector<Node> decisions; 
+  std::vector<Node> decisions;
   std::vector<SatLiteral> miniDecisions = d_satSolver->getDecisions();
   for (SatLiteral d : miniDecisions)
   {