diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 307e797b204b4be894c7d176bb7400c356a58fbd..005c8279ba15754868f6be9033376d7f61055957 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -706,3 +706,14 @@ The command has indeed failed with message:
 In nested Ltac calls to "iRevert ( (ident) )" and 
 "iForallRevert (ident)", last call failed.
 Tactic failure: iRevert: k is used in hypothesis "Hk".
+"iLöb_no_sbi"
+     : string
+The command has indeed failed with message:
+In nested Ltac calls to "iLöb as (constr)",
+"iLöbRevert (constr) with (tactic3)",
+"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
+"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
+"∗" with tac), "iRevertIntros (constr) with (tactic3)", 
+"iRevertIntros_go", "tac" (bound to iLöbCore as IH), 
+"tac" (bound to iLöbCore as IH) and "iLöbCore as (constr)", last call failed.
+Tactic failure: iLöb: not a step-indexed BI entailment.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index be62f71209eb4454cb2957dacb74e67bab963af0..e9c431fea5beb8ba77e3e394aeb56c71706fe6e9 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -928,3 +928,12 @@ Check "iRevert_dep_var".
 Lemma iRevert_dep_var (k : nat) (Φ : nat → PROP) : Φ k -∗ Φ (S k).
 Proof. iIntros "Hk". Fail iRevert (k). Abort.
 End error_tests.
+
+Section error_tests_bi.
+Context {PROP : bi}.
+Implicit Types P Q R : PROP.
+
+Check "iLöb_no_sbi".
+Lemma iLöb_no_sbi P : P.
+Proof. Fail iLöb as "IH". Abort.
+End error_tests_bi.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 6230733d0ab301e1aa7df4cd35ba91cd02e054b5..72ceda801a7c6c34ddfe6998dea73fc04e38c6d9 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2445,7 +2445,9 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
   (* apply is sometimes confused wrt. canonical structures search.
      refine should use the other unification algorithm, which should
      not have this issue. *)
-  notypeclasses refine (tac_löb _ IH _ _ _);
+  first
+      [notypeclasses refine (tac_löb _ IH _ _ _)
+      |fail 1 "iLöb: not a step-indexed BI entailment"];
     [reflexivity || fail "iLöb: spatial context not empty, this should not happen"
     |pm_reduce;
      lazymatch goal with
@@ -2653,7 +2655,9 @@ Local Ltac iRewriteFindPred :=
 
 Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
   iPoseProofCore lem as true (fun Heq =>
-    eapply (tac_rewrite _ Heq _ _ lr);
+    first
+        [eapply (tac_rewrite _ Heq _ _ lr)
+        |fail 1 "iRewrite: not a step-indexed BI entailment"];
       [pm_reflexivity ||
        let Heq := pretty_ident Heq in
        fail "iRewrite:" Heq "not found"