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