mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-05 02:40:24 +00:00
Code Activity

debug

Browse source
This commit is contained in:
Jakob Rath 2023-02-02 14:48:31 +01:00
parent ae41f82939
commit bdf20f513b
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1423,9 +1423,12 @@ namespace polysat {
continue; continue;
size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); }); size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); });
if (undefs == 1) { if (undefs == 1) {
LOG("Missed boolean propagation of clause: " << cl); verbose_stream() << "Missed boolean propagation of clause: " << cl << "\n";
for (sat::literal lit : cl) { for (sat::literal lit : cl) {
LOG(" " << lit_pp(*this, lit)); verbose_stream() << " " << lit_pp(*this, lit);
if (count(m_bvars.watch(lit), &cl) != 0)
verbose_stream() << " (bool-watched)";
verbose_stream() << "\n";
} }
} }
VERIFY(undefs != 1); VERIFY(undefs != 1);