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