diff --git a/src/bin/common/dune b/src/bin/common/dune
index 8cc2a2b71..307f982a5 100644
--- a/src/bin/common/dune
+++ b/src/bin/common/dune
@@ -21,8 +21,7 @@
    Parse_command
    Input_frontend
    Signals_profiling
-   Solving_loop
-   Solving_loop_imperative)
+   Solving_loop)
 )
 
 (generate_sites_module
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index cf3624835..bba5afe2c 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -1199,9 +1199,12 @@ let main () =
         in
         st
 
-      | {contents = `Decls l; _} ->
+      | {contents = `Decls l; loc; _} ->
         let st = DO.Mode.set Util.Assert st in
-        D_cnf.cache_decls l;
+        let decls = D_cnf.make_decls l in
+        let module Api = (val DO.SatSolverModule.get st) in
+        let loc = dl_to_ael file_loc loc in
+        List.iter (fun decl -> Api.FE.declare ~loc decl Api.env) decls;
         st
 
       (* When the next statement is a goal, the solver is called and provided
@@ -1371,7 +1374,7 @@ let main () =
             let st = handle_reset st in
             let whole_path = List.rev_append prefix tl in
             Format.eprintf "Restarting with %i instructions@." (List.length whole_path);
-            aux (State.get named_terms st) st whole_path
+            aux Util.MS.empty st whole_path
           | {contents; _ } ->
             let st =
               let new_current_path =
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 57014fab7..51164af0e 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -697,14 +697,14 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
   in
   Cache.store_sy tcst sy;
   (* 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) *)
+  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
@@ -1898,16 +1898,16 @@ let make_form name_base f loc ~decl_kind =
   else
     E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind
 
-let cache_decls = function
+let make_decls = function
   | [] -> assert false (* We could probably just return (). *)
   | [td] ->
     begin
       match td with
-      | `Type_decl (td, _def) -> mk_ty_decl td
-      | `Term_decl td -> mk_term_decl td;
+      | `Type_decl (td, _def) -> mk_ty_decl td; []
+      | `Term_decl td -> [mk_term_decl td];
     end
   | dcl ->
-    let rec aux acc tdl =
+    let rec aux term_acc 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.
          But it doesn't affect the execution.
@@ -1919,20 +1919,21 @@ let cache_decls = function
           | [otd] -> mk_ty_decl otd
           | _ -> mk_mr_ty_decls (List.rev acc)
         end;
-        mk_term_decl td;
-        aux [] tl
+        let t = mk_term_decl td in
+        aux (t :: term_acc) [] tl
 
       | `Type_decl (td, _def) :: tl ->
-        aux (td :: acc) tl
+        aux term_acc (td :: acc) tl
 
       | [] ->
         begin match acc with
           | [] -> ()
           | [otd] -> mk_ty_decl otd
           | _ ->  mk_mr_ty_decls (List.rev acc)
-        end
+        end;
+        term_acc
     in
-    aux [] dcl
+    aux [] [] dcl
 
 (* Helper function used to check if the expression defining an objective
    function is a pure term. *)
diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli
index 772153c4e..319ce3ed0 100644
--- a/src/lib/frontend/d_cnf.mli
+++ b/src/lib/frontend/d_cnf.mli
@@ -99,7 +99,7 @@ val pp_query :
 (** Registers the declarations in the cache. If there are more than one element
     in the list, it is assumed they are mutually recursive (but if it is not the
     case, it still work). *)
-val cache_decls : D_loop.Typer_Pipe.decl list -> unit
+val make_decls : D_loop.Typer_Pipe.decl list -> (Hstring.t * Ty.t list * Ty.t) list
 
 val builtins :
   Dolmen_loop.State.t ->
diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index b5ebb0c18..9bbc252d3 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -146,6 +146,8 @@ module type S = sig
 
   val init_env : ?sat_env:sat_env -> used_context -> env
 
+  val declare : Id.typed process
+
   val push : int process
 
   val pop : int process
@@ -436,6 +438,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
   let wrap_f f ?loc x env =
     check_if_over (handle_sat_exn f ?loc x) env
 
+  let declare = wrap_f internal_decl
+
   let push = wrap_f internal_push
 
   let pop = wrap_f internal_pop
diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli
index a5606b155..c0ad02e10 100644
--- a/src/lib/frontend/frontend.mli
+++ b/src/lib/frontend/frontend.mli
@@ -70,6 +70,8 @@ module type S = sig
       the user. *)
   type 'a process = ?loc:Loc.t -> 'a -> env -> unit
 
+  val declare : Id.typed process
+
   val push : int process
 
   val pop : int process
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index 6be8fef15..ff4214ec6 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -11,7 +11,7 @@ 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 @a0 (Array Int Int)))
   )
 
diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected
index 6db0558a4..f5b97ee0b 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 @a0 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a1 (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) (store (as @a5 (Array Int Int)) 0 0))
 )
diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected
index bb0b49fe0..6e5eeb8fb 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 @a4 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..7d40ab42e 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 @a3 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..ee4c1de0d 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 @a4 intref))
+  (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )
diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected
index 6db0558a4..f5b97ee0b 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 @a0 (Array Int Int)) 0 0))
-  (define-fun a2 () (Array Int Int) (store (as @a1 (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) (store (as @a5 (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)))
 )