diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index cafa0e96b6bf360f0c103ca51cdb542520381f07..5793c2feb49aabde87b7f8ef4e4ade646c1f5b87 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1464,10 +1464,6 @@ loop_pragma:
       (if $3 <> "UNROLL" then
 	 Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
        Unroll_specs $4)
-    else if $3 = "WIDEN_VARIABLES" then
-      Widen_variables $4
-    else if $3 = "WIDEN_HINTS" then
-      Widen_hints $4
     else raise (Not_well_formed (loc $sloc,"Unknown loop pragma")) }
 ;
 
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 4bc1d09e3912cfc2307e68172b2237329b35579d..9a3077594832805d91a225cca66de4852d2434fd 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -82,7 +82,6 @@ let extract_from_pragmas global_find_init s =
     match a.annot_content with
     | APragma (Loop_pragma (Unroll_specs specs)) ->
       List.fold_left (update_info global_find_init e) info specs
-    | APragma (Loop_pragma _) -> info
     | _ -> assert false (* should have been filtered above. *)
   in
   List.fold_left get_infos empty_info pragmas
diff --git a/src/kernel_services/analysis/logic_deps.ml b/src/kernel_services/analysis/logic_deps.ml
index 874fb84942604f9d0ea8c9a8d6806d6b4926a8e4..65883a64ce26715463f3aa69166f17dff78a4b14 100644
--- a/src/kernel_services/analysis/logic_deps.ml
+++ b/src/kernel_services/analysis/logic_deps.ml
@@ -478,9 +478,7 @@ let get_zone_from_annot a (ki,kf) loop_body_opt results =
   | AVariant (term,_) ->
     (* to preserve the interpretation of the variant *)
     get_zone_from_term (Option.get loop_body_opt) term results
