Steven, there's something wrong with the arithmetic on your machine, but I can't guess what from here (perhaps you have a non-standard rounding mode enabled, perhaps your CPU is broken, ...).

In binary, (2**53-1)/2**53 * 2049 is:

0.11111111111111111111111111111111111111111111111111111
times
100000000001.0

which is exactly:

100000000000.11111111111111111111111111111111111111111 011111111111

I inserted a blank after the 53rd bit.  Because the tail (011111111111) is "less than half", under any rounding mode _except_ "to +inf" that should be rounded to the 53-bit result:

100000000000.11111111111111111111111111111111111111111

That's strictly less than 2049, so int() of that should deliver 2048.

For a start, is it the multiplication that's broken on your machine, or the int() part?

These are the expected hex values (same as the binary values shown above, but easier to get Python to show - and these should be identical across all 754-conforming boxes using the default rounding mode):

>>> x = 1.-2.**-53
>>> y = 2049.0
>>> x.hex()
'0x1.fffffffffffffp-1'
>>> y.hex()
'0x1.0020000000000p+11'
>>> (x*y).hex()
'0x1.001ffffffffffp+11'