packages feed

sbv-8.1: SBVTestSuite/GoldFiles/optFloat3.gold

Optimal model:
  max-x+y        = 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)
  x              = 1.7014117e38 :: Float
                  3  2          1         0
                  1 09876543 21098765432109876543210
                  S ---E8--- ----------F23----------
          Binary: 0 11111101 11111111111111111111111
             Hex: 7EFF FFFF
       Precision: SP
            Sign: Positive
        Exponent: 126 (Stored: 253, Bias: 127)
       Hex-float: +0x1.fffffep126
           Value: +1.7014117e38 (NORMAL)
  y              = 1.7014117e38 :: Float
                  3  2          1         0
                  1 09876543 21098765432109876543210
                  S ---E8--- ----------F23----------
          Binary: 0 11111101 11111111111111111111111
             Hex: 7EFF FFFF
       Precision: SP
            Sign: Positive
        Exponent: 126 (Stored: 253, Bias: 127)
       Hex-float: +0x1.fffffep126
           Value: +1.7014117e38 (NORMAL)
  metric-max-x+y =   0xff7fffff :: Word32