From 27c220a1b4eee4c981597095516fdb4de939dbca Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 18 Jul 2023 18:23:59 +0200 Subject: [PATCH] Fix the error message. --- src/bin/common/solving_loop.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 52e1be3d3..bcb16ccb7 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -358,9 +358,9 @@ let main () = 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 current SAT solver. Please choose the \ + for 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-models", Symbol { name = Simple "false"; _ } -> Options.set_interpretation INone | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } -> @@ -514,6 +514,14 @@ 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. *)