Skip to content

Commit 3c27e68

Browse files
committed
Congruences: Add testing for overflow in subtraction where result it too large.
1 parent 7a3d072 commit 3c27e68

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

tests/regression/37-congruence/17-sub-congruence.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,9 @@ int main(void)
2323

2424
__goblint_check(ov == INT_MAX); //UNKNOWN!
2525

26+
int ov2 = 0 - min;
27+
__goblint_check(ov2 == INT_MAX); //UNKNOWN!
28+
2629
return (0);
2730

2831
}

0 commit comments

Comments
 (0)