mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix for unintialized variable m_conflict_lvl

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-24 17:01:46 -07:00
parent ef7915858b
commit b2ebd095cb
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/maxres.cpp
View file

@ -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);

1
src/sat/sat_solver.cpp
View file

@ -964,6 +964,7 @@ namespace sat {
set_conflict(justification(), ~lit);
flet<bool> _min1(m_config.m_minimize_core, false);
flet<bool> _min2(m_config.m_minimize_core_partial, false);
m_conflict_lvl = 1;
resolve_conflict_for_unsat_core();
m_assumptions.pop_back();
weight += weights[i];