Set assertion in `CnfStream::ensureLiteral()` (#3927)

Fixes #3814. `CnfProof` has a stack of assertions that are being
converted to clauses. `CnfStream::ensureLiteral()` can result in clauses
being added to the SAT solver. When adding a clause, we require an
assertion that can be associated with the clause
(https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476).
However, in the issue that was reported, the stack was empty, resulting
in an assertion failure. This commit fixes the issue by setting the
current assertion to be the null node when a literal is being ensured
(and changing the proof code to update the assertion associated with a
literal if it is currently null). This should be ok since the clauses
are not inputs or lemmas (if they are, the assertion associated with the
clause will be updated).

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);
 }