diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 6e6d3de14c2c2204b94af80ffc96d3eca7f86150..a9534ac43959ab1a161c491ad93a90310a8ed4f9 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -1213,12 +1213,14 @@ end
 (* --- Dataflow computation                                           --- *)
 (* ---------------------------------------------------------------------- *)
 
+type 'a widening = Fixpoint | Widening of 'a
+
 module type Domain =
 sig
   type t
 
   val join : t -> t -> t
-  val widen : t -> t -> t option (* returns None when inclusion *)
+  val widen : t -> t -> t widening
   val transfer : vertex -> vertex edge ->  t -> t option
 end
 
@@ -1292,8 +1294,8 @@ struct
       | None, _ -> true (* Previous was bottom *)
       | Some v1, Some v2 ->
         match D.widen v1 v2 with
-        | None -> false (* End of iteration *)
-        | Some value -> (* new value *)
+        | Fixpoint -> false (* End of iteration *)
+        | Widening value -> (* new value *)
           States.replace results v value;
           true
     in
diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index 0fe34c38337a0929fb88382d83f8466d514c0eb2..939a7929c584df1618d256473f33c9128c13ab58 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/src/kernel_services/analysis/interpreted_automata.mli
@@ -310,6 +310,12 @@ end
     See tests/misc/interpreted_automata_dataflow.ml for a complete example
     using this dataflow computation. *)
 
+type 'a widening =
+  | Fixpoint       (** The analysis have reached a fixpoint *)
+  | Widening of 'a (** The analysis have not reached a fixpoint and must
+                       continue with the provided state, widened if termination
+                       requires it. *)
+
 (** Input domain for a simple dataflow analysis. *)
 module type Domain =
 sig
@@ -321,15 +327,15 @@ sig
   (** [widen v1 v2] is called on loop heads after each iteration of the
       analysis on the loop body: [v1] is the previous state before the
       iteration, and [v2] the new state after the iteration.
-      The function must return None if the analysis has reached a fixpoint for
-      the loop: this is the case if [join v1 v2] is equivalent to [v1], as a new
-      iteration would have the same entry state as the last one.
+      The function must return [Fixpoint] if the analysis has reached a fixpoint
+      for the loop: this is the case if [join v1 v2] is equivalent to [v1], as a
+      new iteration would have the same entry state as the last one.
       Otherwise, it must return the new entry state for the next iteration,
       by over-approximating the join between [v1] and [v2] such that
       any sequence of successive widenings is ultimately stationary,
-      i.e. […widen (widen (widen x0 x1) x2) x3…] eventually returns None.
+      i.e. […widen (widen (widen x0 x1) x2) x3…] eventually returns [Fixpoint].
       This ensures the analysis termination. *)
-  val widen : t -> t -> t option
+  val widen : t -> t -> t widening
 
   (** Transfer function for edges: computes the state after the transition
       from the state before. Returns None if the end of the transition is not
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index 444b362690d450331706660c8c312762d14c310d..c2a29ac70d6e80b39fb0e82a9e2d8e1ce46bf4a7 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/tests/misc/interpreted_automata_dataflow_backward.ml
@@ -16,9 +16,9 @@ struct
 
   let widen v1 v2 =
     if Set.subset v2 v1 then
-      None (* Inclusion *)
+      Interpreted_automata.Fixpoint (* Inclusion *)
     else
-      Some v2 (* No widening necessary *)
+      Interpreted_automata.Widening v2 (* No widening necessary *)
 
   let rec vars exp =
     match exp.enode with
diff --git a/tests/misc/interpreted_automata_dataflow_forward.ml b/tests/misc/interpreted_automata_dataflow_forward.ml
index 017d2f638d0b723b8731704db434122718c5fb6b..922109a7ec9e9a52b0657cb22ebdaaf9e8281c9b 100644
--- a/tests/misc/interpreted_automata_dataflow_forward.ml
+++ b/tests/misc/interpreted_automata_dataflow_forward.ml
@@ -25,9 +25,9 @@ struct
       Map.find_opt vi v2 = Some x
     in
     if Map.for_all same_entry v1 then
-      None (* Inclusion *)
+      Interpreted_automata.Fixpoint (* Inclusion *)
     else
-      Some v2 (* No widening necessary *)
+      Interpreted_automata.Widening v2 (* No widening necessary *)
 
   exception Not_constant