mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

wlist_invariant

Browse source
This commit is contained in:
Jakob Rath 2022-01-20 17:47:17 +01:00
parent 543ad2f205
commit daf23cfe02
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -975,7 +975,7 @@ namespace polysat {
} }
unsigned expected_watches = std::min(2u, c->vars().size()); unsigned expected_watches = std::min(2u, c->vars().size());
if (num_watches != expected_watches) if (num_watches != expected_watches)
LOG("wrong number of watches: " << c); LOG("wrong number of watches: " << sc << " vars: " << sc->vars());
SASSERT_EQ(num_watches, expected_watches); SASSERT_EQ(num_watches, expected_watches);
} }
return true; return true;