[PyRAT] Split all tasks so that conjuctions must appear at top-level only.

src/printers/pyrat.ml

@@ -31,7 +31,6 @@ let rec print_term info fmt t =
   | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
   | Teps _ ->
     Printer.unsupportedTerm t "Not supported by PyRAT"
-  | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
   | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
   | Tapp (ls, l) -> (
     match Printer.query_syntax info.info_syn ls.ls_name with
@@ -40,6 +39,8 @@ let rec print_term info fmt t =
       match (Term.Hls.find_opt info.variables ls, l) with
       | Some s, [] -> Fmt.string fmt s
       | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
+  | Tbinop (Tand, _, _) ->
+    Printer.unsupportedTerm t "Unexpected conjunction not at top-level"
   | Tbinop (Tor, t1, t2) ->
     Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2
 

src/verification.ml

@@ -40,11 +40,9 @@ let combine_prover_answers answers =
 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 Trans.apply Split_goal.split_goal_full task_prepared
-    else [ task_prepared ]
+    (* We make [tasks] as a list (ie, conjunction) of disjunctions. *)
+    Trans.apply Split_goal.split_goal_full task_prepared
   in
   let command = Whyconf.get_complete_command ~with_steps:false prover in
   let nn_file =