diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml
index 53f2b147..5dd2d16b 100644
--- a/src/smt/Congruence_closure.ml
+++ b/src/smt/Congruence_closure.ml
@@ -10,7 +10,7 @@ type conflict = Theory.conflict
 (** A signature is a shallow term shape where immediate subterms
     are representative *)
 module Signature = struct
-  type t = node term_cell
+  type t = node Term.view
   include Term_cell.Make_eq(Equiv_class)
 end
 
@@ -119,19 +119,12 @@ let[@inline] same_class_t cc (t1:term)(t2:term): bool =
   Equiv_class.equal (find_tn cc t1) (find_tn cc t2)
 
 (* compute signature *)
-let signature cc (t:term): node term_cell option =
+let signature cc (t:term): node Term.view option =
   let find = find_tn cc in
-  begin match Term.cell t with
+  begin match Term.view t with
     | App_cst (_, a) when IArray.is_empty a -> None
     | App_cst (f, a) -> App_cst (f, IArray.map find a) |> CCOpt.return
-    | Custom {view;tc} ->
-      begin match tc.tc_t_subst find view with
-        | None -> None
-        | Some u' -> Some (Custom{tc; view=u'})
-      end
-    | Bool _
-    | If _
-    | Case _
+    | Bool _ | If _
       -> None (* no congruence for these *)
    end
 
@@ -258,20 +251,12 @@ let rec decompose_explain cc (e:explanation): unit =
     | E_congruence (t1,t2) ->
       (* [t1] and [t2] must be applications of the same symbol to
          arguments that are pairwise equal *)
-      begin match t1.n_term.term_cell, t2.n_term.term_cell with
+      begin match t1.n_term.term_view, t2.n_term.term_view with
         | App_cst (f1, a1), App_cst (f2, a2) ->
           assert (Cst.equal f1 f2);
           assert (IArray.length a1 = IArray.length a2);
           IArray.iter2 (ps_add_obligation_t cc) a1 a2
-        | Custom r1, Custom r2 ->
-          (* ask the theory to explain why [r1 = r2] *)
-          let l = r1.tc.tc_t_explain (same_class_t cc) r1.view r2.view in
-          List.iter (fun (t,u) -> ps_add_obligation_t cc t u) l
-        | If _, _
-        | App_cst _, _
-        | Case _, _
-        | Bool _, _
-        | Custom _, _
+        | If _, _ | App_cst _, _ | Bool _, _
           -> assert false
       end
   end
@@ -470,17 +455,14 @@ and add_new_term cc (t:term) : node =
     add_to_parents_of_sub_node n_u
   in
   (* register sub-terms, add [t] to their parent list *)
-  begin match t.term_cell with
+  begin match t.term_view with
     | Bool _-> ()
     | App_cst (_, a) -> IArray.iter add_sub_t a
     | If (a,b,c) ->
+      (* TODO: relevancy? only [a] needs be decided for now *)
       add_sub_t a;
       add_sub_t b;
       add_sub_t c
-    | Case (u, _) -> add_sub_t u
-    | Custom {view;tc} ->
-      (* add relevant subterms to the CC *)
-      tc.tc_t_relevant view add_sub_t
   end;
   (* remove term when we backtrack *)
   on_backtrack cc
@@ -508,8 +490,7 @@ let reset_on_backtrack cc : unit =
 
 (* assert that this boolean literal holds *)
 let assert_lit cc lit : unit = match Lit.view lit with
-  | Lit_fresh _
-  | Lit_expanded _ -> ()
+  | Lit_fresh _ -> ()
   | Lit_atom t ->
     assert (Ty.is_prop t.term_ty);
     Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" Lit.pp lit);
diff --git a/src/smt/Cst.ml b/src/smt/Cst.ml
index 12b0c669..44c410ce 100644
--- a/src/smt/Cst.ml
+++ b/src/smt/Cst.ml
@@ -1,47 +1,23 @@
 
 open Solver_types
 
+type view = cst_view
 type t = cst
 
-let id t = t.cst_id
+let[@inline] id t = t.cst_id
+let[@inline] view t = t.cst_view
+let[@inline] make cst_id cst_view = {cst_id; cst_view}
 
-let ty_of_kind = function
-  | Cst_defined (ty, _, _)
-  | Cst_undef ty
-  | Cst_test (ty, _)
-  | Cst_proj (ty, _, _) -> ty
-  | Cst_cstor (lazy cstor) -> cstor.cstor_ty
-
-let ty t = ty_of_kind t.cst_kind
-
-let arity t = fst (Ty.unfold_n (ty t))
-
-let make cst_id cst_kind = {cst_id; cst_kind}
-let make_cstor id ty cstor =
-  let _, ret = Ty.unfold ty in
-  assert (Ty.is_data ret);
-  make id (Cst_cstor cstor)
-let make_proj id ty cstor i =
-  make id (Cst_proj (ty, cstor, i))
-let make_tester id ty cstor =
-  make id (Cst_test (ty, cstor))
-
-let make_defined id ty t info = make id (Cst_defined (ty, t, info))
-
-let make_undef id ty = make id (Cst_undef ty)
-
-let as_undefined (c:t) = match c.cst_kind with
+let as_undefined (c:t) = match view c with
   | Cst_undef ty -> Some (c,ty)
-  | Cst_defined _ | Cst_cstor _ | Cst_proj _ | Cst_test _
-    -> None
+  | Cst_def _ -> None
 
 let as_undefined_exn (c:t) = match as_undefined c with
   | Some tup -> tup
   | None -> assert false
 
-let is_finite_cstor c = match c.cst_kind with
-  | Cst_cstor (lazy {cstor_card=Finite; _}) -> true
-  | _ -> false
+let[@inline] mk_undef id ty = make id (Cst_undef ty)
+let[@inline] mk_undef_const id ty = mk_undef id (Ty.Fun.mk [] ty)
 
 let equal a b = ID.equal a.cst_id b.cst_id
 let compare a b = ID.compare a.cst_id b.cst_id
diff --git a/src/smt/Cst.mli b/src/smt/Cst.mli
index 2e68beb6..08d118eb 100644
--- a/src/smt/Cst.mli
+++ b/src/smt/Cst.mli
@@ -1,21 +1,20 @@
 
 open Solver_types
 
+type view = cst_view
 type t = cst
+
 val id : t -> ID.t
-val ty : t -> Ty.t
-val make_cstor : ID.t -> Ty.t -> data_cstor lazy_t -> t
-val make_proj : ID.t -> Ty.t -> data_cstor lazy_t -> int -> t
-val make_tester : ID.t -> Ty.t -> data_cstor lazy_t -> t
-val make_defined : ID.t -> Ty.t -> term lazy_t -> cst_defined_info -> t
-val make_undef : ID.t -> Ty.t -> t
-val arity : t -> int (* number of args *)
+val view : t -> view
 val equal : t -> t -> bool
 val compare : t -> t -> int
 val hash : t -> int
-val as_undefined : t -> (t * Ty.t) option
-val as_undefined_exn : t -> t * Ty.t
-val is_finite_cstor : t -> bool
+val as_undefined : t -> (t * Ty.Fun.t) option
+val as_undefined_exn : t -> t * Ty.Fun.t
+
+val mk_undef : ID.t -> Ty.Fun.t -> t
+val mk_undef_const : ID.t -> Ty.t -> t
+
 val pp : t Fmt.printer
 module Map : CCMap.S with type key = t
 module Tbl : CCHashtbl.S with type key = t
