diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index eedb1df786526354d81e7b1144b458a258094a62..2617a9ad41b8954d8f66682d388f050a891eec78 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -209,7 +209,8 @@ let rec infer env t =
       make Integer.zero (Integer.div (Integer.of_int n) Integer.eight)
     | TArray _ | TPtr _ -> Lazy.force interv_of_unknown_block
     | _ -> assert false)
-  | Tblock_length (_, t) ->
+  | Tblock_length (_, t)
+  | Toffset(_, t) ->
     (match Cil.unrollType (get_cty t) with
     | TArray(_, _, { scache = Computed n }, _) ->
       let nb_bytes = if n mod 8 = 0 then n / 8 else n / 8 + 1 in
@@ -236,7 +237,6 @@ let rec infer env t =
   | TBinOp (MinusPI,_,_)
   | TAddrOf _
   | TStartOf _
-  | Toffset _
   | Tlambda (_,_)
   | TDataCons (_,_)
   | Tbase_addr (_,_)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 7d4c9ab576de60064a22d321426414bdd696951d..bd19b068fdc5bd9f0aee5d5d3181753dc63046d4 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -191,6 +191,7 @@ let rec type_term env ~ctx t =
        with Interval.Not_an_integer ->
          Other)
 
+    | Toffset(_, t')
     | Tblock_length(_, t')
     | TSizeOfE t'
     | TAlignOfE t' ->
@@ -306,7 +307,6 @@ let rec type_term env ~ctx t =
       type_term_lval env tlv;
       Other
 
-    | Toffset(_, t)
     | Tbase_addr (_, t) ->
       (* it is a pointer, as well as [t], but [t] must be typed. *)
       ignore (type_term env ~ctx:Other t);