diff --git a/src/interpretation.ml b/src/interpretation.ml
index ef2ae7639af72590dab3e9f3a0a683db2678d427..bb35079baf0e14f0728747252f28456a83e57fcd 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -382,6 +382,17 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
       Some { new_quant; substitutions }
   | _ -> None
 
+let declare_language_lsymbols caisar_env task =
+  (* Declare [Language] logic symbols for classifiers and vectors only. *)
+  Term.Hls.fold
+    (fun ls _ task ->
+      if Language.mem_vector ls || Language.mem_nn_classifier ls
+      then
+        let decl = Decl.create_param_decl ls in
+        Task.add_decl task decl
+      else task)
+    caisar_env.caisar_op_of_ls task
+
 let interpret_task ~cwd env task =
   let known_map = Task.task_known task in
   let caisar_env = caisar_env env cwd in
@@ -399,17 +410,7 @@ let interpret_task ~cwd env task =
   let g, f = (Task.task_goal task, Task.task_goal_fmla task) in
   let f = CRE.normalize ~limit:Int.max_value engine Term.Mvs.empty f in
   let _, task = Task.task_separate_goal task in
-  let task =
-    (* Declare logic symbols introduced for classifiers and vectors. *)
-    Term.Hls.fold
-      (fun ls _ task ->
-        if Language.mem_vector ls || Language.mem_nn_classifier ls
-        then
-          let decl = Decl.create_param_decl ls in
-          Task.add_decl task decl
-        else task)
-      caisar_env.caisar_op_of_ls task
-  in
+  let task = declare_language_lsymbols caisar_env task in
   let task = Task.(add_prop_decl task Pgoal g f) in
   (* Fmt.pr "%a : %a@.%a@." Pretty.print_pr (Task.task_goal task)
      Pretty.print_term *)