pub open spec fn max3(x: int, y: int, z: int) -> int
{ if x < y { max(y, z) } else { max(x, z) } }
This function computes the maximum of three given integers.