(let-const x f32)
(let-const y f64)
(let-const z f32)
(let-const w f32)
(let-const v f32)
(let-const u f64)
(let-const r f64)
(let-const s f64)
(push)
(assert (bool.not (f32.is_nan x)))
(assert (f32.is_nan x))
(check-sat)
(pop 1)
(push)
(assert (f32.ne x (f32 nan)))
(assert (f32.is_nan x))
(check-sat)
(pop 1)
(assert (f32.eq x (f32 0.504)))
(assert (f32.eq z (f32.ceil x)))
(assert (f32.eq w (f32.floor x)))
(assert (f32.eq v (f32.trunc x)))
(check-sat)
(get-model)
(pop 1)
(push)
(assert (f32.eq x (f32.neg (f32 2.7))))
(assert (f32.eq z (f32.ceil x)))
(assert (f32.eq w (f32.floor x)))
(assert (f32.eq v (f32.trunc x)))
(check-sat)
(get-model)
(pop 1)
(push)
(assert (f64.is_nan u))
(check-sat)
(pop 1)
(push)
(assert (f64.eq y (f64 314159265359.000)))
(assert (f64.eq r (f64.div (f64 1.0) (f64 0.0))))
(assert
  (f64.eq
    s
    (f64 -338460706455329128135018695364373065576360054171204343201037173805357995568625611429596369334345869072216864991017687935090688.000000)))
(check-sat)
(get-model)
(pop 1)
