sbv-8.1: SBVTestSuite/GoldFiles/optFloat1.gold
Objective "min-x": Optimal model:
x = -3.4028235e38 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------F23----------
Binary: 1 11111110 11111111111111111111111
Hex: FF7F FFFF
Precision: SP
Sign: Negative
Exponent: 127 (Stored: 254, Bias: 127)
Hex-float: -0x1.fffffep127
Value: -3.4028235e38 (NORMAL)
y = 9.351032988705757e-251 :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------F52-------------------------
Binary: 0 00011000000 0101011011001001110011000000001001101000111010000000
Hex: 0C05 6C9C C026 8E80
Precision: DP
Sign: Positive
Exponent: -831 (Stored: 192, Bias: 1023)
Hex-float: +0x1.56c9cc0268e8p-831
Value: +9.351032988705757e-251 (NORMAL)
min-x = 0x00800000 :: Word32
max-x = 0x00800000 :: Word32
min-y = 0x8c056c9cc0268e80 :: Word64
max-y = 0x8c056c9cc0268e80 :: Word64
Objective "max-x": Optimal model:
x = 3.4028235e38 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------F23----------
Binary: 0 11111110 11111111111111111111111
Hex: 7F7F FFFF
Precision: SP
Sign: Positive
Exponent: 127 (Stored: 254, Bias: 127)
Hex-float: +0x1.fffffep127
Value: +3.4028235e38 (NORMAL)
y = 9.351032988705757e-251 :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------F52-------------------------
Binary: 0 00011000000 0101011011001001110011000000001001101000111010000000
Hex: 0C05 6C9C C026 8E80
Precision: DP
Sign: Positive
Exponent: -831 (Stored: 192, Bias: 1023)
Hex-float: +0x1.56c9cc0268e8p-831
Value: +9.351032988705757e-251 (NORMAL)
min-x = 0xff7fffff :: Word32
max-x = 0xff7fffff :: Word32
min-y = 0x8c056c9cc0268e80 :: Word64
max-y = 0x8c056c9cc0268e80 :: Word64
Objective "min-y": Optimal model:
x = 3.4028235e38 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------F23----------
Binary: 0 11111110 11111111111111111111111
Hex: 7F7F FFFF
Precision: SP
Sign: Positive
Exponent: 127 (Stored: 254, Bias: 127)
Hex-float: +0x1.fffffep127
Value: +3.4028235e38 (NORMAL)
y = -1.7976931348623157e308 :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------F52-------------------------
Binary: 1 11111111110 1111111111111111111111111111111111111111111111111111
Hex: FFEF FFFF FFFF FFFF
Precision: DP
Sign: Negative
Exponent: 1023 (Stored: 2046, Bias: 1023)
Hex-float: -0x1.fffffffffffffp1023
Value: -1.7976931348623157e308 (NORMAL)
min-x = 0xff7fffff :: Word32
max-x = 0xff7fffff :: Word32
min-y = 0x0010000000000000 :: Word64
max-y = 0x0010000000000000 :: Word64
Objective "max-y": Optimal model:
x = -1.8892078e22 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------F23----------
Binary: 1 11001001 00000000000010010001000
Hex: E480 0488
Precision: SP
Sign: Negative
Exponent: 74 (Stored: 201, Bias: 127)
Hex-float: -0x1.00091p74
Value: -1.8892078e22 (NORMAL)
y = 1.7976931348623157e308 :: Double
6 5 4 3 2 1 0
3 21098765432 1098765432109876543210987654321098765432109876543210
S ----E11---- ------------------------F52-------------------------
Binary: 0 11111111110 1111111111111111111111111111111111111111111111111111
Hex: 7FEF FFFF FFFF FFFF
Precision: DP
Sign: Positive
Exponent: 1023 (Stored: 2046, Bias: 1023)
Hex-float: +0x1.fffffffffffffp1023
Value: +1.7976931348623157e308 (NORMAL)
min-x = 0x1b7ffb77 :: Word32
max-x = 0x1b7ffb77 :: Word32
min-y = 0xffefffffffffffff :: Word64
max-y = 0xffefffffffffffff :: Word64