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