mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #6107

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-27 20:51:30 -07:00
parent 61f5489223
commit 4c8f6b60ce
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/sat/smt/pb_solver.cpp
View file

@ -596,12 +596,13 @@ namespace pb {
s().reset_mark(v); s().reset_mark(v);
--m_num_marks; --m_num_marks;
} }
if (idx == 0 && !_debug_conflict) { if (idx == 0 && !_debug_conflict && m_num_marks > 0) {
_debug_conflict = true; _debug_conflict = true;
_debug_var2position.reserve(s().num_vars()); _debug_var2position.reserve(s().num_vars());
for (unsigned i = 0; i < lits.size(); ++i) { for (unsigned i = 0; i < lits.size(); ++i) {
_debug_var2position[lits[i].var()] = i; _debug_var2position[lits[i].var()] = i;
} }
IF_VERBOSE(0, verbose_stream() << "num marks: " << m_num_marks << "\n");
IF_VERBOSE(0, IF_VERBOSE(0,
active2pb(m_A); active2pb(m_A);
uint64_t c = 0; uint64_t c = 0;
@ -617,20 +618,19 @@ namespace pb {
} }
} }
m_num_marks = 0; m_num_marks = 0;
resolve_conflict(); resolve_conflict();
exit(0);
} }
--idx; --idx;
} }
} }
lbool solver::resolve_conflict() { lbool solver::resolve_conflict() {
if (0 == m_num_propagations_since_pop) { if (0 == m_num_propagations_since_pop)
return l_undef; return l_undef;
}
if (s().m_config.m_pb_resolve == sat::PB_ROUNDING) { if (s().m_config.m_pb_resolve == sat::PB_ROUNDING)
return resolve_conflict_rs(); return resolve_conflict_rs();
}
m_overflow = false; m_overflow = false;
reset_coeffs(); reset_coeffs();