diff --git a/src/lib/dune b/src/lib/dune
index 0cf1a7cb24..aef40ae5a6 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -61,7 +61,7 @@
     Emap Gc_debug Hconsing Hstring Heap Lists Loc
     MyUnix Numbers Uqueue
     Options Timers Util Vec Version Steps Printer My_zip
-    Theories
+    Theories Nest
   )
 
  (js_of_ocaml
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 6f8d8c1179..99a1dc603d 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -556,10 +556,11 @@ and handle_ty_app ?(update = false) ty_c l =
 let mk_ty_decl (ty_c: DE.ty_cst) =
   match DT.definition ty_c with
   | Some (
-      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ }
+      Adt { cases = [| { cstr = { id_ty; _ } as cstr; dstrs; _ } |]; _ } as adt
     ) ->
     (* Records and adts that only have one case are treated in the same way,
        and considered as records. *)
+    Nest.add_nest [adt];
     let tyvl = Cache.store_ty_vars_ret id_ty in
     let rev_lbs =
       Array.fold_left (
@@ -580,9 +581,8 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in
     Cache.store_ty ty_c ty
 
-  | Some (
-      (Adt { cases; _ } as _adt)
-    ) ->
+  | Some ((Adt { cases; _ } as adt)) ->
+    Nest.add_nest [adt];
     let uid = Uid.of_dolmen ty_c in
     let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
     let rev_cs, is_enum =
@@ -594,7 +594,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
               if Array.length dstrs = 0
               then true
               else (
-                let ty = Ty.t_adt (Uid.of_dolmen ty_c) tyvl in
+                let ty = Ty.t_adt uid tyvl in
                 Cache.store_ty ty_c ty;
                 false
               )
@@ -681,10 +681,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       in
       Cache.store_ty ty_c ty
 
-    | Tadt (hs, tyl),
-      Some (
-        Adt { cases; ty = ty_c; _ }
-      ) ->
+    | Tadt (hs, tyl), Some (Adt { cases; ty = ty_c; _ }) ->
       let rev_cs =
         Array.fold_left (
           fun accl DE.{ cstr; dstrs; _ } ->
@@ -714,19 +711,21 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
     List.fold_left (
       fun (acc, ca) ty_c ->
         match DT.definition ty_c with
-        | Some (Adt { record; cases; _ }) as df
+        | Some (Adt { record; cases; _ } as df)
           when not record && Array.length cases > 1 ->
           df :: acc, true
-        | df -> df :: acc, ca
+        | Some (Adt _ as df) ->
+          df :: acc, ca
+        | Some Abstract | None ->
+          assert false
     ) ([], false) tdl
   in
+  Nest.add_nest rev_tdefs;
   let rev_l =
     List.fold_left (
       fun acc tdef ->
         match tdef with
-        | Some (
-            (DE.Adt { cases; record; ty = ty_c; }) as adt
-          ) ->
+        | DE.Adt { cases; record; ty = ty_c; } as adt ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
 
           let cns, is_enum =
@@ -754,8 +753,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             Cache.store_ty ty_c ty;
             (ty, Some adt) :: acc
           )
-        | None
-        | Some Abstract ->
+        | Abstract ->
           assert false (* unreachable in the second iteration *)
     ) [] (List.rev rev_tdefs)
   in
@@ -979,8 +977,7 @@ let rec mk_expr
 
           | B.Constructor _ ->
             let ty = dty_to_ty term_ty in
-            let sy = Sy.Op (Sy.Constr (Uid.of_dolmen tcst)) in
-            E.mk_term sy [] ty
+            E.mk_constr (Uid.of_dolmen tcst) [] ty
 
           | _ -> unsupported "Constant term %a" DE.Term.print term
         end
@@ -1349,7 +1346,7 @@ let rec mk_expr
             let ty = dty_to_ty term_ty in
             begin match ty with
               | Ty.Tadt (_, _) ->
-                let sy = Sy.Op (Sy.Constr (Uid.of_dolmen tcst)) in
+                let sy = Sy.constr @@ Uid.of_dolmen tcst in
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 E.mk_term sy l ty
               | Ty.Trecord _ ->
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 5e7b64b537..f6091d907d 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -401,12 +401,17 @@ module Shostak (X : ALIEN) = struct
 
 
   let assign_value _ _ _ =
-    Printer.print_err
-      "[ADTs.models] assign_value currently not implemented";
-    raise (Util.Not_implemented "Models for ADTs")
-
-  let to_model_term _r =
-    Printer.print_err
-      "[ADTs.models] to_model_term currently not implemented";
-    raise (Util.Not_implemented "Models for ADTs")
+    (* Model generation is performed by the case-split mechanism
+       in [Adt_rel]. *)
+    None
+
+  let to_model_term r =
+    match embed r with
+    | Constr { c_name; c_ty; c_args } ->
+      let args = Lists.try_map (fun (_, arg) -> X.to_model_term arg) c_args in
+      Option.bind args @@ fun args ->
+      Some (E.mk_constr c_name args c_ty)
+
+    | Select _ -> None
+    | Alien a -> X.to_model_term a
 end
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index c2a04e390d..af7d51914e 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -36,6 +36,15 @@ module LR = Uf.LX
 module Th = Shostak.Adt
 module SLR = Set.Make(LR)
 
+module TSet = Set.Make
+    (struct
+      type t = Uid.t
+
+      (* We use a dedicated total order on the constructors to ensure
+         the termination of the model generation. *)
+      let compare = Nest.compare
+    end)
+
 let timer = Timers.M_Adt
 
 module Domain = struct
@@ -43,27 +52,34 @@ module Domain = struct
      assigned to the semantic value has to use a constructor lying in the
      domain. *)
   type t = {
-    constrs : Uid.Set.t;
+    constrs : TSet.t;
     ex : Ex.t;
   }
 
   exception Inconsistent of Ex.t
 
