diff --git a/src/lib/dune b/src/lib/dune
index 4abcc7c748..b32a54d785 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -50,7 +50,7 @@
     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
+    Polynome Satml_frontend_hybrid Satml_frontend Satml
     Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils Bitlist
     ; structures
     Commands Errors Explanation Fpa_rounding
diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml
index 14a641b61d..47d2826988 100644
--- a/src/lib/frontend/cnf.ml
+++ b/src/lib/frontend/cnf.ml
@@ -107,12 +107,20 @@ let rec make_term quant_basename t =
       E.mk_term (Sy.Op Sy.Concat)
         [mk_term t1; mk_term t2] ty
 
-    | TTdot (t, s) ->
-      E.mk_term (Sy.Op (Sy.Access s)) [mk_term t] ty
-
-    | TTrecord lbs ->
+    | TTrecord (ty, lbs) ->
       let lbs = List.map (fun (_, t) -> mk_term t) lbs in
-      E.mk_term (Sy.Op Sy.Record) lbs ty
+      let cstr =
+        match ty with
+        | Tadt (name, params, true) ->
+          begin
+            let Adt cases = Ty.type_body name params in
+            match cases with
+            | [{ constr; _ }] -> Hstring.view constr
+            | _ -> assert false
+          end
+        | _ -> assert false
+      in
+      E.mk_constr cstr lbs ty
 
     | TTlet (binders, t2) ->
       let binders =
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index faf10c54c4..4cd1bb399a 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -197,7 +197,7 @@ let ty name ty =
   Dolmen_type.Base.app0 (module Dl.Typer.T) env s ty
 
 let builtin_enum = function
-  | Ty.Tadt (name, params) as ty_ ->
+  | Ty.Tadt (name, params, _) as ty_ ->
     let Adt cases = Ty.type_body name params in
     let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
     let ty_cst =
@@ -505,53 +505,11 @@ let rec dty_to_ty ?(update = false) ?(is_var = false) dty =
   | _ -> unsupported "Type %a" DE.Ty.print dty
 
 and handle_ty_app ?(update = false) ty_c l =
-  (* Applies the substitutions in [tysubsts] to each encountered type
-     variable. *)
-  let rec apply_ty_substs tysubsts ty =
-    match ty with
-    | Ty.Tvar { v; _ } ->
-      Ty.M.find v tysubsts
-
-    | Text (tyl, hs) ->
-      Ty.Text (List.map (apply_ty_substs tysubsts) tyl, hs)
-
-    | Tfarray (ti, tv) ->
-      Tfarray (
-        apply_ty_substs tysubsts ti,
-        apply_ty_substs tysubsts tv
-      )
-
-    | Tadt (hs, tyl) ->
-      Tadt (hs, List.map (apply_ty_substs tysubsts) tyl)
-
-    | Trecord ({ args; lbs; _ } as rcrd) ->
-      Trecord {
-        rcrd with
-        args = List.map (apply_ty_substs tysubsts) args;
-        lbs = List.map (
-            fun (hs, t) ->
-              hs, apply_ty_substs tysubsts t
-          ) lbs;
-      }
-
-    | _ -> ty
-  in
   let tyl = List.map (dty_to_ty ~update) l in
   (* Recover the initial versions of the types and apply them on the provided
      type arguments stored in [tyl]. *)
   match Cache.find_ty (DE.Ty.Const.hash ty_c) with
-  | Tadt (hs, _) -> Tadt (hs, tyl)
-
-  | Trecord { args; _ } as ty ->
-    let tysubsts =
-      List.fold_left2 (
-        fun acc tv ty ->
-          match tv with
-          | Ty.Tvar { v; _ } -> Ty.M.add v ty acc
-          | _ -> assert false
-      ) Ty.M.empty args tyl
-    in
-    apply_ty_substs tysubsts ty
+  | Tadt (hs, _, record) -> Tadt (hs, tyl, record)
 
   | Text (_, s) -> Text (tyl, s)
   | _ -> assert false
@@ -559,32 +517,6 @@ and handle_ty_app ?(update = false) ty_c l =
 (** Handles a simple type declaration. *)
 let mk_ty_decl (ty_c: DE.ty_cst) =
   match DT.definition ty_c with
-  | Some (
-      Adt { cases = [| { cstr = { id_ty; path; _ }; dstrs; _ } |]; _ }
-    ) ->
-    (* Records and adts that only have one case are treated in the same way,
-       and considered as records. *)
-    let tyvl = Cache.store_ty_vars_ret id_ty in
-    let rev_lbs =
-      Array.fold_left (
-        fun acc c ->
-          match c with
-          | Some DE.{ path; id_ty; _ } ->
-            let pn = get_basename path in
-            let pty = dty_to_ty id_ty in
-            (pn, pty) :: acc
-          | _ ->
-            Fmt.failwith
-              "Unexpected null label for some field of the record type %a"
-              DE.Ty.Const.print ty_c
-
-      ) [] dstrs
-    in
-    let lbs = List.rev rev_lbs in
-    let record_constr = Format.asprintf "%a" DStd.Path.print path in
-    let ty = Ty.trecord ~record_constr tyvl (get_basename ty_c.path) lbs in
-    Cache.store_ty (DE.Ty.Const.hash ty_c) ty
-
   | Some (
       (Adt { cases; _ } as _adt)
     ) ->
@@ -662,35 +594,9 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
 let mk_mr_ty_decls (tdl: DE.ty_cst list) =
   let handle_ty_decl (ty: Ty.t) (tdef: DE.Ty.def option) =
     match ty, tdef with
