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