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

no need to handle both x=y and y=x

Browse source
This commit is contained in:
Jakob Rath 2023-07-20 14:54:21 +02:00
parent 73757e3fa4
commit ec4be975ee
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/slicing.cpp
View file

@ -769,6 +769,9 @@ namespace polysat {
// m_disequality_conflict = n; // m_disequality_conflict = n;
} }
} }
// without this check, when p = x - y we would handle both x = y and y = x separately
if (body.is_unary())
break;
} }
} }