Context Navigation

quantifierSARLBug.cvl@ cb4d4f4

main test-branch

Last change on this file since cb4d4f4 was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c

File size: 441 bytes

Rev	Line
[cabd216]	1	int main() {
	2	int N;
	3	int M;
	4
	5	$havoc(&M);
	6	$havoc(&N);
	7	$assume(N > 0 && M > 0);
	8
	9	int (*a)[M+2];
	10	int (*b)[M+2];
	11	int i, j;
	12	int c[N+2][M+2];
	13	int d[N+2][M+2];
	14
	15	a = c;
	16	b = d;
	17	$havoc(&i);
	18	$havoc(&j);
	19	$assume(1 <= i && i <= N+1 && ($forall (int t : 1 .. i-1) $forall (int x : 1 .. M)
	20	b[t][x] == 0 ));
	21	$assume(i < N+1);
	22	i++;
	23	$assert(($forall (int t : 1 .. i-1) $forall (int x : 1 .. M)
	24	b[t][x] == 0));
	25	}

Note: See TracBrowser for help on using the repository browser.