Method mkBFloatVar

smt/expr.cpp:325–327

}

expr expr::mkBFloatVar(const char *name) {
  return ::mkVar(name, mk_bfloat_sort());
}

expr expr::mkFloatVar(const char *name) {
  return ::mkVar(name, Z3_mk_fpa_sort_single(ctx()));