diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 42940fee7b9b09305406e32eb07482dee1edabb0..019a1c8af305ac3c470e1ced7c7e90d8959cf75b 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -145,6 +145,9 @@ Section tests.
   Lemma wp_pures_val (b : bool) :
     ⊢ WP #b {{ _, True }}.
   Proof. wp_pures. done. Qed.
+  Lemma twp_pures_val (b : bool) :
+    ⊢ WP #b [{ _, True }].
+  Proof. wp_pures. done. Qed.
 
   Lemma wp_cmpxchg l v :
     val_is_unboxed v →