diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 9915457b0172f7bddab3b036778dea7d4257f637..d1b711e531c46edbd92e9f838066f3f3337d2280 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -56,6 +56,11 @@ Section iris_tests.
   Context `{!invGS_gen hlc Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
+  Lemma test_except_0_inv N P : ▷ False -∗ inv N P.
+  Proof.
+    iIntros "H". by iMod "H". (* works because invariants are [IsExcept0] *)
+  Qed.
+
   Lemma test_masks  N E P Q R :
     ↑N ⊆ E →
     (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.