diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index ee03be85c4d500b2e32be83932d7b28745f4a87e..c0246453727e3d9baa9a73febe08a74cdbabce44 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -73,3 +73,8 @@
 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.
+"not_cas"
+     : string
+The command has indeed failed with message:
+Ltac call to "wp_cas_suc" failed.
+Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 7efc06e02b8ca348d577a4c5b5d9f2dec1604f1e..eba3026da02e9c6d1bb25b1280f9d8ecbeae799c 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -170,6 +170,13 @@ Section error_tests.
   Proof.
     iIntros "H↦". Fail wp_cas_suc.
   Abort.
+
+  Check "not_cas".
+  Lemma not_cas :
+    (WP #() {{ _, True }})%I.
+  Proof.
+    Fail wp_cas_suc.
+  Abort.
 End error_tests.
 
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).