Reverting to old (stronger) definition of atomicity
In Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: e is atomic if for any e' such that e reduces to e' we have that e' is stuck.
The old definition was: e is atomic if for any e' such that e reduces to e' we have that e' is a value.
These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike WP do not guarantee safety, e.g., IC (if convergent predicates).