-    | Trecord { args; name; record_constr; _ },
+    | Tadt (hs, tyl, _),
       Some (
-        Adt { cases = [| { dstrs; _ } |]; ty = ty_c; _ }
-      ) ->
-      let rev_lbs =
-        Array.fold_left (
-          fun acc c ->
-            match c with
-            | Some DE.{ path; id_ty; _ } ->
-              let pn = get_basename path in
-              let pty = dty_to_ty id_ty in
-              (pn, pty) :: acc
-            | _ ->
-              Fmt.failwith
-                "Unexpected null label for some field of the record type %a"
-                DE.Ty.Const.print ty_c
-        ) [] dstrs
-      in
-      let lbs = List.rev rev_lbs in
-      let name = Hstring.view name in
-      let record_constr = Hstring.view record_constr in
-      let ty =
-        Ty.trecord ~record_constr args name lbs
-      in
-      Cache.store_ty (DE.Ty.Const.hash ty_c) ty
-
-    | Tadt (hs, tyl),
-      Some (
-        Adt { cases; ty = ty_c; _ }
+        Adt { cases; ty = ty_c; record }
       ) ->
       let rev_cs =
         Array.fold_left (
@@ -710,30 +616,18 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
       in
       let body = Some (List.rev rev_cs) in
       let args = tyl in
-      let ty = Ty.t_adt ~body (Hstring.view hs) args in
+      let ty = Ty.t_adt ~record ~body (Hstring.view hs) args in
       Cache.store_ty (DE.Ty.Const.hash ty_c) ty
 
     | _ -> assert false
   in
-  (* If there are adts in the list of type declarations then records are
-     converted to adts, because that's how it's done in the legacy typechecker.
-     But it might be more efficient not to do that. *)
-  let rev_tdefs, contains_adts =
-    List.fold_left (
-      fun (acc, ca) ty_c ->
-        match DT.definition ty_c with
-        | Some (Adt { record; cases; _ }) as df
-          when not record && Array.length cases > 1 ->
-          df :: acc, true
-        | df -> df :: acc, ca
-    ) ([], false) tdl
-  in
+  let rev_tdefs = List.rev_map DT.definition tdl in
   let rev_l =
     List.fold_left (
       fun acc tdef ->
         match tdef with
         | Some (
-            (DE.Adt { cases; record; ty = ty_c; }) as adt
+            (DE.Adt { cases; ty = ty_c; _ }) as adt
           ) ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
           let name = get_basename ty_c.path in
@@ -754,15 +648,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             acc
           )
           else (
-            let ty =
-              if (record || Array.length cases = 1) && not contains_adts
-              then
-                let record_constr =
-                  Format.asprintf "%a" DStd.Path.print ty_c.path
-                in
-                Ty.trecord ~record_constr tyvl name []
-              else Ty.t_adt name tyvl
-            in
+            let ty = Ty.t_adt name tyvl in
             Cache.store_ty (DE.Ty.Const.hash ty_c) ty;
             (ty, Some adt) :: acc
           )
@@ -1042,10 +928,7 @@ let rec mk_expr
                     let e = aux_mk_expr x in
                     let sy =
                       match Cache.find_ty (DE.Ty.Const.hash adt) with
-                      | Trecord _ ->
-                        Sy.Op (Sy.Access (Hstring.make name))
-                      | Tadt _ ->
-                        Sy.destruct name
+                      | Tadt _ -> Sy.destruct name
                       | _ -> assert false
                     in
                     E.mk_term sy [e] ty
@@ -1077,11 +960,6 @@ let rec mk_expr
               match Cache.find_ty (DE.Ty.Const.hash ty_c) with
               | Ty.Tadt _ ->
                 E.mk_builtin ~is_pos:true builtin [aux_mk_expr x]
-              | Ty.Trecord _ ->
-                (* The typechecker allows only testers whose the
-                   two arguments have the same type. Thus, we can always
-                   replace the tester of a record by the true literal. *)
-                E.vrai
               | _ -> assert false
             end
 
@@ -1368,13 +1246,10 @@ let rec mk_expr
             let name = get_basename path in
             let ty = dty_to_ty term_ty in
             begin match ty with
-              | Ty.Tadt (_, _) ->
+              | Ty.Tadt _ ->
                 let sy = Sy.Op (Sy.Constr (Hstring.make name)) in
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 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
               | _ ->
                 Fmt.failwith
                   "Constructor error: %a does not belong to a record nor an\
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 4ed2f92ec2..9207b718f2 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -53,7 +53,7 @@ module Pp_smtlib_term = struct
     asprintf "%a" Ty.pp_smtlib t
 
   let rec print fmt t =
-    let {Expr.f;xs;ty; _} = Expr.term_view t in
+    let {Expr.f;xs; _} = Expr.term_view t in
     match f, xs with
 
     | Sy.Lit lit, xs ->
@@ -149,26 +149,6 @@ module Pp_smtlib_term = struct
     | Sy.Op Sy.Extract (i, j), [e] ->
       fprintf fmt "%a^{%d,%d}" print e i j
 
-    | Sy.Op (Sy.Access field), [e] ->
-      if Options.get_output_smtlib () then
-        fprintf fmt "(%s %a)" (Hstring.view field) print e
-      else
-        fprintf fmt "%a.%s" print e (Hstring.view field)
-
-    | Sy.Op (Sy.Record), _ ->
-      begin match ty with
-        | Ty.Trecord { Ty.lbs = lbs; _ } ->
-          assert (List.length xs = List.length lbs);
-          fprintf fmt "{";
-          ignore (List.fold_left2 (fun first (field,_) e ->
-              fprintf fmt "%s%s = %a"  (if first then "" else "; ")
-                (Hstring.view field) print e;
-              false
-            ) true lbs xs);
-          fprintf fmt "}";
-        | _ -> assert false
-      end
-
     (* TODO: introduce PrefixOp in the future to simplify this ? *)
     | Sy.Op op, [e1; e2] when op == Sy.Pow || op == Sy.Integer_round ||
                               op == Sy.Max_real || op == Sy.Max_int ||
diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 5cda559e08..9842033c2a 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -71,8 +71,7 @@ module Types = struct
   let check_number_args loc lty ty =
     match ty with
     | Ty.Text (lty', s)
-    | Ty.Trecord { Ty.args = lty'; name = s; _ }
-    | Ty.Tadt (s,lty') ->
+    | Ty.Tadt (s,lty', _) ->
       if List.length lty <> List.length lty' then
         Errors.typing_error (WrongNumberofArgs (Hstring.view s)) loc;
       lty'
@@ -151,10 +150,10 @@ module Types = struct
       let ty = Ty.t_adt ~body:(Some body) id [] 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
-      let sort_fields = String.equal record_constr "{" in
-      let ty = Ty.trecord ~sort_fields ~record_constr ty_vars id lbs in
+      let lbs = List.map (fun (x, pp) -> x, ty_of_pp loc env None pp) lbs in
+      let ty =
+        Ty.t_adt ~record:true ~body:(Some [record_constr, lbs]) id ty_vars
+      in
       ty, { to_ty = MString.add id ty env.to_ty;
             builtins = env.builtins;
             from_labels =
@@ -188,7 +187,9 @@ module Types = struct
     in
     check_duplicates SH.empty lbs;
     match ty with
-    | Ty.Trecord { Ty.lbs = l; _ } ->
+    | Ty.Tadt (name, params, true) ->
+      let Adt cases = Ty.type_body name params in
+      let l = match cases with [{ destrs; _ }] -> destrs | _ -> assert false in
       if List.length lbs <> List.length l then
         Errors.typing_error WrongNumberOfLabels loc;
       List.iter
@@ -226,10 +227,7 @@ module Env = struct
   type profile = { args : Ty.t list; result : Ty.t }
 
   type logic_kind =
-    | RecordConstr
-    | RecordDestr
     | AdtConstr
-    | EnumConstr
     | AdtDestr
     | Other
 
@@ -259,7 +257,7 @@ module Env = struct
   let add_fpa_enum map =
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
-    | Ty.Tadt (name, params) ->
+    | 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
@@ -284,7 +282,7 @@ module Env = struct
 
   let find_builtin_cstr ty n =
     match ty with
-    | Ty.Tadt (name, params) ->
+    | 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 @@ Hstring.view c) cstrs
@@ -486,19 +484,13 @@ module Env = struct
     in
     decl, { env with logics }
 
-  let add_constr ~record env constr args_ty ty loc =
+  let add_constr env constr args_ty ty loc =
     let pp_profile = PFunction (args_ty, ty) in
-    let kind = if record then RecordConstr else AdtConstr in
-    add_logics ~kind env Symbols.constr [constr, ""] pp_profile loc
+    add_logics ~kind:AdtConstr env Symbols.constr [constr, ""] pp_profile loc
 
-  let add_destr ~record env destr pur_ty lbl_ty loc =
+  let add_destr env destr pur_ty lbl_ty loc =
     let pp_profile = PFunction ([pur_ty], lbl_ty) in
-    let mk_sy s =
-      if record then (Symbols.Op (Access (Hstring.make s)))
-      else Symbols.destruct s
-    in
-    let kind = if record then RecordDestr else AdtDestr in
-    add_logics ~kind env mk_sy [destr, ""] pp_profile loc
+    add_logics ~kind:AdtDestr env Symbols.destruct [destr, ""] pp_profile loc
 
   let find { var_map = m; _ } n = MString.find n m
 
@@ -554,7 +546,7 @@ let type_var_desc env p loc =
   match Env.fresh_type env p loc with
   | s,
     { Env.args = []; result = ty},
-    (Env.Other | Env.AdtConstr | Env.EnumConstr) ->
+    (Env.Other | Env.AdtConstr) ->
     TTapp (s, []) , ty
   | _ -> Errors.typing_error (ShouldBeApply p) loc
 
@@ -609,23 +601,12 @@ let check_pattern_matching missing dead loc =
 let mk_adequate_app p s te_args ty logic_kind =
   let hp = Hstring.make p in
   match logic_kind, te_args, ty with
-  | (Env.AdtConstr | Env.EnumConstr | Env.Other), _, _ ->
+  | (Env.AdtConstr | Env.Other), _, _ ->
     (* symbol 's' alreadt contains the information *)
     TTapp(s, te_args)
 
-  | Env.RecordConstr, _, Ty.Trecord { Ty.lbs; _ } ->
-    let lbs =
-      try List.map2 (fun (hs, _) e -> hs, e) lbs te_args
-      with Invalid_argument _ -> assert false
-    in
-    TTrecord lbs
-
-  | Env.RecordDestr, [te], _ -> TTdot(te, hp)
-
   | Env.AdtDestr, [te], _ -> TTproject (te, hp)
 
-  | Env.RecordDestr, _, _ -> assert false
-  | Env.RecordConstr, _, _ -> assert false
   | Env.AdtDestr, _, _ -> assert false
 
 let fresh_type_app env p loc =
@@ -837,22 +818,6 @@ let rec type_term ?(call_from_type_form=false) env f =
         Options.tool_req 1 (append_type "TR-Typing-Ite type" ty2);
         TTite (cond, te2, te3) , ty2
       end
-    | PPdot(t, a) ->
-      begin
-        let te = type_term env t in
-        let ty = Ty.shorten te.c.tt_ty in
-        match ty with
-        | Ty.Trecord { Ty.name = g; lbs; _ } ->
-          begin
-            try
-              let a = Hstring.make a in
-              TTdot(te, a), Hstring.list_assoc a lbs
-            with Not_found ->
-              let g = Hstring.view g in
-              Errors.typing_error (ShouldHaveLabel(g,a)) t.pp_loc
-          end
-        | _ -> Errors.typing_error (ShouldHaveTypeRecord ty) t.pp_loc
-      end
     | PPrecord lbs ->
       begin
         let lbs =
@@ -862,7 +827,11 @@ let rec type_term ?(call_from_type_form=false) env f =
         let ty = Types.from_labels env.Env.types lbs loc in
         let ty, _ = Ty.fresh (Ty.shorten ty) Ty.esubst in
         match ty with
-        | Ty.Trecord { Ty.lbs=ty_lbs; _ } ->
+        | Ty.Tadt (name, params, true) ->
+          let Adt cases = Ty.type_body name params in
+          let ty_lbs =
+            match cases with [{ destrs; _ }] -> destrs | _ -> assert false
+          in
           begin
             try
               let lbs =
@@ -871,7 +840,7 @@ let rec type_term ?(call_from_type_form=false) env f =
                      Ty.unify te.c.tt_ty ty_lb;
                      lb, te) lbs ty_lbs
               in
-              TTrecord(lbs), ty
+              TTrecord (ty, lbs), ty
             with Ty.TypeClash(t1,t2) ->
               Errors.typing_error (Unification(t1,t2)) loc
           end
@@ -885,7 +854,11 @@ let rec type_term ?(call_from_type_form=false) env f =
             (fun (lb, t) -> Hstring.make lb, (type_term env t, t.pp_loc)) lbs in
         let ty = Ty.shorten te.c.tt_ty in
         match ty with
-        | Ty.Trecord { Ty.lbs = ty_lbs; _ } ->
+        | Ty.Tadt (name, params, true) ->
+          let Adt cases = Ty.type_body name params in
+          let ty_lbs =
+            match cases with [{ destrs; _ }] -> destrs | _ -> assert false
+          in
           let nlbs =
             List.map
               (fun (lb, ty_lb) ->
@@ -895,7 +868,7 @@ let rec type_term ?(call_from_type_form=false) env f =
                    lb, v
                  with
                  | Not_found ->
-                   lb, {c = { tt_desc = TTdot(te, lb); tt_ty = ty_lb};
+                   lb, {c = { tt_desc = TTproject(te, lb); tt_ty = ty_lb};
                         annot = te.annot }
                  | Ty.TypeClash(t1,t2) ->
                    Errors.typing_error (Unification(t1,t2)) loc
@@ -906,7 +879,7 @@ let rec type_term ?(call_from_type_form=false) env f =
                try ignore (Hstring.list_assoc lb ty_lbs)
                with Not_found ->
                  Errors.typing_error (NoLabelInType(lb, ty)) loc) lbs;
-          TTrecord(nlbs), ty
+          TTrecord (ty, nlbs), ty
         | _ ->  Errors.typing_error ShouldBeARecord loc
       end
     | PPlet(l, t2) ->
@@ -952,6 +925,27 @@ let rec type_term ?(call_from_type_form=false) env f =
         | Ty.TypeClash(t1,t2) -> Errors.typing_error (Unification(t1,t2)) loc
       end
 
+    | PPdot(t, a) ->
+      begin
+        let te = type_term env t in
+        let ty = Ty.shorten te.c.tt_ty in
+        match ty with
+        | Ty.Tadt (name, params, true) ->
+          let Adt cases = Ty.type_body name params in
+          let lbs =
+            match cases with [{ destrs; _ }] -> destrs | _ -> assert false
+          in
+          begin
+            try
+              let a = Hstring.make a in
+              TTproject (te, a), Hstring.list_assoc a lbs
+            with Not_found ->
+              let g = Hstring.view name in
+              Errors.typing_error (ShouldHaveLabel(g,a)) t.pp_loc
+          end
+        | _ -> Errors.typing_error (ShouldHaveTypeRecord ty) t.pp_loc
+      end
+
     | PPproject (t, lbl) ->
       let te = type_term env t in
       begin
@@ -961,9 +955,6 @@ let rec type_term ?(call_from_type_form=false) env f =
             Ty.unify te.c.tt_ty arg;
             TTproject (te, Hstring.make lbl), Ty.shorten result
 
-          | _, {Env.args = [arg] ; result}, Env.RecordDestr ->
-            Ty.unify te.c.tt_ty arg;
-            TTdot (te, Hstring.make lbl), Ty.shorten result
           | _ -> assert false
         with Ty.TypeClash(t1,t2) ->
           Errors.typing_error (Unification(t1,t2)) loc
@@ -974,12 +965,9 @@ let rec type_term ?(call_from_type_form=false) env f =
       let e = type_term env e in
       let ty = Ty.shorten e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params) ->
-          begin match Ty.type_body name params with
-            | Ty.Adt cases -> cases
-          end
-        | Ty.Trecord { Ty.record_constr; lbs; _ } ->
-          [{Ty.constr = record_constr; destrs = lbs}]
+        | Ty.Tadt (name, params, _) ->
+          let Adt cases = Ty.type_body name params in
+          cases
         | _ -> Errors.typing_error (ShouldBeADT ty) loc
       in
       let pats =
@@ -1244,20 +1232,8 @@ and type_form ?(in_theory=false) env f =
             let top = TTisConstr (tt, Hstring.make lbl) in
             let r = TFatom { c = top; annot = new_id () } in
             r
-          | Env.EnumConstr ->
-            let tt_desc, tt_ty = type_var_desc env lbl f.pp_loc in
-            let rhs = { c = { tt_desc; tt_ty }; annot = new_id () } in
-            TFatom (mk_ta_eq tt rhs)
           | _ ->
-            begin match result with
-              | Ty.Trecord _ ->
-                (* The typechecker allows only testers whose the
-                   two arguments have the same type. Thus, we can always
-                   replace the tester of a record by the true literal. *)
-                TFatom { c = TAtrue; annot = new_id () }
-              | _ ->
-                Errors.typing_error (NotAdtConstr (lbl, result)) f.pp_loc
-            end
+            Errors.typing_error (NotAdtConstr (lbl, result)) f.pp_loc
         with Ty.TypeClash(t1,t2) ->
           Errors.typing_error (Unification(t1,t2)) f.pp_loc
       end
@@ -1383,12 +1359,10 @@ and type_form ?(in_theory=false) env f =
       let e = type_term env e in
       let ty = e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params) ->
+        | Ty.Tadt (name, params, _) ->
           begin match Ty.type_body name params with
             | Ty.Adt cases -> cases
           end
-        | Ty.Trecord { Ty.record_constr; lbs; _ } ->
-          [{Ty.constr = record_constr ; destrs = lbs}]
 
         | _ ->
           Errors.typing_error (ShouldBeADT ty) f.pp_loc
@@ -2074,10 +2048,8 @@ let rec mono_term {c = {tt_ty=tt_ty; tt_desc=tt_desc}; annot = id} =
       TTextract(mono_term t1, i, j)
     | TTconcat (t1,t2)->
       TTconcat (mono_term t1, mono_term t2)
-    | TTdot (t1, a) ->
-      TTdot (mono_term t1, a)
-    | TTrecord lbs ->
-      TTrecord (List.map (fun (x, t) -> x, mono_term t) lbs)
+    | TTrecord (ty, lbs) ->
+      TTrecord (ty, List.map (fun (x, t) -> x, mono_term t) lbs)
     | TTlet (l,t2)->
       let l = List.rev_map (fun (x, t1) -> x, mono_term t1) (List.rev l) in
       TTlet (l, mono_term t2)
@@ -2329,7 +2301,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) =
     let ty = PFunction([], pur_ty) in
     let tlogic, env =
       (* can also use List.fold Env.add_constr *)
-      Env.add_logics ~kind:Env.EnumConstr env Symbols.constr lcl ty loc
+      Env.add_logics ~kind:Env.AdtConstr env Symbols.constr lcl ty loc
     in
     let td2_a = { c = TLogic(loc, lc, tlogic); annot=new_id () } in
     (td2_a,env)::acc, env
@@ -2345,14 +2317,14 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) =
       else
         let args_ty = List.map snd lrec in
         let tlogic, env =
-          Env.add_constr ~record:true env constr args_ty pur_ty loc
+          Env.add_constr env constr args_ty pur_ty loc
         in
         ({c = TLogic(loc, [constr], tlogic); annot=new_id ()}, env)::acc, env
     in
     List.fold_left (* register fields *)
       (fun (acc, env) (lbl, ty_lbl) ->
          let tlogic, env =
-           Env.add_destr ~record:true env lbl pur_ty ty_lbl loc
+           Env.add_destr env lbl pur_ty ty_lbl loc
          in
          ({c = TLogic(loc, [lbl], tlogic); annot=new_id ()}, env) :: acc, env
       )(acc, env) lrec
@@ -2362,7 +2334,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) =
       (fun (acc, env) (cstr, lbl_args_ty) ->
          let args_ty = List.map snd lbl_args_ty in
          let tty, env =
-           Env.add_constr ~record:false env cstr args_ty pur_ty loc
+           Env.add_constr env cstr args_ty pur_ty loc
          in
          let acc =
            ({c = TLogic(loc, [cstr], tty); annot=new_id ()}, env) :: acc
@@ -2370,7 +2342,7 @@ let type_user_defined_type_body ~is_recursive env acc (loc, ls, s, body) =
          List.fold_left (* register destructors *)
            (fun (acc, env) (lbl, ty_lbl) ->
               let tty, env =
-                Env.add_destr ~record:false env lbl pur_ty ty_lbl loc
+                Env.add_destr env lbl pur_ty ty_lbl loc
               in
               ({c = TLogic(loc, [lbl], tty); annot=new_id ()}, env) :: acc, env
            )(acc, env) lbl_args_ty
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index a5b9eac68e..d951f330e1 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -58,7 +58,7 @@ let constr_of_destr ty dest =
       ~module_name:"Adt" ~function_name:"constr_of_destr"
       "ty = %a" Ty.print ty;
   match ty with
-  | Ty.Tadt (s, params) ->
+  | Ty.Tadt (s, params, _) ->
     begin
       let Ty.Adt cases = Ty.type_body s params in
       try
@@ -87,7 +87,8 @@ module Shostak (X : ALIEN) = struct
   let is_mine_symb sy ty =
     not (Options.get_disable_adts ()) &&
     match sy, ty with
-    | Sy.Op (Sy.Constr _), Ty.Tadt _ -> true
+    | Sy.Op (Sy.Constr _), Ty.Tadt _
+    | Sy.Op Sy.Destruct _, Ty.Tadt (_, _, true) -> true
     | Sy.Op Sy.Destruct _, Ty.Tadt _ ->
       (* A destructor is partially interpreted by the ADT theory.
          If we assume the tester of the constructor associated with
@@ -177,7 +178,7 @@ module Shostak (X : ALIEN) = struct
     in
     let xs = List.rev sx in
     match f, xs, ty with
-    | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) ->
+    | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params, _) ->
       let Ty.Adt cases = Ty.type_body name params in
       let case_hs =
         try Ty.assoc_destrs hs cases with Not_found -> assert false
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index e5b6741023..34b6659111 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -74,7 +74,7 @@ module Domain = struct
 
   let unknown ty =
     match ty with
