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.

7 files changed, 67 insertions, 27 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() {
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 99a347744..32833d9a1 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -127,6 +127,11 @@ public:
   void popCurrentDefinition();
   Node getCurrentDefinition();
 
+  /**
+   * Checks whether the assertion stack is empty.
+   */
+  bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); }
+
   void setProofRecipe(LemmaProofRecipe* proofRecipe);
   LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
   bool haveProofRecipe(const std::set<Node> &lemma);
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d8ab811bc..f2205e2ed 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -332,6 +332,9 @@ void ProofManager::traceUnsatCore() {
   d_satProof->collectClausesUsed(used_inputs,
                                  used_lemmas);
 
+  // At this point, there should be no assertions without a clause id
+  Assert(d_cnfProof->isAssertionStackEmpty());
+
   IdToSatClause::const_iterator it = used_inputs.begin();
   for(; it != used_inputs.end(); ++it) {
     Node node = d_cnfProof->getAssertionForClause(it->first);
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 68050d93c..82e7cb7b2 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -565,6 +565,9 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit,
 
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
+      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
+                          "input (UNIT CLAUSE): "
+                       << lit << std::endl;
       d_inputClauses.insert(newId);
     }
     if (kind == THEORY_LEMMA) {
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8f5b37e74..c312ac146 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -236,33 +236,34 @@ void Solver::resizeVars(int newSize) {
 }
 
 CRef Solver::reason(Var x) {
+  Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
 
-    // If we already have a reason, just return it
-    if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
+  // If we already have a reason, just return it
+  if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
 
-    // What's the literal we are trying to explain
-    Lit l = mkLit(x, value(x) != l_True);
+  // What's the literal we are trying to explain
+  Lit l = mkLit(x, value(x) != l_True);
 
-    // Get the explanation from the theory
-    SatClause explanation_cl;
-    // FIXME: at some point return a tag with the theory that spawned you
-    proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
-                              explanation_cl);
-    vec<Lit> explanation;
-    MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
+  // Get the explanation from the theory
+  SatClause explanation_cl;
+  // FIXME: at some point return a tag with the theory that spawned you
+  proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
+  vec<Lit> explanation;
+  MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
-    Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl;
+  Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl
+                   << std::endl;
 
-    // Sort the literals by trail index level
-    lemma_lt lt(*this);
-    sort(explanation, lt);
-    Assert(explanation[0] == l);
+  // Sort the literals by trail index level
+  lemma_lt lt(*this);
+  sort(explanation, lt);
+  Assert(explanation[0] == l);
 
-    // Compute the assertion level for this clause
-    int explLevel = 0;
-    if (assertionLevelOnly())
-    {
-      explLevel = assertionLevel;
+  // Compute the assertion level for this clause
+  int explLevel = 0;
+  if (assertionLevelOnly())
+  {
+    explLevel = assertionLevel;
     }
     else
     {
@@ -321,10 +322,15 @@ CRef Solver::reason(Var x) {
     // FIXME: at some point will need more information about where this explanation
     // came from (ie. the theory/sharing)
     Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
-    PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
-           ProofManager::getCnfProof()->registerConvertedClause(id, true);
-           // no need to pop current assertion as this is not converted to cnf
-           );
+    PROOF(ClauseId id = ProofManager::getSatProof()->registerClause(
+              real_reason, THEORY_LEMMA);
+          ProofManager::getCnfProof()->registerConvertedClause(id, true);
+          // explainPropagation() pushes the explanation on the assertion stack
+          // in CnfProof, so we need to pop it here. This is important because
+          // reason() may be called indirectly while adding a clause, which can
+          // lead to a wrong assertion being associated with the clause being
+          // added (see issue #2137).
+          ProofManager::getCnfProof()->popCurrentAssertion(););
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -1021,6 +1027,9 @@ void Solver::propagateTheory() {
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
         ClauseId id; // FIXME: mark it as explanation here somehow?
         addClause(explanation, true, id);
+        // explainPropagation() pushes the explanation on the assertion
+        // stack in CnfProof, so we need to pop it here.
+        PROOF(ProofManager::getCnfProof()->popCurrentAssertion();)
       }
     }
   }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 3c02ea13c..377e91897 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -580,6 +580,7 @@ REG0_TESTS = \
 	regress0/push-pop/inc-double-u.smt2 \
 	regress0/push-pop/incremental-subst-bug.cvc \
 	regress0/push-pop/issue1986.smt2 \
+	regress0/push-pop/issue2137.min.smt2 \
 	regress0/push-pop/quant-fun-proc-unfd.smt2 \
 	regress0/push-pop/simple_unsat_cores.smt2 \
 	regress0/push-pop/test.00.cvc \
diff --git a/test/regress/regress0/push-pop/issue2137.min.smt2 b/test/regress/regress0/push-pop/issue2137.min.smt2
new file mode 100644
index 000000000..372e8f1f3
--- /dev/null
+++ b/test/regress/regress0/push-pop/issue2137.min.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental --check-unsat-cores
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () Real)
+(declare-fun b () Bool)
+(assert (< 0 a))
+(assert (xor b (< 0 a 0) false))
+(check-sat)
+(assert (not b))
+(check-sat)