(set-logic QF_FP)
(set-option :produce-models true)
(declare-const p (_ FloatingPoint 11 53))
(declare-const b (_ FloatingPoint 8 24))
(declare-const m (_ FloatingPoint 8 24))
(declare-const lo (_ FloatingPoint 11 53))
(declare-const hi (_ FloatingPoint 11 53))
(assert (fp.gt p (_ +zero 11 53)))
(assert (not (fp.isInfinite p)))
(assert (not (fp.isNaN p)))
(assert (fp.gt b (_ +zero 8 24)))
(assert (not (fp.isInfinite b)))
(assert (not (fp.isNaN b)))
(assert (fp.gt m (_ +zero 8 24)))
(assert (fp.leq m b))
(assert (fp.geq lo (_ +zero 11 53)))
(assert (not (fp.isInfinite hi)))
(assert (fp.lt lo hi))
(assert (not (fp.gt (fp.sub RNE hi lo) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000))))
(assert (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p lo)))) m))
(assert (fp.lt ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p hi)))) m))
(assert (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p (fp.add RNE lo (fp #b0 #b01111111011 #b0011001100110011001100110011001100110011001100110011)))))) m))
(check-sat)
(get-value (p b m lo hi))