diff --git a/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart b/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart
index 002764fddf1..ec912f17ea7 100644
--- a/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart
+++ b/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart
@@ -2668,11 +2668,18 @@ class FlowModel<Type extends Object> {
         //
         // In all of these cases, the correct thing to do is to keep all
         // promotions that were done in both the `try` and `finally` blocks.
-        newPromotedTypes = PromotionModel.rebasePromotedTypes(
-          helper,
-          thisModel.promotedTypes,
-          afterFinallyModel.promotedTypes,
-        );
+        newPromotedTypes =
+            helper.typeAnalyzerOptions.soundFlowAnalysisEnabled
+                ? PromotionModel.rebasePromotedTypes(
+                  helper,
+                  afterFinallyModel.promotedTypes,
+                  thisModel.promotedTypes,
+                )
+                : PromotionModel.rebasePromotedTypes(
+                  helper,
+                  thisModel.promotedTypes,
+                  afterFinallyModel.promotedTypes,
+                );
         // And we can safely restore the SSA node from the end of the try block.
         newSsaNode = thisModel.ssaNode;
         if (newSsaNode != afterFinallyModel.ssaNode) {
@@ -3382,6 +3389,9 @@ mixin FlowModelHelper<Type extends Object> {
   @visibleForTesting
   PromotionKeyStore<Object> get promotionKeyStore;
 
+  /// Language features enables affecting the behavior of flow analysis.
+  TypeAnalyzerOptions get typeAnalyzerOptions;
+
   /// The [FlowAnalysisTypeOperations], used to access types and check
   /// subtyping.
   @visibleForTesting
@@ -4988,7 +4998,7 @@ class _FlowAnalysisImpl<
     implements
         FlowAnalysis<Node, Statement, Expression, Variable, Type>,
         _PropertyTargetHelper<Expression, Type> {
-  /// Language features enables affecting the behavior of flow analysis.
+  @override
   final TypeAnalyzerOptions typeAnalyzerOptions;
 
   /// The [FlowAnalysisOperations], used to access types, check subtyping, and
diff --git a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart
index 16d875a3165..e550f28ff15 100644
--- a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart
+++ b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart
@@ -6,6 +6,7 @@ import 'package:_fe_analyzer_shared/src/flow_analysis/flow_analysis.dart';
 import 'package:_fe_analyzer_shared/src/flow_analysis/flow_analysis_operations.dart';
 import 'package:_fe_analyzer_shared/src/type_inference/promotion_key_store.dart';
 import 'package:_fe_analyzer_shared/src/type_inference/type_analysis_result.dart';
+import 'package:_fe_analyzer_shared/src/type_inference/type_analyzer.dart';
 import 'package:_fe_analyzer_shared/src/types/shared_type.dart';
 
 import '../mini_ast.dart';
@@ -38,6 +39,9 @@ class FlowAnalysisTestHarness extends Harness
   @override
   final SharedTypeView boolType = SharedTypeView(Type('bool'));
 
+  @override
+  TypeAnalyzerOptions get typeAnalyzerOptions => computeTypeAnalyzerOptions();
+
   @override
   FlowAnalysisOperations<Var, SharedTypeView> get typeOperations =>
       typeAnalyzer.operations;
diff --git a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart
index 2bbdca8c084..d308aca7a41 100644
--- a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart
+++ b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart
@@ -12200,14 +12200,13 @@ main() {
               x.as_('List<dynamic>'),
               checkPromoted(x, 'List<dynamic>'),
             ]),
-            // After the try/finally, the promotions in the try block are
-            // layered over the promotions in the finally block (see
-            // https://github.com/dart-lang/language/issues/4382), so the
-            // promotion to `List<Object?>` layers over the promotion to
-            // `List<dynamic>`. But since the two types are mutual subtypes, the
-            // promotion to `List<Object?>` is discarded, leaving only the
-            // promotion to `List<dynamic>`.
-            checkPromoted(x, 'List<dynamic>'),
+            // After the try/finally, the promotions in the finally block are
+            // layered over the promotions in the try block, so the
+            // promotion to `List<dynamic>` layers over the promotion to
+            // `List<Object?>`. But since the two types are mutual subtypes, the
+            // promotion to `List<dynamic>` is discarded, leaving only the
+            // promotion to `List<Object?>`.
+            checkPromoted(x, 'List<Object?>'),
           ]);
         });
 
@@ -12224,14 +12223,13 @@ main() {
               x.property('_property').as_('List<dynamic>'),
               checkPromoted(x.property('_property'), 'List<dynamic>'),
             ]),
