mk
open fun <T : KFpSort> mkFpToBvExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, bvSize: Int, isSigned: Boolean): KExpr<KBvSort>
Create Fp to BitVec conversion (fp.to_sbv, fp.to_ubv) expression. Provided Fp value is rounded to the nearest integral according to the roundingMode.
See also
for binary conversion.