In general, these conversions are non-trivial, e.g., when converting from 64-bit down to 32-bit some precision may be lost. This is why the conversion functions take a rounding mode. The SMT standard for floating-point numbers does contain conversion functions of the following type:
; from another floating point sort
((_ to_fp eb sb) RoundingMode (_ FloatingPoint m n) (_ FloatingPoint eb sb))
So, the correct way to convert between floating-point numbers is to use the to_fp function. [Previously, the asFloat function served this purpose as well; I don't get an error using the latest unstable version of Z3 when using it.] A full example would be this:
(set-logic QF_FPA)
(set-option :produce-models true)
(declare-fun x_64 () (_ FP 11 53))
(declare-fun x_32 () (_ FP 8 24))
(assert (== ((_ to_fp 11 53) roundNearestTiesToEven x_32) x_64))
(check-sat)
which Z3 (latest unstable) accepts without errors and solves instantly. Alternatively, we could also think of casting x_64
down to 32 bit, in which case the assertion would look like this:
(assert (== ((_ to_fp 8 24) roundNearestTiesToEven x_64) x_32))