How to use loop invariants inference

Feb 19, 2010 at 5:50 PM

Boogie supports the infer flag with a number of options to infer loop invariants. Unfortunatelly I could so far only come up with extremely simple examples where this functionality actually help to infer invariants. The only one i found so far was to set a variable to a constant in the loop.

Could someone provide a more complex example of boogie code where these infer flags actually help reducing manually specified invariants.

Thanks, Thorsten