Method mkBFloat

smt/expr.cpp:238–240

}

expr expr::mkBFloat(float n) {
  return Z3_mk_fpa_numeral_float(ctx(), n, mk_bfloat_sort());
}

expr expr::mkFloat(float n) {
  return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_single(ctx()));