diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 285e1d57..a10ea86a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -287,6 +287,16 @@ jobs:
           # ('qualLeak'); IsCatchAll matches only the canonical spellings (CodeRabbit review).
           echo "$out" | grep -qE "OWN001.*'qualLeak'" \
             || { echo "FAIL: expected OWN001 on the qualified-typed-catch leak"; exit 1; }
+          # remaining flow-lowering gaps closed: finally-before-return threading (an early
+          # return that skips a later dispose leaks -> 'earlyRet'), `do` desugar (a body-local
+          # never disposed leaks per iteration -> 'doLeak'), and `switch` lowering (a default
+          # branch that does not dispose leaks -> 'swLeak').
+          echo "$out" | grep -qE "OWN001.*'earlyRet'" \
+            || { echo "FAIL: expected OWN001 on the early-return-skips-dispose leak"; exit 1; }
+          echo "$out" | grep -qE "OWN001.*'doLeak'" \
+            || { echo "FAIL: expected OWN001 on the undisposed local in a do-while loop"; exit 1; }
+          echo "$out" | grep -qE "OWN001.*'swLeak'" \
+            || { echo "FAIL: expected OWN001 on the switch default-branch leak"; exit 1; }
           # dispose-optional (Task), disposed/escaping locals, a `for` loop whose
           # disposable is disposed after it (`looped`, balanced), a balanced
           # acquire+dispose in a loop (`whileClean`), a try/finally dispose (`tfClean`,
@@ -303,7 +313,12 @@ jobs:
           # `lamPrior`: a `new` inside a LAMBDA body is deferred (runs on invoke, not at the
           # declaration), so the lambda statement is not a throw point -> no phantom edge skips
           # its post-try dispose -> silent (Codex review: don't descend into lambda bodies).
-          for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior; do
+          # `other`: disposed by the finally, so threaded before the early return -> silent.
+          # `doClean`: acquire+dispose balanced each `do` iteration. `swAll`: every `switch`
+          # case disposes (no default) -> last case is the tail, no phantom no-match leak.
+          # `ncf`: `ncf?.Dispose()` (null-conditional) in a threaded finally IS a release
+          # (member-binding form), so it is disposed on the return path -> silent (Codex review).
+          for ok in clean looped esc exemptTask whileClean asyncDisposed asyncDisposedCfg tfClean tfCatch tfRet tfNull cda daci cif ctorLater lamPrior other doClean swAll ncf; do
             if echo "$out" | grep -q "'$ok'"; then echo "FAIL: silent/exempt case '$ok' was reported"; exit 1; fi
           done
           echo "OK: flow-sensitive OWN001/002/003 on real C# (path-sensitive, loops via while/foreach/for, try/finally sequential, never-vs-every-path wording, dispose-optional exempt, beyond flat)"
diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md
index a0992929..1f8a2b65 100644
--- a/docs/ROADMAP.md
+++ b/docs/ROADMAP.md
@@ -96,8 +96,10 @@ architectural strictness, and the borrow-checker showcase):
    throw exit before each may-throw leaf in a `try` (including inside nested branches, with a
    constructor `new` as a throw point and typed/filtered catches handled). That closes the
    `dispose-not-called-on-throw` shape, which now lands in cross-tool **Agree** with
-   CodeQL's dedicated query on the fixture. Deferred: `finally`-before-`return`,
-   `switch`/`do`. See [docs/notes/real-world-mining.md](notes/real-world-mining.md).
+   CodeQL's dedicated query on the fixture. `finally`-before-`return`, `do` and `switch` are
+   lowered too, so the flow detector covers every common control-flow construct (only
+   `goto`/labeled statements and a few exotic forms still bail). See
+   [docs/notes/real-world-mining.md](notes/real-world-mining.md).
 2. **Resource core** — generalise WPF subscriptions + `IDisposable` into one
    acquire/release/owner/release-region model (P-004 ∪ P-005), so WPF is a
    *profile*, not a one-off.
