Remove manually applied transformation for inlining net_apply as not actually useful.

The driver seems to do the job already.

src/transformations/actual_net_apply.mli

@@ -14,9 +14,5 @@
     are stored inside of an environment, their shape being either provided by
     the NIER or inferred with the expected result of ONNX operations. *)
 
-open Why3
-
-val actual_net_apply : Env.env -> Task.task Trans.trans
-
 val init : unit -> unit
 (** Register the transformation. *)

src/verification.ml

@@ -93,14 +93,12 @@ let answer_saver limit config env config_prover dataset_csv task =
     let additional_info = Fmt.str "(%d/%d)" answer.nb_proved answer.nb_total in
     (prover_answer, Some additional_info)
 
-let answer_generic limit config prover config_prover driver task env =
+let answer_generic limit config prover config_prover driver task =
   let task_prepared = Driver.prepare_task driver task in
   let tasks =
     match prover with
     | Prover.Marabou -> Trans.apply Split.split_all task_prepared
     | Pyrat -> Trans.apply Split.split_premises task_prepared
-    | Prover.CVC5 ->
-      [ Trans.apply (Actual_net_apply.actual_net_apply env) task_prepared ]
     | _ -> [ task_prepared ]
   in
   let command = Whyconf.get_complete_command ~with_steps:false config_prover in
@@ -130,7 +128,7 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
     | Prover.Saver ->
       answer_saver limit config env config_prover dataset_csv task
     | Marabou | Pyrat | CVC5 ->
-      answer_generic limit config prover config_prover driver task env
+      answer_generic limit config prover config_prover driver task
   in
   Logs.app (fun m ->
     m "@[Goal %a:@ %a%a@]" Pretty.print_pr (Task.task_goal task)