# HG changeset patch
# User boehmes
# Date 1330593178 -3600
# Node ID 8e365bc843e9641ae7ef1f2120d3ceab22e46f56
# Parent  4dc7ddb473501188b41b6fb071762ba19c2961b0
fine-tune intended failure of smt method when the chosen SMT solver is not installed: restrict failures to true invocations of the SMT solver and don't fail for runs based on certificates

diff -r 4dc7ddb47350 -r 8e365bc843e9 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Feb 29 17:43:41 2012 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Mar 01 10:12:58 2012 +0100
@@ -65,7 +65,9 @@
 fun run ctxt name mk_cmd input =
   (case SMT_Config.certificates_of ctxt of
     NONE =>
-      if Config.get ctxt SMT_Config.debug_files = "" then
+      if not (SMT_Config.is_available ctxt name) then
+        error ("The SMT solver " ^ quote name ^ " is not installed.")
+      else if Config.get ctxt SMT_Config.debug_files = "" then
         trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
           (Cache_IO.run mk_cmd) input
       else
@@ -237,13 +239,10 @@
 fun gen_apply (ithms, ctxt) =
   let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt
   in
-    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 =)
+    (ithms, ctxt)
+    |-> invoke name command
+    |> reconstruct ctxt
+    |>> distinct (op =)
   end
 
 fun apply_solver ctxt = gen_apply o gen_preprocess ctxt