diff --git a/src/transformations/actual_net_apply.mli b/src/transformations/actual_net_apply.mli
index e45ca3e9317f1bd26d2c74f04dc67cb3e34baf60..f4c6a6be9a0bf09b9579df6ef48a30335ca42b49 100644
--- a/src/transformations/actual_net_apply.mli
+++ b/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. *)
diff --git a/src/verification.ml b/src/verification.ml
index d0e5f1a54abd2971fecb2472cf4ec2d0f54efa2d..2541404a9d3625ac312caaffe61067c605b8112c 100644
--- a/src/verification.ml
+++ b/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)