(declare-const x Bool) (declare-fun c () Float64) (push 1) (assert (or x (fp.gt c (fp (_ bv0 1) (_ bv2047 11) (_ bv1 52))))) (set-info :status sat) (check-sat) (pop 1) (assert (fp.gt c ((_ to_fp 11 53) RNE (_ bv2 32)))) (set-info :status sat) (check-sat)