Method mkNumber

smt/expr.cpp:259–262

}

expr expr::mkNumber(const char *n, const expr &type) {
  C2(type);
  return Z3_mk_numeral(ctx(), n, type.sort());
}

expr expr::mkConst(Z3_decl decl) {
  return Z3_mk_app(ctx(), decl, 0, {});