Create a Solver that uses this tactic.
Solver toSolver() { return _c._getSolver(_c._z3.mk_solver_from_tactic(_tactic)); }