# HG changeset patch # User blanchet # Date 1290683472 -3600 # Node ID 7fa054c3f810b4c0d443ca79e0312260a06800a1 # Parent a68f64f998328724cd183cd7e917b024b7329aba make "debug" mode of Sledgehammer/SMT more liberal diff -r a68f64f99832 -r 7fa054c3f810 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 00:32:30 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 12:11:12 2010 +0100 @@ -482,9 +482,9 @@ | SOME (SMT_Failure.Abnormal_Termination code) => (if verbose then "The SMT solver invoked with " ^ string_of_int num_facts ^ - " fact" ^ plural_s num_facts ^ " terminated abnormally with exit\ - \code " ^ string_of_int code ^ "." - |> (if debug then error else warning) + " fact" ^ plural_s num_facts ^ " terminated abnormally with \ + \exit code " ^ string_of_int code ^ "." + |> warning else (); true (* kind of *))