From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 19 Aug 2021 14:06:23 +0000 (-0300)
Subject: [unsat cores] [proofs] Revert test about when to explain propagations (#7034)
X-Git-Tag: cvc5-1.0.0~1370
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d72b82ba383cb1e0cccab33218fdf5af280ec7cb;p=cvc5.git

[unsat cores] [proofs] Revert test about when to explain propagations (#7034)

Reverts a change from #7031, which changed the contract for when the proof CNF stream is handling propagations. When doing unsat cores with sat proofs (but not full proofs), theory engine will not be proof producing but the proof cnf stream still needs to connect theory lemmas with their clausified equivalents in the SAT solver.
---

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index b4bc7fa60..c18fe2dd4 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -98,7 +98,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (d_env.isTheoryProofProducing())
+  if (d_env.isSatProofProducing())
   {
     Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
            || tte.getGenerator());