\false provable from recursive logic definition
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.