diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index afa71e83d2..f78f955c13 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -27,13 +27,11 @@ let constraints = ref MS.empty
 type t = {
   propositional : Expr.Set.t;
   model : ModelMap.t;
-  term_values : Expr.t Expr.Map.t
 }
 
 let empty = {
   propositional = Expr.Set.empty;
   model = ModelMap.empty ~suspicious:false [];
-  term_values = Expr.Map.empty;
 }
 
 module Pp_smtlib_term = struct
diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli
index 75b21ef841..dfafbe7e4e 100644
--- a/src/lib/frontend/models.mli
+++ b/src/lib/frontend/models.mli
@@ -21,8 +21,6 @@
 type t = {
   propositional : Expr.Set.t;
   model : ModelMap.t;
-  term_values : Expr.t Expr.Map.t
-  (** A map from terms to their values in the model. *)
 }
 
 val empty : t
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index fca71829f6..cfd06fcbbd 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -418,15 +418,15 @@ module Shostak (X : ALIEN) = struct
        in [Adt_rel]. *)
     None
 
-  let to_model_term r =
+  let to_model_term abstract r =
     match embed r with
     | Constr { c_name; c_ty; c_args } ->
       let args =
-        My_list.try_map (fun (_, arg) -> X.to_model_term arg) c_args
+        My_list.try_map (fun (_, arg) -> X.to_model_term abstract arg) c_args
       in
       Option.bind args @@ fun args ->
       Some (E.mk_constr c_name args c_ty)
 
     | Select _ -> None
-    | Alien a -> X.to_model_term a
+    | Alien a -> X.to_model_term abstract a
 end
diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml
index afc1b7ae91..0738cd896b 100644
--- a/src/lib/reasoners/arith.ml
+++ b/src/lib/reasoners/arith.ml
@@ -744,7 +744,7 @@ module Shostak
         cpt := Q.add Q.one (max_constant distincts !cpt);
         Some (term_of_cst (Q.to_string !cpt), true)
 
-  let to_model_term r =
+  let to_model_term _abstract r =
     match P.is_const (embed r), X.type_info r with
     | Some i, Ty.Tint ->
       assert (Z.equal (Q.den i) Z.one);
diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index e05e3c93fd..8c6e1d4b4b 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -1584,7 +1584,7 @@ module Shostak(X : ALIEN) = struct
         let bv = String.make sz '0' in
         Some (E.bitv bv (Ty.Tbitv sz), true)
 
-  let to_model_term r =
+  let to_model_term _abstract r =
     match embed r with
     | [{ bv = Cte b; sz }] ->
       let s = Z.format ("%0" ^ string_of_int sz ^ "b") b in
diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index bc6c2a452f..102e654e4d 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -401,7 +401,7 @@ module Shostak (X : ALIEN) = struct
         Some (s, false) (* false <-> not a case-split *)
       | _ -> assert false
 
-  let to_model_term =
+  let to_model_term abstract =
     let rec to_model_term r =
       match r with
       | Record (fields, ty) ->
@@ -414,7 +414,7 @@ module Shostak (X : ALIEN) = struct
         Some (E.mk_term Sy.(Op Record) l ty)
 
       | Other (a, _) ->
-        X.to_model_term a
+        X.to_model_term abstract a
       | Access _ -> None
     in fun r -> to_model_term (embed r)
 end
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index 919783407a..ee0d8dc23a 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -232,14 +232,20 @@ struct
     | Ac _ -> None, false (* SYLVAIN : TODO *)
     | Term t -> Some t, true
 
-  let to_model_term r =
+  let to_model_term abstract r =
     let res =
       match r.v with
-      | Arith _ -> ARITH.to_model_term r
-      | Records _ -> RECORDS.to_model_term r
-      | Bitv _ -> BITV.to_model_term r
-      | Adt _ -> ADT.to_model_term r
-      | Term t when Expr.is_model_term t -> Some t
+      | Arith _ -> ARITH.to_model_term abstract r
+      | Records _ -> RECORDS.to_model_term abstract r
+      | Bitv _ -> BITV.to_model_term abstract r
+      | Adt _ -> ADT.to_model_term abstract r
+      | Term t when Expr.is_model_term t ->
+        let Expr.{ f; _ } = Expr.term_view t in
+        (match f with
+         | Symbols.Name { ns = Internal | Fresh | Fresh_ac; _ } ->
+           Some (abstract t)
+         | _ ->
+           Some t)
       | Ac _ | Term _ -> None
     in
     Option.bind res @@ fun t ->
diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli
index 3050e1f23b..cc17921b55 100644
--- a/src/lib/reasoners/sig.mli
+++ b/src/lib/reasoners/sig.mli
@@ -137,24 +137,24 @@ module type SHOSTAK = sig
      [Some (t, false)], then there must be no context in which
      [solve r (fst X.make t)] raises [Unsolvable]. You have been warned! *)
 
-  val to_model_term : r -> Expr.t option
-  (** [to_model_term r] creates a model term if [r] is constant.
-      The function cannot fail if [r] is a constant (that is statisfied the
-      predicate [X.is_constant]).
-
-      The returned value always satisfies the predicate
-      [Expr.is_model_term]. See its documentation for more details about
-      model terms. *)
+  val to_model_term : (Expr.t -> Expr.t) -> r -> Expr.t option
+  (** [to_model_term abstract r] creates a model term if [r] is constant.
+      The function must succeed when [r] is a constant, this is [r] satisfied
+      the predicate [X.is_constant].
+
+      The [abstract] function is used to replace internal or fresh names by
+      abstract values.
+
+      The returned value always satisfies the predicate [Expr.is_model_term].
+      Refer to its documentation for more details about model terms. *)
 end
 
 module type X = sig
   type r
 
   val save_cache : unit -> unit
-  (** saves the module's current cache *)
 
   val reinit_cache : unit -> unit
-  (** restores the module's cache *)
 
   val make : Expr.t -> r * Expr.t list
 
@@ -178,7 +178,7 @@ module type X = sig
 
   val term_embed : Expr.t -> r
 
-  val term_extract : r -> Expr.t option * bool (* original term ? *)
+  val term_extract : r -> Expr.t option * bool
 
   val ac_embed : r ac -> r
 
@@ -196,19 +196,8 @@ module type X = sig
 
   val is_solvable_theory_symbol : Symbols.t -> bool
 
-  (* the returned bool is true when the returned term in a constant of the
-     theory. Otherwise, the term contains aliens that should be assigned
-     (eg. records). In this case, it's a unit fact, not a decision
-  *)
   val assign_value :
     r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
 
-  val to_model_term : r -> Expr.t option
-  (** [to_model_term r] creates a model term if [r] is constant.
-      The function cannot fail if [r] is a constant (that is statisfied the
-      predicate [X.is_constant]).
-
-      The returned value always satisfies the predicate
-      [Expr.is_model_term]. See its documentation for more details about
-      model terms. *)
+  val to_model_term : (Expr.t -> Expr.t) -> r -> Expr.t option
 end
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 0d94864e6b..33d21f344b 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1085,20 +1085,6 @@ let reinit_cache () =
 (*                      Model generation functions                          *)
 (****************************************************************************)
 
-let model_repr_of_term 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
-    (* We call this function during the model generation only. At this time,
-       we are sure that class representatives are constant semantic values, or
-       uninterpreted names. *)
-    match X.to_model_term rep with
-    | Some v -> v, ME.add t v mrepr
-    | None ->
-      (* [X.to_model_term] cannot fail on constant semantic values. *)
-      assert false
-
 (* A map of expressions to terms, ordered by depth first, and then by
    [Expr.compare] for expressions with same depth. This structure will
    be used to build a model, by starting with the inner/smaller terms
@@ -1128,63 +1114,58 @@ let terms env =
        let Expr.{ f; _ } = Expr.term_view t in
        match f with
        | Name { defined = true; _ } ->
-         (* We don't store names defined by the user. *)
+         (* We do not store names defined by the user. *)
          acc
        | _ ->
          let suspicious = is_suspicious_symbol f || suspicious in
          MED.add t r terms, suspicious
     ) env.make (MED.empty, false)
 
-(* Helper functions used by the caches during the computation of the model. *)
-module Cache = struct
-  let store_array_get arrays_cache (t : E.t) (i : E.t) (v : E.t) =
-    match E.Table.find arrays_cache t with
-    | exception Not_found ->
-      let values = E.Table.create 17 in
-      E.Table.add values i v;
-      E.Table.add arrays_cache t values
-    | values ->
-      E.Table.replace values i v
-
-  let get_abstract_for abstracts_cache env (t : E.t) =
-    let r, _ = find env t in
-    match Shostak.HX.find abstracts_cache r with
-    | exception Not_found ->
-      let abstract = E.mk_abstract (E.type_info t) in
-      Shostak.HX.add abstracts_cache r abstract;
-      abstract
-    | abstract -> abstract
-end
-
-type cache = {
-  array_selects: Expr.t E.Table.t E.Table.t;
-  (** Stores all the get accesses to array names. *)
-
-  abstracts: Expr.t Shostak.HX.t;
-  (** Stores all the abstract values generated. This cache is necessary
-      to ensure we do not generate twice an abstract value for a given
-      symbol. *)
-}
-
 let is_destructor = function
   | Sy.Op (Destruct _) -> true
   | _ -> false
 
-(* The environment of the union-find contains almost a first-order model.
-   There are two situations that require some computations to retrieve an
-   appropriate model value:
-   - As our array theory has no semantic values, there are no value
-     which represents an array in the union-find environment. Instead, the
-     union-find stores the collection of all the access to the array. This
-     function retrieves all these accesses in order to build an expression
-     which defines the approriate array.
-   - If the problem involves declared terms whose the type is abstract,
-     Alt-Ergo cannot produces a constant value for them. This function creates
-     a new abstract value in this case. *)
-let compute_concrete_model_of_val cache =
-  let store_array_select = Cache.store_array_get cache.array_selects
-  and get_abstract_for = Cache.get_abstract_for cache.abstracts
-  in fun env t ((mdl, mrepr) as acc) ->
+let model_repr_of_term abstract cache env t =
+  let mk = try ME.find t env.make with Not_found -> assert false in
+  let r, _ = try MapX.find mk env.repr with Not_found -> assert false in
+  match Shostak.HX.find cache r with
+  | exception Not_found -> (
+      (* We call this function during the model generation only. At this time,
+         we are sure that class representatives are constant semantic values, or
+         uninterpreted names. *)
+      match X.to_model_term abstract r with
+      | Some v ->
+        Shostak.HX.replace cache r v;
+        v
+      | None ->
+        (* [X.to_model_term] cannot fail on constant semantic values. *)
+        assert false)
+  | v -> v
+
+let store_select selects (t : E.t) (i : E.t) (v : E.t) =
+  match E.Table.find selects t with
+  | exception Not_found ->
+    let values = E.Table.create 17 in
+    E.Table.add values i v;
+    E.Table.add selects t values
+  | values ->
+    E.Table.replace values i v
+
+(* The union-find environment is almost a first-order model. There are two
+   situations where additional computations are required to retrieve
+   an appropriate model value:
+   1. As our Array theory has no semantic values, there is no single value
+      representing an array in the union-find. Instead, the union-find stores
+      a collection of select terms on this array. This function collects all
+      the selects terms to construct an expression that defines the appropriate
+      array.
+   2. When the problem involves declared terms with abstract types, Alt-Ergo
+      cannot produce a constant value for them. This function creates an
+      abstract value in this case. *)
+let compute_concrete_model_of_val abstract selects cache env =
+  let store_array_select = store_select selects in
+  let model_repr_of_term = model_repr_of_term abstract cache env
+  in fun t mdl ->
     let { E.f; xs; ty; _ } = E.term_view t in
     (* TODO: We have to filter out destructors here as we don't consider
        pending destructors as solvable theory symbols of the ADT theory.
@@ -1195,43 +1176,29 @@ let compute_concrete_model_of_val cache =
     then
       (* These terms are built-in interpreted ones and we don't have
          to produce a definition for them. *)
-      acc
+      mdl
     else
       begin
-        let arg_vals, arg_tys, mrepr =
+        let arg_vals, arg_tys =
           List.fold_left
-            (fun (arg_vals, arg_tys, mrepr) arg ->
-               let rep_arg, mrepr = model_repr_of_term arg env mrepr in
+            (fun (arg_vals, arg_tys) arg ->
+               let rep_arg = model_repr_of_term arg in
                rep_arg :: arg_vals,
-               (Expr.type_info arg) :: arg_tys,
-               mrepr
+               (Expr.type_info arg) :: arg_tys
             )
-            ([], [], mrepr) (List.rev xs)
+            ([], []) (List.rev xs)
         in
-        let ret_rep, mrepr = model_repr_of_term t env mrepr in
+        let ret_rep = model_repr_of_term t in
         match f, arg_vals, ty with
         | Sy.Name _, [], Ty.Tfarray _ ->
           begin
-            match E.Table.find cache.array_selects t with
+            match E.Table.find selects t with
             | exception Not_found ->
               (* We have to add an abstract array in case there is no
                  constraint on its values. *)
-              E.Table.add cache.array_selects t (E.Table.create 17);
-              acc
-            | _ -> acc
-          end
-
-        | Sy.Op Sy.Set, _, _ -> acc
-
-        | Sy.Op Sy.Get, [a; i], _ ->
-          begin
-            let E.{ f = fa; _ } = E.term_view a in
-            match fa with
-            | Sy.Name _ ->
-              store_array_select a i ret_rep;
-              acc
-            | _ ->
-              acc
+              E.Table.add selects t (E.Table.create 17);
+              mdl
+            | _ -> mdl
           end
 
         | Sy.Name { hs = id; _ }, _, _ ->
@@ -1241,10 +1208,23 @@ let compute_concrete_model_of_val cache =
               (* We cannot produce a concrete value as the type is abstract.
                  In this case, we produce an abstract value with the appropriate
                  type. *)
-              get_abstract_for env t
+              abstract t
             | _ -> ret_rep
           in
-          ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr
+          ModelMap.(add (id, arg_tys, ty) arg_vals value mdl)
+
+        | Sy.Op Sy.Set, _, _ -> mdl
+
+        | Sy.Op Sy.Get, [a; i], _ ->
+          begin
+            let E.{ f = fa; _ } = E.term_view a in
+            match fa with
+            | Sy.Name _ ->
+              store_array_select a i ret_rep;
+              mdl
+            | _ ->
+              mdl
+          end
 
         | _ ->
           Printer.print_err
@@ -1253,57 +1233,71 @@ let compute_concrete_model_of_val cache =
           assert false
       end
 
-let extract_concrete_model cache =
-  let compute_concrete_model_of_val = compute_concrete_model_of_val cache in
-  let get_abstract_for = Cache.get_abstract_for cache.abstracts
-  in fun ~prop_model ~declared_ids env ->
-    let terms, suspicious = terms env in
-    let model, mrepr =
-      MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc)
-        terms (ModelMap.empty ~suspicious declared_ids, ME.empty)
-    in
-    let model =
-      E.Table.fold (fun t vals mdl ->
-          (* We produce a fresh identifiant for abstract value in order to
-             prevent any capture. *)
-          let abstract = get_abstract_for env t in
-          let ty = Expr.type_info t in
-          let arr_val =
-            E.Table.fold (fun i v arr_val ->
-                Expr.ArraysEx.store arr_val i v
-              ) vals abstract
-          in
-          let id, is_user =
-            let Expr.{ f; _ } = Expr.term_view t in
-            match f with
-            | Sy.Name { hs; ns = User; _ } -> hs, true
-            | Sy.Name { hs; _ } -> hs, false
-            | _ ->
-              (* Excluded in [compute_concrete_model_of_val] *)
-              assert false
-          in
-          let mdl =
-            if is_user then
-              ModelMap.add (id, [], ty) [] arr_val mdl
-            else
-              (* Internal identifiers can occur here if we need to generate
-                 a model term for an embedded array but this array isn't itself
-                 declared by the user -- see the [embedded-array] test . *)
-              mdl
-          in
-          (* We need to update the model [mdl] in order to substitute all the
-             occurrences of the array identifier [id] by an appropriate model
-             term. This cannot be performed while computing the model with
-             `compute_concrete_model_of_val` because we need to first iterate
-             on all the union-find environment to collect array values. *)
-          ModelMap.subst id arr_val mdl
-        ) cache.array_selects model
-    in
-    { Models.propositional = prop_model; model; term_values = mrepr }
-
-let extract_concrete_model ~prop_model ~declared_ids =
-  let cache : cache = {
-    array_selects = E.Table.create 17;
-    abstracts = Shostak.HX.create 17;
-  }
-  in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env
+let extract_concrete_model ~prop_model ~declared_ids env =
+  let selects : Expr.t E.Table.t E.Table.t =
+    (** Stores all the select terms by arrays. *)
+    E.Table.create 17
+  in
+  let abstract =
+    let cache : Expr.t E.Table.t =
+      (** Caches all generated abstract values. This cache is necessary
+          to prevent from generating duplicate abstract values for the same
+          name. *)
+      E.Table.create 17
+    in fun t ->
+      match E.Table.find cache t with
+      | exception Not_found ->
+        let v = E.mk_abstract (E.type_info t) in
+        E.Table.replace cache t v;
+        v
+      | v -> v
+  in
+  let cache : Expr.t Shostak.HX.t =
+    (** Cache used to memoize results of [model_repr_of_term]. *)
+    Shostak.HX.create 17
+  in
+  let compute_concrete_model_of_val =
+    compute_concrete_model_of_val abstract selects cache env
+  in
+  let terms, suspicious = terms env in
+  let model =
+    MED.fold (fun t _mk mdl -> compute_concrete_model_of_val t mdl)
+      terms (ModelMap.empty ~suspicious declared_ids)
+  in
+  let model =
+    E.Table.fold (fun t vals mdl ->
+        (* Generates a fresh abstract value for the name [t]. *)
+        let a = abstract t in
+        let ty = Expr.type_info t in
+        let arr_val =
+          E.Table.fold (fun i v arr_val ->
+              Expr.ArraysEx.store arr_val i v
+            ) vals a
+        in
+        let id, is_user =
+          let Expr.{ f; _ } = Expr.term_view t in
+          match f with
+          | Sy.Name { hs; ns = User; _ } -> hs, true
+          | Sy.Name { hs; _ } -> hs, false
+          | _ ->
+            (* Excluded in [compute_concrete_model_of_val] *)
+            assert false
+        in
+        let mdl =
+          if is_user then
+            ModelMap.add (id, [], ty) [] arr_val mdl
+          else
+            (* Internal identifiers can occur here if we need to generate
+               a model term for an embedded array but this array is not itself
+               declared by the user -- see the [embedded-array] test . *)
+            mdl
+        in
+        (* We need to update the model [mdl] in order to substitute all the
+           occurrences of the array identifier [id] by an appropriate model
+           term. This cannot be performed while computing the model with
+           `compute_concrete_model_of_val` because we need to first iterate
+           on all the union-find environment to collect array values. *)
+        ModelMap.subst id arr_val mdl
+      ) selects model
+  in
+  { Models.propositional = prop_model; model }
diff --git a/tests/issues/854/function.default.expected b/tests/issues/854/function.default.expected
index 63577badcf..d17389dd52 100644
--- a/tests/issues/854/function.default.expected
+++ b/tests/issues/854/function.default.expected
@@ -2,7 +2,7 @@
 unknown
 (
   (define-fun a () Int 0)
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a5 intref))
   (define-fun f ((_arg_0 Int)) Int 0)
   (define-fun a1 () Int 0)
 )
diff --git a/tests/issues/854/twice_eq.default.expected b/tests/issues/854/twice_eq.default.expected
index 3488c940f2..8897dafab6 100644
--- a/tests/issues/854/twice_eq.default.expected
+++ b/tests/issues/854/twice_eq.default.expected
@@ -3,6 +3,6 @@ unknown
 (
   (define-fun a () Int 0)
   (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
-  (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref))
+  (define-fun another_mk ((_arg_0 Int)) intref (as @a5 intref))
   (define-fun a1 () Int 0)
 )
diff --git a/tests/models/array/embedded-array.default.expected b/tests/models/array/embedded-array.default.expected
index 0cb5c3d3ec..ab83077c09 100644
--- a/tests/models/array/embedded-array.default.expected
+++ b/tests/models/array/embedded-array.default.expected
@@ -2,7 +2,7 @@
 unknown
 (
   (define-fun x () Pair
-   (pair (store (as @a3 (Array Int S)) 0 s)
-         (store (as @a3 (Array Int S)) 0 s)))
+   (pair (store (as @a4 (Array Int S)) 0 s)
+         (store (as @a4 (Array Int S)) 0 s)))
   (define-fun s () S (as @a2 S))
 )