From 0c6202e40389cffce00ae244885c93fa54d1c387 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20Ruet-Cros?= <cecile.ruet-cros@cea.fr>
Date: Fri, 5 Jul 2024 10:04:04 +0200
Subject: [PATCH] [wp] vset: clean useless lemmas in test
---
src/plugins/wp/share/why3/frama_c_wp/vset.mlw | 12 ------------
1 file changed, 12 deletions(-)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
index 8839185f2a4..1bc8a862eac 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
@@ -53,18 +53,6 @@ theory Vset
axiom member_bool : forall x:'a. forall s:set 'a [member_bool x s].
if mem x s then member_bool x s = True else member_bool x s = False
- lemma member_range : forall x:int,a:int,b:int [mem x (range a b)].
- mem x (range a b) <-> (a <= x /\ x <= b)
-
- lemma member_range_sup : forall x:int,a:int [mem x (range_sup a)].
- mem x (range_sup a) <-> (a <= x)
-
- lemma member_range_inf : forall x:int,b:int [mem x (range_inf b)].
- mem x (range_inf b) <-> (x <= b)
-
- lemma member_range_all : forall x:int [mem x range_all].
- mem x range_all
-
(* -------------------------------------------------------------------------- *)
end
--
GitLab