### Error messages for the Upper Bound Checker
array.access.unsafe.high=Potentially unsafe array access: the index could be larger than the array's bound%nfound   : %s%nrequired: @IndexFor("%s") or @LTLengthOf("%s") -- an integer less than %s's length
array.access.unsafe.high.constant=Potentially unsafe array access: the constant index %s could be larger than the array's bound%nfound   : %s%nrequired: @MinLen(%s) -- an array guaranteed to have at least %s elements
array.access.unsafe.high.range=Potentially unsafe array access: the index could be larger than the array's bound%nindex type found: %s%narray type found: %s%nrequired        : index of type @IndexFor("%s") or @LTLengthOf("%s"), or array of type @MinLen(%s)
different.length.sequences.offsets=If offsets are provided, the annotation must contain the same number of sequences and offsets, but this annotation has %s sequence(s) and %s offset(s).
to.not.ltel=While attempting to validate a subsequence type, the Upper Bound Checker could not prove that %s is less than or equal to the length of %s.%nfound   : %s%nrequired: @IndexOrHigh("%s") or @LTEqLengthOf("%s") -- an integer less than or equal to %s's length
which.subsequence=The Index Checker cannot prove that %s is a subsequence. The Index Checker did prove that %s is non-negative, that %s is less than or equal to %s, and that %s is less than or equal to the length of %s. You should manually verify that %s is actually the name of the subsequence that the Index Checker verified, and then suppress this warning.
not.final=The Index Checker cannot prove that the expression %s is effectively final, but it is used in a HasSubsequence expression.