Then you missed the point that CBMC is a formal verification tool (the best practical one btw), which also does bounded model checking. But it has of course its limitations, esp. with unbounded models, such as linked lists or recursion.
Here he explains how to overcome its limitations in one case. A likely bug in the loop unroller. With --unwind N you can tell CBMC how far to unroll automatically, and --depth is for recursion. In this case he just unrolled it manually.
Note: should check if it works out of the box with a current version. CBMC is getting better and better lately.
I often use satabs then, which doesn't struggle with unbounded models, but has other limitations.