diff --git a/src/interpretation.ml b/src/interpretation.ml
index 560cee7c08dd326d9cd1c57f66ed7103245df7e5..f7901c003c85f8663cf340d7d436c3cd4c8806a9 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -127,6 +127,7 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
   let error_message ls =
     Fmt.str "Invalid arguments for '%a'" Pretty.print_ls ls
   in
+
   (* Vector *)
   let vget : _ CRE.builtin =
    fun engine ls vl ty ->
@@ -146,14 +147,14 @@ let caisar_builtins : caisar_env CRE.built_in_theories list =
         in
         let ty_features =
           match ty with
-          | Some { ty_node = Tyapp (_, [ ty; _ ]); _ } -> Some ty
+          | Some { ty_node = Tyapp (_, [ _; ty ]); _ } -> Some ty
           | _ -> assert false
         in
         let t_features, t_label =
           ( term_of_caisar_op engine (Data (D_csv features)) ty_features,
             Term.t_int_const (BigInt.of_int (Int.of_string label)) )
         in
-        value_term (Term.t_tuple [ t_features; t_label ])
+        value_term (Term.t_tuple [ t_label; t_features ])
       | Vector v ->
         let n = Option.value_exn (Language.lookup_vector v) in
         assert (List.length tl1 = n && i <= n);
diff --git a/src/language.ml b/src/language.ml
index d3bcf56edce751e64c154b8b7fb69d820a898fca..6d9a186638aa5d1270848491c0e6c5280b89906d 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -272,7 +272,7 @@ let fresh_dataset_csv_ls env name =
     let th = Env.read_theory env [ "interpretation" ] "Dataset" in
     Ty.ty_app
       (Theory.ns_find_ts th.th_export [ "dataset" ])
-      [ ty_elt; Ty.ty_int ]
+      [ Ty.ty_int; ty_elt ]
   in
   let id = Ident.id_fresh name in
   Term.create_fsymbol id [] ty
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index eb6ef3e756420ce07c278a303cb10e6e138722a2..8ce1d6076853bf3f506625105d98ae35f5600ea9 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -14,7 +14,6 @@ Test interpret on dataset
   $ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
-  >   use bool.Bool
   >   use int.Int
   >   use interpretation.Vector
   >   use interpretation.NeuralNetwork
@@ -35,7 +34,7 @@ Test interpret on dataset
   >   predicate bounded_by_epsilon (i: image) (eps: t) =
   >     forall v: index. valid_index i v -> .- eps .<= i[v] .<= eps
   > 
-  >   predicate robust_around (n: nn) (eps: t) (i: image) (l: label_) =
+  >   predicate robust_around (n: nn) (eps: t) (l: label_) (i: image) =
   >     forall perturbed_image: image.
   >       has_length perturbed_image (length i) ->
   >       valid_image perturbed_image ->
@@ -43,7 +42,7 @@ Test interpret on dataset
   >       bounded_by_epsilon perturbation eps ->
   >       advises n perturbed_image l
   > 
-  >   predicate robust (n: nn) (d: dataset image label_) (eps: t) =
+  >   predicate robust (n: nn) (d: dataset label_ image) (eps: t) =
   >     Dataset.forall_ d (robust_around n eps)
   > 
   >   goal G: