mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

remove overly strict assertion

Browse source
This commit is contained in:
Jakob Rath 2023-11-07 13:14:47 +01:00
parent 3796a46b55
commit f51b194017
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/saturation.cpp
View file

@ -129,7 +129,6 @@ namespace polysat {
continue;
if (!i.as_signed_constraint().contains_var(y))
continue;
SASSERT_EQ(s.get_level(y), s.get_level(x)); // propagated by slicing egraph since they are equivalent
SASSERT(s.m_search.get_pvar_index(y) < s.m_search.get_pvar_index(x)); // y was the earlier one since we are currently resolving x
pdd const lhs = i.lhs().subst_pdd(x, s.var(y));
pdd const rhs = i.rhs().subst_pdd(x, s.var(y));