Re: Logic Error

From: Anja Karl <akarl ***AT***>
Date: Mon, 21 Nov 2016 19:42:37 +0100
Subject: Re: Logic Error
Organization: Technische Universitaet Graz
Message-id: <o0vf6t$kv5$>
User-agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0
References: <o0vb5e$3c4$>
Am 21.11.2016 um 18:33 schrieb Franco Nieddu:
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!


that is really strange, since my version accepts this step :S
Could you maybe please compile with make z3debug and send me the output via Email?

Thank you!