diff --git a/src/meta.ml b/src/meta.ml
index ae6eb300890d16b13794cc8bbed98975f69b8ad9..b55609001dc7213a2a91eb1803c3d26184bd6ba3 100644
--- a/src/meta.ml
+++ b/src/meta.ml
@@ -49,3 +49,21 @@ let meta_dataset_filename =
   Why3.Theory.(
     register_meta_excl "caisar_dataset"
       ~desc:"Indicates the filename of the dataset" [ MTstring ])
+
+let rec get_io_meta ~input_name ~output_name info task =
+  match task with
+  | None -> ()
+  | Some { Why3.Task.task_prev; task_decl; _ } -> (
+    get_io_meta ~input_name ~output_name info task_prev;
+    match task_decl.Why3.Theory.td_node with
+    | Use _ | Clone _ -> ()
+    | Meta (meta, l) when Why3.Theory.meta_equal meta meta_input -> (
+      match l with
+      | [ MAls ls; MAint i ] -> Why3.Term.Hls.add info ls (input_name i)
+      | _ -> assert false)
+    | Meta (meta, l) when Why3.Theory.meta_equal meta meta_output -> (
+      match l with
+      | [ MAls ls; MAint i ] -> Why3.Term.Hls.add info ls (output_name i)
+      | _ -> assert false)
+    | Meta _ -> ()
+    | Decl _ -> ())
diff --git a/src/meta.mli b/src/meta.mli
index 0ed5f6a0b7ae2f7441905952ccbbcb38c808a70b..c15dd4cfa3d7e5df19d185a31883500cc1aa3036 100644
--- a/src/meta.mli
+++ b/src/meta.mli
@@ -34,3 +34,6 @@ val meta_svm_filename : Why3.Theory.meta
 
 val meta_dataset_filename : Why3.Theory.meta
 (** The filename of the dataset. *)
+
+val get_io_meta: input_name:(int -> 'a) -> output_name:(int -> 'a) -> 'a Why3.Term.Hls.t -> Why3.Task.task -> unit
+(** Add to the given hashtbl all the name for the inputs and outputs *)
\ No newline at end of file
diff --git a/src/printers/marabou.ml b/src/printers/marabou.ml
index 052964adea5be903654075737b0470631b68f326..1f0a06ba7dc7df1353d3d9dbfed8d5a9e78195fe 100644
--- a/src/printers/marabou.ml
+++ b/src/printers/marabou.ml
@@ -169,14 +169,6 @@ let rec print_tdecl info fmt task =
     print_tdecl info fmt task_prev;
     match task_decl.Theory.td_node with
     | Use _ | Clone _ -> ()
-    | Meta (meta, l) when Theory.meta_equal meta Meta.meta_input -> (
-      match l with
-      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "x%i" i)
-      | _ -> assert false)
-    | Meta (meta, l) when Theory.meta_equal meta Meta.meta_output -> (
-      match l with
-      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "y%i" i)
-      | _ -> assert false)
     | Meta (_, _) -> ()
     | Decl d -> print_decl info fmt d)
 
@@ -198,6 +190,8 @@ let print_task args ?old:_ fmt task =
     }
   in
   Printer.print_prelude fmt args.Printer.prelude;
+  Meta.get_io_meta info.variables task ~input_name:(Fmt.str "x%i")
+    ~output_name:(Fmt.str "y%i");
   print_tdecl info fmt task
 
 let init () =
diff --git a/src/printers/pyrat.ml b/src/printers/pyrat.ml
index 162d91e3f0b3a64af9ccc54171f61a07d3fc5273..ef66f0df18b9207b7c545e5831ea0cd4fe2bff4e 100644
--- a/src/printers/pyrat.ml
+++ b/src/printers/pyrat.ml
@@ -155,14 +155,6 @@ let rec print_tdecl info fmt task =
     print_tdecl info fmt task_prev;
     match task_decl.Theory.td_node with
     | Use _ | Clone _ -> ()
-    | Meta (meta, l) when Theory.meta_equal meta Meta.meta_input -> (
-      match l with
-      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "x%i" i)
-      | _ -> assert false)
-    | Meta (meta, l) when Theory.meta_equal meta Meta.meta_output -> (
-      match l with
-      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "y%i" i)
-      | _ -> assert false)
     | Meta (_, _) -> ()
     | Decl d -> print_decl info fmt d)
 
@@ -184,6 +176,8 @@ let print_task args ?old:_ fmt task =
     }
   in
   Printer.print_prelude fmt args.Printer.prelude;
+  Meta.get_io_meta info.variables task ~input_name:(Fmt.str "x%i")
+    ~output_name:(Fmt.str "y%i");
   print_tdecl info fmt task
 
 let init () =
diff --git a/src/printers/vnnlib.ml b/src/printers/vnnlib.ml
index 2bad9dec08f133c0b75b7905b1c58752258b8345..072339ddc98278029d2bf19fb4a5e383b1b5c52a 100644
--- a/src/printers/vnnlib.ml
+++ b/src/printers/vnnlib.ml
@@ -502,16 +502,6 @@ let rec print_tdecl info fmt task =
     print_tdecl info fmt task_prev;
     match task_decl.Theory.td_node with
     | Use _ | Clone _ -> ()
-    | Meta (meta, l) when Theory.meta_equal meta Meta.meta_input -> (
-      match l with
-      | [ MAls ls; MAint i ] ->
-        Term.Hls.add info.variables ls (Fmt.str "X_%i" i)
-      | _ -> assert false)
-    | Meta (meta, l) when Theory.meta_equal meta Meta.meta_output -> (
-      match l with
-      | [ MAls ls; MAint i ] ->
-        Term.Hls.add info.variables ls (Fmt.str "Y_%i" i)
-      | _ -> assert false)
     | Meta _ -> ()
     | Decl d -> print_decl info fmt d)
 
@@ -534,6 +524,8 @@ let print_task args ?old:_ fmt task =
     }
   in
   Printer.print_prelude fmt args.Printer.prelude;
+  Meta.get_io_meta info.variables task ~input_name:(Fmt.str "X_%i")
+    ~output_name:(Fmt.str "Y_%i");
   print_tdecl info fmt task
 
 let init () =