Holds if this expression is side-effect free (conservative approximation). This predicate cannot be overridden; override mayBeImpure() instead.
Note that this predicate does not strictly correspond with the usual definition of a ‘pure’ function because reading from global state is permitted, just not writing / output.
predicate isPure()