mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
WMax conflict budget bug fix
This commit is contained in:
parent
e1d7f5deba
commit
24b35fb925
|
@ -84,6 +84,9 @@ namespace opt {
|
|||
if (m.canceled()) {
|
||||
is_sat = l_undef;
|
||||
}
|
||||
if (is_sat == l_undef) {
|
||||
break;
|
||||
}
|
||||
if (is_sat == l_false) {
|
||||
TRACE("opt", tout << "Unsat\n";);
|
||||
break;
|
||||
|
@ -97,9 +100,6 @@ namespace opt {
|
|||
//DEBUG_CODE(verify_cores(cores););
|
||||
s().assert_expr(fml);
|
||||
}
|
||||
else {
|
||||
//DEBUG_CODE(verify_cores(cores););
|
||||
}
|
||||
update_cores(wth(), cores);
|
||||
wth().init_min_cost(m_upper - m_lower);
|
||||
trace_bounds("wmax");
|
||||
|
|
Loading…
Reference in a new issue