diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 16c04fc09ca8b761c684cc157dcf6a14bea1870b..65ff69a9b88586d14ad5200049359a688a392bb6 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -136,18 +136,27 @@ let match_mod t =
   | Logic.Mod (e1, e2) -> e1, e2
   | _ -> raise Not_found
 
+(* integration with qed should be improved! *)
+let is_positive t =
+  match F.repr t with
+  | Logic.Kint c -> Integer.le Integer.one c
+  | _ -> false
+
 (* integration with qed should be improved! *)
 let rec is_positive_or_null e = match F.repr e with
   | Logic.Fun( f , [e] ) when Fun.equal f f_lnot -> is_negative e
   | Logic.Fun( f , es ) when Fun.equal f f_land  -> List.exists is_positive_or_null es
   | Logic.Fun( f , es ) when Fun.equal f f_lor   -> List.for_all is_positive_or_null es
-  | Logic.Fun( f , es ) when Fun.equal f f_lxor   -> (match xor_sign es with | Some b -> b | _ -> false)
+  | Logic.Fun( f , es ) when Fun.equal f f_lxor  -> (match mul_xor_sign es with | Some b -> b | _ -> false)
   | Logic.Fun( f , es ) when Fun.equal f f_lsr || Fun.equal f f_lsl
     -> List.for_all is_positive_or_null es
   | _ -> (* try some improvement first then ask to qed *)
       let improved_is_positive_or_null e = match F.repr e with
         | Logic.Add es -> List.for_all is_positive_or_null es
-        | Logic.Mod(e1,_) -> is_positive_or_null e1
+        | Logic.Mul es -> (match mul_xor_sign es with | Some b -> b | _ -> false)
+        | Logic.Mod(e1,e2) when is_positive e2 || is_negative e2 ->
+            (* e2<>0 ==> ( 0<=(e1 % e2) <=> 0<=e1 ) *)
+            is_positive_or_null e1
         | _ -> false
       in if improved_is_positive_or_null e then true
       else match F.is_true (F.e_leq e_zero e) with
@@ -155,20 +164,21 @@ let rec is_positive_or_null e = match F.repr e with
         | Logic.No | Logic.Maybe -> false
 and is_negative e = match F.repr e with
   | Logic.Fun( f , [e] ) when Fun.equal f f_lnot -> is_positive_or_null e
-  | Logic.Fun( f , es ) when Fun.equal f f_lor  -> List.exists is_negative es
-  | Logic.Fun( f , es ) when Fun.equal f f_land -> List.for_all is_negative es
-  | Logic.Fun( f , es ) when Fun.equal f f_lxor  -> (match xor_sign es with | Some b -> (not b) | _ -> false)
+  | Logic.Fun( f , es ) when Fun.equal f f_lor   -> List.exists is_negative es
+  | Logic.Fun( f , es ) when Fun.equal f f_land  -> List.for_all is_negative es
+  | Logic.Fun( f , es ) when Fun.equal f f_lxor  -> (match mul_xor_sign es with | Some b -> (not b) | _ -> false)
   | Logic.Fun( f , [k;n] ) when Fun.equal f f_lsr || Fun.equal f f_lsl
     -> is_positive_or_null n && is_negative k
   | _ -> (* try some improvement first then ask to qed *)
       let improved_is_negative e = match F.repr e with
         | Logic.Add es -> List.for_all is_negative es
+        | Logic.Mul es -> (match mul_xor_sign es with | Some b -> (not b) | _ -> false)
         | _ -> false
       in if improved_is_negative e then true
       else match F.is_true (F.e_lt e e_zero) with
         | Logic.Yes -> true
         | Logic.No | Logic.Maybe -> false
-and xor_sign es = try
+and mul_xor_sign es = try
     Some (List.fold_left (fun acc e ->
         if is_positive_or_null e then acc (* as previous *)
         else if is_negative e then (not acc) (* opposite sign *)
diff --git a/src/plugins/wp/tests/wp_acsl/bitwise.i b/src/plugins/wp/tests/wp_acsl/bitwise.i
index b2e5594f27096dbe8e31f400e04a8cc75ee1abce..931ba45bd5a98105e7cac707a1989445b491a1c8 100644
--- a/src/plugins/wp/tests/wp_acsl/bitwise.i
+++ b/src/plugins/wp/tests/wp_acsl/bitwise.i
@@ -115,7 +115,7 @@ void lemma(unsigned a, unsigned b, unsigned k) {
   /* note: a5 is not simplified because Qed cannot infer that a&b is positive
    */
 
-  //@ check           ( a & (85 % b) & 0xFF ) == ( (a & (85 % b)) % 0x100 );
+  //@ check           ( a & ((b & 0xFFFF) % 55) & 0xFF ) == ( (a & ((b & 0xFFFF) % 55)) % 0x100 );
 
   //@ check zbit: a5: ( a & b & 77 & ((1 << k)-1) ) == ( (a & b & 77) % (1 << k) );
   /* note: a4 is not simplified because Qed cannot infer that k is positive