copysign is not modeled

[keram88]

We do not currently handle the copysign family of functions. This is due to a limitation of SMT-LIB where NaN has a singular representation, whereas C allows numerous representations for NaN including both signed and unsigned.

For example, copysign(1.0, NAN) could yield -1.0 or 1.0, but with a unique value for NaN, it is impossible to distinguish between these cases.