-    | Ty.Tadt (name, params) ->
+    | Ty.Tadt (name, params, _) ->
       (* Return the list of all the constructors of the type of [r]. *)
       let Adt body = Ty.type_body name params in
       let constrs =
@@ -347,7 +347,7 @@ let assume_subst ~ex r1 r2 env =
 
 let is_tightenable ty c =
   match ty with
-  | Ty.Tadt (name, params) ->
+  | Ty.Tadt (name, params, _) ->
     let Adt cases = Ty.type_body name params in
     let b = Lists.is_empty @@ Ty.assoc_destrs c cases in
     b
@@ -488,7 +488,7 @@ let build_constr_eq r c =
   match Th.embed r with
   | Alien r ->
     begin match X.type_info r with
-      | Ty.Tadt (name, params) as ty ->
+      | Ty.Tadt (name, params, _) as ty ->
         let Ty.Adt body = Ty.type_body name params in
         let ds =
           try Ty.assoc_destrs c body with Not_found -> assert false
@@ -584,7 +584,7 @@ let two = Numbers.Q.from_int 2
 (* TODO: we should compute this reverse map in `Ty` and store it there. *)
 let constr_of_destr ty d =
   match ty with
-  | Ty.Tadt (name, params) ->
+  | Ty.Tadt (name, params, _) ->
     begin
       let Ty.Adt cases = Ty.type_body name params in
       try
diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml
index 798a56ce65..cfbf791ca1 100644
--- a/src/lib/reasoners/matching.ml
+++ b/src/lib/reasoners/matching.ml
@@ -314,11 +314,11 @@ module Make (X : Arg) : S with type theory = X.t = struct
     | _ , [] -> l1
     | _ -> List.fold_left (fun acc e -> e :: acc) l2 (List.rev l1)
 
-  let xs_modulo_records t { Ty.lbs; _  } =
-    List.rev
+  (* let xs_modulo_records t { Ty.lbs; _  } =
+     List.rev
       (List.rev_map
          (fun (hs, ty) ->
-            E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs)
+            E.mk_term (Symbols.Op (Symbols.Access hs)) [t] ty) lbs) *)
 
   module SLE = (* sets of lists of terms *)
     Set.Make(struct
@@ -413,13 +413,13 @@ module Make (X : Arg) : S with type theory = X.t = struct
               (fun t l ->
                  let { E.f = f; xs = xs; ty = ty; _ } = E.term_view t in
                  if Symbols.compare f_pat f = 0 then xs::l
-                 else
-                   begin
-                     match f_pat, ty with
-                     | Symbols.Op (Symbols.Record), Ty.Trecord record ->
-                       (xs_modulo_records t record) :: l
-                     | _ -> l
-                   end
+                 else l
+                 (* begin
+                    match f_pat, ty with
+                    | Symbols.Op (Symbols.Record), Ty.Trecord record ->
+                     (xs_modulo_records t record) :: l
+                    | _ -> l
+                    end *)
               ) cl []
           in
           let cl = filter_classes mconf cl tbox in
diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml
index 8fcf11b0b0..4d518026cf 100644
--- a/src/lib/reasoners/relation.ml
+++ b/src/lib/reasoners/relation.ml
@@ -34,15 +34,13 @@ module X = Shostak.Combine
 
 module Rel1 : Sig_rel.RELATION = IntervalCalculus
 
-module Rel2 : Sig_rel.RELATION = Records_rel
+module Rel2 : Sig_rel.RELATION = Bitv_rel
 
-module Rel3 : Sig_rel.RELATION = Bitv_rel
+module Rel3 : Sig_rel.RELATION = Arrays_rel
 
-module Rel4 : Sig_rel.RELATION = Arrays_rel
+module Rel4 : Sig_rel.RELATION = Adt_rel
 
-module Rel5 : Sig_rel.RELATION = Adt_rel
-
-module Rel6 : Sig_rel.RELATION = Ite_rel
+module Rel5 : Sig_rel.RELATION = Ite_rel
 
 (* This value is unused. *)
 let timer = Timers.M_None
@@ -53,7 +51,6 @@ type t = {
   r3: Rel3.t;
   r4: Rel4.t;
   r5: Rel5.t;
-  r6: Rel6.t;
 }
 
 let empty classes = {
@@ -62,7 +59,6 @@ let empty classes = {
   r3=Rel3.empty classes;
   r4=Rel4.empty classes;
   r5=Rel5.empty classes;
-  r6=Rel6.empty classes;
 }
 
 let (|@|) l1 l2 =
@@ -92,13 +88,9 @@ let assume env uf sa =
     Timers.with_timer Rel5.timer Timers.F_assume @@ fun () ->
     Rel5.assume env.r5 uf sa
   in
-  let env6, ({ assume = a6; remove = rm6}:_ Sig_rel.result) =
-    Timers.with_timer Rel6.timer Timers.F_assume @@ fun () ->
-    Rel6.assume env.r6 uf sa
-  in
-  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6},
-  ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6;
-     remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6}
+  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5},
+  ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5;
+     remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5}
    : _ Sig_rel.result)
 
 let assume_th_elt env th_elt dep =
@@ -108,8 +100,7 @@ let assume_th_elt env th_elt dep =
   let env3 = Rel3.assume_th_elt env.r3 th_elt dep in
   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
-  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6}
+  {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5}
 
 let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a
     k =
@@ -124,8 +115,7 @@ let query env uf a =
   try_query (module Rel2) env.r2 uf a @@ fun () ->
   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 () -> None
+  try_query (module Rel5) env.r5 uf a @@ fun () -> None
 
 let case_split env uf ~for_model =
   Options.exec_thread_yield ();
@@ -134,8 +124,7 @@ let case_split env uf ~for_model =
   let seq3 = Rel3.case_split env.r3 uf ~for_model in
   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 splits = [seq1; seq2; seq3; seq4; seq5; seq6] in
+  let splits = [seq1; seq2; seq3; seq4; seq5] in
   let splits = List.fold_left (|@|) [] splits in
   List.fast_sort
     (fun (_ ,_ , sz1) (_ ,_ , sz2) ->
@@ -160,8 +149,7 @@ let optimizing_objective env uf o =
     Rel1.optimizing_objective env.r1 uf;
     Rel2.optimizing_objective env.r2 uf;
     Rel3.optimizing_objective env.r3 uf;
-    Rel4.optimizing_objective env.r4 uf;
-    Rel5.optimizing_objective env.r5 uf
+    Rel4.optimizing_objective env.r4 uf
   ]
 
 let add env uf r t =
@@ -171,8 +159,7 @@ let add env uf r t =
   let r3, eqs3 =Rel3.add env.r3 uf r t in
   let r4, eqs4 =Rel4.add env.r4 uf r t in
   let r5, eqs5 =Rel5.add env.r5 uf r t in
-  let r6, eqs6 =Rel6.add env.r6 uf r t in
-  {r1;r2;r3;r4;r5;r6},eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5|@|eqs6
+  {r1;r2;r3;r4;r5},eqs1|@|eqs2|@|eqs3|@|eqs4|@|eqs5
 
 
 let instantiate ~do_syntactic_matching t_match env uf selector =
@@ -187,10 +174,8 @@ let instantiate ~do_syntactic_matching t_match env uf selector =
     Rel4.instantiate ~do_syntactic_matching t_match env.r4 uf selector in
   let r5, l5 =
     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
-  {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6},
-  l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1
+  {r1=r1; r2=r2; r3=r3; r4=r4; r5=r5},
+  l5 |@| l4 |@| l3 |@| l2 |@| l1
 
 let new_terms env =
   Rel1.new_terms env.r1
@@ -198,4 +183,3 @@ let new_terms env =
   |> 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 9bdee60341..e7b82f01f2 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -40,14 +40,11 @@ module rec CX : sig
   val extract1 : r -> ARITH.t option
   val embed1 : ARITH.t -> r
 
-  val extract2 : r -> RECORDS.t option
-  val embed2 : RECORDS.t -> r
+  val extract2 : r -> BITV.t option
+  val embed2 : BITV.t -> r
 
-  val extract3 : r -> BITV.t option
-  val embed3 : BITV.t -> r
-
-  val extract4 : r -> ADT.t option
-  val embed4 : ADT.t -> r
+  val extract3 : r -> ADT.t option
+  val embed3 : ADT.t -> r
 
 end =
 struct
@@ -56,7 +53,6 @@ struct
     | Term of Expr.t
     | Ac of AC.t
     | Arith of ARITH.t
-    | Records of RECORDS.t
     | Bitv of BITV.t
     | Adt of ADT.t
 
@@ -71,7 +67,6 @@ struct
       if Options.get_term_like_pp () then begin
         match r.v with
         | Arith t -> fprintf fmt "%a" ARITH.print t
-        | Records t -> fprintf fmt "%a" RECORDS.print t
         | Bitv t -> fprintf fmt "%a" BITV.print t
         | Adt t -> fprintf fmt "%a" ADT.print t
         | Term t -> fprintf fmt "%a" Expr.print t
@@ -81,8 +76,6 @@ struct
         match r.v with
         | Arith t ->
           fprintf fmt "Arith(%s):[%a]" ARITH.name ARITH.print t
-        | Records t ->
-          fprintf fmt "Records(%s):[%a]" RECORDS.name RECORDS.print t
         | Bitv t ->
           fprintf fmt "Bitv(%s):[%a]" BITV.name BITV.print t
         | Adt t ->
@@ -164,7 +157,6 @@ struct
     let hash r =
       let res = match r.v with
         | Arith x -> 1 + 10 * ARITH.hash x
