[verification] Apply strategy before calling answer_generic.

src/verification.ml

@@ -223,18 +223,7 @@ let answer_dataset limit config env prover config_prover driver dataset task =
   in
   (prover_answer, additional_info)
 
-let answer_generic limit config env prover config_prover driver task =
-  let task =
-    let proof_strategy =
-      match prover with
-      | Prover.Marabou | Pyrat | Nnenum -> Proof_strategy.apply_native_nn_prover
-      | CVC5 -> Proof_strategy.apply_classic_prover
-      | _ ->
-        (* Only previous provers admitted here. *)
-        assert false
-    in
-    proof_strategy env task
-  in
+let answer_generic limit config prover config_prover driver task =
   let task = Driver.prepare_task driver task in
   let nn_file =
     match Task.on_meta_excl Utils.meta_nn_filename task with
@@ -266,8 +255,12 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
     | (Marabou | Pyrat | Nnenum) when Option.is_some dataset ->
       let dataset = Unix.realpath (Option.value_exn dataset) in
       answer_dataset limit config env prover config_prover driver dataset task
-    | Marabou | Pyrat | Nnenum | CVC5 ->
-      answer_generic limit config env prover config_prover driver task
+    | Marabou | Pyrat | Nnenum ->
+      let task = Proof_strategy.apply_native_nn_prover env task in
+      answer_generic limit config prover config_prover driver task
+    | CVC5 ->
+      let task = Proof_strategy.apply_classic_prover env task in
+      answer_generic limit config prover config_prover driver task
   in
   let id = Task.task_goal task in
   { id; prover_answer; additional_info }