diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index e035485889d5ec0fe9ac4aefc087e14285f25c3e..8a88c457a02594f3ed71782c945dd02f79bed895 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -26,7 +26,6 @@ time "why3cpulimit time : %s s"
 
 transformation "inline_trivial"
 transformation "introduce_premises"
-
 transformation "eliminate_builtin"
 transformation "simplify_formula"
 transformation "caisar_native_prover"
diff --git a/src/transformations.ml b/src/transformations.ml
index 762bd9d674ca257d90508c58d4c4f4d2246d476d..99dda35a650554ab37d6067e80f0677e828d9c07 100644
--- a/src/transformations.ml
+++ b/src/transformations.ml
@@ -18,6 +18,8 @@ let meta_output =
       ~desc:"Indicates the position of the output in the neural network"
       [ MTlsymbol; MTint ])
 
+(* Retrieves the (input) variables appearing, as arguments, after an
+   'nnet_apply' symbol. *)
 let get_input_variables =
   let rec aux acc (term : Why3.Term.term) =
     match term.t_node with
@@ -40,6 +42,8 @@ let get_input_variables =
     (fun decl acc -> Why3.Decl.decl_fold aux acc decl)
     Why3.Term.Mls.empty
 
+(* Creates logic symbols for output variables and simplifies the formula. *)
+(* TODO: [Reduction_engine] is probably an overkill and should be replaced. *)
 let simplify_goal env input_variables =
   let rec aux hls (term : Why3.Term.term) =
     match term.t_node with
@@ -100,11 +104,7 @@ let simplify_goal env input_variables =
     None
 
 let caisar_native_prover env =
-  Why3.Trans.seq
-    [
-      Why3.Trans.bind get_input_variables (simplify_goal env)
-      (* Why3.Simplify_formula.simplify_; *);
-    ]
+  Why3.Trans.seq [ Why3.Trans.bind get_input_variables (simplify_goal env) ]
 
 let init () =
   Why3.Trans.register_env_transform