-  | APragma (Loop_pragma (Unroll_specs terms))
-  | APragma (Loop_pragma (Widen_hints terms))
-  | APragma (Loop_pragma (Widen_variables terms)) ->
+  | APragma (Loop_pragma (Unroll_specs terms)) ->
     (* to select the declaration of the variables *)
     List.fold_left
       (fun results term -> {
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index 0b27f448cc4937d02c715c9f40ba63603e12ac99..0ae3f376d5ac98e2a2fb00a3cd2649de377df45c 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1738,8 +1738,6 @@ and behavior = {
 (** Pragmas for the value analysis plugin of Frama-C. *)
 and loop_pragma =
   | Unroll_specs of term list
-  | Widen_hints of term list
-  | Widen_variables of term list
 
 (** Pragmas for the slicing plugin of Frama-C. *)
 and slice_pragma =
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a9d7c98103737e6c3f99048062c7ff2a5af3647a..31b287429f816c944a15ba5bd08533f4dcafd02c 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -3164,12 +3164,6 @@ class cil_printer () = object (self)
       (pp_list false self#disjoint_behaviors) disjoint
 
   method private loop_pragma fmt = function
-    | Widen_hints terms ->
-      fprintf fmt "WIDEN_HINTS @[%a@]"
-        (Pretty_utils.pp_list ~sep:",@ " self#term) terms
-    | Widen_variables terms ->
-      fprintf fmt "WIDEN_VARIABLES @[%a@]"
-        (Pretty_utils.pp_list ~sep:",@ " self#term) terms
     | Unroll_specs terms ->
       fprintf fmt "UNROLL @[%a@]"
         (Pretty_utils.pp_list ~sep:",@ " self#term) terms
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index bdd64597f8619aa9e107a96a7c81671aebfdff2c..ed13828430d9dd900638e11bcc8df886892228ac 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -932,10 +932,6 @@ and pp_termination_kind fmt = function
 and pp_loop_pragma fmt = function
   | Unroll_specs(term_list) ->
     Format.fprintf fmt "Unroll_specs(%a)" (pp_list pp_term) term_list
-  | Widen_hints(term_list) ->
-    Format.fprintf fmt "Widen_hints(%a)" (pp_list pp_term) term_list
-  | Widen_variables(term_list) ->
-    Format.fprintf fmt "Widen_variables(%a)" (pp_list pp_term) term_list
 
 and pp_slice_pragma fmt = function
   | SPexpr(term) -> Format.fprintf fmt "SPexpr(%a)" pp_term term
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 9509cb045c44331814e5fa1af17e9fa7769da74f..f0aeef687bad114badea91a4fd70bc0170de689e 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -453,10 +453,6 @@ let print_spec fmt spec =
 let print_loop_pragma fmt p =
   match p with
     Unroll_specs l -> fprintf fmt "UNROLL@ %a" (pp_list ~sep:",@ " print_lexpr) l
-  | Widen_hints l ->
-    fprintf fmt "WIDEN_HINTS@ %a" (pp_list ~sep:",@ " print_lexpr) l
-  | Widen_variables l ->
-    fprintf fmt "WIDEN_VARIABLES@ %a" (pp_list ~sep:",@ " print_lexpr) l
 
 let print_slice_pragma fmt p =
   match p with
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 58fe0aa05cd35e230ab82958356a766b3c2961f3..35206eb8bd56bf238238d2225f58100c2b6d0f43 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -702,11 +702,7 @@ and is_same_variant (v,m) (v',m') env =
 
 and is_same_loop_pragma p p' env =
   match p, p' with
-  | Unroll_specs l, Unroll_specs l'
-  | Widen_hints l, Widen_hints l'
-  | Widen_variables l, Widen_variables l' ->
-    is_same_list is_same_term l l' env
-  | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false
+  | Unroll_specs l, Unroll_specs l' -> is_same_list is_same_term l l' env
 
 and is_same_slice_pragma p p' env =
   match p, p' with
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 891b2fb3a4be7fafa4dad423808b06e8dae0d002..7eb80e74d5a03dbb1bf3bb1771ae9c88a7adc34e 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2049,10 +2049,6 @@ and childrenLoopPragma vis p =
   match p with
   | Unroll_specs lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
     if lt' != lt then Unroll_specs lt' else p
-  | Widen_hints lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
-    if lt' != lt then Widen_hints lt' else p
-  | Widen_variables lt -> let lt' = mapNoCopy (visitCilTerm vis) lt in
-    if lt' != lt then Widen_variables lt' else p
 
 and childrenModelInfo vis m =
   let field_type = visitCilLogicType vis m.mi_field_type in
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 3377cdbb68d9e20a77b0aecff2ded641130ea2be..9c5eddcfe4c9e0491a19a30ddcb18c113e06fb6b 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3632,29 +3632,9 @@ struct
 
   let plain_logic_type loc env t = logic_type (base_ctxt env) loc env t
 
-  (* For Widen_hints and Widen_variables, we check that the arguments of the
-     pragma can be understood later. Keep this code synchronized with
-     src/plugins/eva/utils/widen.ml. *)
   let loop_pragma env p =
-    let accept_int = function
-        { term_node = TConst (Integer _)} -> true | _ -> false
-    in
-    let accept_var = function
-        { term_node = TLval (TVar {lv_origin = Some _}, _)} -> true | _ -> false
-    in
-    (* fail when the translation of [p] does not verify the predicate [accept]*)
-    let term_accept accept p =
-      let t = term env p in
-      if not (accept t) then
-        C.error t.term_loc "invalid pragma '%a'" Cil_printer.pp_term t;
-      t
-    in
     match p with
     | Unroll_specs l -> Cil_types.Unroll_specs (List.map (term env) l)
-    | Widen_variables l -> Cil_types.Widen_variables (List.map (term_accept accept_var) l)
-    | Widen_hints l ->
-      let accept t = accept_int t || accept_var t in
-      Cil_types.Widen_hints (List.map (term_accept accept) l)
 
   let model_annot loc ti =
     let env = Lenv.empty() in
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index cd74caa5993ca4a66e9c79f9fa9ec10fd9d103d1..6846b6e71144681376f1988aae766b0a4376282a 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1179,9 +1179,6 @@ let is_same_logic_type_info t1 t2 =
 let is_same_loop_pragma p1 p2 =
   match p1,p2 with
     Unroll_specs l1, Unroll_specs l2 -> is_same_list is_same_term l1 l2
-  | Widen_hints l1, Widen_hints l2 -> is_same_list is_same_term l1 l2
-  | Widen_variables l1, Widen_variables l2 -> is_same_list is_same_term l1 l2
-  | (Unroll_specs _ | Widen_hints _ | Widen_variables _), _ -> false
 
 let is_same_slice_pragma p1 p2 =
   match p1,p2 with
@@ -2302,7 +2299,7 @@ let is_trivial_annotation a =
     -> false
 
 let is_property_pragma = function
-  | Loop_pragma (Unroll_specs _ | Widen_hints _ | Widen_variables _)
+  | Loop_pragma (Unroll_specs _)
   | Slice_pragma (SPexpr _ | SPctrl | SPstmt)
   | Impact_pragma (IPexpr _ | IPstmt) -> false
 (* If at some time a pragma becomes something which should be proven,
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 0dfa48308069b1bc63f3554dbec3bb165539da0e..d123c416326462beb7a280287382364b46fe7872 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -323,8 +323,6 @@ type spec = {
 
 type loop_pragma =
   | Unroll_specs of lexpr list
-  | Widen_hints of lexpr list
-  | Widen_variables of lexpr list
 
 (** Pragmas for the slicing plugin of Frama-C. *)
 and slice_pragma =