diff --git a/src/SAVer.ml b/src/SAVer.ml
index 243f1561ef1b4669c8e4f1c5c2ed1103ba1ea1cf..79fd9e2cd0eb24ddb6bf35639785e9c393c591ae 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 df79cd4207e880575e59b8298bfdcba05c6c6825..dba33cb4121b6639d475be22ce2d2f45456d63a9 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)