diff --git a/TypeSystem/flow-analysis/reachability_A12_t01.dart b/TypeSystem/flow-analysis/reachability_A12_t01.dart
new file mode 100644
index 0000000000..a6b33985f1
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A12_t01.dart
@@ -0,0 +1,26 @@
+// 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.
+
+/// @assertion instance check If `N` is an expression of the form `E1 is S`
+/// where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - Let `true(N) = promote(E1, S, after(E1))`
+/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is S`
+/// `true(N) = promote(E1, S, after(E1))` and
+/// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
+/// the case `T` is `R?` and `Null <: S`.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+main() {
+  int? i = 2 > 1 ? null : 42;
+  if (i is Null) {
+    Null n = i;
+  } else {
+    i.expectStaticType<Exactly<int>>();
+  }
+}
diff --git a/TypeSystem/flow-analysis/reachability_A12_t02.dart b/TypeSystem/flow-analysis/reachability_A12_t02.dart
new file mode 100644
index 0000000000..b0df00ef5f
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A12_t02.dart
@@ -0,0 +1,26 @@
+// 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.
+
+/// @assertion instance check If `N` is an expression of the form `E1 is S`
+/// where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - Let `true(N) = promote(E1, S, after(E1))`
+/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is S`
+/// `true(N) = promote(E1, S, after(E1))` and
+/// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
+/// the case `T` is `R?` and `S` is not subtype of `Null`.
+/// @author sgrekhov22@gmail.com
+
+import '../../Utils/static_type_helper.dart';
+
+main() {
+  int? i = 2 > 1 ? null : 42;
+  if (i is int) {
+    i.expectStaticType<Exactly<int>>();
+  } else {
+    i.expectStaticType<Exactly<Null>>();
+  }
+}
diff --git a/TypeSystem/flow-analysis/reachability_A12_t03.dart b/TypeSystem/flow-analysis/reachability_A12_t03.dart
new file mode 100644
index 0000000000..0163cefa70
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A12_t03.dart
@@ -0,0 +1,33 @@
+// 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.
+
+/// @assertion instance check If `N` is an expression of the form `E1 is S`
+/// where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - Let `true(N) = promote(E1, S, after(E1))`
+/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is S`
+/// `true(N) = promote(E1, S, after(E1))` and
+/// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
+/// the case `T` is `FutureOr<R>` and `Future<R> <: S`.
+/// @author sgrekhov22@gmail.com
+
+import 'dart:async';
+import '../../Utils/static_type_helper.dart';
+
+class C {}
+
+test(FutureOr<C> foc) async {
+  if (foc is Future<C>) {
+    foc.expectStaticType<Exactly<Future<C>>>();
+  } else {
+    foc.expectStaticType<Exactly<C>>();
+  }
+}
+
+main() {
+  test(C());
+  test(Future<C>.value(C()));
+}
diff --git a/TypeSystem/flow-analysis/reachability_A12_t04.dart b/TypeSystem/flow-analysis/reachability_A12_t04.dart
new file mode 100644
index 0000000000..563660c61f
--- /dev/null
+++ b/TypeSystem/flow-analysis/reachability_A12_t04.dart
@@ -0,0 +1,33 @@
+// 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.
+
+/// @assertion instance check If `N` is an expression of the form `E1 is S`
+/// where the static type of `E1` is `T` then:
+/// - Let `before(E1) = before(N)`
+/// - Let `true(N) = promote(E1, S, after(E1))`
+/// - Let `false(N) = promote(E1, factor(T, S), after(E1))`
+///
+/// @description Checks that for expression of the form `E1 is S`
+/// `true(N) = promote(E1, S, after(E1))` and
+/// `false(N) = promote(E1, factor(T, S), after(E1))`. Test `factor(T, S)` for
+/// the case `T` is `FutureOr<R>` and `R <: S`.
+/// @author sgrekhov22@gmail.com
+
+import 'dart:async';
+import '../../Utils/static_type_helper.dart';
+
+class C {}
+
+test(FutureOr<C> foc) async {
+  if (foc is C) {
+    foc.expectStaticType<Exactly<C>>();
+  } else {
+    foc.expectStaticType<Exactly<Future<C>>>();
+  }
+}
+
+main() {
+  test(C());
+  test(Future<C>.value(C()));
+}