> I'm a comp. engineer, so I know it's ultimately related to the binary
> value of 15.25 which cannot be precisely represented (without an
> infinite number of bits)

Unfortunately no, it looks like a bug.  Because 15.25 is 1111.01 in
binary -- exactly.

Paolo