--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on October 2015 ---
Hi David, > On 05 Oct 2015, at 18:02, David MENTRE <dmentre at linux-france.org> wrote: > > Le 05/10/2015 17:56, Christoph Rauch a écrit : >> If I completely remove the loop and thus the invariant, it doesnât verify. How can it possibly prove the loop invariant? > > Which prover are you using? I tried with Alt-Ergo and CVC3 and the loop invariant in not proved, for both your first code and the code not calling swap(). Using `-wp-invariantsâ, which seems to be the cause for the troubles, every prover I tried yields positive (i.e. wrong) results: Alt-Ergo, CVC4, and Z3. Best, Christoph