diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f00723e452b98894d6ddf2f99f76b921ca709175..082649a8d3f0c0945daccfbefc99284e105af643 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -78,6 +78,11 @@ Section tests.
   Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
   Proof. wp_lam. wp_op. by case_bool_decide. Qed.
 
+  Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
+
+  Lemma heap_e7_spec l : l ↦ #0 -∗ WP heap_e7 #l [{_,  l ↦ #1 }].
+  Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + #1 in
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 6baede50eef36e14ea95ca7a11815514beba296e..90e561f2fb320740831868db8f416b729b4b42c4 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -511,7 +511,7 @@ Tactic Notation "wp_cas_suc" :=
     |try congruence
     |try fast_done (* vals_cas_compare_safe *)
     |simpl; try wp_value_head]
-  | |- envs_entails _ (twp ?E ?e ?Q) =>
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];