J. Berger: > This is more or less what Jonathan said in his last post. You are right, if the state isn't changed between two method calls, there's no point in calling the invariant two times after the method call and before the next method call. Bye, bearophile