\false provable from recursive logic definition
ID0002338: This issue was created automatically from Mantis Issue 2338. Further discussion may take place here.
|ID0002338||Frama-C||Plug-in > wp||public||2017-12-18||2020-02-17|
|Platform||Sulfur-20171101||OS||Ubuntu 17.04||OS Version||-|
|Product Version||-||Target Version||-||Fixed in Version||Frama-C 20-Calcium|
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.