Hello, > Is it maybe possible in some cases to look at how the induction > variable is used (e.g. as an array index and we know that it is > undefined to have an index outside the array domain), and decide > on whether the loop must be finite or not based on that? we do this on tree level. Zdenek