Logic Error

From: Franco Nieddu <franco.nieddu ***AT***student.tugraz.at>
Date: Mon, 21 Nov 2016 18:33:34 +0100
Subject: Logic Error
Newsgroups: tu-graz.lv.vt
Organization: Technische Universitaet Graz
Message-id: <o0vb5e$3c4$1@news.tugraz.at>
User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.11; rv:45.0) Gecko/20100101 Thunderbird/45.4.0
Hi all!

I have a problem regarding the following 2 lines:

1: @assert (forall i in (0, index): array[i] <= max) && (index >=length)
2: @assert (forall i in (0, length): array[i] <= max)

In my opinion, the first line should imply the second line thus making it stronger (because max has to be larger than at least as many values as in line 2), but the tool always prints a "strengthening error".

Maybe I got a tunnel view on this but I am pretty stuck right now...

Thanks in advance!