diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index eb689f8e6d73a02541e2e8963cf9ed35ce1739fd..ee03be85c4d500b2e32be83932d7b28745f4a87e 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -68,3 +68,8 @@
     let: "val2" := fun2 "val1" in
     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
   {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
+"not_cas_compare_safe"
+     : string
+The command has indeed failed with message:
+Ltac call to "wp_cas_suc" failed.
+Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 09ed3ecc6d7e172f19529be96b835995a5de69ce..7efc06e02b8ca348d577a4c5b5d9f2dec1604f1e 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -161,5 +161,16 @@ Section printing_tests.
 
 End printing_tests.
 
+Section error_tests.
+  Context `{heapG Σ}.
+
+  Check "not_cas_compare_safe".
+  Lemma not_cas_compare_safe (l : loc) (v : val) :
+    l ↦ v -∗ WP CAS #l v v {{ _, True }}.
+  Proof.
+    iIntros "H↦". Fail wp_cas_suc.
+  Abort.
+End error_tests.
+
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index c46eafa574440188ab96a9dbc6bab6d08e68764f..17236f403ce7ba382d87045b2efb29ba50c42e59 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -406,7 +406,7 @@ Tactic Notation "wp_cas_fail" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -415,7 +415,7 @@ Tactic Notation "wp_cas_fail" :=
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_fail: Values are not safe to compare for CAS"
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_fail: not a 'wp'"
   end.
@@ -434,7 +434,7 @@ Tactic Notation "wp_cas_suc" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
     |pm_reflexivity
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
@@ -444,7 +444,7 @@ Tactic Notation "wp_cas_suc" :=
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |done
+    |fast_done || fail "wp_cas_suc: Values are not safe to compare for CAS"
     |pm_reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"