diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml
index efd3852b..476a2450 100644
--- a/src/base/Base_types.ml
+++ b/src/base/Base_types.ml
@@ -1,17 +1,19 @@
 (** Basic type definitions for Sidekick_base *)
 
-module Vec = Sidekick_util.Vec
-module Log = Sidekick_util.Log
-module Fmt = CCFormat
-module CC_view = Sidekick_sigs_cc.View
-module Proof_ser = Sidekick_base_proof_trace.Proof_ser
-module Storage = Sidekick_base_proof_trace.Storage
+(*
+
+open Sidekick_core
+module CC_view = Sidekick_cc.View
+(* FIXME
+   module Proof_ser = Sidekick_base_proof_trace.Proof_ser
+   module Storage = Sidekick_base_proof_trace.Storage
+*)
 
 let hash_z = Z.hash
 let[@inline] hash_q q = CCHash.combine2 (hash_z (Q.num q)) (hash_z (Q.den q))
 
 module LRA_pred = struct
-  type t = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
+  type t = Sidekick_th_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
 
   let to_string = function
     | Lt -> "<"
@@ -25,7 +27,7 @@ module LRA_pred = struct
 end
 
 module LRA_op = struct
-  type t = Sidekick_arith_lra.op = Plus | Minus
+  type t = Sidekick_th_lra.op = Plus | Minus
 
   let to_string = function
     | Plus -> "+"
@@ -154,34 +156,12 @@ module LIA_view = struct
     | Var v -> LRA_view.Var (f v)
 end
 
-type term = {
-  mutable term_id: int; (* unique ID *)
-  mutable term_ty: ty;
-  term_view: term term_view;
-}
-(** Term.
+type term = Term.t
+type ty = Term.t
+type value = Term.t
 
-    A term, with its own view, type, and a unique identifier.
-    Do not create directly, see {!Term}. *)
-
-(** Shallow structure of a term.
-
-    A term is a DAG (direct acyclic graph) of nodes, each of which has a
-    term view. *)
-and 'a term_view =
-  | Bool of bool
-  | App_fun of fun_ * 'a array (* full, first-order application *)
-  | Eq of 'a * 'a
-  | Not of 'a
-  | Ite of 'a * 'a * 'a
-  | LRA of 'a LRA_view.t
-  | LIA of 'a LIA_view.t
-
-and fun_ = { fun_id: ID.t; fun_view: fun_view }
-(** type of function symbols *)
-
-and fun_view =
-  | Fun_undef of fun_ty (* simple undefined constant *)
+type fun_view =
+  | Fun_undef of ty (* simple undefined constant *)
   | Fun_select of select
   | Fun_cstor of cstor
   | Fun_is_a of cstor
@@ -202,19 +182,9 @@ and fun_view =
       congruence but not for evaluation.
 *)
 
-and fun_ty = { fun_ty_args: ty list; fun_ty_ret: ty }
-(** Function type *)
-
-and ty = { mutable ty_id: int; ty_view: ty_view }
-(** Hashconsed type *)
-
 and ty_view =
-  | Ty_bool
-  | Ty_real
   | Ty_int
-  | Ty_atomic of { def: ty_def; args: ty list; mutable finite: bool }
-
-and ty_def =
+  | Ty_real
   | Ty_uninterpreted of ID.t
   | Ty_data of { data: data }
   | Ty_def of {
@@ -245,21 +215,22 @@ and select = {
   select_i: int;
 }
 
-(** Semantic values, used for models (and possibly model-constructing calculi) *)
-and value =
-  | V_bool of bool
-  | V_element of { id: ID.t; ty: ty }
-      (** a named constant, distinct from any other constant *)
-  | V_cstor of { c: cstor; args: value list }
-  | V_custom of {
-      view: value_custom_view;
-      pp: value_custom_view Fmt.printer;
-      eq: value_custom_view -> value_custom_view -> bool;
-      hash: value_custom_view -> int;
-    }  (** Custom value *)
-  | V_real of Q.t
+(* FIXME: just use  terms; introduce a Const.view for V_element
+   (** Semantic values, used for models (and possibly model-constructing calculi) *)
+   type value_view =
+     | V_element of { id: ID.t; ty: ty }
+         (** a named constant, distinct from any other constant *)
+     | V_cstor of { c: cstor; args: value list }
+     | V_custom of {
+         view: value_custom_view;
+         pp: value_custom_view Fmt.printer;
+         eq: value_custom_view -> value_custom_view -> bool;
+         hash: value_custom_view -> int;
+       }  (** Custom value *)
+     | V_real of Q.t
 
-and value_custom_view = ..
+   and value_custom_view = ..
+*)
 
 type definition = ID.t * ty * term
 
@@ -278,15 +249,50 @@ type statement =
   | Stmt_get_value of term list
   | Stmt_exit
 
-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
-let fun_compare a b = ID.compare a.fun_id b.fun_id
-let pp_fun out a = ID.pp out a.fun_id
-let id_of_fun a = a.fun_id
-let[@inline] eq_ty a b = a.ty_id = b.ty_id
-let eq_cstor c1 c2 = ID.equal c1.cstor_id c2.cstor_id
+type Const.view += Ty of ty_view
 
+let ops_ty : Const.ops =
+  (module struct
+    let pp out = function
+      | Ty ty ->
+        (match ty with
+        | Ty_real -> Fmt.string out "Real"
+        | Ty_int -> Fmt.string out "Int"
+        | 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
+        | Ty_atomic { def = Ty_data d; args = []; _ } ->
+          ID.pp out d.data.data_id
+        | Ty_atomic { def = Ty_data d; args; _ } ->
+          Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data.data_id
+            (Util.pp_list pp_ty) args)
+      | _ -> ()
+
+    let equal a b =
+      match a, b with
+      | Ty a, Ty b ->
+        (match a, b with
+        | Ty_bool, Ty_bool | Ty_int, Ty_int | Ty_real, Ty_real -> true
+        | Ty_atomic a1, Ty_atomic a2 ->
+          equal_def a1.def a2.def && CCList.equal equal a1.args a2.args
+        | (Ty_bool | Ty_atomic _ | Ty_real | Ty_int), _ -> false)
+      | _ -> false
+
+    let hash t =
+      match t.ty_view with
+      | Ty_bool -> Hash.int 1
+      | Ty_real -> Hash.int 2
+      | Ty_int -> Hash.int 3
+      | 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)
+      | Ty_atomic { def = Ty_data d; args; _ } ->
+        Hash.combine3 30 (ID.hash d.data.data_id) (Hash.list hash args)
+  end)
+
+(*
 let rec eq_value a b =
   match a, b with
   | V_bool a, V_bool b -> a = b
@@ -314,22 +320,7 @@ let rec pp_value out = function
   | V_cstor { c; args } ->
     Fmt.fprintf out "(@[%a@ %a@])" ID.pp c.cstor_id (Util.pp_list pp_value) args
   | V_real x -> Q.pp_print out x
-
-let pp_db out (i, _) = Format.fprintf out "%%%d" i
-
-let rec pp_ty out t =
-  match t.ty_view with
-  | Ty_bool -> Fmt.string out "Bool"
-  | Ty_real -> Fmt.string out "Real"
-  | Ty_int -> Fmt.string out "Int"
-  | 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
-  | Ty_atomic { def = Ty_data d; args = []; _ } -> ID.pp out d.data.data_id
-  | Ty_atomic { def = Ty_data d; args; _ } ->
-    Fmt.fprintf out "(@[%a@ %a@])" ID.pp d.data.data_id (Util.pp_list pp_ty)
-      args
+  *)
 
 let pp_term_view_gen ~pp_id ~pp_t out = function
   | Bool true -> Fmt.string out "true"
