sbv-14.4: SBVTestSuite/GoldFiles/optFloat2c.gold
Optimal model:
x = 1.7976931348623157e308 :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------S52-------------------------
Binary layout: 0 11111111110 1111111111111111111111111111111111111111111111111111
Hex layout: 7FEF FFFF FFFF FFFF
Precision: Double
Sign: Positive
Exponent: 1023 (Stored: 2046, Bias: 1023)
Classification: FP_NORMAL
Binary: 0b1.1111111111111111111111111111111111111111111111111111p+1023
Octal: 0o1.777777777777777774p+1023
Decimal: 1.7976931348623157e308
Hex: 0xf.ffffffffffff8p+1020
toMetricSpace(max-x) = 18442240474082181119 :: Word64
6 5 4 3 2 1 0
3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210
Binary layout: 1111 1111 1110 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111
Hex layout: FFEF FFFF FFFF FFFF
Type: Unsigned 64-bit word
Binary: 0b1111111111101111111111111111111111111111111111111111111111111111
Octal: 0o1777577777777777777777
Decimal: 18442240474082181119
Hex: 0xffefffffffffffff
max-x = 1.7976931348623157e308 :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------S52-------------------------
Binary layout: 0 11111111110 1111111111111111111111111111111111111111111111111111
Hex layout: 7FEF FFFF FFFF FFFF
Precision: Double
Sign: Positive
Exponent: 1023 (Stored: 2046, Bias: 1023)
Classification: FP_NORMAL
Binary: 0b1.1111111111111111111111111111111111111111111111111111p+1023
Octal: 0o1.777777777777777774p+1023
Decimal: 1.7976931348623157e308
Hex: 0xf.ffffffffffff8p+1020