Re: [Why3-club] proof of a test program

Le 05/03/2018 à 11:43, Sandrine Blazy a écrit : None of my provers (Alt-Ergo, cvc3, cvc4, Eprover, Z3) is able to prove any of these 3 assertions. However, if I choose the "get counter-example" option in the preference window, then cvc4 manages to prove this test program. Does it mean that

Re: [Why3-club] proof of a test program

Hi, I just tried to understand what's happening with this example: - I noticed that only CVC4 1.4 proves the example with "get   counter-example" option. Version 1.5 does not. - I used the bisect capability of Why3 to generate a smaller VC   that is proved with CVC4-1.4 + "get

[Why3-club] proof of a test program

Hi, I am using Why3 0.87.3 to prove the following test program of the selection sort given in the gallery of verified programs (http://toccata.lri.fr/gallery/selection_sort.en.html ). let test1 () = let a = make 3 0 in a[0] <- 7;