Incorrect Encoding of break Stmt

[ArquintL]

The following program successfully verifies despite leading to an infinite loop at runtime, since break only escapes the switch statement but not the loop:

package test

decreases
func foo() {
    invariant i == 0
    decreases
    for i := 0; ; i++ {
        switch i {
            default:
                break
        }
    }
}

[ArquintL]

Gobra incorrectly ignores the switch / select context of a break stmt and associates it with the surrounding loop