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/cnf_proof.h | |
| 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/cnf_proof.h')
| -rw-r--r-- | src/proof/cnf_proof.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 99a347744..32833d9a1 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -127,6 +127,11 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); + /** + * Checks whether the assertion stack is empty. + */ + bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); } + void setProofRecipe(LemmaProofRecipe* proofRecipe); LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma); bool haveProofRecipe(const std::set<Node> &lemma); |