diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-25 15:38:28 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-25 20:38:28 +0000 |
| commit | 85f57e1b106e0c91ef73a51ff3ad5194d6634b60 (patch) | |
| tree | eb65ed078673c8557d077c960cfc3c216a17dbc1 | |
| parent | f3a2e3814d0a3f32fe1e9e24de954bc2d9ff999e (diff) | |
Fix spurious checks to closed proofs (#7484)
This leads to issues when (1) proofs are enabled, (2) unsat cores are enabled and full proofs are disabled in a subsolver.
This is the case for the abduction algorithm that uses unsat core learning, when proofs are explicitly enabled. This led to spurious assertion failures when testing proof new.
| -rw-r--r-- | src/theory/theory_engine.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0f3260920..ee1528f4d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1428,14 +1428,14 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) // Process the explanation TrustNode tncExp = getExplanation(vec); - Trace("te-proof-debug") - << "Check closed conflict explained with sharing" << std::endl; - tncExp.debugCheckClosed("te-proof-debug", - "TheoryEngine::conflict_explained_sharing"); Node fullConflict = tncExp.getNode(); if (isProofEnabled()) { + Trace("te-proof-debug") + << "Check closed conflict explained with sharing" << std::endl; + tncExp.debugCheckClosed("te-proof-debug", + "TheoryEngine::conflict_explained_sharing"); Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl; Trace("te-proof-debug") << "Conflict " << tconflict << " from " << tconflict.identifyGenerator() << std::endl; @@ -1498,7 +1498,10 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) Assert(properConflict(fullConflict)); Trace("te-proof-debug") << "Check closed conflict with sharing" << std::endl; - tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing"); + if (isProofEnabled()) + { + tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing"); + } lemma(tconf, LemmaProperty::REMOVABLE); } else { // When only one theory, the conflict should need no processing |