ID0001588: **This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001588 | Frama-C | Plug-in > wp | public | 2013-12-20 | 2014-03-13 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 | ### Description : 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 ## Attachments - [wp.c](/uploads/f296e3e3d81e278bf5e25179c5d16e29/wp.c)