Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
honour timeouts which are not rounded to full seconds
authorboehmes
Mon, 15 Nov 2010 22:23:26 +0100
changeset 40560 b57f7fee72ee
parent 40558 e75614d0a859
child 40561 0125cbb5d3c7
honour timeouts which are not rounded to full seconds
src/HOL/Tools/SMT/smt_solver.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 21:08:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 15 22:23:26 2010 +0100
@@ -308,7 +308,7 @@
     val ctxt =
       Proof.context_of st
       |> Config.put C.oracle false
-      |> Config.put C.timeout (Real.fromInt (Time.toSeconds time_limit))
+      |> Config.put C.timeout (Time.toReal time_limit)
       |> Config.put C.drop_bad_facts true
       |> Config.put C.filter_only_facts true
     val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
isabelle