diff --git a/src/saver.ml b/src/SAVer.ml similarity index 100% rename from src/saver.ml rename to src/SAVer.ml diff --git a/src/saver.mli b/src/SAVer.mli similarity index 93% rename from src/saver.mli rename to src/SAVer.mli index 2bec2d23605e691463c168bf83d5d16bc2af7589..2119b52d22cdacc5703155d261141de6b073267c 100644 --- a/src/saver.mli +++ b/src/SAVer.mli @@ -24,8 +24,8 @@ open Why3 type answer = { prover_answer : Call_provers.prover_answer; - nb_total : int; (* Total number of data points. *) - nb_proved : int; (* Number of data points verifying the property. *) + nb_total : int; (** Total number of data points. *) + nb_proved : int; (** Number of data points verifying the property. *) } val call : diff --git a/src/verification.ml b/src/verification.ml index 2d12c9dd196f7e5380cd09dc0346619def7c70b4..836ff1bcb8c628832d6ed9732a2b28518451ac92 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -74,7 +74,7 @@ let answer_saver limit config env config_prover dataset_csv task = | None -> invalid_arg "No dataset provided for SAVer" | Some filename -> filename in - let answer = Saver.call limit config env config_prover ~dataset task in + let answer = SAVer.call limit config env config_prover ~dataset task in let prover_answer = answer.prover_answer in let additional_info = Fmt.str "(%d/%d)" answer.nb_proved answer.nb_total in (prover_answer, Some additional_info)