diff --git a/tests/counter.v b/tests/counter.v
index 1a6f6c753ec4c0d8319fae3ac4b03d3e1776e7fc..c5e84d11d76f6f8bcbcd1098e63bc885a3fa5825 100644
--- a/tests/counter.v
+++ b/tests/counter.v
@@ -94,7 +94,7 @@ Lemma newcounter_spec N :
   heapN ⊥ N →
   heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, v = #l ∧ C l 0 }}.
 Proof.
-  iIntros (?) "#Hh !# _ /=". rewrite /newcounter. wp_seq. wp_alloc l as "Hl".
+  iIntros (?) "#Hh !# _ /=". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl".
   iVs (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
   rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]".
   iVs (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?".
@@ -128,7 +128,7 @@ Lemma read_spec l n :
   {{ C l n }} read #l {{ v, ∃ m : nat, ■ (v = #m ∧ n ≤ m) ∧ C l m }}.
 Proof.
   iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)".
-  rewrite /read. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
+  rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load.
   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']".
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 111a9f5542819951476e5268ba0fd8e45ada0d14..3e610b65d9ad5dd6d1549dc8575c201d0b16df37 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -42,7 +42,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "[#? Hf] /=".
-  rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let.
+  rewrite /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
   iVs (own_alloc Pending) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
   { iNext. iLeft. by iSplitL "Hl". }
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index 18a8a4d892215f952aecd6d9b09ae47c2216c8dd..73a023c116a2b864379247a04e715298e9ce5ce6 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -60,7 +60,7 @@ Lemma sum_wp `{!heapG Σ} v t Φ :
   heap_ctx ★ is_tree v t ★ (is_tree v t -★ Φ #(sum t))
   ⊢ WP sum' v {{ Φ }}.
 Proof.
-  iIntros "(#Hh & Ht & HΦ)". rewrite /sum'.
+  iIntros "(#Hh & Ht & HΦ)". rewrite /sum' /=.
   wp_let. wp_alloc l as "Hl". wp_let.
   wp_apply sum_loop_wp; iFrame "Hh Ht Hl".
   rewrite Z.add_0_r.