Skip to content

Commit 2c8901f

Browse files
added test from lin2vareq to affeq that found mistake in dim_add
1 parent 92802e5 commit 2c8901f

File tree

1 file changed

+21
-0
lines changed

1 file changed

+21
-0
lines changed
Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none
2+
// This test was added from 77-lin2vareq because it found mistakes in dim_add that weren't detected by the other tests
3+
#include <goblint.h>
4+
5+
int check_equal(int x, int y, int z) {
6+
__goblint_check(x == y);
7+
__goblint_check(z == y);
8+
__goblint_check(x == z);
9+
return 8;
10+
}
11+
12+
int main(void) {
13+
int x, y, z;
14+
15+
y = x;
16+
z = y;
17+
18+
check_equal(x, y, z);
19+
20+
return 0;
21+
}

0 commit comments

Comments
 (0)