Frama-C is unsound when employing both alt-ergo and cvc4
ID0002237: This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.
|ID0002237||Frama-C||Plug-in > wp||public||2016-06-30||2016-12-05|
|Product Version||Frama-C Aluminium||Target Version||-||Fixed in Version||-|
Running "frama-c -wp -wp-out out -wp-prover alt-ergo -wp-prover cvc4 bug.c" on the attached file "bug.c" proves both lemmas, although they are both obviously false. A look at file "lemma_Two_Alt-Ergo.mlw" shows that Alt-ergo proved in fact One==>Two, while a look at file "Axiomatic.why" indicates that cvc4 proved in fact Two==>One.
Apparently, the order of lemmas is reversed when piping through "why" - the output generated for coq amounts to "prove One" and "prove One==>Two", similar to that for Alt-ergo.
The problem disappeared when the type of the bound variable "x" was changed to "integer".