+  let[@inline always] cardinal { constrs; _ } = TSet.cardinal constrs
+
+  let[@inline always] choose { constrs; _ } =
+    (* We choose the minimal element to ensure the termination of
+       model generation. *)
+    TSet.min_elt constrs
+
   let[@inline always] as_singleton { constrs; ex } =
-    if Uid.Set.cardinal constrs = 1 then
-      Some (Uid.Set.choose constrs, ex)
+    if TSet.cardinal constrs = 1 then
+      Some (TSet.choose constrs, ex)
     else
       None
 
   let domain ~constrs ex =
-    if Uid.Set.is_empty constrs then
+    if TSet.is_empty constrs then
       raise @@ Inconsistent ex
     else
       { constrs; ex }
 
-  let[@inline always] singleton ~ex c = { constrs = Uid.Set.singleton c; ex }
+  let[@inline always] singleton ~ex c = { constrs = TSet.singleton c; ex }
 
-  let[@inline always] subset d1 d2 = Uid.Set.subset d1.constrs d2.constrs
+  let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs
 
   let unknown ty =
     match ty with
@@ -73,31 +89,31 @@ module Domain = struct
       let constrs =
         List.fold_left
           (fun acc Ty.{ constr; _ } ->
-             Uid.Set.add constr acc
-          ) Uid.Set.empty body
+             TSet.add constr acc
+          ) TSet.empty body
       in
-      assert (not @@ Uid.Set.is_empty constrs);
+      assert (not @@ TSet.is_empty constrs);
       { constrs; ex = Ex.empty }
     | _ ->
       (* Only ADT values can have a domain. This case shouldn't happen since
          we check the type of semantic values in both [add] and [assume]. *)
       assert false
 
-  let equal d1 d2 = Uid.Set.equal d1.constrs d2.constrs
+  let equal d1 d2 = TSet.equal d1.constrs d2.constrs
 
   let pp ppf d =
     Fmt.(braces @@
-         iter ~sep:comma Uid.Set.iter Uid.pp) ppf d.constrs;
+         iter ~sep:comma TSet.iter Uid.pp) ppf d.constrs;
     if Options.(get_verbose () || get_unsat_core ()) then
       Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex
 
   let intersect ~ex d1 d2 =
-    let constrs = Uid.Set.inter d1.constrs d2.constrs in
+    let constrs = TSet.inter d1.constrs d2.constrs in
     let ex = ex |> Ex.union d1.ex |> Ex.union d2.ex in
     domain ~constrs ex
 
   let remove ~ex c d =
-    let constrs = Uid.Set.remove c d.constrs in
+    let constrs = TSet.remove c d.constrs in
     let ex = Ex.union ex d.ex in
     domain ~constrs ex
 end
@@ -209,6 +225,8 @@ module Domains = struct
         ) t.changed acc
     in
     acc, { t with changed = SX.empty }
+
+  let fold f t = MX.fold f t.domains
 end
 
 let calc_destructor d e uf =
@@ -327,7 +345,7 @@ let assume_th_elt t th_elt _ =
    This function alone isn't sufficient to produce a complete decision
    procedure for the ADT theory. For instance, let's assume we have three
    semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's
-   clear that `(distinct r1 r2 r3)` is unsatisfiable but we haven't enough
+   clear that `(distinct r1 r2 r3)` is unsatisfiable but we have not enough
    information to discover this contradiction.
 
    We plan to support model generation for ADT. As a by-product, we will got
@@ -566,45 +584,81 @@ let constr_of_destr ty d =
 
 exception Found of X.r * Uid.t
 
