diff --git a/src/lib/dune b/src/lib/dune
index aef40ae5a..786ffcf6b 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -48,7 +48,7 @@
     Cnf D_cnf D_loop D_state_option Input Frontend Parsed_interface Typechecker
     Models
     ; reasoners
-    Ac Arith Arrays_rel Bitv Ccx Shostak Relation Enum Enum_rel
+    Ac Arith Arrays_rel Bitv Ccx Shostak Relation
     Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 66b3e54ea..76434c768 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -540,7 +540,6 @@ and handle_ty_app ?(update = false) ty_c l =
     in
     apply_ty_substs tysubsts ty
 
-  | Tsum _ as ty -> ty
   | Text (_, s) -> Text (tyl, s)
   | _ -> assert false
 
@@ -573,48 +572,29 @@ 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 =
+    Cache.store_ty ty_c (Ty.t_adt uid tyvl);
+    let rev_cs =
       Array.fold_left (
-        fun (accl, is_enum) DE.{ cstr; dstrs; _ } ->
-          let is_enum =
-            if is_enum
-            then
-              if Array.length dstrs = 0
-              then true
-              else (
-                let ty = Ty.t_adt uid tyvl in
-                Cache.store_ty ty_c ty;
-                false
-              )
-            else false
-          in
+        fun accl DE.{ cstr; dstrs; _ } ->
           let rev_fields =
             Array.fold_left (
               fun acc tc_o ->
                 match tc_o with
-                | Some (DE.{ id_ty; _ } as id) ->
-                  (Uid.of_dolmen id, dty_to_ty id_ty) :: acc
+                | Some (DE.{ id_ty; _ } as field) ->
+                  (Uid.of_dolmen field, dty_to_ty id_ty) :: acc
                 | None -> assert false
             ) [] dstrs
           in
-          (Uid.of_dolmen cstr, List.rev rev_fields) :: accl, is_enum
-      ) ([], true) cases
+          (Uid.of_dolmen cstr, List.rev rev_fields) :: accl
+      ) [] cases
     in
-    if is_enum
-    then
-      let cstrs =
-        List.map (fun s -> fst s) (List.rev rev_cs)
-      in
-      let ty = Ty.tsum uid cstrs in
-      Cache.store_ty ty_c ty
-    else
-      let body = Some (List.rev rev_cs) in
-      let ty = Ty.t_adt ~body uid tyvl in
-      Cache.store_ty ty_c ty
+    let body = Some (List.rev rev_cs) in
+    let ty = Ty.t_adt ~body uid tyvl in
+    Cache.store_ty ty_c ty
 
   | None | Some Abstract ->
     let ty_params = []
@@ -690,8 +670,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
         ) [] cases
       in
       let body = Some (List.rev rev_cs) in
-      let args = tyl in
-      let ty = Ty.t_adt ~body hs args in
+      let ty = Ty.t_adt ~body hs tyl in
       Cache.store_ty ty_c ty
 
     | _ -> assert false
@@ -719,32 +698,16 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
         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 cns, is_enum =
-            Array.fold_right (
-              fun DE.{ dstrs; cstr; _ } (nacc, is_enum) ->
-                Uid.of_dolmen cstr :: nacc,
-                Array.length dstrs = 0 && is_enum
-            ) cases ([], true)
-          in
           let uid = Uid.of_dolmen ty_c in
-          if is_enum && not contains_adts
-          then (
-            let ty = Ty.tsum uid cns in
-            Cache.store_ty ty_c ty;
-            (* If it's an enum we don't need the second iteration. *)
-            acc
-          )
-          else (
-            let ty =
-              if (record || Array.length cases = 1) && not contains_adts
-              then
-                Ty.trecord ~record_constr:uid tyvl uid []
-              else Ty.t_adt uid tyvl
-            in
-            Cache.store_ty ty_c ty;
-            (ty, Some adt) :: acc
-          )
+          let ty =
+            if (record || Array.length cases = 1) && not contains_adts
+            then
+              Ty.trecord ~record_constr:uid tyvl uid []
+            else Ty.t_adt uid tyvl
+          in
+          Cache.store_ty ty_c ty;
+          (ty, Some adt) :: acc
+
         | Abstract ->
           assert false (* unreachable in the second iteration *)
     ) [] (List.rev rev_tdefs)
@@ -1044,9 +1007,7 @@ let rec mk_expr
               match Cache.find_ty ty_c with
               | Ty.Tadt _ ->
                 E.mk_builtin ~is_pos:true builtin [aux_mk_expr x]
-              | Ty.Tsum _ as ty ->
-                let cstr = E.mk_constr (Uid.of_dolmen cstr) [] ty in
-                E.mk_eq ~iff:false (aux_mk_expr x) cstr
+
               | Ty.Trecord _ ->
                 (* The typechecker allows only testers whose the
                    two arguments have the same type. Thus, we can always
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 7056b933d..3c6723480 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -73,10 +73,6 @@ module Types = struct
       if List.length lty <> List.length lty' then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       lty'
-    | Ty.Tsum (s, _) ->
-      if List.length lty <> 0 then
-        Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
-      []
     | _ -> assert false
 
   let equal_pp_vars lpp lvars =
@@ -145,13 +141,6 @@ module Types = struct
     | Abstract ->
       let ty = Ty.text ty_vars (Uid.of_string id) in
       ty, { env with to_ty = MString.add id ty env.to_ty }
-    | Enum lc ->
-      if not (Lists.is_empty ty_vars) then
-        Errors.typing_error (PolymorphicEnum id) loc;
-      let ty =
-        Ty.tsum (Uid.of_string id) (List.map Uid.of_string lc)
-      in
-      ty, { env with to_ty = MString.add id ty env.to_ty }
     | Record (record_constr, lbs) ->
       let lbs =
         List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in
@@ -171,6 +160,10 @@ module Types = struct
             from_labels =
               List.fold_left
                 (fun fl (l,_) -> MString.add l id fl) env.from_labels lbs }
