--- 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
--- 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 ()