From b2ebd095cb76eacb9fa4f083b1300e68f0035626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Aug 2015 17:01:46 -0700 Subject: [PATCH] fix for unintialized variable m_conflict_lvl Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 4 +++- src/sat/sat_solver.cpp | 1 + 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 693200f61..f4d8e1b43 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -228,7 +228,6 @@ public: switch (is_sat) { case l_true: get_current_correction_set(cs); - IF_VERBOSE(2, display_vec(verbose_stream() << "correction set: ", cs);); if (cs.empty()) { m_found_feasible_optimum = m_model.get() != 0; m_lower = m_upper; @@ -350,9 +349,11 @@ public: is_sat = minimize_core(core); ++m_stats.m_num_cores; if (is_sat != l_true) { + IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";); break; } if (core.empty()) { + IF_VERBOSE(100, verbose_stream() << "(opt.maxres core is empty)\n";); cores.reset(); m_lower = m_upper; return l_true; @@ -470,6 +471,7 @@ public: SASSERT(!core.empty()); rational w = split_core(core); TRACE("opt", display_vec(tout << "minimized core: ", core);); + IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core);); max_resolve(core, w); fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr())); s().assert_expr(fml); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index db82cbe0e..9d4f5df0f 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -964,6 +964,7 @@ namespace sat { set_conflict(justification(), ~lit); flet _min1(m_config.m_minimize_core, false); flet _min2(m_config.m_minimize_core_partial, false); + m_conflict_lvl = 1; resolve_conflict_for_unsat_core(); m_assumptions.pop_back(); weight += weights[i];