--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on December 2013 ---
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