I compared the md5sum values with my versions.  All were identical except
for libmtwkbench.a (because I was using the version with the "volatile"
change).  I reverted to the one that matches the md5sum value you sent
(the original GPL version).  Of course, that didn't make any difference
because only libfinalized.a is being linked in and its md5sum value
matches your value.

Here's my results, in case you see something wrong:

/bin/rm -f test
gcc -o test -O3 -pipe -march=i686 -D_GNU_SOURCE -m32  -DEIF_IEEE_BEHAVIOR -I"/home/eiffel/Eiffel13.11.93542/studio/spec/linux-x86/include" -I.  -m32    C14/Cobj14.o C13/Cobj13.o C12/Cobj12.o C11/Cobj11.o C10/Cobj10.o C9/Cobj9.o C8/Cobj8.o C7/Cobj7.o C6/Cobj6.o C5/Cobj5.o C4/Cobj4.o C3/Cobj3.o C2/Cobj2.o C1/Cobj1.o E2/Eobj2.o E1/eref.o E1/epoly.o E1/esize.o E1/eplug.o E1/eskelet.o E1/enames.o E1/evisib.o E1/ececil.o E1/einit.o E1/eparents.o E1/emain.o \
		  "/home/eiffel/Eiffel13.11.93542/studio/spec/linux-x86/lib/libfinalized.a" -lm
hilbert 151% 
hilbert 151% md5sum /home/eiffel/Eiffel13.11.93542/studio/spec/linux-x86/lib/libfinalized.a
5a0d1717177c8ef04ae1e9ff04b7d860  /home/eiffel/Eiffel13.11.93542/studio/spec/linux-x86/lib/libfinalized.a
hilbert 152% ./test
-Infinity


Now what?  Do we need a version of libfinalized.a compiled with -O3 -g
and then we both step through ieee_init and see where things are different?
Any other ideas?