diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 26256dfdd10b9ee9c3dfcfcc6256af154420ffb5..fd0ba303f420b37044368bddaf1850e91e70da62 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -49,6 +49,21 @@ let rec constFoldTermToLogicReal = function
     end
   | _ -> None
 
+
+module Global_Static_Hints =
+  State_builder.Ref
+    (Widen_type)
+    (struct
+      let dependencies = [ Ast.self ]
+      let name = "Widen.Global_Static_Hints"
+      let default = Widen_type.default
+    end)
+let () = Ast.add_monotonic_state Global_Static_Hints.self
+
+let update_global_hints new_hints =
+  let hints = Widen_type.join (Global_Static_Hints.get ()) new_hints in
+  Global_Static_Hints.set hints;
+
 class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
   inherit Visitor.frama_c_inplace
 
@@ -56,16 +71,16 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
   val enclosing_loops = init_enclosing_loops
 
   method private add_int_thresholds ?base int_thresholds =
-    widen_hints :=
-      Widen_type.join
-        (Widen_type.num_hints None(*see note*) base int_thresholds)
-        !widen_hints
+    let new_hints = Widen_type.num_hints None(*see note*) base int_thresholds in
+    if Extlib.may_map Base.is_global ~dft:false base
+    then update_global_hints new_hints
+    else widen_hints := Widen_type.join new_hints !widen_hints
 
   method private add_float_thresholds ?base float_thresholds =
-    widen_hints :=
-      Widen_type.join
-        (Widen_type.float_hints None(*see note*) base float_thresholds)
-        !widen_hints
+    let new_hints = Widen_type.float_hints None base float_thresholds in
+    if Extlib.may_map Base.is_global ~dft:false base
+    then update_global_hints new_hints
+    else widen_hints := Widen_type.join new_hints !widen_hints
 
   method private add_var_hints ~stmt hints =
     widen_hints := Widen_type.join (Widen_type.var_hints stmt hints) !widen_hints
@@ -385,35 +400,18 @@ class hints_visitor init_widen_hints global = object(self)
     Cil.DoChildren
 end
 
-module Global_Static_Hints =
-  State_builder.Ref
-    (Widen_type)
-    (struct
-      let dependencies = [ Ast.self ]
-      let name = "Widen.Global_Static_Hints"
-      let default = Widen_type.default
-    end)
-let () = Ast.add_monotonic_state Global_Static_Hints.self
-
-(* Global widen hints, used for all functions *)
-let global_widen_hints () =
-  if (not (Global_Static_Hints.is_computed ())) then
-    begin
-      Value_parameters.debug ~dkey "computing global widen hints";
-      let global_widen_hints = ref (Widen_type.default ()) in
-      Globals.Functions.iter_on_fundecs (fun fd ->
-          let visitor = new hints_visitor global_widen_hints true in
-          ignore (Visitor.visitFramacFunction visitor fd)
-        );
-      Global_Static_Hints.set !global_widen_hints;
-      Global_Static_Hints.mark_as_computed ();
-      !global_widen_hints
-    end
-  else
-    Global_Static_Hints.get ()
+(* Precompute global widen hints, used for all functions *)
+let compute_global_static_hints () =
+  Value_parameters.debug ~dkey "computing global widen hints";
+  let global_widen_hints = ref (Global_Static_Hints.get ()) in
+  Globals.Functions.iter_on_fundecs (fun fd ->
+      let visitor = new hints_visitor global_widen_hints true in
+      ignore (Visitor.visitFramacFunction visitor fd)
+    );
+  Global_Static_Hints.set !global_widen_hints
 
 let per_function_static_hints fdec =
-  let widen_hints = ref (global_widen_hints ()) in
+  let widen_hints = ref Widen_type.empty in
   let visitor_pragma = new pragma_widen_visitor widen_hints [] in
   ignore (Visitor.visitFramacFunction visitor_pragma fdec);
   let visitor_local = new hints_visitor widen_hints false in
@@ -433,6 +431,7 @@ let () = Ast.add_monotonic_state Per_Function_Static_Hints.self
 
 (* parse and precompute global and local static hints *)
 let precompute_widen_hints () =
+  compute_global_static_hints ();
   Globals.Functions.iter_on_fundecs
     (fun fd ->
        Per_Function_Static_Hints.replace fd (per_function_static_hints fd))
@@ -549,12 +548,13 @@ module Per_Function_Hints =
 let () = Ast.add_monotonic_state Per_Function_Hints.self
 
 let extract_per_function_hints fdec =
+  let global = Global_Static_Hints.get () in
   let for_fdec =
     try Per_Function_Static_Hints.find fdec
     with Not_found -> assert false
   in
   let dynamic = Dynamic_Hints.get () in
-  Widen_type.join for_fdec dynamic
+  Widen_type.join (Widen_type.join global for_fdec) dynamic
 
 let per_function_hints = Per_Function_Hints.memo extract_per_function_hints