Poetry

Stevendeo · Dec 12, 2023 · d639b04 · d639b04
1 parent 8b80218
commit d639b04
Showing 1 changed file with 15 additions and 18 deletions.
diff --git 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);