infinity in FlatZinc
Although constraints with infinity values can often be rewritten into other constraints (such as the examples in #661), there is nothing preventing infinity from being used as arguments for solver built-in predicates. This is problematic because infinity (and -infinity) are not part of the FlatZinc specification, and are not supported by many FlatZinc parsers.
The first consideration is whether to add infinity to the FlatZinc specification. This would be a slow change, but might be required for correctness.
However, the use-cases where the infinity value should appear in the FlatZinc seem very limited and we have not yet seen any model that would require this. We can also consider making it an error when infinity appears in the FlatZinc. Even if this is allowed, we should consider whether a warning should be given to the modeller.