# HG changeset patch
# User blanchet
# Date 1289148685 -3600
# Node ID f2fbea1e5f9e1d4ea2f13d17441f195bda16d16b
# Parent  36b7ed41ca9ff36a30b5efc9a44a6f47ac73faa0
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed

diff -r 36b7ed41ca9f -r f2fbea1e5f9e src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 13:29:59 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 17:51:25 2010 +0100
@@ -417,11 +417,12 @@
 val smt_filter_max_iter = 5
 val smt_filter_fact_divisor = 2
 
-fun smt_filter_loop iter msecs_so_far remote timeout state facts i =
+fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
   let
     val timer = Timer.startRealTimer ()
     val {outcome, used_facts, run_time_in_msecs} =
       SMT_Solver.smt_filter remote timeout state facts i
+    val outcome0 = if is_none outcome0 then SOME outcome else outcome0
     val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
     val too_many_facts_perhaps =
       case outcome of
@@ -434,13 +435,13 @@
     if too_many_facts_perhaps andalso iter < smt_filter_max_iter andalso
        not (null facts) then
       let val facts = take (length facts div smt_filter_fact_divisor) facts in
-        smt_filter_loop (iter + 1) msecs_so_far remote
+        smt_filter_loop (iter + 1) outcome0 msecs_so_far remote
                         (Time.- (timeout, Timer.checkRealTimer timer)) state
                         facts i
       end
     else
-      {outcome = outcome, used_facts = used_facts,
-       run_time_in_msecs = msecs_so_far}
+      {outcome = if is_none outcome then NONE else the outcome0,
+       used_facts = used_facts, run_time_in_msecs = msecs_so_far}
   end
 
 fun run_smt_solver auto remote ({timeout, ...} : params) minimize_command
@@ -449,7 +450,7 @@
   let
     val ctxt = Proof.context_of state
     val {outcome, used_facts, run_time_in_msecs} =
-      smt_filter_loop 1 (SOME 0) remote timeout state
+      smt_filter_loop 1 NONE (SOME 0) remote timeout state
                       (map_filter (try dest_Untranslated) facts) subgoal
     val message =
       case outcome of