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

guard against different bitwidth

Browse source
This commit is contained in:
Jakob Rath 2023-03-09 13:51:10 +01:00
parent 9773ce60d6
commit dba8a4b73a
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -749,6 +749,8 @@ namespace polysat {
if (!d->is_ule()) if (!d->is_ule())
continue; continue;
auto u_l_k = inequality::from_ule(d); auto u_l_k = inequality::from_ule(d);
if (u_l_k.rhs().power_of_2() != m.power_of_2())
continue;
// a <= k or x <= k // a <= k or x <= k
k = u_l_k.rhs(); k = u_l_k.rhs();
if (!k.is_val()) if (!k.is_val())