diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 78b301fdbe..3fe1c22d5b 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -101,20 +101,13 @@ module Cache = struct
   let find_ty id =
     HT.find ae_ty_ht (Id id)
 
-  let fresh_ty ?(is_var = true) ?id () =
+  let fresh_ty ?(is_var = true) () =
     if is_var
     then Ty.fresh_tvar ()
-    else
-      match id with
-      | Some id -> Ty.text [] (Uid.of_dolmen id)
-      | None -> Ty.fresh_empty_text ()
-
-  let update_ty_store ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id () in
-    store_ty id ty
+    else Ty.fresh_empty_text ()
 
   let update_ty_store_ret ?(is_var = true) id =
-    let ty = fresh_ty ~is_var ~id () in
+    let ty = fresh_ty ~is_var () in
     store_ty id ty;
     ty
 
@@ -125,7 +118,8 @@ module Cache = struct
       update_ty_store_ret ~is_var id
 
   let store_tyv ?(is_var = true) t_v =
-    update_ty_store ~is_var t_v
+    let ty = fresh_ty ~is_var () in
+    store_ty t_v ty
 
   let store_tyvl ?(is_var = true) (tyvl: DE.ty_var list) =
     List.iter (store_tyv ~is_var) tyvl
@@ -585,11 +579,13 @@ 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; _ } |]; _ } as adt
+      (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];
+    Nest.attach_orders [adt];
+    let uid = Uid.of_ty_cst ty_c in
     let tyvl = Cache.store_ty_vars_ret id_ty in
     let rev_lbs =
       Array.fold_left (
@@ -597,7 +593,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
           match c with
           | Some (DE.{ id_ty; _ } as id) ->
             let pty = dty_to_ty id_ty in
-            (Uid.of_dolmen id, pty) :: acc
+            (Uid.of_term_cst id, pty) :: acc
           | _ ->
             Fmt.failwith
               "Unexpected null label for some field of the record type %a"
@@ -606,13 +602,13 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
       ) [] dstrs
     in
     let lbs = List.rev rev_lbs in
-    let record_constr = Uid.of_dolmen cstr in
-    let ty = Ty.trecord ~record_constr tyvl (Uid.of_dolmen ty_c) lbs in
+    let record_constr = Uid.of_term_cst cstr in
+    let ty = Ty.trecord ~record_constr tyvl uid lbs in
     Cache.store_ty ty_c ty
 
   | Some (Adt { cases; _ } as adt) ->
-    Nest.add_nest [adt];
-    let uid = Uid.of_dolmen ty_c in
+    Nest.attach_orders [adt];
+    let uid = Uid.of_ty_cst ty_c in
     let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
     Cache.store_ty ty_c (Ty.t_adt uid tyvl);
     let rev_cs =
@@ -623,11 +619,11 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
               fun acc tc_o ->
                 match tc_o with
                 | Some (DE.{ id_ty; _ } as field) ->
-                  (Uid.of_dolmen field, dty_to_ty id_ty) :: acc
+                  (Uid.of_term_cst field, dty_to_ty id_ty) :: acc
                 | None -> assert false
             ) [] dstrs
           in
-          (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+          (Uid.of_term_cst cstr, List.rev rev_fields) :: accl
       ) [] cases
     in
     let body = Some (List.rev rev_cs) in
@@ -638,7 +634,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     let ty_params = []
     (* List.init ty_c.id_ty.arity (fun _ -> Ty.fresh_tvar ()) *)
     in
-    let ty = Ty.text ty_params (Uid.of_dolmen ty_c) in
+    let ty = Ty.text ty_params (Uid.of_ty_cst ty_c) in
     Cache.store_ty ty_c ty
 
 (** Handles term declaration by storing the eventual present type variables
@@ -678,7 +674,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             match c with
             | Some (DE.{ id_ty; _ } as id) ->
               let pty = dty_to_ty id_ty in
-              (Uid.of_dolmen id, pty) :: acc
+              (Uid.of_term_cst id, pty) :: acc
             | _ ->
               Fmt.failwith
                 "Unexpected null label for some field of the record type %a"
@@ -700,11 +696,11 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
                 fun acc tc_o ->
                   match tc_o with
                   | Some (DE.{ id_ty; _ } as id) ->
-                    (Uid.of_dolmen id, dty_to_ty id_ty) :: acc
+                    (Uid.of_term_cst id, dty_to_ty id_ty) :: acc
                   | None -> assert false
               ) [] dstrs
             in
-            (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+            (Uid.of_term_cst cstr, List.rev rev_fields) :: accl
         ) [] cases
       in
       let body = Some (List.rev rev_cs) in
@@ -729,18 +725,19 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
           assert false
     ) ([], false) tdl
   in
