From 05ce7976a67b8ecbbf6cd123b6d83d872aad633f Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 5 Oct 2022 16:23:58 +0200
Subject: [PATCH] [SAVer] Harmonize output on SAVer's Unknown answer.
No "empty parenthesis" anymore.
---
src/verification.ml | 12 +++++++++---
tests/simple_ovo.t | 2 +-
2 files changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 836ff1b..85e7b26 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 120aab2..5015016 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)
--
GitLab