See the doc:
What if the number of unwindings specified is too small? In this case, bugs that require paths that are deeper may be missed. In order to address this problem, CBMC can optionally insert checks that the given unwinding bound is actually sufficiently large. These checks are called unwinding assertions, and are enabled with the option
--unwinding-assertions. Continuing the generic example above, this unwinding assertion for a bound of five corresponds to checking the following loop-free program:
