ID0002454: **This issue was created automatically from Mantis Issue 2454. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002454 | Frama-C | Plug-in > wp | public | 2019-06-17 | 2019-06-19 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jwaksbaum | **Assigned To** | correnson | **Resolution** | no change required | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | i386 | **OS** | Darwin | **OS Version** | 18.6.0 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : Why3 errors on the generated goals produce by w3 on certain inputs with the following message: Ambiguous path: both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why ### Steps To Reproduce : Why3 errors on the generated goals produce by w3 on certain inputs with the following message: Ambiguous path: both /nix/store/nf4sbv0j6dc0grks7iplf9byv989mjg5-why3-0.88.3/share/why3/modules/Matrix.mlw and /var/folders/2j/dbl_p0mj3rgd879z8nt7r4600000gp/T/wpdeac45.dir/typed/Matrix.why ## Attachments - [example.c](/uploads/ba254a88318716a5e0665ff9fe46d1f4/example.c)