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