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, 11 insertions, 0 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6690f12db..aa5bb92d9 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -160,8 +160,19 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
     // If we were called with something other than a theory atom (or
     // Boolean variable), we get a SatLiteral that is definitionally
     // equal to it.
+    //
+    // We are setting the current assertion to be null. This is because `toCNF`
+    // may add clauses to the SAT solver and we look up the current assertion
+    // in that case. Setting it to null ensures that the assertion stack is
+    // non-empty and that we are not associating a bogus assertion with the
+    // clause. This should be ok because we use the mapping back to assertions
+    // for clauses from input assertions only.
+    PROOF(if (d_cnfProof) { d_cnfProof->pushCurrentAssertion(Node::null()); });
+
     lit = toCNF(n, false);
 
+    PROOF(if (d_cnfProof) { d_cnfProof->popCurrentAssertion(); });
+
     // Store backward-mappings
     // These may already exist
     d_literalToNodeMap.insert_safe(lit, n);