Model toContext(Context c) { final ptr = _c._z3.model_translate(_model, c._context); return c._getModel(ptr); }