object PackUnpack {
  case class Message(id: Byte, payload: Int)
  type Bits = Long

  def decode(b: Bits): Message = {
    Message(((b >> 32) & 0xFF).toByte, (b & 0xFFFFFFFF).toInt)
  }

  /*
  def encode1(m: Message): Bits = {
    (m.id.toLong << 32) | m.payload.toLong
  }.ensuring(result => decode(result) == m)
  */

  def encode2(m: Message): Bits = {
    ((m.id.toLong & 0xFFL) << 32) | (m.payload.toLong & 0xFFFFFFFFL)
  }.ensuring(result => decode(result) == m)

  // --solvers=smt-z3 --strict-arithmetic=false --debug=smt 
  // check smt-sessions/ 
}