# HG changeset patch
# User blanchet
# Date 1357036522 -3600
# Node ID acea12b85315cf5793de51a2739173a26f3c82df
# Parent  6894f11e228b8991472535612e370f369cbecb26
Z3's soft timeout is expressed in ms, not in s -- this explains the frequenty "error code 112" failures we had recently

diff -r 6894f11e228b -r acea12b85315 src/HOL/Tools/SMT/smt_setup_solvers.ML
--- 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"]