This paper presents a systematic method of building a more precise static analysis from a given one. The key idea is to lift
an abstract domain to the finite sets of its labeled abstract properties. The labels are designed to gather information about
the history of control flow and to obtain a finite partitioning of the program execution traces. The abstract operations of
the lifted domain are derived from those of the original one. This is a particular instance of the reduced cardinal power
introduced by P. and R. Cousot, where the base is the set of labels approximating the control history and the exponent is
an abstract domain. The method is applied to the domain of convex polyhedra and to the domain of linear congruences.
Key words abstract interpretation - reduced cardinal power - trace semantics