diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index ed1d22069662f63a5336e00c980814240a001273..a3fd3727f0804e74ace83abd6470867fe1bd469d 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3957,8 +3957,8 @@ let find_sizeof t f =
     | Error (msg, t') -> raise (SizeOfError(msg, t'))
   with Not_found ->
   try
-    let size = f () in
-    TypSize.add t (Size size) ;
+    let t', size = f () in
+    TypSize.add t' (Size size) ;
     size
   with SizeOfError(t',msg) as e ->
     TypSize.add t (Error (t', msg)) ;
@@ -4378,7 +4378,7 @@ and bitsSizeOf t =
       (SizeOfError
          (Format.sprintf "abstract type '%s'" (compFullName comp), t))
   | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo() ->
-    find_sizeof t (fun () -> 0)
+    find_sizeof t (fun () -> t,0)
   | TComp ({cfields=Some[]} as comp,_) ->
     find_sizeof t
       (fun () ->
@@ -4405,9 +4405,9 @@ and bitsSizeOf t =
          then
            (* On MSVC if we have just a zero-width bitfields then the length
             * is 32 and is not padded  *)
-           32
+           t, 32
          else
-           addTrailing lastoff.oaFirstFree (8 * bytesAlignOf t))
+           t, addTrailing lastoff.oaFirstFree (8 * bytesAlignOf t))
 
   | TComp (comp, _) -> (* Union *)
     find_sizeof t
@@ -4428,14 +4428,14 @@ and bitsSizeOf t =
          (* Note: we treat None above *)
          let max = List.fold_left fold 0 (Option.get comp.cfields) in
          (* Add trailing by simulating adding an extra field *)
-         addTrailing max (8 * bytesAlignOf t))
+         t, addTrailing max (8 * bytesAlignOf t))
 
-  | TArray(bt, Some len, _) ->
+  | TArray(bt, Some len, attrs) ->
     find_sizeof t
       (fun () ->
          begin
-           match (constFold true len).enode with
-             Const(CInt64(l,_,_)) ->
+           match constFold true len with
+             { enode = Const(CInt64(l,_,_)) } as v->
              let sz = Integer.mul (Integer.of_int (bitsSizeOf bt)) l in
              let sz' =
                match Integer.to_int_opt sz with
@@ -4447,7 +4447,7 @@ and bitsSizeOf t =
                        ^"represented with an OCaml int.", t))
 
              in
-             sz' (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
+             (TArray(bt, Some v,attrs), sz') (*WAS: addTrailing sz' (8 * bytesAlignOf t)*)
            | _ -> raise (SizeOfError ("Array with non-constant length.", t))
          end)
   | TVoid _ ->
diff --git a/tests/misc/array_sizeof.i b/tests/misc/array_sizeof.i
new file mode 100644
index 0000000000000000000000000000000000000000..fa364f4725aac76c1268793f11fbb2b7d737c367
--- /dev/null
+++ b/tests/misc/array_sizeof.i
@@ -0,0 +1,10 @@
+/* run.config
+PLUGIN: @EVA_PLUGINS@
+STDOPT:
+*/
+
+int x;
+void main() {
+  unsigned char buf[sizeof(unsigned char[1]) + sizeof(x)];
+  buf[sizeof(buf)];
+}
diff --git a/tests/misc/oracle/array_sizeof.res.oracle b/tests/misc/oracle/array_sizeof.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e580c4e07525d3a39e1a6ffc69cb23038a53307c
--- /dev/null
+++ b/tests/misc/oracle/array_sizeof.res.oracle
@@ -0,0 +1,29 @@
+[kernel] Parsing array_sizeof.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  x ∈ {0}
+[eva:alarm] array_sizeof.i:9: Warning: 
+  accessing out of bounds index.
+  assert
+  sizeof(unsigned char [sizeof(unsigned char [1]) + sizeof(x)]) <
+  (unsigned int)(sizeof(unsigned char [1]) + sizeof(int));
+[eva] Recording results for main
+[eva] done for function main
+[eva] array_sizeof.i:9: assertion 'Eva,index_bound' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+  NON TERMINATING FUNCTION
+[from] Computing for function main
+[from] Non-terminating function main (no dependencies)
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function main:
+  NON TERMINATING - NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+    tmp
+[inout] Inputs for function main:
+    \nothing