From b57f3740ed85d001e285781d03150a09f501be83 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 19 Jul 2023 12:42:37 +0200 Subject: [PATCH] Improve error message --- src/bin/common/solving_loop.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index bcb16ccb72..20c3a5ac24 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 \ - for the SAT solver %a. Please choose the \ - SAT solver Tableaux." + else Printer.print_wrn "%a The generation of models is not supported yet \ + by the SAT solver %a. Please use the \ + meta-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 @@ -369,9 +369,9 @@ let main () = if Stdlib.(Options.get_sat_solver () = Tableaux) then Options.set_unsat_core true else Printer.print_wrn "%a The generation of unsat cores is not \ - supported for the current SAT solver. Please \ + supported by the SAT solver %a. Please \ choose the SAT solver Tableaux." - Loc.report st_loc + Loc.report st_loc Util.pp_sat_solver (Options.get_sat_solver ()) | ":produce-unsat-cores", Symbol { name = Simple "false"; _ } -> Options.set_unsat_core false | (":produce-models" | ":produce-unsat-cores" as name), _ ->