diff --git a/docs/notes/real-world-mining.md b/docs/notes/real-world-mining.md
index f2d2b4bc..8765387b 100644
--- a/docs/notes/real-world-mining.md
+++ b/docs/notes/real-world-mining.md
@@ -135,8 +135,14 @@ Their leak findings are **nearly disjoint** (file overlap: **1**):
   with a Dispose *after* the try/catch (the caught path disposes the resource) still lowers
   sequentially, to avoid a false leak (PR #32 review). The three recall wins are pinned in CI
   (`nestedLeak`, `ctorPrior`, `typedLeak`) and on the core's IR (the `flow_nested_throw`
-  fixture). Still deferred — both **sound recall gaps** (missed leaks, never false ones):
-  `finally`-before-`return` threading (bailed today) and `switch`/`do`.
+  fixture). The remaining control-flow gaps are now closed too: `finally`-before-`return`
+  (the finally is threaded BEFORE the return instead of bailing the method), `do` (desugared
+  to `B; while(c){B}` — the body runs 1+ times, so a plain 0+-trip `while` would falsely leak
+  a body-released resource), and `switch` (opaque mutually-exclusive branches; with no
+  `default` the last case is the tail rather than an empty no-match path, so an *exhaustive*
+  switch is never falsely flagged — a non-exhaustive no-match leak is only missed when every
+  case disposes, a sound recall gap). The flow detector now models every common control-flow
+  construct; only `goto`/labeled statements and a few exotic forms still honestly bail.
 - **Agree — 1** (`HttpHelper.cs`).
 
 So the SystemEvents and VideoSource findings are **differentiated — confirmed by the
diff --git a/frontend/roslyn/OwnSharp.Extractor/Program.cs b/frontend/roslyn/OwnSharp.Extractor/Program.cs
index fa4bbca7..faa0fdfb 100644
--- a/frontend/roslyn/OwnSharp.Extractor/Program.cs
+++ b/frontend/roslyn/OwnSharp.Extractor/Program.cs
@@ -342,8 +342,9 @@ cc.Filter is null
                                or "global::System.Exception");
 
 // Lower a method block to OwnIR flow nodes (acquire/use/release/if/return) for the
-// `tracked` local IDisposables. Returns null on any UNMODELLED statement
-// (loop/try/switch/...): the method is then honestly skipped, not guessed.
+// `tracked` local IDisposables. Returns null on any UNMODELLED statement (a `goto`, labeled
+// statement, local function, `lock`/`fixed`, …): the method is then honestly skipped, not
+// guessed. Loops, `try`, `do` and `switch` ARE modelled below.
 static List<object>? LowerFlowBody(BlockSyntax block, HashSet<string> tracked)
 {
     var nodes = new List<object>();
@@ -356,16 +357,19 @@ cc.Filter is null
 // `canEscape`: can a throw at the current position leave the METHOD (no enclosing
 // catch-all swallows it)? `onThrow`: the continuation a throw here runs to leave the
 // method (finally-stack + return), or null when no exception edge should be injected
-// (method level, or a region an enclosing catch-all swallows). Both default to the
-// method-body context: a throw escapes, but no edge is injected until a `try` sets one.
+// (method level, or a region an enclosing catch-all swallows). `onReturn`: the continuation
+// a `return` here runs FIRST — the enclosing `finally`(s), then the exit — so a resource a
+// finally disposes is released on the return path; null = a bare return (outside any try).
+// Defaults are the method-body context: throws escape, nothing is injected, returns are bare.
 static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<object> nodes,
-                          bool canEscape = true, List<object>? onThrow = null)
+                          bool canEscape = true, List<object>? onThrow = null,
+                          List<object>? onReturn = null)
 {
     switch (st)
     {
         case BlockSyntax b:
             foreach (var s2 in b.Statements)
-                if (!LowerFlowStmt(s2, tracked, nodes, canEscape, onThrow))
+                if (!LowerFlowStmt(s2, tracked, nodes, canEscape, onThrow, onReturn))
                     return false;
             return true;
         case LocalDeclarationStatementSyntax ld:
@@ -384,10 +388,10 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
         case IfStatementSyntax ifs:
         {
             var thenNodes = new List<object>();
-            if (!LowerFlowStmt(ifs.Statement, tracked, thenNodes, canEscape, onThrow))
+            if (!LowerFlowStmt(ifs.Statement, tracked, thenNodes, canEscape, onThrow, onReturn))
                 return false;
             var elseNodes = new List<object>();
-            if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, elseNodes, canEscape, onThrow))
+            if (ifs.Else is { } e && !LowerFlowStmt(e.Statement, tracked, elseNodes, canEscape, onThrow, onReturn))
                 return false;
             nodes.Add(new { op = "if", line = LineOf(ifs), then = thenNodes, @else = elseNodes });
             return true;
@@ -395,11 +399,16 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
         case UsingStatementSyntax us:
             // using(...) {body}: the using local is auto-disposed (untracked); still
             // lower the body so a tracked plain local used inside is seen.
-            return us.Statement is null || LowerFlowStmt(us.Statement, tracked, nodes, canEscape, onThrow);
+            return us.Statement is null || LowerFlowStmt(us.Statement, tracked, nodes, canEscape, onThrow, onReturn);
         case ReturnStatementSyntax rs:
-            // a tracked local never escapes (excluded), so a returned value is not a
-            // tracked resource — model it as a bare return (a CFG exit edge).
-            nodes.Add(new { op = "return", var = (string?)null, line = LineOf(rs) });
+            // a tracked local never escapes (excluded), so a returned value is not a tracked
+            // resource. A `return` first runs any enclosing `finally`(s) — threaded as
+            // `onReturn`, so a resource the finally disposes is released on the return path —
+            // then exits; outside a try it is a bare CFG exit edge.
+            if (onReturn is not null)
+                nodes.AddRange(onReturn);
+            else
+                nodes.Add(new { op = "return", var = (string?)null, line = LineOf(rs) });
             return true;
         case WhileStatementSyntax ws:
         {
@@ -409,7 +418,7 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
             // double-release). The condition is opaque (we model control flow, not
             // values). If the body has an unmodelled statement, bail the method.
             var bodyNodes = new List<object>();
-            if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, bodyNodes, canEscape, onThrow))
+            if (ws.Statement is null || !LowerFlowStmt(ws.Statement, tracked, bodyNodes, canEscape, onThrow, onReturn))
                 return false;
             nodes.Add(new { op = "while", line = LineOf(ws), body = bodyNodes });
             return true;
