diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index ef2abff218b916020e2fb5dd7de661babd2feb06..901318923047d2072dca5bd25ce481b9a488cd5a 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -99,7 +99,7 @@ Proof.
   iApply (big_sepL2_impl with "Hwp").
   iIntros "!#" (? e Φ ??) "Hwp".
   destruct (to_val e) as [v2|] eqn:He2'; last done.
-  apply of_to_val in He2' as <-. iApply (wp_value_inv' with "Hwp").
+  apply of_to_val in He2' as <-. simpl. iApply wp_value_fupd'. done.
 Qed.
 End adequacy.
 
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index e1aa91555d668bf9a8203af1bf5861bca5206474..22c0331dbcdcb205cbf30d8f5f8b5e819b56e68a 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -103,10 +103,8 @@ Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
 Qed.
 
-Lemma twp_value' s E Φ v : Φ v -∗ WP of_val v @ s; E [{ Φ }].
-Proof. iIntros "HΦ". rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
-Lemma twp_value_inv' s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}=∗ Φ v.
-Proof. by rewrite twp_unfold /twp_pre to_of_val. Qed.
+Lemma twp_value_fupd' s E Φ v : WP of_val v @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.
+Proof. rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
 
 Lemma twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
   s1 ⊑ s2 → E1 ⊆ E2 →
@@ -151,8 +149,8 @@ Proof.
     + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod (twp_value_inv' with "H") as ">H".
-    iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value'.
+    rewrite twp_value_fupd'. iMod "H" as ">H".
+    iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value_fupd'.
 Qed.
 
 Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
@@ -230,14 +228,12 @@ Global Instance twp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (twp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply twp_mono. Qed.
 
-Lemma twp_value s E Φ e v : IntoVal e v → Φ v -∗ WP e @ s; E [{ Φ }].
-Proof. intros <-. by apply twp_value'. Qed.
-Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }].
-Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
-Lemma twp_value_fupd s E Φ e v : IntoVal e v → (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
-Proof. intros ?. rewrite -twp_fupd -twp_value //. Qed.
-Lemma twp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E [{ Φ }] ={E}=∗ Φ v.
-Proof. intros <-. by apply twp_value_inv'. Qed.
+Lemma twp_value_fupd s E Φ e v : IntoVal e v → WP e @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.
+Proof. intros <-. by apply twp_value_fupd'. Qed.
+Lemma twp_value' s E Φ v : Φ v ⊢ WP (of_val v) @ s; E [{ Φ }].
+Proof. rewrite twp_value_fupd'. auto. Qed.
+Lemma twp_value s E Φ e v : IntoVal e v → Φ v ⊢ WP e @ s; E [{ Φ }].
+Proof. intros <-. apply twp_value'. Qed.
 
 Lemma twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, R ∗ Φ v }].
 Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index a80ee8512f2bf454398fb19b54f2e1203365e9a9..6c510ba6d081890fc0f4d3996d5e875b7ddabbfd 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -90,10 +90,8 @@ Proof.
   by repeat (f_contractive || f_equiv).
 Qed.
 
-Lemma wp_value' s E Φ v : Φ v ⊢ WP of_val v @ s; E {{ Φ }}.
-Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
-Lemma wp_value_inv' s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}=∗ Φ v.
-Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
+Lemma wp_value_fupd' s E Φ v : WP of_val v @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v.
+Proof. rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
 
 Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
   s1 ⊑ s2 → E1 ⊆ E2 →
