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

4 files changed, 33 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);
 }
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);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 62c9c87b1..15728ec1d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -76,6 +76,7 @@ set(regress_0_tests
   regress0/arrays/incorrect8.smtv1.smt2
   regress0/arrays/incorrect9.smtv1.smt2
   regress0/arrays/issue3813-massign-assert.smt2
+  regress0/arrays/issue3814.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
   regress0/arrays/x2.smtv1.smt2
   regress0/arrays/x3.smtv1.smt2
diff --git a/test/regress/regress0/arrays/issue3814.smt2 b/test/regress/regress0/arrays/issue3814.smt2
new file mode 100644
index 000000000..6c557d99d
--- /dev/null
+++ b/test/regress/regress0/arrays/issue3814.smt2
@@ -0,0 +1,12 @@
+; REQUIRES: proof
+; COMMAND-LINE: --produce-unsat-cores
+; EXPECT: sat
+(set-logic QF_AX)
+(declare-fun a () (Array Bool Bool))
+(declare-fun b () (Array Bool Bool))
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(declare-fun e () Bool)
+(assert (= a (store b c d)))
+(assert (= e (select a (select b d))))
+(check-sat)