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