ID0002226: **This issue was created automatically from Mantis Issue 2226. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002226 | Frama-C | Kernel | public | 2016-05-02 | 2016-05-04 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | Sodium-20150201 | **OS** | xubuntu14.04 | **OS Version** | - | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : Running "frama-c -wp p1on.c" on the attached program proves both the statement contract in line 9 and the trivial assertion in line 11, as expected. However, if line 11 is commented out, Alt-Ergo immediately reports "unknown" on line 9. (Cvc4 runs into its timeout then.) The file "foo_stmt_post_Alt-Ergo.mlw" contains the goal "goal foo_stmt_post: false" for some reason. It seems that the statement contract is translated in a wrong way, unless the final trivla assertion is present in line 11. ## Attachments - [p1on.c](/uploads/9351b0cad4fd440f1a5283a7287fdf93/p1on.c)