Re: Logic Error

From: Markus Meyer <markus.meyer ***AT***student.tugraz.at>
Date: Tue, 22 Nov 2016 17:57:31 +0100
Subject: Re: Logic Error
Newsgroups: tu-graz.lv.vt
Organization: Technische Universitaet Graz
Message-id: <o11tdr$mpo$1@news.tugraz.at>
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0
References: <o0vb5e$3c4$1@news.tugraz.at>
On 2016-11-21 18:33, Franco Nieddu wrote:
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)

I got stuck with the same problem, and I found out that the following works:
1: @assert (forall i in (0, index): array[i] <= max) && (index >=length) && (length >= 0)
2: @assert (forall i in (0, length): array[i] <= max)

I'm sure that you can easily extend your line 1 with this statement ;)