-            // After the try/finally, the promotions in the try block are
-            // layered over the promotions in the finally block (see
-            // https://github.com/dart-lang/language/issues/4382), so the
-            // promotion to `List<Object?>` layers over the promotion to
-            // `List<dynamic>`. But since the two types are mutual subtypes, the
-            // promotion to `List<Object?>` is discarded, leaving only the
-            // promotion to `List<dynamic>`.
-            checkPromoted(x.property('_property'), 'List<dynamic>'),
+            // After the try/finally, the promotions in the finally block are
+            // layered over the promotions in the try block, so the
+            // promotion to `List<dynamic>` layers over the promotion to
+            // `List<Object?>`. But since the two types are mutual subtypes, the
+            // promotion to `List<dynamic>` is discarded, leaving only the
+            // promotion to `List<Object?>`.
+            checkPromoted(x.property('_property'), 'List<Object?>'),
           ]);
         });
 
@@ -12281,6 +12279,331 @@ main() {
         ]);
       });
     });
+
+    group('Try/finally layering order:', () {
+      group('Local variables:', () {
+        test('When disabled, promotions in `finally` applied first', () {
+          h.disableSoundFlowAnalysis();
+          var x = Var('x');
+          var y = Var('y');
+          h.run([
+            declare(x, initializer: expr('Object')),
+            declare(y, initializer: expr('Object')),
+            if_(
+              expr('bool'),
+              [
+                x.as_('num'),
+                y.as_('num'),
+                // The promotion chains for `x` and `y` are both `[num]`.
+                checkPromoted(x, 'num'),
+                checkPromoted(y, 'num'),
+              ],
+              [
+                try_([
+                  x.as_('num'),
+                  y.as_('int'),
+                  checkPromoted(x, 'num'),
+                  checkPromoted(y, 'int'),
+                ]).finally_([
+                  // Neither `x` nor `y` is promoted at this point, because in
+                  // principle an exception could have occurred at any point in
+                  // the `try` block.
+                  checkNotPromoted(x),
+                  checkNotPromoted(y),
+                  x.as_('int'),
+                  y.as_('num'),
+                  checkPromoted(x, 'int'),
+                  checkPromoted(y, 'num'),
+                ]),
+                // After the try/finally, both `x` and `y` are fully promoted to
+                // `int`.
+                checkPromoted(x, 'int'),
+                checkPromoted(y, 'int'),
+                // But since the promotions from the `try` block are layered
+                // over the promotions from the `finally` block, `x` has
+                // promotion chain `[int]`, whereas `y` has promotion chain
+                // `[num, int]`. Therefore, after the `if` and `else` control
+                // flow paths are joined...
+              ],
+            ),
+            // `x` is no longer promoted at all (since `[num]` and `[int]` have
+            // no types in common), whereas `y` is promoted to `num` (since
+            // `[num]` and `[num, int]` both contain the type `num`).
+            checkNotPromoted(x),
+            checkPromoted(y, 'num'),
+          ]);
+        });
+
+        test('When enabled, promotions in `try` applied first', () {
+          var x = Var('x');
+          var y = Var('y');
+          h.run([
+            declare(x, initializer: expr('Object')),
+            declare(y, initializer: expr('Object')),
+            if_(
+              expr('bool'),
+              [
+                x.as_('num'),
+                y.as_('num'),
+                // The promotion chains for `x` and `y` are both `[num]`.
+                checkPromoted(x, 'num'),
+                checkPromoted(y, 'num'),
+              ],
+              [
+                try_([
+                  x.as_('num'),
+                  y.as_('int'),
+                  checkPromoted(x, 'num'),
+                  checkPromoted(y, 'int'),
+                ]).finally_([
+                  // Neither `x` nor `y` is promoted at this point, because in
+                  // principle an exception could have occurred at any point in
+                  // the `try` block.
+                  checkNotPromoted(x),
+                  checkNotPromoted(y),
+                  x.as_('int'),
+                  y.as_('num'),
+                  checkPromoted(x, 'int'),
+                  checkPromoted(y, 'num'),
+                ]),
+                // After the try/finally, both `x` and `y` are fully promoted to
+                // `int`.
+                checkPromoted(x, 'int'),
+                checkPromoted(y, 'int'),
+                // But since the promotions from the `finally` block are layered
+                // over the promotions from the `try` block, `x` has
+                // promotion chain `[num, int]`, whereas `y` has promotion chain
+                // `[int]`. Therefore, after the `if` and `else` control flow
+                // paths are joined...
+              ],
+            ),
+            // `x` is promoted to `num` (since `[num]` and `[num, int]` both
+            // contain the type `num`), whereas `y` is no longer promoted at all
+            // (since `[num]` and `[int]` have no types in common).
+            checkPromoted(x, 'num'),
+            checkNotPromoted(y),
+          ]);
+        });
+      });
+
+      group('Fields of unmodified local variables:', () {
+        test('When disabled, promotions in `finally` applied first', () {
+          h.disableSoundFlowAnalysis();
+          h.addMember('C', '_f', 'Object', promotable: true);
+          var x = Var('x');
+          var y = Var('y');
+          h.run([
+            declare(x, initializer: expr('C')),
+            declare(y, initializer: expr('C')),
+            if_(
+              expr('bool'),
+              [
+                x.property('_f').as_('num'),
+                y.property('_f').as_('num'),
+                // The promotion chains for `x._f` and `y._f` are both `[num]`.
+                checkPromoted(x.property('_f'), 'num'),
+                checkPromoted(y.property('_f'), 'num'),
+              ],
+              [
+                try_([
+                  x.property('_f').as_('num'),
+                  y.property('_f').as_('int'),
+                  checkPromoted(x.property('_f'), 'num'),
+                  checkPromoted(y.property('_f'), 'int'),
+                ]).finally_([
+                  // Neither `x._f` nor `y._f` is promoted at this point,
+                  // because in principle an exception could have occurred at
+                  // any point in the `try` block.
+                  checkNotPromoted(x.property('_f')),
+                  checkNotPromoted(y.property('_f')),
+                  x.property('_f').as_('int'),
+                  y.property('_f').as_('num'),
+                  checkPromoted(x.property('_f'), 'int'),
+                  checkPromoted(y.property('_f'), 'num'),
+                ]),
+                // After the try/finally, both `x._f` and `y._f` are fully
+                // promoted to `int`.
+                checkPromoted(x.property('_f'), 'int'),
+                checkPromoted(y.property('_f'), 'int'),
+                // But since the promotions from the `try` block are layered
+                // over the promotions from the `finally` block, `x._f` has
+                // promotion chain `[int]`, whereas `y._f` has promotion chain
+                // `[num, int]`. Therefore, after the `if` and `else` control
+                // flow paths are joined...
+              ],
+            ),
+            // `x._f` is no longer promoted at all (since `[num]` and `[int]`
+            // have no types in common), whereas `y._f` is promoted to `num`
+            // (since `[num]` and `[num, int]` both contain the type `num`).
+            checkNotPromoted(x.property('_f')),
+            checkPromoted(y.property('_f'), 'num'),
+          ]);
+        });
+
+        test('When enabled, promotions in `try` applied first', () {
+          h.addMember('C', '_f', 'Object', promotable: true);
+          var x = Var('x');
+          var y = Var('y');
+          h.run([
+            declare(x, initializer: expr('C')),
+            declare(y, initializer: expr('C')),
+            if_(
+              expr('bool'),
+              [
+                x.property('_f').as_('num'),
+                y.property('_f').as_('num'),
+                // The promotion chains for `x._f` and `y._f` are both `[num]`.
+                checkPromoted(x.property('_f'), 'num'),
+                checkPromoted(y.property('_f'), 'num'),
+              ],
+              [
+                try_([
+                  x.property('_f').as_('num'),
+                  y.property('_f').as_('int'),
+                  checkPromoted(x.property('_f'), 'num'),
+                  checkPromoted(y.property('_f'), 'int'),
+                ]).finally_([
+                  // Neither `x._f` nor `y._f` is promoted at this point,
+                  // because in principle an exception could have occurred at
+                  // any point in the `try` block.
+                  checkNotPromoted(x.property('_f')),
+                  checkNotPromoted(y.property('_f')),
+                  x.property('_f').as_('int'),
+                  y.property('_f').as_('num'),
+                  checkPromoted(x.property('_f'), 'int'),
+                  checkPromoted(y.property('_f'), 'num'),
+                ]),
+                // After the try/finally, both `x._f` and `y._f` are fully
+                // promoted to `int`.
+                checkPromoted(x.property('_f'), 'int'),
+                checkPromoted(y.property('_f'), 'int'),
+                // But since the promotions from the `finally` block are layered
+                // over the promotions from the `try` block, `x._f` has
+                // promotion chain `[num, int]`, whereas `y._f` has promotion
+                // chain `[int]`. Therefore, after the `if` and `else` control
+                // flow paths are joined...
+              ],
+            ),
+            // `x._f` is promoted to `num` (since `[num]` and `[num, int]` both
+            // contain the type `num`), whereas `y._f` is no longer promoted at
+            // all (since `[num]` and `[int]` have no types in common).
+            checkPromoted(x.property('_f'), 'num'),
+            checkNotPromoted(y.property('_f')),
+          ]);
+        });
+      });
+
+      group('Fields of local variables modified in try clause:', () {
+        test('When disabled, promotions in `try` applied first', () {
+          h.disableSoundFlowAnalysis();
+          h.addMember('C', '_f', 'Object', promotable: true);
+          var x = Var('x');
+          var y = Var('y');
+          h.run([
+            declare(x, initializer: expr('C')),
+            declare(y, initializer: expr('C')),
+            if_(
+              expr('bool'),
+              [
+                x.property('_f').as_('num'),
+                y.property('_f').as_('num'),
+                // The promotion chains for `x._f` and `y._f` are both `[num]`.
+                checkPromoted(x.property('_f'), 'num'),
+                checkPromoted(y.property('_f'), 'num'),
+              ],
+              [
+                try_([
+                  x.write(expr('C')),
+                  y.write(expr('C')),
+                  x.property('_f').as_('num'),
+                  y.property('_f').as_('int'),
+                  checkPromoted(x.property('_f'), 'num'),
+                  checkPromoted(y.property('_f'), 'int'),
+                ]).finally_([
+                  // Neither `x._f` nor `y._f` is promoted at this point,
+                  // because in principle an exception could have occurred at
+                  // any point in the `try` block.
+                  checkNotPromoted(x.property('_f')),
+                  checkNotPromoted(y.property('_f')),
+                  x.property('_f').as_('int'),
+                  y.property('_f').as_('num'),
+                  checkPromoted(x.property('_f'), 'int'),
+                  checkPromoted(y.property('_f'), 'num'),
+                ]),
+                // After the try/finally, both `x._f` and `y._f` are fully
+                // promoted to `int`.
+                checkPromoted(x.property('_f'), 'int'),
+                checkPromoted(y.property('_f'), 'int'),
+                // But since the promotions from the `finally` block are layered
+                // over the promotions from the `try` block, `x._f` has
+                // promotion chain `[num, int]`, whereas `y._f` has promotion
+                // chain `[int]`. Therefore, after the `if` and `else` control
+                // flow paths are joined...
+              ],
+            ),
+            // `x._f` is promoted to `num` (since `[num]` and `[num, int]` both
+            // contain the type `num`), whereas `y._f` is no longer promoted at
+            // all (since `[num]` and `[int]` have no types in common).
+            checkPromoted(x.property('_f'), 'num'),
+            checkNotPromoted(y.property('_f')),
+          ]);
+        });
+
+        test('When enabled, promotions in `try` applied first', () {
+          h.addMember('C', '_f', 'Object', promotable: true);
+          var x = Var('x');
+          var y = Var('y');
+          h.run([
+            declare(x, initializer: expr('C')),
+            declare(y, initializer: expr('C')),
+            if_(
+              expr('bool'),
+              [
+                x.property('_f').as_('num'),
+                y.property('_f').as_('num'),
+                // The promotion chains for `x._f` and `y._f` are both `[num]`.
+                checkPromoted(x.property('_f'), 'num'),
+                checkPromoted(y.property('_f'), 'num'),
+              ],
+              [
+                try_([
+                  x.write(expr('C')),
+                  y.write(expr('C')),
+                  x.property('_f').as_('num'),
+                  y.property('_f').as_('int'),
+                  checkPromoted(x.property('_f'), 'num'),
+                  checkPromoted(y.property('_f'), 'int'),
+                ]).finally_([
+                  // Neither `x._f` nor `y._f` is promoted at this point,
+                  // because in principle an exception could have occurred at
+                  // any point in the `try` block.
+                  checkNotPromoted(x.property('_f')),
+                  checkNotPromoted(y.property('_f')),
+                  x.property('_f').as_('int'),
+                  y.property('_f').as_('num'),
+                  checkPromoted(x.property('_f'), 'int'),
+                  checkPromoted(y.property('_f'), 'num'),
+                ]),
+                // After the try/finally, both `x._f` and `y._f` are fully
+                // promoted to `int`.
+                checkPromoted(x.property('_f'), 'int'),
+                checkPromoted(y.property('_f'), 'int'),
+                // But since the promotions from the `finally` block are layered
+                // over the promotions from the `try` block, `x._f` has
+                // promotion chain `[num, int]`, whereas `y._f` has promotion
+                // chain `[int]`. Therefore, after the `if` and `else` control
+                // flow paths are joined...
+              ],
+            ),
+            // `x._f` is promoted to `num` (since `[num]` and `[num, int]` both
+            // contain the type `num`), whereas `y._f` is no longer promoted at
+            // all (since `[num]` and `[int]` have no types in common).
+            checkPromoted(x.property('_f'), 'num'),
+            checkNotPromoted(y.property('_f')),
+          ]);
+        });
+      });
+    });
   });
 
   group('Demotion and type of interest promotion:', () {
diff --git a/tests/language/sound_flow_analysis/proper_subtypes_test.dart b/tests/language/sound_flow_analysis/proper_subtypes_test.dart
index a8fe9a7d539..d2a80a09639 100644
--- a/tests/language/sound_flow_analysis/proper_subtypes_test.dart
+++ b/tests/language/sound_flow_analysis/proper_subtypes_test.dart
@@ -168,15 +168,18 @@ testFinallyClauseVariable(Object? x) {
     // Verify that the type really is `List<dynamic>` and not `List<Object?>`.
     x.first.abs();
   }
-  // After the try/finally, the promotions in the try block are layered over the
-  // promotions in the finally block (see
-  // https://github.com/dart-lang/language/issues/4382), so the promotion to
-  // `List<Object?>` layers over the promotion to `List<dynamic>`. But since the
-  // two types are mutual subtypes, the promotion to `List<Object?>` is
-  // discarded, leaving only the promotion to `List<dynamic>`.
-  x.expectStaticType<Exactly<List<dynamic>>>();
-  // Verify that the type really is `List<dynamic>` and not `List<Object?>`.
-  x.first.abs();
+  // After the try/finally, the promotions in the finally block are layered over
+  // the promotions in the try block, so the promotion to `List<dynamic>` layers
+  // over the promotion to `List<Object?>`. But since the two types are mutual
+  // subtypes, the promotion to `List<dynamic>` is discarded, leaving only the
+  // promotion to `List<Object?>`.
+  x.expectStaticType<Exactly<List<Object?>>>();
+  // Verify that the type really is `List<Object?>` and not `List<dynamic>`.
+  {
+    var z = x.first;
+    z!;
+    [z].expectStaticType<Exactly<List<Object>>>();
+  }
 }
 
 // When promotions from a `try` block and `finally` block are combined, a
@@ -204,15 +207,20 @@ testFinallyClausePropertyOfUnmodifiedVariable(C x) {
     // Verify that the type really is `List<dynamic>` and not `List<Object?>`.
     x._f.first.abs();
   }
-  // After the try/finally, the promotions in the try block are layered over the
-  // promotions in the finally block (see
-  // https://github.com/dart-lang/language/issues/4382), so the promotion to
-  // `List<Object?>` layers over the promotion to `List<dynamic>`. But since the
-  // two types are mutual subtypes, the promotion to `List<Object?>` is
-  // discarded, leaving only the promotion to `List<dynamic>`.
-  x._f.expectStaticType<Exactly<List<dynamic>>>();
-  // Verify that the type really is `List<dynamic>` and not `List<Object?>`.
-  x._f.first.abs();
+  // After the try/finally, the promotions in the finally block are layered over
+  // the promotions in the try block, so the promotion to `List<dynamic>` layers
+  // over the promotion to `List<Object?>`. But since the two types are mutual
+  // subtypes, the promotion to `List<dynamic>` is discarded, leaving only the
+  // promotion to `List<Object?>`.
+  x._f.expectStaticType<Exactly<List<Object?>>>();
+  // Verify that the type really is `List<Object?>` and not `List<dynamic>`.
+  // (This works because applying `!` to a variable of type `Object?` promotes
+  // it, but applying `!` to a variable of type `dynamic` doesn't promote it.)
+  {
+    var z = x._f.first;
+    z!;
+    [z].expectStaticType<Exactly<List<Object>>>();
+  }
 }
 
 // When promotions from a `try` block and `finally` block are combined, a