@@ -1396,3 +1387,5 @@ module Statement = struct
     | Stmt_define _ -> assert false
   (* TODO *)
 end
+
+*)
diff --git a/src/base/Config.ml b/src/base/Config.ml
index 63afe4eb..f82120c5 100644
--- a/src/base/Config.ml
+++ b/src/base/Config.ml
@@ -2,8 +2,8 @@
 
 type 'a sequence = ('a -> unit) -> unit
 
-module Key = CCHet.Key
+module Key = Het.Key
 
-type pair = CCHet.pair = Pair : 'a Key.t * 'a -> pair
+type pair = Het.pair = Pair : 'a Key.t * 'a -> pair
 
-include CCHet.Map
+include Het.Map
diff --git a/src/base/Config.mli b/src/base/Config.mli
index 5adda152..2c7f51c3 100644
--- a/src/base/Config.mli
+++ b/src/base/Config.mli
@@ -1,4 +1,4 @@
-(** {1 Configuration} *)
+(** Configuration *)
 
 type 'a sequence = ('a -> unit) -> unit
 
diff --git a/src/base/Form.ml b/src/base/Form.ml
index 45cb908a..bb6794ab 100644
--- a/src/base/Form.ml
+++ b/src/base/Form.ml
@@ -1,3 +1,5 @@
+(*
+
 (** Formulas (boolean terms).
 
     This module defines function symbols, constants, and views
@@ -202,3 +204,5 @@ module Gensym = struct
     let id = ID.make name in
     T.const self.tst @@ Fun.mk_undef_const id ty
 end
+
+*)
diff --git a/src/base/Hashcons.ml b/src/base/Hashcons.ml
deleted file mode 100644
index 28ca6e21..00000000
--- a/src/base/Hashcons.ml
+++ /dev/null
@@ -1,34 +0,0 @@
-module type ARG = sig
-  type t
-
-  val equal : t -> t -> bool
-  val hash : t -> int
-  val set_id : t -> int -> unit
-end
-
-module Make (A : ARG) : sig
-  type t
-
-  val create : ?size:int -> unit -> t
-  val hashcons : t -> A.t -> A.t
-  val size : t -> int
-  val to_iter : t -> A.t Iter.t
-end = struct
-  module W = Weak.Make (A)
-
-  type t = { tbl: W.t; mutable n: int }
-
-  let create ?(size = 1024) () : t = { tbl = W.create size; n = 0 }
-
-  (* hashcons terms *)
-  let hashcons st t =
-    let t' = W.merge st.tbl t in
-    if t == t' then (
-      st.n <- 1 + st.n;
-      A.set_id t' st.n
-    );
-    t'
-
-  let size st = W.count st.tbl
-  let to_iter st yield = W.iter yield st.tbl
-end
diff --git a/src/base/CCHet.ml b/src/base/Het.ml
similarity index 71%
rename from src/base/CCHet.ml
rename to src/base/Het.ml
index 52c748e8..5404ca76 100644
--- a/src/base/CCHet.ml
+++ b/src/base/Het.ml
@@ -74,58 +74,6 @@ let pair_of_e_pair (E_pair (k, e)) =
   | K.Store v -> Pair (k, v)
   | _ -> assert false
 