@@ -419,10 +428,10 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
             // `foreach` runs its body 0+ times over an (opaque) collection — the same
             // ownership shape as `while`. The loop variable is never a `new`'d
             // candidate and the hidden enumerator is auto-disposed, so modelling the
-            // body as a `while` is sound. (`do` stays unmodelled below — it runs 1+
-            // times; `for` is handled next.)
+            // body as a `while` is sound. (`for` and `do` are handled below; `do` runs 1+
+            // times, so it is desugared rather than modelled as a bare 0+-trip `while`.)
             var bodyNodes = new List<object>();
-            if (fes.Statement is null || !LowerFlowStmt(fes.Statement, tracked, bodyNodes, canEscape, onThrow))
+            if (fes.Statement is null || !LowerFlowStmt(fes.Statement, tracked, bodyNodes, canEscape, onThrow, onReturn))
                 return false;
             nodes.Add(new { op = "while", line = LineOf(fes), body = bodyNodes });
             return true;
@@ -434,9 +443,9 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
             // model control flow, not values); the tracked locals are the ones the
             // BODY declares. A resource declared in the `for` *initializer* is not a
             // method-body local, so it is never a tracked candidate — no soundness
-            // concern, just a separate (rare) recall gap. `do`/try/switch stay below.
+            // concern, just a separate (rare) recall gap.
             var bodyNodes = new List<object>();
-            if (fors.Statement is null || !LowerFlowStmt(fors.Statement, tracked, bodyNodes, canEscape, onThrow))
+            if (fors.Statement is null || !LowerFlowStmt(fors.Statement, tracked, bodyNodes, canEscape, onThrow, onReturn))
                 return false;
             nodes.Add(new { op = "while", line = LineOf(fors), body = bodyNodes });
             return true;
@@ -458,13 +467,6 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
             foreach (var cc in trys.Catches)
                 if (cc.Block.DescendantNodes().OfType<InvocationExpressionSyntax>().Any(IsDisposeShaped))
                     return false;
