# HG changeset patch
# User boehmes
# Date 1330533821 -3600
# Node ID 4dc7ddb473501188b41b6fb071762ba19c2961b0
# Parent  c8ec1958f822ab50178c9b7e1554d259ae1ddeb5
SMT fails if the chosen SMT solver is not installed

diff -r c8ec1958f822 -r 4dc7ddb47350 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Feb 28 21:58:59 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Feb 29 17:43:41 2012 +0100
@@ -14,6 +14,7 @@
     options: Proof.context -> string list }
   val add_solver: solver_info -> Context.generic -> Context.generic
   val set_solver_options: string * string -> Context.generic -> Context.generic
+  val is_available: Proof.context -> string -> bool
   val available_solvers_of: Proof.context -> string list
   val select_solver: string -> Context.generic -> Context.generic
   val solver_of: Proof.context -> string
diff -r c8ec1958f822 -r 4dc7ddb47350 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Feb 28 21:58:59 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Feb 29 17:43:41 2012 +0100
@@ -237,10 +237,13 @@
 fun gen_apply (ithms, ctxt) =
   let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt
   in
-    (ithms, ctxt)
-    |-> invoke name command
-    |> reconstruct ctxt
-    |>> distinct (op =)
+    if not (SMT_Config.is_available ctxt name) then
+      error ("The SMT solver " ^ quote name ^ " is not installed.")
+    else
+      (ithms, ctxt)
+      |-> invoke name command
+      |> reconstruct ctxt
+      |>> distinct (op =)
   end
 
 fun apply_solver ctxt = gen_apply o gen_preprocess ctxt