Simple ADTs with a single constructor are records

src/lib/frontend/cnf.ml

@@ -115,7 +115,7 @@ let rec make_term quant_basename t =
 
     | TTrecord lbs ->
       let lbs = List.map (fun (_, t) -> mk_term t) lbs in
-      E.mk_term (Sy.Op Sy.Record) lbs ty
+      E.mk_record lbs ty
 
     | TTlet (binders, t2) ->
       let binders =

src/lib/frontend/d_cnf.ml

@@ -970,8 +970,14 @@ let rec mk_expr
             E.mk_term sy [] ty
 
           | B.Constructor _ ->
-            let ty = dty_to_ty term_ty in
-            E.mk_constr (Uid.of_dolmen tcst) [] ty
+            begin match dty_to_ty term_ty with
+              | Trecord _ as ty ->
+                E.mk_record [] ty
+              | Tadt _ as ty ->
+                E.mk_constr (Uid.of_dolmen tcst) [] ty
+              | _ ->
+                assert false
+            end
 
           | _ -> unsupported "Constant term %a" DE.Term.print term
         end
@@ -1343,7 +1349,7 @@ let rec mk_expr
                 E.mk_term sy l ty
               | Ty.Trecord _ ->
                 let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_term (Sy.Op Sy.Record) l ty
+                E.mk_record l ty
               | _ ->
                 Fmt.failwith
                   "Constructor error: %a does not belong to a record nor an\

src/lib/reasoners/adt.ml

@@ -193,8 +193,11 @@ module Shostak (X : ALIEN) = struct
          if equal sel (embed sel_x) then X.term_embed t, ctx
          else sel_x, ctx (* canonization OK *)
     *)
-    | _ ->
-      assert false
+
+    | Sy.Op Sy.Constr _, _, Ty.Trecord _ ->
+      Fmt.failwith "unexpected record constructor %a@." E.print t
+
+    | _ -> assert false
 
   let hash x =
     abs @@ match x with

src/lib/structures/expr.ml

@@ -1264,6 +1264,8 @@ let mk_constr cons xs ty = mk_term (Sy.Op (Constr cons)) xs ty
 let mk_tester cons t =
   mk_builtin ~is_pos:true (Sy.IsConstr cons) [t]
 
+let mk_record xs ty = mk_term (Sy.Op Record) xs ty
+
 (** Substitutions *)
 
 let is_skolem_cst v =

src/lib/structures/expr.mli

@@ -282,6 +282,7 @@ val mk_ite : t -> t -> t -> t
 
 val mk_constr : Uid.t -> t list -> Ty.t -> t
 val mk_tester : Uid.t -> t -> t
+val mk_record : t list -> Ty.t -> t
 
 (** Substitutions *)