Properly clean up assertion stack in CnfProof (#2147)

Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.

1 files changed, 10 insertions, 2 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index d7672f1b4..016198735 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -161,10 +161,14 @@ void CnfProof::setCnfDependence(Node from, Node to) {
 }
 
 void CnfProof::pushCurrentAssertion(Node assertion) {
-  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
-                     << assertion  << std::endl;
+  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion
+                     << std::endl;
 
   d_currentAssertionStack.push_back(assertion);
+
+  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
+                     << "new stack size = " << d_currentAssertionStack.size()
+                     << std::endl;
 }
 
 void CnfProof::popCurrentAssertion() {
@@ -174,6 +178,10 @@ void CnfProof::popCurrentAssertion() {
                      << d_currentAssertionStack.back() << std::endl;
 
   d_currentAssertionStack.pop_back();
+
+  Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
+                     << "new stack size = " << d_currentAssertionStack.size()
+                     << std::endl;
 }
 
 Node CnfProof::getCurrentAssertion() {