ID0002338: **This issue was created automatically from Mantis Issue 2338. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002338 | Frama-C | Plug-in > wp | public | 2017-12-18 | 2020-02-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | duplicate | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | Sulfur-20171101 | **OS** | Ubuntu 17.04 | **OS Version** | - | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium | ### Description : Running "frama-c -wp foo.c -wp-prover alt-ergo -wp-prover eprover" on the attached file proves all goals, including a lemma "Check" which just says "\false", from nothing but a recursive definition of a logic int function. The latter is well-founded since its only recursive call uses a parameter value n==0 which immediately employs the base case. The problem disappears (1) when "integer" is used as result type and as 3rd parameter type, (2) when "a[]" is omitted, (3) when lemma "Alpha" is renamed to a name lexicographically after "Check", or (4) when "cvc3" or "cvc4-15" is used instead of "eprover". The problem remains, however, when "z3" is used. ## Attachments - [foo.c](/uploads/340c077780845d501a0ff97285b34e30/foo.c) - [diff.txt](/uploads/2fe9c477a8a70ef0a92fbd1b0e09d964/diff.txt) - [eprover.input](/uploads/ad8ebe320b201413c34ff6998234e1e0/eprover.input)