sbv-10.11: SBVTestSuite/GoldFiles/optFloat3.gold
Optimal model:
max-x+y = 3.4028235e38 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------S23----------
Binary layout: 0 11111110 11111111111111111111111
Hex layout: 7F7F FFFF
Precision: Single
Sign: Positive
Exponent: 127 (Stored: 254, Bias: 127)
Classification: FP_NORMAL
Binary: 0b1.11111111111111111111111p+127
Octal: 0o3.77777774p+126
Decimal: 3.4028235e38
Hex: 0xf.fffffp+124
metric-max-x+y = 3.4028235e38 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------S23----------
Binary layout: 0 11111110 11111111111111111111111
Hex layout: 7F7F FFFF
Precision: Single
Sign: Positive
Exponent: 127 (Stored: 254, Bias: 127)
Classification: FP_NORMAL
Binary: 0b1.11111111111111111111111p+127
Octal: 0o3.77777774p+126
Decimal: 3.4028235e38
Hex: 0xf.fffffp+124
x = 1.7014117e38 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------S23----------
Binary layout: 0 11111101 11111111111111111111111
Hex layout: 7EFF FFFF
Precision: Single
Sign: Positive
Exponent: 126 (Stored: 253, Bias: 127)
Classification: FP_NORMAL
Binary: 0b1.11111111111111111111111p+126
Octal: 0o1.77777776p+126
Decimal: 1.7014117e38
Hex: 0x7.fffff8p+124
y = 1.7014117e38 :: Float
3 2 1 0
1 09876543 21098765432109876543210
S ---E8--- ----------S23----------
Binary layout: 0 11111101 11111111111111111111111
Hex layout: 7EFF FFFF
Precision: Single
Sign: Positive
Exponent: 126 (Stored: 253, Bias: 127)
Classification: FP_NORMAL
Binary: 0b1.11111111111111111111111p+126
Octal: 0o1.77777776p+126
Decimal: 1.7014117e38
Hex: 0x7.fffff8p+124
toMetricSpace(metric-max-x+y) = 4286578687 :: Word32
3 2 1 0
1098 7654 3210 9876 5432 1098 7654 3210
Binary layout: 1111 1111 0111 1111 1111 1111 1111 1111
Hex layout: FF7F FFFF
Type: Unsigned 32-bit word
Binary: 0b11111111011111111111111111111111
Octal: 0o37737777777
Decimal: 4286578687
Hex: 0xff7fffff