--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on August 2017 ---
-- "Gerlach, Jens" (2017-08-09) > Hello Yannick and Johannes. > > Thank you for your pointers. > I am not sure what you mean by âsmt2 filesâ. These are the input files for CVC4, in SMT-LIB2 syntax. > When I run Frama-C/WP I do not obtain files with an â.smt2â extension. The extension does not matter. In SPARK, we generate files with an extension .smt2 for CVC4, since we're using the SMT-LIB2 syntax for these. But maybe Frama-C/WP uses another extension. Or maybe you don't get the intermediate file in SMT-LIB2 syntax unless you use an option to keep intermediate files? > 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? CVC4 people will need files in SMT-LIB2 syntax, not files in Why3 syntax. -- Yannick Moy, Senior Software Engineer, AdaCore -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170809/48684137/attachment.html>