-            // A `return` in a try-WITH-finally isn't threaded through the exceptional exits
-            // below (finally-before-return), so its finally release would be unreachable ->
-            // bail to stay sound. The common `try { …; return; } finally { dispose }` is
-            // safe anyway, so skipping it loses no real catch.
-            if (trys.Finally is not null
-                && trys.Block.DescendantNodes().OfType<ReturnStatementSyntax>().Any())
-                return false;
             var finallyNodes = new List<object>();
             if (trys.Finally is { } fin && !LowerFlowStmt(fin.Block, tracked, finallyNodes))
                 return false;
@@ -493,17 +495,100 @@ static bool LowerFlowStmt(StatementSyntax st, HashSet<string> tracked, List<obje
                 bodyOnThrow.AddRange(onThrow ?? new List<object>
                     { new { op = "return", var = (string?)null, line = LineOf(trys) } });
             }
+            // A `return` inside the body runs THIS finally, then the enclosing return path
+            // (its finallys), then exits — independent of catches (a `return` is never caught,
+            // unlike a throw), so it is threaded even where the throw edges are suppressed. The
+            // finally release thus runs before the return: `try { …; return; } finally { d }`
+            // disposes on the return path instead of being bailed.
+            var bodyOnReturn = new List<object>(finallyNodes);
+            bodyOnReturn.AddRange(onReturn ?? new List<object>
+                { new { op = "return", var = (string?)null, line = LineOf(trys) } });
             foreach (var stmt in trys.Block.Statements)
-                if (!LowerFlowStmt(stmt, tracked, nodes, bodyCanEscape, bodyOnThrow))
+                if (!LowerFlowStmt(stmt, tracked, nodes, bodyCanEscape, bodyOnThrow, bodyOnReturn))
                     return false;
             nodes.AddRange(finallyNodes);   // normal completion runs the finally
             return true;
         }
+        case DoStatementSyntax dos:
+        {
+            // do { B } while(c)  ≡  B; while(c) { B }  — the body runs 1+ times. Lower B once
+            // unconditionally (the guaranteed first iteration), then a `while` of B (0+ more).
+            // Modelling it as a plain `while` (0+ trips) would be UNSOUND: a resource released
+            // only in the body but acquired before the loop would falsely leak on the phantom
+            // 0-trip path. Bail (like the loops) if the body has an unmodelled statement.
+            if (dos.Statement is null
+                || !LowerFlowStmt(dos.Statement, tracked, nodes, canEscape, onThrow, onReturn))
+                return false;
+            var bodyNodes = new List<object>();
+            if (!LowerFlowStmt(dos.Statement, tracked, bodyNodes, canEscape, onThrow, onReturn))
+                return false;
+            nodes.Add(new { op = "while", line = LineOf(dos), body = bodyNodes });
+            return true;
+        }
+        case SwitchStatementSyntax sw:
+        {
+            // switch(e) { (case L: | default:) section … } modelled as a chain of opaque,
+            // mutually-exclusive branches: `if(*){ s1 } else { if(*){ s2 } else { … } }` — one
+            // per section, value-opaque (we model control flow, not the matched value). A
+            // trailing `break` ends a section (stripped); a section doing anything the model
+            // can't place here (a nested `break`, `goto case`, `throw`) bails the method.
+            List<object>? defaultNodes = null;
+            var cases = new List<List<object>>();
+            foreach (var section in sw.Sections)
+            {
+                var secNodes = new List<object>();
+                if (!LowerSwitchSection(section, tracked, secNodes, canEscape, onThrow, onReturn))
+                    return false;
+                if (section.Labels.Any(l => l is DefaultSwitchLabelSyntax))
+                    defaultNodes = secNodes;
+                else
+                    cases.Add(secNodes);
+            }
+            // The chain's tail — the "no earlier case matched" branch. A `default` IS that
+            // branch. With NO default we do NOT model an empty no-match path: that would falsely
+            // flag a resource disposed in every case of an EXHAUSTIVE switch (e.g. over an enum)
+            // as leaking on a path that cannot occur. Instead the LAST case becomes the tail
+            // (assume some branch runs) — sound: a genuinely non-exhaustive no-match leak is only
+            // missed when EVERY case disposes the resource (a recall gap, never a false positive).
+            List<object> chain;
+            if (defaultNodes is not null)
+                chain = defaultNodes;
+            else if (cases.Count == 0)
+                return true;                         // empty switch -> no flow effect
+            else
+            {
+                chain = cases[^1];
+                cases.RemoveAt(cases.Count - 1);
+            }
+            for (int k = cases.Count - 1; k >= 0; k--)
+                chain = new List<object>
+                    { new { op = "if", line = LineOf(sw), then = cases[k], @else = chain } };
+            nodes.AddRange(chain);
+            return true;
+        }
         default:
