(declare-const x (_ FloatingPoint 1 2))