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

fix unsound backjump for out of order search stacks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-02 19:12:49 -07:00
parent 48e663776b
commit 6fb4e0d5a9
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -450,9 +450,7 @@ namespace polysat {
continue;
justification& j = m_justification[v];
LOG("Justification: " << j);
if (j.level() <= base_level())
break;
if (!resolve_value(v) && j.is_decision()) {
if (j.level() > base_level() && !resolve_value(v) && j.is_decision()) {
revert_decision(v);
return;
}
@ -464,8 +462,8 @@ namespace polysat {
sat::bool_var const var = lit.var();
if (!m_conflict.is_bmarked(var))
continue;
if (m_bvars.level(var) <= base_level()) // TODO: this doesn't work with out-of-level-order iteration.
break;
if (m_bvars.level(var) <= base_level())
continue;
if (m_bvars.is_decision(var)) {
revert_bool_decision(lit);
return;
@ -624,7 +622,8 @@ namespace polysat {
clause_builder reason_builder = m_conflict.build_lemma();
bool contains_lit = std::find(reason_builder.begin(), reason_builder.end(), ~lit);
SASSERT(std::find(reason_builder.begin(), reason_builder.end(), ~lit));
#if 0
if (!contains_lit) {
// At this point, we do not have ~lit in the reason.
// For now, we simply add it (thus weakening the reason)
@ -639,6 +638,7 @@ namespace polysat {
std::cout << "ADD extra " << ~lit << "\n";
reason_builder.push(~lit);
}
#endif
clause_ref reason = reason_builder.build();
if (reason->empty()) {