(define-fun float__first () Float32 ((_ to_fp 0 24) #xFF7FFFFF))