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

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).