diff --git a/src/verification.ml b/src/verification.ml
index 5bfa184cb9d5a03e28acc0c2a6c5561803a07750..2a9bfbd8d9f020dcf0d60c964bceb4b319652e6a 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -32,26 +32,19 @@ let nnet_or_onnx = Re.compile (Re.str "%{nnet-onnx}")
 
 let combine_prover_answers answers =
   let open Why3 in
-  List.fold_left answers ~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
+  List.fold_left answers ~init:Call_provers.Valid ~f:(fun acc r ->
+    match (acc, r) with
     | Call_provers.Valid, r | r, Call_provers.Valid -> r
-    | _ -> r1)
+    | _ -> acc)
 
 let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
   let open Why3 in
   let task_prepared = Driver.prepare_task driver task in
+  (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
   let tasks =
     if String.equal prover.prover.prover_name "Marabou"
-    then
-      let conjs = Trans.apply Split_goal.split_goal_full task_prepared in
-      List.map ~f:(fun c -> [ c ]) conjs
-    else [ [ task_prepared ] ]
+    then Trans.apply Split_goal.split_goal_full task_prepared
+    else [ task_prepared ]
   in
   let command = Whyconf.get_complete_command ~with_steps:false prover in
   let nn_file =
@@ -68,7 +61,7 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
     let prover_result = Call_provers.wait_on_call prover_call in
     prover_result.pr_answer
   in
-  let answers = List.map tasks ~f:(List.map ~f:call_prover_on_task) in
+  let answers = List.map tasks ~f:call_prover_on_task in
   let answer = combine_prover_answers answers in
   Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
     Call_provers.print_prover_answer answer