diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index d9ab16e89b60ad8eaf85a22679e003574e15645e..36c1f6342dab48e53a6a0b26d272a24f0cfa8b13 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1007,7 +1007,9 @@ Ltac iSpecializePat_go H1 pats :=
             [notypeclasses refine (tac_unlock_emp _ _ _)
             |notypeclasses refine (tac_unlock_True _ _ _)
             |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
-            |fail "iSpecialize: premise cannot be solved by framing"]
+            |let P :=
+               match goal with |- envs_entails _ (?P ∗ locked _)%I => P end in
+             fail 1 "iSpecialize: premise" P "cannot be solved by framing"]
          |exact eq_refl]; iIntro H1; iSpecializePat_go H1 pats
     end.
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index e2b369c4abd8dbdd091ec270f0f40a053b0a100a..fd5ebf4ad2b5dcbe3a0c68e1f7b4e23c3fc05d7f 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -549,6 +549,18 @@ Tactic failure: iSpecialize: "H" not found.
      : string
 The command has indeed failed with message:
 Tactic failure: iSpecialize: "H" not found.
+"iSpecialize_autoframe_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpecialize: premise P cannot be solved by framing.
+The command has indeed failed with message:
+Tactic failure: iSpecialize: premise P cannot be solved by framing.
+"iSpecialize_autoframe_fail2"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpecialize: premise Q cannot be solved by framing.
+The command has indeed failed with message:
+Tactic failure: iSpecialize: premise Q cannot be solved by framing.
 "iExact_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 03b44f242cce64a05a09000da3b14566dd5e92b6..31cc46faa14e1b1d2bf74238b14435a34b6fd889 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1305,6 +1305,22 @@ Proof.
   iIntros "HW HP". Fail iSpecialize ("HW" with "H").
 Abort.
 
+Check "iSpecialize_autoframe_fail".
+Lemma iSpecialize_autoframe_fail P Q : (P -∗ Q) -∗ Q.
+Proof.
+  iIntros "H".
+  Fail iSpecialize ("H" with "[$]").
+  Fail iApply ("H" with "[$]").
+Abort.
+
+Check "iSpecialize_autoframe_fail2".
+Lemma iSpecialize_autoframe_fail2 P Q R : (P -∗ Q -∗ R) -∗ P -∗ R.
+Proof.
+  iIntros "H HP".
+  Fail iSpecialize ("H" with "[$] [$]").
+  Fail iApply ("H" with "[$] [$]").
+Abort.
+
 Check "iExact_fail".
 Lemma iExact_fail P Q :
   <affine> P -∗ Q -∗ <affine> P.