From 18c6156059f5d3a331522874170b1f68e5419f4a Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 21 Nov 2019 12:59:34 +0100
Subject: [PATCH] [WP/QED] Fixes comparison with lsr
---
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 c6d48f85cc3..25ec6fa672e 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -721,7 +721,7 @@ let smp_cmp_with_lsr cmp a0 b0 =
e/A2 cmp b2 <==> (e/A2)*A2 cmp b2*A2) with A2==2**a2
So, A2>0 and (e/A2)*A2 == e&~((2**a2)-1)
*)
- mk_cmp_with_lsr_cst e_eq e a2 b1
+ mk_cmp_with_lsr_cst cmp e a2 b1
with Not_found ->
(* This rule takes into acount several cases.
One of them is
--
GitLab