diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index eca53a8ad9748efcdf3535efa00dc030edb8bd70..5f74f033294982cb7e143c11cc7f7487e078ef16 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -121,6 +121,23 @@ Section tests.
     ⊢ WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }].
   Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
 
+  Definition Id : val :=
+    rec: "go" "x" :=
+      if: "x" = #0 then #() else "go" ("x" - #1).
+
+  (** These tests specially test the handling of the [vals_compare_safe]
+  side-condition of the [=] operator. *)
+  Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌝ }}.
+  Proof.
+    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+    by replace (S n - 1) with (n:Z) by lia.
+  Qed.
+  Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌝ }].
+  Proof.
+    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+    by replace (S n - 1) with (n:Z) by lia.
+  Qed.
+
   Lemma wp_apply_evar e P :
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 98ea0e6758ebc15bcc7577466f5034ad664f91ba..cb9c1a2afbd6c7d4dc53cc9d3de4dfb3fa557c33 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -97,7 +97,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       unify e' efoc;
       eapply (tac_twp_pure _ _ _ (fill K e'));
       [iSolveTC                       (* PureExec *)
-      |try fast_done                  (* The pure condition for PureExec *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec *)
       |wp_finish                      (* new goal *)
       ])
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"