## 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).