(declare-fun c () Float64)
(assert (exists ((m Float64)) (= c (fp (_ bv1 1) (_ bv0 11) (_ bv0 52)))))
(push 1)
(assert (forall ((m Float64)) false))
(set-info :status unsat)
(check-sat)
(pop 1)
(set-info :status sat)
(check-sat)