It seems that if bit 48 or above is set then there's a problem with printf
producing binary, shown by the attached short program. If bit 56 or above is set
then the problem is more severe. Any chance of a fix? :)
Carl.