ID0002100: **This issue was created automatically from Mantis Issue 2100. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002100 | Frama-C | Plug-in > wp | public | 2015-03-31 | 2019-10-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jens | **Assigned To** | correnson | **Resolution** | won't fix | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - | ### Description : Consider the following ACSL lemma: /*@ lemma X : \forall integer a, b; (a+b)*(a-b) == a*a - b*b; */ which is automatically discharged by alt-ergo. When I open the proof obligation in Coq, the lemma looks like follows: Goal forall (i_1 i : Z), (((i_1 * i_1) = ((i * i) + ((i + i_1) * (i_1 - i))))%Z)%Z. Under Neon the proof coq representation preserves the original names much better Goal forall (a_0 b_0 : Z), (((a_0 * a_0) = ((b_0 * b_0) + ((a_0 + b_0) * (a_0 - b_0))))%Z)%Z. The problem gets worse with more parameters. ### Steps To Reproduce : frama-c-gui -wp lemma.c ## Attachments - [lemma.c](/uploads/61fcccb55ed44434e03f68ed4e4963af/lemma.c)