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

[Frama-c-discuss] Frama-C/WP and CVC4 (version 1.5)



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