# HG changeset patch
# User blanchet
# Date 1300810854 -3600
# Node ID 71077681eaf65bf14ee966644b4d41ef6eba45fe
# Parent  889d767ce5f47b9d412f9aa83676534a4ea35ce9
let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now

diff -r 889d767ce5f4 -r 71077681eaf6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 22 17:20:53 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Mar 22 17:20:54 2011 +0100
@@ -495,8 +495,6 @@
 val smt_failures =
   remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
 
-val internal_error_prefix = "Internal error: "
-
 fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
@@ -506,8 +504,7 @@
                              string_of_int code ^ "."))
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
-    if String.isPrefix internal_error_prefix msg then InternalError
-    else UnknownError msg
+    UnknownError msg
 
 (* FUDGE *)
 val smt_max_iters = Unsynchronized.ref 8
@@ -565,7 +562,7 @@
           handle exn => if Exn.is_interrupt exn then
                           reraise exn
                         else
-                          (internal_error_prefix ^ ML_Compiler.exn_message exn
+                          (ML_Compiler.exn_message exn
                            |> SMT_Failure.Other_Failure |> SOME, [])
         val death = Timer.checkRealTimer timer
         val _ =