# HG changeset patch
# User blanchet
# Date 1292433032 -3600
# Node ID 043f8dc3b51f41232cbe29fcad361421208b6a14
# Parent  5645aaee6b3873ba1c622f0079e728bb6a5fdfd1
facilitate debugging

diff -r 5645aaee6b38 -r 043f8dc3b51f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 17:43:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 18:10:32 2010 +0100
@@ -458,7 +458,7 @@
 val smt_iter_min_msecs = Unsynchronized.ref 5000
 val smt_monomorph_limit = Unsynchronized.ref 4
 
-fun smt_filter_loop ({verbose, timeout, ...} : params) remote state i =
+fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
   let
     val ctxt = Proof.context_of state
     fun iter timeout iter_num outcome0 time_so_far facts =
@@ -482,6 +482,11 @@
           else
             ()
         val birth = Timer.checkRealTimer timer
+        val _ =
+          if debug then
+            Output.urgent_message "Invoking SMT solver..."
+          else
+            ()
         val {outcome, used_facts, ...} =
           SMT_Solver.smt_filter remote iter_timeout state facts i
         val death = Timer.checkRealTimer timer
@@ -489,6 +494,8 @@
           if verbose andalso is_some outcome then
             "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
             |> Output.urgent_message
+          else if debug then
+            Output.urgent_message "SMT solver returned."
           else
             ()
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
diff -r 5645aaee6b38 -r 043f8dc3b51f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 17:43:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 18:10:32 2010 +0100
@@ -180,9 +180,11 @@
                                   | (false, _) => run_prover problem prover)
                    provers (false, state)
             else
-              provers |> (if blocking then Par_List.map else map)
-                             (run_prover problem)
-                      |> exists fst |> rpair state
+              provers
+              |> (if blocking andalso length provers > 1 then Par_List.map
+                  else map)
+                     (run_prover problem)
+              |> exists fst |> rpair state
           end
       val run_atps =
         run_provers "ATP" no_dangerous_types atp_relevance_fudge