Consider the following code:
_(ensures x == \old(x))
This code verifies... but should not? Shouldn't x be able to obtain any value during the execution of foo?
It might be that the post-condition won't be able to be used to infer other properties, and thus, this will not really lead to any issues. Nonetheless, it doesn't seem correct to me.