-module Tbl = struct
-  module M = Hashtbl.Make (struct
-    type t = int
-
-    let equal (i : int) j = i = j
-    let hash (i : int) = Hashtbl.hash i
-  end)
-
-  type t = exn_pair M.t
-
-  let create ?(size = 16) () = M.create size
-  let mem t k = M.mem t (Key.id k)
-
-  let find_exn (type a) t (k : a Key.t) : a =
-    let module K = (val k) in
-    let (E_pair (_, v)) = M.find t K.id in
-    match v with
-    | K.Store v -> v
-    | _ -> assert false
-
-  let find t k = try Some (find_exn t k) with Not_found -> None
-
-  let add_pair_ t p =
-    let (Pair (k, v)) = p in
-    let module K = (val k) in
-    let p = E_pair (k, K.Store v) in
-    M.replace t K.id p
-
-  let add t k v = add_pair_ t (Pair (k, v))
-
-  let remove (type a) t (k : a Key.t) =
-    let module K = (val k) in
-    M.remove t K.id
-
-  let length t = M.length t
-  let iter f t = M.iter (fun _ pair -> f (pair_of_e_pair pair)) t
-  let to_iter t yield = iter yield t
-  let to_list t = M.fold (fun _ p l -> pair_of_e_pair p :: l) t []
-  let add_list t l = List.iter (add_pair_ t) l
-  let add_iter t seq = seq (add_pair_ t)
-
-  let of_list l =
-    let t = create () in
-    add_list t l;
-    t
-
-  let of_iter seq =
-    let t = create () in
-    add_iter t seq;
-    t
-end
-
 module Map = struct
   module M = Map.Make (struct
     type t = int
diff --git a/src/base/CCHet.mli b/src/base/Het.mli
similarity index 58%
rename from src/base/CCHet.mli
rename to src/base/Het.mli
index e98271ad..196e251d 100644
--- a/src/base/CCHet.mli
+++ b/src/base/Het.mli
@@ -1,5 +1,3 @@
-(* This file is free software, part of containers. See file "license" for more details. *)
-
 (** {1 Associative containers with Heterogeneous Values}
 
     This is similar to {!CCMixtbl}, but the injection is directly used as
@@ -21,29 +19,6 @@ end
 
 type pair = Pair : 'a Key.t * 'a -> pair
 
-(** {2 Imperative table indexed by [Key]} *)
-module Tbl : sig
-  type t
-
-  val create : ?size:int -> unit -> t
-  val mem : t -> _ Key.t -> bool
-  val add : t -> 'a Key.t -> 'a -> unit
-  val remove : t -> _ Key.t -> unit
-  val length : t -> int
-  val find : t -> 'a Key.t -> 'a option
-
-  val find_exn : t -> 'a Key.t -> 'a
-  (** @raise Not_found if the key is not in the table. *)
-
-  val iter : (pair -> unit) -> t -> unit
-  val to_iter : t -> pair iter
-  val of_iter : pair iter -> t
-  val add_iter : t -> pair iter -> unit
-  val add_list : t -> pair list -> unit
-  val of_list : pair list -> t
-  val to_list : t -> pair list
-end
-
 (** {2 Immutable map} *)
 module Map : sig
   type t
diff --git a/src/base/ID.ml b/src/base/ID.ml
index 90c761d5..a1e5f808 100644
--- a/src/base/ID.ml
+++ b/src/base/ID.ml
@@ -21,8 +21,7 @@ let pp_name out a = CCFormat.string out a.name
 let to_string_full a = Printf.sprintf "%s/%d" a.name a.id
 
 module AsKey = struct
-  type t_ = t
-  type t = t_
+  type nonrec t = t
 
   let equal = equal
   let compare = compare
diff --git a/src/base/Lit.ml b/src/base/Lit.ml
deleted file mode 100644
index 42b275a1..00000000
--- a/src/base/Lit.ml
+++ /dev/null
@@ -1 +0,0 @@
-include Sidekick_lit.Make (Solver_arg)
diff --git a/src/base/Lit.mli b/src/base/Lit.mli
deleted file mode 100644
index aa24343c..00000000
--- a/src/base/Lit.mli
+++ /dev/null
@@ -1 +0,0 @@
-include Sidekick_core.LIT with module T = Solver_arg
diff --git a/src/base/Model.ml b/src/base/Model.ml
deleted file mode 100644
index 21c53d05..00000000
--- a/src/base/Model.ml
+++ /dev/null
@@ -1,246 +0,0 @@
-(* This file is free software. See file "license" for more details. *)
-
-open! Base_types
-
-module Val_map = struct
-  module M = CCMap.Make (CCInt)
-
-  module Key = struct
-    type t = Value.t list
-
-    let equal = CCList.equal Value.equal
-    let hash = Hash.list Value.hash
-  end
-
-  type key = Key.t
-  type 'a t = (key * 'a) list M.t
-
-  let empty = M.empty
-  let is_empty m = M.cardinal m = 0
-  let cardinal = M.cardinal
-
-  let find k m =
-    try Some (CCList.assoc ~eq:Key.equal k @@ M.find (Key.hash k) m)
-    with Not_found -> None
-
-  let add k v m =
-    let h = Key.hash k in
-    let l = M.get_or ~default:[] h m in
-    let l = CCList.Assoc.set ~eq:Key.equal k v l in
-    M.add h l m
-
-  let to_iter m yield = M.iter (fun _ l -> List.iter yield l) m
-end
-
-module Fun_interpretation = struct
-  type t = { cases: Value.t Val_map.t; default: Value.t }
-
-  let default fi = fi.default
-  let cases_list fi = Val_map.to_iter fi.cases |> Iter.to_rev_list
-
-  let make ~default l : t =
-    let m =
-      List.fold_left (fun m (k, v) -> Val_map.add k v m) Val_map.empty l
-    in
-    { cases = m; default }
-end
-
-type t = { values: Value.t Term.Map.t; funs: Fun_interpretation.t Fun.Map.t }
-
-let empty : t = { values = Term.Map.empty; funs = Fun.Map.empty }
-
-(* FIXME: ues this to allocate a default value for each sort
-    (* get or make a default value for this type *)
-    let rec get_ty_default (ty:Ty.t) : Value.t =
-      match Ty.view ty with
-      | Ty_prop -> Value.true_
-      | Ty_atomic { def = Ty_uninterpreted _;_} ->
-        (* domain element *)
-        Ty_tbl.get_or_add ty_tbl ~k:ty
-          ~f:(fun ty -> Value.mk_elt (ID.makef "ty_%d" @@ Ty.id ty) ty)
-      | Ty_atomic { def = Ty_def d; args; _} ->
-        (* ask the theory for a default value *)
-        Ty_tbl.get_or_add ty_tbl ~k:ty
-          ~f:(fun _ty ->
-            let vals = List.map get_ty_default args in
-            d.default_val vals)
-    in
-*)
-
-let[@inline] mem t m = Term.Map.mem t m.values
-let[@inline] find t m = Term.Map.get t m.values
-
-let add t v m : t =
-  match Term.Map.find t m.values with
-  | v' ->
-    if not @@ Value.equal v v' then
-      Error.errorf
-        "@[Model: incompatible values for term %a@ :previous %a@ :new %a@]"
-        Term.pp t Value.pp v Value.pp v';
-    m
-  | exception Not_found -> { m with values = Term.Map.add t v m.values }
-
-let add_fun c v m : t =
-  match Fun.Map.find c m.funs with
-  | _ ->
-    Error.errorf "@[Model: function %a already has an interpretation@]" Fun.pp c
-  | exception Not_found -> { m with funs = Fun.Map.add c v m.funs }
-
-(* merge two models *)
-let merge m1 m2 : t =
-  let values =
-    Term.Map.merge_safe m1.values m2.values ~f:(fun t o ->
-        match o with
-        | `Left v | `Right v -> Some v
-        | `Both (v1, v2) ->
-          if Value.equal v1 v2 then
-            Some v1
-          else
-            Error.errorf
-              "@[Model: incompatible values for term %a@ :previous %a@ :new \
-               %a@]"
-              Term.pp t Value.pp v1 Value.pp v2)
-  and funs =
-    Fun.Map.merge_safe m1.funs m2.funs ~f:(fun c o ->
-        match o with
-        | `Left v | `Right v -> Some v
-        | `Both _ ->
-          Error.errorf "cannot merge the two interpretations of function %a"
-            Fun.pp c)
-  in
-  { values; funs }
-
-let add_funs fs m : t = merge { values = Term.Map.empty; funs = fs } m
-
-let pp out { values; funs } =
-  let module FI = Fun_interpretation in
-  let pp_tv out (t, v) =
-    Fmt.fprintf out "(@[%a@ := %a@])" Term.pp t Value.pp v
-  in
-  let pp_fun_entry out (vals, ret) =
-    Format.fprintf out "(@[%a@ := %a@])" (Fmt.Dump.list Value.pp) vals Value.pp
-      ret
-  in
-  let pp_fun out ((c, fi) : Fun.t * FI.t) =
-    Format.fprintf out "(@[<hov>%a :default %a@ %a@])" Fun.pp c Value.pp
-      fi.FI.default
-      (Fmt.list ~sep:(Fmt.return "@ ") pp_fun_entry)
-      (FI.cases_list fi)
-  in
-  Fmt.fprintf out "(@[model@ @[:terms (@[<hv>%a@])@]@ @[:funs (@[<hv>%a@])@]@])"
-    (Fmt.iter ~sep:Fmt.(return "@ ") pp_tv)
-    (Term.Map.to_iter values)
-    (Fmt.iter ~sep:Fmt.(return "@ ") pp_fun)
-    (Fun.Map.to_iter funs)
-
-exception No_value
-
-let eval (m : t) (t : Term.t) : Value.t option =
-  let module FI = Fun_interpretation in
-  let rec aux t =
-    match Term.view t with
-    | Bool b -> Value.bool b
-    | Not a ->
-      (match aux a with
-      | V_bool b -> V_bool (not b)
-      | v ->
-        Error.errorf "@[Model: wrong value@ for boolean %a@ :val %a@]" Term.pp a
-          Value.pp v)
-    | Ite (a, b, c) ->
-      (match aux a with
-      | V_bool true -> aux b
-      | V_bool false -> aux c
-      | v ->
-        Error.errorf "@[Model: wrong value@ for boolean %a@ :val %a@]" Term.pp a
-          Value.pp v)
-    | Eq (a, b) ->
-      let a = aux a in
-      let b = aux b in
-      if Value.equal a b then
-        Value.true_
-      else
-        Value.false_
-    | LRA _l ->
-      assert false
-      (* TODO: evaluation
-         begin match l with
-           | LRA_pred (p, a, b) ->
-           | LRA_op (_, _, _)|LRA_const _|LRA_other _ -> assert false
-         end
-      *)
-    | LIA _l -> assert false (* TODO *)
-    | App_fun (c, args) ->
-      (match Fun.view c, (args : _ array :> _ array) with
-      | Fun_def udef, _ ->
-        (* use builtin interpretation function *)
-        let args = CCArray.map aux args in
-        udef.eval args
-      | Fun_cstor c, _ -> Value.cstor_app c (Util.array_to_list_map aux args)
-      | Fun_select s, [| u |] ->
-        (match aux u with
-        | V_cstor { c; args } when Cstor.equal c s.select_cstor ->
-          List.nth args s.select_i
-        | v_u ->
-          Error.errorf "cannot eval selector %a@ on %a" Term.pp t Value.pp v_u)
-      | Fun_is_a c1, [| u |] ->
-        (match aux u with
-        | V_cstor { c = c2; args = _ } -> Value.bool (Cstor.equal c1 c2)
-        | v_u ->
-          Error.errorf "cannot eval is-a %a@ on %a" Term.pp t Value.pp v_u)
-      | Fun_select _, _ -> Error.errorf "bad selector term %a" Term.pp t
-      | Fun_is_a _, _ -> Error.errorf "bad is-a term %a" Term.pp t
-      | Fun_undef _, _ ->
-        (try Term.Map.find t m.values
-         with Not_found ->
-           (match Fun.Map.find c m.funs with
-           | fi ->
-             let args = CCArray.map aux args |> CCArray.to_list in
-             (match Val_map.find args fi.FI.cases with
-             | None -> fi.FI.default
-             | Some v -> v)
-           | exception Not_found ->
-             raise No_value (* no particular interpretation *))))
-  in
-  try Some (aux t) with No_value -> None
-
-(* TODO: get model from each theory, then complete it as follows based on types
-   let mk_model (cc:t) (m:A.Model.t) : A.Model.t =
-     let module Model = A.Model in
-     let module Value = A.Value in
-     Log.debugf 15 (fun k->k "(@[cc.mk-model@ %a@])" pp_full cc);
-     let t_tbl = N_tbl.create 32 in
-     (* populate [repr -> value] table *)
-     T_tbl.values cc.tbl
-       (fun r ->
-          if N.is_root r then (
-            (* find a value in the class, if any *)
-            let v =
-              N.iter_class r
-              |> Iter.find_map (fun n -> Model.eval m n.n_term)
-            in
-            let v = match v with
-              | Some v -> v
-              | None ->
-                if same_class r (true_ cc) then Value.true_
-                else if same_class r (false_ cc) then Value.false_
-                else Value.fresh r.n_term
-            in
-            N_tbl.add t_tbl r v
-          ));
-     (* now map every term to its representative's value *)
-     let pairs =
-       T_tbl.values cc.tbl
-       |> Iter.map
-         (fun n ->
-            let r = find_ n in
-            let v =
-              try N_tbl.find t_tbl r
-              with Not_found ->
-                Error.errorf "didn't allocate a value for repr %a" N.pp r
-            in
-            n.n_term, v)
-     in
-     let m = Iter.fold (fun m (t,v) -> Model.add t v m) m pairs in
-     Log.debugf 5 (fun k->k "(@[cc.model@ %a@])" Model.pp m);
-     m
-*)
diff --git a/src/base/Model.mli b/src/base/Model.mli
deleted file mode 100644
index c87c8b64..00000000
--- a/src/base/Model.mli
+++ /dev/null
@@ -1,56 +0,0 @@
-(* This file is free software. See file "license" for more details. *)
-
-(** Models
-
-    A model is a solution to the satisfiability question, created by the
-    SMT solver when it proves the formula to be {b satisfiable}.
-
-    A model gives a value to each term of the original formula(s), in
-    such a way that  the formula(s) is true when the term is replaced by its
-    value.
-*)
-
-open Base_types
-
-module Val_map : sig
-  type key = Value.t list
-  type 'a t
-
-  val empty : 'a t
-  val is_empty : _ t -> bool
-  val cardinal : _ t -> int
-  val find : key -> 'a t -> 'a option
-  val add : key -> 'a -> 'a t -> 'a t
-end
-
-(** Model for function symbols.
-
-    Function models are a finite map from argument tuples to values,
-    accompanied with a default value that every other argument tuples
-    map to. In other words, it's of the form:
-
-    [lambda x y. if (x=vx1,y=vy1) then v1 else if … then … else vdefault]
-*)
-module Fun_interpretation : sig
-  type t = { cases: Value.t Val_map.t; default: Value.t }
-
-  val default : t -> Value.t
-  val cases_list : t -> (Value.t list * Value.t) list
-  val make : default:Value.t -> (Value.t list * Value.t) list -> t
-end
-
-type t = { values: Value.t Term.Map.t; funs: Fun_interpretation.t Fun.Map.t }
-(** Model *)
-
-val empty : t
-(** Empty model *)
-
-val add : Term.t -> Value.t -> t -> t
-val mem : Term.t -> t -> bool
-val find : Term.t -> t -> Value.t option
-val merge : t -> t -> t
-val pp : t CCFormat.printer
-
-val eval : t -> Term.t -> Value.t option
-(** [eval m t] tries to evaluate term [t] in the model.
-    If it succeeds, the value is returned, otherwise [None] is. *)
diff --git a/src/base/Proof_dummy.ml b/src/base/Proof_dummy.ml
deleted file mode 100644
index af268417..00000000
--- a/src/base/Proof_dummy.ml
+++ /dev/null
@@ -1,76 +0,0 @@
-open Base_types
-
-type lit = Lit.t
-type term = Term.t
-
-module Arg = struct
-  type nonrec rule = unit
-  type nonrec step_id = unit
-
-  module Step_vec = Vec_unit
-
-  let dummy_step_id = ()
-end
-
-include Sidekick_proof_trace_dummy.Make (Arg)
-
-type rule = A.rule
-type step_id = A.step_id
-
-let create () : t = ()
-let with_proof _ _ = ()
-
-module Rule_sat = struct
-  type nonrec rule = rule
-  type nonrec step_id = step_id
-  type nonrec lit = lit
-
-  let sat_redundant_clause _ ~hyps:_ = ()
-  let sat_input_clause _ = ()
-  let sat_unsat_core _ = ()
-end
-
-module Rule_core = struct
-  type nonrec rule = rule
-  type nonrec step_id = step_id
-  type nonrec lit = lit
-  type nonrec term = term
-
-  let define_term _ _ = ()
-  let proof_p1 _ _ = ()
-  let proof_r1 _ _ = ()
-  let proof_res ~pivot:_ _ _ = ()
-  let lemma_preprocess _ _ ~using:_ = ()
-  let lemma_true _ = ()
-  let lemma_cc _ = ()
-  let lemma_rw_clause _ ~res:_ ~using:_ = ()
-  let with_defs _ _ = ()
-end
-
-let lemma_lra _ = ()
-
-module Rule_bool = struct
-  type nonrec rule = rule
-  type nonrec lit = lit
-
-  let lemma_bool_tauto _ = ()
-  let lemma_bool_c _ _ = ()
-  let lemma_bool_equiv _ _ = ()
-  let lemma_ite_true ~ite:_ = ()
-  let lemma_ite_false ~ite:_ = ()
-end
-
-module Rule_data = struct
-  type nonrec rule = rule
-  type nonrec lit = lit
-  type nonrec term = term
-
-  let lemma_isa_cstor ~cstor_t:_ _ = ()
-  let lemma_select_cstor ~cstor_t:_ _ = ()
-  let lemma_isa_split _ _ = ()
-  let lemma_isa_sel _ = ()
-  let lemma_isa_disj _ _ = ()
-  let lemma_cstor_inj _ _ _ = ()
-  let lemma_cstor_distinct _ _ = ()
-  let lemma_acyclicity _ = ()
-end
diff --git a/src/base/Proof_dummy.mli b/src/base/Proof_dummy.mli
deleted file mode 100644
index 3aca187e..00000000
--- a/src/base/Proof_dummy.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(** Dummy proof module that does nothing. *)
-
-open Base_types
-
-module Arg :
-  Sidekick_sigs_proof_trace.ARG with type rule = unit and type step_id = unit
-
-include Sidekick_sigs_proof_trace.S with module A = Arg
-
-type rule = A.rule
-type step_id = A.step_id
-
-module Rule_sat :
-  Sidekick_sigs_proof_sat.S with type rule = rule and type lit = Lit.t
-
-module Rule_core :
-  Sidekick_core.PROOF_CORE
-    with type rule = rule
-     and type lit = Lit.t
-     and type term = Term.t
-
-val create : unit -> t
-val lemma_lra : Lit.t Iter.t -> rule
-
-module Rule_data :
-  Sidekick_th_data.PROOF_RULES
-    with type rule = rule
-     and type lit = Lit.t
-     and type term = Term.t
-
-module Rule_bool :
-  Sidekick_th_bool_static.PROOF_RULES
-    with type rule = rule
-     and type lit = Lit.t
-     and type term = Term.t
-     and type term := Term.t
diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml.tmp
similarity index 100%
rename from src/base/Proof_quip.ml
rename to src/base/Proof_quip.ml.tmp
diff --git a/src/base/Proof_quip.mli b/src/base/Proof_quip.mli.tmp
similarity index 100%
rename from src/base/Proof_quip.mli
rename to src/base/Proof_quip.mli.tmp
diff --git a/src/base/Proof.ml b/src/base/Proof_storage.ml.tmp
similarity index 100%
rename from src/base/Proof.ml
rename to src/base/Proof_storage.ml.tmp
diff --git a/src/base/Proof.mli b/src/base/Proof_storage.mli.tmp
similarity index 100%
rename from src/base/Proof.mli
rename to src/base/Proof_storage.mli.tmp
diff --git a/src/base/Sidekick_base.ml b/src/base/Sidekick_base.ml
index bbd89507..c89d4f06 100644
--- a/src/base/Sidekick_base.ml
+++ b/src/base/Sidekick_base.ml
@@ -16,15 +16,12 @@
 
     *)
 
+module Term = Sidekick_core.Term
 module Base_types = Base_types
 module ID = ID
-module Fun = Base_types.Fun
 module Stat = Stat
-module Model = Model
-module Term = Base_types.Term
 module Value = Base_types.Value
 module Term_cell = Base_types.Term_cell
-module Ty = Base_types.Ty
 module Statement = Base_types.Statement
 module Data = Base_types.Data
 module Select = Base_types.Select
@@ -37,6 +34,6 @@ module LIA_pred = Base_types.LIA_pred
 module LIA_op = Base_types.LIA_op
 module Solver_arg = Solver_arg
 module Lit = Lit
-module Proof_dummy = Proof_dummy
 module Proof = Proof
 module Proof_quip = Proof_quip
+module Types_ = Types_
diff --git a/src/base/Ty.ml b/src/base/Ty.ml
new file mode 100644
index 00000000..fcdbe96f
--- /dev/null
+++ b/src/base/Ty.ml
@@ -0,0 +1,59 @@
+(** Core types *)
+
+open Sidekick_core
+include Sidekick_core.Term
+open Types_
+
+type Const.view += Ty of ty_view
+type data = Types_.data
+
+let ops_ty : Const.ops =
+  (module struct
+    let pp out = function
+      | Ty ty ->
+        (match ty with
+        | Ty_real -> Fmt.string out "Real"
+        | Ty_int -> Fmt.string out "Int"
+        | Ty_uninterpreted { id; _ } -> ID.pp out id
+        | Ty_data d -> ID.pp out d.data.data_id)
+      | _ -> ()
+
+    let equal a b =
+      match a, b with
+      | Ty a, Ty b ->
+        (match a, b with
+        | Ty_int, Ty_int | Ty_real, Ty_real -> true
+        | Ty_uninterpreted u1, Ty_uninterpreted u2 -> ID.equal u1.id u2.id
+        | Ty_data d1, Ty_data d2 -> ID.equal d1.data.data_id d2.data.data_id
+        | (Ty_real | Ty_int | Ty_uninterpreted _ | Ty_data _), _ -> false)
+      | _ -> false
+
+    let hash = function
+      | Ty a ->
+        (match a with
+        | Ty_real -> Hash.int 2
+        | Ty_int -> Hash.int 3
+        | Ty_uninterpreted u -> Hash.combine2 10 (ID.hash u.id)
+        | Ty_data d -> Hash.combine2 30 (ID.hash d.data.data_id))
+      | _ -> assert false
+  end)
+
+open struct
+  let mk_ty0 tst view =
+    let ty = Term.type_ tst in
+    Term.const tst @@ Const.make (Ty view) ops_ty ~ty
+end
+(* TODO: handle polymorphic constants *)
+
+let int tst : ty = mk_ty0 tst Ty_int
+let real tst : ty = mk_ty0 tst Ty_real
+
+let uninterpreted tst id : t =
+  mk_ty0 tst (Ty_uninterpreted { id; finite = false })
+
+let data tst data : t = mk_ty0 tst (Ty_data { data })
+
+let is_uninterpreted (self : t) =
+  match view self with
+  | E_const { Const.c_view = Ty (Ty_uninterpreted _); _ } -> true
+  | _ -> false
diff --git a/src/base/Ty.mli b/src/base/Ty.mli
new file mode 100644
index 00000000..dac21a9a
--- /dev/null
+++ b/src/base/Ty.mli
@@ -0,0 +1,24 @@
+open Types_
+
+include module type of struct
+  include Term
+end
+
+type t = ty
+type data = Types_.data
+
+val bool : store -> t
+val real : store -> t
+val int : store -> t
+val uninterpreted : store -> ID.t -> t
+val data : store -> data -> t
+val is_uninterpreted : t -> bool
+
+(* TODO: separate functor?
+      val finite : t -> bool
+      val set_finite : t -> bool -> unit
+   val args : t -> ty list
+   val ret : t -> ty
+   val arity : t -> int
+   val unfold : t -> ty list * ty
+*)
diff --git a/src/base/arith_types_.ml b/src/base/arith_types_.ml
new file mode 100644
index 00000000..ec5cc14f
--- /dev/null
+++ b/src/base/arith_types_.ml
@@ -0,0 +1,146 @@
+let hash_z = Z.hash
+let[@inline] hash_q q = CCHash.combine2 (hash_z (Q.num q)) (hash_z (Q.den q))
+
+module LRA_pred = struct
+  type t = Sidekick_th_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
+
+  let to_string = function
+    | Lt -> "<"
+    | Leq -> "<="
+    | Neq -> "!="
+    | Eq -> "="
+    | Gt -> ">"
+    | Geq -> ">="
+
+  let pp out p = Fmt.string out (to_string p)
+end
+
+module LRA_op = struct
+  type t = Sidekick_th_lra.op = Plus | Minus
+
+  let to_string = function
+    | Plus -> "+"
+    | Minus -> "-"
+
+  let pp out p = Fmt.string out (to_string p)
+end
+
+module LRA_view = struct
+  type 'a t =
+    | Pred of LRA_pred.t * 'a * 'a
+    | Op of LRA_op.t * 'a * 'a
+    | Mult of Q.t * 'a
+    | Const of Q.t
+    | Var of 'a
+    | To_real of 'a
+
+  let map ~f_c f (l : _ t) : _ t =
+    match l with
+    | Pred (p, a, b) -> Pred (p, f a, f b)
+    | Op (p, a, b) -> Op (p, f a, f b)
+    | Mult (n, a) -> Mult (f_c n, f a)
+    | Const c -> Const (f_c c)
+    | Var x -> Var (f x)
+    | To_real x -> To_real (f x)
+
+  let iter f l : unit =
+    match l with
+    | Pred (_, a, b) | Op (_, a, b) ->
+      f a;
+      f b
+    | Mult (_, x) | Var x | To_real x -> f x
+    | Const _ -> ()
+
+  let pp ~pp_t out = function
+    | Pred (p, a, b) ->
+      Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_pred.to_string p) pp_t a pp_t b
+    | Op (p, a, b) ->
+      Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_op.to_string p) pp_t a pp_t b
+    | Mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Q.pp_print n pp_t x
+    | Const q -> Q.pp_print out q
+    | Var x -> pp_t out x
+    | To_real x -> Fmt.fprintf out "(@[to_real@ %a@])" pp_t x
+
+  let hash ~sub_hash = function
+    | Pred (p, a, b) -> Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
+    | Op (p, a, b) -> Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
+    | Mult (n, x) -> Hash.combine3 83 (hash_q n) (sub_hash x)
+    | Const q -> Hash.combine2 84 (hash_q q)
+    | Var x -> sub_hash x
+    | To_real x -> Hash.combine2 85 (sub_hash x)
+
+  let equal ~sub_eq l1 l2 =
+    match l1, l2 with
+    | Pred (p1, a1, b1), Pred (p2, a2, b2) ->
+      p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
+    | Op (p1, a1, b1), Op (p2, a2, b2) ->
+      p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
+    | Const a1, Const a2 -> Q.equal a1 a2
+    | Mult (n1, x1), Mult (n2, x2) -> Q.equal n1 n2 && sub_eq x1 x2
+    | Var x1, Var x2 | To_real x1, To_real x2 -> sub_eq x1 x2
+    | (Pred _ | Op _ | Const _ | Mult _ | Var _ | To_real _), _ -> false
+end
+
+module LIA_pred = LRA_pred
+module LIA_op = LRA_op
+
+module LIA_view = struct
+  type 'a t =
+    | Pred of LIA_pred.t * 'a * 'a
+    | Op of LIA_op.t * 'a * 'a
+    | Mult of Z.t * 'a
+    | Const of Z.t
+    | Var of 'a
+
+  let map ~f_c f (l : _ t) : _ t =
+    match l with
+    | Pred (p, a, b) -> Pred (p, f a, f b)
+    | Op (p, a, b) -> Op (p, f a, f b)
+    | Mult (n, a) -> Mult (f_c n, f a)
+    | Const c -> Const (f_c c)
+    | Var x -> Var (f x)
+
+  let iter f l : unit =
+    match l with
+    | Pred (_, a, b) | Op (_, a, b) ->
+      f a;
+      f b
+    | Mult (_, x) | Var x -> f x
+    | Const _ -> ()
+
+  let pp ~pp_t out = function
+    | Pred (p, a, b) ->
+      Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_pred.to_string p) pp_t a pp_t b
+    | Op (p, a, b) ->
+      Fmt.fprintf out "(@[%s@ %a@ %a@])" (LRA_op.to_string p) pp_t a pp_t b
+    | Mult (n, x) -> Fmt.fprintf out "(@[*@ %a@ %a@])" Z.pp_print n pp_t x
+    | Const n -> Z.pp_print out n
+    | Var x -> pp_t out x
+
+  let hash ~sub_hash = function
+    | Pred (p, a, b) -> Hash.combine4 81 (Hash.poly p) (sub_hash a) (sub_hash b)
+    | Op (p, a, b) -> Hash.combine4 82 (Hash.poly p) (sub_hash a) (sub_hash b)
+    | Mult (n, x) -> Hash.combine3 83 (hash_z n) (sub_hash x)
+    | Const n -> Hash.combine2 84 (hash_z n)
+    | Var x -> sub_hash x
+
+  let equal ~sub_eq l1 l2 =
+    match l1, l2 with
+    | Pred (p1, a1, b1), Pred (p2, a2, b2) ->
+      p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
+    | Op (p1, a1, b1), Op (p2, a2, b2) ->
+      p1 = p2 && sub_eq a1 a2 && sub_eq b1 b2
+    | Const a1, Const a2 -> Z.equal a1 a2
+    | Mult (n1, x1), Mult (n2, x2) -> Z.equal n1 n2 && sub_eq x1 x2
+    | Var x1, Var x2 -> sub_eq x1 x2
+    | (Pred _ | Op _ | Const _ | Mult _ | Var _), _ -> false
+
+  (* convert the whole structure to reals *)
+  let to_lra f l : _ LRA_view.t =
+    match l with
+    | Pred (p, a, b) -> LRA_view.Pred (p, f a, f b)
+    | Op (op, a, b) -> LRA_view.Op (op, f a, f b)
+    | Mult (c, x) -> LRA_view.Mult (Q.of_bigint c, f x)
+    | Const x -> LRA_view.Const (Q.of_bigint x)
+    | Var v -> LRA_view.Var (f v)
+end
diff --git a/src/base/dune b/src/base/dune
index 2846b4e8..af6aa5f3 100644
--- a/src/base/dune
+++ b/src/base/dune
@@ -2,8 +2,7 @@
  (name sidekick_base)
  (public_name sidekick-base)
  (synopsis "Base term definitions for the standalone SMT solver and library")
