Simplify rules ignore side-effects

[superaxander]

The following program verifies erroneously:

class A {
    int a;
}

context Perm(a.a, write);
ensures a.a == \old(a.a) + 1;
ensures \result == a.a;
int incr(A a);

requires Perm(a.a, write);
void main(A a) {
    a.a = 0;
    int b = incr(a) - incr(a);
    assert b == 0;
    assert a.a == 0;
}

The rule i - i == 0 removes the two calls to incr. There are probably plenty more examples like this.