diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 2164500fb683112434b47f82935d4307eca843ea..f8e473067068ad2ee15cc2833bdf307e176c4abe 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -246,7 +246,7 @@ let abstract_nn_term env =
     (output_vars, term)
   in
   Why3.Trans.fold_map
-    (fun task_hd (((index, input_vars) as acc), task) ->
+    (fun task_hd ((input_vars as acc), task) ->
       let tdecl = task_hd.task_decl in
       match tdecl.td_node with
       | Decl { d_node = Dparam ls; _ } when Language.mem_nn ls ->
@@ -269,15 +269,9 @@ let abstract_nn_term env =
             _;
           }
         when Why3.Ty.ty_equal ty th_float64.ty ->
-        (* Add meta for input variable declarations. Each meta needs to appear
-           before the corresponding declaration in order to be leveraged by
-           prover printers. *)
-        let task =
-          Why3.Task.add_meta task Meta.meta_input [ MAls ls; MAint index ]
-        in
         let task = Why3.Task.add_tdecl task tdecl in
-        let input_vars = Why3.Term.Mls.add ls index input_vars in
-        ((index + 1, input_vars), task)
+        let input_vars = Why3.Term.Sls.add ls input_vars in
+        (input_vars, task)
       | Decl { d_node = Dprop (Pgoal, pr, goal); _ } ->
         let output_vars, goal = create_output_vars goal in
         let pr = Why3.Decl.create_prsymbol (Why3.Ident.id_clone pr.pr_name) in
@@ -326,6 +320,19 @@ let abstract_nn_term env =
             (fun acc term (index, _) -> { index; term } :: acc)
             [] output_vars
         in
+        let _, input_vars =
+          Why3.Term.Mls.mapi_fold (fun _ () i -> (i + 1, i)) input_vars 0
+        in
+        (* Add meta for input variable declarations. Each meta needs to appear
+           before the corresponding declaration in order to be leveraged by
+           prover printers. *)
+        let task =
+          Why3.Term.Mls.fold_left
+            (fun task ls index ->
+              Why3.Task.add_meta task Meta.meta_input [ MAls ls; MAint index ])
+            task input_vars
+        in
+
         let nn_filename = create_new_nn env input_vars output_vars in
         let task =
           Why3.Task.add_meta task Meta.meta_nn_filename [ MAstr nn_filename ]
@@ -335,7 +342,7 @@ let abstract_nn_term env =
         (* TODO: check no nn applications *)
         (acc, Why3.Task.add_tdecl task tdecl)
       | _ -> (acc, Why3.Task.add_tdecl task tdecl))
-    (0, Why3.Term.Mls.empty) None
+    Why3.Term.Sls.empty None
 
 (** {2 Old way} *)