diff options
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index c8284762c..21636650d 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -69,7 +69,7 @@ ProofRule CnfProof::getProofRule(ClauseId clause) { Node CnfProof::getAssertionForClause(ClauseId clause) { ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause); - Assert(it != d_clauseToAssertion.end()); + Assert(it != d_clauseToAssertion.end() && !(*it).second.isNull()); return (*it).second; } @@ -135,8 +135,15 @@ void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { // case we keep the first assertion. For example asserting a /\ b // and then b /\ c where b is an atom, would assert b twice (note // that since b is top level, it is not cached by the CnfStream) - if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end()) + // + // Note: If the current assertion associated with the clause is null, we + // update it because it means that it was previously added the clause without + // associating it with an assertion. + const auto& it = d_clauseToAssertion.find(clause); + if (it != d_clauseToAssertion.end() && (*it).second != Node::null()) + { return; + } d_clauseToAssertion.insert (clause, expr); } |