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