Skip to content
Snippets Groups Projects
Commit 05ce7976 authored by Michele Alberti's avatar Michele Alberti
Browse files

[SAVer] Harmonize output on SAVer's Unknown answer.

No "empty parenthesis" anymore.
parent 9a680abf
No related branches found
No related tags found
No related merge requests found
......@@ -75,9 +75,15 @@ let answer_saver limit config env config_prover dataset_csv task =
| Some filename -> filename
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)
match answer.prover_answer with
| Call_provers.Unknown "" ->
let additional_info = Fmt.str "%d/%d" answer.nb_proved answer.nb_total in
(Call_provers.Unknown additional_info, None)
| Call_provers.Unknown _ ->
assert false (* By construction of SAVer's Unknown answer. *)
| prover_answer ->
let additional_info = Fmt.str "(%d/%d)" answer.nb_proved answer.nb_total in
(prover_answer, Some additional_info)
let answer_generic limit config prover config_prover driver task =
let task_prepared = Driver.prepare_task driver task in
......
......@@ -39,4 +39,4 @@ Test verify
> EOF
[caisar] Goal G: Valid (2/2)
[caisar] Goal H: Invalid (1/2)
[caisar] Goal I: Unknown () (0/2)
[caisar] Goal I: Unknown (0/2)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment