diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index de54d6beef06179e7628d41342b308561fe4becd..b4b3a8f031b955b02b5b1a6a1f2c6718a880377f 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -63,6 +63,14 @@ struct
       List.iter (pp_call fmt) cs.stack;
       Format.fprintf fmt "%a@]" Kernel_function.pretty cs.entry_point
 
+    let compare_lex ls1 ls2 =
+      if ls1 == ls2 then 0 else
+        let c = Thread.compare ls1.thread ls2.thread in
+        if c <> 0 then c else
+          let c = Kernel_function.compare ls1.entry_point ls2.entry_point in
+          if c <> 0 then c else
+            Calls.compare (List.rev ls1.stack) (List.rev ls2.stack)
+
     let hash cs =
       Hashtbl.hash
         (cs.thread, Kernel_function.hash cs.entry_point, Calls.hash cs.stack)
@@ -105,6 +113,10 @@ struct
 
   include Datatype.Make_with_collections (Prototype)
 
+  let compare_lex cs1 cs2 =
+    match cs1, cs2 with
+    | Local ls1, Local ls2 -> LocalStack.compare_lex ls1 ls2
+    | cs1, cs2 -> compare cs1 cs2
 
   (* Constructor *)
 
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
index dc6b71c84df1d3dc9f8f7c0043e4f410ba58da89..97a4b2957e0390667edff4ce582faff520972bb6 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -41,6 +41,8 @@ sig
 
   include Datatype.S_with_collections with type t = callstack
 
+  val compare_lex : t -> t -> int
+
   val init_global : Cil_types.varinfo -> t
   val init_local : ?thread:int -> Cil_types.kernel_function -> t
 
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 18d459bb8869651e338068a2d54d008b7e7de21f..1b7b47ac288ce582fd528fe56b4c17ea33606f5e 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -143,6 +143,11 @@ module Callstack: sig
     with type t = callstack
      and module Hashtbl = Eva_types.Callstack.Hashtbl
 
+  (** [compare_lex] compares callstack lexicographically, slightly slower
+      than [compare] but in a more natural order, giving more importance
+      to the function at bottom of the callstack - the first functions called. *)
+  val compare_lex : t -> t -> int
+
   (* Constructor *)
   val init_global : Cil_types.varinfo -> t
   val init_local : ?thread:int -> Cil_types.kernel_function -> t
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 4a22d47031dc385f76e9856c0d396cd85b06df85..7de74799a42b21f38eacae8a5b63ab3f47cd1652 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -48,6 +48,11 @@ include Datatype.S_with_collections
   with type t = callstack
    and module Hashtbl = Eva_types.Callstack.Hashtbl
 
+(** [compare_lex] compares callstack lexicographically, slightly slower
+    than [compare] but in a more natural order, giving more importance
+    to the function at bottom of the callstack - the first functions called. *)
+val compare_lex : t -> t -> int
+
 (* Constructor *)
 val init_global : Cil_types.varinfo -> t
 val init_local : ?thread:int -> Cil_types.kernel_function -> t
diff --git a/src/plugins/nonterm/nonterm_run.ml b/src/plugins/nonterm/nonterm_run.ml
index 0f1ae23f1c88cc2b1ebb8609368dd7548ef4591d..176678b5e498016794add8061f174db1042246fd 100644
--- a/src/plugins/nonterm/nonterm_run.ml
+++ b/src/plugins/nonterm/nonterm_run.ml
@@ -328,7 +328,7 @@ let run () =
           let warned_kfs =
             Stmt.Hptset.fold (fun stmt acc ->
                 let cs = Hashtbl.find nonterm_stacks stmt in
-                let cs = List.sort Eva.Callstack.compare cs in
+                let cs = List.sort Eva.Callstack.compare_lex cs in
                 warn_nonterminating_statement stmt cs;
                 Kernel_function.Set.add (Kernel_function.find_englobing_kf stmt) acc
               ) new_nonterm_stmts Kernel_function.Set.empty