@@ -138,8 +136,8 @@ Proof.
     + iMod ("H" $! _ [] with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
       by edestruct (atomic _ _ _ _ _ Hstep).
   - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
-    iMod (wp_value_inv' with "H") as ">H".
-    iModIntro. iFrame "Hσ Hefs". by iApply wp_value'.
+    rewrite wp_value_fupd'. iMod "H" as ">H".
+    iModIntro. iFrame "Hσ Hefs". by iApply wp_value_fupd'.
 Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
@@ -207,15 +205,12 @@ Global Instance wp_flip_mono' s E e :
   Proper (pointwise_relation _ (flip (⊢)) ==> (flip (⊢))) (wp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
 
+Lemma wp_value_fupd s E Φ e v : IntoVal e v → WP e @ s; E {{ Φ }} ⊣⊢ |={E}=> Φ v.
+Proof. intros <-. by apply wp_value_fupd'. Qed.
+Lemma wp_value' s E Φ v : Φ v ⊢ WP (of_val v) @ s; E {{ Φ }}.
+Proof. rewrite wp_value_fupd'. auto. Qed.
 Lemma wp_value s E Φ e v : IntoVal e v → Φ v ⊢ WP e @ s; E {{ Φ }}.
-Proof. intros <-. by apply wp_value'. Qed.
-Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ s; E {{ Φ }}.
-Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
-Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
-  (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}.
-Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
-Lemma wp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E {{ Φ }} ={E}=∗ Φ v.
-Proof. intros <-. by apply wp_value_inv'. Qed.
+Proof. intros <-. apply wp_value'. Qed.
 
 Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 40f8387df0c82536d53deb2401e276caad9c7d63..e8d64a3c764b6e845446b2168844b3994dad1232 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -79,7 +79,7 @@ Section proof.
     iIntros (Hvdst Hvsrc Φ) "[Hdst Hsrc] HΦ".
     iInduction vdst as [|v1 vdst] "IH" forall (n dst src vsrc Hvdst Hvsrc);
       destruct vsrc as [|v2 vsrc]; simplify_eq/=; try lia; wp_rec; wp_pures.
-    { iApply "HΦ". iFrame. }
+    { iApply "HΦ". auto with iFrame. }
     iDestruct (array_cons with "Hdst") as "[Hv1 Hdst]".
     iDestruct (array_cons with "Hsrc") as "[Hv2 Hsrc]".
     wp_load; wp_store.
@@ -199,7 +199,7 @@ Section proof.
       { by rewrite /= Z2Nat.id; last lia. }
       { by rewrite loc_add_0. }
       iIntros "!>" (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
-      iApply ("HΦ" $! _ vs). iSplit.
+      iApply ("HΦ" $! _ vs). iModIntro. iSplit.
       { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
       rewrite loc_add_0. iFrame.
     Qed.
@@ -218,7 +218,7 @@ Section proof.
       { by rewrite /= Z2Nat.id; last lia. }
       { by rewrite loc_add_0. }
       iIntros (vs). iDestruct 1 as (Hlen) "[Hl Hvs]". wp_pures.
-      iApply ("HΦ" $! _ vs). iSplit.
+      iApply ("HΦ" $! _ vs). iModIntro. iSplit.
       { iPureIntro. by rewrite Hlen Z2Nat.id; last lia. }
       rewrite loc_add_0. iFrame.
     Qed.
diff --git a/iris_heap_lang/lib/clairvoyant_coin.v b/iris_heap_lang/lib/clairvoyant_coin.v
index e840732bbfcb50fa08eda7d641f65d85af76a940..eedba0d8833a7485383f02a61cf3f95350f76de1 100644
--- a/iris_heap_lang/lib/clairvoyant_coin.v
+++ b/iris_heap_lang/lib/clairvoyant_coin.v
@@ -47,7 +47,7 @@ Section proof.
     wp_alloc c as "Hc".
     wp_pair.
     iApply ("HΦ" $! (#c, #p)%V (b :: prophecy_to_list_bool vs)).
-    rewrite /coin; eauto with iFrame.
+    rewrite /coin; eauto 10 with iFrame.
   Qed.
 
   Lemma read_coin_spec cp bs :
@@ -59,7 +59,7 @@ Section proof.
     iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
     destruct bs as [|b bs]; simplify_eq/=.
     wp_lam. wp_load.
-    iApply "HΦ"; iSplit; first done.
+    iApply "HΦ"; iSplitR; first done.
     rewrite /coin; eauto 10 with iFrame.
   Qed.
 
@@ -78,7 +78,7 @@ Section proof.
     wp_apply (wp_resolve_proph with "[Hp]"); first done.
     iIntros (ws) "[-> Hp]".
     wp_seq.
-    iApply "HΦ"; iSplit; first done.
+    iApply "HΦ"; iSplitR; first done.
     destruct r; rewrite /coin; eauto 10 with iFrame.
   Qed.
 
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index 378b03fcf0552dff46e9d612e154903fd7ec48c9..a40c90c2b0f554873b3796e74fd9a235155461b1 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -59,7 +59,7 @@ Section mono_proof.
       { apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. }
       wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_pures. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
+      wp_pures. iApply "HΦ". iModIntro. iExists γ; repeat iSplit; eauto.
       iApply (own_mono with "Hγf").
       (* FIXME: FIXME(Coq #6294): needs new unification *)
       apply: auth_frag_mono. by apply max_nat_included, le_n_S.
diff --git a/iris_heap_lang/lib/lazy_coin.v b/iris_heap_lang/lib/lazy_coin.v
index 588380e97c42dac16a12d085b897a179ff44d242..cc7fdefdc69621cfc4ba16b5401144c5a95d5030 100644
--- a/iris_heap_lang/lib/lazy_coin.v
+++ b/iris_heap_lang/lib/lazy_coin.v
@@ -63,7 +63,7 @@ Section proof.
       rewrite !prophecy_to_bool_of_bool.
       wp_seq.
       iApply "HΦ".
-      rewrite /coin; eauto with iFrame.
+      rewrite /coin; eauto 10 with iFrame.
   Qed.
 
 End proof.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index a847b985a51807641c25957b52b0b357e3ceae11..5fcfeed6191e751d652e77f639bbaf05e0048f28 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -85,7 +85,7 @@ Section proof.
   Proof.
     iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
     wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
-    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
+    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; auto with iFrame.
     - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
   Qed.
 
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 46b122bfe78b39e854bf3728c25c5b21e15bb07e..9dc2d4622f0bc6413befc8d7bb8fb452a5dc17fe 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -46,17 +46,40 @@ Proof.
   rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
 Qed.
 
-Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
+Lemma tac_wp_value_nofupd `{!heapG Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
 Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
-Lemma tac_twp_value `{!heapG Σ} Δ s E Φ v :
+Lemma tac_twp_value_nofupd `{!heapG Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 
+Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
+  envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
+Proof. rewrite envs_entails_eq=> ->. by rewrite wp_value_fupd. Qed.
+Lemma tac_twp_value `{!heapG Σ} Δ s E Φ v :
+  envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
+Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed.
+
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 
 Ltac wp_value_head :=
-  first [eapply tac_wp_value | eapply tac_twp_value].
+  lazymatch goal with
+  (* If the postcondition already allows a fupd, do not add a second one.
+     But otherwise, *do* add a fupd. This ensures that all the lemmas applied
+     here are bidirectional, so we never will make a goal unprovable. *)
+  | |- envs_entails _ (wp ?s ?E (Val _) (fun _ => fupd ?E _ _)) =>
+      eapply tac_wp_value_nofupd
+  | |- envs_entails _ (wp ?s ?E (Val _) (fun _ => wp _ ?E _ _)) =>
+      eapply tac_wp_value_nofupd
+  | |- envs_entails _ (wp ?s ?E (Val _) _) =>
+      eapply tac_wp_value
+  | |- envs_entails _ (twp ?s ?E (Val _) (fun _ => fupd ?E _ _)) =>
+      eapply tac_twp_value_nofupd
+  | |- envs_entails _ (twp ?s ?E (Val _) (fun _ => twp _ ?E _ _)) =>
+      eapply tac_twp_value_nofupd
+  | |- envs_entails _ (twp ?s ?E (Val _) _) =>
+      eapply tac_twp_value
+  end.
 
 Ltac wp_finish :=
   wp_expr_simpl;      (* simplify occurences of subst/fill *)
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index a3530755c4d23615178cae2731402cfac1a62034..457f073b79d226abe150ab03648fb22948d1e5a7 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -1,3 +1,5 @@
+"heap_e_spec"
+     : string
 1 subgoal
   
   Σ : gFunctors
@@ -18,6 +20,8 @@
   --------------------------------------∗
   WP #l <- #1 + #1;; ! #l @ E {{ v, ⌜v = #2⌝ }}
   
+"heap_e2_spec"
+     : string
 1 subgoal
   
   Σ : gFunctors
@@ -30,6 +34,18 @@
   WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
   @ E [{ v, ⌜v = #2⌝ }]
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  E : coPset
+  l, l' : loc
+  ============================
+  "Hl" : l ↦ #1
+  _ : l' ↦ #1
+  --------------------------------------∗
+  WP #l <- #1 + #1;; ! #l @ E [{ v, ⌜v = #2⌝ }]
+  
 "heap_e7_spec"
      : string
 1 subgoal
@@ -50,7 +66,7 @@
   ============================
   _ : l ↦ #1
   --------------------------------------∗
-  l ↦ #1
+  |={⊤}=> l ↦ #1
   
 1 subgoal
   
@@ -61,7 +77,7 @@
   "Hl1" : l ↦{1 / 2} #0
   "Hl2" : l ↦{1 / 2} #0
   --------------------------------------∗
-  True
+  |={⊤}=> True
   
 1 subgoal
   
@@ -70,7 +86,7 @@
   l : loc
   ============================
   --------------------------------------∗
-  True
+  |={⊤}=> True
   
 "wp_nonclosed_value"
      : string
@@ -97,7 +113,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   "HΦ" : ∀ l0 : loc, l0 ↦∗ replicate (Z.to_nat n) #0 -∗ Φ #l0
   _ : l ↦∗ replicate (Z.to_nat n) #0
   --------------------------------------∗
-  Φ #l
+  |={⊤}=> Φ #l
   
 "test_array_fraction_destruct"
      : string
@@ -113,6 +129,28 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   l ↦∗{1 / 2} vs ∗ l ↦∗{1 / 2} vs
   
+"test_wp_finish_fupd"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  v : val
+  ============================
+  --------------------------------------∗
+  |={⊤}=> True
+  
+"test_twp_finish_fupd"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  v : val
+  ============================
+  --------------------------------------∗
+  |={⊤}=> True
+  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 6cf991f211d830d66b62e4e9b9e5b92a7962f78b..4ae4e64032e79eb540609e5aaa4273644f7f7422 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -25,10 +25,11 @@ Section tests.
   Definition heap_e : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
 
+  Check "heap_e_spec".
   Lemma heap_e_spec E : ⊢ WP heap_e @ E {{ v, ⌜v = #2⌝ }}.
   Proof.
     iIntros "". rewrite /heap_e. Show.
-    wp_alloc l as "?". wp_load. Show.
+    wp_alloc l as "?". wp_pures. wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
     wp_store. by wp_load.
   Qed.
 
@@ -37,11 +38,13 @@ Section tests.
     let: "y" := ref #1 in
     "x" <- !"x" + #1 ;; !"x".
 
+  Check "heap_e2_spec".
   Lemma heap_e2_spec E : ⊢ WP heap_e2 @ E [{ v, ⌜v = #2⌝ }].
   Proof.
     iIntros "". rewrite /heap_e2.
     wp_alloc l as "Hl". Show. wp_alloc l'.
-    wp_load. wp_store. wp_load. done.
+    wp_pures. wp_bind (!_)%E. wp_load. Show. (* No fupd was added *)
+    wp_store. wp_load. done.
   Qed.
 
   Definition heap_e3 : expr :=
@@ -235,7 +238,6 @@ Section tests.
     iIntros "[$ _]". (* splits the fraction, not the app *)
   Qed.
 
-
   Lemma test_wp_free l v :
     {{{ l ↦ v }}} Free #l {{{ RET #(); True }}}.
   Proof.
@@ -247,6 +249,20 @@ Section tests.
   Proof.
     iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
   Qed.
+
+  Check "test_wp_finish_fupd".
+  Lemma test_wp_finish_fupd (v : val) :
+    ⊢ WP v {{ v, |={⊤}=> True }}.
+  Proof.
+    wp_pures. Show. (* No second fupd was added. *)
+  Abort.
+
+  Check "test_twp_finish_fupd".
+  Lemma test_twp_finish_fupd (v : val) :
+    ⊢ WP v [{ v, |={⊤}=> True }].
+  Proof.
+    wp_pures. Show. (* No second fupd was added. *)
+  Abort.
 End tests.
 
 Section inv_mapsto_tests.
diff --git a/tests/heap_lang_proph.v b/tests/heap_lang_proph.v
index 109958a5c95ecef365280e11671ff4835e5bc21f..cab2dda3ac8d7e31e01ea5cf0818cffb2a823092 100644
--- a/tests/heap_lang_proph.v
+++ b/tests/heap_lang_proph.v
@@ -15,7 +15,7 @@ Section tests.
       {{ v, ⌜v = (#n, #true)%V⌝ ∗ ∃vs, proph p vs ∗ l ↦ #(n+1) }}.
   Proof.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
-    wp_cmpxchg_suc. iIntros (ws ->) "Hp". eauto with iFrame.
+    wp_cmpxchg_suc. iIntros "!>" (ws ->) "Hp". eauto with iFrame.
   Restart.
     iIntros "Hl Hp". wp_pures. wp_apply (wp_resolve_cmpxchg_suc with "[$Hp $Hl]"); first by left.
     iIntros "Hpost". iDestruct "Hpost" as (ws ->) "Hp". eauto with iFrame.
@@ -26,7 +26,7 @@ Section tests.
     WP Resolve (#n + #m - (#n + #m)) #p #() @ E {{ v, ⌜v = #0⌝ ∗ ∃vs, proph p vs }}.
   Proof.
     iIntros "Hp". wp_pures. wp_apply (wp_resolve with "Hp"); first done.
-    wp_pures. iIntros (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
+    wp_pures. iIntros "!>" (ws ->) "Hp". rewrite Z.sub_diag. eauto with iFrame.
   Qed.
 
   Lemma test_resolve3 s E (p1 p2 : proph_id) (vs1 vs2 : list (val * val)) (n : Z) :
@@ -38,7 +38,7 @@ Section tests.
     wp_apply (wp_resolve with "Hp1"); first done.
     wp_apply (wp_resolve with "Hp2"); first done.
     wp_op.
-    iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
+    iIntros "!>" (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
     iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
   Qed.
 
@@ -51,7 +51,7 @@ Section tests.
     wp_apply (wp_resolve with "Hp1"); first done.
     wp_apply (wp_resolve with "Hp2"); first done.
     wp_op.
-    iIntros (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
+    iIntros "!>" (vs2' ->) "Hp2". iIntros (vs1' ->) "Hp1". rewrite Z.sub_diag.
     iApply "HΦ". iExists vs1', vs2'. eauto with iFrame.
   Qed.
 
diff --git a/tests/ipm_paper.ref b/tests/ipm_paper.ref
index 9bcb74f82069801b5c48be7eae96fc66eb070ff9..486e79dd063618065ce99a0a2518d25471d59fa9 100644
--- a/tests/ipm_paper.ref
+++ b/tests/ipm_paper.ref
@@ -96,5 +96,5 @@ P
   "Hl" : l ↦ #c
   "Hγ" : own γ (Auth c)
   --------------------------------------∗
-  ▷ I γ l ∗ (∃ m : nat, ⌜#c = #m ∧ n ≤ m⌝ ∧ C l m)
+  |={⊤ ∖ ↑N}=> ▷ I γ l ∗ (∃ m : nat, ⌜#c = #m ∧ n ≤ m⌝ ∧ C l m)
   
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index b3e0527dd0fad2378e97be5f101e57e5c51c04c3..5895fe954477bdabba737c7ec8c7afb8b27d13d4 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -220,7 +220,7 @@ Section counter_proof.
     iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
     wp_bind (! _)%E. iApply wp_inv_open; last iFrame "Hinv"; auto.
     iDestruct 1 as (c) "[Hl Hγ]".
-    wp_load. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     wp_let. wp_op.
     wp_bind (CmpXchg _ _ _). iApply wp_inv_open; last iFrame "Hinv"; auto.
     iDestruct 1 as (c') ">[Hl Hγ]".
@@ -229,11 +229,11 @@ Section counter_proof.
       iDestruct (own_valid with "Hγ") as %?%auth_frag_valid; rewrite -auth_frag_op //.
       iMod (own_update with "Hγ") as "Hγ"; first apply M_update.
       rewrite (auth_frag_op (S n) (S c)); last lia; iDestruct "Hγ" as "[Hγ Hγf]".
-      wp_cmpxchg_suc. iSplitL "Hl Hγ".
+      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
       { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
       wp_pures. rewrite {3}/C; eauto 10.
     - wp_cmpxchg_fail; first (intros [=]; abstract lia).
-      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
+      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
       wp_pures. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
   Qed.
 
@@ -247,7 +247,7 @@ Section counter_proof.
     iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[-]") as % ?%auth_frag_valid.
     { iApply own_op. by iFrame. }
     rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
-    iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
+    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
     rewrite /C; eauto 10 with lia.
   Qed.
 End counter_proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 3de778074989ff8490913e049a2dee1ecb24d6b9..cec2f71d4bb4178adaba7b502066e9559c11a9e7 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -74,7 +74,7 @@ Proof.
       + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iSplitL "Hinv"; first by eauto.
-    iModIntro. wp_pures. iIntros "!>". wp_lam.
+    iModIntro. wp_pures. iIntros "!> !>". wp_lam.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']";
       subst; wp_match; [done|].
     wp_bind (! _)%E.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 13230b72860e57a20aecb047bb4ed4f6c4f22069..e2fb69892d6938a7f1c9ed5a391ef30d95459d44 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -90,7 +90,7 @@ Proof.
       + Show. iSplit. iLeft; by iSplitL "Hl". eauto.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     iSplitL "Hinv"; first by eauto.
-    iModIntro. wp_pures. iIntros "!>". wp_lam. wp_bind (! _)%E.
+    iModIntro. wp_pures. iIntros "!> !>". wp_lam. wp_bind (! _)%E.
     iInv N as "Hinv".
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as (m) "[% Hγ']"; subst.
     + iDestruct "Hinv" as "[[Hl >Hγ]|H]"; last iDestruct "H" as (m') "[Hl Hγ]";