The following code is verified in VCC although the assertion clearly does not hold.
static int s=0;
Verification of main succeeded. [1.19]
Verification of stat succeeded. [0.00]
Seemingly, VCC treats variable s as a non-static local variable instead of a static local variable.
Does anyone have an idea why this is the case? Is this issue simply a bug or does it extend to a conceptual flaw?