(set-logic QF_BVFP)
(set-info :status sat)
(declare-fun _substvar_114_ () (_ BitVec 56))
(define-fun fp32_mantissa_bit_visible_for_int32 ((f Float32)) Bool (fp.gt f (_ +zero 8 24)))
(define-fun raw_cast_fp32_int56 ((f Float32)) (_ BitVec 56) (ite (fp32_mantissa_bit_visible_for_int32 (_ +zero 8 24)) _substvar_114_ #x00000000000000))
(define-fun cast_fp32_uint32 ((f Float32)) (_ BitVec 32) ((_ extract 31 0) (raw_cast_fp32_int56 (_ +zero 8 24))))
(declare-fun v_12$$1 () (_ BitVec 32))
(declare-fun v_144$$1 () (_ BitVec 32))
(assert (= v_144$$1 (cast_fp32_uint32 (_ +zero 8 24))))
(assert (= v_12$$1 v_144$$1))
(declare-fun v_92$$2 () (_ BitVec 32))
(declare-fun v_116$$2 () Float32)
(assert (= v_92$$2 v_12$$1))
(assert (= v_116$$2 ((_ to_fp_unsigned 8 24) RNE v_92$$2)))
(check-sat)