mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 03:27:52 +00:00
Code Activity

update

Browse source
This commit is contained in:
Jakob Rath 2023-02-20 16:19:56 +01:00
parent 4cca164bb4
commit 455abb1db3
1 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/polysat/viable.cpp
View file

@ -1323,12 +1323,9 @@ namespace {
} }
while (e != first); while (e != first);
// Doesn't hold anymore: we may get new constraints with unassigned variables, see test_polysat::test_bench23_fi_lemma. // TODO: violated in bench27
// SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) == l_false || s.lit2cnstr(lit).is_currently_false(s); })); SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
// NSB review: bench23 exposes a scenario where s.m_bvars.value(lit) == l_true. So the viable lemma is mute, but the literal in the premise
// is a conflict.
// SASSERT(all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; }));
core.add_lemma("viable", lemma.build()); core.add_lemma("viable", lemma.build());
core.logger().log(inf_fi(*this, v)); core.logger().log(inf_fi(*this, v));
return true; return true;