(set-logic QF_BVFP)
(declare-fun bv () (_ BitVec 32))
(assert (not (fp.isNaN ((_ to_fp 8 24) bv))))
(assert (not (and (fp.isInfinite ((_ to_fp 8 24) bv))
          (fp.isPositive ((_ to_fp 8 24) bv)))))
(assert (not (and (fp.isZero ((_ to_fp 8 24) bv)) (fp.isNegative ((_ to_fp 8 24) bv)))))
(assert (let ((a!1 (ite (and (fp.isNegative ((_ to_fp 8 24) bv))
                     (fp.isNegative (_ +zero 8 24)))
                (_ -zero 8 24)
                (_ +zero 8 24)))
      (a!4 ((_ to_fp 8 24)
             (ite (= #b1 ((_ extract 31 31) bv))
                  (bvsub bv #x00000001)
                  (bvadd bv #x00000001)))))
(let ((a!2 (ite (and (fp.isZero ((_ to_fp 8 24) bv)) (fp.isZero (_ +zero 8 24)))
                a!1
                (ite (fp.gt ((_ to_fp 8 24) bv) (_ +zero 8 24))
                     ((_ to_fp 8 24) bv)
                     (_ +zero 8 24))))
      (a!5 (ite (and (fp.isZero a!4) (fp.isZero (_ +zero 8 24)))
                (ite (and (fp.isNegative a!4) (fp.isNegative (_ +zero 8 24)))
                     (_ -zero 8 24)
                     (_ +zero 8 24))
                (ite (fp.gt a!4 (_ +zero 8 24)) a!4 (_ +zero 8 24)))))
(let ((a!3 (ite (or (fp.isNaN ((_ to_fp 8 24) bv)) (fp.isNaN (_ +zero 8 24)))
                (_ NaN 8 24)
                a!2))
      (a!6 (fp.add roundNearestTiesToEven
                   (fp #b0 #x7f #b00000000000000000000000)
                   (ite (or (fp.isNaN a!4) (fp.isNaN (_ +zero 8 24)))
                        (_ NaN 8 24)
                        a!5))))
  (not (fp.geq (fp.div roundNearestTiesToEven
                       (fp #b0 #x7f #b00000000000000000000000)
                       (fp.add roundNearestTiesToEven
                               (fp #b0 #x7f #b00000000000000000000000)
                               a!3))
               (fp.div roundNearestTiesToEven
                       (fp #b0 #x7f #b00000000000000000000000)
                       a!6)))))))
(check-sat)