Method mkFloat

smt/expr.cpp:225–228

}

expr expr::mkFloat(double n, const expr &type) {
  C2(type);
  return Z3_mk_fpa_numeral_double(ctx(), n, type.sort());
}

expr expr::mkHalf(float n) {
  return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx()));