sbv-10.8: SBVTestSuite/GoldFiles/arbFp_opt_1.gold

Optimal model:
  s0 = 65504.0 :: FloatingPoint 5 11
  x  =   64511 :: Word16