-        | Records x -> 2 + 10 * RECORDS.hash x
         | Bitv x -> 3 + 10 * BITV.hash x
         | Adt x -> 6 + 10 * ADT.hash x
         | Ac ac -> 9 + 10 * AC.hash ac
@@ -175,7 +167,6 @@ struct
     let eq  r1 r2 =
       match r1.v, r2.v with
       | Arith x, Arith y -> ARITH.equal x y
-      | Records x, Records y -> RECORDS.equal x y
       | Bitv x, Bitv y -> BITV.equal x y
       | Adt x, Adt y -> ADT.equal x y
       | Term x, Term y -> Expr.equal x y
@@ -201,9 +192,8 @@ struct
   (* end: Hconsing modules and functions *)
 
   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 = Adt x; id = -1000 (* dummy *)}
+  let embed2 x = hcons {v = Bitv x; id = -1000 (* dummy *)}
+  let embed3 x = hcons {v = Adt x; id = -1000 (* dummy *)}
 
   let ac_embed ({ Sig.l; _ } as t) =
     match l with
@@ -218,9 +208,8 @@ struct
   let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)}
 
   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=Adt r; _ } -> Some r | _ -> None
+  let extract2 = function { v=Bitv r; _ } -> Some r | _ -> None
+  let extract3 = function { v=Adt r; _ } -> Some r | _ -> None
 
   let ac_extract = function
     | { v = Ac t; _ }   -> Some t
@@ -229,7 +218,6 @@ struct
   let term_extract r =
     match r.v with
     | Arith _ -> ARITH.term_extract r
-    | Records _ -> RECORDS.term_extract r
     | Bitv _ -> BITV.term_extract r
     | Adt _ -> ADT.term_extract r
     | Ac _ -> None, false (* SYLVAIN : TODO *)
@@ -239,7 +227,6 @@ struct
     let res =
       match r.v with
       | Arith _ -> ARITH.to_model_term r
-      | Records _ -> RECORDS.to_model_term r
       | Bitv _ -> BITV.to_model_term r
       | Adt _ -> ADT.to_model_term r
       | Term t when Expr.is_model_term t -> Some t
@@ -254,7 +241,6 @@ struct
 
   let type_info = function
     | { v = Arith t; _ } -> ARITH.type_info t
-    | { v = Records t; _ } -> RECORDS.type_info t
     | { v = Bitv t; _ } -> BITV.type_info t
     | { v = Adt t; _ } -> ADT.type_info t
     | { v = Ac x; _ } -> AC.type_info x
@@ -266,9 +252,8 @@ struct
     | Ac _ -> -1
     | Term  _ -> -2
     | Arith _ -> -3
-    | Records _ -> -4
-    | Bitv _ -> -5
-    | Adt _ -> -7
+    | Bitv _ -> -4
+    | Adt _ -> -5
 
   let compare_tag a b = theory_num a - theory_num b
 
@@ -277,7 +262,6 @@ struct
     else
       match a.v, b.v with
       | Arith _, Arith _ -> ARITH.compare a b
-      | Records _, Records _ -> RECORDS.compare a b
       | Bitv _, Bitv _ -> BITV.compare a b
       | Adt _, Adt _ -> ADT.compare a b
       | Term x, Term y -> Expr.compare x y
@@ -292,7 +276,6 @@ struct
        | Term  t -> Expr.hash t
        | Ac x -> AC.hash x
        | Arith x -> ARITH.hash x
-       | Records x -> RECORDS.hash x
        | Bitv x -> BITV.hash x
        | Arrays x -> ARRAYS.hash x
        | Adt x -> ADT.hash x
@@ -321,7 +304,6 @@ struct
   let leaves r =
     match r.v with
     | Arith t -> ARITH.leaves t
-    | Records t -> RECORDS.leaves t
     | Bitv t -> BITV.leaves t
     | Adt t -> ADT.leaves t
     | Ac t -> r :: (AC.leaves t)
@@ -330,7 +312,6 @@ struct
   let is_constant r =
     match r.v with
     | Arith t -> ARITH.is_constant t
-    | Records t -> RECORDS.is_constant t
     | Bitv t -> BITV.is_constant t
     | Adt t -> ADT.is_constant t
     | Term t ->
@@ -347,7 +328,6 @@ struct
     if equal p v then r
     else match r.v with
       | Arith t -> ARITH.subst p v t
-      | Records t -> RECORDS.subst p v t
       | Bitv t -> BITV.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
@@ -358,32 +338,27 @@ struct
     let not_restricted = not @@ Options.get_restricted () in
     match
       ARITH.is_mine_symb sb ty,
-      not_restricted && RECORDS.is_mine_symb sb ty,
       not_restricted && BITV.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 ->
+    | true, false, false, false ->
       Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () ->
       ARITH.make t
 
-    | false, true, false, false, false ->
-      Timers.with_timer Timers.M_Records Timers.F_make @@ fun () ->
-      RECORDS.make t
-
-    | false, false, true, 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, false, true, false ->
       Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () ->
       ADT.make t
 
-    | false, false, false, false, true  ->
+    | 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 ->
       term_embed t, []
 
     | _ -> assert false
@@ -392,30 +367,26 @@ struct
     let not_restricted = not @@ Options.get_restricted () in
     match
       ARITH.is_mine_symb sb ty,
-      not_restricted && RECORDS.is_mine_symb sb ty,
       not_restricted && BITV.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 ->
+    | true, false, false, false ->
       ARITH.fully_interpreted sb
-    | false, true, false, false, false ->
-      RECORDS.fully_interpreted sb
-    | false, false, true, false, false ->
+    | false, true, false, false ->
       BITV.fully_interpreted sb
-    | false, false, false, true, false ->
+    | false, false, true, false ->
       ADT.fully_interpreted sb
-    | false, false, false, false, true  ->
+    | false, false, false, true  ->
       AC.fully_interpreted sb
-    | false, false, false, false, false ->
+    | false, false, false, false ->
       false
     | _ -> assert false
 
   let is_solvable_theory_symbol sb ty =
     ARITH.is_mine_symb sb ty ||
     not (Options.get_restricted ()) &&
-    (RECORDS.is_mine_symb sb ty ||
-     BITV.is_mine_symb sb ty ||
+    (BITV.is_mine_symb sb ty ||
      ADT.is_mine_symb sb ty)
 
   let is_a_leaf r = match r.v with
@@ -430,18 +401,15 @@ struct
       let ty = ac.Sig.t in
       match
         ARITH.is_mine_symb ac.Sig.h ty,
-        RECORDS.is_mine_symb ac.Sig.h ty,
         BITV.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 ->
+      | true, false, false, false ->
         ARITH.color ac
-      | false, true, false, false, false ->
-        RECORDS.color ac
-      | false, false, true, false, false ->
+      | false, true, false, false ->
         BITV.color ac
-      | false, false, false, true, false ->
+      | false, false, true, false ->
         ADT.color ac
       | _  -> ac_embed ac
 
@@ -449,7 +417,6 @@ struct
     Debug.debug_abstract_selectors a;
     match a.v with
     | Arith a -> ARITH.abstract_selectors a acc
-    | Records a -> RECORDS.abstract_selectors a acc
     | Bitv a -> BITV.abstract_selectors a acc
     | Adt a -> ADT.abstract_selectors a acc
     | Term _ -> a, acc
@@ -531,10 +498,6 @@ struct
             Timers.with_timer ARITH.timer Timers.F_solve @@ fun () ->
             ARITH.solve ra rb pb
 
-          | Ty.Trecord _       ->
-            Timers.with_timer RECORDS.timer Timers.F_solve @@ fun () ->
-            RECORDS.solve ra rb pb
-
           | Ty.Tbitv _         ->
             Timers.with_timer BITV.timer Timers.F_solve @@ fun () ->
             BITV.solve ra rb pb
@@ -581,7 +544,6 @@ struct
     let opt = match r.v, type_info r with
       | _, Ty.Tint
       | _, Ty.Treal     -> ARITH.assign_value r distincts eq
-      | _, Ty.Trecord _ -> RECORDS.assign_value r distincts eq
       | _, Ty.Tbitv _   -> BITV.assign_value r distincts eq
       | Term t, Ty.Tfarray _ ->
         begin
@@ -646,24 +608,14 @@ and ARITH : Sig.SHOSTAK
       let embed =  CX.embed1
     end)
 
-and RECORDS : Sig.SHOSTAK
-  with type r = CX.r
-   and type t = CX.r Records.abstract =
-  Records.Shostak
-    (struct
-      include CX
-      let extract = extract2
-      let embed = embed2
-    end)
-
 and BITV : Sig.SHOSTAK
   with type r = CX.r
    and type t = CX.r Bitv.abstract =
   Bitv.Shostak
     (struct
       include CX
-      let extract = extract3
-      let embed = embed3
+      let extract = extract2
+      let embed = embed2
     end)
 
 and ADT : Sig.SHOSTAK
@@ -672,8 +624,8 @@ and ADT : Sig.SHOSTAK
   Adt.Shostak
     (struct
       include CX
-      let extract = extract4
-      let embed = embed4
+      let extract = extract3
+      let embed = embed3
     end)
 
 (* Its signature is not Sig.SHOSTAK because it does not provide a solver *)
@@ -712,7 +664,6 @@ module Combine = struct
 end
 
 module Arith = ARITH
-module Records = RECORDS
 module Bitv = BITV
 module Adt = ADT
 module Polynome = TARITH
diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli
index e3a2acac14..7b8ae33b92 100644
--- a/src/lib/reasoners/shostak.mli
+++ b/src/lib/reasoners/shostak.mli
@@ -41,9 +41,6 @@ module Polynome : Polynome.T
 module Arith : Sig.SHOSTAK
   with type r = Combine.r and type t = Polynome.t
 
