--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on May 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Code proved with Fluorine is more proved with Neon



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