mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

report_unsat: propagate after backjump to restore conflict dependencies

Browse source
This commit is contained in:
Jakob Rath 2023-03-17 13:07:07 +01:00
parent 6c9cf6182c
commit 2000ab2cfc
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1507,7 +1507,16 @@ namespace polysat {
}
void solver::report_unsat() {
// NOTE: backjump may destroy dependencies of the conflict (e.g., lose boolean propagations).
// so we reset the conflict, backjump, then propagate to restore the conflicts
m_conflict.reset();
backjump(base_level());
while (can_repropagate_units() || should_add_pwatch() || can_propagate() || can_repropagate()) {
if (can_repropagate_units()) repropagate_units();
else if (should_add_pwatch()) add_pwatch();
else if (can_propagate()) propagate();
else if (can_repropagate()) repropagate();
}
VERIFY(!m_conflict.empty());
}