diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index d78ac2bd27308ea2531701755545426636c607eb..ffba8070d60ca2f3a44b4fcd662f65f7047ee3f3 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -61,9 +61,10 @@ PLUGIN_NAME:=Wp
 PLUGIN_CMO:= \
 	rformat wprop \
 	wp_parameters wp_error \
-	dyncall ctypes clabels \
 	Why3Provers \
-	Context Warning AssignsCompleteness MemoryContext wpContext \
+	Context Warning \
+	dyncall ctypes clabels \
+	AssignsCompleteness MemoryContext wpContext \
 	LogicUsage RefUsage \
 	Layout Region \
 	RegionAnnot RegionAccess RegionDump RegionAnalysis \
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 542d8e413968a44764e750adddb57680a67714f8..374fda3f93978b0669ff93edbea5e4c6bad67546 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -237,8 +237,13 @@ let char c = Integer.to_int64 (Cil.charConstToInt c)
 
 let constant e =
   match (Cil.constFold true e).enode with
-  | Const(CInt64(k,_,_)) -> Integer.to_int64 k
-  | _ -> WpLog.fatal "Non-constant expression (%a)" Printer.pp_exp e
+  | Const(CInt64(k,_,_)) ->
+      begin
+        try Integer.to_int64 k
+        with Z.Overflow ->
+          Warning.error "Array size too large (%a)" (Integer.pretty ~hexa:true) k
+      end
+  | _ -> Warning.error "Non-constant expression (%a)" Printer.pp_exp e
 
 let get_int e =
   match (Cil.constFold true e).enode with