Method mkQVar

smt/expr.cpp:297–300

}

expr expr::mkQVar(unsigned n, const expr &type) {
  C2(type);
  return Z3_mk_bound(ctx(), n, type.sort());
}

expr expr::mkQVar(unsigned n, unsigned bits) {
  return Z3_mk_bound(ctx(), n, mkBVSort(bits));