diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 6037ecd4764ebf255bf5f5cf75a15d0ebd0db9f7..d8aa1f987abebcace1b7a905d5defb3207046f71 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -211,7 +211,10 @@ let rec infer t =
   | TBinOp (MinusPP, t, _) ->
     (match Cil.unrollType (get_cty t) with
     | TArray(_, _, { scache = Computed n (* size in bits *) }, _) ->
-      make Integer.zero (Integer.div (Integer.of_int n) Integer.eight)
+      (* the second argument must be in the same block than [t]. Consequently
+         the result of the difference belongs to [0; \block_length(t)] *)
+      let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
+      make Integer.zero (Integer.of_int nb_bytes)
     | TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
     | _ -> assert false)
   | Tblock_length (_, t)