Encoding the pigeonhole principle in CBMC
If I understand correctly, you're actually looking for a technique to check if an out-of-bounds condition exists (more pigeons than pigeonholes).

Here's some example code that fits your analogy. I think you're asking about this technique as an analogy to whatever problem you're actually trying to encode, but next time be direct with what problem you want to solve rather than an analogy :)

/* pigeonhole.c */
int main() {
  _Bool holes_occupied[3];
  unsigned int pigeon;
  for (pigeon = 0; pigeon &lt; 4; ++pigeon) {
    holes_occupied[pigeon] = 1;
  }
  return 0;
}


Run with:

cbmc --bounds-check pigeonhole.c

VERIFICATION FAILED (with error trace)