(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun e () (Array (_ BitVec 32) (_ BitVec 8)))
(define-fun t1 () (_ BitVec 24) (concat (select e (_ bv2 32)) (select e (_ bv1 32)) (select e (_ bv0 32))))
(define-fun t2 () Float32 ((_ to_fp 8 24) (concat (select e (_ bv3 32)) t1)))
(define-fun t3 () Float32 ((_ to_fp 8 24) (concat (select d (_ bv7 32)) (select d (_ bv6 32)) (select d (_ bv5 32)) (select d (_ bv4 32)))))
(assert (not (fp.lt (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) t3)))
(assert (fp.eq t2 t3))
(assert (not (fp.eq t2 ((_ to_fp 8 24) (concat (select d (bvadd (_ bv3 32) (bvmul (_ bv4 32) (bvsdiv (_ bv2 32) (ite (fp.gt (fp (_ bv0 1) (_ bv1 8) (_ bv0 23)) ((_ to_fp 8 24) (concat (select e (_ bv3 32)) t1))) (_ bv2 32) (_ bv0 32)))))) t1)))))
(set-info :status unsat)
(check-sat)