CORE
main.c
--apply-loop-contracts
^EXIT=10$
^SIGNAL=0$
^\[main.\d+\] .* Check loop invariant before entry: UNKNOWN$
^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$
^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
^\[main.\d+\] .* Check that loop invariant is preserved: UNKNOWN$
^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
^VERIFICATION FAILED$
--
--
This test (taken from #6021) shows the need for assigns clauses on loops.
The alias analysis in this case returns `unknown`,
and so we must manually annotate an assigns clause on the loop.

Note that the annotated assigns clause in this case is an underapproximation,
per the current semantics of the assigns clause -- it must model ALL memory
being assigned to by the loop, not just a single symbolic iteration.