mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fix eval_invariant

Browse source
This commit is contained in:
Jakob Rath 2023-03-05 12:42:02 +01:00
parent 0433f81f78
commit 5067707a9c
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1668,13 +1668,19 @@ namespace polysat {
signed_constraint const c = lit2cnstr(lit); signed_constraint const c = lit2cnstr(lit);
if (!all_of(c->vars(), [this](pvar w) { return is_assigned(w); })) if (!all_of(c->vars(), [this](pvar w) { return is_assigned(w); }))
continue; continue;
if (c.is_always_true() || c.is_always_false())
continue;
lbool const bvalue = m_bvars.value(lit); lbool const bvalue = m_bvars.value(lit);
lbool const pvalue = c.eval(*this); lbool const pvalue = c.eval(*this);
if (bvalue != l_undef && pvalue != l_undef && bvalue != pvalue) { if (bvalue != l_undef && pvalue != l_undef && bvalue != pvalue) {
verbose_stream() << "missed bool/eval conflict: " << lit_pp(*this, lit) << "\n"; verbose_stream() << "missed bool/eval conflict: " << lit_pp(*this, lit) << "\n";
return false; return false;
} }
if (bvalue == l_undef && pvalue != l_undef) { bool const on_search_stack =
any_of(m_search, [lit](auto const& item) {
return item.is_boolean() && (item.lit() == lit || item.lit() == ~lit);
});
if (on_search_stack && bvalue == l_undef && pvalue != l_undef) {
verbose_stream() << "missed evaluation: " << lit_pp(*this, lit) << "\n"; verbose_stream() << "missed evaluation: " << lit_pp(*this, lit) << "\n";
return false; return false;
} }