[verification] Interpret task for classic provers also.

On such tasks, the interpretation should provide no effect.

src/verification.ml

@@ -223,8 +223,9 @@ 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 ~strategy task =
-  let tasks = strategy env task in
+let answer_generic limit config env prover config_prover driver ~proof_strategy
+  task =
+  let tasks = proof_strategy env task in
   let answers =
     List.concat_map tasks ~f:(fun task ->
       let task = Driver.prepare_task driver task in
@@ -263,11 +264,14 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task
       answer_dataset limit config env prover config_prover driver dataset task
     | Marabou | Pyrat | Nnenum ->
       let task = Interpretation.interpret_task ~cwd env task in
-      let strategy = Proof_strategy.apply_native_nn_prover in
-      answer_generic limit config env prover config_prover driver ~strategy task
+      let proof_strategy = Proof_strategy.apply_native_nn_prover in
+      answer_generic limit config env prover config_prover driver
+        ~proof_strategy task
     | CVC5 ->
-      let strategy = Proof_strategy.apply_classic_prover in
-      answer_generic limit config env prover config_prover driver ~strategy task
+      let task = Interpretation.interpret_task ~cwd env task in
+      let proof_strategy = Proof_strategy.apply_classic_prover in
+      answer_generic limit config env prover config_prover driver
+        ~proof_strategy task
   in
   let id = Task.task_goal task in
   { id; prover_answer; additional_info }