fix: consider functions with assertions/assumptions/errors impure

I had some doubts as to the semantics of this when I omitted these constructs to
begin with, but it was confirmed by GCC ≥ 4.7 leveraging this to make
model-breaking optimisations. We now conservatively consider any property
statement or error statement to be an indicator of impurity.