Sane(r) error messages for produce-models error situations

This is a reloaded version of OCamlPro#738 with tests.

Fixes OCamlPro#737

src/bin/common/solving_loop.ml

@@ -362,10 +362,10 @@ 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 current SAT solver. Please choose the \
-                              SAT solver Tableaux."
-          Loc.report st_loc
+      else
+        Printer.print_smtlib_err
+          "Model generation requires the Tableaux solver \
+           (try --produce-models)";
     | ":produce-models", Symbol { name = Simple "false"; _ } ->
       Options.set_interpretation INone
     | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } ->
@@ -523,9 +523,7 @@ let main () =
           begin
             (* TODO: add the location of the statement. *)
             Printer.print_smtlib_err
-              "You have to set the flag :produce-models with \
-               (set-option :produce-models true) \
-               before using the statement (get-model).";
+              "Model generation disabled (try --produce-models)";
             st
           end
 

tests/cram.t/run.t

@@ -45,3 +45,45 @@ And some SMT2 action.
   unknown
 
   unsat
+
+Here are some tests to check that we have sane behavior given the insane
+combinations of produce-models et al.
+
+First, if model generation is not enabled, we should error out when a
+`(get-model)` statement is issued:
+
+  $ echo '(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2
+  (error "Model generation disabled (try --produce-models)")
+
+This should be the case Tableaux solver as well:
+
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  (error "Model generation disabled (try --produce-models)")
+
+The messages above mention `--produce-models`, but we can also use
+`set-option`. This requires the Tableaux solver, however:
+
+  $ echo '(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2
+  (error "No model produced.")
+
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2
+  (error "No model produced.")
+
+  $ echo '(set-option :produce-models true)(get-model)' | alt-ergo --frontend dolmen -i smtlib2 -o smtlib2
+  (error "Model generation requires the Tableaux solver (try --produce-models)")
+  (error "Model generation disabled (try --produce-models)")
+
+And now some cases where it should work (using either `--produce-models` or
+`Tableaux` with `set-option`):
+
+  $ echo '(check-sat)(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 2>/dev/null
+
+  unknown
+  (
+  )
+
+  $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null
+
+  unknown
+  (
+  )