Exploiting state encoding for invariant generation in induction-based property checking