Temporal Properties

The invariant X is not a state predicate (one with no primes or temporal operators).

This can occur when you added a temporal formula as an invariant to your model. To fix this remove the formula from the invariants and add it as a property.