(set-logic QF_FP)
(set-info :status unsat)
(set-option :produce-unsat-assumptions true)
(declare-const a Float16);
(declare-const b Float16);
(declare-const rm RoundingMode);
(define-fun b1 () Bool (= (fp.abs a) (fp.abs (fp.neg a))))
(define-fun b2 () Bool (not (and (fp.isNormal (fp.neg a)) (not (fp.isNormal a)))))
(define-fun b3 () Bool (not (and (fp.isSubnormal (fp.neg a)) (not (fp.isSubnormal a)))))
(define-fun b5 () Bool (not (fp.isInfinite b)))
(assert (! (not (fp.isNaN b)) :named a6))
(assert (! (not (fp.isNegative b)) :named a7))
(assert (! (fp.isPositive b) :named a8))
(assert (! (and (fp.leq a a) (not (fp.lt a a))) :named a9))
(assert (! (and (fp.geq (fp.sqrt RNE a) (fp.roundToIntegral RNE b)) (not (fp.gt (fp.add RNA a a) b))) :named a10))
(assert (! (fp.geq (fp.add RTN a b) (fp.sub RTN a b)) :named a11))
(assert (! (fp.leq (fp.mul RTP a (_ +zero 5 11)) (_ -zero 5 11)) :named a12))
(assert (! (fp.isNaN (fp.div RTP a (_ +zero 5 11))) :named a13))
(assert (! (fp.eq (fp.add rm (fp.mul RTZ a b) a) (fp.fma RTZ a b (fp.rem a b))) :named a14))
(check-sat-assuming ((= (fp.abs a) b) b1 b2 b3 (and (fp.isZero (fp.neg a)) (not (fp.isNormal a))) b5))
(get-unsat-assumptions)