What is the form of free loop invariant in the smack generated boogie code(from c)?

[Luweicai]

The loop invariant invariant xxx will be transferred into the form of assert XXX in the smack-generated boogie code (from c code). I wonder the form of free loop invariant free invariant XXX in the smack-generated boogie code.

[zvonimir]

Hi. Sorry, I did not keep an eye on the questions here. This is a new feature to me :).
Let me look into this a little bit.