diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml
index 391aa95ea..31f2cd0d2 100644
--- a/src/lib/reasoners/enum_rel.ml
+++ b/src/lib/reasoners/enum_rel.ml
@@ -28,32 +28,181 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module A  = Xliteral
 module L  = List
-module Hs = Hstring
+module X = Shostak.Combine
+module Ex = Explanation
+module MX = Shostak.MXH
+module SX = Shostak.SXH
+module HSS = Set.Make (Hstring)
+module LR = Uf.LX
+module Th = Shostak.Enum
 
 let timer = Timers.M_Sum
 
-type 'a abstract = 'a Enum.abstract =
-  | Cons of Hs.t * Ty.t
-  | Alien of 'a
+module Domain = struct
+  type t = {
+    constrs : HSS.t;
+    ex : Ex.t;
+  }
 
-module X = Shostak.Combine
-module Sh = Shostak.Enum
+  exception Inconsistent of Ex.t
 
-module Ex = Explanation
+  let[@inline always] cardinal { constrs; _ } = HSS.cardinal constrs
 
-module MX = Shostak.MXH
-module HSS = Set.Make (struct type t=Hs.t let compare = Hs.compare end)
+  let[@inline always] choose { constrs; _ } = HSS.choose constrs
 
-module LR = Uf.LX
+  let[@inline always] as_singleton { constrs; _ } =
+    if HSS.cardinal constrs = 1 then
+      Some (HSS.choose constrs)
+    else
+      None
+
+  let domain ~constrs ex =
+    if HSS.is_empty constrs then
+      raise_notrace @@ Inconsistent ex
+    else
+      { constrs; ex }
+
+  let[@inline always] singleton ~ex c = { constrs = HSS.singleton c; ex }
+
+  let[@inline always] subset d1 d2 = HSS.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 = HSS.of_list constrs in
+      assert (not @@ HSS.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 = HSS.equal d1.constrs d2.constrs
+
+  let pp ppf d =
+    Fmt.(braces @@
+         iter ~sep:comma HSS.iter Hstring.print) 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 = HSS.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 = HSS.remove c d.constrs in
+    let ex = Ex.union ex d.ex in
+    domain ~constrs ex
+end
+
+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]. *)
+  }
+
+  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 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 (r, _) ->
+      (* For sake of efficiency, we don't look in the map if the
+         semantic value is a constructor. *)
+      Domain.singleton ~ex:Explanation.empty r
+    | _ ->
+      try MX.find r t.domains
+      with Not_found ->
+        Domain.unknown (X.type_info r)
+
+  let add r t =
+    if MX.mem r t.domains then t
+    else
+      match Th.embed r with
+      | Cons _ -> t
+      | _ ->
+        (* 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
+
+  (** [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]. *)
+    assert (not (Options.get_enable_assertions ()) || 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 }
+
+  (** [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 -> 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 = {
-  (* TODO: rename the field domains to be consistent with the ADT theory. *)
-  mx : (HSS.t * Ex.t) MX.t;
-  (* Map of uninterpreted enum semantic values to domains of their possible
-     values. The explanation justifies that any value assigned to the semantic
-     value has to lie in the domain. *)
+  domains : Domains.t;
+  (* Map of class representatives of enum semantic values to their
+     domains. *)
 
   classes : Expr.Set.t list;
   (* State of the union-find represented by all its equivalence classes.
@@ -68,265 +217,205 @@ type t = {
      [Options.get_max_split ()]. *)
 }
 
-let empty classes = {
-  mx = MX.empty;
-  classes = classes;
-  size_splits = Numbers.Q.one
-}
-
 (*BISECT-IGNORE-BEGIN*)
 module Debug = struct
-  open Printer
-
-  let assume bol r1 r2 =
+  let assume l =
     if Options.get_debug_sum () then
-      print_dbg
-        ~module_name:"Enum_rel" ~function_name:"assume"
-        "we assume %a %s %a"
-        X.print r1 (if bol then "=" else "<>") X.print r2
-
-  let print_env env =
-    if Options.get_debug_sum () then begin
-      Printer.print_dbg ~flushed:false
-        ~module_name:"Enum_rel" ~function_name:"print_env"
-        "@[<v 2>--SUM env ---------------------------------@ ";
-      MX.iter
-        (fun r (hss, ex) ->
-           Printer.print_dbg  ~flushed:false ~header:false
-             "%a ::= " X.print r;
-           begin
-             match HSS.elements hss with
-               []      -> ()
-             | hs :: l ->
-               Printer.print_dbg  ~flushed:false ~header:false
-                 " %s" (Hs.view hs);
-               L.iter (fun hs ->
-                   Printer.print_dbg  ~flushed:false ~header:false
-                     " | %s" (Hs.view hs)) l
-           end;
-           Printer.print_dbg ~flushed:false ~header:false
-             " : %a@ " Ex.print ex;
-        ) env.mx;
-      Printer.print_dbg ~header:false
-        "@ -------------------------------------------";
-    end
-
-  let case_split r r' =
+      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 r X.print r'
+      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:"no_case_split"
-        "sum: nothing"
+      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"
+      Printer.print_dbg ~module_name:"Enum_rel" ~function_name:"add"
         "%a" X.print r
 
+  let pp_env env =
+    if Options.get_debug_sum () then
+      Printer.print_dbg ~module_name:"Enum_rel"
+        "The environment before assuming:@ @[%a@]" Domains.pp env.domains
 end
 (*BISECT-IGNORE-END*)
 
-(* Return the list of all the constructors of the type of [r]. *)
-let values_of r =
-  match X.type_info r with
-  | Ty.Tsum (_,l) ->
-    Some (List.fold_left (fun st hs -> HSS.add hs st) HSS.empty l)
-  | _ ->
-    (* This case can happen since we don't dispatch the literals
-       processed in [assume] by their types in the Relation module. *)
-    None
-
-(* Update the domains of the semantic values [sm1] and [sm2] according to
-   the disequality [sm1 <> sm2]. More precisely, if one of these semantic
-   values is a constructor, we remove it from the domain of the other one.
-
-   In any case, we produce an equality if the domain of one of these semantic
-   values becomes a singleton.
-
-   @raise Ex.Inconsistent if the disequality is inconsistent with the
-   current environment [env]. *)
-let add_diseq hss sm1 sm2 dep env eqs =
-  match sm1, sm2 with
-  | Alien r , Cons(h,ty)
-  | Cons (h,ty), Alien r  ->
-    let enum, ex = try MX.find r env.mx with Not_found -> hss, Ex.empty in
-    let enum = HSS.remove h enum in
-    let ex = Ex.union ex dep in
-    if HSS.is_empty enum then raise (Ex.Inconsistent (ex, env.classes))
-    else
-      let env = { env with mx = MX.add r (enum, ex) env.mx } in
-      if HSS.cardinal enum = 1 then
-        let h' = HSS.choose enum in
-        env,
-        (Literal.LSem (LR.mkv_eq r (Sh.is_mine (Cons(h',ty)))),
-         ex, Th_util.Other)::eqs
-      else env, eqs
-
-  | Alien r1, Alien r2 ->
-    let enum1,ex1= try MX.find r1 env.mx with Not_found -> hss,Ex.empty in
-    let enum2,ex2= try MX.find r2 env.mx with Not_found -> hss,Ex.empty in
-
-    let eqs =
-      if HSS.cardinal enum1 = 1 then
-        let ex = Ex.union dep ex1 in
-        let h' = HSS.choose enum1 in
-        let ty = X.type_info r1 in
-        (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
-         ex, Th_util.Other)::eqs
-      else eqs
-    in
-    let eqs =
-      if HSS.cardinal enum2 = 1 then
-        let ex = Ex.union dep ex2 in
-        let h' = HSS.choose enum2 in
-        let ty = X.type_info r2 in
-        (Literal.LSem (LR.mkv_eq r2 (Sh.is_mine (Cons(h',ty)))),
-         ex, Th_util.Other)::eqs
-      else eqs
-    in
-    env, eqs
-
-  |  _ -> env, eqs
-
-(* Update the domains of the semantic values [sm1] and [sm2] according to
-   the equation [sm1 = sm2]. More precisely, we replace their domains by
-   the intersection of these domains.
-
-   @raise Ex.Inconsistent if the domains of [sm1] and [sm2] are disjoint. *)
-let add_eq hss sm1 sm2 dep env eqs =
-  match sm1, sm2 with
-  | Alien r, Cons(h,_)
-  | Cons (h,_), Alien r  ->
-    let enum, ex = try MX.find r env.mx with Not_found -> hss, Ex.empty in
-    let ex = Ex.union ex dep in
-    if not (HSS.mem h enum) then raise (Ex.Inconsistent (ex, env.classes));
-    (* We don't need to produce a new equality as we are already processing
-       it. *)
-    {env with mx = MX.add r (HSS.singleton h, ex) env.mx} , eqs
-
-  | Alien r1, Alien r2   ->
-    let enum1,ex1 =
-      try MX.find r1 env.mx with Not_found -> hss, Ex.empty in
-    let enum2,ex2 =
-      try MX.find r2 env.mx with Not_found -> hss, Ex.empty in
-    let ex = Ex.union dep (Ex.union ex1 ex2) in
-    let diff = HSS.inter enum1 enum2 in
-    if HSS.is_empty diff then raise (Ex.Inconsistent (ex, env.classes));
-    let mx = MX.add r1 (diff, ex) env.mx in
-    let env = {env with mx = MX.add r2 (diff, ex) mx } in
-
-    (* We produce an equality if the domain of these semantic values becomes
-       a singleton. *)
-    if HSS.cardinal diff = 1 then
-      let h' = HSS.choose diff in
-      let ty = X.type_info r1 in
-      env, (Literal.LSem (LR.mkv_eq r1 (Sh.is_mine (Cons(h',ty)))),
-            ex, Th_util.Other)::eqs
-    else env, eqs
-
-  |  _ -> env, eqs
+let empty classes = {
+  domains = Domains.empty;
+  classes = classes;
+  size_splits = Numbers.Q.one
+}
 
 (* Update the counter of case-split size in [env]. *)
 let count_splits env la =
   let nb =
     List.fold_left
-      (fun nb (_,_,_,i) ->
+      (fun nb (_, _, _, i) ->
          match i with
          | Th_util.CS (Th_util.Th_sum, n) -> Numbers.Q.mult nb n
          | _ -> nb
-      )env.size_splits la
+      ) env.size_splits la
   in
   {env with size_splits = nb}
 
-(* Add the uninterpreted semantic value [r] to the environment [env] with
-   all the constructors of its type as domain. *)
-let add_aux env r =
-  Debug.add r;
-  match Sh.embed r, values_of r with
-  | Alien r, Some hss ->
-    if MX.mem r env.mx then env else
-      { env with mx = MX.add r (hss, Ex.empty) env.mx }
-  | _ -> env
+let tighten_domain rr nd env =
+  { env with domains = Domains.tighten rr nd env.domains }
+
+(* Update the domains of the semantic values [r1] and [r2] according to
+   the substitution `r1 |-> r2`.
+
+   @raise Domain.Inconsistent if this substitution is inconsistent with
+          the current environment [env]. *)
+let assume_subst ~ex r1 r2 env =
+  { env with domains = Domains.subst ~ex r1 r2 env.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 env =
+  let d1 = Domains.get r1 env.domains in
+  let d2 = Domains.get r2 env.domains in
+  let env =
+    match Domain.as_singleton d1 with
+    | Some c ->
+      let nd = Domain.remove ~ex c d2 in
+      tighten_domain r2 nd env
+    | None ->
+      env
+  in
+  match Domain.as_singleton d2 with
+  | Some c ->
+    let nd = Domain.remove ~ex c d1 in
+    tighten_domain r1 nd env
+  | None ->
+    env
+
+let is_enum r =
+  match X.type_info r with
+  | Ty.Tsum _ -> true
+  | _ -> false
 
-(* Needed for models generation because fresh terms are not added with function
-   add. *)
-let add_rec env r = List.fold_left add_aux env (X.leaves r)
+let add r uf env =
+  match X.type_info r with
+  | Ty.Tsum _ ->
+    Debug.add r;
+    let rr, _ = Uf.find_r uf r in
+    { env with domains = Domains.add rr env.domains }
+  | _ ->
+    env
+
+let add_rec r uf env =
+  List.fold_left (fun env leaf -> add leaf uf env) env (X.leaves r)
+
+let add env uf r _t = add r uf env, []
+
+let assume_literals la uf env =
+  List.fold_left
+    (fun env lit ->
+       let open Xliteral in
+       match lit with
+       | Eq (r1, r2) as l, _, ex, Th_util.Subst when is_enum r1 ->
+         Debug.assume l;
+         (* Needed for models generation because fresh terms are not added with
+            the function add. *)
+         let env = add_rec r1 uf env in
+         let env = add_rec r2 uf env in
+         assume_subst ~ex r1 r2 env
+
+       | 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 env = add_rec r1 uf env in
+         let env = add_rec r2 uf env in
+         assume_distinct ~ex r1 r2 env
+
+       | _ ->
+         (* We ignore [Eq] literals that aren't substitutions as the propagation
+            of such equalities will produce substitutions later.
+            More precisely, the equation [Eq (r1, r2)] will produce two
+            substitutions:
+              [Eq (r1, rr)] and [Eq (r2, rr)]
+            where [rr] is the new class representative. *)
+         env
+    ) env la
+
+let propagate_domains env =
+  Domains.propagate
+    (fun eqs rr d ->
+       match Domain.as_singleton d with
+       | Some c ->
+         let nr = Th.is_mine (Cons (c, X.type_info rr)) in
+         let eq = Literal.LSem (LR.mkv_eq rr nr), d.ex, Th_util.Other in
+         eq :: eqs
+       | None ->
+         eqs
+    ) [] env.domains
 
 let assume env uf la =
+  Debug.pp_env env;
   let env = count_splits env la in
   let classes = Uf.cl_extract uf in
   let env = { env with classes = classes } in
-  let aux bol r1 r2 dep env eqs = function
-    | None     -> env, eqs
-    | Some hss ->
-      Debug.assume bol r1 r2;
-      if bol then
-        add_eq hss (Sh.embed r1) (Sh.embed r2) dep env eqs
-      else
-        add_diseq hss (Sh.embed r1) (Sh.embed r2) dep env eqs
-  in
-  Debug.print_env env;
-  let env, eqs =
-    List.fold_left
-      (fun (env,eqs) -> function
-         | A.Eq(r1,r2), _, ex, _ ->
-           (* needed for models generation because fresh terms are not
-              added with function add *)
-           let env = add_rec (add_rec env r1) r2 in
-           aux true  r1 r2 ex env eqs (values_of r1)
-
-         | A.Distinct(false, [r1;r2]), _, ex, _ ->
-           (* needed for models generation because fresh terms are not
-              added with function add *)
-           let env = add_rec (add_rec env r1) r2 in
-           aux false r1 r2 ex env eqs (values_of r1)
-
-         | _ -> env, eqs
-
-      ) (env,[]) la
+  let env =
+    try
+      assume_literals la uf env
+    with Domain.Inconsistent ex ->
+      raise_notrace (Ex.Inconsistent (ex, env.classes))
   in
-  env, { Sig_rel.assume = eqs; remove = [] }
+  let assume, domains = propagate_domains env in
+  { env with domains }, Sig_rel.{ assume; remove = [] }
 
-let add env _ r _ = add_aux env r, []
+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 value for an uninterpreted semantic value
-   whose domain in [env] is of minimal size. *)
+(* Do a case-split by choosing a constructor for class representatives of
+   minimal size. *)
 let case_split env uf ~for_model =
-  let acc = MX.fold
-      (fun r (hss, _) acc ->
-         let x, _ = Uf.find_r uf r in
-         match Sh.embed x with
-         | Cons _ ->
-           (* The equivalence class of [r] already contains a value so
-              we don't need to make another case-split for this semantic
-              value. *)
-           acc
-         | _ ->
-           (* We have to perform a case-split, even if the domain of [r] is
-              of cardinal 1 as we have to let the union-find know this
-              equality. *)
-           let sz = HSS.cardinal hss in
-           match acc with
-           | Some (n,_,_) when n <= sz -> acc
-           | _ -> Some (sz, r, HSS.choose hss)
-      ) env.mx None
+  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)
+      ) env.domains None
   in
-  match acc with
-  | Some (n,r,hs) ->
+  match best with
+  | Some (n, r, c) ->
     let n = Numbers.Q.from_int n in
-    if for_model ||
-       Numbers.Q.compare
-         (Numbers.Q.mult n env.size_splits) (Options.get_max_split ()) <= 0  ||
-       Numbers.Q.sign  (Options.get_max_split ()) < 0 then
-      let r' = Sh.is_mine (Cons(hs,X.type_info r)) in
-      Debug.case_split r r';
-      [LR.mkv_eq r r', true, Th_util.CS (Th_util.Th_sum, n)]
+    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 ->
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
index fb17f1528..23232ae7b 100644
--- a/src/lib/reasoners/rel_utils.ml
+++ b/src/lib/reasoners/rel_utils.ml
@@ -250,7 +250,7 @@ end
 module type Domains = sig
   type t
   (** The type of domain maps. A domain map maps each representative (semantic
-      value, of type [X.r]) to its associated domain.*)
+      value, of type [X.r]) to its associated domain. *)
 
   val pp : t Fmt.t
   (** Pretty-printer for domain maps. *)
@@ -269,7 +269,7 @@ module type Domains = sig
   val add : X.r -> t -> t
   (** [add r t] adds a domain for [r] in the domain map. If [r] does not
       already have an associated domain, a fresh domain will be created for
-      [r]. *)
+      [r] using [Domain.unknown]. *)
 
   val get : X.r -> t -> elt
   (** [get r t] returns the domain currently associated with [r] in [t]. *)