Counterexample-guided abstraction reﬁnement (CEGAR) is a powerful technique to scale automatic program analysis techniques to large programs. However, so far it has been used primarily for model checking in the context of predicate abstraction. We formalize CEGAR for general powerset domains. If a spurious abstract counterexample needs to be removed through abstraction reﬁnement, there are often several choices, such as which program location(s) to reﬁne, which abstract domain(s) to use at diﬀerent locations, and which abstract values to compute. We deﬁne several plausible preference orderings on abstraction reﬁnements, such as reﬁning as “late” as possible and as “coarse” as possible. We present generic algorithms for ﬁnding reﬁnements that are optimal with respect to the diﬀerent preference orderings. We also compare the diﬀerent orderings with respect to desirable properties, including the property if locally optimal reﬁnements compose to a global optimum. Finally, we point out some diﬃculties with CEGAR for nonpowerset domains.