https://gcc.gnu.org/bugzilla/show_bug.cgi?id=64308
--- Comment #2 from Marc Glisse <glisse at gcc dot gnu.org> --- You would need symbolic ranges, b and ret are in [0,m-1]. And then you are using that very specific x86 instruction that divides 64 bits by 32 bits but only works if the result fits in 32 bits. It works here because (m-1)*(m-1)/m<m is small enough, but that's very hard for the compiler to prove, and I don't know of another architecture with a similar instruction. (Related: PR58897, PR53100)