changeset 56094 | 2adbc6e4cd8f |
parent 56090 | 34bd10a9a2ad |
child 56099 | bc036c1cf111 |
--- 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)),