@@ -445,14 +445,6 @@ module CfgImpl {
       l = n.(Go::GotoStmt).getLabel()
     }
 
-    private predicate hasLabelOrEnclosingLabel(Ast::AstNode n, Label l) {
-      hasLabel(n, l)
-      or
-      exists(Go::LabeledStmt labeled |
-        labeled.getStmt() = n and hasLabelOrEnclosingLabel(labeled, l)
-      )
-    }
-
     predicate preOrderExpr(Ast::Expr e) {
       // The call of a `defer` statement is not invoked at the statement
       // itself; its callee expression and arguments are evaluated in place,
@@ -796,24 +788,16 @@ module CfgImpl {
       n.isAdditional(ast, "catch-return") and
       c.getSuccessorType() instanceof ReturnSuccessor
       or
-      // A `break` in a communication clause body terminates the enclosing
-      // `select` statement, continuing after it. This mirrors the shared
-      // library's handling of `break` in a `switch` case body, but `select` is
-      // modeled language-specifically (it is not a `Switch`), so the break
-      // must be caught here. The break completion bubbles up the AST until it
-      // reaches a top-level statement of the comm clause body, at which point
-      // flow resumes after the `select`. An unlabeled `break` targets the
-      // innermost enclosing construct; a labeled `break` only targets this
-      // `select` if it (or a `LabeledStmt` wrapping it) carries that label.
+      // An unlabeled `break` in a communication clause body terminates the
+      // enclosing `select`. Labeled breaks are handled by the shared
+      // `LabeledStmt` logic.
       exists(Go::SelectStmt sel, Go::CommClause cc |
         cc = sel.getACommClause() and
         ast = cc.getStmt(_) and
         n.isAfter(sel) and
         c.getSuccessorType() instanceof BreakSuccessor
       |
         not c.hasLabel(_)
-        or
-        exists(Label l | c.hasLabel(l) and hasLabelOrEnclosingLabel(sel, l))
       )
       or
       exists(Go::FuncDef fd |
 
@@ -35,6 +35,13 @@ self:
 	goto self // $ gotoTarget=self
 }
 
+func gotoDirectTarget() {
+step1:
+	goto step2 // $ gotoTarget=step2
+step2:
+	goto step1 // $ gotoTarget=step1
+}
+
 func gotoEnclosingStackedLabel(flag bool) {
 outer:
 inner:
 
@@ -1285,23 +1285,9 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
         )
       }
 
-      /** Holds if `n` has `l`, possibly through enclosing labeled statements. */
-      private predicate hasLabel(AstNode n, Input1::Label l) {
-        Input1::hasLabel(n, l)
-        or
-        exists(LabeledStmt labeled | labeled.getStmt() = n and hasLabel(labeled, l))
-      }
-
-      /**
-       * Holds if `target` is a labeled statement at the start of `root`,
-       * possibly nested under other labeled statements.
-       */
-      private predicate labeledTargetInRoot(Stmt root, LabeledStmt target) {
-        root = target
-        or
-        exists(LabeledStmt labeled |
-          root = labeled and labeledTargetInRoot(labeled.getStmt(), target)
-        )
+      /** Holds if `n` is marked with a `LabeledStmt` with label `l`. */
+      private predicate hasEnclosingLabel(AstNode n, Input1::Label l) {
+        exists(LabeledStmt labeled | labeled.getStmt+() = n and Input1::hasLabel(labeled, l))
       }
 
       private predicate callableHasParamDefault(Callable c, Expr defaultValue) {
@@ -1342,7 +1328,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
             or
             exists(Input1::Label l |
               c.hasLabel(l) and
-              hasLabel(loop, l)
+              hasEnclosingLabel(loop, l)
             )
           )
         )
@@ -1382,7 +1368,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
           or
           exists(Input1::Label l |
             c.hasLabel(l) and
-            hasLabel(switch, l)
+            hasEnclosingLabel(switch, l)
           )
         )
         or
@@ -1394,19 +1380,11 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
           c.hasLabel(l)
         )
         or
-        exists(AstNode parent, Stmt root, LabeledStmt target, Input1::Label l |
+        exists(AstNode parent, LabeledStmt root, LabeledStmt target, Input1::Label l |
           ast = getChild(parent, _) and
           root = getChild(parent, _) and
-          labeledTargetInRoot(root, target) and
-          Input1::hasLabel(target, l) and
-          n.isBefore(target) and
-          c.getSuccessorType() instanceof GotoSuccessor and
-          c.hasLabel(l)
-        )
-        or
-        exists(LabeledStmt target, Input1::Label l |
-          ast = target.getStmt() and
-          Input1::hasLabel(target, l) and
+          root.getStmt*() = target and
+          Input1::hasLabel(pragma[only_bind_into](target), l) and
           n.isBefore(target) and
           c.getSuccessorType() instanceof GotoSuccessor and
           c.hasLabel(l)