Model getModel() { final result = _c._z3.optimize_get_model(_optimize); return _c._getModel(result); }