--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on August 2017 ---
Hi Jens, 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" Nothing to do with your question, but notice that Alt-Ergo can be used directly (-wp-prover alt-ergo) or through why3 (-wp-prover why3:alt-ergo). The POs given to Alt-Ergo are not the same. The best way to keep the temporary files sent to the provers is to use the option: -wp-out <dir>. Hope it helps, Patrick.