diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 8d19418d3e9f263a36b63e9848174f844e820406..80cab8e26b16b0e6f878b71c678dc6de0eb97f88 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -113,6 +113,15 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   l ↦∗{1 / 2} vs ∗ l ↦∗{1 / 2} vs
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  f : val → Prop
+  Heq : ∀ v : val, f v ↔ f #true
+  ============================
+  ⊢ l ↦□ (λ _ : val, f #true)
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 6b88e361c6150d1fec7b32d21c915a084d817de0..1b16d673324966a1ce5b97df13b42fe49392a668 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -220,13 +220,21 @@ Section tests.
 
 End tests.
 
-Section notation_tests.
+Section inv_mapsto_tests.
   Context `{!heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
   Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
-End notation_tests.
+
+  (* Make sure [setoid_rewrite] works. *)
+  Lemma inv_mapsto_setoid_rewrite (l : loc) (f : val → Prop) :
+    (∀ v, f v ↔ f #true) →
+    ⊢ l ↦□ (λ v, f v).
+  Proof.
+    iIntros (Heq). setoid_rewrite Heq. Show.
+  Abort.
+End inv_mapsto_tests.
 
 Section printing_tests.
   Context `{!heapG Σ}.