mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-05 05:00:23 +00:00
Code Activity

count

Browse source
This commit is contained in:
Jakob Rath 2022-10-04 14:08:44 +02:00
parent 3d27ec41d0
commit 9cc9d1fac4
5 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/conflict.cpp
View file

@ -343,9 +343,9 @@ namespace polysat {
// resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
SASSERT(contains(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(count(cl, lit) > 0);
SASSERT(!contains(~lit));
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
SASSERT(count(cl, ~lit) == 0);
remove(s.lit2cnstr(lit));
for (sat::literal other : cl)