int invariant;