1. Normalization

From PIPS execution on SPEC95's applu.f program, with computation of transformers, preconditions and regions, we observed constraint systems of very large sizes. For example, the printed out constraint system number $23499$ which was passed to $C^3$ normalization operator, takes $52,4$ MB of disk space, with only $7$ dimensions, no equation but a whooping $906530$ inequalities. 6_fig:example_normalization_large_constraint_system is the first fragment of the system.

Figure 4: Example: first fragment of a large constraint system which fails the normalization operator

We remark that the coefficients of this constraint system are quite large in the million to the billion range. Linear combinations such as Fourier-Motzkin elimination are likely to raise integer overflows with a 64-bit representation. When this system is passed to other operators, it raises exceptions, thus block our analyses. The origin of the system is identified as follows: from constraint systems of some hundred of constraints, operations on those systems such as projection, normalization, convex hull, etc sometimes yield up to constraint systems of thousand of constraints, mostly inequalities.

Moreover, when the satisfiability test cannot handle those constraint systems, we cannot remove redundant constraints, thus those systems remain very large and increase from operation to operation and we cannot obtain useful information.