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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002237 | Frama-C | Plug-in > wp | public | 2016-06-30 | 2016-12-05 |
| Reporter | Jochen | Assigned To | correnson | Resolution | fixed |
| Priority | high | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | xubuntu |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | - |
Description :
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".