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