False negative with k-Induction and incremental BMC

[lu-w]

Hey all,

while working with 2LS I noticed a possible bug. It basically boils down to the following program being reported as safe:

extern void __VERIFIER_error();
int main() {
	for (int i = 0; i < 1; i++) {
		for (int j = 0; j < 2; j++) {}
		__VERIFIER_error();
	}
	return 0;
}

When using --k-induction or --incremental-bmc, 2LS claims

[main.assertion.1] : OK

** 0 of 1 unknown
** 0 of 1 failed
VERIFICATION SUCCESSFUL

In both cases, it reports to have generated a proof after 2 unwindings, although this program should be proven unsafe.