--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on October 2013 ---
"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 |