From d72b82ba383cb1e0cccab33218fdf5af280ec7cb Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 19 Aug 2021 11:06:23 -0300 Subject: [PATCH] [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. --- src/prop/theory_proxy.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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()); -- 2.30.2