--- layout: fc_discuss_archives title: Message 75 from Frama-C-discuss on November 2013 ---
On 11/08/2013 08:11 AM, Xiao-lei Cui wrote: > Another question arises when I use why3 is that there seems no source > code(ACSL and C) tracing from given proof obligations. You should see the positions of the PO in the lower right part of Why3ide window. If you don't, then there is a problem: look at the standard error if there are some problems reported.