Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas
ID0002011: This issue was created automatically from Mantis Issue 2011. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002011 | Frama-C | Plug-in > wp | public | 2014-12-02 | 2014-12-02 |
| Reporter | jzinzind | Assigned To | correnson | Resolution | open |
| Priority | high | Severity | major | Reproducibility | always |
| Platform | Linux | OS | Ubuntu | OS Version | 14.04 |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
One can prove the following : /*@ axiomatic Bla{ predicate Pred(integer x); lemma lemme1: \forall integer x; Pred(x) ; lemma lemme2: \forall integer x; Pred(x) ; } */ using native alt-ergo and an SMT solver from the Why3 plateform. Native alt-ergo and the why3 based SMT solver do not parse the lemmas in the same order. So one can prove lemma2 assuming lemma1, the other can prove lemma1 because it assumes lemma2, and evenntually the whole axiomatic is proven. This is very problematic and confusing whenever several different SMT solvers are used.
Steps To Reproduce :
Have SMT solvers imported from why3 0.83, Frama C Neon and the WP plugin