Question regarding CBMC

[A-Mehdi]

For the following code, if I run cbmc --unwind 100 test.c, cbmc will unwind the recursion 100 times. But from the code, it can be seen that recursion will only happen for 8 times (because of __CPROVER_assume). So what does it mean, when cbmc outputs Unwinding recursion recursive iteration 100?

#include <stdio.h>
#include <assert.h>

void recursive(unsigned n){
    if (n < 8){
        recursive(n + 1);
    }
    else {
        return;
    }
}

int main() {
    unsigned a = non_det();
    __CPROVER_assume(a > 0 && a < 2);
    recursive(a);
    assert(1);
}

[moonzoo]

Sorry that I missed this question.
CBMC unwinds a loop or a recursive function following a user's command (i.e., --unwind N), regardless of that many unwindings is necessary or not.
Note that unwinding a loop/a recursive function too many times does NOT change the behavior of target code because of a loop condition/a termination condition of a recursive function (see the page 17 of Oct 11's lecture slides).