List<Expr> getAssertions() { final vec = _c._z3.optimize_get_assertions(_optimize); return _c._unpackAstVector(vec).cast(); }