1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
// RUN: %boogie -vc:nested "%s" > "%t" // RUN: %diff "%s.expect" "%t" procedure P() { A: goto B, C; B: goto G; C: goto D, E; D: goto F; E: goto F; F: goto G; G: return; } procedure Q(x: bool) { A: goto B, C; B: assert x; goto G; C: goto D, E; D: goto F; E: goto F; F: goto G; G: return; }