Function postconditions are not checked

[siddharth-krishna]

This example passes:

pure function foo(x: Int) returns (y: Int)
  ensures y > x
{
  x - 2
}

Was there some reason why these checks are hard to do in general, or have we just not implemented the checks yet?

[wies]

For functions they are easy to implement, but for non-pure predicates it is a bit more involved. I was always hoping we could do it once and for all for both functions and predicates, but no one has risen to the occasion so far (including myself :-)

[siddharth-krishna]

Haha. It's not critical, I just thought we should have an issue to keep track of the fact that they're not checked.