diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-08-19 11:06:23 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-19 14:06:23 +0000 |
| commit | d72b82ba383cb1e0cccab33218fdf5af280ec7cb (patch) | |
| tree | db42034fd38e759e36e8db48397e3cc3f0b38365 /src/prop/theory_proxy.cpp | |
| parent | fbf6733b9c182d0e0ecedfaa5dc9f576f6f1607f (diff) | |
[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.
Diffstat (limited to 'src/prop/theory_proxy.cpp')
| -rw-r--r-- | src/prop/theory_proxy.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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()); |