diff --git a/src/kernel_services/analysis/wto_statement.ml b/src/kernel_services/analysis/wto_statement.ml
index bfa182f5e12a8603b8a2989ba244fd5a4bae7a21..b69dd555d6df1d8677820742661f3347b329d35e 100644
--- a/src/kernel_services/analysis/wto_statement.ml
+++ b/src/kernel_services/analysis/wto_statement.ml
@@ -39,7 +39,7 @@ let build_wto kf =
   let init = Kernel_function.find_first_stmt kf
   and succs = fun stmt -> List.rev stmt.succs
   in
-  Scheduler.partition ?pref:None ~init ~succs
+  Scheduler.partition ~pref:(fun _ _ -> 0) ~init ~succs
 
 
 (* ********************************************************************** *)
diff --git a/src/libraries/utils/wto.ml b/src/libraries/utils/wto.ml
index ec3583f300351100430761003f5348622c2220e2..5c6ed3e9801f96d8fb047afd2ad8ca49cc1f8acd 100644
--- a/src/libraries/utils/wto.ml
+++ b/src/libraries/utils/wto.ml
@@ -187,10 +187,9 @@ module Make(N:sig
           let element = Stack.pop state.stack in
           DFN.remove state.dfn element;
           if not (N.equal element vertex) then begin
-            let best_head = match pref with
-              (** the strict is important because we are conservative *)
-              | Some cmp when cmp best_head element < 0 -> element
-              | _ -> best_head
+            (** the strict is important because we are conservative *)
+            let best_head =
+              if pref best_head element < 0 then element else best_head
             in
             reset_SCC best_head
           end
@@ -223,7 +222,7 @@ module Make(N:sig
 
   type pref = N.t -> N.t -> int
 
-  let partition ?pref ~init ~succs =
+  let partition ~pref ~init ~succs =
     let state = {dfn = DFN.create 17; num = 0; succs;
                  stack = Stack.create () } in
     let loop,component = visit ~pref state init [] in
diff --git a/src/libraries/utils/wto.mli b/src/libraries/utils/wto.mli
index 004312ad709592fbdc8c8e98b139f2a098da10f1..1a693e0f597fba0d8209a17f240e94ea390c4daf 100644
--- a/src/libraries/utils/wto.mli
+++ b/src/libraries/utils/wto.mli
@@ -53,11 +53,12 @@ module Make(Node:sig
   end):sig
 
   type pref = Node.t -> Node.t -> int
-  (** partial order of preference for the choice of the head of a loop *)
+  (** Partial order of preference for the choice of the head of a loop.
+      Use "(fun _ _ -> 0)" for no specific preference. *)
 
   (** Implements Bourdoncle "Efficient chaotic iteration strategies with
   widenings" algorithm to compute a WTO. *)
-  val partition: ?pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
+  val partition: pref:pref -> init:Node.t -> succs:(Node.t -> Node.t list) -> Node.t partition
 
   val pretty_partition: Format.formatter -> Node.t partition -> unit
   val pretty_component: Format.formatter -> Node.t component -> unit
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index f5236949e0ae9c9826c14289b87253d90caf0a88..5466a629e8d5f07e5029164aa35342820fc18558 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -597,7 +597,7 @@ struct
     let next = (a.return_point,Vertex.Set.empty) in
     let wto =
       WTO.partition
-        ?pref:None (* natural loop keep the heads *)
+        ~pref:(fun _ _ -> 0) (* natural loops keep their heads *)
         ~succs:(UnrollUnnatural.G.succ g)
         ~init:here in