decreases clause does not support impure specs

[gebner]

fn rec foo (x: ref nat)
  preserves live x
  decreases !x
{
  if (!x > 0) {
    x := (!x) - 1;
    foo x;
  }
}