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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 109, Issue 4



Hello,

to answer Jochen’s question that he accidentally posted to the mailing list (and therefore in German.)

>    CVC3 nur fuer diejenigen Faelle aufgerufen, in denen Alt-Ergo keinen 
>   Beweis gefunden hat?

No,  all  provers received all prover obligations that Qed could not discharge.
That is the difference between the results in appendices A.2 and A3.
  
>    Und warum sind die Zahlen so klein? Allein push-heap muesste doch knapp 
>   100 Proof Obligations gehabt haben, und fuer das ganze "ACSL by Example" 
>    wuerde ich spontan ca. 1000 erwarten - ? Kann der Qed ca. 900 davon 
>    schon alleine loesen?

The numbers refer to algorithms not proof obligations!
I think you missed that point.

Jens