diff --git a/src/dataset.ml b/src/dataset.ml index a1f0f6e097cfe16444c27f6810367cb49a84dba6..b7929720a04da2d26c5b965a97125f6b0aead0b8 100644 --- a/src/dataset.ml +++ b/src/dataset.ml @@ -316,15 +316,16 @@ let add_decls ~kind task = | `In n -> (n, Fmt.str "x%d", Utils.meta_input) | `Out n -> (n, Fmt.str "y%d", Utils.meta_output) in - let lls = - List.init n ~f:(fun idx -> - Term.create_lsymbol (Ident.id_fresh (fid idx)) [] (Some Ty.ty_real)) + let id_lls = + List.init n ~f:(fun id -> + (id, Term.create_lsymbol (Ident.id_fresh (fid id)) [] (Some Ty.ty_real))) in - let task = - List.foldi lls ~init:task ~f:(fun idx task ls -> - let task = Task.add_meta task meta [ MAls ls; MAint idx ] in - Task.add_param_decl task ls) + let lls, task = + List.fold id_lls ~init:([], task) ~f:(fun (lls, task) (id, ls) -> + let task = Task.add_meta task meta [ MAls ls; MAint id ] in + (ls :: lls, Task.add_param_decl task ls)) in + let lls = List.rev lls in (lls, task) let tasks_of_nn_csv_predicate env