I am including this summary of what we have discovered so far, though most
of the communication was done directly via e-mail with Manu.

After considerable experimentation, it appears that this is a bug in the
gcc optimizer.  When the run-time is compiled with -O0, a compiler linked
with that runtime produces correct C code.  When the runtime is compiled with
-O3, a compiler linked with that runtime produces wrong C code.
Note that this only happens with the gcc version Manu is currently using:

   gcc (GCC) 4.2.4 (Ubuntu 4.2.4-1ubuntu4)

With my version (gcc (GCC) 4.4.7 20120313 (Red Hat 4.4.7-4)), it seems to
generate correct C code with optimization level -O3.

Since the runtime for 7.3 does not have this problem, I wonder whether 
your compiler was updated to a newer version after 7.3 was released.  I also
do not understand why you cannot reproduce this problem, since the 
file libmtwkbench.a seems to have incorrect code for ieee_init
(inlined into eif_rtinit).

I have attached the log of the gdb session when stepping through routine
ieee_init (in main.c).  It looks like that routine is inlined and that
the inlined version does not set values like ` eif_real_64_negative_infinity'
correctly (it is set to 0 instead of -inf).