Frama-C Bug Tracking System - Frama-C
View Issue Details
0002011Frama-CPlug-in > wppublic2014-12-02 12:132014-12-02 12:13
jzinzind 
correnson 
highmajoralways
assignedopen 
LinuxUbuntu14.04
Frama-C Neon-20140301 
 
0002011: Unsoundness bug using native alt-ergo and Why3 due to reordering of lemmas
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.
Have SMT solvers imported from why3 0.83, Frama C Neon and the WP plugin
No tags attached.
Issue History
2014-12-02 12:13jzinzindNew Issue
2014-12-02 12:13jzinzindStatusnew => assigned
2014-12-02 12:13jzinzindAssigned To => correnson

There are no notes attached to this issue.