diff --git a/theories/tests/memcpy.v b/theories/tests/memcpy.v
index e21e7bc33235ee0d1674e23c20e245c2ce79639d..a4707f902600169e65562214e7c0ae92decf152b 100644
--- a/theories/tests/memcpy.v
+++ b/theories/tests/memcpy.v
@@ -23,7 +23,7 @@ Section memcpy.
     qq ↦C cloc_to_val q -∗
     AWP whileᶜ (∗ᶜ (a_ret (cloc_to_val pp)) <∗ᶜ a_ret (cloc_to_val (cloc_plus p n)))
        { (a_ret (cloc_to_val pp) +∗=ᶜ ♯1) =ᶜ (∗ᶜ (a_ret (cloc_to_val qq) +∗=ᶜ ♯1)) }
-      @ R {{ _, p ↦C∗ ls2 ∗ q ↦C∗ ls2 }}.
+      @ R {{ _, p ↦C∗ ls2 ∗ q ↦C∗ ls2 ∗ pp ↦C cloc_to_val p ∗ qq ↦C cloc_to_val q }}.
   Proof.
     iIntros (Hlen1 Hlen2) "Hp Hq Hpp Hqq".
     simplify_eq/=.