diff --git a/src/verification.ml b/src/verification.ml index 836ff1bcb8c628832d6ed9732a2b28518451ac92..85e7b263d5d8a0439d1f7046f8a9f0b8810145d1 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -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 diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t index 120aab2d099ffa527f9d8aae7425911ec5eb3855..50150161a62f90f67fc64a2b12210acf4eb1c575 100644 --- a/tests/simple_ovo.t +++ b/tests/simple_ovo.t @@ -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)