ID0002404: **This issue was created automatically from Mantis Issue 2404. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002404 | Frama-C | Plug-in > wp | public | 2018-10-08 | 2019-10-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | - | ### Description : WP allows to select properties by using the option -wp-prop. I have noticed the following: When selecting a property 'foo' by -wp-prop=foo, sometimes all VCs that belong to that property are verified. However, when I wish to verify all properties, some VC's of the property 'foo' are not verified. This might be caused by the fact that the the actual "shape" of a VC appears to depend on -wp-prop. (I attach an example of the slight differences between a VC that belongs to a certain property "foo" depending on whether -wp-prop=foo is used or not.) This of course defeats somehow the purpose of using -wp-prop and it would be a welcome feature if the generation of a VC of a property 'foo' is not affected by "-wp-prop=foo". ### Additional Information : Is this maybe a problem of Qed? Also, if there are several ways to generate/simplify a VC, it would be nice if one chooses one that has a higher likelihood to be verified. ## Attachments - [diff.txt](/uploads/14ff154d537bcec5e27f7f5946ba2bfd/diff.txt)