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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 110, Issue 6



Hello jens,

When some goals are not discharged, the generated smt2 files can be 
found in the tmp folder. I do not know how to always keep them.

Regards,

Allan



Le 09/08/2017 à 18:23, Gerlach, Jens a écrit :
> Hello Yannick and Johannes.
>
> Thank you for your pointers.
> I am not sure what you mean by “smt2 files”.
> When I run Frama-C/WP I do not obtain files with an “.smt2” extension.
>
> As far as I understand the proof obligations are contained in files that end in “.why”.
> Do you think that they might be sufficient for the cvc4 people?
>
> Regards
>
> Jens
>   
>      ----------------------------------------------------------------------
>      
>      As a complement to Yannick's answer, the cvc4 team likes benchmarks, so
>      you could collect the VCs (smt2 files) that proved with 1.4 but don't with
>      1.5, and send the result to above list.
>      
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss