diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-05-04 15:36:41 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-04 15:36:41 -0300 |
| commit | 5018442120cb22e6f1923a97df7cd98c2d2b5a4a (patch) | |
| tree | 4b2c5331b7fe482c047665e069bffe0392b3989e /src/prop/theory_proxy.cpp | |
| parent | 4f265b2c81c4cb858942f6e1e51ce8abdd01345b (diff) | |
Do not use proof CNF stream with assumptions-based cores (#6488)
Previously using proof CNF stream together with assumptions-based unsat cores added unnecessary performance overhead.
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
Diffstat (limited to 'src/prop/theory_proxy.cpp')
| -rw-r--r-- | src/prop/theory_proxy.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 43f91f732..090b44b90 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -98,7 +98,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { theory::TrustNode tte = d_theoryEngine->getExplanation(lNode); Node theoryExplanation = tte.getNode(); - if (options::produceProofs()) + if (options::produceProofs() + && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS) { Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF || tte.getGenerator()); |