[test] Updated AIMOS and SAVER prover answer to match Why3 1.7 prover output

src/aimos.ml

@@ -23,6 +23,7 @@
 open Why3
 open Base
 
+let src = Logs.Src.create "AIMOS" ~doc:"AIMOS verifier"
 let re_aimos_file = Re__Core.(compile (str "%{aimos_file}"))
 
 let write_config inputs_path models_path perturbation perturbation_path out_mode
@@ -109,7 +110,7 @@ let build_answer predicate_kind prover_result =
     | _ -> failwith "Unsupported property"
   in
   match prover_result.Call_provers.pr_answer with
-  | Call_provers.HighFailure -> (
+  | Call_provers.Unknown _ -> (
     let pr_output = prover_result.pr_output in
     match Re__Core.exec_opt re_aimos_output pr_output with
     | Some re_group ->
@@ -126,10 +127,12 @@ let build_answer predicate_kind prover_result =
       in
       prover_answer
     | None -> failwith "Cannot interpret the output provided by AIMOS")
-  | _ ->
+  | unexpected_pr_answer ->
     (* Any other answer than HighFailure should never happen as we do not define
        anything in AIMOS's driver. *)
-    assert false
+    Logging.code_error ~src (fun m ->
+      m "Unexpected AIMOS prover answer '%a'"
+        Why3.Call_provers.print_prover_answer unexpected_pr_answer)
 
 let call_prover limit config config_prover
   (predicate : (Language.nn_shape, string) Dataset.predicate) =

src/saver.ml

@@ -105,7 +105,7 @@ let negative_answer = function
 
 let build_answer_on_dataset_predicate predicate_kind prover_result =
   match prover_result.Call_provers.pr_answer with
-  | Call_provers.HighFailure -> (
+  | Call_provers.Unknown _ -> (
     let pr_output = prover_result.pr_output in
     match Re__Core.exec_opt re_saver_output pr_output with
     | Some re_group ->
@@ -165,7 +165,7 @@ let call_prover_on_dataset_predicate limit config config_prover predicate =
 
 let build_answer prover_result =
   match prover_result.Call_provers.pr_answer with
-  | Call_provers.HighFailure -> (
+  | Call_provers.Unknown _ -> (
     let pr_output = prover_result.pr_output in
     match Re__Core.exec_opt re_saver_output pr_output with
     | Some re_group ->