--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on April 2014 ---
Hi Anne, thanks for the hint, it works exactly as you said: I can now prove all assertions with the exception of the initial one. Frank