diff --git a/test/Fail/TypeBasedTermination/Issue7269.agda b/test/Fail/TypeBasedTermination/Issue7269.agda
new file mode 100644
index 00000000000..92f3341fda5
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7269.agda
@@ -0,0 +1,14 @@
+-- Andreas, 2024-05-16, issue #7269
+-- --no-syntax-based-termination should not turn on --type-based-termination
+
+{-# OPTIONS --no-type-based-termination #-}
+{-# OPTIONS --no-syntax-based-termination #-}  -- Turns on TBT, but should not
+
+record U : Set where
+  coinductive
+  field force : U
+open U
+
+-- This should not pass since no termination checker is on.
+u : U
+u .force = u
diff --git a/test/Fail/TypeBasedTermination/Issue7269.err b/test/Fail/TypeBasedTermination/Issue7269.err
new file mode 100644
index 00000000000..1e73df3345c
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7269.err
@@ -0,0 +1 @@
+AGDA_FAIL
\ No newline at end of file
diff --git a/test/Fail/TypeBasedTermination/Issue7270.agda b/test/Fail/TypeBasedTermination/Issue7270.agda
new file mode 100644
index 00000000000..8956c5ce768
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7270.agda
@@ -0,0 +1,21 @@
+-- Andreas, 2024-05-16, issue #7270
+
+{-# OPTIONS --type-based-termination #-}
+
+record U : Set where
+  coinductive
+  field force : U
+open U
+
+postulate d : U → U
+
+-- f is classified as size preserving, but is not, since d is unknown
+-- Counterexamples: d = id; d u = u .force
+--
+f : U → U
+f u = d u .force
+
+-- This should not pass:
+--
+u : U
+u .force = f u
diff --git a/test/Fail/TypeBasedTermination/Issue7270.err b/test/Fail/TypeBasedTermination/Issue7270.err
new file mode 100644
index 00000000000..1e73df3345c
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7270.err
@@ -0,0 +1 @@
+AGDA_FAIL
\ No newline at end of file
diff --git a/test/Fail/TypeBasedTermination/Issue7271.agda b/test/Fail/TypeBasedTermination/Issue7271.agda
new file mode 100644
index 00000000000..92cbef3e92e
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7271.agda
@@ -0,0 +1,32 @@
+-- Andreas, 2024-05-16, issue #7271.
+-- Bug in size-preservation checker.
+
+{-# OPTIONS --type-based-termination #-}
+
+data ⊥ : Set where
+
+record _×_ (A B : Set) : Set where
+  field
+    fst : A
+    snd : B
+open _×_
+
+-- Empty stream type.
+--
+record S : Set where
+  coinductive; constructor delay
+  field force : ⊥ × S
+open S
+
+-- This is not size-preserving:
+--
+f : S → ⊥ × S
+f s = s' .force where s' = s
+
+-- This should not be accepted:
+--
+s : S
+s .force = f s
+
+absurd : ⊥
+absurd = s .force .fst
diff --git a/test/Fail/TypeBasedTermination/Issue7271.err b/test/Fail/TypeBasedTermination/Issue7271.err
new file mode 100644
index 00000000000..1e73df3345c
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7271.err
@@ -0,0 +1 @@
+AGDA_FAIL
\ No newline at end of file
diff --git a/test/Fail/TypeBasedTermination/Issue7271With.agda b/test/Fail/TypeBasedTermination/Issue7271With.agda
new file mode 100644
index 00000000000..3e856debc9a
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7271With.agda
@@ -0,0 +1,33 @@
+-- Andreas, 2024-05-16, issue #7271.
+-- Bug in size-preservation checker.
+
+{-# OPTIONS --type-based-termination #-}
+
+data ⊥ : Set where
+
+record _×_ (A B : Set) : Set where
+  field
+    fst : A
+    snd : B
+open _×_
+
+-- Empty stream type.
+--
+record S : Set where
+  coinductive; constructor delay
+  field force : ⊥ × S
+open S
+
+-- This is not size-preserving:
+--
+f : S → ⊥ × S
+f s with s
+... | s' = s' .force
+
+-- This should not be accepted:
+--
+s : S
+s .force = f s
+
+absurd : ⊥
+absurd = s .force .fst
diff --git a/test/Fail/TypeBasedTermination/Issue7271With.err b/test/Fail/TypeBasedTermination/Issue7271With.err
new file mode 100644
index 00000000000..1e73df3345c
--- /dev/null
+++ b/test/Fail/TypeBasedTermination/Issue7271With.err
@@ -0,0 +1 @@
+AGDA_FAIL
\ No newline at end of file