[json] Rename result into prover_answer.

src/JSON.ml

@@ -42,7 +42,7 @@ and property = {
 
 type output = {
   id : string;
-  result : prover_answer;
+  prover_answer : prover_answer;
   percentage_valid : float;
   dataset_results : string;
 }

src/JSON.mli

@@ -41,7 +41,7 @@ and property = private {
 
 type output = {
   id : string;
-  result : prover_answer;
+  prover_answer : prover_answer;
   percentage_valid : float;
   dataset_results : string;
 }

src/main.ml

@@ -125,13 +125,13 @@ let log_theory_answer =
     Logs.info (fun m ->
       m "@[Verification results for theory '%s'@]" theory_name);
     List.iter task_answers
-      ~f:(fun { Verification.id; result; additional_info } ->
+      ~f:(fun { Verification.id; prover_answer; additional_info } ->
       let additional_info =
         match additional_info with Generic s -> s | Dataset _ -> None
       in
       Logs.app (fun m ->
         m "@[Goal %a:@ %a%a@]" Pretty.print_pr id
-          Call_provers.print_prover_answer result
+          Call_provers.print_prover_answer prover_answer
           Fmt.(option ~none:nop (any " " ++ string))
           additional_info)))
 
@@ -149,7 +149,7 @@ let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
   List.iter theory_answers ~f:log_theory_answer;
   theory_answers
 
-let record_dataset_results id result dataset outfile =
+let record_dataset_results id prover_answer dataset outfile =
   let percentage_valid =
     let nb_valid =
       List.count dataset ~f:(fun record ->
@@ -170,7 +170,7 @@ let record_dataset_results id result dataset outfile =
     Csv.close_out csv_out_channel;
     dataset_results
   in
-  let output = { JSON.id; result; percentage_valid; dataset_results } in
+  let output = { JSON.id; prover_answer; percentage_valid; dataset_results } in
   let out_channel = Stdlib.open_out outfile in
   Yojson.Safe.to_channel out_channel (JSON.output_to_yojson output);
   Logs.info (fun m -> m "@[Results recorded in file '%s'@]" outfile);
@@ -179,8 +179,9 @@ let record_dataset_results id result dataset outfile =
 let record_theory_answers id outfile =
   Why3.Wstdlib.Mstr.iter (fun theory_name task_answers ->
     match task_answers with
-    | [ { Verification.result; additional_info = Dataset dataset; _ } ] ->
-      record_dataset_results id result dataset outfile
+    | [ { Verification.prover_answer; additional_info = Dataset dataset; _ } ]
+      ->
+      record_dataset_results id prover_answer dataset outfile
     | _ -> failwith (Fmt.str "Unexpected answers for theory '%s'" theory_name))
 
 let verify_json ?memlimit ?timelimit ?outfile json =

src/verification.ml

@@ -61,7 +61,7 @@ type theory_answer = answer list Wstdlib.Mstr.t
 
 and answer = {
   id : Decl.prsymbol;
-  result : Call_provers.prover_answer;
+  prover_answer : Call_provers.prover_answer;
   additional_info : additional_info;
 }
 
@@ -223,7 +223,7 @@ let answer_generic limit config env prover config_prover driver task =
   (prover_answer, None)
 
 let call_prover ?dataset ~limit config env prover config_prover driver task =
-  let result, additional_info =
+  let prover_answer, additional_info =
     match prover with
     | Prover.Saver ->
       let prover_answer, additional_info =
@@ -243,7 +243,7 @@ let call_prover ?dataset ~limit config env prover config_prover driver task =
       (prover_answer, Generic additional_info)
   in
   let id = Task.task_goal task in
-  { id; result; additional_info }
+  { id; prover_answer; additional_info }
 
 let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
   prover ?prover_altern file =

src/verification.mli

@@ -34,7 +34,7 @@ type theory_answer = answer list Wstdlib.Mstr.t
 
 and answer = private {
   id : Decl.prsymbol;
-  result : Call_provers.prover_answer;
+  prover_answer : Call_provers.prover_answer;
   additional_info : additional_info;
 }