Running China+PPL on our benchmark suite I observed the following phenomenon: when the constraints of polyhedra are printed I see, e.g., both B + C + D + E - F = -2, and -B - C - D - E + F = 2. These constraints are equivalent and are also normalized with our current notion of normalization. In fact, gcd(1,-1,-2) = gcd(-1,1,2) = 1. The question is: are we using too weak a notion of normalization? What happens if, for equalities, we insist having a non-negative inhomogeneous term? Notice that, in some places, we are rather syntactic when dealing with constraints. For instance, in Matrix::merge_rows_assign() we regard the above constraints as different and we get them both in the result. Any idea? Ciao, Roberto -- Roberto Bagnara Computer Science Group Department of Mathematics, University of Parma, Italy http://www.cs.unipr.it/~bagnara/ mailto:bagnara@cs.unipr.it