next up previous
Next: References Up: 5 Presburger Arithmetic with Previous: 5 Presburger Arithmetic with

5.1 Current limitations

The transitive closure operation will not work on a relation with uninterpreted function symbols of arity > 0. Any operation that requires the projection of input or output variables (such as composition) may return inexact results if variables in the argument list of a function symbol are projected.