diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-07-13 13:24:43 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-13 13:24:43 -0700 |
| commit | ca65101e2d56a476367c8ad09b416b66403be7a7 (patch) | |
| tree | f0217edeee991073146d7d681cdf64c6c3476f22 /src/proof/proof_manager.cpp | |
| parent | c369afa180b7cb3d9388c39d18fcb81e8246ff21 (diff) | |
Properly clean up assertion stack in CnfProof (#2147)
Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.
Diffstat (limited to 'src/proof/proof_manager.cpp')
| -rw-r--r-- | src/proof/proof_manager.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index d8ab811bc..f2205e2ed 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -332,6 +332,9 @@ void ProofManager::traceUnsatCore() { d_satProof->collectClausesUsed(used_inputs, used_lemmas); + // At this point, there should be no assertions without a clause id + Assert(d_cnfProof->isAssertionStackEmpty()); + IdToSatClause::const_iterator it = used_inputs.begin(); for(; it != used_inputs.end(); ++it) { Node node = d_cnfProof->getAssertionForClause(it->first); |