-module Records : Sig.SHOSTAK
-  with type r = Combine.r and type t = Combine.r Records.abstract
-
 module Bitv : Sig.SHOSTAK
   with type r = Combine.r and type t = Combine.r Bitv.abstract
 
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 5bb4936f55..bd51d48734 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -162,18 +162,13 @@ module Main_Default : S = struct
            | Tint | Treal | Tbool | Tunit | Tbitv _ | Tfarray _ -> mp
            | Tvar _ -> assert false
 
-           | Text (_, hs) | Trecord { name = hs; _ } when
-               Hstring.Map.mem hs mp -> mp
+           | Text (_, hs) when Hstring.Map.mem hs mp -> mp
 
            | Text (l, hs) ->
              let l = List.map (fun _ -> Ty.fresh_tvar()) l in
              Hstring.Map.add hs (Text(l, hs)) mp
 
-           | Trecord { name; _ } ->
-             (* cannot do better for records ? *)
-             Hstring.Map.add name ty mp
-
-           | Tadt (hs, _) ->
+           | Tadt (hs, _, _) ->
              (* cannot do better for ADT ? *)
              Hstring.Map.add hs ty mp
         )sty Hstring.Map.empty
@@ -187,20 +182,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
-           | Trecord { Ty.lbs; _ } ->
-             print_dbg ~flushed:false ~header:false "type %a = " Ty.print ty;
-             begin match lbs with
-               | [] -> assert false
-               | (lbl, ty)::l ->
-                 let print fmt (lbl,ty) =
-                   Format.fprintf fmt " ; %s :%a"
-                     (Hstring.view lbl) Ty.print ty in
-                 print_dbg ~flushed:false ~header:false
-                   "{ %s : %a%a"
-                   (Hstring.view lbl) Ty.print ty
-                   (pp_list_no_space print) l;
-                 print_dbg ~flushed:false ~header:false " }@ "
-             end
            | Tadt _ ->
              print_dbg ~flushed:false ~header:false "%a@ " Ty.print_full ty
         )types;
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 2b29fcd649..4245116ce4 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -409,20 +409,6 @@ module SmtPrinter = struct
         pp x.let_e
         pp_boxed x.in_e
 
-    | Sy.(Op Record), _ ->
-      begin
-        match ty with
-        | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } ->
-          assert (List.compare_lengths xs lbs = 0);
-          Fmt.pf ppf "@[<2>(%a %a@])"
-            Hstring.print record_constr
-            Fmt.(list ~sep:sp pp |> box) xs
-
-        | _ ->
-          (* Excluded by the typechecker. *)
-          assert false
-      end
-
     | Sy.Op op, [] -> Symbols.pp_smtlib_operator ppf op
 
     | Sy.Op Minus, [e1; { f = Sy.Real q; _ }] when is_zero e1.f ->
@@ -581,7 +567,7 @@ module AEPrinter = struct
       assert false
 
   and pp_silent ppf t =
-    let { f ; xs ; ty; bind; _ } = t in
+    let { f ; xs ; bind; _ } = t in
     match f, xs with
     | Sy.Form form, xs -> pp_formula ppf form xs bind
 
@@ -608,25 +594,6 @@ module AEPrinter = struct
     | Sy.(Op Extract (i, j)), [e] ->
       Fmt.pf ppf "%a^{%d, %d}" pp e i j
 
-    | Sy.(Op (Access field)), [e] ->
-      Fmt.pf ppf "%a.%s" pp e (Hstring.view field)
-
-    | Sy.(Op Record), _ ->
-      begin match ty with
-        | Ty.Trecord { Ty.lbs = lbs; _ } ->
-          assert (List.compare_lengths xs lbs = 0);
-          Fmt.pf ppf "{";
-          ignore (List.fold_left2 (fun first (field,_) e ->
-              Fmt.pf ppf "%s%s = %a"  (if first then "" else "; ")
-                (Hstring.view field) pp e;
-              false
-            ) true lbs xs);
-          Fmt.pf ppf "}";
-        | _ ->
-          (* Excluded by the typechecker. *)
-          assert false
-      end
-
     | Sy.(Op ((Pow | Integer_round | Max_real | Min_real | Max_int
               | Min_int) as op)), [e1; e2] ->
       Fmt.pf ppf "%a(%a, %a)" Symbols.pp_ae_operator op pp e1 pp e2
@@ -1035,7 +1002,7 @@ let mk_ite cond th el =
 
 let rec is_model_term e =
   match e.f, e.xs with
-  | (Op Constr _ | Op Record | Op Set), xs -> List.for_all is_model_term xs
+  | (Op Constr _ | Op Set), xs -> List.for_all is_model_term xs
   | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true
   | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero
   | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero
@@ -1857,11 +1824,9 @@ module Triggers = struct
     | { f = Op (Get | Set) ; xs = [t1 ; t2]; _ } ->
       max (score_term t1) (score_term t2)
 
-    | { f = Op (Access _ | Destruct _ | Extract _) ; xs = [t]; _ } ->
+    | { f = Op (Destruct _ | Extract _) ; xs = [t]; _ } ->
       1 + score_term t
-    | { f = Op Record; xs; _ } ->
-      1 + (List.fold_left
-             (fun acc t -> max (score_term t) acc) 0 xs)
+
     | { f = Op Set; xs = [t1; t2; t3]; _ } ->
       max (score_term t1) (max (score_term t2) (score_term t3))
 
@@ -1944,14 +1909,6 @@ module Triggers = struct
     | { f = Op Concat; _ }, _ -> -1
     | _, { f = Op Concat; _ } -> 1
 
-    | { f = Op (Access a1) ; xs=[t1]; _ },
-      { f = Op (Access a2) ; xs=[t2]; _ } ->
-      let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *)
-      if c<>0 then c else cmp_trig_term t1 t2
-
-    | { f = Op (Access _); _ }, _ -> -1
-    | _, { f = Op (Access _); _ } -> 1
-
     | { f = Op (Destruct a1) ; xs = [t1]; _ },
       { f = Op (Destruct a2) ; xs = [t2]; _ } ->
       let c = Stdlib.compare a1 a2 in (* should be Hstring.compare *)
@@ -1960,11 +1917,6 @@ module Triggers = struct
     | { f = Op (Destruct _); _ }, _ -> -1
     | _, { f =Op (Destruct _); _ } -> 1
 
-    | { f = Op Record ; xs= lbs1; _ }, { f = Op Record ; xs = lbs2; _ } ->
-      Util.cmp_lists lbs1 lbs2 cmp_trig_term
-    | { f = Op Record; _ }, _ -> -1
-    | _, { f = Op Record; _ } -> 1
-
     | { f = (Op _) as s1; xs=tl1; _ }, { f = (Op _) as s2; xs=tl2; _ } ->
       (* ops that are not infix or prefix *)
       let l1 = List.map score_term tl1 in
@@ -2536,7 +2488,6 @@ let mk_match e cases =
   let mk_destr =
     match ty with
     | Ty.Tadt _ -> (fun hs -> Sy.destruct (Hstring.view hs))
-    | Ty.Trecord _ -> (fun hs -> Sy.Op (Sy.Access hs))
     | _ -> assert false
   in
   let mker =
@@ -2544,9 +2495,6 @@ let mk_match e cases =
     | Ty.Tadt _ ->
       (fun e name -> mk_builtin ~is_pos:true (Sy.IsConstr name) [e])
 
-    | Ty.Trecord _ ->
-      (fun _e _name -> assert false) (* no need to test for records *)
-
     | _ -> assert false
   in
   let res = compile_match mk_destr mker e cases e in
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index d868f69406..80dbfdb461 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -37,8 +37,7 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Hstring.t | Record
-  | Constr of Hstring.t (* enums, adts *)
+  | Constr of Hstring.t
   | Destruct of Hstring.t
   (* Arrays *)
   | Get | Set