-(* Pick a delayed destructor application in [env.delayed]. Returns [None]
-   if there is no delayed destructor. *)
-let pick_delayed_destructor env =
-  try
-    Rel_utils.Delayed.iter_delayed
-      (fun r sy _e ->
-         match sy with
-         | Sy.Destruct d ->
-           raise_notrace @@ Found (r, d)
-         | _ ->
-           ()
-      ) env.delayed;
-    None
-  with Found (r, d) -> Some (r, d)
+let (let*) = Option.bind
 
-(* Do a case-split by choosing a semantic value [r] and constructor [c]
+(* Do a cases-plit by choosing a semantic value [r] and constructor [c]
    for which there are delayed destructor applications and propagate the
    literal [(not (_ is c) r)]. *)
+let split_delayed_destructor env =
+  if not @@ Options.get_enable_adts_cs () then
+    None
+  else
+    try
+      Rel_utils.Delayed.iter_delayed
+        (fun r sy _e ->
+           match sy with
+           | Sy.Destruct destr -> raise_notrace @@ Found (r, destr)
+           | _ -> ()
+        ) env.delayed;
+      None
+    with Found (r, d) ->
+      let c = constr_of_destr (X.type_info r) d in
+      Some (LR.mkv_builtin false (Sy.IsConstr c) [r])
+
+(* Pick a constructor in a tracked domain with minimal cardinal.
+   Returns [None] if there is no such constructor. *)
+let pick_best ds =
+  let* _, r, c =
+    Domains.fold
+      (fun r d best ->
+         let cd = Domain.cardinal d in
+         match Th.embed r, best with
+         | Constr _, _ -> best
+         | _, Some (n, _, _) when n <= cd -> best
+         | _ ->
+           let c = Domain.choose d in
+           Some (cd, r, c)
+      ) ds None
+  in
+  Some (r, c)
+
+let split_best_domain ~for_model uf =
+  if not for_model then
+    None
+  else
+    let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
+    let* r, c = pick_best ds in
+    let _, cons = Option.get @@ build_constr_eq r c in
+    (* In the current implementation of `X.make`, we produce
+       a nonempty context only for interpreted semantic values
+       of the `Arith` and `Records` theories. The semantic
+       values `cons` never involves such values. *)
+    let nr, ctx = X.make cons in
+    assert (Lists.is_empty ctx);
+    Some (LR.mkv_eq r nr)
+
+let next_case_split ~for_model env uf =
+  match split_delayed_destructor env with
+  | Some _ as r -> r
+  | None -> split_best_domain ~for_model uf
+
 let case_split env uf ~for_model =
-  if Options.get_disable_adts () || not (Options.get_enable_adts_cs())
-  then
+  if Options.get_disable_adts () then
     []
   else begin
-    assert (not for_model);
-    if Options.get_debug_adt () then
-      Debug.pp_domains "before cs"
-        (Uf.GlobalDomains.find (module Domains) (Uf.domains uf));
-    match pick_delayed_destructor env with
-    | Some (r, d) ->
-      if Options.get_debug_adt () then
+    match next_case_split ~for_model env uf with
+    | Some cs ->
+      if Options.get_debug_adt () then begin
+        Debug.pp_domains "before cs"
+          (Uf.GlobalDomains.find (module Domains) (Uf.domains uf));
         Printer.print_dbg ~flushed:false
           ~module_name:"Adt_rel" ~function_name:"case_split"
-          "found r = %a and d = %a@ " X.print r Uid.pp d;
-      (* CS on negative version would be better in general. *)
-      let c = constr_of_destr (X.type_info r) d in
-      let cs =  LR.mkv_builtin false (Sy.IsConstr c) [r] in
-      [ cs, true, Th_util.CS (Th_util.Th_adt, two) ]
+          "Assume %a" (Xliteral.print_view X.print) cs;
+      end;
+      [ cs, true, Th_util.CS (Th_util.Th_adt, two)]
     | None ->
-      Debug.no_case_split ();
+      if Options.get_debug_adt () then
+        Debug.no_case_split ();
       []
   end
 
diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index f8ddac6655..094cf510df 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -268,7 +268,7 @@ let tighten_domain rr nd domains =
    This function alone isn't sufficient to produce a complete decision
    procedure for the Enum theory. For instance, let's assume we have three
    semantic values [r1], [r2] and [r3] whose the domain is `{C1, C2}`. It's
-   clear that `(distinct r1 r2 r3)` is unsatisfiable but we haven't enough
+   clear that `(distinct r1 r2 r3)` is unsatisfiable but we have not enough
    information to discover this contradiction.
 
    Now, if we produce a case-split for one of these semantic values,
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index 2956b40ce0..3a56a50ba7 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -1275,10 +1275,6 @@ module Make (Th : Theory.S) = struct
     match Options.get_instantiation_heuristic () with
     | INormal ->
       (* TODO: check if this test still produces a wrong model. *)
-      (* S: This seems spurious!
-         On example UFDT/20170428-Barrett/cdt-cade2015/data/gandl/cotree/
-         x2015_09_10_16_49_52_978_1009894.smt_in.smt2,
-         this returns a wrong model. *)
       update_model_and_return_unknown
         env (Options.get_last_interpretation ())
         ~unknown_reason:Incomplete (* may becomes ModelGen *)
@@ -1885,7 +1881,8 @@ module Make (Th : Theory.S) = struct
     Expr.reinit_cache ();
     Hstring.reinit_cache ();
     Shostak.Combine.reinit_cache ();
-    Uf.reinit_cache ()
+    Uf.reinit_cache ();
+    Nest.reinit ()
 
   let () =
     Steps.save_steps ();
diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index c797d3ea94..87244a43d9 100644
--- a/src/lib/reasoners/satml.ml
+++ b/src/lib/reasoners/satml.ml
@@ -143,7 +143,7 @@ end
 module MFF = FF.Map
 module SFF = FF.Set
 
-module Vheap = Heap.Make(struct
+module Vheap = Heap.MakeRanked(struct
     type t = Atom.var
 
     let index (a : t) = a.hindex
@@ -478,7 +478,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
       simpDB_props = 0;
 
-      order = Vheap.make 0 Atom.dummy_var; (* sera mis a jour dans solve *)
+      order = Vheap.create 0 Atom.dummy_var; (* sera mis a jour dans solve *)
 
       progress_estimate = 0.;
 
@@ -1827,7 +1827,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
           env.next_split <- None;
           pick_branch_aux env atom
         | None ->
-          match Vheap.remove_min env.order with
+          match Vheap.pop_min env.order with
           | v -> pick_branch_aux env v.na
           | exception Not_found ->
             if Options.get_cdcl_tableaux_inst () then
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index aaf94087ef..0a3ed11f7a 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1393,7 +1393,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     Expr.reinit_cache ();
     Hstring.reinit_cache ();
     Shostak.Combine.reinit_cache ();
-    Uf.reinit_cache ()
+    Uf.reinit_cache ();
+    Nest.reinit ()
 
   let () =
     Steps.save_steps ();
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index 7a97695997..898070ff53 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -440,7 +440,8 @@ struct
     not (Options.get_restricted ()) &&
     (RECORDS.is_mine_symb sb ty ||
      BITV.is_mine_symb sb ty ||
-     ENUM.is_mine_symb sb ty)
+     ENUM.is_mine_symb sb ty ||
+     ADT.is_mine_symb sb ty)
 
   let is_a_leaf r = match r.v with
     | Term _ | Ac _ -> true
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 9c0a59ee5c..7b51a8fc6a 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -525,7 +525,7 @@ module Main_Default : S = struct
     let r =
       try
         if t.choices == [] then
-          (* We haven't make choice yet. Initialize the environment
+          (* We have not make choice yet. Initialize the environment
              [gamma_finite] with [gamma]. *)
           let t = reset_case_split_env t in
           look_for_sat ~for_model t [] []
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 69759a5a84..4774e072d9 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1163,6 +1163,10 @@ type cache = {
       to ensure we don't generate twice an abstract value for a given symbol. *)
 }
 
+let is_destructor = function
+  | Sy.Op (Destruct _) -> true
+  | _ -> false
+
 (* The environment of the union-find contains almost a first-order model.
    There are two situations that require some computations to retrieve an
    appropriate model value:
@@ -1179,9 +1183,13 @@ let compute_concrete_model_of_val cache =
   and get_abstract_for = Cache.get_abstract_for cache.abstracts
   in fun env t ((mdl, mrepr) as acc) ->
     let { E.f; xs; ty; _ } = E.term_view t in
-    if X.is_solvable_theory_symbol f ty
-    || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t
-    || E.equal t E.vrai || E.equal t E.faux
+    (* TODO: We have to filter out destructors here as we don't consider
+       pending destructors as solvable theory symbols of the ADT theory.
+       We should check if these symbols can be defined as solvable to
+       remove this particular case here. *)
+    if X.is_solvable_theory_symbol f ty || is_destructor f
+       || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t
+       || E.equal t E.vrai || E.equal t E.faux
     then
       (* These terms are built-in interpreted ones and we don't have
          to produce a definition for them. *)
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 7c64153965..d433db81e6 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -144,7 +144,7 @@ let bitv s =
         | _ -> assert false) Z.zero s
   in Bitv (String.length s, biv)
 let real r = Real (Q.of_string r)
-let constr s = Op (Constr s)
+let constr c = Op (Constr c)
 let destruct s = Op (Destruct s)
 
 let mk_bound kind sort ~is_open ~is_lower =
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
index 801d7bd15b..de7909ca69 100644
--- a/src/lib/structures/uid.mli
+++ b/src/lib/structures/uid.mli
@@ -30,7 +30,9 @@
 
 module DE = Dolmen.Std.Expr
 
-type t
+type t = private
+  | Hstring : Hstring.t -> t
+  | Dolmen : 'a DE.id -> t
 
 val of_dolmen : 'a DE.Id.t -> t
 val of_string : string -> t
diff --git a/src/lib/util/heap.ml b/src/lib/util/heap.ml
index 44f7f61991..da5e77aad0 100644
--- a/src/lib/util/heap.ml
+++ b/src/lib/util/heap.ml
@@ -35,33 +35,7 @@ module type RankedType = sig
   val compare : t -> t -> int
 end
 
-module type S = sig
-  type elt
-
-  type t
-
-  val make : int -> elt -> t
-
-  val in_heap : elt -> bool
-
-  val decrease : t -> elt -> unit
-
-  val increase : t -> elt -> unit
-
-  val size : t -> int
-
-  val is_empty : t -> bool
-
-  val insert : t -> elt -> unit
-
-  val grow_to_by_double : t -> int -> unit
-
-  val remove_min : t -> elt
-
-  val filter : t -> (elt -> bool) -> unit
-end
-
-module Make(Rank : RankedType) = struct
+module MakeRanked(Rank : RankedType) = struct
   type elt = Rank.t
 
   type t = { heap : elt Vec.t } [@@unboxed]
@@ -69,7 +43,7 @@ module Make(Rank : RankedType) = struct
   (* Negative value; used to indicate an element is not in the heap *)
   let absent = -1
 
-  let make sz dummy = { heap = Vec.make ~dummy sz }
+  let create sz dummy = { heap = Vec.make ~dummy sz }
 
   let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
   let[@inline] right i = (i + 1) lsl 1 (* (i + 1) * 2*)
@@ -148,7 +122,7 @@ module Make(Rank : RankedType) = struct
   let[@inline] grow_to_by_double { heap } sz =
     Vec.grow_to_by_double heap sz
 
-  let remove_min ({ heap } as s) =
+  let pop_min ({ heap } as s) =
     match Vec.size heap with
     | 0 -> raise Not_found
     | 1 ->
@@ -165,3 +139,36 @@ module Make(Rank : RankedType) = struct
       if Vec.size s.heap > 1 then percolate_down s y;
       x
 end
+
+module type OrderedTypeDefault = sig
+  type t
+
+  val compare : t -> t -> int
+
+  val default : t
+end
+
+module MakeOrdered(V : OrderedTypeDefault) = struct
+  type entry = { value : V.t ; mutable index : int }
+  type elt = V.t
+
+  module H = MakeRanked
+      (struct
+        type t = entry
+
+        let index e = e.index
+
+        let set_index e i = e.index <- i
+
+        let compare x y = V.compare x.value y.value
+      end)
+
+  let entry value = { value ; index = -1 }
+
+  type t = H.t
+
+  let create n = H.create n (entry V.default)
+  let is_empty = H.is_empty
+  let insert h v = H.insert h (entry v)
+  let pop_min h = (H.pop_min h).value
+end
diff --git a/src/lib/util/heap.mli b/src/lib/util/heap.mli
index 388db8c4c4..d532b1ee91 100644
--- a/src/lib/util/heap.mli
+++ b/src/lib/util/heap.mli
@@ -62,13 +62,14 @@ end
 
 (** {2 Priority heaps} *)
 
-module type S = sig
-  type elt
+module MakeRanked(Rank : RankedType) : sig
+  type elt = Rank.t
+  (** The type of elements of the heap. *)
 
   type t
   (** The type of heaps. *)
 
-  val make : int -> elt -> t
+  val create : int -> elt -> t
   (** Create a heap with the given initial size and dummy element. *)
 
   val in_heap : elt -> bool
@@ -87,13 +88,13 @@ module type S = sig
   (** Is the heap empty ? *)
 
   val insert : t -> elt -> unit
-  (** Inset a new element in the heap. *)
+  (** Insert a new element in the heap. *)
 
   val grow_to_by_double: t -> int -> unit
   (** Grow the size of the heap by multiplying it by 2
       until it is at least the size specified. *)
 
-  val remove_min : t -> elt
+  val pop_min : t -> elt
   (** Remove the minimum element from the heap and return it.
 
       @raise Not_found if the heap is empty. *)
@@ -102,4 +103,35 @@ module type S = sig
   (** Filter elements in the heap. *)
 end
 
-module Make(Rank : RankedType) : S with type elt = Rank.t
+(** {2 Ordered priority heaps} *)
+
+module type OrderedTypeDefault = sig
+  type t
+
+  val compare : t -> t -> int
+
+  val default : t
+  (** Dummy value used in the heap. *)
+end
+
+module MakeOrdered(V : OrderedTypeDefault) : sig
+  type elt = V.t
+  (** The type of elements of the heap. *)
+
+  type t
+  (** The type of heaps. *)
+
+  val create : int -> t
+  (** Create a heap with the given initial size. *)
+
+  val is_empty : t -> bool
+  (** Is the heap empty ? *)
+
+  val insert : t -> elt -> unit
+  (** Insert a new element in the heap. *)
+
+  val pop_min : t -> elt
+  (** Remove the minimum element from the heap and return it.
+
+      @raise Not_found if the heap is empty. *)
+end
diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml
new file mode 100644
index 0000000000..ac42686f82
--- /dev/null
+++ b/src/lib/util/nest.ml
@@ -0,0 +1,186 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) 2024 --- OCamlPro SAS                                *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+module DStd = Dolmen.Std
+module DE = DStd.Expr
+module DT = DE.Ty
+module B = Dolmen.Std.Builtin
+
+type t = Dolmen.Std.Expr.ty_def list
+
+(* A nest is the set of all the constructors of a mutually recursive definition
+   of ADTs.
+
+   For each type ty of a nest, we denote by S(ty) the set of all the
+   constructors of this type in this nest and G(ty) the set of the constructors
+   with an argument of type ty in this nest.
+
+   Recall that a (directed) hypergraph is a set of nodes and hyperedges between
+   subsets of these nodes.
+
+   To generate our total order of a nest, we build in [build_graph] a hypergraph
+   where:
+   - the nodes are all the constructors of the nest;
+   - for all type ty of the nest, there is a hyperedge from S(ty) to G(ty).
+
+   In particular, our graph has exactly one outgoing hyperedge per node. *)
+
+(* Node of the hypergraph. *)
+type node = {
+  id : DE.term_cst;
+  (* Dolmen constructor identifier. *)
+
+  weight : int;
+  (* This weight is used to prioritize constructors with less destructors
+     during the sorting (see [add_nest]). *)
+
+  mutable outgoing : edge;
+  (* Hyperedge from a subset S in S(ty) to a subset G in G(ty) where ty is
+     the type of [id]. At the beginning, we have S = S(ty) and G = G(ty).
+
+     One use a double indirection because this hyperedge is shared between
+     all the elements of S. *)
+
+  mutable in_degree : int;
+  (* Number of hyperedges into this constructor. *)
+}
+
+(* Type of a hyperedge. *)
+and edge = node list ref
+
+module Hp =
+  Heap.MakeOrdered
+    (struct
+      type t = node
+      let compare { weight = w1; _ } { weight = w2; _ } = w1 - w2
+
+      let default =
+        let dummy_edge : node list ref = ref [] in
+        {
+          id = DE.Term.Const.Int.int "0" (* dummy *);
+          outgoing = dummy_edge;
+          in_degree = -1;
+          weight = -1;
+        }
+    end)
+
+let (let*) = Option.bind
+
+(* Return the type definition of the return type of the destructor [dstr]. *)
+let def_of_dstr dstr =
+  let* ty_cst =
+    match dstr with
+    | DE.{ builtin = B.Destructor _; id_ty; _ } ->
+      begin match DT.view id_ty with
+        | `Arrow (_, ty) ->
+          begin match DT.view ty with
+            | `App (`Generic ty_cst, _) -> Some ty_cst
+            | _ -> None
+          end
+        | _ -> None
+      end
+    | _ -> assert false
+  in
+  DT.definition ty_cst
+
+(* Build the hypergraph of dependencies between the constructors of the
+   nest [defs].
+
+   @return a heap that contains all the nodes of this graph without ingoing
+   hyperedges. *)
+let build_graph (defs : DE.ty_def list) : Hp.t =
+  let map : (DE.ty_def, edge) Hashtbl.t = Hashtbl.create 17 in
+  let hp : Hp.t = Hp.create 17 in
+  List.iter (fun d -> Hashtbl.add map d (ref [])) defs;
+  List.iter
+    (fun def ->
+       match def with
+       | DE.Abstract -> assert false
+       | DE.Adt { cases; _ } ->
+         Array.iter
+           (fun DE.{ cstr; dstrs; _ } ->
+              let node = {
+                id = cstr;
+                outgoing = Hashtbl.find map def;
+                in_degree = -1; (* dummy value *)
+                weight = Array.length dstrs
+              }
+              in
+              let in_degree =
+                Array.fold_left
+                  (fun acc dstr ->
+                     match Option.bind dstr def_of_dstr with
+                     | Some d ->
+                       begin match Hashtbl.find map d with
+                         | edge -> edge := node :: !edge; acc + 1
+                         | exception Not_found -> acc
+                       end
+                     | None -> acc
+                  ) 0 dstrs
+              in
+              node.in_degree <- in_degree;
+              if in_degree = 0 then Hp.insert hp node
+           ) cases
+    ) defs;
+  hp
+
+module H = Hashtbl.Make (Uid)
+
+(* Internal state used to store the current order. *)
+let add_cstr, find_weight, reinit =
+  let ctr = ref 0 in
+  let order : int H.t = H.create 100 in
+  let add_cstr cstr =
+    H.add order cstr !ctr;
+    incr ctr
+  and find_weight cstr =
+    try
+      H.find order cstr
+    with Not_found ->
+      Fmt.failwith "cannot find uid %a" Uid.pp cstr
+  and reinit () =
+    ctr := 0;
+    H.clear order
+  in add_cstr, find_weight, reinit
+
+(* Sort the constructors of the nest using a sorting based on
+   Kahn's algorithm. *)
+let add_nest n =
+  let hp = build_graph n in
+  while not @@ Hp.is_empty hp do
+    (* Loop invariant: the set of nodes in heap [hp] is exactly
+       the set of the nodes of the graph without ingoing hyperedge. *)
+    let { id; outgoing; in_degree; _ } = Hp.pop_min hp in
+    add_cstr @@ Uid.of_dolmen id;
+    assert (in_degree = 0);
+    List.iter
+      (fun node ->
+         assert (node.in_degree > 0);
+         node.in_degree <- node.in_degree - 1;
+         if node.in_degree = 0 then
+           Hp.insert hp node
+      ) !outgoing;
+    outgoing := [];
+  done
+
+let compare (id1 : Uid.t) (id2 : Uid.t) =
+  match id1, id2 with
+  | Dolmen _, Dolmen _ ->
+    find_weight id1 - find_weight id2
+  | _ ->
+    Uid.compare id1 id2
diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli
new file mode 100644
index 0000000000..47777be59e
--- /dev/null
+++ b/src/lib/util/nest.mli
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) 2024 --- OCamlPro SAS                                *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     ---------------------------------------------------------------    *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+module DE = Dolmen.Std.Expr
+
+(** The purpose of this module is to construct a total order on ADT
+    constructors to ensure the termination of model generation for
+    this theory.
+
+    By nest, we mean the set of all the constructors in a mutually
+    recursive definition of ADTs.
+
+    Before comparing constructors with [compare], the complete
+    nest to which they belong have to be added with [add_nest]. *)
+
+type t = DE.ty_def list
+(** Type of nest. *)
+
+val add_nest : t -> unit
+(** [add_nest defs] sorts and adds the nest [defs] in the current
+    internal order.
+
+    {b Note:} Assume that [defs] is a complete nest (in any order). *)
+
+val compare : Uid.t -> Uid.t -> int
+(** [compare id1 id2] compares the constructors [id1] and [id2] with
+    the order generated by [add_nest] if they are both Dolmen identifiers.
+
+    @raise Failure if the nests of the constructors [id1] and [id2] have not
+                   been added with [add_nest] before. *)
+
+val reinit : unit -> unit
+(** [reinit ()] clears all the registered constructors by [add_nest]. *)
diff --git a/tests/dune.inc b/tests/dune.inc
index 70477ddb97..88dec1477f 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -194871,6 +194871,137 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir models/adt
+  (rule
+   (target small.models_dolmen.output)
+   (deps (:input small.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps small.models_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff small.models.expected small.models_dolmen.output)))
+  (rule
+   (target rec3.models_dolmen.output)
+   (deps (:input rec3.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps rec3.models_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff rec3.models.expected rec3.models_dolmen.output)))
+  (rule
+   (target rec2.models_dolmen.output)
+   (deps (:input rec2.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps rec2.models_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff rec2.models.expected rec2.models_dolmen.output)))
+  (rule
+   (target rec.models_dolmen.output)
+   (deps (:input rec.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps rec.models_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff rec.models.expected rec.models_dolmen.output)))
+  (rule
+   (target list.models_dolmen.output)
+   (deps (:input list.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps list.models_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff list.models.expected list.models_dolmen.output)))
+  (rule
+   (target arith.models_dolmen.output)
+   (deps (:input arith.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps arith.models_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff arith.models.expected arith.models_dolmen.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir models/arith
   (rule
diff --git a/tests/models/adt/arith.models.expected b/tests/models/adt/arith.models.expected
new file mode 100644
index 0000000000..7da79872d1
--- /dev/null
+++ b/tests/models/adt/arith.models.expected
@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun a () Data (cons1 2.0 0.0))
+  (define-fun b () Data (cons3 0.0))
+  (define-fun x () Real 2.0)
+  (define-fun y () Real 0.0)
+)
diff --git a/tests/models/adt/arith.models.smt2 b/tests/models/adt/arith.models.smt2
new file mode 100644
index 0000000000..e1bb697759
--- /dev/null
+++ b/tests/models/adt/arith.models.smt2
@@ -0,0 +1,18 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatype Data (
+  (cons1 (d1 Real) (d2 Real))
+  (cons2)
+  (cons3 (d3 Real))
+))
+(declare-const a Data)
+(declare-const b Data)
+(declare-const x Real)
+(declare-const y Real)
+(assert ((_ is cons1) a))
+(assert ((_ is cons3) b))
+(assert (= (d1 a) x))
+(assert (= (d3 b) y))
+(assert (= (d1 a) (- 2 (d3 b))))
+(check-sat)
+(get-model)
diff --git a/tests/models/adt/list.models.expected b/tests/models/adt/list.models.expected
new file mode 100644
index 0000000000..07eb25ebba
--- /dev/null
+++ b/tests/models/adt/list.models.expected
@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun a () List empty)
+  (define-fun b () List empty)
+  (define-fun c () List (cons 0 empty))
+  (define-fun d () List empty)
+)
diff --git a/tests/models/adt/list.models.smt2 b/tests/models/adt/list.models.smt2
new file mode 100644
index 0000000000..33dda60ccf
--- /dev/null
+++ b/tests/models/adt/list.models.smt2
@@ -0,0 +1,15 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatype List (
+  (empty)
+  (cons (head Int) (tail List))
+))
+(declare-const a List)
+(declare-const b List)
+(declare-const c List)
+(declare-const d List)
+(assert (= (tail a) b))
+(assert ((_ is cons) c))
+(assert (= (tail c) d))
+(check-sat)
+(get-model)
diff --git a/tests/models/adt/rec.models.expected b/tests/models/adt/rec.models.expected
new file mode 100644
index 0000000000..3cac54112e
--- /dev/null
+++ b/tests/models/adt/rec.models.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun a () data (cons1 cons2))
+)
diff --git a/tests/models/adt/rec.models.smt2 b/tests/models/adt/rec.models.smt2
new file mode 100644
index 0000000000..d724e94f5b
--- /dev/null
+++ b/tests/models/adt/rec.models.smt2
@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatype data (
+  (cons1 (d1 data))
+  (cons2)
+))
+(declare-const a data)
+(assert ((_ is cons1) a))
+(check-sat)
+(get-model)
diff --git a/tests/models/adt/rec2.models.expected b/tests/models/adt/rec2.models.expected
new file mode 100644
index 0000000000..d5a224aa49
--- /dev/null
+++ b/tests/models/adt/rec2.models.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun a () data1 (cons1 (cons2 cons4)))
+)
diff --git a/tests/models/adt/rec2.models.smt2 b/tests/models/adt/rec2.models.smt2
new file mode 100644
index 0000000000..511d9a5a83
--- /dev/null
+++ b/tests/models/adt/rec2.models.smt2
@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes ((data1 0) (data2 0)) (
+  ((cons1 (d1 data1)) (cons2 (d2 data2)))
+  ((cons3 (d3 data1)) (cons4))
+))
+(declare-const a data1)
+(assert ((_ is cons1) a))
+(check-sat)
+(get-model)
diff --git a/tests/models/adt/rec3.models.expected b/tests/models/adt/rec3.models.expected
new file mode 100644
index 0000000000..2714125021
--- /dev/null
+++ b/tests/models/adt/rec3.models.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun a () data1 (cons1 (cons2 (cons4 0 1))))
+)
diff --git a/tests/models/adt/rec3.models.smt2 b/tests/models/adt/rec3.models.smt2
new file mode 100644
index 0000000000..6b23dc3f0d
--- /dev/null
+++ b/tests/models/adt/rec3.models.smt2
@@ -0,0 +1,10 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes ((data1 0) (data2 0)) (
+  ((cons1 (d1 data1)) (cons2 (d2 data2)))
+  ((cons3 (d3 data1)) (cons4 (d4 Int) (d5 Int)))
+))
+(declare-const a data1)
+(assert ((_ is cons1) a))
+(check-sat)
+(get-model)
diff --git a/tests/models/adt/small.models.expected b/tests/models/adt/small.models.expected
new file mode 100644
index 0000000000..a0f6a5ba55
--- /dev/null
+++ b/tests/models/adt/small.models.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun a () data1 (cons1 (cons2 (cons5 false))))
+)
diff --git a/tests/models/adt/small.models.smt2 b/tests/models/adt/small.models.smt2
new file mode 100644
index 0000000000..b03dd5902a
--- /dev/null
+++ b/tests/models/adt/small.models.smt2
@@ -0,0 +1,11 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes ((data1 0) (data2 0)) (
+  ((cons1 (d1 data1)) (cons2 (d2 data2)))
+  ((cons3 (d3 data1)) (cons4 (d4 Int) (d5 Int) (d6 Bool))
+                      (cons5 (d7 Bool)))
+))
+(declare-const a data1)
+(assert ((_ is cons1) a))
+(check-sat)
+(get-model)