How to add the free loop invariant into 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.

[shazqadeer]

@zvonimir : This is really a SMACK question and should have been posted on the SMACK (if it has one). But please provide some answer here to help out @Luweicai .