Make registration of unit clauses more robust (#3965)

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.

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6abaa30c65d4ba8c7a565d5630669a1afa4eefc7..80cce599fb65399826626064d024e61a9ba26713 100644 (file)
--- 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/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5ef9f9f6c09e9f468abfbf49ef98f3846290a8d7..d96360ad64b4678360c8d6753c5ccddb256f5660 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -574,6 +574,7 @@ set(regress_0_tests
   regress0/nl/issue3718.smt2
   regress0/nl/issue3719.smt2
   regress0/nl/issue3729-cm-solved-tf.smt2
+  regress0/nl/issue3959.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2

diff --git a/test/regress/regress0/nl/issue3959.smt2 b/test/regress/regress0/nl/issue3959.smt2
new file mode 100644 (file)
index 0000000..cce64a8
--- /dev/null
+++ b/test/regress/regress0/nl/issue3959.smt2
@@ -0,0 +1,12 @@
+; REQUIRES: proof
+; COMMAND-LINE: --produce-unsat-cores --incremental
+; EXPECT: sat
+
+; Note: the logic must include UF to trigger the bug
+(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)