http://gcc.gnu.org/bugzilla/show_bug.cgi?id=49048
--- Comment #2 from Cecilio <s.cecilio at gmail dot com> 2011-05-18 20:23:23 UTC --- printf output is 5798.12. I think this is the expected output. Does this confirms your guess? (sorry, I don't understand your previous answer. My knowledge about GCC is just the name "GCC". I know nothing about gcc and its internals. I can only report that there is a bug somewhere in the gcc compiler. What is the next step I should do to help to solve this? Have I to report the bug in another place? Please, where? Thanks, Cecilio