Invalid Postcondition for Bytecode.Gas

[DavePearce]

The postcondition is written as:

    function method Gas(st: State): (st': State)
    requires st.IsExecuting() 
    ensures st'.OK? || st' == INVALID(STACK_OVERFLOW) 
    ensures st'.OK? <==> st.Capacity() >= 1 && st.Gas() <= (MAX_U256 as nat)

The part st.Gas() <= (MAX_U256 as nat) is invalid. The problem is that its constraining the permitted values for st.