diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 005c8279ba15754868f6be9033376d7f61055957..03b2e892b40437d5f80081bb0a87c7bb56d4bd09 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -433,6 +433,11 @@ Tactic failure: iFrame: cannot frame Q.
   ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
              ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"iStopProof_not_proofmode"
+     : string
+The command has indeed failed with message:
+Ltac call to "iStopProof" failed.
+Tactic failure: iStopProof: proofmode not started.
 "iAlways_spatial_non_empty"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e9c431fea5beb8ba77e3e394aeb56c71706fe6e9..8e52115fd7da796277b199fd5ad24a4a87f54fd1 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -44,6 +44,9 @@ Definition bar : PROP := (∀ P, foo P)%I.
 Lemma test_unfold_constants : bar.
 Proof. iIntros (P) "HP //". Qed.
 
+Lemma test_iStopProof Q : emp -∗ Q -∗ Q.
+Proof. iIntros "#H1 H2". iStopProof. by rewrite bi.sep_elim_r. Qed.
+
 Lemma test_iRewrite {A : ofeT} (x y : A) P :
   □ (∀ z, P -∗ <affine> (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
 Proof.
@@ -765,6 +768,10 @@ Section error_tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
+Check "iStopProof_not_proofmode".
+Lemma iStopProof_not_proofmode : 10 = 10.
+Proof. Fail iStopProof. Abort.
+
 Check "iAlways_spatial_non_empty".
 Lemma iAlways_spatial_non_empty P :
   P -∗ □ emp.