The following verifies:

void test() {
int x;
_(unchecked) x++;
}

According to the C standard, signed arithmetic overflow produces undefined behavior. I didn't find anything in MSDN to contradict this. So we should simply refuse to verify anything with a signed overflow (instead of producing an indeterminate value, which VCC does now).