Method check

smt/solver.cpp:281–284

  void reset_solver()  { goal.reset(); }

  void check() {
    if (tactic_verbose)
      goal = tactics.exec(goal).toGoal();
  }

  Z3_solver getSolver() const {
    return Z3_mk_solver_from_tactic(ctx(), tactics.t);