WP ignores some goal
ID0001588: This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.
|Plug-in > wp
|have not tried
|Fixed in Version
On this example, WP ignore some of the goals. There should be 3 goals, but :
[wp] 1 goal scheduled [wp] [Qed] Goal typed_f_loop_inv_l1_2_established : Valid
Loop invariant preservation and assertion are ignore.
Additional Information :
I simplified the example as much as possible, but it seems that the number of statements is important to reproduce the problem 8-/
Steps To Reproduce :
frama-c wp.c -wp