--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2011 ---
Hi, Thank you for this example. It was actually a bug in the WP, related to the treatment of 'Here' in loop invariants. We also optimized the traduction of separation predicates, which results in your copy2.c is now entirely proved but the last assertion. Regards, L.