mk
open fun <T : KFpSort> mkBvToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KBvSort>, signed: Boolean): KExpr<T>
Create Fp from BitVec value. Rounding is performed according to the roundingMode.
See also
for IEEE binary conversion.