--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on May 2014 ---
Claude March? <Claude.Marche at inria.fr> writes: > Le 27/05/2014 10:36, Christophe Garion a ?crit : >> z3 4.3.1 via why3 seems to prove all the assertions under Neon, so it >> may be an Alt-Ergo problem. > > External provers are not supposed to be equivalent, so this is non-sense > to say that there is a problem with a prover X if it does not prove > something that is proved by a prover Y. Yes, you are right of course, sorry for my mistake. I just wanted to precise that all the assertions can be proved, but not with Alt-Ergo as previously. Christophe -- Christophe Garion ISAE/DMIA - SUPAERO/IN garion at isae.fr 10 avenue Edouard Belin T?l : (33)5 61 33 80 57 BP 54032 Fax : (33)5 61 33 83 45 31055 Toulouse Cedex 4