--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on September 2017 ---
Le 23/08/2017 à 11:46, BAUDIN Patrick a écrit : > Le 23/08/2017 à 11:05, Gerlach, Jens a écrit : >> Is there a simple way to let Frama-C/WP generate proof obligations in âsmtlib2â format? >> When I use the â-wp-genâ option then only file of the form â*_Alt-Ergo.mlwâ and â*.ergoâ are generated. > WP can generate PO in coq, altergo (default) or why3 formats. > The translation into "smtlib2 format" should be done using why3 (as it > is done when using -wp-prover why3:cvc4). > May be you have to select a prover managed by why3 using the option > "-wp-prover why3:cvc4" in addition to "-wp-gen" Additionally you could use "-wp-why-opt \"-output foo\"" to ask why3 to produce the file in foo directory. But usually I just use the edit button of why3ide to look at the smt2 file. Best, -- François