CBMC is a Bounded Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot. It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions.
For the pigeon-hole principle I understand that the constraints are:
- Each Pigeon is in some Hole.
- Two different Pigeon can't be in same hole.
Let's take an example of 4 pigeons and 3 holes. I need to convert this into a CBMC check. I'm trying using two for loops, but I can't find how to do it.