-            return false;   // unmodelled (do/switch/...) -> bail the method
+            return false;   // unmodelled (goto/labeled/throw/...) -> bail the method
     }
 }
 
+// Lower one `switch` section's statements, treating a top-level `break` as the section
+// terminator (it just exits the switch, so it is stripped). Bails (false) on any statement the
+// flow model doesn't handle here — including a `break` nested inside an `if`/loop, which reaches
+// the unmodelled default and conservatively skips the whole method.
+static bool LowerSwitchSection(SwitchSectionSyntax section, HashSet<string> tracked,
+                               List<object> nodes, bool canEscape,
+                               List<object>? onThrow, List<object>? onReturn)
+{
+    foreach (var stmt in section.Statements)
+    {
+        if (stmt is BreakStatementSyntax)
+            break;
+        if (!LowerFlowStmt(stmt, tracked, nodes, canEscape, onThrow, onReturn))
+            return false;
+    }
+    return true;
+}
+
 static void EmitFlowExpr(ExpressionSyntax expr, HashSet<string> tracked, List<object> nodes)
 {
     // `await x.DisposeAsync()` is the IAsyncDisposable release — look through the
@@ -527,6 +612,20 @@ static void EmitFlowExpr(ExpressionSyntax expr, HashSet<string> tracked, List<ob
         nodes.Add(new { op = "release", var = rid.Identifier.Text, line = LineOf(inv) });
         return;
     }
+    // x?.Dispose()/x?.Close()/x?.DisposeAsync() (null-conditional) is the release too — the
+    // call is a member BINDING under a conditional access, not a member access. Mirrors
+    // IsDisposeShaped so a `?.` dispose (e.g. in a finally) is not mistaken for a bare use,
+    // which would otherwise falsely flag the resource as leaked.
+    if (expr is ConditionalAccessExpressionSyntax cond
+        && cond.Expression is IdentifierNameSyntax cid
+        && tracked.Contains(cid.Identifier.Text)
+        && cond.WhenNotNull is InvocationExpressionSyntax condInv
+        && condInv.Expression is MemberBindingExpressionSyntax mb
+        && mb.Name.Identifier.Text is "Dispose" or "Close" or "DisposeAsync")
+    {
+        nodes.Add(new { op = "release", var = cid.Identifier.Text, line = LineOf(cond) });
+        return;
+    }
     // any other reference to a tracked local -> use (once per local in this expr).
     var used = new SortedSet<string>(StringComparer.Ordinal);
     foreach (var idn in expr.DescendantNodesAndSelf().OfType<IdentifierNameSyntax>())
diff --git a/frontend/roslyn/samples/FlowLocalsSample.cs b/frontend/roslyn/samples/FlowLocalsSample.cs
index 06ccd28f..2b65da94 100644
--- a/frontend/roslyn/samples/FlowLocalsSample.cs
+++ b/frontend/roslyn/samples/FlowLocalsSample.cs
@@ -116,9 +116,10 @@ public void CatchDisposesSkipped()
         catch (Exception) { tfCatch.Dispose(); }
     }
 
-    // a `return` inside a try-with-finally: the finally still disposes (SAFE), but the
-    // model can't yet place the finally before the return — so it bails rather than
-    // falsely flag the resource as leaked on the return path -> silent.
+    // a `return` inside a try-with-finally: the finally is now threaded BEFORE the return
+    // (onReturn), so `tfRet.Dispose()` runs on the early-return path too -> disposed on every
+    // path -> silent. (Previously the whole method bailed to avoid a false leak; now it is
+    // analysed, and an early return that skipped a dispose would be caught — see EarlyReturnLeak.)
     public void TryFinallyReturn(bool c)
     {
         var tfRet = new MemoryStream();
@@ -266,6 +267,83 @@ public void CtorInLambdaNotThrow()
         lamPrior.Dispose();
     }
 
