sbv-8.11: SBVTestSuite/GoldFiles/arbFp_opt_1.gold

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