Make registration of unit clauses more robust

Fixes #3959. It can happen that we generate a lemma that results in a
unit clause that matches a unit clause that was added as an input.
However, we are asserting that a unit clause can only be registered as
either one of them. This commit fixes the issue by only registering a
unit clause from a lemma if it is not already satisfied. I chose this
fix because the existing code doesn't seem to do anything (in terms of
solving) for the case where we have a unit clause that is already
satisfied because of an input unit clause.

2 files changed, 22 insertions, 11 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6abaa30c6..80cce599f 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1956,22 +1956,24 @@ CRef Solver::updateLemmas() {
         clauses_persistent.push(lemma_ref);
       }
       attachClause(lemma_ref);
-    } else {
-      PROOF
-        (
-         Node cnf_assertion = lemmas_cnf_assertion[j].first;
-         Node cnf_def = lemmas_cnf_assertion[j].second;
-
-         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
-         ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
-         ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
-         ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
-         );
     }
 
     // If the lemma is propagating enqueue its literal (or set the conflict)
     if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
       if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
+        if (PROOF_ON() && lemma.size() == 1)
+        {
+          Node cnf_assertion = lemmas_cnf_assertion[j].first;
+          Node cnf_def = lemmas_cnf_assertion[j].second;
+
+          Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3) "
+                           << cnf_assertion << value(lemma[0]) << std::endl;
+          ClauseId id = ProofManager::getSatProof()->registerUnitClause(
+              lemma[0], THEORY_LEMMA);
+          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
+        }
+
         if (value(lemma[0]) == l_False) {
           // We have a conflict
           if (lemma.size() > 1) {
diff --git a/test/regress/regress0/nl/issue3959.smt2 b/test/regress/regress0/nl/issue3959.smt2
new file mode 100644
index 000000000..d538db591
--- /dev/null
+++ b/test/regress/regress0/nl/issue3959.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --produce-unsat-cores --incremental
+; EXPECT: sat
+(set-logic QF_UFNIA)
+(declare-const v10 Bool)
+(declare-const i12 Int)
+(declare-const i16 Int)
+(push 1)
+(assert (=> (<= (mod i12 38) i16) v10))
+(check-sat)