From 350350ce23b5d1276490b9b6dcb8c6093a3fb4c4 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 8 Jan 2021 15:52:48 +0100
Subject: [PATCH] [WP] minor: fixes a comment
---
src/plugins/wp/Cint.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 5b642e95417..d0aced04c22 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -765,7 +765,7 @@ let smp_leq_with_lsr x y =
(* p >= 0 ==> ( 0 <= (a >> p) <==> 0 <= a )*)
e_leq e_zero a
else
- (* p >= 0 ==> ( x <= (a >> p) <= y <==> x <= a/(2**p) ) *)
+ (* p >= 0 ==> ( x <= (a >> p) <==> x <= a/(2**p) ) *)
let k = two_power_k p in
e_leq x (e_div a (e_zint k))
with Not_found ->
--
GitLab