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