--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] z3 failure



    "This is surprising since Z3 is a very powerful prover"

I do believe Z3 is very powerful, however I have a lot of examples of
VCs not discharged by Z3 but discharged by other ATPs. (See
http://toccata.lri.fr/gallery/index.en.html)

It is surely possible that the way VCs are translated to Z3 by Why3 is
not perfect. I copy the mail to the Why3 list in case one wants to
investigate.

- claude

Le 06/10/2013 23:06, Stephen Siegel a ?crit :
> I have a very simple example (below) which I want to verify with frama-c + Jessie.  The VCs are discharged easily by Alt-Ergo, CVC3, and CVC4.  However they are not discharged by Z3.  This is surprising since Z3 is a very powerful prover.   I'm wondering if anyone has any idea what is going on, or how to look into it.
> 
> I am using Z3 4.3.1.  There are two VCs.  One, "copy_safety" is discharged by Z3 very quickly.  The other, "copy_ensures_default" runs forever. I've moved the timeout to 60 seconds, and it still times out.
> 
> BTW, this warning appears with both VCs:
> 
> WARNING: '=' cannot be used in patterns
> 
> Here is the program copy.c:
> 
> /*@
>   @ requires n>=0 && \valid(a+(0..n-1)) && \valid(b+(0..n-1)) ;
>   @ ensures \forall integer i ; 0 <= i < n ==> a[i] == b[i] ;
>   @ assigns b[0..n-1] ; 
>   @*/
> void copy(int n, double a[], double b[]) {
>   int i = 0;
> 
>   /*@
>     @ loop invariant 0<=i<=n;
>     @ loop invariant \forall integer j ; 0<=j<i ==> b[j] == a[j] ;
>     @ loop variant n - i ;
>     @*/
>   while (i < n) {
>     b[i] = a[i];
>     i++;
>   }
> }
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |