Debugger doesn't handle multiple tests for the same function

If there are multiple tests for a single function - in particular, when a non-recursive predicate is auto-unfolded - the debugger only selects the first relevant case, leading to an under-approximate verification *only* when debugging. This needs to be fixed.

I propose having the root node branch for each test.