diff --git a/tests/atomic.ref b/tests/atomic.ref
index 6184f371c9cb452e5276630face9bbee9598cc9a..7146b97eacba07167809160248fe52f86fe6892d 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -12,6 +12,17 @@
   AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
        << l ↦{q} v0, COMM Q -∗ Q >>
   
+"non_laterable"
+     : string
+The command has indeed failed with message:
+Tactic failure: iAuIntro: not all spatial assumptions are laterable.
+The command has indeed failed with message:
+Tactic failure: wp_apply: cannot apply
+(<<< ∀ (v : val) (q : Qp), ?Goal ↦{q} v >>>
+   ! #?Goal @ ⊤
+ <<< ?Goal ↦{q} v, RET v >>>).
+"printing"
+     : string
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 6e3b5707708c36a2c59723e04b74956901b3d132..4e69316d0a7253ce02964cf5cb19033b59a4e9e6 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -17,7 +17,24 @@ Section tests.
   Qed.
 End tests.
 
+(* Test if we get reasonable error messages with non-laterable assertions in the context. *)
+Section error.
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Import atomic_heap.notation.
+
+  Check "non_laterable".
+  Lemma non_laterable (P : iProp Σ) (l : loc) :
+    P -∗ WP !#l {{ _, True }}.
+  Proof.
+    iIntros "HP". wp_apply load_spec. Fail iAuIntro.
+  Restart.
+    iIntros "HP". Fail awp_apply load_spec.
+  Abort.
+End error.  
+
+
 (* Test if AWP and the AU obtained from AWP print. *)
+Check "printing".
 Section printing.
   Context `{!heapG Σ}.