add test for unwinding counter reset

[kroening]

No description provided.

[tautschnig]

Please provide a justification in the commit message. What is the added value of what has been added in a4945f3? Now that running regression tests is the primary cost of builds it would be desirable to get a rationale for added tests.

[kroening]

This certainly complements a4945f3. The new test catches the case that the reset of the counter of the inner loop is forgotten. None of the existing tests covers that case.

[tautschnig]

The new test catches the case that the reset of the counter of the inner loop is forgotten.

That was exactly the bug that was fixed in a4945f3 so I'm still not convinced. In my opinion the difference between the tests is just that one uses a user-level assertion while the other test relies on unwinding assertions. Before a4945f3 the unwinding assertion was placed prematurely, while in this test the unwinding assumption would be placed prematurely.

I think the following would serve as litmus test: does the newly proposed test fail before a4945f3? If it doesn't, then I'm obviously wrong. If it does, but also fails after a4945f3 (and is only fixed by some later change) then I'm also wrong. If it is a4945f3 that turns it from failure to success, then the remaining question is what different code paths it exercises.

[tautschnig]

For the record: I have gone back to eac8e2c, which is the merge commit before any of the commits in #988 (which a4945f3 is part of), and the newly proposed test does return VERIFICATION SUCCESSFUL, i.e., fails. Then resetting to 32b68ce (#988 merged) yields VERIFICATION FAILED, i.e., the test now succeeds.

[TGWDB]

Closing due to no response in block and PR being stale.

If you believe this is erroneous please reopen this PR.