From 19b858dbea1ae968a2f886213208fb53220cb059 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Feb 2018 04:00:32 -0800 Subject: [PATCH] fix reset code for level marking Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 2 +- src/sat/sat_solver.cpp | 9 +++++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 3b9b81448..e5dd057bb 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1389,7 +1389,7 @@ namespace sat { } } } - else { + else if (lvl(lit) < m_conflict_lvl) { slack -= std::abs(coeff); m_lemma.push_back(~lit); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e384a944d..84a875d55 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2536,8 +2536,13 @@ namespace sat { } num = i; // reset m_diff_levels. - for (i = 0; i < num; i++) - m_diff_levels[lvl(lits[i])] = false; + for (i = 0; i < num; i++) { + literal lit = lits[i]; + if (value(lit) == l_false) { + VERIFY(lvl(lit) < m_diff_levels.size()); + m_diff_levels[lvl(lit)] = false; + } + } return glue < max_glue; }