--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [wp] invoke provers from command line



Hello,

Le 09/12/2013 06:22, Xiao-lei Cui a ?crit :
> [wp] Goal typed_max_post : trivial
> [wp] Goal typed_max_post_2 : trivial
> [wp] Goal typed_max_assert : trivial
> ------------------------------------------------------------------------------
> why3IDE did not show up.

My guess is that the VP are so easy that WP does not feed them to Why3. 
I'll let expert confirm this.

Try set-up an unprovable VC (e.g. "assert zz < 0;").

Best regards,
david