diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index d0aced04c226e0fc72883b2771e38e2d07f24df9..dbba575d2a09e5b5a7d8186869eaeece7f6c9c95 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -618,11 +618,11 @@ let smp_eq_with_land a b =
 let smp_eq_with_lor a b =
   let b1 = match_integer b in
   let es = match_fun f_lor a in
-  try (* b1==(a2|t22) <==> (b1^a2)==(~a2&e) *)
+  try (* b1==(a2|e) <==> (b1^a2)==(~a2&e) *)
     let a2,es = match_integer_extraction es in
     let k1 = Integer.logxor b1 a2 in
     let k2 = Integer.lognot a2 in
-    e_eq (e_zint k1) (e_fun f_land ((e_zint k2)::es))
+    e_eq (e_zint k1) (e_fun f_land [e_zint k2 ; e_fun f_lor es])
   with Not_found when b == e_zero ->
     (* 0==(a1|a2) <=> (0==a1 && 0==a2) *)
     F.e_and (List.map (e_eq b) es)