diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index fd5ebf4ad2b5dcbe3a0c68e1f7b4e23c3fc05d7f..d034829324d7d278312e82243c02984f9aaa0348 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -752,3 +752,11 @@ Tactic failure: iPure: (φ n) not pure.
      : string
 The command has indeed failed with message:
 Tactic failure: iIntuitionistic: Q not persistent.
+"test_iDestruct_intuitionistic_not_fresh"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntuitionistic: "H" not fresh.
+"test_iDestruct_spatial_not_fresh"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpatial: "H" not fresh.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7b2ac9d6b43f5e839bc98a4a6fe94f0386b0139f..fa820d1ff2c0bfdc1630ae6c78d5a5de9049069b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1650,4 +1650,18 @@ Proof.
   auto.
 Qed.
 
+Check "test_iDestruct_intuitionistic_not_fresh".
+Lemma test_iDestruct_intuitionistic_not_fresh P Q :
+  P -∗ □ Q -∗ False.
+Proof.
+  iIntros "H H'". Fail iDestruct "H'" as "#H".
+Abort.
+
+Check "test_iDestruct_spatial_not_fresh".
+Lemma test_iDestruct_spatial_not_fresh P Q :
+  P -∗ Q -∗ False.
+Proof.
+  iIntros "H H'". Fail iDestruct "H'" as "-#H".
+Abort.
+
 End tactic_tests.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index f7d43a2cc857cd80d4cce0f9281468d4b63c0a27..4c4d3a96cccfc31df83059af42080a21c3d91ac8 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -168,6 +168,10 @@ Tactic failure: iInv: invariant "H2" not found.
   "H" : own γ 1%Qp
   --------------------------------------∗
   own γ 1%Qp
+"test_iDestruct_mod_not_fresh"
+     : string
+The command has indeed failed with message:
+Tactic failure: iMod: "H" not fresh.
 "test_iInv"
      : string
 1 goal
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 89ac3f55660d78d58e5e23cdb9bf9f0bb72509bc..466099cd2894d91d28bf7bbd46a8d71ba42a314c 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -243,6 +243,13 @@ Section iris_tests.
     iExact "H".
   Qed.
 
+  Check "test_iDestruct_mod_not_fresh".
+  Lemma test_iDestruct_mod_not_fresh P Q :
+    P -∗ (|={⊤}=> Q) -∗ (|={⊤}=> False).
+  Proof.
+    iIntros "H H'". Fail iDestruct "H'" as ">H".
+  Abort.
+
 End iris_tests.
 
 Section monpred_tests.