After some discussion at GobCon yesterday, we were able to come up with an example where locals "escape" to recursive calls.

• The program has one call to f(0,&t).
  • This call recursively calls f(5,&x) passing a reference to its local x (Let us call this variable x0 for convenience).
    • The call to f(5,&x) then sets its x (x5) to 31. The following *ptr has &x and this is understood to refer to x5, where x0 would be correct
    • After the nondeterministic branch ptr may point to x0 and x5
    • The assignment modifies one, meaning that the asserts should be unknown
    • The call returns, having potentially modified x of its caller (x0)
  • After f(5,&x) returns x (x0) may have the values 17 or 12, the assert should fail.

@jerhard and I discussed how one could fix this: Our conclusion was to modify the enter such that ptr would point to a different copy of x (the one from the caller). In combine, one would then take the value of this outer copy in the return state of the function as the new value for the local x. This ought to be enough, as one can only refer to the outer copies of variables via pointers, and references to the variable directly refer to the instance in the current stackframe.