diff --git a/src/aimos.ml b/src/aimos.ml
index a74f2a26706c790fb35e7755536eaafb05904f5b..1cec3cab2b13b1817d6751f8ea2c5d1b323dd5cc 100644
--- a/src/aimos.ml
+++ b/src/aimos.ml
@@ -23,6 +23,7 @@
 open Why3
 open Base
 
+let src = Logs.Src.create "AIMOS" ~doc:"AIMOS verifier"
 let re_aimos_file = Re__Core.(compile (str "%{aimos_file}"))
 
 let write_config inputs_path models_path perturbation perturbation_path out_mode
@@ -109,7 +110,7 @@ let build_answer predicate_kind prover_result =
     | _ -> failwith "Unsupported property"
   in
   match prover_result.Call_provers.pr_answer with
-  | Call_provers.HighFailure -> (
+  | Call_provers.Unknown _ -> (
     let pr_output = prover_result.pr_output in
     match Re__Core.exec_opt re_aimos_output pr_output with
     | Some re_group ->
@@ -126,10 +127,12 @@ let build_answer predicate_kind prover_result =
       in
       prover_answer
     | None -> failwith "Cannot interpret the output provided by AIMOS")
-  | _ ->
+  | unexpected_pr_answer ->
     (* Any other answer than HighFailure should never happen as we do not define
        anything in AIMOS's driver. *)
-    assert false
+    Logging.code_error ~src (fun m ->
+      m "Unexpected AIMOS prover answer '%a'"
+        Why3.Call_provers.print_prover_answer unexpected_pr_answer)
 
 let call_prover limit config config_prover
   (predicate : (Language.nn_shape, string) Dataset.predicate) =
diff --git a/src/saver.ml b/src/saver.ml
index 2aef85892a31a804ec036ed168d4898d9adde33c..09cf70dcfb5656788327a37de0146af92cccbc7b 100644
--- a/src/saver.ml
+++ b/src/saver.ml
@@ -105,7 +105,7 @@ let negative_answer = function
 
 let build_answer_on_dataset_predicate predicate_kind prover_result =
   match prover_result.Call_provers.pr_answer with
-  | Call_provers.HighFailure -> (
+  | Call_provers.Unknown _ -> (
     let pr_output = prover_result.pr_output in
     match Re__Core.exec_opt re_saver_output pr_output with
     | Some re_group ->
@@ -165,7 +165,7 @@ let call_prover_on_dataset_predicate limit config config_prover predicate =
 
 let build_answer prover_result =
   match prover_result.Call_provers.pr_answer with
-  | Call_provers.HighFailure -> (
+  | Call_provers.Unknown _ -> (
     let pr_output = prover_result.pr_output in
     match Re__Core.exec_opt re_saver_output pr_output with
     | Some re_group ->