Function mk_bfloat_sort

smt/expr.cpp:234–236

}

static Z3_sort mk_bfloat_sort() {
  return Z3_mk_fpa_sort(ctx(), 8, 8);
}

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