Definition of SumHeap is not emitted if last method has no gotos

[bobismijnnaam]

Adds a test and an optimistic fix for #422. Please let us know if additional work is needed!

[gauravpartha]

Looks good to me, thanks a lot for the fix!

For documentation purposes:

The sum of heap axioms should be emitted if the loop detector is used at least for one method to identify loops (which is the case when the program has gotos). The problem was that there was only a single boolean flag used to query whether this was the case, but this boolean flag was reset every time a new method was analyzed. @bobismijnnaam introduced another boolean flag that is true if the loop detector was used once for at least one method.

[gauravpartha]

I removed sumheap_bug.vpr in #424 and instead added it in the Silver repo (see viperproject/silver#591) in the corresponding Carbon issues folder. We usually add all our regression tests for the CI in the Silver repo (the ones in the Carbon repo are currently not taken into account when running the CI).

One way to make sure that one does not need to merge a Carbon PR first before adding the tests in the Silver repo is to create a Silver PR with the added tests without merging the Carbon PR. Then, one changes the Silver submodule in the Carbon PR to point to the Silver PR, which will make the Carbon CI take into account the added tests.

If the CI succeeds, one can merge the Carbon PR and after that the Silver PR (if one merges the Silver PR first, then the Silver PR will change Carbon master to point to the merged Silver commit, which might lead to the Carbon master CI to fail).