# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID 2adbc6e4cd8fff00c9e6cfe91a6f7df5291c884a
# Parent  4eeb73a1feec3f70d3b7e27de033314e9f5d61ce
let exception pass through in debug mode

diff -r 4eeb73a1feec -r 2adbc6e4cd8f src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -275,8 +275,7 @@
     val cprop =
       (case try negate (Thm.rhs_of (SMT2_Normalize.atomize_conv ctxt concl)) of
         SOME ct => ct
-      | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure (
-          "goal is not a HOL term")))
+      | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure "goal is not a HOL term"))
 
     val xthms = map (apsnd snd) xwthms
 
diff -r 4eeb73a1feec -r 2adbc6e4cd8f src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -27,10 +27,9 @@
   if String.isPrefix unsat line then SMT2_Solver.Unsat
   else if String.isPrefix sat line then SMT2_Solver.Sat
   else if String.isPrefix unknown line then SMT2_Solver.Unknown
-  else raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ("Solver " ^
-    quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
-    "configuration option " ^ quote (Config.name_of SMT2_Config.trace) ^ " and " ^
-    "see the trace for details."))
+  else raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure ("Solver " ^ quote solver_name ^
+    " failed -- enable tracing using the " ^ quote (Config.name_of SMT2_Config.trace) ^
+    " option for details"))
 
 fun on_first_line test_outcome solver_name lines =
   let
diff -r 4eeb73a1feec -r 2adbc6e4cd8f src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -157,7 +157,7 @@
         val {outcome, used_facts, z3_steps} =
           SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i slice_timeout
           handle exn =>
-            if Exn.is_interrupt exn then
+            if Exn.is_interrupt exn orelse debug then
               reraise exn
             else
               {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),