ID0002330: **This issue was created automatically from Mantis Issue 2330. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002330 | Frama-C | Plug-in > wp | public | 2017-10-26 | 2020-02-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | Phosphorus-20170501 | **OS** | - | **OS Version** | xubuntu 17.04 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium | ### Description : Running "frama-c -wp foo.c -wp-out wp-out -wp-prop=D" on the attached program fails to prove the property D, although it follows immediately from A and C. A look at the generated file "foo_assert_D_Alt-Ergo.mlw" reveals that the condition "y<=15" from C is not given to Alt-Ergo, while "0<=y" is. If the former is inserted into the mlw file, Alt-Ergo proves the goal without problems. Probably, "y<=15" is considered a trivial consequence of "y==(x&0xf)" by Qed; however, it shouldn't, since (e.g.) Alt-Ergo is unable to to infer this: goal C cannot be proven by Alt-Ergo. ### Steps To Reproduce : Name translation c -> mlw for convenience: x -> i y -> x z -> x_1 ## Attachments - [foo.c](/uploads/2114c61520580b96d2b67fca503e569d/foo.c)