diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 16c04fc09ca8b761c684cc157dcf6a14bea1870b..b2f0dd887bc2689924cf8995643f9e575d022dfc 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -136,6 +136,12 @@ 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
@@ -147,7 +153,9 @@ let rec is_positive_or_null e = match F.repr e with
   | _ -> (* 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.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
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