On 10/11/2012 10:23 AM, Jonathan M Davis wrote: > but there _are_ cases > where you can't have an invariant because of it. Except that you could write the invariant to be inclusive of the .init state.