diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
index 72d993e6edd828a9eea57821bd958bd2ea54f7ac..a3f9185273b897d0d0eebbbde3e4ec0a5bd52004 100644
--- a/tests/atomic.8.8.ref
+++ b/tests/atomic.8.8.ref
@@ -1,3 +1,17 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  aheap : atomic_heap Σ
+  Q : iProp Σ
+  l : loc
+  v : val
+  ============================
+  "Hl" : l ↦ v
+  --------------------------------------∗
+  AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
+       << l ↦{q} v0, COMM Q -∗ Q >>
+  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 0005668844f7627ae6f7e6f474e7907bbff93473..236ec1e71c6f641b70281fc407182ab11ac2d497 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,9 +1,22 @@
 From iris.heap_lang Require Export lifting notation.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 
+Section tests.
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Import atomic_heap.notation.
+
+  (* FIXME: removing the `val` type annotation breaks printing. *)
+  Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
+    Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
+  Proof.
+    iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
+    iAaccIntro with "Hl"; eauto with iFrame.
+  Qed.
+End tests.
+
 (* Test if AWP and the AU obtained from AWP print. *)
 Section printing.
   Context `{!heapG Σ}.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index e9e83a10bb8c82ecda2c1728ef796d0926ecfcd1..f46b92465981cfa67f8c38b7c44a5dc529cd5b89 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -246,7 +246,7 @@ Lemma wp_frame_wand_l s E e Q Φ :
 Proof.
   iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
   iIntros (v) "HΦ". by iApply "HΦ".
-Qed. 
+Qed.
 
 End wp.