--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on May 2010 ---
Hello, > I'm very surprised that you could prove your post-condition with HAVOC. For > me you need a smart loop invariant for the inner loop to prove it I have been wondering about this too ever since the original question. Does HAVOC aim at being correct? Is it stated somewhere that the program is correct when HAVOC remains silent? Pascal