diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 64e37382064e716331fc28ad29f4b1d9f4bea613..e61cca8e1e6d475d17e33bda8a885296814b785d 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -267,6 +267,37 @@ goal 2 is:
 --------------------------------------∗
 WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 
+"xchg_example"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  v₁, v₂ : val
+  Φ : val → iPropI Σ
+  ============================
+  "Hl" : l ↦ v₂
+  "HΦ" : l ↦ v₂ -∗ Φ v₁
+  --------------------------------------∗
+  |={⊤}=> Φ v₁
+  
+1 goal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  N : namespace
+  l : loc
+  v : val
+  Φ : language.val heap_lang → iPropI Σ
+  v' : val
+  ============================
+  "HΦ" : ∀ v'0 : language.val heap_lang, True -∗ Φ v'0
+  "Hl" : l ↦ v
+  "Hclose" : ▷ (∃ v0 : val, l ↦ v0) ={⊤ ∖ ↑N,⊤}=∗ emp
+  --------------------------------------∗
+  |={⊤ ∖ ↑N,⊤}=> Φ v'
+  
 1 goal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index a05b855a233e2906283cd485d5c8076b3f2b894b..458755adedb4bfa33a7e31e5d0d38f94793ad1c8 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -333,7 +333,7 @@ Section mapsto_tests.
   (* Loading from the general mapsto for any [dfrac]. *)
   Lemma general_mapsto dq l v :
     [[{ l ↦{dq} v }]] ! #l [[{ RET v; True }]].
-  Proof. 
+  Proof.
     iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
   Qed.
 
@@ -382,6 +382,30 @@ Section atomic.
     (* Test if a side-condition for [Atomic] is generated *)
     iIntros (?) "H". iInv "H" as "H". Show.
   Abort.
+
+  Check "xchg_example".
+
+  Lemma xchg_example l (v₁ v₂ : val) :
+    {{{ l ↦ v₁ }}}
+      Xchg #l vâ‚‚
+    {{{ RET v₁; l ↦ v₂ }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ".
+    wp_xchg.
+    Show.
+  Abort.
+
+  Lemma xchg_inv_example N l (v : val) :
+    {{{ inv N (∃ v, l ↦ v) }}}
+      Xchg #l v
+    {{{ v', RET v'; True }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ".
+    iInv "Hl" as (v') "Hl" "Hclose".
+    wp_xchg.
+    Show.
+  Abort.
+
 End atomic.
 
 Section printing_tests.