# HG changeset patch
# User blanchet
# Date 1288122664 -7200
# Node ID 5da3e8ede850817f7fc5a36f99a56edcca360879
# Parent  8819ffd603576b7a8e18c2b65e47cc9a32094a0b
adapted SMT solver error handling to reflect latest changes in "SMT_Solver"

diff -r 8819ffd60357 -r 5da3e8ede850 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 21:43:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 21:51:04 2010 +0200
@@ -427,14 +427,16 @@
      run_time_in_msecs = msecs}
   end
 
-fun failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
-  | failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
-  | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError
+fun failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
+  | failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
+  | failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
+  | failure_from_smt_failure _ = UnknownError
 
 fun run_smt_solver remote ({timeout, ...} : params) minimize_command
                    ({state, subgoal, subgoal_count, facts, ...}
                     : prover_problem) =
   let
+    val ctxt = Proof.context_of state
     val {outcome, used_facts, run_time_in_msecs} =
       SMT_Solver.smt_filter remote timeout state
                             (map_filter (try dest_Untranslated) facts) subgoal
@@ -447,7 +449,8 @@
         minimize_line minimize_command (map fst used_facts)
       | SOME SMT_Solver.Time_Out => "Timed out."
       | SOME (SMT_Solver.Counterexample _) => "The SMT problem is unprovable."
-      | SOME (SMT_Solver.Other_Failure message) => message
+      | SOME failure =>
+        SMT_Solver.string_of_failure ctxt "The SMT solver" failure
     val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
   in
     {outcome = outcome, used_facts = used_facts,