mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 18:36:41 +00:00
Code Activity

fix assertion failure

Browse source
This commit is contained in:
Jakob Rath 2022-11-23 13:21:58 +01:00
parent 2787a22007
commit 58c299dc33
1 changed files with 17 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/math/polysat/solver.cpp
View file

@ -693,14 +693,18 @@ namespace polysat {
LOG(m_justification[v]); LOG(m_justification[v]);
LOG("Conflict: " << m_conflict); LOG("Conflict: " << m_conflict);
justification const& j = m_justification[v]; justification const& j = m_justification[v];
// NOTE: propagation level may be out of order (cf. replay), but decisions are always in order
if (j.level() <= base_level()) {
if (j.is_decision()) {
report_unsat();
return;
}
continue;
}
if (j.is_decision()) { if (j.is_decision()) {
if (j.level() <= base_level())
break;
revert_decision(v); revert_decision(v);
return; return;
} }
if (j.level() <= base_level()) // propagation level may be out of order (cf. replay)
continue;
m_conflict.resolve_value(v); m_conflict.resolve_value(v);
} }
else { else {
@ -714,17 +718,20 @@ namespace polysat {
LOG(bool_justification_pp(m_bvars, lit)); LOG(bool_justification_pp(m_bvars, lit));
LOG("Literal " << lit << " is " << lit2cnstr(lit)); LOG("Literal " << lit << " is " << lit2cnstr(lit));
LOG("Conflict: " << m_conflict); LOG("Conflict: " << m_conflict);
// NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
// Thus we can only skip base level literals here, instead of aborting the loop.
if (m_bvars.level(var) <= base_level()) {
if (m_bvars.is_decision(var)) {
report_unsat(); // decisions are always in order
return;
}
continue;
}
SASSERT(!m_bvars.is_assumption(var)); SASSERT(!m_bvars.is_assumption(var));
if (m_bvars.is_decision(var)) { if (m_bvars.is_decision(var)) {
if (m_bvars.level(var) <= base_level())
break;
revert_bool_decision(lit); revert_bool_decision(lit);
return; return;
} }
// NOTE: the levels of boolean literals on the stack aren't always ordered by level (cf. replay functionality in pop_levels).
// Thus we can only skip base level literals here, instead of aborting the loop.
if (m_bvars.level(var) <= base_level())
continue;
if (m_bvars.is_bool_propagation(var)) if (m_bvars.is_bool_propagation(var))
// TODO: this could be a propagation at an earlier level. // TODO: this could be a propagation at an earlier level.
// do we really want to resolve these eagerly? // do we really want to resolve these eagerly?