ID0002169: **This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002169 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : Running "frama-c -wp 483.c -wp-out wp-out" on the attached file generates an Alt-Ergo obligation file "foo_assert_Alt-Ergo.mlw" which contains neither the lemma "xxx" nor the proof goal for the assertion in line 5. Apparently, Frama-C/Wp tacitly crashes during translating the lemma. The problem disappears ifin line 2 "int" is changed to "integer", or "\false" is changed to some formula containing "x". ## Attachments - [483.c](/uploads/b7743ec7ca8f15e3df9b2238386f8533/483.c)