List<Expr> getUnsatCore() { final result = _c._z3.optimize_get_unsat_core(_optimize); return _c._unpackAstVector(result).cast(); }