Predicate ArrayIndexOutOfBounds::bestArrayAccessBound

Holds if the index expression is less than or equal to the array length plus k, but not necessarily less than or equal to the array length plus k-1.

predicate bestArrayAccessBound(ArrayAccess aa, int k)