diff --git a/src/transformations/split_disjunction.ml b/src/transformations/split_disjunction.ml
new file mode 100644
index 0000000000000000000000000000000000000000..96518e98a6408460bda5ea429b448fac8d8baf3f
--- /dev/null
+++ b/src/transformations/split_disjunction.ml
@@ -0,0 +1,13 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Base
+open Why3
+
+let split_disjunction =
+  Trans.goal_l (fun pr t ->
+    let l = Split_goal.split_neg_full t in
+    List.map l ~f:(fun t -> [ Decl.create_prop_decl Pgoal pr t ]))
diff --git a/src/verification.ml b/src/verification.ml
index aaf623e0fe9c325aa70053741590bfc3dc7f7e32..b274a68e186bc5e0c4efb84e16e893dfdaf4c565 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -28,9 +28,19 @@ let create_env loadpath =
 
 let nnet_or_onnx = Re.compile (Re.str "%{nnet-onnx}")
 
-let call_prover ~limit prover driver task =
+let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
   let open Why3 in
   let task_prepared = Driver.prepare_task driver task in
+  let tasks =
+    if String.equal prover.prover.prover_name "Marabou"
+    then
+      let conjs = Trans.apply Split_goal.split_goal_full task_prepared in
+      let disjs =
+        List.map ~f:(Trans.apply Split_disjunction.split_disjunction) conjs
+      in
+      disjs
+    else [ [ task_prepared ] ]
+  in
   let command = Whyconf.get_complete_command ~with_steps:false prover in
   let nn_file =
     match Task.on_meta_excl Native_nn_prover.meta_nn_filename task_prepared with
@@ -39,12 +49,28 @@ let call_prover ~limit prover driver task =
     | None -> invalid_arg (Fmt.str "No neural network model found in task")
   in
   let command = Re.replace_string nnet_or_onnx ~by:nn_file command in
-  let prover_call =
-    Driver.prove_task_prepared ~command ~limit driver task_prepared
+  let call_task task_prepared =
+    let prover_call =
+      Driver.prove_task_prepared ~command ~limit driver task_prepared
+    in
+    let prover_result = Call_provers.wait_on_call prover_call in
+    prover_result.pr_answer
+  in
+  let results = List.map tasks ~f:(List.map ~f:call_task) in
+  let answer =
+    List.fold_left results ~init:Call_provers.Valid ~f:(fun r1 l2 ->
+      let r2 =
+        List.fold_left l2 ~init:Call_provers.Invalid ~f:(fun r1 r2 ->
+          match (r1, r2) with
+          | Call_provers.Valid, _ | _, Call_provers.Valid -> Call_provers.Valid
+          | _ -> r2)
+      in
+      match (r1, r2) with
+      | Call_provers.Valid, r | r, Call_provers.Valid -> r
+      | _ -> r1)
   in
-  let prover_result = Call_provers.wait_on_call prover_call in
   Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
-    Call_provers.print_prover_answer prover_result.pr_answer
+    Call_provers.print_prover_answer answer
 
 let verify format loadpath ?memlimit ~prover file =
   let open Why3 in
diff --git a/tests/marabout.t b/tests/marabout.t
index 78194e3b714a2b6f0fe5afd6ee7b14da311adb4b..16ae72e58d27f9a736685124d708b4e0cff2a60b 100644
--- a/tests/marabout.t
+++ b/tests/marabout.t
@@ -27,6 +27,11 @@ Test verify
   >      (0.0:t) .< x1 .< (0.5:t) ->
   >      let (y1,_,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
   >      (0.0:t) .< y1 .< (0.5:t)
+  > 
+  >   goal H: forall x1 x2 x3 x4 x5.
+  >      (0.0:t) .< x1 .< (0.5:t) /\ (0.5:t) .< x2 .< (1.0:t) ->
+  >      let (y1,y2,_,_,_) = nnet_apply x1 x2 x3 x4 x5 in
+  >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
   <autodetect>0 prover(s) added
@@ -40,3 +45,5 @@ Test verify
   <autodetect>3 prover(s) added
   Goal G: Unknown
   ()
+  Goal H: Unknown
+  ()