Better error message on missing solver

lib/dune

@@ -104,24 +104,29 @@
     z3_mappings.nop.ml
     (progn
      (echo "let solver_name = \"Z3\"\n")
+     (echo "let solver_package = \"z3\"\n")
      (cat mappings.nop.ml)))
    (with-stdout-to
     z3_mappings2.nop.ml
     (progn
      (echo "let solver_name = \"Z3\"\n")
+     (echo "let solver_package = \"z3\"\n")
      (cat mappings.nop.ml)))
    (with-stdout-to
     colibri2_mappings.nop.ml
     (progn
      (echo "let solver_name = \"Colibri2\"\n")
+     (echo "let solver_package = \"colibri2\"\n")
      (cat mappings.nop.ml)))
    (with-stdout-to
     bitwuzla_mappings.nop.ml
     (progn
      (echo "let solver_name = \"Bitwuzla\"\n")
+     (echo "let solver_package = \"bitwuzla-cxx\"\n")
      (cat mappings.nop.ml)))
    (with-stdout-to
     cvc5_mappings.nop.ml
     (progn
      (echo "let solver_name = \"cvc5\"\n")
+     (echo "let solver_package = solver_name\n")
      (cat mappings.nop.ml))))))

lib/mappings.nop.ml

@@ -300,7 +300,16 @@ module Nop = struct
       let eval ?completion:_ _ = assert false
     end
 
-    let die () = Fmt.failwith "%s not installed" solver_name
+    let die () =
+      Fmt.epr
+        "The %s solver is not installed. You must install it through opam with \
+         the command `opam install %s`. You could also try to use another \
+         solver (have a look at the supported solvers here: \
+         https://github.com/formalsec/smtml?tab=readme-ov-file#supported-solvers). \
+         Note that installing the solver with your system package manager is \
+         not enough, you must install it through opam."
+        solver_name solver_package;
+      exit 1
 
     module Solver = struct
       let make ?params:_ ?logic:_ = die ()

test/regression/dune

@@ -2,6 +2,11 @@
  (enabled_if %{lib-available:z3})
  (deps %{bin:smtml} test_pr_71.smtml))
 
+(cram
+ (applies_to test_issue_183)
+ (enabled_if
+  (not %{lib-available:colibri2})))
+
 (tests
  (names test_pr_77)
  (libraries smtml))

test/regression/test_issue_183.t

@@ -0,0 +1,8 @@
+Test solver not installed error message:
+  $ smtml run --solver colibri2 <<EOF
+  > (let-const x int)
+  > (assert (= x 1))
+  > (check-sat)
+  > EOF
+  The Colibri2 solver is not installed. You must install it through opam with the command `opam install colibri2`. You could also try to use another solver (have a look at the supported solvers here: https://github.com/formalsec/smtml?tab=readme-ov-file#supported-solvers). Note that installing the solver with your system package manager is not enough, you must install it through opam.
+  [1]