diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 942c1aa93ebedde7266e52785607866515f6f2b5..b4ac2c10a5b6822a67b8883062addc91665b61a3 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -18,6 +18,38 @@
   --------------------------------------∗
   WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
   
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  E : coPset
+  l : loc
+  ============================
+  "Hl" : l ↦ #1
+  --------------------------------------∗
+  WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
+  @ E [{ v, ⌜v = #2⌝ }]
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  l : loc
+  ============================
+  "Hl1" : l ↦{1 / 2} #0
+  "Hl2" : l ↦{1 / 2} #0
+  --------------------------------------∗
+  True
+  
+1 subgoal
+  
+  Σ : gFunctors
+  H : heapG Σ
+  l : loc
+  ============================
+  --------------------------------------∗
+  True
+  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 0d93617243d23e00a0f86e06747292644b30a9e3..dd4a53e4e7a1d1f5488298966329db92fbad2d13 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -27,7 +27,7 @@ Section tests.
   Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
   Proof.
     iIntros "". rewrite /heap_e. Show.
-    wp_alloc l. wp_let. wp_load. Show.
+    wp_alloc l as "?". wp_let. wp_load. Show.
     wp_op. wp_store. by wp_load.
   Qed.
 
@@ -39,7 +39,7 @@ Section tests.
   Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, ⌜v = #2⌝ }]%I.
   Proof.
     iIntros "". rewrite /heap_e2.
-    wp_alloc l. wp_let. wp_alloc l'. wp_let.
+    wp_alloc l as "Hl". Show. wp_let. wp_alloc l'. wp_let.
     wp_load. wp_op. wp_store. wp_load. done.
   Qed.
 
@@ -123,6 +123,14 @@ Section tests.
     iIntros (?) "?". wp_cas as ? | ?. done. done.
   Qed.
 
+  Lemma wp_alloc_split :
+    WP Alloc #0 {{ _, True }}%I.
+  Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
+
+  Lemma wp_alloc_drop :
+    WP Alloc #0 {{ _, True }}%I.
+  Proof. wp_alloc l as "_". Show. done. Qed.
+
 End tests.
 
 Section printing_tests.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 15c2f92de46d3170ff944e44fbaa2657d52cd008..fe8a81c37912c9fed184b9b37957fc36cf21e6c4 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -360,31 +360,32 @@ Tactic Notation "wp_apply" open_constr(lem) :=
     end).
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
+  let Htmp := iFresh in
   let finish _ :=
     first [intros l | fail 1 "wp_alloc:" l "not fresh"];
       eexists; split;
         [pm_reflexivity || fail "wp_alloc:" H "not fresh"
-        |wp_expr_simpl; try wp_value_head] in
+        |iDestruct Htmp as H; wp_expr_simpl; try wp_value_head] in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_alloc _ _ _ _ H K); [iSolveTC|..])
+         eapply (tac_wp_alloc _ _ _ _ Htmp K); [iSolveTC|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     [iSolveTC
     |finish ()]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_twp_alloc _ _ _ H K); [iSolveTC|..])
+         eapply (tac_twp_alloc _ _ _ Htmp K); [iSolveTC|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     finish ()
   | _ => fail "wp_alloc: not a 'wp'"
   end.
 
 Tactic Notation "wp_alloc" ident(l) :=
-  let H := iFresh in wp_alloc l as H.
+  wp_alloc l as "?".
 
 Tactic Notation "wp_load" :=
   let solve_mapsto _ :=