- (libraries containers iter sidekick.core sidekick.util sidekick.lit
-   sidekick-base.proof-trace sidekick.quip sidekick.arith-lra
-   sidekick.th-bool-static sidekick.th-data sidekick.zarith zarith
-   sidekick.proof-trace.dummy)
- (flags :standard -w -32 -open Sidekick_util))
+ (libraries containers iter sidekick.core sidekick.util sidekick.smt-solver
+   sidekick.cc sidekick.quip sidekick.th-lra sidekick.th-bool-static
+   sidekick.th-data sidekick.zarith zarith)
+ (flags :standard -w +32 -open Sidekick_util))
diff --git a/src/base/solver/dune b/src/base/solver/dune
index ab2c62ab..35b17f20 100644
--- a/src/base/solver/dune
+++ b/src/base/solver/dune
@@ -3,7 +3,7 @@
  (public_name sidekick-base.solver)
  (synopsis "Instantiation of solver and theories for Sidekick_base")
  (libraries sidekick-base sidekick.core sidekick.smt-solver
-   sidekick.th-bool-static sidekick.mini-cc sidekick.th-data
-   sidekick.arith-lra sidekick.zarith)
+   sidekick.th-bool-static sidekick.mini-cc sidekick.th-data sidekick.th-lra
+   sidekick.zarith)
  (flags :standard -warn-error -a+8 -safe-string -color always -open
    Sidekick_util))