+    // finally-before-return: the early `return` runs the finally (disposing `other`) FIRST,
+    // then exits — so `other` is released on the return path and stays silent. But `earlyRet`
+    // is disposed only AFTER the try, which the early return (and the throw on WriteByte) skip
+    // -> it leaks on those paths (OWN001). The try-with-finally + return used to bail the whole
+    // method; it is now threaded and analysed.
+    public void EarlyReturnLeak(bool c)
+    {
+        var earlyRet = new MemoryStream();
+        var other = new MemoryStream();
+        try { if (c) return; earlyRet.WriteByte(1); }
+        finally { other.Dispose(); }
+        earlyRet.Dispose();
+    }
+
+    // `ncf?.Dispose()` (null-conditional) in a finally IS a release — EmitFlowExpr recognizes
+    // the member-binding form, not just `ncf.Dispose()`. With the return threaded through the
+    // finally, `ncf` is disposed on the early-return path too -> silent (Codex review on PR #34:
+    // a `?.Dispose()` in a now-threaded finally must not be mistaken for a bare use -> false leak).
+    public void NullCondFinallyDispose(bool c)
+    {
+        var ncf = new MemoryStream();
+        try { if (c) return; ncf.WriteByte(1); }
+        finally { ncf?.Dispose(); }
+    }
+
+    // `do { B } while(c)` runs B 1+ times -> desugared to `B; while(c){ B }`. A local acquired
+    // in the body and never disposed leaks per iteration -> OWN001 on `doLeak`.
+    public void DoLeak(bool c)
+    {
+        do
+        {
+            var doLeak = new MemoryStream();
+            doLeak.WriteByte(1);
+        }
+        while (c);
+    }
+
+    // acquire + dispose within a `do` body is balanced every iteration -> silent. The desugar
+    // keeps the guaranteed first iteration; a naive 0+-trip `while` would have falsely leaked a
+    // body-released resource on the phantom 0-trip path.
+    public void DoClean(bool c)
+    {
+        do
+        {
+            var doClean = new MemoryStream();
+            doClean.WriteByte(1);
+            doClean.Dispose();
+        }
+        while (c);
+    }
+
+    // `switch` modelled as opaque mutually-exclusive branches. Every case disposes `swAll` and
+    // there is NO default -> the last case is the tail (no empty no-match branch), so an
+    // exhaustive switch is not falsely flagged -> silent. (A genuinely non-exhaustive no-match
+    // leak is only missed when EVERY case disposes — a sound recall gap, never a false leak.)
+    public void SwitchAllDispose(int mode)
+    {
+        var swAll = new MemoryStream();
+        switch (mode)
+        {
+            case 0: swAll.WriteByte(1); swAll.Dispose(); break;
+            case 1: swAll.Dispose(); break;
+        }
+    }
+
+    // a `switch` whose default branch does NOT dispose `swLeak` -> it leaks on that path
+    // (OWN001). The case-0 branch disposes it; the default (the chain's tail) does not.
+    public void SwitchOneLeak(int mode)
+    {
+        var swLeak = new MemoryStream();
+        switch (mode)
+        {
+            case 0: swLeak.Dispose(); break;
+            default: swLeak.WriteByte(1); break;
+        }
+    }
+
     private static void MayThrow() { }
 
     // acquire + dispose within the loop body is balanced -> silent (no false
