The counter examples produced by CBMC omit variables that are not relevant to reproduction of the problem. At first this could be confusing to the users.
In order to improve the situation, CBMC could have a mode that produces "special" assignments for these irrelevant variables (e.g. where the value is "variable not needed for counter example") and those could then be shown in the debugger.