Z3's soft timeout is expressed in ms, not in s -- this explains the frequenty "error code 112" failures we had recently

--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Jan 01 10:53:43 2013 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Jan 01 11:35:22 2013 +0100
@@ -148,7 +148,7 @@
     ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
       "MODEL=true",
       "SOFT_TIMEOUT=" ^
-        string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
+        string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout)),
       "-smt"]
     |> not (Config.get ctxt SMT_Config.oracle) ?
          append ["DISPLAY_PROOF=true", "PROOF_MODE=2"]