How is BoogiePL translated into verification condition in Source code ?

Jan 22, 2013 at 3:06 PM

Hello Everyone,

I  am just wondering how is the BoogiePL translated into verification condition in the source code ? I checked the source code but did not find it, can anyone points it out ?

Thank you