--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on June 2011 ---
> But in the file "max_element2.c", in Line 47, > I replace "loop invariant !(\exists integer k; 0 <= k < i && (a[max] < > a[k]));" > with "loop invariant IsMaximum(a, i, max);" which are the same. > But in this case, Frama-C can not prove. It's only a bug in Frama-C if Frama-C generates an obligation that is not provable. Did you look at the generated obligation? It often happens that adding a layer of definition prevents automatic provers to conclude on a property that was provable when it was simple. Which automatic prover(s) did you use? Pascal