# HG changeset patch
# User boehmes
# Date 1288369026 -7200
# Node ID 6efa052b9213ce6c9e206e2ea876f38d1646427e
# Parent  eed48b11abdb5cf15a851e36b1db841e126ff42b
clarified error message

diff -r eed48b11abdb -r 6efa052b9213 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Oct 29 18:17:05 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Fri Oct 29 18:17:06 2010 +0200
@@ -17,7 +17,9 @@
   else if String.isPrefix sat line then SMT_Solver.Sat
   else if String.isPrefix unknown line then SMT_Solver.Unknown
   else raise SMT_Solver.SMT (SMT_Solver.Other_Failure ("Solver " ^
-    quote solver_name ^ " failed, " ^ "see trace for details."))
+    quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
+    "configuration option " ^ quote SMT_Solver.traceN ^ " and " ^
+    " see the trace for details."))
 
 fun on_first_line test_outcome solver_name lines =
   let
diff -r eed48b11abdb -r 6efa052b9213 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 29 18:17:05 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 29 18:17:06 2010 +0200
@@ -36,6 +36,7 @@
   val datatypes: bool Config.T
   val timeout: int Config.T
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
+  val traceN: string
   val trace: bool Config.T
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val trace_used_facts: bool Config.T
@@ -128,7 +129,8 @@
   TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
   handle TimeLimit.TimeOut => raise SMT Time_Out
 
-val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false)
+val traceN = "smt_trace"
+val (trace, setup_trace) = Attrib.config_bool traceN (K false)
 
 fun trace_msg ctxt f x =
   if Config.get ctxt trace then tracing (f x) else ()