diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index aa433d1c85eb29566bb916f268d57487f0ed73de..910aedffc26320790c682c299c5fa5f129b9ab76 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -311,6 +311,10 @@ Proof.
   done.
 Qed.
 
+Lemma test_iNext_fail P Q a b c d e f g h i j:
+  ▷^(a + b) ▷^(c + d + e) P -∗ ▷^(f + g + h + i + j) True.
+Proof. iIntros "H". iNext. done. Qed.
+
 Lemma test_iEval x y : ⌜ (y + x)%nat = 1 ⌝ -∗ ⌜ S (x + y) = 2%nat ⌝ : uPred M.
 Proof.
   iIntros (H).