diff --git a/src/base/types_.ml b/src/base/types_.ml
new file mode 100644
index 00000000..69e0070e
--- /dev/null
+++ b/src/base/types_.ml
@@ -0,0 +1,94 @@
+include Sidekick_core
+
+(* FIXME
+   module Proof_ser = Sidekick_base_proof_trace.Proof_ser
+   module Storage = Sidekick_base_proof_trace.Storage
+*)
+
+type term = Term.t
+type ty = Term.t
+type value = Term.t
+
+type fun_view =
+  | Fun_undef of ty (* simple undefined constant *)
+  | Fun_select of select
+  | Fun_cstor of cstor
+  | Fun_is_a of cstor
+  | Fun_def of {
+      pp: 'a. ('a Fmt.printer -> 'a array Fmt.printer) option;
+      abs: self:term -> term array -> term * bool; (* remove the sign? *)
+      do_cc: bool; (* participate in congruence closure? *)
+      relevant: 'a. ID.t -> 'a array -> int -> bool; (* relevant argument? *)
+      ty: ID.t -> term array -> ty; (* compute type *)
+      eval: value array -> value; (* evaluate term *)
+    }
+      (** Methods on the custom term view whose arguments are ['a].
+    Terms must be printable, and provide some additional theory handles.
+
+    - [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.
+*)
+
+and ty_view =
+  | Ty_int
+  | Ty_real
+  | Ty_uninterpreted of { id: ID.t; mutable finite: bool }
+  | Ty_data of { data: data }
+
+and data = {
+  data_id: ID.t;
+  data_cstors: cstor ID.Map.t lazy_t;
+  data_as_ty: ty lazy_t;
+}
+
+and cstor = {
+  cstor_id: ID.t;
+  cstor_is_a: ID.t;
+  mutable cstor_arity: int;
+  cstor_args: select list lazy_t;
+  cstor_ty_as_data: data;
+  cstor_ty: ty lazy_t;
+}
+
+and select = {
+  select_id: ID.t;
+  select_cstor: cstor;
+  select_ty: ty lazy_t;
+  select_i: int;
+}
+
+(* FIXME: just use  terms; introduce a Const.view for V_element
+   (** Semantic values, used for models (and possibly model-constructing calculi) *)
+   type value_view =
+     | V_element of { id: ID.t; ty: ty }
+         (** a named constant, distinct from any other constant *)
+     | V_cstor of { c: cstor; args: value list }
+     | V_custom of {
+         view: value_custom_view;
+         pp: value_custom_view Fmt.printer;
+         eq: value_custom_view -> value_custom_view -> bool;
+         hash: value_custom_view -> int;
+       }  (** Custom value *)
+     | V_real of Q.t
+
+   and value_custom_view = ..
+*)
+
+type definition = ID.t * ty * term
+
+type statement =
+  | Stmt_set_logic of string
+  | Stmt_set_option of string list
+  | Stmt_set_info of string * string
+  | Stmt_data of data list
+  | Stmt_ty_decl of ID.t * int (* new atomic cstor *)
+  | Stmt_decl of ID.t * ty list * ty
+  | Stmt_define of definition list
+  | Stmt_assert of term
+  | Stmt_assert_clause of term list
+  | Stmt_check_sat of (bool * term) list
+  | Stmt_get_model
+  | Stmt_get_value of term list
+  | Stmt_exit