diff --git a/src/lib/dune b/src/lib/dune
index fe1f9080f7..6a5429faba 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -24,8 +24,9 @@
     dune-build-info
     alt_ergo_prelude
     fmt
+    ppx_deriving.ord
   )
-  (preprocess (pps ppx_blob))
+  (preprocess (pps ppx_blob ppx_deriving.ord))
   (preprocessor_deps (glob_files ../preludes/*.ae))
 
   ; .mli only modules *also* need to be in this field
diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index 4cb87144c6..e045b5f6fa 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -162,12 +162,10 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
            far. You may need to change your model generation strategy \
            or to increase your timeouts. Returned timeout reason = %s@]" s
 
-    | Some mdl ->
+    | Some _ ->
       assert (get_m);
-      if get_m then
-        Printer.print_dbg "@[<v 0>Returned timeout reason = %s@]" s;
-      let mdl = Lazy.force mdl in
-      Models.pp (Options.Output.get_fmt_std ()) mdl
+      if get_m && Options.get_debug () then
+        Printer.print_dbg "@[<v 0>; Returned timeout reason = %s@]" s
 
   let filter_by_all_sat propositional filter =
     if filter == E.Set.empty then propositional
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 04d502c46c..623f6ff4f2 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -48,14 +48,14 @@ let constraints = ref MS.empty
 type objective_value =
   | Obj_pinfty
   | Obj_minfty
-  | Obj_val of string
+  | Obj_val of X.Value.t
   | Obj_unk
 
 let pp_objective_value ppf obj_val =
   match obj_val with
   | Obj_pinfty -> Fmt.pf ppf "+oo"
   | Obj_minfty -> Fmt.pf ppf "-oo"
-  | Obj_val s -> Fmt.pf ppf "%s" s
+  | Obj_val v -> X.Value.pp ppf v
   | Obj_unk -> Fmt.pf ppf "(interval -oo +oo)"
 
 let pp_objective ppf (obj_t, obj_val) =
@@ -73,10 +73,7 @@ type t = {
   functions : ModelMap.t;
   arrays : ModelMap.t;
   objectives : (Expr.t * objective_value) Util.MI.t;
-  terms_values : (X.r * string) ME.t (* a map from terms to their values
-                                        in the model (as a
-                                        representative of type X.r and
-                                        as a string *)
+  terms_values : Shostak.Combine.Value.t ME.t
 }
 
 module Pp_smtlib_term = struct
@@ -142,15 +139,15 @@ module Pp_smtlib_term = struct
 
         | Sy.L_built (Sy.IsConstr hs), [e] ->
           if get_output_smtlib () then
-            fprintf fmt "((_ is %a) %a)" Hstring.print hs print e
+            fprintf fmt "((_ is %a) %a)" Hstring.pp hs print e
           else
-            fprintf fmt "(%a ? %a)" print e Hstring.print hs
+            fprintf fmt "(%a ? %a)" print e Hstring.pp hs
 
         | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
           if get_output_smtlib () then
-            fprintf fmt "(not ((_ is %a) %a))" Hstring.print hs print e
+            fprintf fmt "(not ((_ is %a) %a))" Hstring.pp hs print e
           else
-            fprintf fmt "not (%a ? %a)" print e Hstring.print hs
+            fprintf fmt "not (%a ? %a)" print e Hstring.pp hs
 
         | (Sy.L_built (Sy.LT | Sy.LE) | Sy.L_neg_built (Sy.LT | Sy.LE)
           | Sy.L_neg_pred | Sy.L_eq | Sy.L_neg_eq
@@ -209,7 +206,7 @@ module Pp_smtlib_term = struct
 
     (* TODO: introduce PrefixOp in the future to simplify this ? *)
     | Sy.Op (Sy.Constr hs), ((_::_) as l) ->
-      fprintf fmt "%a(%a)" Hstring.print hs print_list l
+      fprintf fmt "%a(%a)" Hstring.pp hs print_list l
 
     | Sy.Op _, [e1; e2] ->
       if get_output_smtlib () then
@@ -219,7 +216,7 @@ module Pp_smtlib_term = struct
 
     | Sy.Op Sy.Destruct (hs, grded), [e] ->
       fprintf fmt "%a#%s%a"
-        print e (if grded then "" else "!") Hstring.print hs
+        print e (if grded then "" else "!") Hstring.pp hs
 
 
     | Sy.In(lb, rb), [t] ->
@@ -263,6 +260,12 @@ module Pp_smtlib_term = struct
 
 end
 
+module MV = Map.Make (struct
+    type t = X.Value.t
+
+    let compare = X.Value.compare
+  end)
+
 module SmtlibCounterExample = struct
   let rec pp_dummy_value_of_type ppf ty =
     match ty with
@@ -277,16 +280,17 @@ module SmtlibCounterExample = struct
     if not (Options.get_interpretation_use_underscore ()) then
       pp_dummy_value_of_type fmt ty
     else
-      fprintf fmt "_ "
+      Fmt.pf fmt "_ "
 
-  let add_records_destr records record_name destr_name rep =
-    let destrs =
+  (* let add_records_destr records record_name destr_name rep =
+     let destrs =
       try MS.find record_name records
       with Not_found -> MS.empty
-    in
-    let destrs =
-      MS.add destr_name rep destrs in
-    MS.add record_name destrs records
+     in
+     let destrs =
+      MS.add destr_name rep destrs
+     in
+     MS.add record_name destrs records *)
 
   let mk_records_constr records record_name
       { Ty.name = _n; record_constr = cstr; lbs = lbs; _} =
@@ -313,37 +317,40 @@ module SmtlibCounterExample = struct
       (Hstring.view cstr)
       print_destr (destrs,lbs)
 
-  let add_record_constr records record_name
+  (* let add_record_constr records record_name
       { Ty.name = _n; record_constr = _cstr; lbs = lbs; _} xs_values =
-    List.fold_left2(fun records (destr,_) (rep,_) ->
+     List.fold_left2(fun records (destr,_) (rep,_) ->
         add_records_destr
           records
           record_name
           (Hstring.view destr)
           (asprintf "%a" Pp_smtlib_term.print rep)
-      ) records lbs xs_values
-
-  let check_records records xs_ty_named xs_values f ty rep =
-    match xs_ty_named with
-    | [Ty.Trecord _r, _arg] -> begin
+      ) records lbs xs_values *)
+
+  (* TODO: restore this check. *)
+  (* let check_records records xs_ty_named xs_values f ty v =
+     let records = MS.map (MS.map (Fmt.str "%a" X.Value.pp)) records in
+     let name = Fmt.str "%a" X.Value.pp v in
+     match xs_ty_named with
+     | [Ty.Trecord _r, _arg] -> begin
         match xs_values with
         | [record_name,_] ->
           add_records_destr
             records
             (asprintf "%a" Expr.print record_name)
             (Sy.to_string f)
-            rep
+            name
         | [] | _ -> records
       end
-    | _ ->
+     | _ ->
       match ty with
       | Ty.Trecord r ->
-        add_record_constr records rep r xs_values
-      | _ -> records
+        add_record_constr records name r xs_values
+      | _ -> records *)
 
-  let print_fun_def ~is_array fmt name args ty t =
-    let print_args fmt (ty,name) =
-      Format.fprintf fmt "(%s %a)" name Ty.pp_smtlib ty in
+  let print_fun_def ppf name args ty t =
+    let print_args ppf (ty,name) =
+      Fmt.pf ppf "(%s %a)" name Ty.pp_smtlib ty in
     let defined_value =
       try
         let res,_,_ = (MS.find (Sy.to_string name) !constraints) in
@@ -351,9 +358,8 @@ module SmtlibCounterExample = struct
       with _ -> t
     in
 
-    Format.fprintf fmt
-      "@ (@[define-%s %a (%a) %a@ %t)@]"
-      (if is_array then "array" else "fun")
+    Fmt.pf ppf
+      "@ (@[define-fun %a (%a) %a@ %t)@]"
       Sy.print name
       (Printer.pp_list_space (print_args)) args
       Ty.pp_smtlib ty
@@ -364,7 +370,7 @@ module SmtlibCounterExample = struct
       (fun (f, xs_ty, ty) st ->
          assert (xs_ty == []);
          match ModelMap.V.elements st with
-         | [[], rep] ->
+         | [([], rep)] ->
            let rep =
              match ty with
              | Ty.Trecord r ->
@@ -373,31 +379,34 @@ module SmtlibCounterExample = struct
              | _ -> dprintf "%a" pp rep
            in
 
-           print_fun_def ~is_array:false fmt f [] ty rep
+           print_fun_def fmt f [] ty rep
          | _ -> assert false
       )
 
-  let output_functions_counterexample ?(is_array=false) pp fmt records fprofs =
+  let output_functions_counterexample pp fmt records fprofs =
     let records = ref records in
     ModelMap.iter
       (fun (f, xs_ty, ty) st ->
-         let xs_ty_named = List.mapi (fun i ty ->
-             ty,(sprintf "arg_%d" i)
-           ) xs_ty in
-
+         let xs_ty_named =
+           List.mapi (fun i ty ->
+               ty,(sprintf "arg_%d" i)
+             ) xs_ty
+         in
          let rep =
            let representants =
-             ModelMap.V.fold (fun (xs_values,(rep,srep)) acc ->
+             ModelMap.V.fold (fun (xs_values, v) acc ->
                  assert ((List.length xs_ty_named) = (List.length xs_values));
-                 records :=
-                   check_records !records xs_ty_named xs_values f ty srep;
-                 let reps = try MX.find rep acc |> snd with Not_found -> [] in
-                 MX.add rep (srep, xs_values :: reps) acc
-               ) st MX.empty in
-
-           let representants = MX.fold (fun rep (srep, xs_values_list) acc ->
-               ((rep, srep),xs_values_list) :: acc) representants [] in
-
+                 (* records :=
+                    check_records !records xs_ty_named xs_values f ty v; *)
+                 let vs = try MV.find v acc with Not_found -> [] in
+                 MV.add v (xs_values :: vs) acc
+               ) st MV.empty
+           in
+           let representants =
+             MV.fold (fun v xs_values_list acc ->
+                 (v, xs_values_list) :: acc
+               ) representants []
+           in
            let rec mk_ite_and xs tys =
              match xs, tys with
              | [],[] -> assert false
@@ -446,15 +455,10 @@ module SmtlibCounterExample = struct
            else
              reps_aux representants
          in
-         print_fun_def ~is_array fmt f xs_ty_named ty rep;
+         print_fun_def fmt f xs_ty_named ty rep;
       ) fprofs;
     !records
 
-  let output_arrays_counterexample pp fmt arrays =
-    let _records = output_functions_counterexample
-        ~is_array:true pp fmt MS.empty arrays in
-    ()
-
 end
 (* of module SmtlibCounterExample *)
 
@@ -466,28 +470,23 @@ type value_defn =
   | Constant of Symbols.t * Ty.t
   (* A constant of a given type. If the constant is defined in a model, it
      must be resolved before being printed. *)
-  | Value of X.r * string
-  (* A leaf semantic value. This must be an actual value, i.e. it must not
+  | Value of X.Value.t
+  (* A model value. This must be an actual value, i.e. it must not
      contain any uninterpreted terms. *)
 
-let value (r, s) =
-  match X.term_extract r with
-  | Some t, _ ->
-    begin match E.term_view t with
-      | { f = Name _ as sy; _ } -> Constant (sy, X.type_info r)
-      | _ -> Value (r, s)
-    end
-  | _ ->
-    Value (r, s)
+let value v =
+  match X.Value.extract v with
+  | Some (Name _ as sy, ty) -> Constant (sy, ty)
+  | _ -> Value v
 
 let rec pp_value ppk ppf = function
   | Store (a, k, v) ->
-    Format.fprintf ppf "(@[<hv>store@ %a@ %a %a)@]"
+    Fmt.pf ppf "(@[<hv>store@ %a@ %a %a)@]"
       (pp_value ppk) a
       (pp_value ppk) k
       (pp_value ppk) v
   | Constant (sy, t) -> ppk ppf (sy, t)
-  | Value (_, s) -> Format.pp_print_string ppf s
+  | Value v -> X.Value.pp ppf v
 
 let pp_constant ppf (_, t) =
   Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t
@@ -506,9 +505,9 @@ let pp fmt mdl =
     (* Add the constants *)
     ModelMap.iter (fun (f, xs_ty, _) st ->
         assert (Lists.is_empty xs_ty);
-        ModelMap.V.iter (fun (keys, (value_r, value_s)) ->
+        ModelMap.V.iter (fun (keys, v) ->
             assert (Lists.is_empty keys);
-            Hashtbl.add values f (value (value_r, value_s))
+            Hashtbl.add values f (value v)
           ) st
       ) mdl.constants;
 
@@ -519,8 +518,8 @@ let pp fmt mdl =
           with Not_found -> Constant (f, Tfarray (List.hd xs_ty, ty))
         in
         Hashtbl.replace values f @@
-        ModelMap.V.fold (fun (keys, rs) acc ->
-            Store (acc, value (snd (List.hd keys)), value rs)) st root
+        ModelMap.V.fold (fun (keys, v) acc ->
+            Store (acc, value (snd (List.hd keys)), value v)) st root
       ) mdl.arrays;
 
     let pp_value =
@@ -533,16 +532,13 @@ let pp fmt mdl =
     (* Functions *)
     let records =
       SmtlibCounterExample.output_functions_counterexample
-        ~is_array:false pp_x fmt MS.empty mdl.functions
+        pp_x fmt MS.empty mdl.functions
     in
 
     (* Constants *)
     SmtlibCounterExample.output_constants_counterexample
       pp_x fmt records mdl.constants;
 
-    (* Arrays *)
-    SmtlibCounterExample.output_arrays_counterexample pp_x fmt mdl.arrays;
-
     Printer.print_fmt fmt "@]@,)";
 
     (* TODO: Remove this option
diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli
index bbb8af4798..d7d17f85d6 100644
--- a/src/lib/frontend/models.mli
+++ b/src/lib/frontend/models.mli
@@ -33,7 +33,7 @@
 type objective_value =
   | Obj_pinfty
   | Obj_minfty
-  | Obj_val of string
+  | Obj_val of Shostak.Combine.Value.t
   | Obj_unk
 
 type t = {
@@ -43,9 +43,8 @@ type t = {
   arrays : ModelMap.t;
   objectives : (Expr.t * objective_value) Util.MI.t;
 
-  terms_values : (Shostak.Combine.r * string) Expr.Map.t
-  (* a map from terms to their values in the model (as a
-     representative of type X.r and as a string *)
+  terms_values : Shostak.Combine.Value.t Expr.Map.t
+  (** A map from terms to their values in the model. *)
 }
 
 (** Print the given counterexample on the given formatter with the
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 686acd2886..e21a627968 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -71,6 +71,17 @@ module Shostak (X : ALIEN) = struct
   type t = X.r abstract
   type r = X.r
 
+  module Value = struct
+    type t = unit [@@deriving ord]
+
+    let pp _ppf _v = Fmt.failwith "Not implemented yet"
+
+    let choose ?unbounded:_ _t _r _cls =
+      Printer.print_err
+        "[ADTs.models] choose_adequate_model currently not implemented";
+      raise (Util.Not_implemented "Models for ADTs")
+  end
+
   module SX = Set.Make(struct type t = r let compare = X.hash_cmp end)
 
   let name = "Adt"
@@ -94,22 +105,22 @@ module Shostak (X : ALIEN) = struct
       Format.fprintf fmt "%a" X.print x
 
     | Constr { c_name; c_args; _ } ->
-      Format.fprintf fmt "%a" Hs.print c_name;
+      Format.fprintf fmt "%a" Hs.pp c_name;
       begin
         match c_args with
           [] -> ()
         | (lbl, v) :: l ->
-          Format.fprintf fmt "(%a : %a " Hs.print lbl X.print v;
+          Format.fprintf fmt "(%a : %a " Hs.pp lbl X.print v;
           List.iter
             (fun (lbl, v) ->
-               Format.fprintf fmt "; %a : %a" Hs.print lbl X.print v) l;
+               Format.fprintf fmt "; %a : %a" Hs.pp lbl X.print v) l;
           Format.fprintf fmt ")"
       end
 
     | Select d ->
-      Format.fprintf fmt "%a#!!%a" X.print d.d_arg Hs.print d.d_name
+      Format.fprintf fmt "%a#!!%a" X.print d.d_arg Hs.pp d.d_name
     | Tester t ->
-      Format.fprintf fmt "(%a ? %a)" X.print t.t_arg Hs.print t.t_name
+      Format.fprintf fmt "(%a ? %a)" X.print t.t_arg Hs.pp t.t_name
 
 
   let is_mine u =
@@ -432,9 +443,4 @@ module Shostak (X : ALIEN) = struct
       "[ADTs.models] assign_value currently not implemented";
     raise (Util.Not_implemented "Models for ADTs")
 
-  let choose_adequate_model _ _ _ =
-    Printer.print_err
-      "[ADTs.models] choose_adequate_model currently not implemented";
-    raise (Util.Not_implemented "Models for ADTs")
-
 end
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index f48c4728d6..e71017ca84 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -116,7 +116,7 @@ module Debug = struct
            HSS.iter
              (fun hs ->
                 print_dbg ~flushed:false ~header:false
-                  "(%a is %a)@ " X.print r Hs.print hs
+                  "(%a is %a)@ " X.print r Hstring.pp hs
              )hss
         )env.seen_testers;
       print_dbg ~flushed:false ~header:false
@@ -128,7 +128,7 @@ module Debug = struct
                 List.iter (fun (a, _) ->
                     print_dbg ~flushed:false ~header:false
                       "(%a is %a) ==> %a@ "
-                      X.print r Hs.print hs E.print a
+                      X.print r Hstring.pp hs E.print a
                   ) l
              )mhs
         )env.selectors;
@@ -325,7 +325,7 @@ let add_guarded_destr env uf t hs e t_ty =
   if Options.get_debug_adt () then
     Printer.print_dbg ~header:false
       "associated with constr %a@,%a => %a"
-      Hstring.print c
+      Hstring.pp c
       E.print is_c
       E.print eq;
   let r_e, ex_e = try Uf.find uf e with Not_found -> assert false in
@@ -459,7 +459,7 @@ let assume_is_constr uf hs r dep env eqs =
     if Options.get_debug_adt () then
       Printer.print_dbg
         ~module_name:"Adt_rel" ~function_name:"assume_is_constr"
-        "assume is constr %a %a" X.print r Hs.print hs;
+        "assume is constr %a %a" X.print r Hstring.pp hs;
     if seen_tester r hs env then
       env, eqs
     else
@@ -585,7 +585,7 @@ let update_cs_modulo_eq r1 r2 ex env eqs =
                Printer.print_dbg
                  ~flushed:false ~header:false
                  "make deduction because %a ? %a is trivial@ "
-                 X.print r2 Hs.print hs;
+                 X.print r2 Hstring.pp hs;
              List.iter
                (fun (a, dep) ->
                   eqs := (Sig_rel.LTerm a, dep, Th_util.Other) :: !eqs) l;
@@ -700,7 +700,7 @@ let case_split env _ ~for_model ~to_optimize =
         let hs, _ = MHs.choose mhs in
         if Options.get_debug_adt () then
           Printer.print_dbg ~header:false
-            "found hs = %a" Hs.print hs;
+            "found hs = %a" Hstring.pp hs;
         (* cs on negative version would be better in general *)
         let cs =  LR.mkv_builtin false (Sy.IsConstr hs) [r] in
         Sig_rel.Split [ cs, true, Th_util.CS(None, Th_util.Th_adt, two) ]
diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml
index 30f63bc6aa..0221df6afc 100644
--- a/src/lib/reasoners/arith.ml
+++ b/src/lib/reasoners/arith.ml
@@ -82,9 +82,75 @@ module Shostak
     (P : Polynome.EXTENDED_Polynome with type r = X.r) = struct
 
   type t = P.t
-
   type r = P.r
 
+  let embed r = match P.extract r with
+    | Some p -> p
+    | _ -> P.create [Q.one, r] Q.zero (X.type_info r)
+
+  module Value = struct
+    type t =
+      | Num of Q.t
+      | Inf of Th_util.inf
+    [@@deriving ord]
+
+    let pp ppf v =
+      let pp_positive_value ppf v =
+        let num = Q.num v in
+        let den = Q.den v in
+        if Z.is_one den then
+          Fmt.pf ppf "%a" Z.print num
+        else Fmt.pf ppf "(/ %a %a)" Z.print num Z.print den
+      in
+      match v with
+      | Num v ->
+        let sign = Q.sign v in
+        if sign = 0 then
+          Fmt.pf ppf "0"
+        else if sign > 0 then
+          pp_positive_value ppf v
+        else
+          Fmt.pf ppf "(- %a)" pp_positive_value (Q.abs v)
+      | Inf i -> Th_util.pp_inf ppf i
+
+    let choose ?unbounded t r cls =
+      assert (Ty.equal (Expr.type_info t) (X.type_info r));
+      if Options.get_debug_interpretation () then
+        Printer.print_dbg
+          ~module_name:"Arith" ~function_name:"choose_adequate_model"
+          "choose_adequate_model for %a" E.print t;
+      match unbounded with
+      | Some ((`Pinfinity | `Minfinity) as u) -> Inf u
+      | None ->
+        (* We keep only constant polynomials as nonconstant polynomials or
+           alien semantic values aren't adequate model values. *)
+        let cls =
+          List.partition_map (fun (_, r) ->
+              match P.is_const (embed r) with
+              | Some c ->
+                Left (c, r)
+              | None ->
+                Right ()
+            ) cls
+          |> fst
+        in
+        match cls with
+        | (c, _) :: cls ->
+          (* TODO: why this test is valid? *)
+          assert (List.for_all (fun (_, x) -> X.equal x r) cls);
+          Num c
+        | [] ->
+          (* This case happens because terms of some semantic values created
+             by case-split are not added to union-find. *)
+          match P.is_const (embed r) with
+          | Some c -> Num c
+          | None ->
+            Printer.print_dbg
+              ~module_name:"Arith" ~function_name:"choose_adequate_model"
+              "no adequate model found for %a" X.print r;
+            assert false
+  end
+
   let name = "arith"
 
   (*BISECT-IGNORE-BEGIN*)
@@ -130,10 +196,6 @@ module Shostak
     | Some (a,x,b) when Q.equal a Q.one && Q.sign b = 0 -> x
     | _ -> P.embed p
 
-  let embed r = match P.extract r with
-    | Some p -> p
-    | _ -> P.create [Q.one, r] Q.zero (X.type_info r)
-
   (* t1 % t2 = md  <->
      c1. 0 <= md ;
      c2. md < t2 ;
@@ -814,51 +876,4 @@ module Shostak
         cpt := Q.add Q.one (max_constant distincts !cpt);
         Some (term_of_cst (Q.to_string !cpt), true)
 
-
-
-  let pprint_const_for_model =
-    let pprint_positive_const c =
-      let num = Q.num c in
-      let den = Q.den c in
-      if Z.is_one den then Z.to_string num
-      else Format.sprintf "(/ %s %s)" (Z.to_string num) (Z.to_string den)
-    in
-    fun r ->
-      match P.is_const (embed r) with
-      | None -> assert false
-      | Some c ->
-        let sg = Q.sign c in
-        if sg = 0 then "0"
-        else if sg > 0 then pprint_positive_const c
-        else Format.sprintf "(- %s)" (pprint_positive_const (Q.abs c))
-
-  let choose_adequate_model t r cls =
-    if Options.get_debug_interpretation () then
-      Printer.print_dbg
-        ~module_name:"Arith" ~function_name:"choose_adequate_model"
-        "choose_adequate_model for %a" E.print t;
-    (* We keep only constant polynomials as nonconstant polynomials or
-       alien semantic values aren't adequate values in models. *)
-    let cls = List.filter (fun (_, r) -> P.is_const (embed r) != None) cls in
-    let r =
-      match cls with
-      | [] ->
-        (* We do this, because terms of some semantic values created
-           by CS are not created and added to UF *)
-        if (P.is_const (embed r) == None) then begin
-          Printer.print_dbg
-            ~module_name:"Arith" ~function_name:"choose_adequate_model"
-            "no adequate model found for %a" X.print r;
-          assert false
-        end;
-        r
-
-      | (_, r) :: cls ->
-        (* We assume that the argument cls of the function is part of
-           the equivalence class of r in the union-find. *)
-        List.iter (fun (_, x) -> assert (X.equal x r)) cls;
-        r
-    in
-    r, pprint_const_for_model r
-
 end
diff --git a/src/lib/reasoners/arrays.ml b/src/lib/reasoners/arrays.ml
index 881f926138..956c46edd4 100644
--- a/src/lib/reasoners/arrays.ml
+++ b/src/lib/reasoners/arrays.ml
@@ -41,6 +41,32 @@ module Shostak (X : ALIEN) = struct
   type t = X.r abstract
   type r = X.r
 
+  module Value = struct
+    type t = string [@@deriving ord]
+
+    let pp = Fmt.string
+
+    let choose ?unbounded:_ _t _r cls =
+      (* Take the biggest constant term in the equivalence class cls.
+         According to the current definition of Expr.compare, it means we
+         take the oldest constant term in the equivalence class. *)
+      let oldest =
+        List.fold_left
+          (fun oldest (s, r) ->
+             if not @@ Expr.const_term s then oldest
+             else
+               match oldest with
+               | Some (s', _) when Expr.compare s' s > 0 -> oldest
+               | _ -> Some (s, r)
+          ) None cls
+      in
+      match oldest with
+      | Some (_, r) ->
+        Fmt.str "%a" X.print r (* it's a EUF constant *)
+
+      | _ -> assert false
+  end
+
   let name           = "Farrays"
   let is_mine_symb _ _ = false
   let fully_interpreted _ = assert false
@@ -66,21 +92,4 @@ module Shostak (X : ALIEN) = struct
         Some (Expr.fresh_name (X.type_info r), false)
       | _ -> assert false
 
-  let choose_adequate_model _ _ l =
-    let acc =
-      List.fold_left
-        (fun acc (s, r) ->
-           if not (Expr.const_term s) then acc
-           else
-             match acc with
-             | Some(s', _) when Expr.compare s' s > 0 -> acc
-             | _ -> Some (s, r)
-        ) None l
-    in
-    match acc with
-    | Some (_, r) ->
-      r, Format.asprintf "%a" X.print r (* it's a EUF constant *)
-
-    | _ -> assert false
-
 end
diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 4eab14800a..82074bd23b 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -135,6 +135,17 @@ module Shostak(X : ALIEN) = struct
   type t = X.r abstract
   type r = X.r
 
+  module Value = struct
+    type t = unit [@@deriving ord]
+
+    let pp _ppf _v = Fmt.failwith "Not implemented yet"
+
+    let choose ?unbounded:_ _t _r _cls =
+      Printer.print_err
+        "[Bitv.Value] choose currently not implemented";
+      raise (Util.Not_implemented "Models for bit-vectors")
+  end
+
   let name = "bitv"
 
   let is_mine_symb sy _ =
@@ -1332,9 +1343,4 @@ module Shostak(X : ALIEN) = struct
       "[Bitv.models] assign_value currently not implemented";
     raise (Util.Not_implemented "Models for bit-vectors")
 
-  let choose_adequate_model _ _ =
-    Printer.print_err
-      "[Bitv.models] choose_adequate_model currently not implemented";
-    raise (Util.Not_implemented "Models for bit-vectors")
-
 end
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index 2be3c5e74e..81ed4762d0 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -68,8 +68,9 @@ module type S = sig
 
   val case_split :
     t -> for_model:bool ->
-    to_optimize: Th_util.optimized_split option ->
+    to_optimize: Shostak.Combine.r Th_util.optimized_split option ->
     Sig_rel.case_split * t
+
   val query :  t -> E.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
   val class_of : t -> Expr.t -> Expr.Set.t
@@ -88,7 +89,7 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    optimized_splits:Th_util.optimized_split Util.MI.t ->
+    optimized_splits:Shostak.Combine.r Th_util.optimized_split Util.MI.t ->
     t ->
     Models.t Lazy.t option
 
diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli
index d6622f0503..b34ea61b2e 100644
--- a/src/lib/reasoners/ccx.mli
+++ b/src/lib/reasoners/ccx.mli
@@ -60,7 +60,7 @@ module type S = sig
 
   val case_split :
     t -> for_model:bool ->
-    to_optimize: Th_util.optimized_split option ->
+    to_optimize:Shostak.Combine.r Th_util.optimized_split option ->
     Sig_rel.case_split * t
   val query :  t -> Expr.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
@@ -79,7 +79,7 @@ module type S = sig
 
   val extract_concrete_model :
     prop_model:Expr.Set.t ->
-    optimized_splits:Th_util.optimized_split Util.MI.t ->
+    optimized_splits:Shostak.Combine.r Th_util.optimized_split Util.MI.t ->
     t ->
     Models.t Lazy.t option
 end
diff --git a/src/lib/reasoners/enum.ml b/src/lib/reasoners/enum.ml
index 7366b0ab61..5743a0b13b 100644
--- a/src/lib/reasoners/enum.ml
+++ b/src/lib/reasoners/enum.ml
@@ -45,6 +45,33 @@ module Shostak (X : ALIEN) = struct
   type t = X.r abstract
   type r = X.r
 
+  let embed r =
+    match X.extract r with
+    | Some c -> c
+    | None -> Alien r
+
+  module Value = struct
+    include Hstring
+
+    let choose ?unbounded:_ _t r cls =
+      let cls =
+        List.partition_map (fun (_, r) ->
+            match embed r with
+            | Cons (hs, _) -> Left hs
+            | _ -> Right ()
+          ) cls
+        |> fst
+      in
+      match cls with
+      | v :: _ -> v
+      | [] ->
+        (* This case happens because terms of some semantic values created
+           by case-split are not added to union-find. *)
+        match embed r with
+        | Cons (hs, _) -> hs
+        | _ -> assert false
+  end
+
   let name = "Sum"
 
   let is_mine_symb sy ty =
@@ -96,11 +123,6 @@ module Shostak (X : ALIEN) = struct
 
   let print = Debug.print
 
-  let embed r =
-    match X.extract r with
-    | Some c -> c
-    | None -> Alien r
-
   let is_mine = function
     | Alien r -> r
     | Cons _ as c -> X.embed c
@@ -186,21 +208,4 @@ module Shostak (X : ALIEN) = struct
     (* values of theory sum should be assigned by case_split *)
     None
 
-  let choose_adequate_model _ r l =
-    let l =
-      List.filter
-        (fun (_, r) -> match embed r with Cons _ -> true | _ -> false) l
-    in
-    let r = match l with
-      | (_,r)::l ->
-        List.iter (fun (_,x) -> assert (X.equal x r)) l;
-        r
-
-      | [] ->
-        (* We do this, because terms of some semantic values created
-           by CS are not created and added to UF *)
-        match embed r with Cons _ -> r | _ -> assert false
-    in
-    r, Format.asprintf "%a" X.print r  (* it's a EUF constant *)
-
 end
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index 16689af129..3924e46cff 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -2097,7 +2097,7 @@ let optimizing_split env uf opt =
      done without waiting for ~for_model flag to be true *)
   let {Th_util.order; r = r; is_max = to_max; e; value } = opt in
   assert (match value with
-      | Unknown -> true
+      | `Unknown -> true
       | _ -> false
     );
   let repr, _ = Uf.find uf e in
@@ -2114,9 +2114,9 @@ let optimizing_split env uf opt =
     let r2 = alien_of (P.create [] optim  ty) in
     let t2 = mk_const_term optim ty in
     Debug.case_split r1 r2;
-    let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
+    let o = Some {Th_util.opt_ord = order; opt_val = `Value t2} in
     let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
-    Sig_rel.Optimized_split { opt with value = Value s; }
+    Sig_rel.Optimized_split { opt with value = `Value s; }
 
   | None ->
     let sim = if ty == Ty.Tint then env.int_sim else env.rat_sim in
@@ -2132,7 +2132,7 @@ let optimizing_split env uf opt =
       Printer.print_dbg
         "%a is unbounded. Let other methods assign a value for it@."
         E.print e;
-      let value = if to_max then Th_util.Pinfinity else Th_util.Minfinity in
+      let value = if to_max then `Pinfinity else `Minfinity in
       Sig_rel.Optimized_split { opt with value }
 
     | Sim.Core.Max(mx,_sol) ->
@@ -2148,9 +2148,9 @@ let optimizing_split env uf opt =
       let r2 = alien_of (P.create [] optim  ty) in
       Debug.case_split r1 r2;
       let t2 = mk_const_term optim ty in
-      let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
+      let o = Some {Th_util.opt_ord = order; opt_val = `Value t2} in
       let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
-      Sig_rel.Optimized_split { opt with value = Value s; }
+      Sig_rel.Optimized_split { opt with value = `Value s; }
 
 
 let case_split env uf ~for_model ~to_optimize =
diff --git a/src/lib/reasoners/ite.ml b/src/lib/reasoners/ite.ml
index a4daa5c68e..fe8c5fb33a 100644
--- a/src/lib/reasoners/ite.ml
+++ b/src/lib/reasoners/ite.ml
@@ -41,6 +41,14 @@ module Shostak (X : ALIEN) = struct
   type t = X.r abstract
   type r = X.r
 
+  module Value = struct
+    type t = unit [@@deriving ord]
+
+    let pp _ppf _v = Fmt.failwith "Not implemented yet"
+
+    let choose ?unbounded:_ _t _r _cls = assert false
+  end
+
   let name           = "Ite"
   let is_mine_symb _ _ = false
   let fully_interpreted _ = assert false
@@ -59,6 +67,5 @@ module Shostak (X : ALIEN) = struct
   let abstract_selectors _ _ = assert false
   let solve _ _ = assert false
   let assign_value _ _ _ = assert false
-  let choose_adequate_model _ _ _ = assert false
 end
 
diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index 84180f7d7f..aa8ce0133f 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -51,6 +51,32 @@ module Shostak (X : ALIEN) = struct
   type t = X.r abstract
   type r = X.r
 
+  module Value = struct
+    type t = string [@@deriving ord]
+
+    let pp = Fmt.string
+
+    let choose ?unbounded:_ _t _r cls =
+      (* Take the biggest constant term in the equivalence class cls.
+         According to the current definition of Expr.compare, it means we
+         take the oldest constant term in the equivalence class. *)
+      let oldest =
+        List.fold_left
+          (fun oldest (s, r) ->
+             if not @@ Expr.const_term s then oldest
+             else
+               match oldest with
+               | Some (s', _) when Expr.compare s' s > 0 -> oldest
+               | _ -> Some (s, r)
+          ) None cls
+      in
+      match oldest with
+      | Some (_, r) ->
+        Format.asprintf "%a" X.print r (* it's a EUF constant *)
+
+      | _ -> assert false
+  end
+
   (*BISECT-IGNORE-BEGIN*)
   module Debug = struct
 
@@ -417,20 +443,4 @@ module Shostak (X : ALIEN) = struct
         Some (s, false) (* false <-> not a case-split *)
       | _ -> assert false
 
-  let choose_adequate_model _ _ l =
-    let acc =
-      List.fold_left
-        (fun acc (s, r) ->
-           if not (Expr.const_term s) then acc
-           else
-             match acc with
-             | Some(s', _) when Expr.compare s' s > 0 -> acc
-             | _ -> Some (s, r)
-        ) None l
-    in
-    match acc with
-    | Some (_,r) ->
-      r, Format.asprintf "%a" X.print r  (* it's a EUF constant *)
-    | _ -> assert false
-
 end
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 2691dde9fc..14441f4832 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -62,7 +62,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     guards : guards;
     last_saved_model : Models.t Lazy.t option ref;
     model_gen_phase : bool ref;
-    objectives : Th_util.optimized_split Util.MI.t option ref
+    objectives : Shostak.Combine.r Th_util.optimized_split Util.MI.t option ref
   }
 
   let empty_guards () = {
@@ -1052,16 +1052,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
            if !seen_infinity then acc
            else
              match value with
-             | Pinfinity ->
+             | `Pinfinity ->
                seen_infinity := true; acc
-             | Minfinity ->
+             | `Minfinity ->
                seen_infinity := true; acc
-             | Value (_,_, Th_util.CS (Some {opt_val = Value v; _},_,_)) ->
+             | `Value (_,_, Th_util.CS (Some {opt_val = `Value v; _},_,_)) ->
                (* hack-ish to get the value of type expr *)
                (e, v, is_max) :: acc
-             | Value _ ->
+             | `Value _ ->
                assert false
-             | Unknown ->
+             | `Unknown ->
                assert false
         ) obj []
     in
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index e2f829252c..c30f5c548e 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -621,64 +621,123 @@ struct
          | Some(res, _is_cs) -> Format.asprintf "%a" Expr.print res);
     opt
 
-  let choose_adequate_model t rep l =
-    let r, pprint =
-      match Expr.type_info t with
-      | Ty.Tint
-      | Ty.Treal     -> X1.choose_adequate_model t rep l
-      | Ty.Tbitv _   -> X3.choose_adequate_model t rep l
-      | Ty.Tsum _    -> X5.choose_adequate_model t rep l
-      | Ty.Tadt _    when not (Options.get_disable_adts()) ->
-        X6.choose_adequate_model t rep l
-      | Ty.Trecord _ -> X2.choose_adequate_model t rep l
-      | Ty.Tfarray _ -> X4.choose_adequate_model t rep l
-      | Ty.Tbool ->
-        (* case split is now supposed to be done for internal bools if
-           needed as well *)
-        assert (is_bool_const rep);
-        rep, Format.asprintf "%a" print rep
-      | _            ->
-        let acc =
-          List.fold_left
-            (fun acc (s, r) ->
-               if Expr.const_term s then
-                 match acc with
-                 | Some(s', _) when Expr.compare s' s > 0 -> acc
-                 | _ -> Some (s, r)
-               else
-                 acc
-            ) None l
-        in
-        let r =
-          match acc with
-          | Some (_,r) -> r
-          | None ->
-            match term_extract rep with
-            | Some t, true when Expr.const_term t -> rep
-            | _ ->
-              let print_aux fmt (t,r) =
-                Format.fprintf fmt "> impossible case: %a -- %a@ "
-                  Expr.print t
-                  print r
-              in
-              if Options.get_debug_interpretation () then
-                Printer.print_dbg
-                  ~module_name:"Shostak" ~function_name:"choose_adequate_model"
-                  "@[<v 2>What to choose for term %a with rep %a?\
-                   %a@]"
-                  Expr.print t
-                  print rep
-                  (Printer.pp_list_no_space print_aux) l;
-              assert false
-        in
-        r, Format.asprintf "%a" print r (* it's a EUF constant *)
-    in
-    if Options.get_debug_interpretation () then
-      Printer.print_dbg
-        ~module_name:"Shostak" ~function_name:"choose_adequate_model"
-        "%a selected as a model for %a"
-        print r Expr.print t;
-    r, pprint
+  module Value = struct
+    type t =
+      | VX1 of X1.Value.t
+      | VX2 of X2.Value.t
+      | VX3 of X3.Value.t
+      | VX4 of X4.Value.t
+      | VX5 of X5.Value.t
+      | VX6 of X6.Value.t
+      | VX7 of X7.Value.t
+      | Vbool of bool
+      | Const of Symbols.t * Ty.t
+    [@@deriving ord]
+
+    let pp ppf v =
+      match v with
+      | VX1 v -> X1.Value.pp ppf v
+      | VX2 v -> X2.Value.pp ppf v
+      | VX3 v -> X3.Value.pp ppf v
+      | VX4 v -> X4.Value.pp ppf v
+      | VX5 v -> X5.Value.pp ppf v
+      | VX6 v -> X6.Value.pp ppf v
+      | VX7 v -> X7.Value.pp ppf v
+      | Vbool b -> Fmt.bool ppf b
+      | Const (sy, _) -> Fmt.pf ppf "%a" Symbols.print sy
+
+    let extract v =
+      match v with
+      | Const (sy, ty) -> Some (sy, ty)
+      | _ -> None
+
+    let choose ?unbounded t r cls =
+      assert (Ty.equal (Expr.type_info t) (type_info r));
+      (* Fmt.pr "r = %a, cls = { %a }@." print r
+         (Fmt.list ~sep:Fmt.sp (fun ppf (_, x) -> print ppf x)) cls; *)
+      let v =
+        match r.v with
+        | X1 _ ->
+          VX1 (X1.Value.choose ?unbounded t r cls)
+
+        | X2 _ ->
+          VX2 (X2.Value.choose ?unbounded t r cls)
+
+        | X3 _ ->
+          VX3 (X3.Value.choose ?unbounded t r cls)
+
+        | X4 _ ->
+          VX4 (X4.Value.choose ?unbounded t r cls)
+
+        | X5 _   ->
+          VX5 (X5.Value.choose ?unbounded t r cls)
+
+        | X6 _  when not (Options.get_disable_adts()) ->
+          VX6 (X6.Value.choose ?unbounded t r cls)
+
+        | X7 _   ->
+          VX7 (X7.Value.choose ?unbounded t r cls)
+
+        | _ when equal r (top ()) -> Vbool true
+
+        | _ when equal r (bot ()) -> Vbool false
+
+        | Term t ->
+          begin
+            (* Take the biggest constant term in the equivalence class cls.
+               According to the current definition of Expr.compare, it means we
+               take the oldest constant term in the equivalence class. *)
+            let oldest =
+              List.fold_left
+                (fun oldest (s, _) ->
+                   if not @@ Expr.const_term s then oldest
+                   else
+                     match oldest with
+                     | Some s' when Expr.compare s' s > 0 -> oldest
+                     | _ -> Some s
+                ) None cls
+            in
+            match oldest with
+            | Some t ->
+              let Expr.{ f = sy; ty; _ } = Expr.term_view t in
+              Const (sy, ty)
+
+            | None ->
+              begin
+                if Expr.const_term t then
+                  let Expr.{ f = sy; ty; _ } = Expr.term_view t in
+                  Const (sy, ty)
+                else
+                  begin
+                    if Options.get_debug_interpretation () then begin
+                      let pp_aux ppf (t, r) =
+                        Fmt.pf ppf "(%a, %a)" Expr.print t print r
+                      in
+                      Printer.print_dbg
+                        ~module_name:"Shostak"
+                        ~function_name:"choose_adequate_model"
+                        "@[<v 2>What to choose for term %a with rep %a?\
+                         %a@]"
+                        Expr.print t
+                        print r
+                        (Fmt.list ~sep:Fmt.sp pp_aux) cls
+                    end;
+                    assert false
+                  end
+              end
+          end
+        | _ ->
+          (* Case-split is now supposed to be done for internal bools if
+             needed as well. *)
+          assert false
+      in
+      if Options.get_debug_interpretation () then
+        Printer.print_dbg
+          ~module_name:"Shostak" ~function_name:"choose_adequate_model"
+          "%a selected as a model for %a"
+          pp v Expr.print t;
+      v
+  end
 
 end
 
diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli
index 6b673e2dc8..cc8894fbf4 100644
--- a/src/lib/reasoners/sig.mli
+++ b/src/lib/reasoners/sig.mli
@@ -35,11 +35,26 @@ type 'a solve_pb = { sbt : ('a * 'a) list; eqs : ('a * 'a) list }
 
 module type SHOSTAK = sig
 
-  (**Type of terms of the theory*)
   type t
+  (** Type of the semantic value of the theory. *)
 
-  (**Type of representants of terms of the theory*)
   type r
+  (** Type of the semantic values of the super-theory. *)
+
+  (** Module of model values. *)
+  module Value : sig
+    type t [@@deriving ord]
+    (** Type of the model values of the theory. *)
+
+    val pp : t Fmt.t
+    (** [pp ppf v] print the model value [v] in the SMT-LIB format on the
+        formatter [ppf]. *)
+
+    val choose : ?unbounded:Th_util.inf -> Expr.t -> r -> (Expr.t * r) list -> t
+    (** [choose ~unbounded t r cls] choose the model value to print
+        for [t] where [r] is its semantic value and [cls] its equivalence
+        class in the union-find. *)
+  end
 
   (** Name of the theory*)
   val name : string
@@ -86,15 +101,30 @@ module type SHOSTAK = sig
   val assign_value :
     r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
 
-  (* choose the value to print and how to print it for the given term.
-     The second term is its representative. The list is its equivalence class
-  *)
-  val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string
-
 end
 
 module type X = sig
   type r
+  (** Type of the semantic value of the theory. *)
+
+  (** Module of model values. *)
+  module Value : sig
+    type t [@@deriving ord]
+    (** Type of the model values of the theory. *)
+
+    val pp : t Fmt.t
+    (** [pp ppf v] print the model value [v] in the SMT-LIB format on the
+        formatter [ppf]. *)
+
+    (* TODO: return an option instead of failing when we cannot
+       produce the model value. *)
+    val choose : ?unbounded:Th_util.inf -> Expr.t -> r -> (Expr.t * r) list -> t
+    (** [choose ~unbounded t r cls] choose the model value to print
+        for [t] where [r] is its semantic value and [cls] its equivalence
+        class in the union-find. *)
+
+    val extract : t -> (Symbols.t * Ty.t) option
+  end
 
   val save_cache : unit -> unit
   (** saves the module's current cache *)
@@ -149,9 +179,4 @@ module type X = sig
   *)
   val assign_value :
     r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
-
-  (* choose the value to print and how to print it for the given term.
-     The second term is its representative. The list is its equivalence class
-  *)
-  val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string
 end
diff --git a/src/lib/reasoners/sig_rel.mli b/src/lib/reasoners/sig_rel.mli
index 515874833a..24c9ebdf31 100644
--- a/src/lib/reasoners/sig_rel.mli
+++ b/src/lib/reasoners/sig_rel.mli
@@ -50,8 +50,8 @@ type 'a result = {
 }
 
 type case_split =
-  | Split of Th_util.split_info list
-  | Optimized_split of Th_util.optimized_split
+  | Split of Shostak.Combine.r Th_util.split_info list
+  | Optimized_split of Shostak.Combine.r Th_util.optimized_split
 
 module type RELATION = sig
   type t
@@ -65,7 +65,7 @@ module type RELATION = sig
   val case_split :
     t -> Uf.t ->
     for_model:bool ->
-    to_optimize: Th_util.optimized_split option ->
+    to_optimize: Shostak.Combine.r Th_util.optimized_split option ->
     case_split
   (** case_split env returns a list of equalities *)
 
diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml
index 103e0c0487..c1b6bea58a 100644
--- a/src/lib/reasoners/th_util.ml
+++ b/src/lib/reasoners/th_util.ml
@@ -38,11 +38,21 @@ type theory =
   | Th_arrays
   | Th_UF
 
-type 'a optimized_split_value =
-  | Minfinity
-  | Value of 'a
-  | Pinfinity
-  | Unknown
+type inf = [
+  | `Pinfinity
+  | `Minfinity
+] [@@deriving ord]
+
+let pp_inf ppf i =
+  match i with
+  | `Pinfinity -> Fmt.pf ppf "+oo"
+  | `Minfinity -> Fmt.pf ppf "-oo"
+
+type 'a optimized_split_value = [
+  | `Value of 'a
+  | `Unknown
+  | inf
+] [@@deriving_ord]
 
 type optimization =
   { opt_ord : int; opt_val : Expr.t optimized_split_value }
@@ -53,12 +63,12 @@ type lit_origin =
   | NCS of theory * Numbers.Q.t
   | Other
 
-type split_info = Shostak.Combine.r Xliteral.view * bool * lit_origin
+type 'a split_info = 'a Xliteral.view * bool * lit_origin
 
-type optimized_split =
-  { r : Shostak.Combine.r;
-    e : Expr.t;
-    value : split_info optimized_split_value;
-    is_max : bool; (* for linear arithmetic: is_max <-> (opt = maximize) *)
-    order : int (* ordering assigned by the user for this variable *)
-  }
+type 'a optimized_split = {
+  r : 'a;
+  e : Expr.t;
+  value : 'a split_info optimized_split_value;
+  is_max : bool; (* for linear arithmetic: is_max <-> (opt = maximize) *)
+  order : int (* ordering assigned by the user for this variable *)
+}
diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli
index 103e0c0487..cec7b1b902 100644
--- a/src/lib/reasoners/th_util.mli
+++ b/src/lib/reasoners/th_util.mli
@@ -30,7 +30,6 @@
 
 type answer = (Explanation.t * Expr.Set.t list) option
 
-
 type theory =
   | Th_arith
   | Th_sum
@@ -38,11 +37,20 @@ type theory =
   | Th_arrays
   | Th_UF
 
-type 'a optimized_split_value =
-  | Minfinity
-  | Value of 'a
-  | Pinfinity
-  | Unknown
+type inf = [
+  | `Pinfinity
+  | `Minfinity
+] [@@deriving ord]
+
+val pp_inf : inf Fmt.t
+(** [pp_inf ppf i] print the infinity bound [i] in the SMT-LIB format
+    on the formatter [ppf]. *)
+
+type 'a optimized_split_value = [
+  | `Value of 'a
+  | `Unknown
+  | inf
+] [@@deriving_ord]
 
 type optimization =
   { opt_ord : int; opt_val : Expr.t optimized_split_value }
@@ -53,12 +61,12 @@ type lit_origin =
   | NCS of theory * Numbers.Q.t
   | Other
 
-type split_info = Shostak.Combine.r Xliteral.view * bool * lit_origin
+type 'a split_info = 'a Xliteral.view * bool * lit_origin
 
-type optimized_split =
-  { r : Shostak.Combine.r;
-    e : Expr.t;
-    value : split_info optimized_split_value;
-    is_max : bool; (* for linear arithmetic: is_max <-> (opt = maximize) *)
-    order : int (* ordering assigned by the user for this variable *)
-  }
+type 'a optimized_split = {
+  r : 'a;
+  e : Expr.t;
+  value : 'a split_info optimized_split_value;
+  is_max : bool; (* for linear arithmetic: is_max <-> (opt = maximize) *)
+  order : int (* ordering assigned by the user for this variable *)
+}
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 43248121bf..a258b5d4d7 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -73,7 +73,7 @@ module type S = sig
 
   val get_assumed : t -> E.Set.t
   val reinit_cpt : unit -> unit
-  val get_objectives : t -> Th_util.optimized_split Util.MI.t
+  val get_objectives : t -> Shostak.Combine.r Th_util.optimized_split Util.MI.t
 end
 
 module Main_Default : S = struct
@@ -359,7 +359,7 @@ module Main_Default : S = struct
     gamma : CC_X.t;
     gamma_finite : CC_X.t;
     choices : choice list;
-    objectives : Th_util.optimized_split Util.MI.t;
+    objectives : Shostak.Combine.r Th_util.optimized_split Util.MI.t;
   }
 
   let add_explanations_to_splits l =
@@ -382,7 +382,7 @@ module Main_Default : S = struct
       assert false
 
 
-  exception Found of Th_util.optimized_split
+  exception Found of Shostak.Combine.r Th_util.optimized_split
 
   (* TODO: this function could be optimized if "objectives" structure
      is coded differently *)
@@ -390,24 +390,24 @@ module Main_Default : S = struct
     try
       Util.MI.iter (fun _ x ->
           match x.Th_util.value with
-          | Value _ ->
+          | `Value _ ->
             ()
-          | Pinfinity | Minfinity ->
+          | `Pinfinity | `Minfinity ->
             (* We should block case-split at infinite values.
-               Otherwise. Otherwise, we may have soundness issues. We
+               Otherwise, we may have soundness issues. We
                may think an objective is unbounded, but some late
                constraints may make it bounded.
 
                An alternative is to only allow further splits when we
-               know that no extra-assumpptions will be propagated to
+               know that no extra-assumptions will be propagated to
                the env. Hence the test 'if for_model' *)
             if for_model then ()
             else
-              raise (Found { x with Th_util.value = Unknown })
+              raise (Found { x with value = `Unknown })
 
-          | Unknown ->
-            raise (Found { x with Th_util.value = Unknown })
-        )env.objectives;
+          | `Unknown ->
+            raise (Found { x with value = `Unknown })
+        ) env.objectives;
       None
     with Found x ->
       Some x
@@ -425,10 +425,10 @@ module Main_Default : S = struct
              acc
            else
              match v.Th_util.value with
-             | Th_util.Unknown -> acc (* not optimized yet *)
-             | Value _ -> Util.MI.add ord {v with value = Unknown} acc
-             | Pinfinity | Minfinity -> assert false (* may happen? *)
-        )objectives objectives
+             | `Unknown -> acc (* not optimized yet *)
+             | `Value _ -> Util.MI.add ord {v with value = `Unknown} acc
+             | `Pinfinity | `Minfinity -> assert false (* may happen? *)
+        ) objectives objectives
 
   let look_for_sat ?(bad_last=None) ch env l ~for_model =
     let rec aux ch bad_last dl env li =
@@ -454,15 +454,15 @@ module Main_Default : S = struct
             let env = {env with objectives = to_opt} in
             begin
               match u.value with
-              | Value v ->
+              | `Value v ->
                 let splits = add_explanations_to_splits [v] in
                 aux ch None dl env splits
-              | Pinfinity | Minfinity ->
+              | `Pinfinity | `Minfinity ->
                 if for_model then
                   aux ch None dl env []
                 else
                   { env with choices = List.rev dl }, ch
-              | Unknown -> assert false
+              | `Unknown -> assert false
             end
 
         end
@@ -565,7 +565,7 @@ module Main_Default : S = struct
 
 
   let reset_objectives objectives =
-    Util.MI.map (fun x -> Th_util.({ x with value = Unknown }) ) objectives
+    Util.MI.map (fun x -> Th_util.({ x with value = `Unknown }) ) objectives
 
   let reset_case_split_env t =
     { t with
@@ -581,9 +581,9 @@ module Main_Default : S = struct
     Util.MI.for_all
       (fun _ {Th_util.value; _} ->
          match value with
-         | Pinfinity | Minfinity -> false
-         | Value _ | Unknown -> true
-      )objectives
+         | `Pinfinity | `Minfinity -> false
+         | `Value _ | `Unknown -> true
+      ) objectives
 
   let try_it t facts ~for_model =
     Options.exec_thread_yield ();
@@ -703,7 +703,7 @@ module Main_Default : S = struct
                  (* gamma is already initialized with fresh terms *)
                  assert false
              in
-             let x = Th_util.{ r; e; value = Unknown; is_max; order } in
+             let x = Th_util.{ r; e; value = `Unknown; is_max; order } in
              begin
                try
                  let y = Util.MI.find order objectives in
diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli
index 85a8ee3a3a..cf53c83c14 100644
--- a/src/lib/reasoners/theory.mli
+++ b/src/lib/reasoners/theory.mli
@@ -62,7 +62,7 @@ module type S = sig
 
   val get_assumed : t -> Expr.Set.t
   val reinit_cpt : unit -> unit
-  val get_objectives : t -> Th_util.optimized_split Util.MI.t
+  val get_objectives : t -> Shostak.Combine.r Th_util.optimized_split Util.MI.t
 end
 
 module Main_Default : S
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 0c0a7d260e..7a5e92e161 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1000,45 +1000,45 @@ let assign_next env =
   res, env
 
 (**** Counter examples functions ****)
-let is_a_good_model_value (x, _) =
-  match X.leaves x with
+(* let is_a_good_model_value (x, _) =
+   match X.leaves x with
     [] -> true
-  | [y] -> X.equal x y
-  | _ -> false
+   | [y] -> X.equal x y
+   | _ -> false *)
 
-let is_const_term (x, _) =
-  match X.term_extract x with
-  | Some t, _ ->
+(* let is_const_term (x, _) =
+   match X.term_extract x with
+   | Some t, _ ->
     E.const_term t
-  | _ ->
+   | _ ->
     (*cannot test for theories which don't implement term_extract*)
-    true
+    true *)
 
-let model_repr_of_term t env mrepr unbounded =
-  try ME.find t mrepr, mrepr
+let model_repr_of_term ?(unbounded:[`Pinfinity | `Minfinity] option)
+    t env mrepr =
+  try
+    ME.find t mrepr, mrepr
   with Not_found ->
     let mk = try ME.find t env.make with Not_found -> assert false in
-    let rep,_ = try MapX.find mk env.repr with Not_found -> assert false in
-    match unbounded with
-    | Some string_repr -> (rep, string_repr), mrepr
-    | None ->
-      let cls =
-        try SE.elements (MapX.find rep env.classes)
-        with Not_found -> assert false
-      in
-      let cls =
-        try List.rev_map (fun s -> s, ME.find s env.make) cls
-        with Not_found -> assert false
-      in
-      let e = X.choose_adequate_model t rep cls in
-      e, ME.add t e mrepr
+    let rep, _ = try MapX.find mk env.repr with Not_found -> assert false in
+    let cls =
+      try SE.elements (MapX.find rep env.classes)
+      with Not_found -> assert false
+    in
+    let cls =
+      try List.rev_map (fun s -> s, ME.find s env.make) cls
+      with Not_found -> assert false
+    in
+    let e = X.Value.choose ?unbounded t rep cls in
+    (* TODO: shouldn't put the infinity model values in the mrepr? *)
+    e, ME.add t e mrepr
 
 let is_optimization_op = function
   | Sy.Op Sy.Optimize _ -> true
   | _ -> false
 
-let compute_concrete_model_of_val
-    env t ((fprofs, cprofs, carrays, mrepr) as acc) unbounded =
+let compute_concrete_model_of_val ?(unbounded:[`Pinfinity | `Minfinity] option)
+    env t ((fprofs, cprofs, carrays, mrepr) as acc) =
   let { E.f; xs; ty; _ } = E.term_view t in
   if X.is_solvable_theory_symbol f ty
   || E.is_fresh t || E.is_fresh_skolem t
@@ -1050,28 +1050,23 @@ let compute_concrete_model_of_val
     let xs, tys, mrepr =
       List.fold_left
         (fun (xs, tys, mrepr) x ->
-           let rep_x, mrepr = model_repr_of_term x env mrepr None in
-           assert (is_const_term rep_x);
-           (x, rep_x)::xs,
+           let v_x, mrepr = model_repr_of_term x env mrepr in
+           (x, v_x) :: xs,
            (E.type_info x)::tys,
            mrepr
         ) ([],[], mrepr) (List.rev xs)
     in
-    let rep, mrepr = model_repr_of_term t env mrepr unbounded in
-    assert (is_a_good_model_value rep);
-    assert (is_const_term rep);
+    let v, mrepr = model_repr_of_term ?unbounded t env mrepr in
     match f, xs, ty with
     | Sy.Op Sy.Set, _, _ -> acc
 
-    | Sy.Op Sy.Get, [(_,(a,_));((_,(i,_)) as e)], _ ->
+    | Sy.Op Sy.Get, [(_, a); ((t, _) as e)], _ ->
       begin
-        match X.term_extract a with
-        | Some ta, true ->
-          let { E.f = f_ta; xs=xs_ta; _ } = E.term_view ta in
-          assert (xs_ta == []);
+        match X.Value.extract a with
+        | Some (sy, ty) ->
           fprofs,
           cprofs,
-          ModelMap.add (f_ta,[X.type_info i], ty) ([e], rep) carrays,
+          ModelMap.add (sy, [Expr.type_info t], ty) ([e], v) carrays,
           mrepr
 
         | _ -> assert false
@@ -1079,10 +1074,10 @@ let compute_concrete_model_of_val
 
     | _ ->
       if tys == [] then
-        fprofs, ModelMap.add (f, tys, ty) (xs, rep) cprofs, carrays,
+        fprofs, ModelMap.add (f, tys, ty) (xs, v) cprofs, carrays,
         mrepr
       else
-        ModelMap.add (f, tys, ty) (xs, rep) fprofs, cprofs, carrays,
+        ModelMap.add (f, tys, ty) (xs, v) fprofs, cprofs, carrays,
         mrepr
 
 
@@ -1107,11 +1102,11 @@ let compute_concrete_model ?(inline_obj_in_model=Util.MI.empty) env =
       (fun _ord v ((bounded, pinfty, minfty) as acc) ->
          let {Th_util.value; r; order = _; is_max = _; e=_} = v in
          match value with
-         | Value _ ->
+         | `Value _ ->
            SetX.add v.Th_util.r bounded, pinfty, minfty
-         | Pinfinity  -> bounded, SetX.add r pinfty, minfty
-         | Minfinity -> bounded, pinfty, SetX.add r minfty
-         | Unknown -> acc
+         | `Pinfinity  -> bounded, SetX.add r pinfty, minfty
+         | `Minfinity -> bounded, pinfty, SetX.add r minfty
+         | `Unknown -> acc
       ) inline_obj_in_model (SetX.empty, SetX.empty, SetX.empty)
   in
   let not_unbounded = pinfty == SetX.empty && minfty == SetX.empty in
@@ -1123,16 +1118,18 @@ let compute_concrete_model ?(inline_obj_in_model=Util.MI.empty) env =
     (fun t mk acc ->
        if SetX.mem mk pinfty then
          (* mk's optimum is +infinity *)
-         compute_concrete_model_of_val env t acc (Some "+oo")
+         compute_concrete_model_of_val ~unbounded:`Pinfinity
+           env t acc
        else
        if SetX.mem mk minfty then
          (* mk's optimum is -infinity *)
-         compute_concrete_model_of_val env t acc (Some "-oo")
+         compute_concrete_model_of_val ~unbounded:`Minfinity
+           env t acc
        else
        if not_unbounded || SetX.mem mk bounded then
          (* either the pb is bounded (or it isn't an optimization pb)
             or we have an optimum for mk *)
-         compute_concrete_model_of_val env t acc None
+         compute_concrete_model_of_val env t acc
        else
          acc
     ) (terms env)
@@ -1140,10 +1137,7 @@ let compute_concrete_model ?(inline_obj_in_model=Util.MI.empty) env =
       ModelMap.empty, (* functions profile *)
       ModelMap.empty, (* constants profile *)
       ModelMap.empty, (* arrays profile *)
-      (Expr.Map.empty : (r * string) Expr.Map.t) (* a mapping from terms to
-                                                    representatives/values in
-                                                    model as a semantic value and
-                                                    as a string *)
+      (Expr.Map.empty : X.Value.t Expr.Map.t)
     )
 
 let save_cache () = LX.save_cache ()
@@ -1153,7 +1147,7 @@ let reinit_cache () = LX.reinit_cache ()
 let compute_objectives optimized_splits env mrepr =
   let seen_infinity = ref false in
   Util.MI.map
-    (fun {Th_util.e; value; r=_; is_max=_; order=_} ->
+    (fun {Th_util.e; value; r = _ ; is_max = _ ; order = _ } ->
        e,
        (if !seen_infinity then begin
            (* every objective after 'oo' is printed as ]-oo, +oo[ *)
@@ -1161,12 +1155,12 @@ let compute_objectives optimized_splits env mrepr =
          end
         else
           match value with
-          | Pinfinity -> seen_infinity := true; Obj_pinfty
-          | Minfinity -> seen_infinity := true; Obj_minfty
-          | Value _ ->
-            let (_r_x, r_s), _mrepr = model_repr_of_term e env mrepr None in
-            Obj_val r_s
-          | Unknown ->
+          | `Pinfinity -> seen_infinity := true; Obj_pinfty
+          | `Minfinity -> seen_infinity := true; Obj_minfty
+          | `Value _ ->
+            let v, _mrepr = model_repr_of_term e env mrepr in
+            Obj_val v
+          | `Unknown ->
             (* in this case, we should have !seen_infinity == true.
                Which is handled in the if branch. Moreover, we
                continue optimization now even if infinity is
diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli
index 7485e7b7a7..e23487902f 100644
--- a/src/lib/reasoners/uf.mli
+++ b/src/lib/reasoners/uf.mli
@@ -74,7 +74,7 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t
 (** Compute a counterexample using the Uf environment *)
 val extract_concrete_model :
   prop_model:Expr.Set.t ->
-  optimized_splits:Th_util.optimized_split Util.MI.t ->
+  optimized_splits:Shostak.Combine.r Th_util.optimized_split Util.MI.t ->
   t ->
   Models.t Lazy.t option
 
diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml
index aa5d2ba19c..4498518396 100644
--- a/src/lib/structures/errors.ml
+++ b/src/lib/structures/errors.ml
@@ -201,12 +201,12 @@ let report_typing_error fmt = function
   | MatchNotExhaustive missing ->
     fprintf fmt
       "Pattern-matching is not exhaustive. These cases are missing: %a"
-      (Util.print_list ~sep:" |" ~pp:Hstring.print) missing
+      (Util.print_list ~sep:" |" ~pp:Hstring.pp) missing
   | MatchUnusedCases dead ->
     fprintf fmt
       "Pattern-matching contains unreachable cases. These cases are\
        removed: %a"
-      (Util.print_list ~sep:" |" ~pp:Hstring.print) dead
+      (Util.print_list ~sep:" |" ~pp:Hstring.pp) dead
   | NotAdtConstr (lbl, ty) ->
     fprintf fmt
       "The identifiant %s is not a constructor of an algebraic data type. \
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index baf318ffc6..87e57df339 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -390,10 +390,10 @@ module SmtPrinter = struct
       fprintf fmt "(not %a)" print a
 
     | Sy.L_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "((_ is %a) %a)" Hstring.print hs print e
+      fprintf fmt "((_ is %a) %a)" Hstring.pp hs print e
 
     | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "(not ((_ is %a) %a))" Hstring.print hs print e
+      fprintf fmt "(not ((_ is %a) %a))" Hstring.pp hs print e
 
     | (Sy.L_built (Sy.LT | Sy.LE) | Sy.L_neg_built (Sy.LT | Sy.LE)
       | Sy.L_neg_pred | Sy.L_eq | Sy.L_neg_eq
@@ -470,14 +470,14 @@ module SmtPrinter = struct
     (* TODO: introduce PrefixOp in the future to simplify this ? *)
     | Sy.Op (Sy.Constr hs), ((_::_) as l) ->
       fprintf fmt
-        "%a(%a)" Hstring.print hs (Util.print_list ~sep:"," ~pp:print) l
+        "%a(%a)" Hstring.pp hs (Util.print_list ~sep:"," ~pp:print) l
 
     | Sy.Op _, [e1; e2] ->
       fprintf fmt "(%a %a %a)" Sy.print f print e1 print e2
 
     | Sy.Op Sy.Destruct (hs, grded), [e] ->
       fprintf fmt "%a#%s%a"
-        print e (if grded then "" else "!") Hstring.print hs
+        print e (if grded then "" else "!") Hstring.pp hs
 
 
     | Sy.In(lb, rb), [t] ->
@@ -568,10 +568,10 @@ module AEPrinter = struct
       fprintf fmt "(not %a)" print a
 
     | Sy.L_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "(%a ? %a)" print e Hstring.print hs
+      fprintf fmt "(%a ? %a)" print e Hstring.pp hs
 
     | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
-      fprintf fmt "not (%a ? %a)" print e Hstring.print hs
+      fprintf fmt "not (%a ? %a)" print e Hstring.pp hs
 
     | (Sy.L_built (Sy.LT | Sy.LE) | Sy.L_neg_built (Sy.LT | Sy.LE)
       | Sy.L_neg_pred | Sy.L_eq | Sy.L_neg_eq
@@ -648,7 +648,7 @@ module AEPrinter = struct
     (* TODO: introduce PrefixOp in the future to simplify this ? *)
     | Sy.Op (Sy.Constr hs), ((_::_) as l) ->
       fprintf fmt "%a(%a)"
-        Hstring.print hs (Util.print_list ~sep:"," ~pp:print) l
+        Hstring.pp hs (Util.print_list ~sep:"," ~pp:print) l
 
     | Sy.Op _, [e1; e2] ->
       if Options.get_output_smtlib () then
@@ -658,7 +658,7 @@ module AEPrinter = struct
 
     | Sy.Op Sy.Destruct (hs, grded), [e] ->
       fprintf fmt "%a#%s%a"
-        print e (if grded then "" else "!") Hstring.print hs
+        print e (if grded then "" else "!") Hstring.pp hs
 
 
     | Sy.In(lb, rb), [t] ->
@@ -2511,7 +2511,7 @@ let debug_compile_match e cases res =
          | Typed.Constr {name; args} ->
            Printer.print_dbg  ~flushed:false ~header:false
              "| %a %a -> %a@ "
-             Hstring.print name
+             Hstring.pp name
              p_list_vars args
              print v;
          | Typed.Var x ->
diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml
index ff06afff06..f6ecb96742 100644
--- a/src/lib/structures/modelMap.ml
+++ b/src/lib/structures/modelMap.ml
@@ -33,10 +33,11 @@ module X = Shostak.Combine
 module Sy = Symbols
 module E = Expr
 
+type key = Symbols.t * Ty.t list * Ty.t
 
 module P = Map.Make
     (struct
-      type t = Sy.t * Ty.t list * Ty.t
+      type t = key
 
       let (|||) c1 c2 = if c1 <> 0 then c1 else c2
 
@@ -60,16 +61,19 @@ module P = Map.Make
 
 module V = Set.Make
     (struct
-      type t = (E.t * (X.r * string)) list * (X.r * string)
-      let compare (l1, (v1,_)) (l2, (v2,_)) =
-        let c = X.hash_cmp v1 v2 in
+      type t =
+        (Expr.t * Shostak.Combine.Value.t) list *
+        Shostak.Combine.Value.t
+
+      let compare (l1, v1) (l2, v2) =
+        let c = X.Value.compare v1 v2 in
         if c <> 0 then c
         else
           let c = ref 0 in
           try
             List.iter2
-              (fun (_,(x,_)) (_,(y,_)) ->
-                 let d = X.hash_cmp x y in
+              (fun (_, v3) (_, v4) ->
+                 let d = X.Value.compare v3 v4 in
                  if d <> 0 then begin c := d; raise Exit end
               ) l1 l2;
             !c
@@ -78,7 +82,6 @@ module V = Set.Make
           | Invalid_argument _ -> List.length l1 - List.length l2
     end)
 
-type key = P.key
 type elt = V.t
 
 type t = {
diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli
index c9584a88e3..ee1cdf7a6f 100644
--- a/src/lib/structures/modelMap.mli
+++ b/src/lib/structures/modelMap.mli
@@ -33,14 +33,14 @@
     of expressions matching the P.key type (V).
 *)
 
-module P : Map.S with type key =
-                        Symbols.t * Ty.t list * Ty.t
+type key = Symbols.t * Ty.t list * Ty.t
+
+module P : Map.S with type key = key
 
 module V : Set.S with type elt =
-                        (Expr.t * (Shostak.Combine.r * string)) list *
-                        (Shostak.Combine.r * string)
+                        (Expr.t * Shostak.Combine.Value.t) list *
+                        Shostak.Combine.Value.t
 
-type key = P.key
 type elt = V.t
 
 type t
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index bcbcdcf585..4be3ec0c27 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -60,9 +60,9 @@ module Smtlib = struct
       Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t
     | Tsum (name, _) | Text ([], name)
     | Trecord { args = []; name; _ } | Tadt (name, []) ->
-      Fmt.pf ppf "%a" Hstring.print name
+      Fmt.pf ppf "%a" Hstring.pp name
     | Text (args, name) | Trecord { args; name; _ } | Tadt (name, args) ->
-      Fmt.(pf ppf "(@[%a %a@])" Hstring.print name (list ~sep:sp pp) args)
+      Fmt.(pf ppf "(@[%a %a@])" Hstring.pp name (list ~sep:sp pp) args)
     | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v
     | Tvar { value = Some t; _ } -> pp ppf t
 end
@@ -164,10 +164,10 @@ let print_generic body_of =
   and print_adt_tuple fmt = function
     | [] -> ()
     | (d, e)::l ->
-      Format.fprintf fmt " of { %a : %a " Hstring.print d (print None) e;
+      Format.fprintf fmt " of { %a : %a " Hstring.pp d (print None) e;
       List.iter
         (fun (d, e) ->
-           Format.fprintf fmt "; %a : %a " Hstring.print d (print None) e
+           Format.fprintf fmt "; %a : %a " Hstring.pp d (print None) e
         ) l;
       Format.fprintf fmt "}"
 
@@ -503,7 +503,7 @@ module Decls = struct
         add name params body;
         body
     with Not_found ->
-      Printer.print_err "%a not found" Hstring.print name;
+      Printer.print_err "%a not found" Hstring.pp name;
       assert false
 
   let reinit () = decls := MH.empty
diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml
index 3aa89f41d4..a09a100740 100644
--- a/src/lib/structures/typed.ml
+++ b/src/lib/structures/typed.ml
@@ -266,7 +266,7 @@ let rec print_term =
         (fun (p, v) ->
            match p with
            | Constr {name = n; args = l} ->
-             fprintf fmt "| %a %a -> %a\n" Hstring.print n pp_vars l
+             fprintf fmt "| %a %a -> %a\n" Hstring.pp n pp_vars l
                print_term v
            | Var x ->
              fprintf fmt "| %a -> %a\n" Var.print x print_term v;
diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml
index 4f2871a1e4..f9651cbdb2 100644
--- a/src/lib/structures/xliteral.ml
+++ b/src/lib/structures/xliteral.ml
@@ -121,7 +121,7 @@ let print_view ?(lbl="") pr_elt fmt vw =
 
   | Builtin (pos, IsConstr hs, [e]) ->
     Format.fprintf fmt "%s(%a ? %a)"
-      (if pos then "" else "not ") pr_elt e Hstring.print hs
+      (if pos then "" else "not ") pr_elt e Hstring.pp hs
 
   | Builtin (_, IsConstr _, _) ->
     assert false (* not reachable *)
diff --git a/src/lib/util/hstring.ml b/src/lib/util/hstring.ml
index 77d04aea4a..1a2ff3fafc 100644
--- a/src/lib/util/hstring.ml
+++ b/src/lib/util/hstring.ml
@@ -44,7 +44,7 @@ let make s = HC.make {content = s; id = - 1}
 
 let view s = s.content
 
-let print fmt v = Format.fprintf fmt "%s" (view v)
+let pp ppf v = Fmt.pf ppf "%s" (view v)
 
 let equal s1 s2 = s1.id == s2.id
 
diff --git a/src/lib/util/hstring.mli b/src/lib/util/hstring.mli
index 9a7f4f0d5a..3afddd038e 100644
--- a/src/lib/util/hstring.mli
+++ b/src/lib/util/hstring.mli
@@ -34,7 +34,7 @@ val make : string -> t
 
 val view : t -> string
 
-val print : Format.formatter -> t -> unit
+val pp : Format.formatter -> t -> unit
 
 val equal : t -> t -> bool
 
diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli
index 31636e8eed..2bd2943a5a 100644
--- a/src/lib/util/util.mli
+++ b/src/lib/util/util.mli
@@ -108,16 +108,19 @@ val loop:
   init : 'b ->
   'b
 
+(* TODO: use Fmt.list *)
 val print_list:
   sep:string ->
   pp:(Format.formatter -> 'a -> unit) ->
   Format.formatter -> 'a list -> unit
 
+(* TODO: use Fmt.list *)
 val print_list_pp:
   sep:(Format.formatter -> unit -> unit) ->
   pp:(Format.formatter -> 'a -> unit) ->
   Format.formatter -> 'a list -> unit
 
+(* TODO: use Fmt.failwith *)
 val failwith: ('a, Format.formatter, unit, 'b) format4 -> 'a
 
 val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a
diff --git a/src/parsers/psmt2_to_alt_ergo.ml b/src/parsers/psmt2_to_alt_ergo.ml
index a406e240f6..dd62b78784 100644
--- a/src/parsers/psmt2_to_alt_ergo.ml
+++ b/src/parsers/psmt2_to_alt_ergo.ml
@@ -482,9 +482,6 @@ module Translate = struct
     | Cmd_SetInfo _ -> not_supported "set-info"; acc
     | Cmd_Push n -> translate_push_pop mk_push n (pos command) :: acc
     | Cmd_Pop n -> translate_push_pop mk_pop n (pos command) :: acc
-    | Cmd_CheckAllSat _ -> not_supported "check-all-sat"; acc
-    | Cmd_Maximize _ -> not_supported "maximize"; acc
-    | Cmd_Minimize _ -> not_supported "minimize"; acc
     | Cmd_Exit -> acc
 
   let init () =
diff --git a/tests/models/bool/bool1.models.smt2 b/tests/models/bool/bool1.models.smt2
index a7fde5136e..1f22210cba 100644
--- a/tests/models/bool/bool1.models.smt2
+++ b/tests/models/bool/bool1.models.smt2
@@ -2,14 +2,10 @@
 (set-option :produce-models true) ; enable model generation
 (declare-const p Bool)
 (declare-const q Bool)
-; (declare-const t Int)
 (define-fun nq () Bool q)
 (assert (=> (not p) (not nq)))
 (check-sat)
 (get-model)
-(get-assignment)
 (assert q)
 (check-sat)
 (get-model)
-(get-assignment)
-(exit)