diff --git a/tests/fixtures/ownir/flow_finally_switch.facts.json b/tests/fixtures/ownir/flow_finally_switch.facts.json
new file mode 100644
index 00000000..fb38f435
--- /dev/null
+++ b/tests/fixtures/ownir/flow_finally_switch.facts.json
@@ -0,0 +1,55 @@
+{
+  "ownir_version": 0,
+  "module": "Extracted",
+  "comment": "IR the extractor now emits for finally-before-return and switch lowering. (1) FinallyReturnClean: a `return` inside try-with-finally runs the finally (release r) FIRST, so r is released on the return path -> silent (was bailed before). (2) FinallyReturnLeak: an early return with the dispose AFTER the try (empty finally) leaks on that path. (3) SwitchAllDispose: a no-default switch where every case disposes — modelled with the last case as the tail (no empty no-match branch), so it stays silent (Model A: no phantom-leak FP on an exhaustive switch). (4) SwitchOneLeak: a switch whose default/else branch leaks.",
+  "components": [],
+  "functions": [
+    {
+      "name": "FlowLocalsSample.FinallyReturnClean",
+      "file": "FlowLocalsSample.cs",
+      "body": [
+        {"op": "acquire", "var": "r", "line": 10},
+        {"op": "if", "line": 11, "then": [
+          {"op": "release", "var": "r", "line": 11},
+          {"op": "return", "var": null, "line": 11}
+        ], "else": []},
+        {"op": "release", "var": "r", "line": 12}
+      ]
+    },
+    {
+      "name": "FlowLocalsSample.FinallyReturnLeak",
+      "file": "FlowLocalsSample.cs",
+      "body": [
+        {"op": "acquire", "var": "r2", "line": 20},
+        {"op": "if", "line": 21, "then": [
+          {"op": "return", "var": null, "line": 21}
+        ], "else": []},
+        {"op": "release", "var": "r2", "line": 23}
+      ]
+    },
+    {
+      "name": "FlowLocalsSample.SwitchAllDispose",
+      "file": "FlowLocalsSample.cs",
+      "body": [
+        {"op": "acquire", "var": "s", "line": 30},
+        {"op": "if", "line": 31, "then": [
+          {"op": "release", "var": "s", "line": 31}
+        ], "else": [
+          {"op": "release", "var": "s", "line": 32}
+        ]}
+      ]
+    },
+    {
+      "name": "FlowLocalsSample.SwitchOneLeak",
+      "file": "FlowLocalsSample.cs",
+      "body": [
+        {"op": "acquire", "var": "s2", "line": 40},
+        {"op": "if", "line": 41, "then": [
+          {"op": "release", "var": "s2", "line": 41}
+        ], "else": [
+          {"op": "use", "var": "s2", "line": 42}
+        ]}
+      ]
+    }
+  ]
+}
diff --git a/tests/test_ownir.py b/tests/test_ownir.py
index aca92cbf..4d572647 100644
--- a/tests/test_ownir.py
+++ b/tests/test_ownir.py
@@ -58,6 +58,8 @@
                                   "ownir", "flow_leak_two_exits.facts.json")
 _NESTED_THROW_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
                                      "ownir", "flow_nested_throw.facts.json")
+_FINALLY_SWITCH_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
+                                       "ownir", "flow_finally_switch.facts.json")
 _DI_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
                            "ownir", "di.facts.json")
 _UNRESOLVED_FIXTURE = os.path.join(os.path.dirname(__file__), "fixtures",
@@ -375,6 +377,23 @@ def _one(source: str, lambda_: bool = False) -> Finding:
                      f"(nested clean 'cif' and later-acquired 'ctorLater' stay silent), "
                      f"got {got}")
 
+    # --- finally-before-return + switch lowering: a `return` inside a try-with-finally runs
+    #     the finally first (a finally-disposed resource is released on the return path ->
+    #     silent), an early return that skips a later dispose leaks ('r2'), a no-default switch
+    #     where every case disposes stays silent (last case is the tail — no phantom no-match
+    #     leak, the Model-A soundness choice for exhaustive switches), and a switch whose
+    #     else/default branch leaks is flagged ('s2'). Pins the verdicts on the IR the new
+    #     lowering emits (the C# lowering itself is covered in CI).
+    with open(_FINALLY_SWITCH_FIXTURE, encoding="utf-8") as f:
+        fsfacts = json.load(f)
+    fsfindings = check_facts(fsfacts)
+    checks += 1
+    fsgot = sorted((x.event, x.code, x.line) for x in fsfindings)
+    if fsgot != [("r2", "OWN001", 20), ("s2", "OWN001", 40)]:
+        fails.append(f"expected OWN001 on 'r2'@20 (early-return leak) and 's2'@40 (switch "
+                     f"else-branch leak) only — clean 'r' (finally before return) and 's' "
+                     f"(switch all-dispose) stay silent — got {fsgot}")
+
     # --- P-016 A1 reaches the frontend: a `while` flow body (the extractor now
     #     lowers loops instead of skipping the method) routes through the core's
     #     worklist fixpoint. A resource acquired before the loop and released INSIDE