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. *)