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.