--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on June 2012 ---
> I tried your code with Frama-C Nitrogen + Jessie 2.30 + Why3 0.72 (just > with frama-c -jessie <file.c>) and I am able to prove every VCs using > Alt-Ergo/CVC3 and or /Z3. I attached the HTML report produced using > why3session. For Jessie, I just discovered that I can prove all VCs with Alt-Ergo + CVC3 if I use frama-c -jessie r_ges.c but not if I use frama-c -jessie -jessie-atp=gui. The latter fails with Alt-Ergo, CVC3, Simplify, Z3. I use Frama-C Nitrogen + Jessie 2.30 + Why3 0.72. WP with any of the above provers fails to verify the call precondition for r_ges = r_seq(r1,tmp). I haven't tried the latest WP plugin though. -- Best regards, Boris