Solver toContext(Context c) { final ptr = _c._z3.solver_translate(_solver, c._context); return c._getSolver(ptr); }