Method mkFreshVar

smt/expr.cpp:341–344

}

expr expr::mkFreshVar(const char *prefix, const expr &type) {
  C2(type);
  return Z3_mk_fresh_const(ctx(), prefix, type.sort());
}

expr expr::some(const expr &type) {
  return type.isBool() ? expr(false) : mkNumber("3", type);