diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index c7545a8ee..259c737ab 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -53,6 +53,12 @@ module HT = Hashtbl.Make(
     let hash = Fun.id
   end)
 
+module DeclSet = Set.Make
+    (struct
+      type t = Id.typed
+      let compare = Id.compare_typed
+    end)
+
 (** Helper function: returns the basename of a dolmen path, since in AE
     the problems are contained in one-file (for now at least), the path is
     irrelevant and only the basename matters *)
@@ -701,8 +707,15 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
     end
   in
   Cache.store_sy tcst sy;
+  Cache.store_ty_vars id_ty;
   (* Adding polymorphic types to the cache. *)
-  Cache.store_ty_vars id_ty
+  let arg_tys, ret_ty =
+    match DT.view id_ty with
+    | `Arrow (arg_tys, ret_ty) ->
+      List.map dty_to_ty arg_tys, dty_to_ty ret_ty
+    | _ -> [], dty_to_ty id_ty
+  in
+  (Hstring.make name, arg_tys, ret_ty)
 
 (** Handles the definitions of a list of mutually recursive types.
     - If one of the types is an ADT, the ADTs that have only one case are
@@ -2087,14 +2100,24 @@ let make dloc_file acc stmt =
             assert false
         ) defs
 
-    | {contents = `Decls [td]; _ } ->
-      begin match td with
-        | `Type_decl (td, _def) -> mk_ty_decl td
-        | `Term_decl td -> mk_term_decl td
-      end;
-      acc
+    | {contents = `Decls [td]; loc; _ } ->
+      let decl = match td with
+        | `Type_decl (td, _def) ->
+          mk_ty_decl td;
+          None
+
+        | `Term_decl td ->
+          Some (mk_term_decl td)
+      in
+      begin match decl with
+        | Some d ->
+          let st_loc = dl_to_ael dloc_file loc in
+          C.{ st_decl = Decl d; st_loc } :: acc
+        | None ->
+          acc
+      end
 
-    | {contents = `Decls dcl; _ } ->
+    | {contents = `Decls dcl; loc; _ } ->
       let rec aux acc tdl =
         (* for now, when acc has more than one element it is assumed that the
            types are mutually recursive. Which is not necessarily the case.
@@ -2107,21 +2130,24 @@ let make dloc_file acc stmt =
             | [otd] -> mk_ty_decl otd
             | _ -> mk_mr_ty_decls (List.rev acc)
           end;
-          mk_term_decl td;
-          aux [] tl
+          let st_loc = dl_to_ael dloc_file loc in
+          C.{ st_decl = Decl (mk_term_decl td); st_loc } :: aux [] tl
 
         | `Type_decl (td, _def) :: tl ->
           aux (td :: acc) tl
 
         | [] ->
-          begin match acc with
-            | [] -> ()
-            | [otd] -> mk_ty_decl otd
-            | _ ->  mk_mr_ty_decls (List.rev acc)
+          begin
+            let () =
+              match acc with
+              | [] -> ()
+              | [otd] -> mk_ty_decl otd
+              | _ ->  mk_mr_ty_decls (List.rev acc)
+            in
+            []
           end
       in
-      aux [] dcl;
-      acc
+      aux [] dcl @ acc
 
     | { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc
 
diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index 10808c3cf..bf5738549 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -302,6 +302,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
     else Ex.empty
 
+  let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit =
+    ignore loc;
+    match env.res with
+    | `Sat | `Unknown ->
+      SAT.declare env.sat_env id
+    | `Unsat -> ()
+
   let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
@@ -443,6 +450,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
   let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
     try
       match d.st_decl with
+      | Decl id -> check_if_over (internal_decl ~loc:d.st_loc id) env
       | Push n -> check_if_over (internal_push ~loc:d.st_loc n) env
       | Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env
       | Assume (n, f, mf) ->
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 457475278..eefc11ce7 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -43,7 +43,7 @@ type t = {
 
 let empty = {
   propositional = Expr.Set.empty;
-  model = ModelMap.empty ~suspicious:false;
+  model = ModelMap.empty ~suspicious:false [];
   term_values = Expr.Map.empty;
 }
 
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index b52c4327c..9eebb0527 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -86,7 +86,10 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+  val extract_concrete_model :
+    prop_model:Expr.Set.t ->
+    declared_ids:Id.typed list ->
+    t -> Models.t
 
 end
 
@@ -748,6 +751,6 @@ module Main : S = struct
     in
     Uf.term_repr env.uf t
 
-  let extract_concrete_model ~prop_model env =
-    Uf.extract_concrete_model ~prop_model env.uf
+  let extract_concrete_model ~prop_model ~declared_ids env =
+    Uf.extract_concrete_model ~prop_model ~declared_ids env.uf
 end
diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli
index 6d6894a17..e8844ac96 100644
--- a/src/lib/reasoners/ccx.mli
+++ b/src/lib/reasoners/ccx.mli
@@ -77,7 +77,10 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+  val extract_concrete_model :
+    prop_model:Expr.Set.t ->
+    declared_ids:Id.typed list ->
+    t -> Models.t
 
 end
 
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index 879645be9..1f65f6e1d 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -177,6 +177,8 @@ module Make (Th : Theory.S) = struct
     unit_facts_cache : (E.gformula * Ex.t) ME.t ref;
     last_saved_model : Models.t Lazy.t option ref;
     unknown_reason : Sat_solver_sig.unknown_reason option;
+    declare_ids : Id.typed Vec.t;
+    declare_lim : int Vec.t;
   }
 
   let reset_refs () =
@@ -1123,7 +1125,8 @@ module Make (Th : Theory.S) = struct
     else begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
-        let model, _ = Th.compute_concrete_model env.tbox in
+        let declared_ids = Vec.to_list env.declare_ids in
+        let model, _ = Th.compute_concrete_model ~declared_ids env.tbox in
         env.last_saved_model := Some model;
         env
       with Ex.Inconsistent (expl, classes) ->
@@ -1611,6 +1614,10 @@ module Make (Th : Theory.S) = struct
           "solved with backward!";
       raise e
 
+  let declare env id =
+    Vec.push env.declare_ids id;
+    env
+
   let push env to_push =
     if Options.get_tableaux_cdcl () then
       Errors.run_error
@@ -1626,6 +1633,7 @@ module Make (Th : Theory.S) = struct
           let guards = ME.add new_guard
               (mk_gf new_guard "" true true,Ex.empty)
               acc.guards.guards in
+          Vec.push env.declare_lim (Vec.size env.declare_ids);
           {acc with guards =
                       { acc.guards with
                         current_guard = new_guard;
@@ -1656,6 +1664,8 @@ module Make (Th : Theory.S) = struct
           in
           acc.model_gen_phase := false;
           env.last_saved_model := None;
+          let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
+          Vec.shrink env.declare_ids lim;
           {acc with inst;
                     guards =
                       { acc.guards with
@@ -1837,6 +1847,8 @@ module Make (Th : Theory.S) = struct
       add_inst = (fun _ -> true);
       last_saved_model = ref None;
       unknown_reason = None;
+      declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
+      declare_lim = Vec.make 17 ~dummy:(-1);
     }
     in
     assume env gf_true Ex.empty
diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli
index ca5382fe6..fc5eee731 100644
--- a/src/lib/reasoners/fun_sat.mli
+++ b/src/lib/reasoners/fun_sat.mli
@@ -40,6 +40,8 @@ module Make (Th : Theory.S) : sig
 
   val empty_with_inst : (Expr.t -> bool) -> t
 
+  val declare : t -> Id.typed -> t
+
   val push : t -> int -> t
 
   val pop : t -> int -> t
diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml
index bad7812b0..b359df929 100644
--- a/src/lib/reasoners/fun_sat_frontend.ml
+++ b/src/lib/reasoners/fun_sat_frontend.ml
@@ -47,6 +47,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | FS.Unsat expl -> raise (Unsat expl)
     | FS.I_dont_know e -> env := e; raise I_dont_know
 
+  let declare t id =
+    t := FS.declare !t id
+
   let push t i = exn_handler (fun env -> t := FS.push env i) t
 
   let pop t i = exn_handler (fun env -> t := FS.pop env i) t
diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml
index 24c2f1f3b..f01169de0 100644
--- a/src/lib/reasoners/sat_solver_sig.ml
+++ b/src/lib/reasoners/sat_solver_sig.ml
@@ -76,6 +76,8 @@ module type S = sig
   val empty : unit -> t
   val empty_with_inst : (Expr.t -> bool) -> t
 
+  val declare : t -> Id.typed -> unit
+
   (** [push env n] add n new assertion levels.
       A guard g is added for every expression e assumed at the current
       assertion level.
diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli
index 72b361905..40e66c05b 100644
--- a/src/lib/reasoners/sat_solver_sig.mli
+++ b/src/lib/reasoners/sat_solver_sig.mli
@@ -56,6 +56,8 @@ module type S = sig
   val empty : unit -> t
   val empty_with_inst : (Expr.t -> bool) -> t
 
+  val declare : t -> Id.typed -> unit
+
   (** [push env n] add n new assertion levels.
       A guard g is added for every expression e assumed at the current
       assertion level.
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 678d855e1..802f8029b 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -67,6 +67,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     mutable unknown_reason : Sat_solver_sig.unknown_reason option;
     (** The reason why satml raised [I_dont_know] if it does; [None] by
         default. *)
+    declare_ids : Id.typed Vec.t;
+    declare_lim : int Vec.t;
   }
 
   let empty_guards () = {
@@ -97,6 +99,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       last_saved_model = None;
       last_saved_objectives = None;
       unknown_reason = None;
+      declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
+      declare_lim = Vec.make 17 ~dummy:(-1);
     }
 
   let empty_with_inst add_inst =
@@ -968,8 +972,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     if compute then begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
+        let declared_ids = Vec.to_list env.declare_ids in
         let model, objectives =
-          Th.compute_concrete_model (SAT.current_tbox env.satml)
+          Th.compute_concrete_model ~declared_ids (SAT.current_tbox env.satml)
         in
         env.last_saved_model <- Some model;
         env.last_saved_objectives <- Some objectives;
@@ -1207,6 +1212,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       expr_guard, atom_guard
     | _ -> assert false
 
+  let declare env id = Vec.push env.declare_ids id
+
   let push env to_push =
     Util.loop ~f:(fun _n () () ->
         try
@@ -1214,7 +1221,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           SAT.push env.satml atom_guard;
           Stack.push expr_guard env.guards.stack_guard;
           Steps.push_steps ();
-          env.guards.current_guard <- expr_guard
+          env.guards.current_guard <- expr_guard;
+          Vec.push env.declare_lim (Vec.size env.declare_ids)
         with
         | Util.Step_limit_reached _ ->
           (* This function should be called without step limit
@@ -1237,7 +1245,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           env.last_saved_model <- None;
           env.last_saved_objectives <- None;
           env.inst <- inst;
-          env.guards.current_guard <- b
+          env.guards.current_guard <- b;
+          let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
+          Vec.shrink env.declare_ids lim
         )
       ~max:to_pop
       ~elt:()
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 4c5a76ff6..1d721a77f 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -61,7 +61,10 @@ module type S = sig
   val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t
 
   val add_term : t -> Expr.t -> add_in_cs:bool -> t
-  val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
+  val compute_concrete_model :
+    t ->
+    declared_ids:Id.typed list ->
+    Models.t Lazy.t * Objective.Model.t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
   val theories_instances :
@@ -879,13 +882,14 @@ module Main_Default : S = struct
   let get_real_env t = t.gamma
   let get_case_split_env t = t.gamma_finite
 
-  let compute_concrete_model env =
+  let compute_concrete_model env ~declared_ids =
     let { gamma_finite; assumed_set; objectives; _ }, _ =
       do_case_split_aux env ~for_model:true
     in
     lazy (
       CC_X.extract_concrete_model
         ~prop_model:assumed_set
+        ~declared_ids
         gamma_finite
     ), objectives
 
@@ -940,7 +944,8 @@ module Main_Empty : S = struct
   let get_case_split_env _ = CC_X.empty
   let do_case_split env _ = env, E.Set.empty
   let add_term env _ ~add_in_cs:_ = env
-  let compute_concrete_model _env = lazy Models.empty, Objective.Model.empty
+  let compute_concrete_model _env ~declared_ids:_ =
+    lazy Models.empty, Objective.Model.empty
 
   let assume_th_elt e _ _ = e
   let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, []
diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli
index c7e8f71eb..c0f916c74 100644
--- a/src/lib/reasoners/theory.mli
+++ b/src/lib/reasoners/theory.mli
@@ -54,7 +54,10 @@ module type S = sig
 
   val add_term : t -> Expr.t -> add_in_cs:bool -> t
 
-  val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
+  val compute_concrete_model :
+    t ->
+    declared_ids:Id.typed list ->
+    Models.t Lazy.t * Objective.Model.t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
   val theories_instances :
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index c22bcff25..d0f106108 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1167,11 +1167,11 @@ let compute_concrete_model_of_val cache =
 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 env ->
+  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, ME.empty)
+        terms (ModelMap.empty ~suspicious declared_ids, ME.empty)
     in
     let model =
       Hashtbl.fold (fun t vals mdl ->
@@ -1212,9 +1212,9 @@ let extract_concrete_model cache =
     in
     { Models.propositional = prop_model; model; term_values = mrepr }
 
-let extract_concrete_model ~prop_model =
+let extract_concrete_model ~prop_model ~declared_ids =
   let cache : cache = {
     array_selects = Hashtbl.create 17;
     abstracts = Hashtbl.create 17;
   }
-  in fun env -> extract_concrete_model cache ~prop_model env
+  in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env
diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli
index 40fd47cd1..9eef6b30c 100644
--- a/src/lib/reasoners/uf.mli
+++ b/src/lib/reasoners/uf.mli
@@ -72,7 +72,11 @@ val assign_next : t -> (r Xliteral.view * bool * Th_util.lit_origin) list * t
 (** {2 Counterexample function} *)
 
 (** Compute a counterexample using the Uf environment *)
-val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+val extract_concrete_model :
+  prop_model:Expr.Set.t ->
+  declared_ids:Id.typed list ->
+  t ->
+  Models.t
 
 (** saves the module's cache *)
 val save_cache : unit -> unit
diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml
index c539128ba..5c26fa59b 100644
--- a/src/lib/structures/commands.ml
+++ b/src/lib/structures/commands.ml
@@ -31,6 +31,7 @@
 (* Sat entry *)
 
 type sat_decl_aux =
+  | Decl of Id.typed
   | Assume of string * Expr.t * bool
   | PredDef of Expr.t * string (*name of the predicate*)
   | RwtDef of (Expr.t Typed.rwt_rule) list
@@ -46,6 +47,12 @@ type sat_tdecl = {
 }
 
 let print_aux fmt = function
+  | Decl (id, arg_tys, ret_ty) ->
+    Fmt.pf fmt "declare %a with type (%a) -> %a"
+      Id.pp id
+      Fmt.(list ~sep:comma Ty.print) arg_tys
+      Ty.print ret_ty
+
   | Assume (name, e, b) ->
     Format.fprintf fmt "assume %s(%b): @[<hov>%a@]" name b Expr.print e
   | PredDef (e, name) ->
diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli
index 320da889c..800c58f10 100644
--- a/src/lib/structures/commands.mli
+++ b/src/lib/structures/commands.mli
@@ -31,6 +31,7 @@
 (* Sat entry *)
 
 type sat_decl_aux =
+  | Decl of Id.typed
   | Assume of string * Expr.t * bool
   | PredDef of Expr.t * string (*name of the predicate*)
   | RwtDef of (Expr.t Typed.rwt_rule) list
diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml
index e6d8a74f3..62624c385 100644
--- a/src/lib/structures/id.ml
+++ b/src/lib/structures/id.ml
@@ -81,3 +81,7 @@ module Namespace = struct
     Skolem.reset_fresh_cpt ();
     Abstract.reset_fresh_cpt ()
 end
+
+let dummy_typed =
+  let id = Namespace.Internal.fresh () |> Hstring.make in
+  (id, [], Ty.Tunit)
diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli
index a011bd36e..a48fc43c8 100644
--- a/src/lib/structures/id.mli
+++ b/src/lib/structures/id.mli
@@ -36,6 +36,8 @@ type typed = t * Ty.t list * Ty.t
     - Types of its arguments.
     - The returned type. *)
 
+val dummy_typed : typed
+
 val compare_typed : typed -> typed -> int
 val equal : t -> t -> bool
 val show : t -> string
diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml
index e28af0ef3..8a0e68928 100644
--- a/src/lib/structures/modelMap.ml
+++ b/src/lib/structures/modelMap.ml
@@ -42,6 +42,8 @@ module Graph = struct
   let empty = M.empty
   let add = M.add
   let map = M.map
+  let cardinal = M.cardinal
+  let choose = M.choose
 
   (* A fiber of the function [f] over a value [v] is the set of all the values
      in the domain of [f] whose the image by [f] is [v].
@@ -125,12 +127,45 @@ let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } =
   if List.compare_lengths arg_tys arg_vals <> 0 then
     Fmt.invalid_arg "The arity of the symbol %a doesn't agree the number of \
                      arguments" Id.pp id;
-
-  let graph = try P.find sy values with Not_found -> Graph.empty in
+  let graph =
+    try
+      let graph = P.find sy values in
+      (* If the graph associated with [sy] contains only an abstract value,
+         it means there is no constraint on this graph. We replace it by
+         the graph with the only constraint given by [arg_vals] and
+         [ret_val]. *)
+      if Graph.cardinal graph == 1 then
+        let _, value = Graph.choose graph in
+        let Expr.{ f; _ } = Expr.term_view value in
+        match f with
+        | Sy.Name { hs; _ }
+          when Id.Namespace.Abstract.is_id (Hstring.view hs) ->
+          Graph.empty
+        | _ -> graph
+      else
+        graph
+    with Not_found -> Graph.empty in
   let values = P.add sy (Graph.add arg_vals ret_val graph) values in
   { values; suspicious }
 
-let empty ~suspicious = { values = P.empty; suspicious }
+module DeclSets = Set.Make
+    (struct
+      type t = Id.typed
+      let compare = Id.compare_typed
+    end)
+
+let empty ~suspicious declared_ids =
+  let values =
+    List.fold_left
+      (fun values ((_, arg_tys, ret_ty) as sy) ->
+         let arg_vals = List.map Expr.mk_abstract arg_tys in
+         let ret_val = Expr.mk_abstract ret_ty in
+         let graph = Graph.add arg_vals ret_val Graph.empty in
+         P.add sy graph values
+      )
+      P.empty declared_ids
+  in
+  { values; suspicious }
 
 let rec subst_in_term id e c =
   let Expr.{ f; xs; ty = ty'; _ } = Expr.term_view c in
diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli
index b0f90b7f1..b2d03124c 100644
--- a/src/lib/structures/modelMap.mli
+++ b/src/lib/structures/modelMap.mli
@@ -35,7 +35,7 @@ val add : Id.typed -> Expr.t list -> Expr.t -> t -> t
 (** [add sy args ret mdl] adds the binding [args -> ret] to the partial graph
     associated with the symbol [sy]. *)
 
-val empty : suspicious:bool -> t
+val empty : suspicious:bool -> Id.typed list -> t
 (** An empty model. The [suspicious] flag is used to remember that this
     model may be wrong as it involves symbols from theories for which the
     model generation is known to be incomplete. *)
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index 1aa6dc1e5..6e3bf96b8 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -12,7 +12,8 @@ appropriate here.
   (
     (define-fun x () Int 0)
     (define-fun y () Int 0)
-    (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+    (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
+    (define-fun a2 () (Array Int Int) (as @a3 (Array Int Int)))
   )
 
 Now we will test some semantic triggers.
diff --git a/tests/dune.inc b/tests/dune.inc
index 26d82ad68..e5b9775fc 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -209726,6 +209726,27 @@
 
 ; Auto-generated part begin
 (subdir models
+  (rule
+   (target complete_models.models_dolmen.output)
+   (deps (:input complete_models.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes (or 0)
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps complete_models.models_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff complete_models.models.expected complete_models.models_dolmen.output)))
   (rule
    (target check_sat.models_dolmen.output)
    (deps (:input check_sat.models.ae))
diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected
index 086ba7ffb..b35225efb 100644
--- a/tests/issues/555.models.expected
+++ b/tests/issues/555.models.expected
@@ -3,6 +3,6 @@ unknown
 (
   (define-fun x () Int 0)
   (define-fun y () Int 0)
-  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
 )
diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected
index bb0b49fe0..88a28c7d8 100644
--- a/tests/issues/854/function.models.expected
+++ b/tests/issues/854/function.models.expected
@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref))
   (define-fun a () Int 0)
   (define-fun f ((_arg_0 Int)) Int 0)
   (define-fun a1 () Int 0)
diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected
index 9198abbbf..8fbfb8105 100644
--- a/tests/issues/854/original.models.expected
+++ b/tests/issues/854/original.models.expected
@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )
diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected
index f18c7f58e..c51afd4a7 100644
--- a/tests/issues/854/twice_eq.models.expected
+++ b/tests/issues/854/twice_eq.models.expected
@@ -1,8 +1,8 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a0 intref))
-  (define-fun another_mk ((_arg_0 Int)) intref (as @a0 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref))
+  (define-fun another_mk ((_arg_0 Int)) intref (as @a6 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )
diff --git a/tests/models/arith/arith11.optimize.expected b/tests/models/arith/arith11.optimize.expected
index 99f7450f0..722135b53 100644
--- a/tests/models/arith/arith11.optimize.expected
+++ b/tests/models/arith/arith11.optimize.expected
@@ -4,6 +4,7 @@ unknown
   (define-fun p1 () Bool false)
   (define-fun p2 () Bool true)
   (define-fun x () Real 2.0)
+  (define-fun y () Real (as @a3 Real))
 )
 (objectives 
   (x 2.0)
diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected
index 086ba7ffb..b35225efb 100644
--- a/tests/models/array/array1.models.expected
+++ b/tests/models/array/array1.models.expected
@@ -3,6 +3,6 @@ unknown
 (
   (define-fun x () Int 0)
   (define-fun y () Int 0)
-  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
+  (define-fun a2 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
 )
diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected
index dd6a80ae9..057bc1a6c 100644
--- a/tests/models/array/embedded-array.models.expected
+++ b/tests/models/array/embedded-array.models.expected
@@ -1,8 +1,8 @@
 
 unknown
 (
-  (define-fun s () S (as @a0 S))
+  (define-fun s () S (as @a2 S))
   (define-fun x () Pair
-   (pair (store (as @a1 (Array Int S)) 0 s)
-         (store (as @a1 (Array Int S)) 0 s)))
+   (pair (store (as @a3 (Array Int S)) 0 s)
+         (store (as @a3 (Array Int S)) 0 s)))
 )
diff --git a/tests/models/bool/bool2.models.expected b/tests/models/bool/bool2.models.expected
index e0f6879b8..7d4b0eed7 100644
--- a/tests/models/bool/bool2.models.expected
+++ b/tests/models/bool/bool2.models.expected
@@ -2,6 +2,7 @@
 unknown
 (
   (define-fun x () Bool false)
+  (define-fun y () Bool (as @a1 Bool))
 )
 ((notx true))
 
diff --git a/tests/models/complete_models.models.expected b/tests/models/complete_models.models.expected
new file mode 100644
index 000000000..49667d5f1
--- /dev/null
+++ b/tests/models/complete_models.models.expected
@@ -0,0 +1,36 @@
+
+unknown
+(
+  (define-fun x () Int (as @a0 Int))
+)
+
+unknown
+(
+  (define-fun x () Int 5)
+  (define-fun y () Int (as @a2 Int))
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+  (define-fun z () S (as @a5 S))
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+  (define-fun z () S (as @a7 S))
+  (define-fun f ((_arg_0 Int)) Int (as @a9 Int))
+)
+
+unknown
+(
+  (define-fun x () Int 6)
+  (define-fun z () S (as @a11 S))
+  (define-fun f ((_arg_0 Int)) Int 2)
+)
diff --git a/tests/models/complete_models.models.smt2 b/tests/models/complete_models.models.smt2
new file mode 100644
index 000000000..c65cf1d89
--- /dev/null
+++ b/tests/models/complete_models.models.smt2
@@ -0,0 +1,24 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x Int)
+(check-sat)
+(get-model)
+(push 1)
+(declare-const y Int)
+(assert (= x 5))
+(check-sat)
+(get-model)
+(pop 1)
+(assert (= x 6))
+(check-sat)
+(get-model)
+(declare-sort S 0)
+(declare-const z S)
+(check-sat)
+(get-model)
+(declare-fun f (Int) Int)
+(check-sat)
+(get-model)
+(assert (= (f 5) 2))
+(check-sat)
+(get-model)