@@ -181,7 +180,7 @@ let compare_kinds k1 k2 =
 let compare_operators op1 op2 =
   Util.compare_algebraic op1 op2
     (function
-      | Access h1, Access h2 | Constr h1, Constr h2
+      | Constr h1, Constr h2
       | Destruct h1, Destruct h2 ->
         Hstring.compare h1 h2
       | Extract (i1, j1), Extract (i2, j2) ->
@@ -190,7 +189,7 @@ let compare_operators op1 op2 =
       | Int2BV n1, Int2BV n2 -> Int.compare n1 n2
       | _ , (Plus | Minus | Mult | Div | Modulo | Real_is_int
             | Concat | Extract _ | Get | Set | Float
-            | Access _ | Record | Sqrt_real | Abs_int | Abs_real
+            | Sqrt_real | Abs_int | Abs_real
             | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default
             | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int
             | Integer_log2 | Pow | Integer_round
@@ -357,8 +356,6 @@ module AEPrinter = struct
     | Set -> Fmt.pf ppf "set"
 
     (* DT theory *)
-    | Record -> Fmt.pf ppf "@Record"
-    | Access s -> Fmt.pf ppf "@Access_%a" Hstring.print s
     | Constr s
     | Destruct s -> Hstring.print ppf s
 
@@ -454,8 +451,7 @@ module SmtPrinter = struct
     | Set -> Fmt.pf ppf "store"
 
     (* DT theory *)
-    | Record -> ()
-    | Access s | Constr s | Destruct s -> Hstring.print ppf s
+    | Constr s | Destruct s -> Hstring.print ppf s
 
     (* Float theory *)
     | Float -> Fmt.pf ppf "ae.round"
diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli
index 4834545ff9..166a5ad0f1 100644
--- a/src/lib/structures/symbols.mli
+++ b/src/lib/structures/symbols.mli
@@ -37,8 +37,7 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Hstring.t | Record
-  | Constr of Hstring.t (* enums, adts *)
+  | Constr of Hstring.t
   | Destruct of Hstring.t
   (* Arrays *)
   | Get | Set
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index b176cd2ac1..81a1907419 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -37,16 +37,9 @@ type t =
   | Tbitv of int
   | Text of t list * Hstring.t
   | Tfarray of t * t
-  | Tadt of Hstring.t * t list
-  | Trecord of trecord
+  | Tadt of Hstring.t * t list * bool
 
 and tvar = { v : int ; mutable value : t option }
-and trecord = {
-  mutable args : t list;
-  name : Hstring.t;
-  mutable lbs :  (Hstring.t * t) list;
-  record_constr : Hstring.t; (* for ADTs that become records. default is "{" *)
-}
 
 module Smtlib = struct
   let rec pp ppf = function
@@ -57,10 +50,9 @@ 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)
-    | Trecord { args = []; name; _ } | Tadt (name, []) ->
+    | Text ([], name) | Tadt (name, [], _) ->
       Fmt.pf ppf "%a" Hstring.print name
-    | Text (args, name) | Trecord { args; name; _ } | Tadt (name, args) ->
+    | Text (args, name) | Tadt (name, args, _) ->
       Fmt.(pf ppf "(@[%a %a@])" Hstring.print name (list ~sep:sp pp) args)
     | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v
     | Tvar { value = Some t; _ } -> pp ppf t
@@ -98,7 +90,6 @@ let assoc_destrs hs cases =
 
 (*** pretty print ***)
 let print_generic body_of =
-  let h = Hashtbl.create 17 in
   let rec print =
     let open Format in
     fun body_of fmt -> function
@@ -108,13 +99,6 @@ let print_generic body_of =
       | Tunit -> fprintf fmt "unit"
       | Tbitv n -> fprintf fmt "bitv[%d]" n
       | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v
-      | Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } ->
-        if Hashtbl.mem h v then
-          fprintf fmt "%a %s" print_list l (Hstring.view n)
-        else
-          (Hashtbl.add h v ();
-           (*fprintf fmt "('a_%d->%a)" v print t *)
-           print body_of fmt t)
       | Tvar{ value = Some t; _ } ->
         (*fprintf fmt "('a_%d->%a)" v print t *)
         print body_of fmt t
@@ -124,22 +108,7 @@ let print_generic body_of =
         fprintf fmt "%a <ext>%s" print_list l (Hstring.view s)
       | Tfarray (t1, t2) ->
         fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2
-      | Trecord { args = lv; name = n; lbs = lbls; _ } ->
-        begin
-          fprintf fmt "%a <record>%s" print_list lv (Hstring.view n);
-          if body_of != None then begin
-            fprintf fmt " = {";
-            let first = ref true in
-            List.iter
-              (fun (s, t) ->
-                 fprintf fmt "%s%s : %a" (if !first then "" else "; ")
-                   (Hstring.view s) (print body_of) t;
-                 first := false
-              ) lbls;
-            fprintf fmt "}"
-          end
-        end
-      | Tadt (n, lv) ->
+      | Tadt (n, lv, _) ->
         fprintf fmt "%a <adt>%s" print_list lv (Hstring.view n);
         begin match body_of with
           | None -> ()
@@ -217,16 +186,11 @@ let rec shorten ty =
     if t1 == t1' && t2 == t2' then ty
     else Tfarray(t1', t2')
 
-  | Trecord r ->
-    r.args <- List.map shorten r.args;
-    r.lbs <- List.map (fun (lb, ty) -> lb, shorten ty) r.lbs;
-    ty
-
-  | Tadt (n, args) ->
+  | Tadt (n, args, record) ->
     let args' = List.map shorten args in
     shorten_body n args;
     (* should not rebuild the type if no changes are made *)
-    Tadt (n, args')
+    Tadt (n, args', record)
 
   | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
 
@@ -248,17 +212,8 @@ let rec compare t1 t2 =
     if c<>0 then c
     else compare ta2 tb2
   | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1
-  | Trecord { args = a1; name = s1; lbs = l1; _ },
-    Trecord { args = a2; name = s2; lbs = l2; _ } ->
-    let c = Hstring.compare s1 s2 in
-    if c <> 0 then c else
-      let c = compare_list a1 a2 in
-      if c <> 0 then c else
-        let l1, l2 = List.map snd l1, List.map snd l2 in
-        compare_list l1 l2
-  | Trecord _, _ -> -1 | _ , Trecord _ -> 1
-
-  | Tadt (s1, pars1), Tadt (s2, pars2) ->
+
+  | Tadt (s1, pars1, _), Tadt (s2, pars2, _) ->
     let c = Hstring.compare s1 s2 in
     if c <> 0 then c
     else compare_list pars1 pars2
@@ -286,20 +241,10 @@ let rec equal t1 t2 =
      with Invalid_argument _ -> false)
   | Tfarray (ta1, ta2), Tfarray (tb1, tb2) ->
     equal ta1 tb1 && equal ta2 tb2
-  | Trecord { args = a1; name = s1; lbs = l1; _ },
-    Trecord { args = a2; name = s2; lbs = l2; _ } ->
-    begin
-      try
-        Hstring.equal s1 s2 && List.for_all2 equal a1 a2 &&
-        List.for_all2
-          (fun (l1, ty1) (l2, ty2) ->
-             Hstring.equal l1 l2 && equal ty1 ty2) l1 l2
-      with Invalid_argument _ -> false
-    end
   | Tint, Tint | Treal, Treal | Tbool, Tbool | Tunit, Tunit -> true
   | Tbitv n1, Tbitv n2 -> n1 =n2
 
-  | Tadt (s1, pars1), Tadt (s2, pars2) ->
+  | Tadt (s1, pars1, _), Tadt (s2, pars2, _) ->
     begin
       try Hstring.equal s1 s2 && List.for_all2 equal pars1 pars2
       with Invalid_argument _ -> false
@@ -324,13 +269,9 @@ let rec matching s pat t =
     List.fold_left2 matching s l1 l2
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) ->
     matching (matching s ta1 tb1) ta2 tb2
-  | Trecord r1, Trecord r2 when Hstring.equal r1.name r2.name ->
-    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
   | Tint , Tint | Tbool , Tbool | Treal , Treal | Tunit, Tunit -> s
   | Tbitv n , Tbitv m when n=m -> s
-  | Tadt(n1, args1), Tadt(n2, args2) when Hstring.equal n1 n2 ->
+  | Tadt(n1, args1, _), Tadt(n2, args2, _) when Hstring.equal n1 n2 ->
     List.fold_left2 matching s args1 args2
   | _ , _ ->
     raise (TypeClash(pat,t))
@@ -350,20 +291,10 @@ let apply_subst =
       let t2' = apply_subst s t2 in
       if t1 == t1' && t2 == t2' then ty else Tfarray (t1', t2')
 
-    | Trecord r ->
-      let lbs,  same1 = Lists.apply_right (apply_subst s) r.lbs in
-      let args, same2 = Lists.apply (apply_subst s) r.args in
-      if same1 && same2 then ty
-      else
-        Trecord
-          {r with args = args;
-                  name = r.name;
-                  lbs = lbs}
-
-    | Tadt(name, params)
+    | Tadt(name, params, record)
       [@ocaml.ppwarning "TODO: detect when there are no changes "]
       ->
-      Tadt (name, List.map (apply_subst s) params)
+      Tadt (name, List.map (apply_subst s) params, record)
 
     | Tint | Treal | Tbool | Tunit | Tbitv _ -> ty
   in
@@ -385,18 +316,9 @@ let rec fresh ty subst =
     let ty1, subst = fresh ty1 subst in
     let ty2, subst = fresh ty2 subst in
     Tfarray (ty1, ty2), subst
-  | Trecord ({ args; name = n; lbs; _ } as r) ->
-    let args, subst = fresh_list args subst in
-    let lbs, subst =
-      List.fold_right
-        (fun (x,ty) (lbs, subst) ->
-           let ty, subst = fresh ty subst in
-           (x, ty)::lbs, subst) lbs ([], subst)
-    in
-    Trecord {r with  args = args; name = n; lbs = lbs}, subst
-  | Tadt(s,args) ->
+  | Tadt(s,args, record) ->
     let args, subst = fresh_list args subst in
-    Tadt (s,args), subst
+    Tadt (s,args, record), subst
   | t -> t, subst
 
 and fresh_list lty subst =
