https://gcc.gnu.org/bugzilla/show_bug.cgi?id=71231
--- Comment #12 from Marc Glisse <glisse at gcc dot gnu.org> --- -fwrapv seems to fix it. As far as I can tell, the multiplication is done in 32 bits, VRP detects that the numbers are nonnegative, so zeroing the sign bit of the result of the mult+add can be assumed to be a NOP.
