diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 8f0c5dd0358b15a7b63d478b793b41a13013ee51..9deb0c43059410fdd55a579123a83e1c2a05be6a 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -543,6 +543,10 @@ struct
            to a deref of a cast to a pointer `*(T( * )[])(p)` *)
         let cast = cast_ptr dst_ctype t0 in
         L.load (C.current env) (Ctypes.object_of dst_ctype) cast
+    | C_array dst_arr_info, L_array src_arr_info
+      when Ctypes.AinfoComparable.equal dst_arr_info src_arr_info ->
+        (* cast from/to the same type *)
+        C.logic env t
     | C_array {arr_flat=Some _}, (L_integer|L_cint _|L_bool|L_real|L_cfloat _|L_array _) ->
         Warning.error "@[Logic cast to sized array (%a) from (%a) not implemented yet@]"
           Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type