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