Hi Xavier,

But probably you don't need
the interval arithmetic in the end: both "top" and "top + 1" convert
to floats without rounding (*),

Yes, you're right :).

and the scaling by 2^n can be achieved
with "ldexp".

What is the semantics of "ldexp" in bounds cases? For example, I tried "ldexp max_float max_int;;" which returns "8.98846567431157854e+307". Shouldn't we expect something like "infinity"?

Best,

Tung.