diff --git a/tests/language/sound_flow_analysis/try_finally_layering_disabled_test.dart b/tests/language/sound_flow_analysis/try_finally_layering_disabled_test.dart
new file mode 100644
index 00000000000..3df09eba77a
--- /dev/null
+++ b/tests/language/sound_flow_analysis/try_finally_layering_disabled_test.dart
@@ -0,0 +1,184 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+// Tests how flow analysis layers promotions from `try` and `finally` blocks
+// when `sound-flow-analysis` is disabled.
+
+// @dart = 3.8
+
+import '../static_type_helper.dart';
+
+class C {
+  final Object _f;
+  C(this._f);
+}
+
+// For local variables that are not assigned in the `try` block, promotions in
+// the `try` block are layered over promotions in the `finally` block.
+void testUnassignedLocal(bool b, Object x, Object y) {
+  if (b) {
+    x as num;
+    y as num;
+    // The promotion chains for `x` and `y` are both `[num]`.
+    x.expectStaticType<Exactly<num>>();
+    y.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      x as num;
+      y as int;
+      x.expectStaticType<Exactly<num>>();
+      y.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x` nor `y` is promoted at this point, because in principle an
+      // exception could have occurred at any point in the `try` block.
+      x.expectStaticType<Exactly<Object>>();
+      y.expectStaticType<Exactly<Object>>();
+      x as int;
+      y as num;
+    }
+    // After the try/finally, both `x` and `y` are fully promoted to `int`.
+    x.expectStaticType<Exactly<int>>();
+    y.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `try` block are layered over the
+    // promotions from the `finally` block, `x` has promotion chain `[int]`,
+    // whereas `y` has promotion chain `[num, int]`. Therefore, after the `if`
+    // and `else` control flow paths are joined...
+  }
+  // `x` is no longer promoted at all (since `[num]` and `[int]` have no types
+  // in common), whereas `y` is promoted to `num` (since `[num]` and `[num,
+  // int]` both contain the type `num`).
+  x.expectStaticType<Exactly<Object>>();
+  y.expectStaticType<Exactly<num>>();
+}
+
+// For local variables that are assigned in the `try` block, promotions in the
+// `try` block are layered over promotions in the `finally` block.
+void testAssignedLocal(bool b, Object x, Object y) {
+  if (b) {
+    x as num;
+    y as num;
+    // The promotion chains for `x` and `y` are both `[num]`.
+    x.expectStaticType<Exactly<num>>();
+    y.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      (x, y) = (y, x);
+      x as num;
+      y as int;
+      x.expectStaticType<Exactly<num>>();
+      y.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x` nor `y` is promoted at this point, because in principle an
+      // exception could have occurred at any point in the `try` block.
+      x.expectStaticType<Exactly<Object>>();
+      y.expectStaticType<Exactly<Object>>();
+      x as int;
+      y as num;
+    }
+    // After the try/finally, both `x` and `y` are fully promoted to `int`.
+    x.expectStaticType<Exactly<int>>();
+    y.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `try` block are layered over the
+    // promotions from the `finally` block, `x` has promotion chain `[int]`,
+    // whereas `y` has promotion chain `[num, int]`. Therefore, after the `if`
+    // and `else` control flow paths are joined...
+  }
+  // `x` is no longer promoted at all (since `[num]` and `[int]` have no types
+  // in common), whereas `y` is promoted to `num` (since `[num]` and `[num,
+  // int]` both contain the type `num`).
+  x.expectStaticType<Exactly<Object>>();
+  y.expectStaticType<Exactly<num>>();
+}
+
+// For fields of local variables that are not assigned in the `try` block,
+// promotions in the `try` block are layered over promotions in the `finally`
+// block.
+void testUnassignedField(bool b, C x, C y) {
+  if (b) {
+    x._f as num;
+    y._f as num;
+    // The promotion chains for `x._f` and `y._f` are both `[num]`.
+    x._f.expectStaticType<Exactly<num>>();
+    y._f.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      x._f as num;
+      y._f as int;
+      x._f.expectStaticType<Exactly<num>>();
+      y._f.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x._f` nor `y._f` is promoted at this point, because in
+      // principle an exception could have occurred at any point in the `try`
+      // block.
+      x._f.expectStaticType<Exactly<Object>>();
+      y._f.expectStaticType<Exactly<Object>>();
+      x._f as int;
+      y._f as num;
+    }
+    // After the try/finally, both `x._f` and `y._f` are fully promoted to
+    // `int`.
+    x._f.expectStaticType<Exactly<int>>();
+    y._f.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `try` block are layered over the
+    // promotions from the `finally` block, `x._f` has promotion chain `[int]`,
+    // whereas `y._f` has promotion chain `[num, int]`. Therefore, after the
+    // `if` and `else` control flow paths are joined...
+  }
+  // `x._f` is no longer promoted at all (since `[num]` and `[int]` have no
+  // types in common), whereas `y._f` is promoted to `num` (since `[num]` and
+  // `[num, int]` both contain the type `num`).
+  x._f.expectStaticType<Exactly<Object>>();
+  y._f.expectStaticType<Exactly<num>>();
+}
+
+// For fields of local variables that are assigned in the `try` block,
+// promotions in the `finally` block are layered over promotions in the `try`
+// block.
+void testAssignedField(bool b, C x, C y) {
+  if (b) {
+    x._f as num;
+    y._f as num;
+    // The promotion chains for `x._f` and `y._f` are both `[num]`.
+    x._f.expectStaticType<Exactly<num>>();
+    y._f.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      (x, y) = (y, x);
+      x._f as num;
+      y._f as int;
+      x._f.expectStaticType<Exactly<num>>();
+      y._f.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x._f` nor `y._f` is promoted at this point, because in
+      // principle an exception could have occurred at any point in the `try`
+      // block.
+      x._f.expectStaticType<Exactly<Object>>();
+      y._f.expectStaticType<Exactly<Object>>();
+      x._f as int;
+      y._f as num;
+    }
+    // After the try/finally, both `x._f` and `y._f` are fully promoted to
+    // `int`.
+    x._f.expectStaticType<Exactly<int>>();
+    y._f.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `finally` block are layered over the
+    // promotions from the `try` block, `x._f` has promotion chain `[num, int]`,
+    // whereas `y._f` has promotion chain `[int]`. Therefore, after the `if` and
+    // `else` control flow paths are joined...
+  }
+  // `x._f` is promoted to `num` (since `[num]` and `[num, int]` both contain
+  // the type `num`), whereas `y._f` is no longer promoted at all (since `[num]`
+  // and `[int]` have no types in common).
+  x._f.expectStaticType<Exactly<num>>();
+  y._f.expectStaticType<Exactly<Object>>();
+}
+
+main() {
+  for (var b in [false, true]) {
+    testUnassignedLocal(b, 0, 0);
+    testAssignedLocal(b, 0, 0);
+    testUnassignedField(b, C(0), C(0));
+    testAssignedField(b, C(0), C(0));
+  }
+}
diff --git a/tests/language/sound_flow_analysis/try_finally_layering_test.dart b/tests/language/sound_flow_analysis/try_finally_layering_test.dart
new file mode 100644
index 00000000000..526fbb5ca4d
--- /dev/null
+++ b/tests/language/sound_flow_analysis/try_finally_layering_test.dart
@@ -0,0 +1,184 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+// Tests how flow analysis layers promotions from `try` and `finally` blocks
+// when `sound-flow-analysis` is enabled.
+
+// SharedOptions=--enable-experiment=sound-flow-analysis
+
+import '../static_type_helper.dart';
+
+class C {
+  final Object _f;
+  C(this._f);
+}
+
+// For local variables that are not assigned in the `try` block, promotions in
+// the `finally` block are layered over promotions in the `try` block.
+void testUnassignedLocal(bool b, Object x, Object y) {
+  if (b) {
+    x as num;
+    y as num;
+    // The promotion chains for `x` and `y` are both `[num]`.
+    x.expectStaticType<Exactly<num>>();
+    y.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      x as num;
+      y as int;
+      x.expectStaticType<Exactly<num>>();
+      y.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x` nor `y` is promoted at this point, because in principle an
+      // exception could have occurred at any point in the `try` block.
+      x.expectStaticType<Exactly<Object>>();
+      y.expectStaticType<Exactly<Object>>();
+      x as int;
+      y as num;
+    }
+    // After the try/finally, both `x` and `y` are fully promoted to `int`.
+    x.expectStaticType<Exactly<int>>();
+    y.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `finally` block are layered over the
+    // promotions from the `try` block, `x` has promotion chain `[num, int]`,
+    // whereas `y` has promotion chain `[int]`. Therefore, after the `if` and
+    // `else` control flow paths are joined...
+  }
+  // `x` is promoted to `num` (since `[num]` and `[num, int]` both contain the
+  // type `num`), whereas `y` is no longer promoted at all (since `[num]` and
+  // `[int]` have no types in common).
+  x.expectStaticType<Exactly<num>>();
+  y.expectStaticType<Exactly<Object>>();
+}
+
+// For local variables that are assigned in the `try` block, promotions in the
+// `finally` block are layered over promotions in the `try` block.
+void testAssignedLocal(bool b, Object x, Object y) {
+  if (b) {
+    x as num;
+    y as num;
+    // The promotion chains for `x` and `y` are both `[num]`.
+    x.expectStaticType<Exactly<num>>();
+    y.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      (x, y) = (y, x);
+      x as num;
+      y as int;
+      x.expectStaticType<Exactly<num>>();
+      y.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x` nor `y` is promoted at this point, because in principle an
+      // exception could have occurred at any point in the `try` block.
+      x.expectStaticType<Exactly<Object>>();
+      y.expectStaticType<Exactly<Object>>();
+      x as int;
+      y as num;
+    }
+    // After the try/finally, both `x` and `y` are fully promoted to `int`.
+    x.expectStaticType<Exactly<int>>();
+    y.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `finally` block are layered over the
+    // promotions from the `try` block, `x` has promotion chain `[num, int]`,
+    // whereas `y` has promotion chain `[int]`. Therefore, after the `if` and
+    // `else` control flow paths are joined...
+  }
+  // `x` is promoted to `num` (since `[num]` and `[num, int]` both contain the
+  // type `num`), whereas `y` is no longer promoted at all (since `[num]` and
+  // `[int]` have no types in common).
+  x.expectStaticType<Exactly<num>>();
+  y.expectStaticType<Exactly<Object>>();
+}
+
+// For fields of local variables that are not assigned in the `try` block,
+// promotions in the `finally` block are layered over promotions in the `try`
+// block.
+void testUnassignedField(bool b, C x, C y) {
+  if (b) {
+    x._f as num;
+    y._f as num;
+    // The promotion chains for `x._f` and `y._f` are both `[num]`.
+    x._f.expectStaticType<Exactly<num>>();
+    y._f.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      x._f as num;
+      y._f as int;
+      x._f.expectStaticType<Exactly<num>>();
+      y._f.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x._f` nor `y._f` is promoted at this point, because in
+      // principle an exception could have occurred at any point in the `try`
+      // block.
+      x._f.expectStaticType<Exactly<Object>>();
+      y._f.expectStaticType<Exactly<Object>>();
+      x._f as int;
+      y._f as num;
+    }
+    // After the try/finally, both `x._f` and `y._f` are fully promoted to
+    // `int`.
+    x._f.expectStaticType<Exactly<int>>();
+    y._f.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `finally` block are layered over the
+    // promotions from the `try` block, `x._f` has promotion chain `[num, int]`,
+    // whereas `y._f` has promotion chain `[int]`. Therefore, after the `if` and
+    // `else` control flow paths are joined...
+  }
+  // `x._f` is promoted to `num` (since `[num]` and `[num, int]` both contain
+  // the type `num`), whereas `y._f` is no longer promoted at all (since `[num]`
+  // and `[int]` have no types in common).
+  x._f.expectStaticType<Exactly<num>>();
+  y._f.expectStaticType<Exactly<Object>>();
+}
+
+// For fields of local variables that are assigned in the `try` block,
+// promotions in the `finally` block are layered over promotions in the `try`
+// block.
+void testAssignedField(bool b, C x, C y) {
+  if (b) {
+    x._f as num;
+    y._f as num;
+    // The promotion chains for `x._f` and `y._f` are both `[num]`.
+    x._f.expectStaticType<Exactly<num>>();
+    y._f.expectStaticType<Exactly<num>>();
+  } else {
+    try {
+      (x, y) = (y, x);
+      x._f as num;
+      y._f as int;
+      x._f.expectStaticType<Exactly<num>>();
+      y._f.expectStaticType<Exactly<int>>();
+    } finally {
+      // Neither `x._f` nor `y._f` is promoted at this point, because in
+      // principle an exception could have occurred at any point in the `try`
+      // block.
+      x._f.expectStaticType<Exactly<Object>>();
+      y._f.expectStaticType<Exactly<Object>>();
+      x._f as int;
+      y._f as num;
+    }
+    // After the try/finally, both `x._f` and `y._f` are fully promoted to
+    // `int`.
+    x._f.expectStaticType<Exactly<int>>();
+    y._f.expectStaticType<Exactly<int>>();
+    // But since the promotions from the `finally` block are layered over the
+    // promotions from the `try` block, `x._f` has promotion chain `[num, int]`,
+    // whereas `y._f` has promotion chain `[int]`. Therefore, after the `if` and
+    // `else` control flow paths are joined...
+  }
+  // `x._f` is promoted to `num` (since `[num]` and `[num, int]` both contain
+  // the type `num`), whereas `y._f` is no longer promoted at all (since `[num]`
+  // and `[int]` have no types in common).
+  x._f.expectStaticType<Exactly<num>>();
+  y._f.expectStaticType<Exactly<Object>>();
+}
+
+main() {
+  for (var b in [false, true]) {
+    testUnassignedLocal(b, 0, 0);
+    testAssignedLocal(b, 0, 0);
+    testUnassignedField(b, C(0), C(0));
+    testAssignedField(b, C(0), C(0));
+  }
+}