-  Nest.add_nest rev_tdefs;
+  Nest.attach_orders rev_tdefs;
   let rev_l =
     List.fold_left (
       fun acc tdef ->
         match tdef with
         | DE.Adt { cases; record; ty = ty_c; } as adt ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
-          let uid = Uid.of_dolmen ty_c in
+          let uid = Uid.of_ty_cst ty_c in
+          let record_constr = Uid.of_term_cst cases.(0).cstr in
           let ty =
             if (record || Array.length cases = 1) && not contains_adts
             then
-              Ty.trecord ~record_constr:uid tyvl uid []
+              Ty.trecord ~record_constr tyvl uid []
             else
               Ty.t_adt uid tyvl
           in
@@ -793,7 +790,7 @@ let mk_pattern DE.{ term_descr; _ } =
           Array.fold_left (
             fun acc v ->
               match v with
-              | Some dstr -> Uid.of_dolmen dstr :: acc
+              | Some dstr -> Uid.of_term_cst dstr :: acc
               | _ -> assert false
           ) [] dstrs
         | _ ->
@@ -811,10 +808,10 @@ let mk_pattern DE.{ term_descr; _ } =
       ) [] (List.rev rev_vnames) pargs
     in
     let args = List.rev rev_args in
-    Typed.Constr {name = Uid.of_dolmen cst; args}
+    Typed.Constr {name = Uid.of_term_cst cst; args}
 
   | Cst ({ builtin = B.Constructor _; _ } as cst) ->
-    Typed.Constr {name = Uid.of_dolmen cst; args = []}
+    Typed.Constr {name = Uid.of_term_cst cst; args = []}
 
   | Var ({ builtin = B.Base; path; _ } as t_v) ->
     (* Should the type be passed as an argument
@@ -974,7 +971,7 @@ let rec mk_expr
               | Trecord _ as ty ->
                 E.mk_record [] ty
               | Tadt _ as ty ->
-                E.mk_constr (Uid.of_dolmen tcst) [] ty
+                E.mk_constr (Uid.of_term_cst tcst) [] ty
               | ty ->
                 Fmt.failwith "unexpected type %a@." Ty.print ty
             end
@@ -1019,9 +1016,9 @@ let rec mk_expr
                     let sy =
                       match Cache.find_ty adt with
                       | Trecord _ ->
-                        Sy.Op (Sy.Access (Uid.of_dolmen destr))
+                        Sy.Op (Sy.Access (Uid.of_term_cst destr))
                       | Tadt _ ->
-                        Sy.destruct (Uid.of_dolmen destr)
+                        Sy.destruct (Uid.of_term_cst destr)
                       | _ -> assert false
                     in
                     E.mk_term sy [e] ty
@@ -1041,7 +1038,7 @@ let rec mk_expr
               cstr = { builtin = B.Constructor { adt; _ }; _ } as cstr; _
             }, [x] ->
             begin
