From c194aa3a56e8c3f8d44816e21185cecf104432cb Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 21 Jul 2023 14:09:04 +0200 Subject: [PATCH] Replace the warning message by a fatal error --- src/bin/common/solving_loop.ml | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 3fa92e79cc..9a2cd01809 100644 --- 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. *)