Eager casesplits on enum constructors

As we suggested during a dev meeting, we could try perform casesplits on
constructors of ADTs without payload as we do for enum types, that is we
perform this casesplit after each `assert`. This PR may introduce
annoying regressions.

src/lib/reasoners/adt_rel.ml

@@ -133,7 +133,7 @@ module Domains = struct
 
         We don't store domains for constructors and selectors. *)
 
-    enums: SX.t;
+    enums: Uid.t MX.t;
     (** Set of tracked representatives of enum type. *)
 
     changed : SX.t;
@@ -150,18 +150,23 @@ module Domains = struct
         )
       ppf t.domains
 
-  let empty = { domains = MX.empty; enums = SX.empty; changed = SX.empty }
+  let empty = { domains = MX.empty; enums = MX.empty; changed = SX.empty }
 
   let filter_ty = is_adt_ty
 
-  let is_enum r =
-    match X.type_info r with
-    | Ty.Tadt (_, [], true) -> true
-    | _ -> false
-
   let internal_update r nd t =
     let domains = MX.add r nd t.domains in
-    let enums = if is_enum r then SX.add r t.enums else t.enums in
+    let enums =
+      let cstr = Domain.choose nd in
+      let is_enum =
+        match X.type_info r with
+        | Tadt (name, args, _) ->
+          let Adt body = Ty.type_body name args in
+          Lists.is_empty @@ Ty.assoc_destrs cstr body
+        | _ -> assert false
+      in
+      if is_enum then MX.add r cstr t.enums else t.enums
+    in
     let changed = SX.add r t.changed in
     { domains; enums; changed }
 
@@ -201,7 +206,7 @@ module Domains = struct
 
   let remove r t =
     let domains = MX.remove r t.domains in
-    let enums = SX.remove r t.enums in
+    let enums = MX.remove r t.enums in
     let changed = SX.remove r t.changed in
     { domains; enums; changed }
 
@@ -238,7 +243,7 @@ module Domains = struct
 
   let fold f t = MX.fold f t.domains
 
-  let fold_enums f t = SX.fold f t.enums
+  let fold_enums f t = MX.fold f t.enums
 end
 
 let calc_destructor d e uf =
@@ -646,16 +651,14 @@ let pick_best ds uf =
 
 let pick_enum ds uf =
   Domains.fold_enums
-    (fun r best ->
+    (fun r cstr best ->
        let rr, _ = Uf.find_r uf r in
        let d = Domains.get r ds in
        let cd = Domain.cardinal d in
        match Th.embed rr, best with
        | Constr _, _ -> best
        | _, Some (n, _, _) when n <= cd -> best
-       | _ ->
-         let c = Domain.choose d in
-         Some (cd, r, c)
+       | _ -> Some (cd, r, cstr)
     ) ds None
 
 let split_enum env uf =