1 2 3 4 5 6
; REQUIRES: symfpu ; EXPECT: sat (set-logic QF_FP) (declare-fun a () (_ FloatingPoint 53 11)) (assert (= a (_ +oo 53 11))) (check-sat)