From d639b04494ee79db7f7b2ad94613fa505614c2f0 Mon Sep 17 00:00:00 2001
From: Steven de Oliveira <de.oliveira.steven@gmail.com>
Date: Tue, 12 Dec 2023 14:20:15 +0100
Subject: [PATCH] Poetry

---
 src/bin/common/solving_loop.ml | 33 +++++++++++++++------------------
 1 file changed, 15 insertions(+), 18 deletions(-)

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 243b8c4059..c11b4edad3 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -133,22 +133,19 @@ type solve_res =
   | Unknown of model option
   | Unsat of Explanation.t
 
-let check_status_consistency s =
-  let known_status = Options.get_status () in
-  match s with
-  | Unsat _ ->
-    if known_status == Status_Sat then begin
-      Printer.print_wrn
-        "This file is known to be Sat but Alt-Ergo return Unsat";
-      Errors.warning_as_error ()
-    end
-  | Sat _ ->
-    if known_status == Status_Unsat then begin
-      Printer.print_wrn
-        "This file is known to be Unsat but Alt-Ergo return Sat";
-      Errors.warning_as_error ()
-    end
-  | Unknown _ -> assert false
+let check_sat_status () =
+  match Options.get_status () with
+  | Status_Unsat ->
+    recoverable_error
+      "This file is known to be Unsat but Alt-Ergo return Sat";
+  | _ -> ()
+
+let check_unsat_status () =
+  match Options.get_status () with
+  | Status_Unsat ->
+    recoverable_error
+      "This file is known to be Sat but Alt-Ergo return Unsat";
+  | _ -> ()
 
 let print_solve_res loc goal_name r =
   let validity_mode =
@@ -162,7 +159,7 @@ let print_solve_res loc goal_name r =
   | Sat _ ->
     Printer.print_status_sat ~validity_mode
       (Some loc) (Some time) (Some steps) (Some goal_name);
-    check_status_consistency r;
+    check_sat_status ();
   | Unsat dep ->
     Printer.print_status_unsat ~validity_mode
       (Some loc) (Some time) (Some steps) (Some goal_name);
@@ -173,7 +170,7 @@ let print_solve_res loc goal_name r =
       Printer.print_fmt (Options.Output.get_fmt_regular ())
         "unsat-core:@,%a@."
         (Explanation.print_unsat_core ~tab:true) dep;
-    check_status_consistency r
+    check_unsat_status ()
   | Unknown _ ->
     Printer.print_status_unknown ~validity_mode
       (Some loc) (Some time) (Some steps) (Some goal_name);