(define-sort FP8 () (_ FloatingPoint 3 5))
(set-info :status sat)
(declare-fun e () FP8)
(declare-fun r () FP8)
(declare-const rm RoundingMode)
(assert (= e (fp #b0 #b011 #b0000)))
(assert (= r (fp #b0 #b100 #b0000)))
(assert (= (fp.fma rm e e (fp.fma rm e e e)) (fp #b0 #b100 #b1000)))
(assert (= rm RNA))
(check-sat)