diff --git a/src/transformations/native_nn_prover.mli b/src/transformations/native_nn_prover.mli
index 65b43a800952c63a3333323e6ca3417b8a917d74..d8ad4b1276984dd8dce632659dc3b54e55ebe0c0 100644
--- a/src/transformations/native_nn_prover.mli
+++ b/src/transformations/native_nn_prover.mli
@@ -5,7 +5,7 @@
 (**************************************************************************)
 
 val init : unit -> unit
-(** Register the transformations. *)
+(** Register the transformation. *)
 
 val meta_input : Why3.Theory.meta
 (** Indicate the input position. *)
diff --git a/src/transformations/vars_on_lhs.ml b/src/transformations/vars_on_lhs.ml
index b6cb6ae7ebd3317c80c3351fa16771da6ba4b157..a1ac31d6c4768e01100a58578e8cb1b5a0f9b601 100644
--- a/src/transformations/vars_on_lhs.ml
+++ b/src/transformations/vars_on_lhs.ml
@@ -4,6 +4,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Base
+
 let make_rt env =
   let open Why3 in
   let th = Env.read_theory env [ "ieee_float" ] "Float64" in
@@ -21,29 +23,27 @@ let make_rt env =
             ({ t_node = Tconst _; _ } as const);
             ({ t_node = Tapp (_, []); _ } as var);
           ] ) ->
-      Fmt.pr "HERE: %a!@." Pretty.print_term t;
+      let tt = [ var; const ] in
       if Term.ls_equal ls le
-      then Term.ps_app ge [ var; const ]
+      then Term.ps_app ge tt
       else if Term.ls_equal ls ge
-      then Term.ps_app le [ var; const ]
+      then Term.ps_app le tt
       else if Term.ls_equal ls lt
-      then Term.ps_app gt [ var; const ]
+      then Term.ps_app gt tt
       else if Term.ls_equal ls gt
-      then Term.ps_app lt [ var; const ]
+      then Term.ps_app lt tt
       else t
     | _ -> t
   in
-  let init = None in
-  let init = Task.add_ty_decl init t in
-  let init = Task.add_param_decl init le in
-  let init = Task.add_param_decl init lt in
-  let init = Task.add_param_decl init ge in
-  let init = Task.add_param_decl init gt in
-  (rt, init)
+  let task =
+    List.fold [ le; lt; ge; gt ] ~init:(Task.add_ty_decl None t)
+      ~f:Task.add_param_decl
+  in
+  (rt, task)
 
 let vars_on_lhs env =
-  let rt, init = make_rt env in
-  Why3.Trans.rewrite rt init
+  let rt, task = make_rt env in
+  Why3.Trans.rewrite rt task
 
 let init () =
   Why3.Trans.register_env_transform
diff --git a/src/transformations/vars_on_lhs.mli b/src/transformations/vars_on_lhs.mli
new file mode 100644
index 0000000000000000000000000000000000000000..7914140eb39883e8d0e0b2244b98728739cc4cb4
--- /dev/null
+++ b/src/transformations/vars_on_lhs.mli
@@ -0,0 +1,8 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+val init : unit -> unit
+(** Register the transformation. *)
diff --git a/tests/marabout.t b/tests/marabout.t
index f2db6c2f0d4263d40fee67b060157a66b1d587ff..b05012d835e5698bb69e2df0c034b4446b9c8dfa 100644
--- a/tests/marabout.t
+++ b/tests/marabout.t
@@ -43,8 +43,6 @@ Test verify
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.
   <autodetect>3 prover(s) added
-  HERE: lt (0.0:t) x1!
-  HERE: lt (0.0:t) y!
   Goal G: High failure
   Output:
   1.0.+