mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

Don't lose variables when aborting decisions

Browse source
This commit is contained in:
Jakob Rath 2022-12-19 14:02:47 +01:00
parent 69b41a7e70
commit ac0e9ebe5f
1 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -731,9 +731,16 @@ namespace polysat {
SASSERT(!m_search.assignment().contains(v)); SASSERT(!m_search.assignment().contains(v));
if (lemma) { if (lemma) {
add_clause(*lemma); add_clause(*lemma);
SASSERT(!is_conflict()); // if we have a conflict here, we could have produced this lemma already earlier if (is_conflict()) {
if (can_propagate()) // If we have a conflict here, we should have produced this lemma already earlier
LOG("Conflict after constraint::produce_lemma: TODO: should have found this lemma earlier");
m_free_pvars.unassign_var_eh(v);
return; return;
}
if (can_propagate()) {
m_free_pvars.unassign_var_eh(v);
return;
}
} }
if (c) { if (c) {
LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!"); LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
@ -754,6 +761,7 @@ namespace polysat {
return; return;
case find_t::resource_out: case find_t::resource_out:
UNREACHABLE(); // TODO: abort solving UNREACHABLE(); // TODO: abort solving
m_free_pvars.unassign_var_eh(v);
return; return;
} }
} }