This will not succeed when smtFloatMode is FloatUninterpreted, as Clang will turn input /= 30.0 below into a more complicated expression that also checks if 30.0 is NaN or not. This is logically equivalent to the original specification, but an SMT solver cannot conclude this when all of the floating-point operations involved are treated as uninterpreted functions.

To make this work, we set smtFloatMode to FloatIEEE instead. This works because all of the floating-point operations in the specification below are native to SMT-LIB.