https://gcc.gnu.org/bugzilla/show_bug.cgi?id=63332
--- Comment #2 from Jonathan Wakely <redi at gcc dot gnu.org> --- Yes, there must be some difference that isn't visible in the serialized output, which would imply the values fail to do a proper round trip, so we're not writing them with enough precision. Maybe we should use hexfloat output for serializing distributions, not decimal.