(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 (fp #b1 #x7f #b00000000000000000000000)))
                (_ -zero 8 24)
                (_ +zero 8 24)))
      (a!6 ((_ 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 (fp #b1 #x7f #b00000000000000000000000)))
                a!1
                (ite (fp.gt ((_ to_fp 8 24) bv)
                            (fp #b1 #x7f #b00000000000000000000000))
                     ((_ to_fp 8 24) bv)
                     (fp #b1 #x7f #b00000000000000000000000))))
      (a!7 (ite (and (fp.isZero a!6)
                     (fp.isZero (fp #b1 #x7f #b00000000000000000000000)))
                (ite (and (fp.isNegative a!6)
                          (fp.isNegative (fp #b1 #x7f #b00000000000000000000000)))
                     (_ -zero 8 24)
                     (_ +zero 8 24))
                (ite (fp.gt a!6 (fp #b1 #x7f #b00000000000000000000000))
                     a!6
                     (fp #b1 #x7f #b00000000000000000000000)))))
(let ((a!3 (ite (or (fp.isNaN ((_ to_fp 8 24) bv))
                    (fp.isNaN (fp #b1 #x7f #b00000000000000000000000)))
                (_ NaN 8 24)
                a!2))
      (a!8 (fp.isNaN (ite (or (fp.isNaN a!6)
                              (fp.isNaN (fp #b1 #x7f #b00000000000000000000000)))
                          (_ NaN 8 24)
                          a!7)))
      (a!9 (fp.isZero (ite (or (fp.isNaN a!6)
                               (fp.isNaN (fp #b1 #x7f #b00000000000000000000000)))
                           (_ NaN 8 24)
                           a!7)))
      (a!10 (fp.isNegative (ite (or (fp.isNaN a!6)
                                    (fp.isNaN (fp #b1 #x7f #b00000000000000000000000)))
                                (_ NaN 8 24)
                                a!7)))
      (a!11 (fp.lt (fp #b0 #x7f #b00000000000000000000000)
                   (ite (or (fp.isNaN a!6)
                            (fp.isNaN (fp #b1 #x7f #b00000000000000000000000)))
                        (_ NaN 8 24)
                        a!7))))
(let ((a!4 (ite (and (fp.isZero (fp #b0 #x7f #b00000000000000000000000))
                     (fp.isZero a!3))
                (ite (or (fp.isNegative (fp #b0 #x7f #b00000000000000000000000))
                         (fp.isNegative a!3))
                     (_ -zero 8 24)
                     (_ +zero 8 24))
                (ite (fp.lt (fp #b0 #x7f #b00000000000000000000000) a!3)
                     (fp #b0 #x7f #b00000000000000000000000)
                     a!3)))
      (a!12 (ite a!11
                 (fp #b0 #x7f #b00000000000000000000000)
                 (ite (or (fp.isNaN a!6)
                          (fp.isNaN (fp #b1 #x7f #b00000000000000000000000)))
                      (_ NaN 8 24)
                      a!7))))
(let ((a!5 (fp.add roundNearestTiesToEven
                   (fp #b0 #x7f #b00000000000000000000000)
                   (ite (or (fp.isNaN (fp #b0 #x7f #b00000000000000000000000))
                            (fp.isNaN a!3))
                        (_ NaN 8 24)
                        a!4)))
      (a!13 (ite (and (fp.isZero (fp #b0 #x7f #b00000000000000000000000)) a!9)
                 (ite (or (fp.isNegative (fp #b0 #x7f #b00000000000000000000000))
                          a!10)
                      (_ -zero 8 24)
                      (_ +zero 8 24))
                 a!12)))
(let ((a!14 (fp.add roundNearestTiesToEven
                    (fp #b0 #x7f #b00000000000000000000000)
                    (ite (or (fp.isNaN (fp #b0 #x7f #b00000000000000000000000))
                             a!8)
                         (_ NaN 8 24)
                         a!13))))
  (not (fp.leq (fp.div roundNearestTiesToEven
                       a!5
                       (fp #b0 #x80 #b00000000000000000000000))
               (fp.div roundNearestTiesToEven
                       a!14
                       (fp #b0 #x80 #b00000000000000000000000)))))))))))
(check-sat)