diff --git a/src/smt/Lit.ml b/src/smt/Lit.ml
index ed1e1890..11719c27 100644
--- a/src/smt/Lit.ml
+++ b/src/smt/Lit.ml
@@ -9,7 +9,6 @@ type t = lit = {
 and view = lit_view =
   | Lit_fresh of ID.t
   | Lit_atom of term
-  | Lit_expanded of term
 
 let neg l = {l with lit_sign=not l.lit_sign}
 
@@ -38,10 +37,6 @@ let atom ?(sign=true) (t:term) : t =
   let sign = if not sign' then not sign else sign in
   make ~sign (Lit_atom t)
 
-let expanded t = make ~sign:true (Lit_expanded t)
-
-let cstor_test tst cstor t = atom ~sign:true (Term.cstor_test tst cstor t)
-
 let as_atom (lit:t) : (term * bool) option = match lit.lit_view with
   | Lit_atom t -> Some (t, lit.lit_sign)
   | _ -> None
diff --git a/src/smt/Lit.mli b/src/smt/Lit.mli
index f877b444..6aac0a76 100644
--- a/src/smt/Lit.mli
+++ b/src/smt/Lit.mli
@@ -10,7 +10,6 @@ type t = lit = {
 and view = lit_view =
   | Lit_fresh of ID.t
   | Lit_atom of term
-  | Lit_expanded of term
 
 val neg : t -> t
 val abs : t -> t
@@ -21,8 +20,6 @@ val fresh_with : ID.t -> t
 val fresh : unit -> t
 val dummy : t
 val atom : ?sign:bool -> term -> t
-val cstor_test : Term.state -> data_cstor -> term -> t
-val expanded : term -> t
 val hash : t -> int
 val compare : t -> t -> int
 val equal : t -> t -> bool
diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml
index ac0cb093..c7107a6f 100644
--- a/src/smt/Solver_types.ml
+++ b/src/smt/Solver_types.ml
@@ -8,72 +8,17 @@ type 'a lazily_expanded =
   | Lazy_none
 
 (* main term cell. *)
-and term = {
+type term = {
   mutable term_id: int; (* unique ID *)
   mutable term_ty: ty;
-  term_cell: term term_cell;
+  term_view : term term_view;
 }
 
 (* term shallow structure *)
-and 'a term_cell =
+and 'a term_view =
   | Bool of bool
   | App_cst of cst * 'a IArray.t (* full, first-order application *)
   | If of 'a * 'a * 'a
-  | Case of 'a * 'a ID.Map.t (* check head constructor *)
-  | Custom of {
-      view: 'a term_view_custom;
-      tc: term_view_tc;
-    }
-
-(** Methods on the custom term view whose leaves are ['a].
-    Terms must be comparable, hashable, printable, and provide
-    some additional theory handles.
-
-    - [tc_t_sub] must return all immediate subterms (all ['a] contained in the term)
-
-    - [tc_t_subst] must use the function to replace all subterms (all the ['a]
-      returned by [tc_t_sub]) by ['b]
-
-    - [tc_t_relevant] must return a subset of [tc_t_sub] (possibly the same set).
-      The terms it returns will be activated and evaluated whenever possible.
-      Terms in [tc_t_sub t \ tc_t_relevant t] are considered for
-      congruence but not for evaluation.
-
-    - If [t1] and [t2] satisfy [tc_t_is_semantic] and have the same type,
-      then [tc_t_solve t1 t2] must succeed by returning some {!solve_result}.
-
-    - if [tc_t_equal eq a b = true], then [tc_t_explain eq a b] must
-      return all the pairs of equal subterms that are sufficient
-      for [a] and [b] to be equal.
-*)
-and term_view_tc = {
-  tc_t_pp : 'a. 'a Fmt.printer -> 'a term_view_custom Fmt.printer;
-  tc_t_equal : 'a. 'a CCEqual.t -> 'a term_view_custom CCEqual.t;
-  tc_t_hash : 'a. 'a Hash.t -> 'a term_view_custom Hash.t;
-  tc_t_ty : 'a. ('a -> ty) -> 'a term_view_custom -> ty;
-  tc_t_is_semantic : 'a. 'a term_view_custom -> bool; (* is this a semantic term? semantic terms must be solvable *)
-  tc_t_solve: cc_node term_view_custom -> cc_node term_view_custom -> solve_result; (* solve an equation between classes *)
-  tc_t_sub : 'a. 'a term_view_custom -> 'a Sequence.t; (* iter on immediate subterms *)
-  tc_t_abs : self:term -> term term_view_custom -> term * bool; (* remove the sign? *)
-  tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t; (* iter on relevant immediate subterms *)
-  tc_t_subst : 'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option; (* substitute immediate subterms and canonize *)
-  tc_t_explain : 'a. 'a CCEqual.t -> 'a term_view_custom -> 'a term_view_custom -> ('a * 'a) list;
-  (* explain why the two views are equal *)
-}
-
-(** Custom term view for theories *)
-and 'a term_view_custom = ..
-
-(** The result of a call to {!solve}. *)
-and solve_result =
-  | Solve_ok of {
-    subst: (cc_node * term) list; (** binding leaves to other terms *)
-  } (** Success,  the two terms being equal is equivalent
-        to the given substitution *)
-  | Solve_fail of {
-    expl: lit list;
-  } (** Failure, because of the given explanation.
-        The two terms cannot be equal *)
 
 (** A node of the congruence closure.
     An equivalence class is represented by its "root" element,
@@ -118,74 +63,61 @@ and lit = {
 and lit_view =
   | Lit_fresh of ID.t (* fresh literals *)
   | Lit_atom of term
-  | Lit_expanded of term (* expanded? used for recursive calls mostly *)
-      (* TODO: remove this, unfold on the fly *)
 
 and cst = {
   cst_id: ID.t;
-  cst_kind: cst_kind;
+  cst_view: cst_view;
 }
 
-and cst_kind =
-  | Cst_undef of ty (* simple undefined constant *)
-  | Cst_cstor of data_cstor lazy_t
-  | Cst_proj of ty * data_cstor lazy_t * int (* [cstor, argument position] *)
-  | Cst_test of ty * data_cstor lazy_t (* test if [cstor] *)
-  | Cst_defined of ty * term lazy_t * cst_defined_info
+and cst_view =
+  | Cst_undef of fun_ty (* simple undefined constant *)
+  | Cst_def of {
+      pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
+      abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
+      relevant : 'a. 'a IArray.t -> 'a Sequence.t; (* iter on relevant immediate subterms *)
+      ty : term IArray.t -> ty; (* compute type *)
+    }
+(** Methods on the custom term view whose arguments are ['a].
+    Terms must be printable, and provide some additional theory handles.
 
-(* what kind of constant is that? *)
-and cst_defined_info =
-  | Cst_recursive (* TODO: the set of Horn rules compiled from the def *)
-  | Cst_non_recursive
+    - [relevant] must return a subset of [args] (possibly the same set).
+      The terms it returns will be activated and evaluated whenever possible.
+      Terms in [args \ relevant args] are considered for
+      congruence but not for evaluation.
+*)
 
-(* this is a disjunction of sufficient conditions for the existence of
-   some meta (cst). Each condition is a literal *)
-and cst_exist_conds = lit lazy_t list ref
-
-and 'a db_env = {
-  db_st: 'a option list;
-  db_size: int;
+(** Function type *)
+and fun_ty = {
+  fun_ty_args: ty list;
+  fun_ty_ret: ty;
 }
 
-(* Hashconsed type *)
+(** Hashconsed type *)
 and ty = {
   mutable ty_id: int;
-  ty_cell: ty_cell;
-  ty_card: ty_card lazy_t;
+  ty_view: ty_view;
 }
 
+and ty_view =
+  | Ty_prop
+  | Ty_atomic of {
+      def: ty_def;
+      args: ty list;
+      card: ty_card lazy_t;
+    }
+
+and ty_def =
+  | Ty_uninterpreted of ID.t
+  | Ty_def of {
+      id: ID.t;
+      pp: ty Fmt.printer -> ty list Fmt.printer;
+      card: ty list -> ty_card;
+    }
+
 and ty_card =
   | Finite
   | Infinite
 
-and ty_def =
-  | Uninterpreted
-  | Data of datatype (* set of constructors *)
-
-and datatype = {
-  data_cstors: data_cstor ID.Map.t lazy_t;
-}
-
-(* TODO: in cstor, add:
-   - for each selector, a special "magic" term for undefined, in
-     case the selector is ill-applied (Collapse 2)  *)
-
-(* a constructor *)
-and data_cstor = {
-  cstor_ty: ty;
-  cstor_args: ty IArray.t; (* argument types *)
-  cstor_proj: cst IArray.t lazy_t; (* projectors *)
-  cstor_test: cst lazy_t; (* tester *)
-  cstor_cst: cst; (* the cstor itself *)
-  cstor_card: ty_card; (* cardinality of the constructor('s args) *)
-}
-
-and ty_cell =
-  | Prop
-  | Atomic of ID.t * ty_def
-  | Arrow of ty * ty
-
-
 let[@inline] term_equal_ (a:term) b = a==b
 let[@inline] term_hash_ a = a.term_id
 let[@inline] term_cmp_ a b = CCInt.compare a.term_id b.term_id
@@ -197,15 +129,11 @@ let cmp_lit a b =
     let int_of_cell_ = function
       | Lit_fresh _ -> 0
       | Lit_atom _ -> 1
-      | Lit_expanded _ -> 2
     in
     match a.lit_view, b.lit_view with
       | Lit_fresh i1, Lit_fresh i2 -> ID.compare i1 i2
       | Lit_atom t1, Lit_atom t2 -> term_cmp_ t1 t2
-      | Lit_expanded t1, Lit_expanded t2 -> term_cmp_ t1 t2
-      | Lit_fresh _, _
-      | Lit_atom _, _
-      | Lit_expanded _, _
+      | Lit_fresh _, _ | Lit_atom _, _
         -> CCInt.compare (int_of_cell_ a.lit_view) (int_of_cell_ b.lit_view)
   )
 
@@ -216,8 +144,6 @@ let hash_lit a =
   match a.lit_view with
     | Lit_fresh i -> Hash.combine3 1 (Hash.bool sign) (ID.hash i)
     | Lit_atom t -> Hash.combine3 2 (Hash.bool sign) (term_hash_ t)
-    | Lit_expanded t ->
-      Hash.combine3 3 (Hash.bool sign) (term_hash_ t)
 
 let cmp_cc_node a b = term_cmp_ a.n_term b.n_term
 
@@ -245,60 +171,39 @@ let id_of_cst a = a.cst_id
 
 let pp_db out (i,_) = Format.fprintf out "%%%d" i
 
-let ty_unfold ty : ty list * ty =
-  let rec aux acc ty = match ty.ty_cell with
-    | Arrow (a,b) -> aux (a::acc) b
-    | _ -> List.rev acc, ty
-  in
-  aux [] ty
+let rec pp_ty out t = match t.ty_view with
+  | Ty_prop -> Fmt.string out "prop"
+  | Ty_atomic {def=Ty_uninterpreted id; args=[]; _} -> ID.pp out id
+  | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
+    Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args
+  | Ty_atomic {def=Ty_def def; args; _} -> def.pp pp_ty out args
 
-let rec pp_ty out t = match t.ty_cell with
-  | Prop -> Fmt.string out "prop"
-  | Atomic (id, _) -> ID.pp out id
-  | Arrow _ ->
-    let args, ret = ty_unfold t in
-    Format.fprintf out "(@[->@ %a@ %a@])"
-      (Util.pp_list pp_ty) args pp_ty ret
+let pp_term_view ~pp_id ~pp_t out = function
+  | Bool true -> Fmt.string out "true"
+  | Bool false -> Fmt.string out "false"
+  | App_cst ({cst_view=Cst_def {pp=Some pp_custom;_};_},l) -> pp_custom pp_t out l
+  | App_cst (c, a) when IArray.is_empty a ->
+    pp_id out (id_of_cst c)
+  | App_cst (f,l) ->
+    Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_cst f) (Util.pp_iarray pp_t) l
+  | If (a, b, c) ->
+    Fmt.fprintf out "(@[if %a@ %a@ %a@])" pp_t a pp_t b pp_t c
 
 let pp_term_top ~ids out t =
   let rec pp out t =
     pp_rec out t;
-    (* FIXME
-    if Config.pp_hashcons then Format.fprintf out "/%d" t.term_id;
-       *)
-    ()
-
-  and pp_rec out t = match t.term_cell with
-    | Bool true -> Fmt.string out "true"
-    | Bool false -> Fmt.string out "false"
-    | App_cst (c, a) when IArray.is_empty a ->
-      pp_id out (id_of_cst c)
-    | App_cst (f,l) ->
-      Fmt.fprintf out "(@[<1>%a@ %a@])" pp_id (id_of_cst f) (Util.pp_iarray pp) l
-    | If (a, b, c) ->
-      Fmt.fprintf out "(@[if %a@ %a@ %a@])" pp a pp b pp c
-    | Case (t,m) ->
-      let pp_bind out (id,rhs) =
-        Fmt.fprintf out "(@[<1>case %a@ %a@])" pp_id id pp rhs
-      in
-      let print_map =
-        Fmt.seq ~sep:(Fmt.return "@ ") pp_bind
-      in
-      Fmt.fprintf out "(@[match %a@ (@[<hv>%a@])@])"
-        pp t print_map (ID.Map.to_seq m)
-    | Custom {view; tc} -> tc.tc_t_pp pp out view
-  and pp_id =
-    if ids then ID.pp else ID.pp_name
-  in
+    (* FIXME if Config.pp_hashcons then Format.fprintf out "/%d" t.term_id; *)
+  and pp_rec out t = pp_term_view ~pp_id ~pp_t:pp_rec out t.term_view
+  and pp_id = if ids then ID.pp else ID.pp_name in
   pp out t
 
 let pp_term = pp_term_top ~ids:false
+let pp_term_view = pp_term_view ~pp_id:ID.pp_name ~pp_t:pp_term
 
 let pp_lit out l =
   let pp_lit_view out = function
     | Lit_fresh i -> Format.fprintf out "#%a" ID.pp i
     | Lit_atom t -> pp_term out t
-    | Lit_expanded t -> Format.fprintf out "(@[<1>expanded@ %a@])" pp_term t
   in
   if l.lit_sign then pp_lit_view out l.lit_view
   else Format.fprintf out "(@[@<1>¬@ %a@])" pp_lit_view l.lit_view
diff --git a/src/smt/Term.ml b/src/smt/Term.ml
index 39fe2bef..3ae323d8 100644
--- a/src/smt/Term.ml
+++ b/src/smt/Term.ml
@@ -4,36 +4,17 @@ open Solver_types
 type t = term = {
   mutable term_id : int;
   mutable term_ty : ty;
-  term_cell : t term_cell;
+  term_view : t term_view;
 }
 
-type 'a cell = 'a term_cell =
+type 'a view = 'a term_view =
   | Bool of bool
   | App_cst of cst * 'a IArray.t
   | If of 'a * 'a * 'a
-  | Case of 'a * 'a ID.Map.t
-  | Custom of { view : 'a term_view_custom; tc : term_view_tc; }
-
-type 'a custom = 'a Solver_types.term_view_custom = ..
-
-type tc = Solver_types.term_view_tc = {
-  tc_t_pp : 'a. 'a Fmt.printer -> 'a custom Fmt.printer;
-  tc_t_equal : 'a. 'a CCEqual.t -> 'a custom CCEqual.t;
-  tc_t_hash : 'a. 'a Hash.t -> 'a custom Hash.t;
-  tc_t_ty : 'a. ('a -> ty) -> 'a custom -> ty;
-  tc_t_is_semantic : 'a. 'a custom -> bool;
-  tc_t_solve : cc_node custom -> cc_node custom -> solve_result;
-  tc_t_sub : 'a. 'a custom -> 'a Sequence.t;
-  tc_t_abs : self:term -> term custom -> term * bool;
-  tc_t_relevant : 'a. 'a custom -> 'a Sequence.t;
-  tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom option;
-  tc_t_explain : 'a. 'a CCEqual.t -> 'a custom -> 'a custom -> ('a * 'a) list;
-}
-
 
 let[@inline] id t = t.term_id
 let[@inline] ty t = t.term_ty
-let[@inline] cell t = t.term_cell
+let[@inline] view t = t.term_view
 
 let equal = term_equal_
 let hash = term_hash_
@@ -51,13 +32,13 @@ let mk_real_ st c : t =
   let t = {
     term_id= st.n;
     term_ty;
-    term_cell=c;
+    term_view=c;
   } in
   st.n <- 1 + st.n;
   Term_cell.Tbl.add st.tbl c t;
   t
 
-let[@inline] make st (c:t term_cell) : t =
+let[@inline] make st (c:t term_view) : t =
   try Term_cell.Tbl.find st.tbl c
   with Not_found -> mk_real_ st c
 
@@ -83,39 +64,24 @@ let app_cst st f a =
 
 let const st c = app_cst st c IArray.empty
 
-let case st u m = make st (Term_cell.case u m)
-
 let if_ st a b c = make st (Term_cell.if_ a b c)
 
 (* "eager" and, evaluating [a] first *)
 let and_eager st a b = if_ st a b (false_ st)
 
-let custom st ~tc view = make st (Term_cell.custom ~tc view)
-
-let cstor_test st cstor t = make st (Term_cell.cstor_test cstor t)
-let cstor_proj st cstor i t = make st (Term_cell.cstor_proj cstor i t)
-
 (* might need to tranfer the negation from [t] to [sign] *)
-let abs t : t * bool = match t.term_cell with
-  | Custom {view;tc} -> tc.tc_t_abs ~self:t view
+let abs t : t * bool = match view t with
+  | App_cst ({cst_view=Cst_def def; _}, args) ->
+    def.abs ~self:t args
   | _ -> t, true
 
-let[@inline] is_true t = match t.term_cell with Bool true -> true | _ -> false
-let[@inline]  is_false t = match t.term_cell with Bool false -> true | _ -> false
+let[@inline] is_true t = match view t with Bool true -> true | _ -> false
+let[@inline] is_false t = match view t with Bool false -> true | _ -> false
 
-let[@inline] is_const t = match t.term_cell with
+let[@inline] is_const t = match view t with
   | App_cst (_, a) -> IArray.is_empty a
   | _ -> false
 
-let[@inline] is_custom t = match t.term_cell with
-  | Custom _ -> true
-  | _ -> false
-
-let[@inline] is_semantic t = match t.term_cell with
-  | Bool _ -> true
-  | Custom {view;tc} -> tc.tc_t_is_semantic view
-  | _ -> false
-
 module As_key = struct
     type t = term
     let compare = compare
@@ -129,49 +95,23 @@ module Tbl = CCHashtbl.Make(As_key)
 let to_seq t yield =
   let rec aux t =
     yield t;
-    match t.term_cell with
-      | Bool _ -> ()
-      | App_cst (_,a) -> IArray.iter aux a
-      | If (a,b,c) -> aux a; aux b; aux c
-      | Case (t, m) ->
-        aux t;
-        ID.Map.iter (fun _ rhs -> aux rhs) m
-      | Custom {view;tc} -> tc.tc_t_sub view aux
+    match view t with
+    | Bool _ -> ()
+    | App_cst (_,a) -> IArray.iter aux a
+    | If (a,b,c) -> aux a; aux b; aux c
   in
   aux t
 
 (* return [Some] iff the term is an undefined constant *)
-let as_cst_undef (t:term): (cst * Ty.t) option =
-  match t.term_cell with
-    | App_cst (c, a) when IArray.is_empty a ->
-      Cst.as_undefined c
-    | _ -> None
-
-(* return [Some (cstor,ty,args)] if the term is a constructor
-   applied to some arguments *)
-let as_cstor_app (t:term): (cst * data_cstor * term IArray.t) option =
-  match t.term_cell with
-    | App_cst ({cst_kind=Cst_cstor (lazy cstor); _} as c, a) ->
-      Some (c,cstor,a)
-    | _ -> None
-
-(* typical view for unification/equality *)
-type unif_form =
-  | Unif_cst of cst * Ty.t
-  | Unif_cstor of cst * data_cstor * term IArray.t
-  | Unif_none
-
-let as_unif (t:term): unif_form = match t.term_cell with
-  | App_cst ({cst_kind=Cst_undef ty; _} as c, a) when IArray.is_empty a ->
-    Unif_cst (c,ty)
-  | App_cst ({cst_kind=Cst_cstor (lazy cstor); _} as c, a) ->
-    Unif_cstor (c,cstor,a)
-  | _ -> Unif_none
+let as_cst_undef (t:term): (cst * Ty.Fun.t) option =
+  match view t with
+  | App_cst (c, a) when IArray.is_empty a -> Cst.as_undefined c
+  | _ -> None
 
 let pp = Solver_types.pp_term
 
 let dummy : t = {
   term_id= -1;
   term_ty=Ty.prop;
-  term_cell=Term_cell.true_;
+  term_view=Term_cell.true_;
 }
diff --git a/src/smt/Term.mli b/src/smt/Term.mli
index 01f9c124..012ecb71 100644
--- a/src/smt/Term.mli
+++ b/src/smt/Term.mli
@@ -4,34 +4,16 @@ open Solver_types
 type t = term = {
   mutable term_id : int;
   mutable term_ty : ty;
-  term_cell : t term_cell;
+  term_view : t term_view;
 }
 
-type 'a cell = 'a term_cell =
+type 'a view = 'a term_view =
   | Bool of bool
   | App_cst of cst * 'a IArray.t
   | If of 'a * 'a * 'a
-  | Case of 'a * 'a ID.Map.t
-  | Custom of { view : 'a term_view_custom; tc : term_view_tc; }
-
-type 'a custom = 'a Solver_types.term_view_custom = ..
-
-type tc = Solver_types.term_view_tc = {
-  tc_t_pp : 'a. 'a Fmt.printer -> 'a custom Fmt.printer;
-  tc_t_equal : 'a. 'a CCEqual.t -> 'a custom CCEqual.t;
-  tc_t_hash : 'a. 'a Hash.t -> 'a custom Hash.t;
-  tc_t_ty : 'a. ('a -> ty) -> 'a custom -> ty;
-  tc_t_is_semantic : 'a. 'a custom -> bool;
-  tc_t_solve : cc_node custom -> cc_node custom -> solve_result;
-  tc_t_sub : 'a. 'a custom -> 'a Sequence.t;
-  tc_t_abs : self:term -> term custom -> term * bool;
-  tc_t_relevant : 'a. 'a custom -> 'a Sequence.t;
-  tc_t_subst : 'a 'b. ('a -> 'b) -> 'a custom -> 'b custom option;
-  tc_t_explain : 'a. 'a CCEqual.t -> 'a custom -> 'a custom -> ('a * 'a) list;
-}
 
 val id : t -> int
-val cell : t -> term term_cell
+val view : t -> term view
 val ty : t -> Ty.t
 val equal : t -> t -> bool
 val compare : t -> t -> int
@@ -41,18 +23,13 @@ type state
 
 val create : ?size:int -> unit -> state
 
-val make : state -> t term_cell -> t
+val make : state -> t view -> t
 val true_ : state -> t
 val false_ : state -> t
 val const : state -> cst -> t
 val app_cst : state -> cst -> t IArray.t -> t
 val if_: state -> t -> t -> t -> t
-val case : state -> t -> t ID.Map.t -> t
 val and_eager : state -> t -> t -> t (* evaluate left argument first *)
-val custom : state -> tc:tc -> t custom -> t
-
-val cstor_test : state -> data_cstor -> term -> t
-val cstor_proj : state -> data_cstor -> int -> term -> t
 
 (* TODO: remove *)
 val abs : t -> t * bool
@@ -68,23 +45,9 @@ val pp : t Fmt.printer
 val is_true : t -> bool
 val is_false : t -> bool
 val is_const : t -> bool
-val is_custom : t -> bool
-
-val is_semantic : t -> bool
-(** Custom term that is Shostak-ready (ie can be solved) *)
 
 (* return [Some] iff the term is an undefined constant *)
-val as_cst_undef : t -> (cst * Ty.t) option
-
-val as_cstor_app : t -> (cst * data_cstor * t IArray.t) option
-
-(* typical view for unification/equality *)
-type unif_form =
-  | Unif_cst of cst * Ty.t
-  | Unif_cstor of cst * data_cstor * term IArray.t
-  | Unif_none
-
-val as_unif : t -> unif_form
+val as_cst_undef : t -> (cst * Ty.Fun.t) option
 
 (** {6 Containers} *)
 
diff --git a/src/smt/Term_cell.ml b/src/smt/Term_cell.ml
index 3a14203d..5446f2e8 100644
--- a/src/smt/Term_cell.ml
+++ b/src/smt/Term_cell.ml
@@ -3,34 +3,12 @@ open Solver_types
 
 (* TODO: normalization of {!term_cell} for use in signatures? *)
 
-type 'a cell = 'a Solver_types.term_cell =
+type 'a view = 'a Solver_types.term_view =
   | Bool of bool
   | App_cst of cst * 'a IArray.t
   | If of 'a * 'a * 'a
-  | Case of 'a * 'a ID.Map.t
-  | Custom of {
-      view : 'a term_view_custom;
-      tc : term_view_tc;
-    }
 
-type 'a custom = 'a Solver_types.term_view_custom = ..
-
-type tc = Solver_types.term_view_tc = {
-  tc_t_pp : 'a. 'a Fmt.printer -> 'a term_view_custom Fmt.printer;
-  tc_t_equal : 'a. 'a CCEqual.t -> 'a term_view_custom CCEqual.t;
-  tc_t_hash : 'a. 'a Hash.t -> 'a term_view_custom Hash.t;
-  tc_t_ty : 'a. ('a -> ty) -> 'a term_view_custom -> ty;
-  tc_t_is_semantic : 'a. 'a term_view_custom -> bool;
-  tc_t_solve : cc_node term_view_custom -> cc_node term_view_custom -> solve_result;
-  tc_t_sub : 'a. 'a term_view_custom -> 'a Sequence.t;
-  tc_t_abs : self:term -> term custom -> term * bool;
-  tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t;
-  tc_t_subst :
-    'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option;
-  tc_t_explain : 'a. 'a CCEqual.t -> 'a term_view_custom -> 'a term_view_custom -> ('a * 'a) list;
-}
-
-type t = term term_cell
+type t = term view
 
 module type ARG = sig
   type t
@@ -42,41 +20,20 @@ module Make_eq(A : ARG) = struct
   let sub_hash = A.hash
   let sub_eq = A.equal
 
-  let hash (t:A.t term_cell) : int = match t with
+  let hash (t:A.t view) : int = match t with
     | Bool b -> Hash.bool b
     | App_cst (f,l) ->
       Hash.combine3 4 (Cst.hash f) (Hash.iarray sub_hash l)
     | If (a,b,c) -> Hash.combine4 7 (sub_hash a) (sub_hash b) (sub_hash c)
-    | Case (u,m) ->
-      let hash_m =
-        Hash.seq (Hash.pair ID.hash sub_hash) (ID.Map.to_seq m)
-      in
-      Hash.combine3 8 (sub_hash u) hash_m
-    | Custom {view;tc} -> tc.tc_t_hash sub_hash view
 
   (* equality that relies on physical equality of subterms *)
-  let equal (a:A.t term_cell) b : bool = match a, b with
+  let equal (a:A.t view) b : bool = match a, b with
     | Bool b1, Bool b2 -> CCBool.equal b1 b2
     | App_cst (f1, a1), App_cst (f2, a2) ->
       Cst.equal f1 f2 && IArray.equal sub_eq a1 a2
     | If (a1,b1,c1), If (a2,b2,c2) ->
       sub_eq a1 a2 && sub_eq b1 b2 && sub_eq c1 c2
-    | Case (u1, m1), Case (u2, m2) ->
-      sub_eq u1 u2 &&
-      ID.Map.for_all
-        (fun k1 rhs1 ->
-           try sub_eq rhs1 (ID.Map.find k1 m2)
-           with Not_found -> false)
-        m1
-      &&
-      ID.Map.for_all (fun k2 _ -> ID.Map.mem k2 m1) m2
-    | Custom r1, Custom r2 ->
-      r1.tc.tc_t_equal sub_eq r1.view r2.view
-    | Bool _, _
-    | App_cst _, _
-    | If _, _
-    | Case _, _
-    | Custom _, _
+    | Bool _, _ | App_cst _, _ | If _, _
       -> false
 end[@@inline]
 
@@ -92,47 +49,41 @@ let false_ = Bool false
 let app_cst f a = App_cst (f, a)
 let const c = App_cst (c, IArray.empty)
 
-let case u m = Case (u,m)
 let if_ a b c =
   assert (Ty.equal b.term_ty c.term_ty);
   If (a,b,c)
 
-let cstor_test cstor t =
-  app_cst (Lazy.force cstor.cstor_test) (IArray.singleton t)
-
-let cstor_proj cstor i t =
-  let p = IArray.get (Lazy.force cstor.cstor_proj) i in
-  app_cst p (IArray.singleton t)
-
-let custom ~tc view = Custom {view;tc}
-
-(* type of an application *)
-let rec app_ty_ ty l : Ty.t = match Ty.view ty, l with
-  | _, [] -> ty
-  | Arrow (ty_a,ty_rest), a::tail ->
-    assert (Ty.equal ty_a a.term_ty);
-    app_ty_ ty_rest tail
-  | (Prop | Atomic _), _::_ ->
-    assert false
+let pp = pp_term_view
 
 let ty (t:t): Ty.t = match t with
   | Bool _ -> Ty.prop
-  | App_cst (f, a) ->
-    let n_args, ret = Cst.ty f |> Ty.unfold_n in
-    if n_args = IArray.length a
-    then ret (* fully applied *)
-    else (
-      assert (IArray.length a < n_args);
-      app_ty_ (Cst.ty f) (IArray.to_list a)
-    )
+  | App_cst (f, args) ->
+    begin match Cst.view f with
+      | Cst_undef fty -> 
+        let ty_args, ty_ret = Ty.Fun.unfold fty in
+        (* check arity *)
+        if List.length ty_args <> IArray.length args then (
+          Error.errorf "Term_cell.apply: expected %d args, got %d@ in %a"
+            (List.length ty_args) (IArray.length args) pp t
+
+        );
+        (* check types *)
+        List.iteri
+          (fun i ty_a ->
+             let a = IArray.get args i in
+             if not @@ Ty.equal a.term_ty ty_a then (
+               Error.errorf "Term_cell.apply: %d-th argument mismatch:@ \
+                             %a does not have type %a@ in %a"
+                 i pp_term a Ty.pp ty_a pp t
+             ))
+          ty_args;
+        ty_ret
+      | Cst_def def -> def.ty args
+    end
   | If (_,b,_) -> b.term_ty
-  | Case (_,m) ->
-    let _, rhs = ID.Map.choose m in
-    rhs.term_ty
-  | Custom {view;tc} -> tc.tc_t_ty (fun t -> t.term_ty) view
 
 module Tbl = CCHashtbl.Make(struct
-    type t = term term_cell
+    type t = term view
     let equal = equal
     let hash = hash
   end)
diff --git a/src/smt/Term_cell.mli b/src/smt/Term_cell.mli
index f25967da..0ef8bb07 100644
--- a/src/smt/Term_cell.mli
+++ b/src/smt/Term_cell.mli
@@ -1,35 +1,12 @@
 
 open Solver_types
 
-type 'a cell = 'a Solver_types.term_cell =
+type 'a view = 'a Solver_types.term_view =
   | Bool of bool
   | App_cst of cst * 'a IArray.t
   | If of 'a * 'a * 'a
-  | Case of 'a * 'a ID.Map.t
-  | Custom of {
-      view : 'a term_view_custom;
-      tc : term_view_tc;
-    }
 
-type 'a custom = 'a Solver_types.term_view_custom = ..
-
-type tc = Solver_types.term_view_tc = {
-  tc_t_pp : 'a. 'a Fmt.printer -> 'a term_view_custom Fmt.printer;
-  tc_t_equal : 'a. 'a CCEqual.t -> 'a term_view_custom CCEqual.t;
-  tc_t_hash : 'a. 'a Hash.t -> 'a term_view_custom Hash.t;
-  tc_t_ty : 'a. ('a -> ty) -> 'a term_view_custom -> ty;
-  tc_t_is_semantic : 'a. 'a term_view_custom -> bool;
-  tc_t_solve : cc_node term_view_custom -> cc_node term_view_custom -> solve_result;
-  tc_t_sub : 'a. 'a term_view_custom -> 'a Sequence.t;
-  tc_t_abs : self:term -> term custom -> term * bool;
-  tc_t_relevant : 'a. 'a term_view_custom -> 'a Sequence.t;
-  tc_t_subst :
-    'a 'b. ('a -> 'b) -> 'a term_view_custom -> 'b term_view_custom option;
-  tc_t_explain : 'a. 'a CCEqual.t -> 'a term_view_custom -> 'a term_view_custom -> ('a * 'a) list;
-}
-
-
-type t = term term_cell
+type t = term view
 
 val equal : t -> t -> bool
 val hash : t -> int
@@ -38,15 +15,13 @@ val true_ : t
 val false_ : t
 val const : cst -> t
 val app_cst : cst -> term IArray.t -> t
-val cstor_test : data_cstor -> term -> t
-val cstor_proj : data_cstor -> int -> term -> t
-val case : term -> term ID.Map.t -> t
 val if_ : term -> term -> term -> t
-val custom : tc:term_view_tc -> term term_view_custom -> t
 
 val ty : t -> Ty.t
 (** Compute the type of this term cell. Not totally free *)
 
+val pp : t Fmt.printer
+
 module Tbl : CCHashtbl.S with type key = t
 
 module type ARG = sig
@@ -56,6 +31,6 @@ module type ARG = sig
 end
 
 module Make_eq(X : ARG) : sig
-  val equal : X.t term_cell -> X.t term_cell -> bool
-  val hash : X.t term_cell -> int
+  val equal : X.t view -> X.t view -> bool
+  val hash : X.t view -> int
 end
diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml
index 14c2b163..b9e23d15 100644
--- a/src/smt/Theory_combine.ml
+++ b/src/smt/Theory_combine.ml
@@ -48,9 +48,8 @@ let assume_lit (self:t) (lit:Lit.t) : unit =
   (* check consistency first *)
   begin match Lit.view lit with
     | Lit_fresh _ -> ()
-    | Lit_expanded _
-    | Lit_atom {term_cell=Bool true; _} -> ()
-    | Lit_atom {term_cell=Bool false; _} -> ()
+    | Lit_atom {term_view=Bool true; _} -> ()
+    | Lit_atom {term_view=Bool false; _} -> ()
     | Lit_atom _ ->
       (* transmit to theories. *)
       C_clos.assert_lit (cc self) lit;
@@ -102,7 +101,7 @@ let add_formula (self:t) (lit:Lit.t) =
   | Lit_atom t ->
     let lazy cc = self.cc in
     ignore (C_clos.add cc t : cc_node)
-  | Lit_expanded _ | Lit_fresh _ -> ()
+  | Lit_fresh _ -> ()
 
 (* propagation from the bool solver *)
 let assume (self:t) (slice:_ Sat_solver.slice_actions) =
diff --git a/src/smt/Ty.ml b/src/smt/Ty.ml
index b9d4f1a3..ed991ed5 100644
--- a/src/smt/Ty.ml
+++ b/src/smt/Ty.ml
@@ -2,106 +2,94 @@
 open Solver_types
 
 type t = ty
+type view = Solver_types.ty_view
+type def = Solver_types.ty_def
 
-and cell = Solver_types.ty_cell =
-  | Prop
-  | Atomic of ID.t * ty_def
-  | Arrow of ty * ty
-
-type def = Solver_types.ty_def =
-  | Uninterpreted
-  | Data of datatype
-and datatype = Solver_types.datatype = {
-  data_cstors: data_cstor ID.Map.t lazy_t;
-}
-(* a constructor *)
-and data_cstor = Solver_types.data_cstor = {
-  cstor_ty: ty;
-  cstor_args: ty IArray.t; (* argument types *)
-  cstor_proj: cst IArray.t lazy_t; (* projectors *)
-  cstor_test: cst lazy_t; (* tester *)
-  cstor_cst: cst; (* the cstor itself *)
-  cstor_card: ty_card; (* cardinality of the constructor('s args) *)
-}
-
-
-let view t = t.ty_cell
+let view t = t.ty_view
 
 let equal a b = a.ty_id = b.ty_id
 let compare a b = CCInt.compare a.ty_id b.ty_id
 let hash a = a.ty_id
 
+let equal_def d1 d2 = match d1, d2 with
+  | Ty_uninterpreted id1, Ty_uninterpreted id2 -> ID.equal id1 id2
+  | Ty_def d1, Ty_def d2 -> ID.equal d1.id d2.id
+  | Ty_uninterpreted _, _ | Ty_def _, _
+    -> false
+
 module Tbl_cell = CCHashtbl.Make(struct
-    type t = ty_cell
+    type t = ty_view
     let equal a b = match a, b with
-      | Prop, Prop -> true
-      | Atomic (i1,_), Atomic (i2,_) -> ID.equal i1 i2
-      | Arrow (a1,b1), Arrow (a2,b2) ->
-        equal a1 a2 && equal b1 b2
-      | Prop, _
-      | Atomic _, _
-      | Arrow _, _ -> false
+      | Ty_prop, Ty_prop -> true
+      | Ty_atomic a1, Ty_atomic a2 ->
+        equal_def a1.def a2.def && CCList.equal equal a1.args a2.args
+      | Ty_prop, _ | Ty_atomic _, _
+       -> false
 
     let hash t = match t with
-      | Prop -> 1
-      | Atomic (i,_) -> Hash.combine2 2 (ID.hash i)
-      | Arrow (a,b) -> Hash.combine3 3 (hash a) (hash b)
+      | Ty_prop -> 1
+      | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
+        Hash.combine3 10 (ID.hash id) (Hash.list hash args)
+      | Ty_atomic {def=Ty_def d; args; _} ->
+        Hash.combine3 20 (ID.hash d.id) (Hash.list hash args)
   end)
 
 (* build a type *)
-let make_ : ty_cell -> card:ty_card lazy_t -> t =
+let make_ : ty_view -> t =
   let tbl : t Tbl_cell.t = Tbl_cell.create 128 in
   let n = ref 0 in
-  fun c ~card ->
+  fun c ->
     try Tbl_cell.find tbl c
     with Not_found ->
       let ty_id = !n in
       incr n;
-      let ty = {ty_id; ty_cell=c; ty_card=card; } in
+      let ty = {ty_id; ty_view=c; } in
       Tbl_cell.add tbl c ty;
       ty
 
-let prop = make_ Prop ~card:(Lazy.from_val Finite)
+let card t = match view t with
+  | Ty_prop -> Finite
+  | Ty_atomic {card=lazy c; _} -> c
 
-let atomic id def ~card = make_ (Atomic (id,def)) ~card
+let prop = make_ Ty_prop
 
-let arrow a b =
-  let card = lazy (Ty_card.(Lazy.force b.ty_card ^ Lazy.force a.ty_card)) in
-  make_ (Arrow (a,b)) ~card
+let atomic def args : t =
+  let card = lazy (
+    match def with
+    | Ty_uninterpreted _ ->
+      if List.for_all (fun sub -> card sub = Finite) args then Finite else Infinite
+    | Ty_def d -> d.card args
+  ) in
+  make_ (Ty_atomic {def; args; card})
 
-let arrow_l = List.fold_right arrow
+let atomic_uninterpreted id = atomic (Ty_uninterpreted id) []
 
 let is_prop t =
-  match t.ty_cell with | Prop -> true | _ -> false
-
-let is_data t =
-  match t.ty_cell with | Atomic (_, Data _) -> true | _ -> false
+  match t.ty_view with | Ty_prop -> true | _ -> false
 
 let is_uninterpreted t =
-  match t.ty_cell with | Atomic (_, Uninterpreted) -> true | _ -> false
-
-let is_arrow t =
-  match t.ty_cell with | Arrow _ -> true | _ -> false
-
-let unfold = ty_unfold
-
-let unfold_n ty : int * t =
-  let rec aux n ty = match ty.ty_cell with
-    | Arrow (_,b) -> aux (n+1) b
-    | _ -> n, ty
-  in
-  aux 0 ty
+  match t.ty_view with | Ty_atomic {def=Ty_uninterpreted _; _} -> true | _ -> false
 
 let pp = pp_ty
 
-(* representation as a single identifier *)
-let rec mangle t : string = match t.ty_cell with
-  | Prop -> "prop"
-  | Atomic (id,_) -> ID.to_string id
-  | Arrow (a,b) -> mangle a ^ "_" ^ mangle b
-
 module Tbl = CCHashtbl.Make(struct
     type t = ty
     let equal = equal
     let hash = hash
   end)
+
+module Fun = struct
+  type t = fun_ty
+
+  let[@inline] args f = f.fun_ty_args
+  let[@inline] ret f = f.fun_ty_ret
+  let[@inline] arity f = List.length @@ args f
+  let[@inline] mk args ret : t = {fun_ty_args=args; fun_ty_ret=ret}
+  let[@inline] unfold t = args t, ret t
+
+  let pp out f : unit =
+    match args f with
+    | [] -> pp out (ret f)
+    | args ->
+      Format.fprintf out "(@[(@[%a@])@ %a@])" (Util.pp_list pp) args pp (ret f)
+end
diff --git a/src/smt/Ty.mli b/src/smt/Ty.mli
index 79845285..6ee5413c 100644
--- a/src/smt/Ty.mli
+++ b/src/smt/Ty.mli
@@ -4,44 +4,20 @@
 open Solver_types
 
 type t = Solver_types.ty
+type view = Solver_types.ty_view
+type def = Solver_types.ty_def
 
-type cell = Solver_types.ty_cell =
-  | Prop
-  | Atomic of ID.t * ty_def
-  | Arrow of ty * ty
-
-type def = Solver_types.ty_def =
-  | Uninterpreted
-  | Data of datatype
-and datatype = Solver_types.datatype = {
-  data_cstors: data_cstor ID.Map.t lazy_t;
-}
-(* a constructor *)
-and data_cstor = Solver_types.data_cstor = {
-  cstor_ty: ty;
-  cstor_args: ty IArray.t; (* argument types *)
-  cstor_proj: cst IArray.t lazy_t; (* projectors *)
-  cstor_test: cst lazy_t; (* tester *)
-  cstor_cst: cst; (* the cstor itself *)
-  cstor_card: ty_card; (* cardinality of the constructor('s args) *)
-}
-
-
-val view : t -> cell
+val view : t -> view
 
 val prop : t
-val atomic : ID.t -> def -> card:Ty_card.t lazy_t -> t
-val arrow : t -> t -> t
-val arrow_l : t list -> t -> t
+val atomic : def -> t list -> t
+
+val atomic_uninterpreted : ID.t -> t
+
+val card : t -> ty_card
 
 val is_prop : t -> bool
-val is_data : t -> bool
 val is_uninterpreted : t -> bool
-val is_arrow : t -> bool
-val unfold : t -> t list * t
-val unfold_n : t -> int * t
-
-val mangle : t -> string
 
 include Intf.EQ with type t := t
 include Intf.ORD with type t := t
@@ -50,3 +26,15 @@ include Intf.PRINT with type t := t
 
 module Tbl : CCHashtbl.S with type key = t
 
+module Fun : sig
+  type t = fun_ty
+
+  val args : t -> ty list
+  val ret : t -> ty
+  val arity : t -> int
+  val unfold : t -> ty list * ty
+
+  val mk : ty list -> ty -> t
+
+  include Intf.PRINT with type t := t
+end
diff --git a/src/smt/th_bool/Sidekick_th_bool.ml b/src/smt/th_bool/Sidekick_th_bool.ml
index 2948e6f8..f16fb8a1 100644
--- a/src/smt/th_bool/Sidekick_th_bool.ml
+++ b/src/smt/th_bool/Sidekick_th_bool.ml
@@ -2,6 +2,7 @@
 (** {1 Theory of Booleans} *)
 
 open Sidekick_smt
+open Solver_types
 
 module Fmt = CCFormat
 
@@ -15,228 +16,91 @@ type term = Term.t
 (* TODO: in theory (or terms?) have a way to evaluate custom terms
    (like formulas) in a given model, for checking models *)
 
-type 'a builtin =
-  | B_not of 'a
-  | B_eq of 'a * 'a
-  | B_and of 'a list
-  | B_or of 'a list
-  | B_imply of 'a list * 'a
-  | B_distinct of 'a list
+let id_not = ID.make "not"
+let id_and = ID.make "and"
+let id_or = ID.make "or"
+let id_imply = ID.make "=>"
+let id_eq = ID.make "="
+let id_distinct = ID.make "distinct"
 
-let fold_map_builtin
-    (f:'a -> 't -> 'b * 'u) (acc:'a) (b:'t builtin): 'b * 'u builtin =
-  let fold_binary acc a b =
-    let acc, a = f acc a in
-    let acc, b = f acc b in
-    acc, a, b
-  in
-  match b with
-    | B_not t ->
-      let acc, t' = f acc t in
-      acc, B_not t'
-    | B_and l ->
-      let acc, l = CCList.fold_map f acc l in
-      acc, B_and l
-    | B_or l ->
-      let acc, l = CCList.fold_map f acc l in
-      acc, B_or l
-    | B_eq (a,b) ->
-      let acc, a, b = fold_binary acc a b in
-      acc, B_eq (a, b)
-    | B_distinct l ->
-      let acc, l = CCList.fold_map f acc l in
-      acc, B_distinct l
-    | B_imply (a,b) ->
-      let acc, a = CCList.fold_map f acc a in
-      let acc, b = f acc b in
-      acc, B_imply (a, b)
+module C = struct
 
-let map_builtin f b =
-  let (), b = fold_map_builtin (fun () t -> (), f t) () b in
-  b
+  let get_ty _ = Ty.prop
+  let relevant _ = Sequence.empty (* no congruence closure *)
 
-let builtin_to_seq b yield = match b with
-  | B_not t -> yield t
-  | B_or l | B_and l | B_distinct l -> List.iter yield l
-  | B_imply (a,b) -> List.iter yield a; yield b
-  | B_eq (a,b) -> yield a; yield b
-
-type 'a Term.custom +=
-  | Builtin of {
-      view: 'a builtin;
-      (* TODO: bool value + explanation *)
-      (* TODO: caching of Tseiting *)
-    }
-
-module TC = struct
-  let hash sub_hash = function
-    | Builtin {view; _} ->
-      begin match view with
-        | B_not a -> Hash.combine2 20 (sub_hash a)
-        | B_and l -> Hash.combine2 21 (Hash.list sub_hash l)
-        | B_or l -> Hash.combine2 22 (Hash.list sub_hash l)
-        | B_imply (l1,t2) -> Hash.combine3 23 (Hash.list sub_hash l1) (sub_hash t2)
-        | B_eq (t1,t2) -> Hash.combine3 24 (sub_hash t1) (sub_hash t2)
-        | B_distinct l -> Hash.combine2 26 (Hash.list sub_hash l)
-      end
-    | _ -> assert false
-
-  let eq sub_eq a b = match a, b with
-    | Builtin {view=b1; _}, Builtin {view=b2;_} ->
-      begin match b1, b2 with
-        | B_not a1, B_not a2 -> sub_eq a1 a2
-        | B_and l1, B_and l2
-        | B_or l1, B_or l2 -> CCEqual.list sub_eq l1 l2
-        | B_distinct l1, B_distinct l2 -> CCEqual.list sub_eq l1 l2
-        | B_eq (a1,b1), B_eq (a2,b2) -> sub_eq a1 a2 && sub_eq b1 b2
-        | B_imply (a1,b1), B_imply (a2,b2) -> CCEqual.list sub_eq a1 a2 && sub_eq b1 b2
-        | B_not _, _ | B_and _, _ | B_eq _, _
-        | B_or _, _ | B_imply _, _ | B_distinct _, _
-          -> false
-      end
-    | Builtin _, _
-    | _, Builtin _ -> false
-    | _ -> assert false
-
-  let pp sub_pp out = function
-    | Builtin {view=b;_} ->
-      begin match b with
-        | B_not t -> Fmt.fprintf out "(@[<hv>not@ %a@])" sub_pp t
-        | B_and l ->
-          Fmt.fprintf out "(@[<hv>and@ %a@])" (Util.pp_list sub_pp) l
-        | B_or l ->
-          Fmt.fprintf out "(@[<hv>or@ %a@])" (Util.pp_list sub_pp) l
-        | B_imply (a,b) ->
-          Fmt.fprintf out "(@[<hv1>=>@ %a@ %a@])" (Util.pp_list sub_pp) a sub_pp b
-        | B_eq (a,b) ->
-          Fmt.fprintf out "(@[<hv1>=@ %a@ %a@])" sub_pp a sub_pp b
-        | B_distinct l ->
-          Fmt.fprintf out "(@[<hv1>distinct@ %a@])" (Util.pp_list sub_pp) l
-      end
-    | _ -> assert false
-
-  let get_ty _ = function
-    | Builtin _ -> Ty.prop
-    | _ -> assert false
-
-  (* no Shostak for builtins, everything goes through clauses to
-     the SAT solver *)
-  let is_semantic = function
-    | Builtin {view=_;_} -> false
-    | _ -> assert false
-
-  let solve _ _ = assert false (* never called *)
-
-  let sub = function
-    | Builtin {view;_} -> builtin_to_seq view
-    | _ -> assert false
-
-  let relevant = function
-    | Builtin _ -> Sequence.empty (* no congruence closure *)
-    | _ -> assert false
-
-  let abs ~self = function
-    | Builtin {view=B_not b; _} -> b, false
+  let abs ~self _a =
+    match Term.view self with
+    | App_cst ({cst_id;_}, args) when ID.equal cst_id id_not && IArray.length args=1 ->
+      (* [not a] --> [a, false] *)
+      IArray.get args 0, false
     | _ -> self, true
 
-  let subst _ _ = None (* no congruence *)
+  let mk_cst id : Cst.t =
+    {cst_id=id; cst_view=Cst_def { pp=None; abs; ty=get_ty; relevant; }; }
 
-  let explain _eq _ _ = assert false (* no congruence *)
-
-  let tc : Term_cell.tc = {
-    Term_cell.
-    tc_t_pp = pp;
-    tc_t_equal = eq;
-    tc_t_hash = hash;
-    tc_t_ty = get_ty;
-    tc_t_is_semantic = is_semantic;
-    tc_t_solve = solve;
-    tc_t_sub = sub;
-    tc_t_abs = abs;
-    tc_t_relevant = relevant;
-    tc_t_subst = subst;
-    tc_t_explain = explain
-  }
+  let not = mk_cst id_not
+  let and_ = mk_cst id_and
+  let or_ = mk_cst id_or
+  let imply = mk_cst id_imply
+  let eq = mk_cst id_eq
+  let distinct = mk_cst id_distinct
 end
 
-let tc = TC.tc
+let as_id id (t:Term.t) : Term.t IArray.t option =
+  match Term.view t with
+  | App_cst ({cst_id; _}, args) when ID.equal id cst_id -> Some args
+  | _ -> None
 
-module T_cell = struct
-  type t = Term_cell.t
+(* flatten terms of the given ID *)
+let flatten_id id (l:Term.t list) : Term.t list =
+  CCList.flat_map
+    (fun t -> match as_id id t with
+       | Some args -> IArray.to_list args
+       | None -> [t])
+    l
 
-  let builtin b =
-    let mk_ x = Term_cell.custom ~tc (Builtin {view=x}) in
-    (* normalize a bit *)
-    begin match b with
-      | B_imply ([], x) -> Term.cell x
-      | B_eq (a,b) when Term.equal a b -> Term_cell.true_
-      | B_eq (a,b) when Term.id a > Term.id b -> mk_ @@ B_eq (b,a)
-      | B_and l ->
-        begin try
-            let l = CCList.flat_map
-                (function
-                  | {Term.term_cell=Term.Custom {view=Builtin {view=B_and l';_};_};_} -> l'
-                  | {Term.term_cell=Term.Bool false;_} -> raise Exit
-                  | x->[x])
-                l
-            in
-            mk_ @@ B_and l
-          with Exit -> Term_cell.false_
-        end
-      | B_or l ->
-        begin try
-            let l = CCList.flat_map
-                (function
-                  | {Term.term_cell=Term.Custom {view=Builtin {view=B_or l';_};_};_} -> l'
-                  | {Term.term_cell=Term.Bool true;_} -> raise Exit
-                  | x->[x])
-                l
-            in
-            mk_ @@ B_or l
-          with Exit -> Term_cell.true_
-        end
-      | _ -> mk_ b
-    end
-
-  let not_ t = match Term.cell t with
-    | Term_cell.Custom {view=Builtin {view=B_not t';_};_} -> Term.cell t'
-    | _ -> builtin (B_not t)
-
-  let and_ l = builtin (B_and l)
-  let or_ l = builtin (B_or l)
-  let imply a b = builtin (B_imply (a,b))
-  let eq a b = builtin (B_eq (a,b))
-  let distinct = function
-    | [] | [_] -> Term_cell.true_
-    | l -> builtin (B_distinct l)
-  let neq a b = distinct [a;b]
-end
-
-let make = Term.make
-
-let not_ st t = make st (T_cell.not_ t)
-
-let and_l st = function
+let and_l st l =
+  match flatten_id id_and l with
   | [] -> Term.true_ st
-  | [t] -> t
-  | l -> make st (T_cell.and_ l)
+  | l when List.exists Term.is_false l -> Term.false_ st
+  | [x] -> x
+  | args -> Term.app_cst st C.and_ (IArray.of_list args)
 
-let or_l st = function
+let or_l st l =
+  match flatten_id id_and l with
   | [] -> Term.false_ st
-  | [t] -> t
-  | l -> make st (T_cell.or_ l)
+  | l when List.exists Term.is_true l -> Term.true_ st
+  | [x] -> x
+  | args -> Term.app_cst st C.or_ (IArray.of_list args)
 
 let and_ st a b = and_l st [a;b]
 let or_ st a b = or_l st [a;b]
-let imply st a b = match a, Term.cell b with
-  | [], _ -> b
-  | _::_, Term_cell.Custom {view=Builtin {view=B_imply (a',b')}; _} ->
-    make st (T_cell.imply (CCList.append a a') b')
-  | _ -> make st (T_cell.imply a b)
-let eq st a b = make st (T_cell.eq a b)
-let distinct st l = make st (T_cell.distinct l)
-let neq st a b = make st (T_cell.neq a b)
-let builtin st b = make st (T_cell.builtin b)
+
+let eq st a b =
+  if Term.equal a b then Term.true_ st
+  else (
+    let a,b = if Term.id a > Term.id b then b, a else a, b in
+    Term.app_cst st C.eq (IArray.doubleton a b)
+  )
+
+let not_ st a =
+  match as_id id_not a, Term.view a with
+  | _, Bool false -> Term.true_ st
+  | _, Bool true -> Term.false_ st
+  | Some args, _ ->
+    assert (IArray.length args = 1);
+    IArray.get args 0
+  | None, _ -> Term.app_cst st C.not (IArray.singleton a)
+
+let neq st a b = not_ st @@ eq st a b
+
+let imply st xs y = match xs with
+  | [] -> y
+  | _ -> Term.app_cst st C.imply (IArray.of_list @@ y :: xs)
+
+let distinct st = function
+  | [] | [_] -> Term.true_ st
+  | xs -> Term.app_cst st C.distinct (IArray.of_list xs)
 
 module Lit = struct
   include Lit
@@ -244,15 +108,48 @@ module Lit = struct
   let neq tst a b = Lit.atom ~sign:false (neq tst a b)
 end
 
+type 'a view =
+  | B_not of 'a
+  | B_eq of 'a * 'a
+  | B_and of 'a IArray.t
+  | B_or of 'a IArray.t
+  | B_imply of 'a IArray.t * 'a
+  | B_distinct of 'a IArray.t
+  | B_atom of 'a
+
+let view (t:Term.t) : term view =
+  match Term.view t with
+  | App_cst ({cst_id; _}, args) ->
+    if ID.equal cst_id id_not && IArray.length args=1 then (
+      B_not t
+    ) else if ID.equal cst_id id_eq && IArray.length args=2 then (
+      B_eq (IArray.get args 0, IArray.get args 1)
+    ) else if ID.equal cst_id id_and then (
+      B_and args
+    ) else if ID.equal cst_id id_or then (
+      B_or args
+    ) else if ID.equal cst_id id_imply && IArray.length args >= 2 then (
+      (* conclusion is stored first *)
+      let len = IArray.length args in
+      B_imply (IArray.sub args 1 (len-1), IArray.get args 0)
+    ) else if ID.equal cst_id id_distinct then (
+      B_distinct args
+    ) else (
+      B_atom t
+    )
+  | _ -> B_atom t
+
+
 type t = {
   tst: Term.state;
   acts: Theory.actions;
 }
 
-let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
+let tseitin (self:t) (lit:Lit.t) (lit_t:term) (v:term view) : unit =
   Log.debugf 5 (fun k->k "(@[th_bool.tseitin@ %a@])" Lit.pp lit);
   let (module A) = self.acts in
-  match b with
+  match v with
+  | B_atom _ -> ()
   | B_not _ -> assert false (* normalized *)
   | B_eq (t,u) ->
     if Lit.sign lit then (
@@ -261,6 +158,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
       A.propagate_distinct [t;u] ~neq:lit_t lit
     )
   | B_distinct l ->
+    let l = IArray.to_list l in
     if Lit.sign lit then (
       A.propagate_distinct l ~neq:lit_t lit
     ) else (
@@ -270,24 +168,26 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
   | B_and subs ->
     if Lit.sign lit then (
       (* propagate [lit => subs_i] *)
-      List.iter
+      IArray.iter
         (fun sub ->
            let sublit = Lit.atom sub in
            A.propagate sublit [lit])
         subs
     ) else (
       (* propagate [¬lit => ∨_i ¬ subs_i] *)
+      let subs = IArray.to_list subs in
       let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in
       A.add_local_axiom (IArray.of_list c)
     )
   | B_or subs ->
     if Lit.sign lit then (
       (* propagate [lit => ∨_i subs_i] *)
+      let subs = IArray.to_list subs in
       let c = Lit.neg lit :: List.map (Lit.atom ~sign:true) subs in
       A.add_local_axiom (IArray.of_list c)
     ) else (
       (* propagate [¬lit => ¬subs_i] *)
-      List.iter
+      IArray.iter
         (fun sub ->
            let sublit = Lit.atom ~sign:false sub in
            A.propagate sublit [lit])
@@ -296,13 +196,14 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
   | B_imply (guard,concl) ->
     if Lit.sign lit then (
       (* propagate [lit => ∨_i ¬guard_i ∨ concl] *)
+      let guard = IArray.to_list guard in
       let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in
       A.add_local_axiom (IArray.of_list c)
     ) else (
       (* propagate [¬lit => ¬concl] *)
       A.propagate (Lit.atom ~sign:false concl) [lit];
       (* propagate [¬lit => ∧_i guard_i] *)
-      List.iter
+      IArray.iter
         (fun sub ->
            let sublit = Lit.atom ~sign:true sub in
            A.propagate sublit [lit])
@@ -311,8 +212,11 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit =
 
 let on_assert (self:t) (lit:Lit.t) =
   match Lit.view lit with
-  | Lit.Lit_atom ({ Term.term_cell=Term.Custom{view=Builtin {view=b};_}; _ } as t) ->
-    tseitin self lit t b
+  | Lit.Lit_atom t ->
+    begin match view t with
+      | B_atom _ -> ()
+      | v -> tseitin self lit t v
+    end
   | _ -> ()
 
 let final_check _ _ : unit = ()
diff --git a/src/smt/th_bool/Sidekick_th_bool.mli b/src/smt/th_bool/Sidekick_th_bool.mli
index 64575a92..c0b47de2 100644
--- a/src/smt/th_bool/Sidekick_th_bool.mli
+++ b/src/smt/th_bool/Sidekick_th_bool.mli
@@ -5,30 +5,17 @@ open Sidekick_smt
 
 type term = Term.t
 
-type 'a builtin =
+type 'a view = private
   | B_not of 'a
   | B_eq of 'a * 'a
-  | B_and of 'a list
-  | B_or of 'a list
-  | B_imply of 'a list * 'a
-  | B_distinct of 'a list
+  | B_and of 'a IArray.t
+  | B_or of 'a IArray.t
+  | B_imply of 'a IArray.t * 'a
+  | B_distinct of 'a IArray.t
+  | B_atom of 'a
 
-val map_builtin : ('a -> 'b) -> 'a builtin -> 'b builtin
-val builtin_to_seq : 'a builtin -> 'a Sequence.t
+val view : term -> term view
 
-module T_cell : sig
-  type t = Term_cell.t
-  val builtin : term builtin -> t
-  val and_ : term list -> t
-  val or_ : term list -> t
-  val not_ : term -> t
-  val imply : term list -> term -> t
-  val eq : term -> term -> t
-  val neq : term -> term -> t
-  val distinct : term list -> t
-end
-
-val builtin : Term.state -> term builtin -> term
 val and_ : Term.state -> term -> term -> term
 val or_ : Term.state -> term -> term -> term
 val not_ : Term.state -> term -> term
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 3ea89fba..c9749348 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -27,7 +27,7 @@ end
 
 module Conv = struct
   let conv_ty (ty:A.Ty.t) : Ty.t =
-    let mk_ty id = Ty.atomic id Ty.Uninterpreted ~card:(lazy Ty_card.infinite) in
+    let mk_ty id = Ty.atomic_uninterpreted id in
     (* convert a type *)
     let aux_ty (ty:A.Ty.t) : Ty.t = match ty with
       | A.Ty.Prop -> Ty.prop
@@ -40,6 +40,15 @@ module Conv = struct
     in
     aux_ty ty
 
+  let conv_fun_ty (ty:A.Ty.t) : Ty.Fun.t =
+    let rec aux args ty =
+      match ty with
+      | A.Ty.Arrow (a,b) ->
+        aux (conv_ty a :: args) b
+      | _ -> Ty.Fun.mk (List.rev args) (conv_ty ty)
+    in
+    aux [] ty
+
   let conv_term (tst:Term.state) (t:A.term): Term.t =
     (* polymorphic equality *)
     let mk_eq t u = Form.eq tst t u in (* TODO: use theory of booleans *)
@@ -80,7 +89,6 @@ module Conv = struct
     (* convert term.
        @param subst used to expand let-bindings on the fly *)
     let rec aux (subst:Term.t Subst.t) (t:A.term) : Term.t =
-      let ty = A.ty t |> conv_ty in
       begin match A.term_view t with
         | A.Var v ->
           begin match Subst.find subst v with
@@ -88,13 +96,14 @@ module Conv = struct
             | Some t -> t
           end
         | A.Const id ->
-          mk_const (Cst.make_undef id ty)
+          let ty = conv_fun_ty @@ A.ty t in
+          mk_const (Cst.mk_undef id ty)
         | A.App (f, l) ->
           let l = List.map (aux subst) l in
           begin match A.term_view f with
             | A.Const id ->
               (* TODO: lookup definition of [f] *)
-              mk_app (Cst.make_undef id (A.ty f |> conv_ty)) l
+              mk_app (Cst.mk_undef id (conv_fun_ty @@ A.ty f)) l
             | _ -> Error.errorf "cannot process HO application %a" A.pp_term t
           end
         | A.If (a,b,c) ->
@@ -208,54 +217,6 @@ end
 let conv_ty = Conv.conv_ty
 let conv_term = Conv.conv_term
 
-(** {2 Terms for Dimacs atoms} *)
-module I_atom : sig
-  val mk_t : Term.state -> int -> Term.t
-  val mk_atom : Term.state -> int -> Lit.t
-end = struct
-  open Solver_types
-
-  type _ Term.custom +=
-    | Atom of int (* absolute *)
-
-  let pp _ out = function Atom i -> Fmt.int out i | _ -> assert false
-  let eq _ a b = match a, b with Atom a, Atom b -> a = b | _ -> false
-  let hash _ = function Atom i -> CCHash.int i | _ -> 0
-  let get_ty _ _ = Ty.prop
-  let is_semantic _ = false
-  let solve a b = match a, b with
-    | Atom a, Atom b when a=b -> Solve_ok {subst=[]}
-    | _ -> assert false
-  let sub _ _ = ()
-  let abs ~self _ = self, true
-  let relevant _ _ = ()
-  let subst _ _ : _ option = None
-  let explain _ _ _ = []
-
-  let tc : Term_cell.tc = {
-    Term_cell.
-    tc_t_pp = pp;
-    tc_t_equal = eq;
-    tc_t_hash = hash;
-    tc_t_ty = get_ty;
-    tc_t_is_semantic = is_semantic;
-    tc_t_solve = solve;
-    tc_t_sub = sub;
-    tc_t_abs = abs;
-    tc_t_relevant = relevant;
-    tc_t_subst = subst;
-    tc_t_explain = explain
-  }
-
-  let[@inline] mk_t tst i =
-    assert (i>=0);
-    Term.custom tst ~tc (Atom i)
-
-  let[@inline] mk_atom tst i =
-    let a = mk_t tst (Pervasives.abs i) in
-    Lit.atom ~sign:(i>0) a
-end
-
 (* call the solver to check-sat *)
 let solve
     ?gc:_
@@ -299,6 +260,15 @@ let solve
       Format.printf "Unknown (:reason %a)" Solver.pp_unknown reas
   end
 
+(* NOTE: hack for testing with dimacs. Proper treatment should go into
+   scoping in Ast, or having theory-specific state in `Term.state` *)
+let mk_iatom =
+  let tbl = Util.Int_tbl.create 6 in (* for atoms *)
+  fun tst i ->
+    let c = Util.Int_tbl.get_or_add tbl ~k:(abs i) 
+        ~f:(fun i -> Cst.mk_undef_const (ID.makef "a_%d" i) Ty.prop) in
+    Lit.atom ~sign:(i>0) @@ Term.const tst c
+
 (* process a single statement *)
 let process_stmt
     ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_model ?check
@@ -354,7 +324,7 @@ let process_stmt
       Solver.assume solver (IArray.singleton (Lit.atom t));
       E.return()
     | A.Assert_bool l ->
-      let c = List.rev_map (I_atom.mk_atom tst) l in
+      let c = List.rev_map (mk_iatom tst) l in
       Solver.assume solver (IArray.of_list c);
       E.return ()
     | A.Goal (_, _) ->
diff --git a/src/util/IArray.ml b/src/util/IArray.ml
index 74f882d0..48c650df 100644
--- a/src/util/IArray.ml
+++ b/src/util/IArray.ml
@@ -17,6 +17,8 @@ let make n x = Array.make n x
 
 let init n f = Array.init n f
 
+let sub = Array.sub
+
 let get = Array.get
 
 let unsafe_get = Array.unsafe_get
diff --git a/src/util/IArray.mli b/src/util/IArray.mli
index c86bb785..f3e8f219 100644
--- a/src/util/IArray.mli
+++ b/src/util/IArray.mli
@@ -1,7 +1,7 @@
 
 (* This file is free software. See file "license" for more details. *)
 
-type 'a t
+type 'a t = private 'a array
 (** Array of values of type 'a. The underlying type really is
     an array, but it will never be modified.
 
@@ -13,6 +13,8 @@ val is_empty : _ t  -> bool
 
 val length : _ t -> int
 
+val sub : 'a t -> int -> int -> 'a t
+
 val singleton : 'a -> 'a t
 
 val doubleton : 'a -> 'a -> 'a t
diff --git a/src/util/Util.ml b/src/util/Util.ml
index f596a6db..4819fe40 100644
--- a/src/util/Util.ml
+++ b/src/util/Util.ml
@@ -24,6 +24,9 @@ let pp_array ?(sep=" ") pp out l =
 let pp_iarray ?(sep=" ") pp out a =
   Fmt.seq ~sep:(pp_sep sep) pp out (IArray.to_seq a)
 
+let flat_map_l_ia f l =
+  CCList.flat_map (fun x -> IArray.to_list @@ f x) l
+
 let setup_gc () =
   let g = Gc.get () in
   g.Gc.space_overhead <- 3_000; (* major gc *)
diff --git a/src/util/Util.mli b/src/util/Util.mli
index 66826a75..364a5753 100644
--- a/src/util/Util.mli
+++ b/src/util/Util.mli
@@ -15,8 +15,11 @@ val pp_pair : ?sep:string -> 'a printer -> 'b printer -> ('a * 'b) printer
 
 val pp_iarray : ?sep:string -> 'a CCFormat.printer -> 'a IArray.t CCFormat.printer
 
+val flat_map_l_ia : ('a -> 'b IArray.t) -> 'a list -> 'b list
+
 val setup_gc : unit -> unit
 (** Change parameters of the GC *)
 
 module Int_set : CCSet.S with type elt = int
 module Int_map : CCMap.S with type key = int
+module Int_tbl : CCHashtbl.S with type key = int