diff options
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 24 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/nl/issue3959.smt2 | 12 |
3 files changed, 26 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/CMakeLists.txt b/test/regress/CMakeLists.txt index 5ef9f9f6c..d96360ad6 100644 --- 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 index 000000000..cce64a848 --- /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) |