From 40d14d7639231fb645451e29e3350de4ad0819ee Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 3 Oct 2022 13:18:03 +0200
Subject: [PATCH] [SAVer] Use Unknown instead of Invalid as SAVer is not
complete.
---
src/SAVer.ml | 2 +-
tests/simple_ovo.t | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/SAVer.ml b/src/SAVer.ml
index 243f156..79fd9e2 100644
--- a/src/SAVer.ml
+++ b/src/SAVer.ml
@@ -138,7 +138,7 @@ let build_answer pred_kind prover_result =
let prover_answer =
if nb_total = nb_proved
then Call_provers.Valid
- else Call_provers.Invalid
+ else Call_provers.Unknown ""
in
{ prover_answer; nb_total; nb_proved }
| None -> failwith "Cannot interpret the output provided by SAVer")
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index df79cd4..dba33cb 100644
--- a/tests/simple_ovo.t
+++ b/tests/simple_ovo.t
@@ -38,5 +38,5 @@ Test verify
> end
> EOF
[caisar] Goal G: Valid (2/2)
- [caisar] Goal H: Invalid (1/2)
- [caisar] Goal I: Invalid (0/2)
+ [caisar] Goal H: Unknown () (1/2)
+ [caisar] Goal I: Unknown () (0/2)
--
GitLab