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

Thanks for the detailed answers. The situation is much clearer now. Best, Delphine > On 8 Mar 2018, at 10:08, Claude Marché wrote: > > > By the way, I'd like to say that using provers to establish assertions > like these: > > Le 05/03/2018 à 11:43, Sandrine Blazy a

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