- requires: : maxSet ((j @ test7.c:8:3 ) ) >= ( 0 )
-test7.c:6:3: Possible out-of-bounds store. Unable to resolve constraint:
- requires: : maxSet ((g @ test7.c:4:3 ) ) >= ( 4 )
+ requires maxSet(g @ test7.c:6:3) >= 2
+test7.c:8:3: Possible out-of-bounds store: j[0]
+ Unable to resolve constraint:
+ requires maxSet(j @ test7.c:8:3) >= 0