-              let builtin = Sy.IsConstr (Uid.of_dolmen cstr) in
+              let builtin = Sy.IsConstr (Uid.of_term_cst cstr) in
               let ty_c =
                 match DT.definition adt with
                 | Some (
@@ -1326,9 +1323,8 @@ let rec mk_expr
             let ty = dty_to_ty term_ty in
             begin match ty with
               | Ty.Tadt _ ->
-                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
+                E.mk_constr (Uid.of_term_cst tcst) l ty
               | Ty.Trecord _ ->
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 E.mk_record l ty
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 3c8f971e5f..fddbe43b5b 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -190,12 +190,12 @@ module Types = struct
     let rec check_duplicates s = function
       | [] -> ()
       | (lb, _) :: l ->
-        if Uid.Set.mem lb s then
+        if Uid.Term_set.mem lb s then
           Errors.typing_error
             (DuplicateLabel (Hstring.make @@ Uid.show lb)) loc;
-        check_duplicates (Uid.Set.add lb s) l
+        check_duplicates (Uid.Term_set.add lb s) l
     in
-    check_duplicates Uid.Set.empty lbs;
+    check_duplicates Uid.Term_set.empty lbs;
     match ty with
     | Ty.Trecord { Ty.lbs = l; _ } ->
       if List.length lbs <> List.length l then
@@ -586,32 +586,34 @@ let check_no_duplicates =
 let filter_patterns pats ty_body _loc =
   let cases =
     List.fold_left
-      (fun s {Ty.constr=c; _} -> Uid.Set.add c s) Uid.Set.empty ty_body
+      (fun s {Ty.constr=c; _} -> Uid.Term_set.add c s)
+      Uid.Term_set.empty ty_body
   in
   let missing, filtered_pats, dead =
     List.fold_left
       (fun (miss, filtered_pats, dead) ((p, _) as u) ->
          match p with
          | Constr { name; _ } ->
-           assert (Uid.Set.mem name cases); (* pattern is well typed *)
-           if Uid.Set.mem name miss then (* not encountered yet *)
-             Uid.Set.remove name miss, u :: filtered_pats, dead
+           assert (Uid.Term_set.mem name cases); (* pattern is well typed *)
+           if Uid.Term_set.mem name miss then (* not encountered yet *)
+             Uid.Term_set.remove name miss, u :: filtered_pats, dead
            else (* case already seen --> dead pattern *)
              miss, pats, p :: dead
          | Var _ ->
-           if Uid.Set.is_empty miss then
+           if Uid.Term_set.is_empty miss then
              (* match already exhaussive -> dead case *)
              miss, filtered_pats, p :: dead
            else (* covers all remaining cases, miss becomes empty *)
-             Uid.Set.empty, u :: filtered_pats, dead
+             Uid.Term_set.empty, u :: filtered_pats, dead
       )(cases, [], []) pats
   in
   missing, List.rev filtered_pats, dead
 
 let check_pattern_matching missing dead loc =
-  if not (Uid.Set.is_empty missing) then begin
+  if not (Uid.Term_set.is_empty missing) then begin
     let missing =
-      List.map (fun m -> Hstring.make @@ Uid.show m) (Uid.Set.elements missing)
+      List.map (fun m -> Hstring.make @@ Uid.show m)
+        (Uid.Term_set.elements missing)
     in
     Errors.typing_error (MatchNotExhaustive missing) loc end;
   if dead != [] then
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 834ea2ce31..8ce4dad0ac 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -28,12 +28,17 @@
 module Sy = Symbols
 module E  = Expr
 
+
 type 'a abstract =
-  | Constr of { c_name : Uid.t ; c_ty : Ty.t ; c_args : (Uid.t * 'a) list }
+  | Constr of {
+      c_name : Uid.term_cst;
+      c_ty : Ty.t;
+      c_args : (Uid.term_cst * 'a) list
+    }
   (* [Cons { c_name; c_ty; c_args }] reprensents the application of the
      constructor [c_name] of the ADT [ty] with the arguments [c_args]. *)
 
-  | Select of { d_name : Uid.t ; d_ty : Ty.t ; d_arg : 'a }
+  | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a }
   (* [Select { d_name; d_ty; d_arg }] represents the destructor [d_name] of
      the ADT [d_ty] on the ADT value [d_arg]. *)
 
diff --git a/src/lib/reasoners/adt.mli b/src/lib/reasoners/adt.mli
index b90e978db4..81d7267b5d 100644
--- a/src/lib/reasoners/adt.mli
+++ b/src/lib/reasoners/adt.mli
@@ -26,9 +26,13 @@
 (**************************************************************************)
 
 type 'a abstract =
-  | Constr of
-      { c_name : Uid.t ; c_ty : Ty.t ; c_args : (Uid.t * 'a) list }
-  | Select of { d_name : Uid.t ; d_ty : Ty.t ; d_arg : 'a }
+  | Constr of {
+      c_name : Uid.term_cst;
+      c_ty : Ty.t;
+      c_args : (Uid.term_cst * 'a) list
+    }
+
+  | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a }
 
   | Alien of 'a
 
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 18eb871b3f..ff30c40264 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -36,13 +36,19 @@ module LR = Uf.LX
 module Th = Shostak.Adt
 module SLR = Set.Make(LR)
 
-module TSet = Set.Make
+module DE = Dolmen.Std.Expr
+module DT = Dolmen.Std.Expr.Ty
+module B = Dolmen.Std.Builtin
+
+module TSet =
+  Set.Make
     (struct
-      type t = Uid.t
+      type t = Uid.term_cst
 
       (* We use a dedicated total order on the constructors to ensure
-         the termination of the model generation. *)
-      let compare = Nest.compare
+         the termination of model generation. *)
+      let compare id1 id2 =
+        Nest.perfect_hash id1 - Nest.perfect_hash id2
     end)
 
 let timer = Timers.M_Adt
@@ -77,7 +83,8 @@ module Domain = struct
     else
       { constrs; ex }
 
-  let[@inline always] singleton ~ex c = { constrs = TSet.singleton c; ex }
+  let[@inline always] singleton ~ex c =
+    { constrs = TSet.singleton c; ex }
 
   let[@inline always] subset d1 d2 = TSet.subset d1.constrs d2.constrs
 
@@ -609,7 +616,7 @@ let constr_of_destr ty d =
 
   | _ -> assert false
 
-exception Found of X.r * Uid.t
+exception Found of X.r * Uid.term_cst
 
 let can_split env n =
   let m = Options.get_max_split () in
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index 3a56a50ba7..43230d58b7 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -1881,8 +1881,7 @@ module Make (Th : Theory.S) = struct
     Expr.reinit_cache ();
     Hstring.reinit_cache ();
     Shostak.Combine.reinit_cache ();
-    Uf.reinit_cache ();
-    Nest.reinit ()
+    Uf.reinit_cache ()
 
   let () =
     Steps.save_steps ();
diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index e5d354e2a7..350d42420c 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -29,8 +29,8 @@ module E = Expr
 module Sy = Symbols
 
 type 'a abstract =
-  | Record of (Uid.t * 'a abstract) list * Ty.t
-  | Access of Uid.t * 'a abstract * Ty.t
+  | Record of (Uid.term_cst * 'a abstract) list * Ty.t
+  | Access of Uid.term_cst * 'a abstract * Ty.t
   | Other of 'a * Ty.t
 
 module type ALIEN = sig
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 0a3ed11f7a..aaf94087ef 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1393,8 +1393,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     Expr.reinit_cache ();
     Hstring.reinit_cache ();
     Shostak.Combine.reinit_cache ();
-    Uf.reinit_cache ();
-    Nest.reinit ()
+    Uf.reinit_cache ()
 
   let () =
     Steps.save_steps ();
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index c490ed23a8..0c4351e053 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -160,25 +160,25 @@ module Main_Default : S = struct
            | Tvar _ -> assert false
 
            | Text (_, hs) | Trecord { name = hs; _ } when
-               Uid.Map.mem hs mp -> mp
+               Uid.Ty_map.mem hs mp -> mp
 
            | Text (l, hs) ->
              let l = List.map (fun _ -> Ty.fresh_tvar()) l in
-             Uid.Map.add hs (Text(l, hs)) mp
+             Uid.Ty_map.add hs (Text(l, hs)) mp
 
            | Trecord { name; _ } ->
              (* cannot do better for records ? *)
-             Uid.Map.add name ty mp
+             Uid.Ty_map.add name ty mp
 
            | Tadt (hs, _) ->
              (* cannot do better for ADT ? *)
-             Uid.Map.add hs ty mp
-        )sty Uid.Map.empty
+             Uid.Ty_map.add hs ty mp
+        )sty Uid.Ty_map.empty
 
     let print_types_decls ?(header=true) types =
       let open Ty in
       print_dbg ~flushed:false ~header "@[<v 2>(* types decls: *)@ ";
-      Uid.Map.iter
+      Uid.Ty_map.iter
         (fun _ ty ->
            match ty with
            | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> ()
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 1e9bbe92e0..4d47d8ed22 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -1276,7 +1276,7 @@ let mk_tester cons t =
 let mk_record xs ty = mk_term (Sy.Op Record) xs ty
 
 let void =
-  let cstr = Uid.of_dolmen Dolmen.Std.Expr.Term.Cstr.void in
+  let cstr = Uid.of_term_cst Dolmen.Std.Expr.Term.Cstr.void in
   mk_constr cstr [] Ty.tunit
 
 (** Substitutions *)
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index a63ff116a1..87d4458f85 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -280,8 +280,8 @@ val mk_ite : t -> t -> t -> t
 
 (** smart constructor for datatypes. *)
 
-val mk_constr : Uid.t -> t list -> Ty.t -> t
-val mk_tester : Uid.t -> t -> t
+val mk_constr : Uid.term_cst -> t list -> Ty.t -> t
+val mk_tester : Uid.term_cst -> t -> t
 val mk_record : t list -> Ty.t -> t
 
 (** Substitutions *)
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index d12e38d513..238351e99e 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -92,11 +92,12 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   let cstrs =
     List.map (fun c -> DStd.Path.global @@ to_smt_string c, []) cstrs
   in
-  let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  let def, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  Nest.attach_orders [def];
   let body =
-    List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
+    List.map (fun (c, _) -> Uid.of_term_cst c, []) d_cstrs
   in
-  let ty = Ty.t_adt ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
+  let ty = Ty.t_adt ~body:(Some body) (Uid.of_ty_cst ty_cst) [] in
   DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 7c99a2c0be..4f8671c09c 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -27,7 +27,7 @@
 
 type builtin =
     LE | LT (* arithmetic *)
-  | IsConstr of Uid.t (* ADT tester *)
+  | IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type operator =
@@ -35,9 +35,9 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Uid.t | Record
-  | Constr of Uid.t (* enums, adts *)
-  | Destruct of Uid.t
+  | Access of Uid.term_cst | Record
+  | Constr of Uid.term_cst (* enums, adts *)
+  | Destruct of Uid.term_cst
   (* Arrays *)
   | Get | Set
   (* BV *)
diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli
index bcf0af48a8..322a3a9354 100644
--- a/src/lib/structures/symbols.mli
+++ b/src/lib/structures/symbols.mli
@@ -27,7 +27,7 @@
 
 type builtin =
     LE | LT (* arithmetic *)
-  | IsConstr of Uid.t (* ADT tester *)
+  | IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type operator =
@@ -35,9 +35,9 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Uid.t | Record
-  | Constr of Uid.t (* enums, adts *)
-  | Destruct of Uid.t
+  | Access of Uid.term_cst | Record
+  | Constr of Uid.term_cst (* enums, adts *)
+  | Destruct of Uid.term_cst
   (* Arrays *)
   | Get | Set
   (* BV *)
@@ -163,8 +163,8 @@ val var : Var.t -> t
 val int : string -> t
 val bitv : string -> t
 val real : string -> t
-val constr : Uid.t -> t
-val destruct : Uid.t -> t
+val constr : Uid.term_cst -> t
+val destruct : Uid.term_cst -> t
 val mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound
 val mk_in : bound -> bound -> t
 val mk_maps_to : Var.t -> t
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index c00ddd47ae..1887d3b750 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -31,17 +31,19 @@ type t =
   | Tbool
   | Tvar of tvar
   | Tbitv of int
-  | Text of t list * Uid.t
+  | Text of t list * Uid.ty_cst
   | Tfarray of t * t
-  | Tadt of Uid.t * t list
+  | Tadt of Uid.ty_cst * t list
   | Trecord of trecord
 
 and tvar = { v : int ; mutable value : t option }
+
 and trecord = {
   mutable args : t list;
-  name : Uid.t;
-  mutable lbs :  (Uid.t * t) list;
-  record_constr : Uid.t; (* for ADTs that become records. default is "{" *)
+  name : Uid.ty_cst;
+  mutable lbs :  (Uid.term_cst * t) list;
+  record_constr : Uid.term_cst;
+  (* for ADTs that become records. default is "{" *)
 }
 
 module Smtlib = struct
@@ -67,8 +69,8 @@ exception TypeClash of t*t
 exception Shorten of t
 
 type adt_constr =
-  { constr : Uid.t ;
-    destrs : (Uid.t * t) list }
+  { constr : Uid.term_cst ;
+    destrs : (Uid.term_cst * t) list }
 
 type type_body = adt_constr list
 
@@ -405,7 +407,7 @@ and fresh_list lty subst =
 
 module Decls = struct
 
-  module MH = Uid.Map
+  module MH = Uid.Ty_map
 
   module MTY = Map.Make(struct
       type ty = t
@@ -510,7 +512,7 @@ let fresh_empty_text =
       let path = DStd.Path.global @@ Fmt.str "'_c%d" !cpt in
       DStd.Expr.Ty.Const.mk path 0
     in
-    text [] (Uid.of_dolmen id)
+    text [] (Uid.of_ty_cst id)
 
 let t_adt ?(body=None) s ty_vars =
   let ty = Tadt (s, ty_vars) in
@@ -536,15 +538,14 @@ let t_adt ?(body=None) s ty_vars =
 module DE = Dolmen.Std.Expr
 
 let tunit =
-  let name = Uid.of_dolmen DE.Ty.Const.unit in
-  let void = Uid.of_dolmen DE.Term.Cstr.void in
-  let body = Some [void, []] in
-  let ty = t_adt ~body name [] in
   let () =
-    match DE.Ty.definition DE.Ty.Const.unit with
-    | Some def -> Nest.add_nest [def]
-    | _ -> assert false
+    match Dolmen.Std.Expr.Ty.definition DE.Ty.Const.unit with
+    | Some def -> Nest.attach_orders [def]
+    | None -> assert false
   in
+  let void = Uid.of_term_cst DE.Term.Cstr.void in
+  let body = Some [void, []] in
+  let ty = t_adt ~body (Uid.of_ty_cst DE.Ty.Const.unit) [] in
   ty
 
 let trecord ?(sort_fields = false) ~record_constr lv name lbs =
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 43b7b8ddd9..d636faff99 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -42,7 +42,7 @@ type t =
   (** Type variables *)
   | Tbitv of int
   (** Bitvectors of a given length *)
-  | Text of t list * Uid.t
+  | Text of t list * Uid.ty_cst
   (** Abstract types applied to arguments. [Text (args, s)] is
       the application of the abstract type constructor [s] to
       arguments [args]. *)
@@ -51,7 +51,7 @@ type t =
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
 
-  | Tadt of Uid.t * t list
+  | Tadt of Uid.ty_cst * t list
   (** Application of algebraic data types. [Tadt (a, params)] denotes
       the application of the polymorphic datatype [a] to the types parameters
       [params].
@@ -77,22 +77,22 @@ and tvar = {
 and trecord = {
   mutable args : t list;
   (** Arguments passed to the record constructor *)
-  name : Uid.t;
+  name : Uid.ty_cst;
   (** Name of the record type *)
-  mutable lbs :  (Uid.t * t) list;
+  mutable lbs :  (Uid.term_cst * t) list;
   (** List of fields of the record. Each field has a name,
       and an associated type. *)
-  record_constr : Uid.t;
+  record_constr : Uid.term_cst;
   (** record constructor. Useful is case it's a specialization of an
       algeberaic datatype. Default value is "\{__[name]" *)
 }
 (** Record types. *)
 
 type adt_constr =
-  { constr : Uid.t ;
+  { constr : Uid.term_cst ;
     (** constructor of an ADT type *)
 
-    destrs : (Uid.t * t) list
+    destrs : (Uid.term_cst * t) list
     (** the list of destructors associated with the constructor and
         their respective types *)
   }
@@ -109,12 +109,12 @@ module Set : Set.S with type elt = t
 (** Sets of types *)
 
 
-val assoc_destrs : Uid.t -> adt_constr list -> (Uid.t * t) list
+val assoc_destrs : Uid.term_cst -> adt_constr list -> (Uid.term_cst * t) list
 (** [assoc_destrs cons cases] returns the list of destructors associated with
     the constructor [cons] in the ADT defined by [cases].
     @raises Not_found if the constructor is not in the given list. *)
 
-val type_body : Uid.t -> t list -> type_body
+val type_body : Uid.ty_cst -> t list -> type_body
 
 (** {2 Type inspection} *)
 
@@ -160,12 +160,13 @@ val fresh_tvar : unit -> t
 val fresh_empty_text : unit -> t
 (** Return a fesh abstract type. *)
 
-val text : t list -> Uid.t -> t
+val text : t list -> Uid.ty_cst -> t
 (** Apply the abstract type constructor to the list of type arguments
     given. *)
 
 val t_adt :
-  ?body:((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t
+  ?body:((Uid.term_cst * (Uid.term_cst * t) list) list) option ->
+  Uid.ty_cst -> t list -> t
 (** Create an algebraic datatype. The body is a list of
     constructors, where each constructor is associated with the list of
     its destructors with their respective types. If [body] is none,
@@ -175,7 +176,8 @@ val t_adt :
 
 val trecord :
   ?sort_fields:bool ->
-  record_constr:Uid.t -> t list -> Uid.t -> (Uid.t * t) list -> t
+  record_constr:Uid.term_cst ->
+  t list -> Uid.ty_cst -> (Uid.term_cst * t) list -> t
 (** Create a record type. [trecord args name lbs] creates a record
     type with name [name], arguments [args] and fields [lbs].
 
diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml
index 7c495adce1..0c4fa051ef 100644
--- a/src/lib/structures/typed.ml
+++ b/src/lib/structures/typed.ml
@@ -52,7 +52,7 @@ type oplogic =
 
 (** type of pattern in match construct of ADTs *)
 type pattern =
-  | Constr of { name : Uid.t ; args : (Var.t * Uid.t * Ty.t) list}
+  | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list}
   (** A pattern case which is a constructor. [name] is the name of
       constructor. [args] contains the variables bound by this pattern
       with their correponsing destructors and types *)
diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli
index b051c45cf3..281afdab27 100644
--- a/src/lib/structures/typed.mli
+++ b/src/lib/structures/typed.mli
@@ -72,7 +72,7 @@ type oplogic =
 (** Logic operators. *)
 
 type pattern =
-  | Constr of { name : Uid.t ; args : (Var.t * Uid.t * Ty.t) list}
+  | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list}
   | Var of Var.t
 
 
diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml
index a7c4743713..ecb4990eac 100644
--- a/src/lib/structures/uid.ml
+++ b/src/lib/structures/uid.ml
@@ -26,46 +26,84 @@
 (**************************************************************************)
 
 module DStd = Dolmen.Std
-module DE = DStd.Expr
+module DE = Dolmen.Std.Expr
 
-type t =
-  | Hstring : Hstring.t -> t
-  | Dolmen : 'a DE.id -> t
+type _ t =
+  | Hstring : Hstring.t -> 'a t
+  | Term_cst : DE.term_cst -> DE.term_cst t
+  | Ty_cst : DE.ty_cst -> DE.ty_cst t
+  | Ty_var : DE.ty_var -> DE.ty_var t
 
-let[@inline always] of_dolmen id = Dolmen id
+type term_cst = DE.term_cst t
+type ty_cst = DE.ty_cst t
+type ty_var = DE.ty_var t
+
+let order_tag : int DStd.Tag.t = DStd.Tag.create ()
+
+let has_order_if_cstr id =
+  let is_cstr DE.{ builtin; _ } =
+    match builtin with
+    | DStd.Builtin.Constructor _ -> true
+    | _ -> false
+  in
+  let has_attached_order id =
+    DE.Term.Const.get_tag id order_tag |> Option.is_some
+  in
+  (not (is_cstr id)) || has_attached_order id
+
+let[@inline always] of_term_cst id =
+  (* This assertion ensures that the API of the [Nest] module have been
+     correctly used, that is [Nest.attach_orders] have been called on
+     the nest of [id] if [id] is a constructor of ADT. *)
+  if not @@ has_order_if_cstr id then
+    Fmt.invalid_arg "not order on %a" DE.Id.print id;
+  Term_cst id
+
+let[@inline always] of_ty_cst id = Ty_cst id
+let[@inline always] of_ty_var id = Ty_var id
 let[@inline always] of_hstring hs = Hstring hs
 let[@inline always] of_string s = of_hstring @@ Hstring.make s
 
-let hash = function
+let hash (type a) (u : a t) =
+  match u with
   | Hstring hs -> Hstring.hash hs
-  | Dolmen id -> DE.Id.hash id
+  | Term_cst id -> DE.Id.hash id
+  | Ty_cst id -> DE.Id.hash id
+  | Ty_var id -> DE.Id.hash id
 
-let pp ppf = function
+let pp (type a) ppf (u : a t) =
+  match u with
   | Hstring hs -> Hstring.print ppf hs
-  | Dolmen id -> DE.Id.print ppf id
+  | Term_cst id -> DE.Id.print ppf id
+  | Ty_cst id -> DE.Id.print ppf id
+  | Ty_var id -> DE.Id.print ppf id
 
-let show = Fmt.to_to_string pp
+let show (type a) (u : a t) = Fmt.to_to_string pp u
 
-let equal u1 u2 =
+let equal (type a b) (u1 : a t) (u2 : b t) =
   match u1, u2 with
   | Hstring hs1, Hstring hs2 -> Hstring.equal hs1 hs2
-  | Dolmen id1, Dolmen id2 -> DE.Id.equal id1 id2
+  | Term_cst id1, Term_cst id2 -> DE.Id.equal id1 id2
+  | Ty_cst id1, Ty_cst id2 -> DE.Id.equal id1 id2
+  | Ty_var id1, Ty_var id2 -> DE.Id.equal id1 id2
   | _ -> String.equal (show u1) (show u2)
 
-let compare u1 u2 =
+let compare (type a b) (u1 : a t) (u2 : b t) =
   match u1, u2 with
   | Hstring hs1, Hstring hs2 -> Hstring.compare hs1 hs2
-  | Dolmen id1, Dolmen id2 -> DE.Id.compare id1 id2
+  | Term_cst id1, Term_cst id2 -> DE.Id.compare id1 id2
+  | Ty_cst id1, Ty_cst id2 -> DE.Id.compare id1 id2
+  | Ty_var id1, Ty_var id2 -> DE.Id.compare id1 id2
   | _ -> String.compare (show u1) (show u2)
 
-module Set = Set.Make
+module Term_set = Set.Make
     (struct
-      type nonrec t = t
+      type nonrec t = term_cst
       let compare = compare
     end)
 
-module Map = Map.Make
+module Ty_map = Map.Make
     (struct
-      type nonrec t = t
+      type nonrec t = ty_cst
       let compare = compare
     end)
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
index 09e0a76759..11d6570ed4 100644
--- a/src/lib/structures/uid.mli
+++ b/src/lib/structures/uid.mli
@@ -27,18 +27,30 @@
 
 module DE = Dolmen.Std.Expr
 
-type t = private
-  | Hstring : Hstring.t -> t
-  | Dolmen : 'a DE.id -> t
+type _ t = private
+  | Hstring : Hstring.t -> 'a t
+  | Term_cst : DE.term_cst -> DE.term_cst t
+  | Ty_cst : DE.ty_cst -> DE.ty_cst t
+  | Ty_var : DE.ty_var -> DE.ty_var t
 
-val of_dolmen : 'a DE.Id.t -> t
-val of_string : string -> t
-val of_hstring : Hstring.t -> t
-val hash : t -> int
-val pp : t Fmt.t
-val show : t -> string
-val equal : t -> t -> bool
-val compare : t -> t -> int
+type term_cst = DE.term_cst t
+type ty_cst = DE.ty_cst t
+type ty_var = DE.ty_var t
 
-module Set : Set.S with type elt = t
-module Map : Map.S with type key = t
+val of_term_cst : DE.term_cst -> term_cst
+val of_ty_cst : DE.ty_cst -> ty_cst
+val of_ty_var : DE.ty_var -> ty_var
+val of_string : string -> 'a t
+val of_hstring : Hstring.t -> 'a t
+
+val hash : 'a t -> int
+val pp : 'a t Fmt.t
+val show : 'a t -> string
+val equal : 'a t -> 'a t -> bool
+val compare : 'a t -> 'a t -> int
+
+val order_tag : int Dolmen.Std.Tag.t
+(** Tag used to attach the order of constructor. *)
+
+module Term_set : Set.S with type elt = term_cst
+module Ty_map : Map.S with type key = ty_cst
diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml
index 5862e5b685..d7f016445b 100644
--- a/src/lib/structures/xliteral.ml
+++ b/src/lib/structures/xliteral.ml
@@ -27,7 +27,7 @@
 
 type builtin = Symbols.builtin =
     LE | LT | (* arithmetic *)
-    IsConstr of Uid.t (* ADT tester *)
+    IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type 'a view =
diff --git a/src/lib/structures/xliteral.mli b/src/lib/structures/xliteral.mli
index 7f83f90b20..bd60c345a4 100644
--- a/src/lib/structures/xliteral.mli
+++ b/src/lib/structures/xliteral.mli
@@ -27,7 +27,7 @@
 
 type builtin = Symbols.builtin =
     LE | LT | (* arithmetic *)
-    IsConstr of Uid.t (* ADT tester *)
+    IsConstr of Uid.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type 'a view = (*private*)
diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml
index ac42686f82..d497553ea1 100644
--- a/src/lib/util/nest.ml
+++ b/src/lib/util/nest.ml
@@ -19,9 +19,7 @@
 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
+module B = DStd.Builtin
 
 (* A nest is the set of all the constructors of a mutually recursive definition
    of ADTs.
@@ -139,34 +137,32 @@ let build_graph (defs : DE.ty_def list) : Hp.t =
     ) 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
+module H = struct
+  include Hashtbl.Make (DE.Ty.Const)
+
+  let add_cstr t (ty : DE.ty_cst) (cstr : DE.term_cst) =
+    match find t ty with
+    | len, cstrs ->
+      add t ty (len + 1, cstr :: cstrs); len
+    | exception Not_found ->
+      add t ty (1, [cstr]); 0
+end
+
+let ty_cst_of_cstr DE.{ builtin; _ } =
+  match builtin with
+  | B.Constructor { adt; _ } -> adt
+  | _ -> Fmt.failwith "expect an ADT constructor"
+
+let attach_orders defs =
+  let hp = build_graph defs in
+  let r : (int * DE.term_cst list) H.t = H.create 17 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;
+    let { id; outgoing; in_degree;  _ } = Hp.pop_min hp in
+    let ty = ty_cst_of_cstr id in
+    let o = H.add_cstr r ty id in
+    DE.Term.Const.set_tag id Uid.order_tag o;
     assert (in_degree = 0);
     List.iter
       (fun node ->
@@ -178,9 +174,17 @@ let add_nest n =
     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
+let perfect_hash id =
+  match (id : _ Uid.t) with
+  | Term_cst ({ builtin = B.Constructor _; _ } as id) ->
+    begin match DE.Term.Const.get_tag id Uid.order_tag with
+      | Some h -> h
+      | None ->
+        (* Cannot occur as we eliminate this case in the smart constructor
+           [Uid.of_term_cst]. *)
+        assert false
+    end
+  | Term_cst _ -> invalid_arg "Nest.perfect_hash"
+  | Hstring hs ->
+    Hstring.hash hs
+  | _ -> .
diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli
index 47777be59e..d8b30d8624 100644
--- a/src/lib/util/nest.mli
+++ b/src/lib/util/nest.mli
@@ -18,31 +18,27 @@
 
 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]. *)
+(** The purpose of this module is to construct an appropriate total order on
+    constructors of a given ADT to ensure the termination of model generation
+    for this theory.
+
+    For each ADT type, we generate a minimal perfect hash function
+    for its set of constructors, that is a bijection between this set
+    on the integer between 0 and [n] exclusive, where [n] denotes the
+    number of constructors. The total order on ADT constructors is given by
+    the hash function. *)
+
+val attach_orders : DE.ty_def list -> unit
+(** [attach_orders defs] generate and attach orders on the constructors for
+    each ADT of [defs].
+
+    {b Note:} assume that [defs] is a list of definitions of a complete nest
+    (in any order). By nest, we mean the set of all the constructors in a
+    mutually recursive definition of ADTs. *)
+
+val perfect_hash : Uid.term_cst -> int
+(** [perfect_hash u] returns an integer between [0] and [n] exclusive where
+    [u] is a constructor and [n] is the number of constructors of the ADT of
+    [u].
+
+    @raise Invalid_arg if [u] is not a constructor. *)