added test whether loop invariant