sbv-10.11: SBVTestSuite/GoldFiles/optFloat2d.gold
Optimal model:
max-y = Infinity :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------S52-------------------------
Binary layout: 0 11111111111 0000000000000000000000000000000000000000000000000000
Hex layout: 7FF0 0000 0000 0000
Precision: Double
Sign: Positive
Exponent: 1024 (Stored: 2047, Bias: 1023)
Classification: FP_INFINITE
Value: Infinity
x = Infinity :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------S52-------------------------
Binary layout: 0 11111111111 0000000000000000000000000000000000000000000000000000
Hex layout: 7FF0 0000 0000 0000
Precision: Double
Sign: Positive
Exponent: 1024 (Stored: 2047, Bias: 1023)
Classification: FP_INFINITE
Value: Infinity
toMetricSpace(max-y) = 18442240474082181120 :: 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 1111 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000
Hex layout: FFF0 0000 0000 0000
Type: Unsigned 64-bit word
Binary: 0b1111111111110000000000000000000000000000000000000000000000000000
Octal: 0o1777600000000000000000
Decimal: 18442240474082181120
Hex: 0xfff0000000000000