Satisfiable. Model:
  s0 = 4.0 :: Real