Replace the warning message by a fatal error

OCamlPro · Jul 21, 2023 · c194aa3 · c194aa3
1 parent 61729ca
commit c194aa3
Showing 1 changed file with 3 additions and 11 deletions.
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -357,9 +357,9 @@ let main () =
          PR. See https://github.com/OCamlPro/alt-ergo/pull/553 *)
       if Stdlib.(Options.get_sat_solver () = Tableaux) then
         Options.set_interpretation ILast
-      else Printer.print_wrn "%a The generation of models is not supported yet \
-                              by the SAT solver %a. Please use the \
-                              option `--produce-models`."
+      else Util.failwith "%a The generation of models is not supported yet \
+                          by the SAT solver %a. Please use the \
+                          option `--produce-models`."
           Loc.report st_loc Util.pp_sat_solver (Options.get_sat_solver ())
     | ":produce-models", Symbol { name = Simple "false"; _ } ->
       Options.set_interpretation INone
@@ -514,14 +514,6 @@ let main () =
             (* TODO: add the location of the statement. *)
             Printer.print_smtlib_err "No model produced.";
             st
-        else if Stdlib.(Options.get_sat_solver () <> Tableaux) then
-          begin
-            (* TODO: add the location of the statement. *)
-            Printer.print_smtlib_err
-              "get-model is not supported with the SAT solver %a."
-              Util.pp_sat_solver (Options.get_sat_solver ());
-            st
-          end
         else
           begin
             (* TODO: add the location of the statement. *)