diff --git a/src/prover.mli b/src/prover.mli
index 2d0dba9fb28d59d7dbe18bc28be0ec90c19f2755..cf4ff02423623408a861905c0da8da1c9aebf2ac 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type t = private Marabou | Pyrat | Saver
+type t = private Marabou | Pyrat | Saver | CVC5
 
 val list_available : unit -> t list
 val of_string : string -> t option
diff --git a/src/transformations/actual_net_apply.mli b/src/transformations/actual_net_apply.mli
index f4c6a6be9a0bf09b9579df6ef48a30335ca42b49..e45ca3e9317f1bd26d2c74f04dc67cb3e34baf60 100644
--- a/src/transformations/actual_net_apply.mli
+++ b/src/transformations/actual_net_apply.mli
@@ -14,5 +14,9 @@
     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 4e26a9ad0d1376345aa8cadb672d4f12c6cc5e36..d0e5f1a54abd2971fecb2472cf4ec2d0f54efa2d 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -93,13 +93,14 @@ 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 =
+let answer_generic limit config prover config_prover driver task env =
   let task_prepared = Driver.prepare_task driver task in
   let tasks =
-    (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
     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
@@ -128,8 +129,8 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
     match prover with
     | Prover.Saver ->
       answer_saver limit config env config_prover dataset_csv task
-    | Marabou | Pyrat ->
-      answer_generic limit config prover config_prover driver task
+    | Marabou | Pyrat | CVC5 ->
+      answer_generic limit config prover config_prover driver task env
   in
   Logs.app (fun m ->
     m "@[Goal %a:@ %a%a@]" Pretty.print_pr (Task.task_goal task)