Investigate inference of loop invariants using `merge-nodes` functionality

Here https://github.com/runtimeverification/kontrol/pull/444, we update the merge-nodes functionality to allow specifying loop heads in looping code. Here, we have an example that uses a loop invariant to allow verifying a small piece of code with a simple loop: https://github.com/runtimeverification/kontrol/pull/369.

The merge-nodes functionality should help us in identifying the loop invariant needed in order to verify such simple loops. We probably can't infer the entire loop invariant, but at least we can make an initial guess ath the correct LHS of the loop to use.

Here, we should:

• Remove the loop invariant present here: https://github.com/runtimeverification/kontrol/pull/369/files#diff-a2ef7982f6abbbf7c35d297264226ea334b6dbd3830bc673bf68f2b62a755635R141.
• Run the program out to a certain number of iterations of the loop.
• Use the merge-nodes functionality on the loop heads to produce a new state taht is more general than teh loop heads.
• Compare the generated result with the LHS of the original invariant. Post the results here.
• Figure out how to automate more of the invariant generation.

Start with PR 369's loop-invariant example and the merge-nodes changes in PR 444. Remove the invariant from the example, run the program for a chosen number of iterations, apply merge-nodes to the loop heads, and compare the generated state with the original invariant's LHS. Done means posting the comparison results and outlining what can be automated for further invariant generation.