Fix for PR4235: to build a floating-point value from integer parts,