From 74d678e218f3ca0865f1ffeaf3db29cb48c864b4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 13:26:50 +0100
Subject: [PATCH] also test TWP

---
 tests/heap_lang.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 42940fee7..019a1c8af 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 →
-- 
GitLab