+    | Enum l ->
+      let body = List.map (fun constr -> Uid.of_string constr, []) l in
+      let ty = Ty.t_adt ~body:(Some body) (Uid.of_string id) [] in
+      ty, { env with to_ty = MString.add id ty env.to_ty }
     | Algebraic l ->
       let l = (* convert ppure_type to Ty.t in l *)
         List.map (fun (constr, l) ->
@@ -276,7 +269,9 @@ module Env = struct
   let add_fpa_enum map =
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
-    | Ty.Tsum (_, cstrs) ->
+    | Ty.Tadt (name, params) ->
+      let Adt cases = Ty.type_body name params in
+      let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.fold_left
         (fun m c ->
            match Fpa_rounding.translate_smt_rounding_mode
@@ -300,8 +295,10 @@ module Env = struct
 
   let find_builtin_cstr ty n =
     match ty with
-    | Ty.Tsum (_, cstrs) ->
-      List.find (Uid.equal n) cstrs
+    | Ty.Tadt (name, params) ->
+      let Adt cases = Ty.type_body name params in
+      let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
+      List.find (fun c -> String.equal n @@ Uid.show c) cstrs
     | _ -> assert false
 
   let add_fpa_builtins env =
@@ -327,9 +324,9 @@ module Env = struct
     let nte = Fpa_rounding.string_of_rounding_mode NearestTiesToEven in
     let tname = Fpa_rounding.fpa_rounding_mode_ae_type_name in
     let float32 = float (int "24") (int "149") in
-    let float32d = float32 (mode (Uid.of_string nte)) in
+    let float32d = float32 (mode nte) in
     let float64 = float (int "53") (int "1074") in
-    let float64d = float64 (mode (Uid.of_string nte)) in
+    let float64d = float64 (mode nte) in
     let op n op profile =
       MString.add n @@ `Term (Symbols.Op op, profile, Other)
     in
@@ -1007,8 +1004,6 @@ let rec type_term ?(call_from_type_form=false) env f =
           end
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr; destrs = lbs}]
-        | Ty.Tsum (_,l) ->
-          List.map (fun e -> {Ty.constr = e; destrs = []}) l
         | _ -> Errors.typing_error (ShouldBeADT ty) loc
       in
       let pats =
@@ -1419,8 +1414,6 @@ and type_form ?(in_theory=false) env f =
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr ; destrs = lbs}]
 
-        | Ty.Tsum (_,l) ->
-          List.map (fun e -> {Ty.constr = e ; destrs = []}) l
         | _ ->
           Errors.typing_error (ShouldBeADT ty) f.pp_loc
       in
diff --git a/src/lib/reasoners/enum.ml b/src/lib/reasoners/enum.ml
deleted file mode 100644
index 5b1bc45dc..000000000
--- a/src/lib/reasoners/enum.ml
+++ /dev/null
@@ -1,189 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-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.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-module Sy = Symbols
-module E  = Expr
-
-type 'a abstract =
-  | Cons of Uid.t * Ty.t
-  (* [Cons(hs, ty)] represents a constructor of an enum type of type [ty]. *)
-
-  | Alien of 'a
-  (* [Alien r] represents a uninterpreted enum semantic value. *)
-
-module type ALIEN = sig
-  include Sig.X
-  val embed : r abstract -> r
-  val extract : r -> (r abstract) option
-end
-
-module Shostak (X : ALIEN) = struct
-
-  type t = X.r abstract
-  type r = X.r
-
-  let name = "Sum"
-
-  let timer = Timers.M_Sum
-
-  let is_mine_symb sy ty =
-    match sy, ty with
-    | Sy.Op (Sy.Constr _), Ty.Tsum _ -> true
-    | _ -> false
-
-  let fully_interpreted _ = true
-
-  let type_info = function
-    | Cons (_, ty) -> ty
-    | Alien x -> X.type_info x
-
-  let color _ = assert false
-
-
-  (*BISECT-IGNORE-BEGIN*)
-  module Debug = struct
-    open Printer
-
-    let print fmt = function
-      | Cons (hs,_) -> Format.fprintf fmt "%a" Uid.pp hs
-      | Alien x -> Format.fprintf fmt "%a" X.print x
-
-    let solve_bis a b =
-      if Options.get_debug_sum () then
-        print_dbg
-          ~module_name:"Enum" ~function_name:"solve"
-          "@[<v 2>we solve %a = %a@ " X.print a X.print b
-
-    let solve_bis_result res =
-      if Options.get_debug_sum () then
-        match res with
-        | [p,v] ->
-          print_dbg ~header:false
-            "we get: %a |-> %a@]" X.print p X.print v
-        | []    ->
-          print_dbg ~header:false
-            "the equation is trivial"
-        | _ -> assert false
-
-    let solve_bis_unsolvable () =
-      if Options.get_debug_sum () then
-        print_dbg
-          "the equation is unsolvable@]"
-
-  end
-  (*BISECT-IGNORE-END*)
-
-  let print = Debug.print
-
-  let embed r =
-    match X.extract r with
-    | Some c -> c
-    | None -> Alien r
-
-  let is_mine = function
-    | Alien r -> r
-    | Cons _ as c -> X.embed c
-
-  let compare_mine c1 c2 =
-    match c1 , c2 with
-    | Cons (h1,ty1) , Cons (h2,ty2)  ->
-      let n = Uid.compare h1 h2 in
-      if n <> 0 then n else Ty.compare ty1 ty2
-    | Alien r1, Alien r2 -> X.str_cmp r1 r2
-    | Alien _ , Cons _   -> 1
-    | Cons _  , Alien _  -> -1
-
-  let compare x y = compare_mine (embed x) (embed y)
-
-  let equal s1 s2 = match s1, s2 with
-    | Cons (h1,ty1) , Cons (h2,ty2)  -> Uid.equal h1 h2 && Ty.equal ty1 ty2
-    | Alien r1, Alien r2 -> X.equal r1 r2
-    | Alien _ , Cons _  | Cons _  , Alien _  -> false
-
-  let hash = function
-    | Cons (h, ty) -> Uid.hash h + 19 * Ty.hash ty
-    | Alien r -> X.hash r
-
-  let leaves _ = []
-
-  let is_constant _ = true
-
-  let subst p v c =
-    let cr = is_mine c in
-    if X.equal p cr then v
-    else
-      match c with
-      | Cons _ -> cr
-      | Alien r -> X.subst p v r
-
-  let make t = match E.term_view t with
-    | { E.f = Sy.Op (Sy.Constr hs); xs = []; ty; _ } ->
-      is_mine (Cons(hs,ty)), []
-    | _ ->
-      Printer.print_err
-        "Enum theory only expect constructors with no arguments; got %a."
-        E.print t;
-      assert false
-
-  let solve a b =
-    match embed a, embed b with
-    | Cons(c1,_) , Cons(c2,_) when Uid.equal c1 c2 -> []
-    | Cons(_,_) , Cons(_,_) -> raise Util.Unsolvable
-    | Cons _     , Alien r2   -> [r2,a]
-    | Alien r1   , Cons _     -> [r1,b]
-    | Alien _    , Alien _    ->
-      if X.str_cmp a b > 0 then [a,b] else [b,a]
-
-  let solve_bis a b =
-    Debug.solve_bis a b;
-    try
-      let res = solve a b in
-      Debug.solve_bis_result res;
-      res
-    with Util.Unsolvable ->
-      Debug.solve_bis_unsolvable ();
-      raise Util.Unsolvable
-
-  let abstract_selectors v acc = is_mine v, acc
-
-  let term_extract _ = None, false
-
-  let solve r1 r2 pb =
-    Sig.{pb with sbt = List.rev_append (solve_bis r1 r2) pb.sbt}
-
-  let assign_value _ _ _ =
-    (* As the models of this theory are finite, the case-split
-       mechanism can and does exhaust all the possible values.
-       Thus we don't need to guess new values here. *)
-    None
-
-  let to_model_term r =
-    match embed r with
-    | Cons (hs, ty) ->
-      Some (E.mk_term Sy.(Op (Constr hs)) [] ty)
-    | Alien a -> X.to_model_term a
-end
diff --git a/src/lib/reasoners/enum.mli b/src/lib/reasoners/enum.mli
deleted file mode 100644
index 2a685909f..000000000
--- a/src/lib/reasoners/enum.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-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.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-(*type 'a abstract*)
-type 'a abstract = Cons of Uid.t * Ty.t |  Alien of 'a
-
-module type ALIEN = sig
-  include Sig.X
-  val embed : r abstract -> r
-  val extract : r -> (r abstract) option
-end
-
-module Shostak
-    (X : ALIEN) : Sig.SHOSTAK with type r = X.r and type t = X.r abstract
diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
deleted file mode 100644
index f8ddac665..000000000
--- a/src/lib/reasoners/enum_rel.ml
+++ /dev/null
@@ -1,410 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-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.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-module L  = List
-module X = Shostak.Combine
-module Ex = Explanation
-module MX = Shostak.MXH
-module SX = Shostak.SXH
-module LR = Uf.LX
-module Th = Shostak.Enum
-
-let timer = Timers.M_Sum
-
-module Domain = struct
-  type t = {
-    constrs : Uid.Set.t;
-    ex : Ex.t;
-  }
-
-  exception Inconsistent of Ex.t
-
-  let[@inline always] cardinal { constrs; _ } = Uid.Set.cardinal constrs
-
-  let[@inline always] choose { constrs; _ } = Uid.Set.choose constrs
-
-  let[@inline always] as_singleton { constrs; ex } =
-    if Uid.Set.cardinal constrs = 1 then
-      Some (Uid.Set.choose constrs, ex)
-    else
-      None
-
-  let domain ~constrs ex =
-    if Uid.Set.is_empty constrs then
-      raise_notrace @@ Inconsistent ex
-    else
-      { constrs; ex }
-
-  let[@inline always] singleton ~ex c = { constrs = Uid.Set.singleton c; ex }
-
-  let[@inline always] subset d1 d2 = Uid.Set.subset d1.constrs d2.constrs
-
-  let unknown ty =
-    match ty with
-    | Ty.Tsum (_, constrs) ->
-      (* Return the list of all the constructors of the type of [r]. *)
-      let constrs = Uid.Set.of_list constrs in
-      assert (not @@ Uid.Set.is_empty constrs);
-      { constrs; ex = Ex.empty }
-    | _ ->
-      (* Only Enum 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 pp ppf d =
-    Fmt.(braces @@
-         iter ~sep:comma Uid.Set.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 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 ex = Ex.union ex d.ex in
-    domain ~constrs ex
-end
-
-let is_enum_ty = function
-  | Ty.Tsum _ -> true
-  | _ -> false
-
-let is_enum r = is_enum_ty (X.type_info r)
-
-module Domains = struct
-  (** The type of simple domain maps. A domain map maps each representative
-      (semantic value, of type [X.r]) to its associated domain. *)
-  type t = {
-    domains : Domain.t MX.t;
-    (** Map from tracked representatives to their domain.
-
-        We don't store domains for constructors. *)
-
-    changed : SX.t;
-    (** Representatives whose domain has changed since the last flush
-        in [propagation]. *)
-  }
-
-  type _ Uf.id += Id : t Uf.id
-
-  let pp ppf t =
-    Fmt.(iter_bindings ~sep:semi MX.iter
-           (box @@ pair ~sep:(any " ->@ ") X.print Domain.pp)
-         |> braces
-        )
-      ppf t.domains
-
-  let empty = { domains = MX.empty; changed = SX.empty }
-
-  let filter_ty = is_enum_ty
-
-  let internal_update r nd t =
-    let domains = MX.add r nd t.domains in
-    let changed = SX.add r t.changed in
-    { domains; changed }
-
-  let get r t =
-    match Th.embed r with
-    | Cons (c, _) ->
-      (* For sake of efficiency, we don't look in the map if the
-         semantic value is a constructor. *)
-      Domain.singleton ~ex:Explanation.empty c
-    | _ ->
-      try MX.find r t.domains
-      with Not_found ->
-        Domain.unknown (X.type_info r)
-
-  let add r t =
-    match Th.embed r with
-    | Alien _ when not (MX.mem r t.domains) ->
-      (* We have to add a default domain if the key `r` isn't in map in order
-         to be sure that the case-split mechanism will attempt to choose a
-         value for it. *)
-      let nd = Domain.unknown (X.type_info r) in
-      internal_update r nd t
-    | Cons _ | Alien _ -> t
-
-  (** [tighten r d t] replaces the domain of [r] in [t] by a domain [d] contains
-      in the current domain of [r]. The representative [r] is marked [changed]
-      after this call if the domain [d] is strictly smaller. *)
-  let tighten r d t =
-    let od = get r t in
-    (* For sake of completeness, the domain [d] has to be a subset of the old
-       domain of [r]. *)
-    Options.heavy_assert (fun () -> Domain.subset d od);
-    if Domain.equal od d then
-      t
-    else
-      internal_update r d t
-
-  let remove r t =
-    let domains = MX.remove r t.domains in
-    let changed = SX.remove r t.changed in
-    { domains ; changed }
-
-  exception Inconsistent = Domain.Inconsistent
-
-  (** [subst ~ex p v d] replaces all the instances of [p] with [v] in all
-      domains, merging the corresponding domains as appropriate.
-
-      The explanation [ex] justifies the equality [p = v].
-
-      @raise Domain.Inconsistent if this causes any domain in [d] to become
-             empty. *)
-  let subst ~ex r nr t =
-    match MX.find r t.domains with
-    | d ->
-      let nd = Domain.intersect ~ex d (get nr t) in
-      let t = remove r t in
-      tighten nr nd t
-
-    | exception Not_found -> add nr t
-
-  let fold f t acc = MX.fold f t.domains acc
-
-  (* [propagate f a t] iterates on all the changed domains of [t] since the
-     last call of [propagate]. The list of changed domains is flushed after
-     this call. *)
-  let propagate f acc t =
-    let acc =
-      SX.fold
-        (fun r acc ->
-           let d = get r t in
-           f acc r d
-        ) t.changed acc
-    in
-    acc, { t with changed = SX.empty }
-end
-
-type t = {
-  size_splits : Numbers.Q.t
-  (* Estimate the number of case-splits performed by the theory. The
-     estimation is updated while assuming new literals of the theory.
-     We don't perfom new case-splits if this estimation exceeds
-     [Options.get_max_split ()]. *)
-}
-
-(*BISECT-IGNORE-BEGIN*)
-module Debug = struct
-  let assume l =
-    if Options.get_debug_sum () then
-      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"assume"
-        "assume %a"
-        (Xliteral.print_view X.print) l
-
-  let case_split r1 r2 =
-    if Options.get_debug_sum () then
-      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"case_split"
-        "%a = %a" X.print r1 X.print r2
-
-  let no_case_split () =
-    if Options.get_debug_sum () then
-      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"case_split"
-        "nothing"
-
-  let add r =
-    if Options.get_debug_sum () then
-      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"add"
-        "%a" X.print r
-
-  let pp_domains domains =
-    if Options.get_debug_sum () then
-      Printer.print_dbg ~module_name:"Enum_rel"
-        "The environment before assuming:@ @[%a@]" Domains.pp domains
-end
-(*BISECT-IGNORE-END*)
-
-let empty uf = {
-  size_splits = Numbers.Q.one
-}, Uf.GlobalDomains.add (module Domains) Domains.empty (Uf.domains uf)
-
-(* Update the counter of case-split size in [env]. *)
-let count_splits env la =
-  let nb =
-    List.fold_left
-      (fun nb (_, _, _, i) ->
-         match i with
-         | Th_util.CS (Th_util.Th_sum, n) -> Numbers.Q.mult nb n
-         | _ -> nb
-      ) env.size_splits la
-  in
-  {size_splits = nb}
-
-let tighten_domain rr nd domains =
-  Domains.tighten rr nd domains
-
-(* Update the domains of the semantic values [r1] and [r2] according to the
-   disequality [r1 <> r2].
-
-   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
-   information to discover this contradiction.
-
-   Now, if we produce a case-split for one of these semantic values,
-   we reach a contradiction for each choice and so our implementation got
-   a complete decision procedure (assuming we have fuel to produce enough
-   case-splits).
-
-   @raise Domain.Inconsistent if the disequality is inconsistent with
-          the current environment [env]. *)
-let assume_distinct ~ex r1 r2 domains =
-  let d1 = Domains.get r1 domains in
-  let d2 = Domains.get r2 domains in
-  let env =
-    match Domain.as_singleton d1 with
-    | Some (c, ex1) ->
-      let ex = Ex.union ex1 ex in
-      let nd = Domain.remove ~ex c d2 in
-      tighten_domain r2 nd domains
-    | None ->
-      domains
-  in
-  match Domain.as_singleton d2 with
-  | Some (c, ex2) ->
-    let ex = Ex.union ex2 ex in
-    let nd = Domain.remove ~ex c d1 in
-    tighten_domain r1 nd env
-  | None ->
-    env
-
-let add r uf domains =
-  match X.type_info r with
-  | Ty.Tsum _ ->
-    Debug.add r;
-    let rr, _ = Uf.find_r uf r in
-    Domains.add rr domains
-  | _ ->
-    domains
-
-let add_rec r uf domains =
-  List.fold_left (fun env leaf -> add leaf uf env) domains (X.leaves r)
-
-let add env uf _r _t =
-  env, Uf.domains uf, []
-
-let assume_literals la uf domains =
-  List.fold_left
-    (fun domains lit ->
-       let open Xliteral in
-       match lit with
-       | Distinct (false, [r1; r2]) as l, _, ex, _ when is_enum r2 ->
-         Debug.assume l;
-         (* Needed for models generation because fresh terms are not added with
-            the function add. *)
-         let domains = add_rec r1 uf domains in
-         let domains = add_rec r2 uf domains in
-         assume_distinct ~ex r1 r2 domains
-
-       | _ -> domains
-    ) domains la
-
-let propagate_domains domains =
-  Domains.propagate
-    (fun eqs rr d ->
-       match Domain.as_singleton d with
-       | Some (c, ex) ->
-         let nr = Th.is_mine (Cons (c, X.type_info rr)) in
-         let eq = Literal.LSem (LR.mkv_eq rr nr), ex, Th_util.Other in
-         eq :: eqs
-       | None ->
-         eqs
-    ) [] domains
-
-let assume env uf la =
-  let ds = Uf.domains uf in
-  let domains = Uf.GlobalDomains.find (module Domains) ds in
-  Debug.pp_domains domains;
-  let env = count_splits env la in
-  let domains =
-    try
-      assume_literals la uf domains
-    with Domain.Inconsistent ex ->
-      raise_notrace (Ex.Inconsistent (ex, Uf.cl_extract uf))
-  in
-  let assume, domains = propagate_domains domains in
-  env,
-  Uf.GlobalDomains.add (module Domains) domains ds,
-  Sig_rel.{ assume; remove = [] }
-
-let can_split env n =
-  let m = Options.get_max_split () in
-  Numbers.Q.(compare (mult n env.size_splits) m) <= 0 || Numbers.Q.sign m < 0
-
-(* Do a case-split by choosing a constructor for class representatives of
-   minimal size. *)
-let case_split env uf ~for_model =
-  let best =
-    Domains.fold (fun r d best ->
-        let rr, _ = Uf.find_r uf r in
-        match Th.embed rr with
-        | Cons _ ->
-          (* The equivalence class of [r] already contains a model term so
-             we don't need to make another case-split for this semantic
-             value. *)
-          best
-        | _ ->
-          let cd = Domain.cardinal d in
-          match best with
-          | Some (n, _, _) when n <= cd -> best
-          | _ -> Some (cd, r, Domain.choose d)
-      ) (Uf.GlobalDomains.find (module Domains) (Uf.domains uf)) None
-  in
-  match best with
-  | Some (n, r, c) ->
-    let n = Numbers.Q.from_int n in
-    if for_model || can_split env n then
-      let nr = Th.is_mine (Cons (c, X.type_info r)) in
-      Debug.case_split r nr;
-      [LR.mkv_eq r nr, true, Th_util.CS (Th_util.Th_sum, n)]
-    else
-      []
-  | None ->
-    Debug.no_case_split ();
-    []
-
-let optimizing_objective _env _uf _o = None
-
-let query env uf a_ex =
-  try ignore(assume env uf [a_ex]); None
-  with Ex.Inconsistent (expl, classes) -> Some (expl, classes)
-
-let new_terms _ = Expr.Set.empty
-
-let instantiate ~do_syntactic_matching:_ _ env _ _  = env, []
-
-let assume_th_elt t th_elt _ =
-  match th_elt.Expr.extends with
-  | Util.Sum ->
-    failwith "This Theory does not support theories extension"
-  | _ -> t
diff --git a/src/lib/reasoners/enum_rel.mli b/src/lib/reasoners/enum_rel.mli
deleted file mode 100644
index 71cfa717c..000000000
--- a/src/lib/reasoners/enum_rel.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2013-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.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-include Sig_rel.RELATION
diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml
index bfdad703d..12971f1ce 100644
--- a/src/lib/reasoners/relation.ml
+++ b/src/lib/reasoners/relation.ml
@@ -37,11 +37,9 @@ module Rel3 : Sig_rel.RELATION = Bitv_rel
 
 module Rel4 : Sig_rel.RELATION = Arrays_rel
 
-module Rel5 : Sig_rel.RELATION = Enum_rel
+module Rel5 : Sig_rel.RELATION = Adt_rel
 
-module Rel6 : Sig_rel.RELATION = Adt_rel
-
-module Rel7 : Sig_rel.RELATION = Ite_rel
+module Rel6 : Sig_rel.RELATION = Ite_rel
 
 (* This value is unused. *)
 let timer = Timers.M_None
@@ -53,7 +51,6 @@ type t = {
   r4: Rel4.t;
   r5: Rel5.t;
   r6: Rel6.t;
-  r7: Rel7.t;
 }
 
 let empty uf =
@@ -63,8 +60,7 @@ let empty uf =
   let r4, doms4 = Rel4.empty (Uf.set_domains uf doms3) in
   let r5, doms5 = Rel5.empty (Uf.set_domains uf doms4) in
   let r6, doms6 = Rel6.empty (Uf.set_domains uf doms5) in
-  let r7, doms7 = Rel7.empty (Uf.set_domains uf doms6) in
-  {r1; r2; r3; r4; r5; r6; r7}, doms7
+  {r1; r2; r3; r4; r5; r6}, doms6
 
 let (|@|) l1 l2 =
   if l1 == [] then l2
@@ -97,14 +93,10 @@ let assume env uf sa =
     Timers.with_timer Rel6.timer Timers.F_assume @@ fun () ->
     Rel6.assume env.r6 (Uf.set_domains uf doms5) sa
   in
-  let env7, doms7, ({ assume = a7; remove = rm7}:_ Sig_rel.result) =
-    Timers.with_timer Rel7.timer Timers.F_assume @@ fun () ->
-    Rel7.assume env.r7 (Uf.set_domains uf doms6) sa
-  in
-  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7},
-  doms7,
-  ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6 |@| a7;
-     remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 |@| rm7}
+  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6},
+  doms6,
+  ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6;
+     remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 }
    : _ Sig_rel.result)
 
 let assume_th_elt env th_elt dep =
@@ -115,8 +107,7 @@ let assume_th_elt env th_elt dep =
   let env4 = Rel4.assume_th_elt env.r4 th_elt dep in
   let env5 = Rel5.assume_th_elt env.r5 th_elt dep in
   let env6 = Rel6.assume_th_elt env.r6 th_elt dep in
-  let env7 = Rel7.assume_th_elt env.r7 th_elt dep in
-  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7}
+  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6}
 
 let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a
     k =
@@ -132,8 +123,7 @@ let query env uf a =
   try_query (module Rel3) env.r3 uf a @@ fun () ->
   try_query (module Rel4) env.r4 uf a @@ fun () ->
   try_query (module Rel5) env.r5 uf a @@ fun () ->
-  try_query (module Rel6) env.r6 uf a @@ fun () ->
-  try_query (module Rel7) env.r7 uf a @@ fun () -> None
+  try_query (module Rel6) env.r6 uf a @@ fun () -> None
 
 let case_split env uf ~for_model =
   Options.exec_thread_yield ();
@@ -143,8 +133,7 @@ let case_split env uf ~for_model =
   let seq4 = Rel4.case_split env.r4 uf ~for_model in
   let seq5 = Rel5.case_split env.r5 uf ~for_model in
   let seq6 = Rel6.case_split env.r6 uf ~for_model in
-  let seq7 = Rel7.case_split env.r7 uf ~for_model in
-  let splits = [seq1; seq2; seq3; seq4; seq5; seq6; seq7] in
+  let splits = [seq1; seq2; seq3; seq4; seq5; seq6] in
   let splits = List.fold_left (|@|) [] splits in
   List.fast_sort
     (fun (_ ,_ , sz1) (_ ,_ , sz2) ->
@@ -181,8 +170,7 @@ let add env uf r t =
   let r4, doms4, eqs4 =Rel4.add env.r4 (Uf.set_domains uf doms3) r t in
   let r5, doms5, eqs5 =Rel5.add env.r5 (Uf.set_domains uf doms4) r t in
   let r6, doms6, eqs6 =Rel6.add env.r6 (Uf.set_domains uf doms5) r t in
-  let r7, doms7, eqs7 =Rel7.add env.r7 (Uf.set_domains uf doms6) r t in
-  {r1;r2;r3;r4;r5;r6;r7;},doms7,eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6|@|eqs7
+  {r1;r2;r3;r4;r5;r6}, doms6, eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6
 
 
 let instantiate ~do_syntactic_matching t_match env uf selector =
@@ -199,22 +187,13 @@ let instantiate ~do_syntactic_matching t_match env uf selector =
     Rel5.instantiate ~do_syntactic_matching t_match env.r5 uf selector in
   let r6, l6 =
     Rel6.instantiate ~do_syntactic_matching t_match env.r6 uf selector in
-  let r7, l7 =
-    Rel7.instantiate ~do_syntactic_matching t_match env.r7 uf selector in
-  {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6; r7=r7},
-  l7 |@| l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1
+  {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6},
+  l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1
 
 let new_terms env =
-  let t1 = Rel1.new_terms env.r1 in
-  let t2 = Rel2.new_terms env.r2 in
-  let t3 = Rel3.new_terms env.r3 in
-  let t4 = Rel4.new_terms env.r4 in
-  let t5 = Rel5.new_terms env.r5 in
-  let t6 = Rel6.new_terms env.r6 in
-  let t7 = Rel7.new_terms env.r7 in
-  Expr.Set.union t1
-    (Expr.Set.union t2
-       (Expr.Set.union t3
-          (Expr.Set.union t4
-             (Expr.Set.union t5
-                (Expr.Set.union t6 t7)) )))
+  Rel1.new_terms env.r1
+  |> Expr.Set.union @@ Rel2.new_terms env.r2
+  |> Expr.Set.union @@ Rel3.new_terms env.r3
+  |> Expr.Set.union @@ Rel4.new_terms env.r4
+  |> Expr.Set.union @@ Rel5.new_terms env.r5
+  |> Expr.Set.union @@ Rel6.new_terms env.r6
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index 898070ff5..0c38e426d 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -43,11 +43,8 @@ module rec CX : sig
   val extract3 : r -> BITV.t option
   val embed3 : BITV.t -> r
 
-  val extract4 : r -> ENUM.t option
-  val embed4 : ENUM.t -> r
-
-  val extract5 : r -> ADT.t option
-  val embed5 : ADT.t -> r
+  val extract4 : r -> ADT.t option
+  val embed4 : ADT.t -> r
 
 end =
 struct
@@ -58,7 +55,6 @@ struct
     | Arith of ARITH.t
     | Records of RECORDS.t
     | Bitv of BITV.t
-    | Enum of ENUM.t
     | Adt of ADT.t
 
   type r = {v : rview ; id : int}
@@ -74,7 +70,6 @@ struct
         | Arith t -> fprintf fmt "%a" ARITH.print t
         | Records t -> fprintf fmt "%a" RECORDS.print t
         | Bitv t -> fprintf fmt "%a" BITV.print t
-        | Enum t -> fprintf fmt "%a" ENUM.print t
         | Adt t -> fprintf fmt "%a" ADT.print t
         | Term t -> fprintf fmt "%a" Expr.print t
         | Ac t -> fprintf fmt "%a" AC.print t
@@ -87,8 +82,6 @@ struct
           fprintf fmt "Records(%s):[%a]" RECORDS.name RECORDS.print t
         | Bitv t ->
           fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t
-        | Enum t ->
-          fprintf fmt "Enum(%s):[%a]" ENUM.name ENUM.print t
         | Adt t ->
           fprintf fmt "Adt(%s):[%a]" ADT.name ADT.print t
         | Term t ->
@@ -170,7 +163,6 @@ struct
         | Arith x -> 1 + 10 * ARITH.hash x
         | Records x -> 2 + 10 * RECORDS.hash x
         | Bitv x -> 3 + 10 * BITV.hash x
-        | Enum x -> 5 + 10 * ENUM.hash x
         | Adt x -> 6 + 10 * ADT.hash x
         | Ac ac -> 9 + 10 * AC.hash ac
         | Term t -> 8 + 10 * Expr.hash t
@@ -182,7 +174,6 @@ struct
       | Arith x, Arith y -> ARITH.equal x y
       | Records x, Records y -> RECORDS.equal x y
       | Bitv x, Bitv y -> BITV.equal x y
-      | Enum x, Enum y -> ENUM.equal x y
       | Adt x, Adt y -> ADT.equal x y
       | Term x, Term y -> Expr.equal x y
       | Ac x, Ac y -> AC.equal x y
@@ -209,8 +200,7 @@ struct
   let embed1 x = hcons {v = Arith x; id = -1000 (* dummy *)}
   let embed2 x = hcons {v = Records x; id = -1000 (* dummy *)}
   let embed3 x = hcons {v = Bitv x; id = -1000 (* dummy *)}
-  let embed4 x = hcons {v = Enum x; id = -1000 (* dummy *)}
-  let embed5 x = hcons {v = Adt x; id = -1000 (* dummy *)}
+  let embed4 x = hcons {v = Adt x; id = -1000 (* dummy *)}
 
   let ac_embed ({ Sig.l; _ } as t) =
     match l with
@@ -227,8 +217,7 @@ struct
   let extract1 = function { v=Arith r; _ } -> Some r | _ -> None
   let extract2 = function { v=Records r; _ } -> Some r | _ -> None
   let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None
-  let extract4 = function { v=Enum r; _ } -> Some r | _ -> None
-  let extract5 = function { v=Adt r; _ } -> Some r | _ -> None
+  let extract4 = function { v=Adt r; _ } -> Some r | _ -> None
 
   let ac_extract = function
     | { v = Ac t; _ }   -> Some t
@@ -239,7 +228,6 @@ struct
     | Arith _ -> ARITH.term_extract r
     | Records _ -> RECORDS.term_extract r
     | Bitv _ -> BITV.term_extract r
-    | Enum _ -> ENUM.term_extract r
     | Adt _ -> ADT.term_extract r
     | Ac _ -> None, false (* SYLVAIN : TODO *)
     | Term t -> Some t, true
@@ -250,7 +238,6 @@ struct
       | Arith _ -> ARITH.to_model_term r
       | Records _ -> RECORDS.to_model_term r
       | Bitv _ -> BITV.to_model_term r
-      | Enum _ -> ENUM.to_model_term r
       | Adt _ -> ADT.to_model_term r
       | Term t when Expr.is_model_term t -> Some t
       | Ac _ | Term _ -> None
@@ -266,7 +253,6 @@ struct
     | { v = Arith t; _ } -> ARITH.type_info t
     | { v = Records t; _ } -> RECORDS.type_info t
     | { v = Bitv t; _ } -> BITV.type_info t
-    | { v = Enum t; _ } -> ENUM.type_info t
     | { v = Adt t; _ } -> ADT.type_info t
     | { v = Ac x; _ } -> AC.type_info x
     | { v = Term t; _ } -> Expr.type_info t
@@ -279,8 +265,7 @@ struct
     | Arith _ -> -3
     | Records _ -> -4
     | Bitv _ -> -5
-    | Enum _ -> -7
-    | Adt _ -> -8
+    | Adt _ -> -7
 
   let compare_tag a b = theory_num a - theory_num b
 
@@ -291,7 +276,6 @@ struct
       | Arith _, Arith _ -> ARITH.compare a b
       | Records _, Records _ -> RECORDS.compare a b
       | Bitv _, Bitv _ -> BITV.compare a b
-      | Enum _, Enum _ -> ENUM.compare a b
       | Adt _, Adt _ -> ADT.compare a b
       | Term x, Term y -> Expr.compare x y
       | Ac x, Ac y -> AC.compare x y
@@ -308,7 +292,7 @@ struct
        | Records x -> RECORDS.hash x
        | Bitv x -> BITV.hash x
        | Arrays x -> ARRAYS.hash x
-       | Enum x -> ENUM.hash x
+       | Adt x -> ADT.hash x
 
    ***)
 
@@ -336,7 +320,6 @@ struct
     | Arith t -> ARITH.leaves t
     | Records t -> RECORDS.leaves t
     | Bitv t -> BITV.leaves t
-    | Enum t -> ENUM.leaves t
     | Adt t -> ADT.leaves t
     | Ac t -> r :: (AC.leaves t)
     | Term _ -> [r]
@@ -346,7 +329,6 @@ struct
     | Arith t -> ARITH.is_constant t
     | Records t -> RECORDS.is_constant t
     | Bitv t -> BITV.is_constant t
-    | Enum t -> ENUM.is_constant t
     | Adt t -> ADT.is_constant t
     | Term t ->
       begin
@@ -364,7 +346,6 @@ struct
       | Arith t -> ARITH.subst p v t
       | Records t -> RECORDS.subst p v t
       | Bitv t -> BITV.subst p v t
-      | Enum t -> ENUM.subst p v t
       | Adt t -> ADT.subst p v t
       | Ac t -> if equal p r then v else AC.subst p v t
       | Term _ -> if equal p r then v else r
@@ -376,35 +357,30 @@ struct
       ARITH.is_mine_symb sb ty,
       not_restricted && RECORDS.is_mine_symb sb ty,
       not_restricted && BITV.is_mine_symb sb ty,
-      not_restricted && ENUM.is_mine_symb sb ty,
       not_restricted && ADT.is_mine_symb sb ty,
       AC.is_mine_symb sb ty
     with
-    | true  , false , false, false, false, false ->
+    | true, false, false, false, false ->
       Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () ->
       ARITH.make t
 
-    | false , true  , false, false, false, false ->
+    | false, true, false, false, false ->
       Timers.with_timer Timers.M_Records Timers.F_make @@ fun () ->
       RECORDS.make t
 
-    | false , false , true  , false, false, false ->
+    | false, false, true, false, false ->
       Timers.with_timer Timers.M_Bitv Timers.F_make @@ fun () ->
       BITV.make t
 
-    | false , false , false , true , false, false ->
-      Timers.with_timer Timers.M_Sum Timers.F_make @@ fun () ->
-      ENUM.make t
-
-    | false , false , false , false, true , false ->
+    | false, false, false, true, false ->
       Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () ->
       ADT.make t
 
-    | false , false , false , false, false, true  ->
+    | false, false, false, false, true  ->
       Timers.with_timer Timers.M_AC Timers.F_make @@ fun () ->
       AC.make t
 
-    | false , false , false , false, false, false ->
+    | false, false, false, false, false ->
       term_embed t, []
 
     | _ -> assert false
@@ -415,23 +391,20 @@ struct
       ARITH.is_mine_symb sb ty,
       not_restricted && RECORDS.is_mine_symb sb ty,
       not_restricted && BITV.is_mine_symb sb ty,
-      not_restricted && ENUM.is_mine_symb sb ty,
       not_restricted && ADT.is_mine_symb sb ty,
       AC.is_mine_symb sb ty
     with
-    | true  , false , false, false, false, false ->
+    | true, false, false, false, false ->
       ARITH.fully_interpreted sb
-    | false , true  , false, false, false, false ->
+    | false, true, false, false, false ->
       RECORDS.fully_interpreted sb
-    | false , false , true  , false, false, false ->
+    | false, false, true, false, false ->
       BITV.fully_interpreted sb
-    | false , false , false , true , false, false ->
-      ENUM.fully_interpreted sb
-    | false , false , false , false, true, false ->
+    | false, false, false, true, false ->
       ADT.fully_interpreted sb
-    | false , false , false , false, false, true  ->
+    | false, false, false, false, true  ->
       AC.fully_interpreted sb
-    | false , false , false , false, false, false ->
+    | false, false, false, false, false ->
       false
     | _ -> assert false
 
@@ -440,7 +413,6 @@ struct
     not (Options.get_restricted ()) &&
     (RECORDS.is_mine_symb sb ty ||
      BITV.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
@@ -457,19 +429,16 @@ struct
         ARITH.is_mine_symb ac.Sig.h ty,
         RECORDS.is_mine_symb ac.Sig.h ty,
         BITV.is_mine_symb ac.Sig.h ty,
-        ENUM.is_mine_symb ac.Sig.h ty,
         ADT.is_mine_symb ac.Sig.h ty,
         AC.is_mine_symb ac.Sig.h ty with
       (*AC.is_mine may say F if Options.get_no_ac is set to F dynamically *)
-      | true , false, false, false, false, false ->
+      | true, false, false, false, false ->
         ARITH.color ac
-      | false , true  , false, false, false, false ->
+      | false, true, false, false, false ->
         RECORDS.color ac
-      | false , false , true  , false, false, false ->
+      | false, false, true, false, false ->
         BITV.color ac
-      | false , false , false , true , false, false ->
-        ENUM.color ac
-      | false , false , false , false, true, false ->
+      | false, false, false, true, false ->
         ADT.color ac
       | _  -> ac_embed ac
 
@@ -479,7 +448,6 @@ struct
     | Arith a -> ARITH.abstract_selectors a acc
     | Records a -> RECORDS.abstract_selectors a acc
     | Bitv a -> BITV.abstract_selectors a acc
-    | Enum a -> ENUM.abstract_selectors a acc
     | Adt a -> ADT.abstract_selectors a acc
     | Term _ -> a, acc
     | Ac a -> AC.abstract_selectors a acc
@@ -568,10 +536,6 @@ struct
             Timers.with_timer BITV.timer Timers.F_solve @@ fun () ->
             BITV.solve ra rb pb
 
-          | Ty.Tsum _          ->
-            Timers.with_timer ENUM.timer Timers.F_solve @@ fun () ->
-            ENUM.solve ra rb pb
-
           (*| Ty.Tunit           -> pb *)
 
           | Ty.Tadt _ when not (Options.get_disable_adts()) ->
@@ -623,7 +587,6 @@ struct
             Some (Expr.fresh_name (Expr.type_info t), false)
         end
 
-      | _, Ty.Tsum _    -> ENUM.assign_value r distincts eq
       | _, Ty.Tadt _    when not (Options.get_disable_adts()) ->
         ADT.assign_value r distincts eq
 
@@ -700,24 +663,14 @@ and BITV : Sig.SHOSTAK
       let embed = embed3
     end)
 
-and ENUM : Sig.SHOSTAK
-  with type r = CX.r
-   and type t = CX.r Enum.abstract =
-  Enum.Shostak
-    (struct
-      include CX
-      let extract = extract4
-      let embed = embed4
-    end)
-
 and ADT : Sig.SHOSTAK
   with type r = CX.r
    and type t = CX.r Adt.abstract =
   Adt.Shostak
     (struct
       include CX
-      let extract = extract5
-      let embed = embed5
+      let extract = extract4
+      let embed = embed4
     end)
 
 (* Its signature is not Sig.SHOSTAK because it does not provide a solver *)
@@ -758,7 +711,6 @@ end
 module Arith = ARITH
 module Records = RECORDS
 module Bitv = BITV
-module Enum = ENUM
 module Adt = ADT
 module Polynome = TARITH
 module Ac = AC
diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli
index 88226887a..0067e7df9 100644
--- a/src/lib/reasoners/shostak.mli
+++ b/src/lib/reasoners/shostak.mli
@@ -44,9 +44,6 @@ module Records : Sig.SHOSTAK
 module Bitv : Sig.SHOSTAK
   with type r = Combine.r and type t = Combine.r Bitv.abstract
 
-module Enum : Sig.SHOSTAK
-  with type r = Combine.r and type t = Combine.r Enum.abstract
-
 module Adt : Sig.SHOSTAK
   with type r = Combine.r and type t = Combine.r Adt.abstract
 
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 9c0a59ee5..199e8f5df 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -159,16 +159,13 @@ module Main_Default : S = struct
            | Tint | Treal | Tbool | Tunit | Tbitv _ | Tfarray _ -> mp
            | Tvar _ -> assert false
 
-           | Text (_, hs) | Tsum (hs, _) | Trecord { name = hs; _ } when
+           | Text (_, hs) | Trecord { name = hs; _ } when
                Uid.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
 
-           | Tsum (hs, _) ->
-             Uid.Map.add hs ty mp
-
            | Trecord { name; _ } ->
              (* cannot do better for records ? *)
              Uid.Map.add name ty mp
@@ -187,19 +184,6 @@ module Main_Default : S = struct
            | Tint | Treal | Tbool | Tunit | Tbitv _ | Tfarray _ -> ()
            | Tvar _ -> assert false
            | Text _ -> print_dbg ~flushed:false "type %a@ " Ty.print ty
-           | Tsum (_, l) ->
-             print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty;
-             begin match l with
-               | [] -> assert false
-               | e::l ->
-                 let print fmt e =
-                   Format.fprintf fmt " | %a" Uid.pp e
-                 in
-                 print_dbg ~flushed:false ~header:false "%a@ %a@ "
-                   Uid.pp e
-                   (pp_list_no_space print) l;
-             end
-
            | Trecord { Ty.lbs; _ } ->
              print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty;
              begin match lbs with
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 5b2c08c93..3e76084d6 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -2581,7 +2581,6 @@ let mk_match e cases =
     match ty with
     | Ty.Tadt _ -> (fun hs -> Sy.destruct hs)
     | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs))
-    | Ty.Tsum _ -> (fun _hs -> assert false) (* no destructors for Tsum *)
     | _ -> assert false
   in
   let mker =
@@ -2593,13 +2592,6 @@ let mk_match e cases =
     | Ty.Trecord _ ->
       (fun _e _name -> assert false) (* no need to test for records *)
 
-    | Ty.Tsum _ ->
-      (fun e n -> (* testers are equalities for Tsum *)
-         let constr =
-           mk_term (Sy.constr n) [] (type_info e)
-         in
-         mk_eq ~iff:false e constr)
-
     | _ -> assert false
   in
   let res = compile_match mk_destr mker e cases e in
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index c94442bc1..d12e38d51 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -75,7 +75,7 @@ let string_of_rounding_mode = to_smt_string
 
 let hstring_smt_reprs =
   List.map
-    (fun c -> Hs.make (to_smt_string c))
+    (fun c -> to_smt_string c, [])
     cstrs
 
 let hstring_ae_reprs =
@@ -92,18 +92,21 @@ 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 _, cstrs = DE.Term.define_adt ty_cst [] cstrs in
-  DE.Ty.apply ty_cst [], cstrs,
-  Ty.Tsum (Uid.of_dolmen ty_cst, List.map (fun (c, _) -> Uid.of_dolmen c) cstrs)
+  let _, d_cstrs = DE.Term.define_adt ty_cst [] cstrs in
+  let body =
+    List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
+  in
+  let ty = Ty.t_adt ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
+  DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =
   let table = Hashtbl.create 5 in
   List.iter2 (
-    fun key bnd ->
+    fun (key, _) bnd ->
       Hashtbl.add table key bnd
   ) hstring_smt_reprs cstrs;
   fun key ->
-    try Hashtbl.find table key with
+    try Hashtbl.find table (Hstring.view key) with
     | Not_found ->
       Fmt.failwith
         "Error while searching for SMT2 FPA value %a."
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index e1e9621c4..3eaaa6030 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -34,7 +34,6 @@ type t =
   | Tbitv of int
   | Text of t list * Uid.t
   | Tfarray of t * t
-  | Tsum of Uid.t * Uid.t list
   | Tadt of Uid.t * t list
   | Trecord of trecord
 
@@ -55,7 +54,7 @@ module Smtlib = struct
     | Tbitv n -> Fmt.pf ppf "(_ BitVec %d)" n
     | Tfarray (a_t, r_t) ->
       Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t
-    | Text ([], name) | Tsum (name, _)
+    | Text ([], name)
     | Trecord { args = []; name; _ } | Tadt (name, []) -> Uid.pp ppf name
     | Text (args, name)
     | Trecord { args; name; _ } | Tadt (name, args) ->
@@ -122,8 +121,6 @@ let print_generic body_of =
         fprintf fmt "%a <ext>%a" print_list l Uid.pp s
       | Tfarray (t1, t2) ->
         fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2
-      | Tsum(s, _) ->
-        fprintf fmt "<sum>%a" Uid.pp s
       | Trecord { args = lv; name = n; lbs = lbls; _ } ->
         begin
           fprintf fmt "%a <record>%a" print_list lv Uid.pp n;
@@ -228,7 +225,7 @@ let rec shorten ty =
     (* should not rebuild the type if no changes are made *)
     Tadt (n, args')
 
-  | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) -> ty
+  | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
 
 and shorten_body _ _ =
   ()
@@ -248,9 +245,6 @@ let rec compare t1 t2 =
     if c<>0 then c
     else compare ta2 tb2
   | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1
-  | Tsum(s1, _), Tsum(s2, _) ->
-    Uid.compare s1 s2
-  | Tsum _, _ -> -1 | _ , Tsum _ -> 1
   | Trecord { args = a1; name = s1; lbs = l1; _ },
     Trecord { args = a2; name = s2; lbs = l2; _ } ->
     let c = Uid.compare s1 s2 in
@@ -300,7 +294,6 @@ let rec equal t1 t2 =
      with Invalid_argument _ -> false)
   | Tfarray (ta1, ta2), Tfarray (tb1, tb2) ->
     equal ta1 tb1 && equal ta2 tb2
-  | Tsum (s1, _), Tsum (s2, _) -> Uid.equal s1 s2
   | Trecord { args = a1; name = s1; lbs = l1; _ },
     Trecord { args = a2; name = s2; lbs = l2; _ } ->
     begin
@@ -343,7 +336,6 @@ let rec matching s pat t =
     let s = List.fold_left2 matching s r1.args r2.args in
     List.fold_left2
       (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs
-  | Tsum (s1, _), Tsum (s2, _) when Uid.equal s1 s2 -> s
   | Tint , Tint | Tbool , Tbool | Treal , Treal | Tunit, Tunit -> s
   | Tbitv n , Tbitv m when n=m -> s
   | Tadt(n1, args1), Tadt(n2, args2) when Uid.equal n1 n2 ->
@@ -381,7 +373,7 @@ let apply_subst =
       ->
       Tadt (name, List.map (apply_subst s) params)
 
-    | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) -> ty
+    | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
   in
   fun s ty -> if M.is_empty s then ty else apply_subst s ty
 
@@ -537,8 +529,6 @@ let fresh_empty_text =
     in
     text [] (Uid.of_dolmen id)
 
-let tsum s lc = Tsum (s, lc)
-
 let t_adt ?(body=None) s ty_vars =
   let ty = Tadt (s, ty_vars) in
   begin match body with
@@ -585,9 +575,9 @@ let rec hash t =
         (abs h) lbs
     in
     abs h
-  | Tsum (s, _) -> abs (Uid.hash s) (*we do not hash constructors*)
 
   | Tadt (s, args) ->
+    (* We do not hash constructors. *)
     let h =
       List.fold_left (fun h ty -> 31 * h + hash ty) (Uid.hash s) args
     in
@@ -601,7 +591,7 @@ let occurs { v = n; _ } t =
     | Text(l,_) -> List.exists occursrec l
     | Tfarray (t1,t2) -> occursrec t1 || occursrec t2
     | Trecord { args ; _ } | Tadt (_, args) -> List.exists occursrec args
-    | Tsum _ | Tint | Treal | Tbool | Tunit | Tbitv _ -> false
+    | Tint | Treal | Tbool | Tunit | Tbitv _ -> false
   in occursrec t
 
 (*** destructive unification ***)
@@ -622,7 +612,6 @@ let rec unify t1 t2 =
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> unify ta1 tb1;unify ta2 tb2
   | Trecord r1, Trecord r2 when Uid.equal r1.name r2.name ->
     List.iter2 unify r1.args r2.args
-  | Tsum(s1, _) , Tsum(s2, _) when Uid.equal s1 s2 -> ()
   | Tint, Tint | Tbool, Tbool | Treal, Treal | Tunit, Tunit -> ()
   | Tbitv n , Tbitv m when m=n -> ()
 
@@ -673,7 +662,7 @@ let vty_of t =
       List.fold_left vty_of_rec acc args
 
     | Tvar { value = Some _ ; _ }
-    | Tint | Treal | Tbool | Tunit | Tbitv _ | Tsum (_, _) ->
+    | Tint | Treal | Tbool | Tunit | Tbitv _ ->
       acc
   in
   vty_of_rec Svty.empty t
@@ -682,7 +671,7 @@ let vty_of t =
   [@ocaml.ppwarning "TODO: detect when there are no changes "]
 let rec monomorphize ty =
   match ty with
-  | Tint | Treal | Tbool | Tunit   | Tbitv _  | Tsum _ -> ty
+  | Tint | Treal | Tbool | Tunit   | Tbitv _  -> ty
   | Text (tyl,hs) -> Text (List.map monomorphize tyl, hs)
   | Trecord ({ args = tylv; name = n; lbs = tylb; _ } as r) ->
     let m_tylv = List.map monomorphize tylv in
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 5003566a6..d98a51d98 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -48,11 +48,10 @@ type t =
   (** Abstract types applied to arguments. [Text (args, s)] is
       the application of the abstract type constructor [s] to
       arguments [args]. *)
+
   | Tfarray of t * t
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
-  | Tsum of Uid.t * Uid.t list
-  (** Enumeration, with its name, and the list of its constructors. *)
 
   | Tadt of Uid.t * t list
   (** Application of algebraic data types. [Tadt (a, params)] denotes
@@ -169,10 +168,6 @@ val text : t list -> Uid.t -> t
 (** Apply the abstract type constructor to the list of type arguments
     given. *)
 
-val tsum : Uid.t -> Uid.t list -> t
-(** Create an enumeration type. [tsum name enums] creates an enumeration
-    named [name], with constructors [enums]. *)
-
 val t_adt :
   ?body: ((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t
 (** Create an algebraic datatype. The body is a list of