Omitting the disjunct || max(a, b) == b makes the specification of max too strong. When it is called with the second argument larger than the first, the postconditions can not be satisfied by any state, since they imply, together with the assumption that b is larger than a:

max(a,b) == a < b <= max(a, b)

In other words, max(a, b) < max(a, b), which is equivalent to false. Since after a call the postconditions hold, false holds there and anything can be proven, including the doubted assert. This you can check by inserting

assert false;

after the second assert. It will verify.

The danger of bodyless functions and methods is that they introduce axioms that are considered to hold without further verification (that's the idea of axioms, right). If they contain a contradiction, this is carried over to whatever follows.