@@ -521,7 +443,7 @@ let count_same_nest name l =
   Lists.sum
     (fun (_, ty) ->
        match ty with
-       | Tadt (name', _) when Hstring.equal name name' -> 1
+       | Tadt (name', _, _) when Hstring.equal name name' -> 1
        | _ -> 0
     ) l
 
@@ -531,7 +453,7 @@ let count_same_adt name l =
   Lists.sum
     (fun (_, ty) ->
        match ty with
-       | Tadt (name', params) ->
+       | Tadt (name', params, _) ->
          (* TODO: this is a hackish way to check that `name'` and `name` are
             two nests of the same mutually recursive ADT. We should store
             ADT's nests in a data structure as it's done in Dolmen. *)
@@ -542,7 +464,7 @@ let count_same_adt name l =
                   List.exists
                     (fun (_, ty') ->
                        match ty' with
-                       | Tadt (name'', _) -> Hstring.equal name name''
+                       | Tadt (name'', _, _) -> Hstring.equal name name''
                        | _ -> false
                     ) destrs
                ) cases
@@ -565,9 +487,9 @@ let cons_weight name (_, l1) (_, l2) =
     if c <> 0 then c
     else List.compare_lengths l1 l2
 
-let t_adt ?(body=None) s ty_vars =
+let t_adt ?(record=false) ?(body=None) s ty_vars =
   let hs = Hstring.make s in
-  let ty = Tadt (hs, ty_vars) in
+  let ty = Tadt (hs, ty_vars, record) in
   begin match body with
     | None -> ()
     | Some [] -> assert false
@@ -598,35 +520,14 @@ let t_adt ?(body=None) s ty_vars =
   end;
   ty
 
-let trecord ?(sort_fields = false) ~record_constr lv n lbs =
-  let lbs = List.map (fun (l,ty) -> Hstring.make l, ty) lbs in
-  let lbs, record_constr =
-    if sort_fields then
-      List.sort (fun (l1, _) (l2, _) -> Hstring.compare l1 l2) lbs,
-      Format.sprintf "%s___%s" record_constr n
-    else lbs, record_constr
-  in
-  let record_constr = Hstring.make record_constr in
-  Trecord { record_constr; args = lv; name = Hstring.make n; lbs = lbs}
-
 let rec hash t =
   match t with
   | Tvar{ v; _ } -> v
   | Text(l,s) ->
     abs (List.fold_left (fun acc x-> acc*19 + hash x) (Hstring.hash s) l)
   | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2)
-  | Trecord { args; name = s; lbs; _ } ->
-    let h =
-      List.fold_left (fun h ty -> 27 * h + hash ty) (Hstring.hash s) args
-    in
-    let h =
-      List.fold_left
-        (fun h (lb, ty) -> 23 * h + 19 * (Hstring.hash lb) + hash ty)
-        (abs h) lbs
-    in
-    abs h
 
-  | Tadt (s, args) ->
+  | Tadt (s, args, _) ->
     (* We do not hash constructors. *)
     let h =
       List.fold_left (fun h ty -> 31 * h + hash ty) (Hstring.hash s) args
@@ -640,7 +541,7 @@ let occurs { v = n; _ } t =
     | Tvar { v = m; _ } -> n=m
     | Text(l,_) -> List.exists occursrec l
     | Tfarray (t1,t2) -> occursrec t1 || occursrec t2
-    | Trecord { args ; _ } | Tadt (_, args) -> List.exists occursrec args
+    | Tadt (_, args, _) -> List.exists occursrec args
     | Tint | Treal | Tbool | Tunit | Tbitv _ -> false
   in occursrec t
 
@@ -660,12 +561,10 @@ let rec unify t1 t2 =
   | Text(l1,s1) , Text(l2,s2) when Hstring.equal s1 s2 ->
     List.iter2 unify l1 l2
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) -> unify ta1 tb1;unify ta2 tb2
-  | Trecord r1, Trecord r2 when Hstring.equal r1.name r2.name ->
-    List.iter2 unify r1.args r2.args
   | Tint, Tint | Tbool, Tbool | Treal, Treal | Tunit, Tunit -> ()
   | Tbitv n , Tbitv m when m=n -> ()
 
-  | Tadt(n1, p1), Tadt (n2, p2) when Hstring.equal n1 n2 ->
+  | Tadt(n1, p1, _), Tadt (n2, p2, _) when Hstring.equal n1 n2 ->
     List.iter2 unify p1 p2
 
   | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] ->
@@ -705,10 +604,7 @@ let vty_of t =
     | Tvar { v = i ; value = None } -> Svty.add i acc
     | Text(l,_) -> List.fold_left vty_of_rec acc l
     | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2
-    | Trecord { args; lbs; _ } ->
-      let acc = List.fold_left vty_of_rec acc args in
-      List.fold_left (fun acc (_, ty) -> vty_of_rec acc ty) acc lbs
-    | Tadt(_, args) ->
+    | Tadt(_, args, _) ->
       List.fold_left vty_of_rec acc args
 
     | Tvar { value = Some _ ; _ }
@@ -723,18 +619,12 @@ let rec monomorphize ty =
   match ty with
   | 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
-    let m_tylb =
-      List.map (fun (lb, ty_lb) -> lb, monomorphize ty_lb) tylb
-    in
-    Trecord {r with args = m_tylv; name = n; lbs = m_tylb}
   | Tfarray (ty1,ty2)    -> Tfarray (monomorphize ty1,monomorphize ty2)
   | Tvar {v=v; value=None} -> text [] ("'_c"^(string_of_int v))
   | Tvar ({ value = Some ty1; _ } as r) ->
     Tvar { r with value = Some (monomorphize ty1)}
-  | Tadt(name, params) ->
-    Tadt(name, List.map monomorphize params)
+  | Tadt(name, params, record) ->
+    Tadt(name, List.map monomorphize params, record)
 
 let print_subst fmt sbt =
   M.iter (fun n ty -> Format.fprintf fmt "%d -> %a" n print ty) sbt;
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index a47024c523..2b4dbedd8a 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -56,7 +56,7 @@ type t =
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
 
-  | Tadt of Hstring.t * t list
+  | Tadt of Hstring.t * t list * bool
   (** Application of algebraic data types. [Tadt (a, params)] denotes
       the application of the polymorphic datatype [a] to the types parameters
       [params].
@@ -65,9 +65,6 @@ type t =
       value [Tadt (Hstring.make "list", [Tint])] where the identifier "list"
       denotes a polymorphic ADT defined by the user with [t_adt]. *)
 
-  | Trecord of trecord
-  (** Record type. *)
-
 and tvar = {
   v : int;
   (** Unique identifier *)
@@ -79,20 +76,6 @@ and tvar = {
     hence distinct types should have disjoints sets of
     type variables (see function {!val:fresh}). *)
 
-and trecord = {
-  mutable args : t list;
-  (** Arguments passed to the record constructor *)
-  name : Hstring.t;
-  (** Name of the record type *)
-  mutable lbs :  (Hstring.t * t) list;
-  (** List of fields of the record. Each field has a name,
-      and an associated type. *)
-  record_constr : Hstring.t;
-  (** record constructor. Useful is case it's a specialization of an
-      algeberaic datatype. Default value is "\{__[name]" *)
-}
-(** Record types. *)
-
 type adt_constr =
   { constr : Hstring.t ;
     (** constructor of an ADT type *)
@@ -172,6 +155,7 @@ val text : t list -> string -> t
     given. *)
 
 val t_adt :
+  ?record:bool ->
   ?body: ((string * (string * t) list) list) option ->
   string -> t list ->
   t
@@ -182,17 +166,6 @@ val t_adt :
     argument is the name of the type. The third one provides its list
     of arguments. *)
 
-val trecord :
-  ?sort_fields:bool ->
-  record_constr:string -> t list -> string -> (string * t) list -> t
-(** Create a record type. [trecord args name lbs] creates a record
-    type with name [name], arguments [args] and fields [lbs].
-
-    If [sort_fields] is true, the record fields are sorted according to
-    [Hstring.compare]. This is to preserve compatibility with the old
-    typechecker behavior and should not be used in new code. *)
-
-
 (** {2 Substitutions} *)
 
 module M : Map.S with type key = int
diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml
index 8570b388f2..60e73f85cf 100644
--- a/src/lib/structures/typed.ml
+++ b/src/lib/structures/typed.ml
@@ -84,8 +84,7 @@ and 'a tt_desc =
   | TTextract of
       'a atterm * int * int
   | TTconcat of 'a atterm * 'a atterm
-  | TTdot of 'a atterm * Hstring.t
-  | TTrecord of (Hstring.t * 'a atterm) list
+  | TTrecord of Ty.t * (Hstring.t * 'a atterm) list
   | TTlet of (Symbols.t * 'a atterm) list * 'a atterm
   | TTnamed of Hstring.t * 'a atterm
   | TTite of 'a atform *
@@ -221,9 +220,7 @@ let rec print_term =
       fprintf fmt "%a^{%d, %d}" print_term t1 i j
     | TTconcat (t1, t2) ->
       fprintf fmt "%a @@ %a" print_term t1 print_term t2
-    | TTdot (t1, s) ->
-      fprintf fmt "%a.%s" print_term t1 (Hstring.view s)
-    | TTrecord l ->
+    | TTrecord (_, l) ->
       fprintf fmt "{ ";
       List.iter
         (fun (s, t) -> fprintf fmt "%s = %a" (Hstring.view s) print_term t) l;
diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli
index 47ca2a3a4d..fdead62307 100644
--- a/src/lib/structures/typed.mli
+++ b/src/lib/structures/typed.mli
@@ -118,9 +118,7 @@ and 'a tt_desc =
   (** Extract a sub-bitvector *)
   | TTconcat of 'a atterm * 'a atterm
   (* Concatenation of bitvectors *)
-  | TTdot of 'a atterm * Hstring.t
-  (** Field access on structs/records *)
-  | TTrecord of (Hstring.t * 'a atterm) list
+  | TTrecord of Ty.t * (Hstring.t * 'a atterm) list
   (** Record creation. *)
   | TTlet of (Symbols.t * 'a atterm) list * 'a atterm
   (** Let-bindings. Accept a list of mutually recursive le-bindings. *)