--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on July 2017 ---
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