--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on October 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP plugin report incorrect



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