src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 62826 eb94e570c1a4
parent 62735 23de054397e5
child 63692 1bc4bc2c9fd1
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -130,8 +130,8 @@
     1.4  
     1.5          val death = Timer.checkRealTimer timer
     1.6          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
     1.7 -        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
     1.8 -        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
     1.9 +        val time_so_far = time_so_far + (death - birth)
    1.10 +        val timeout = timeout - Timer.checkRealTimer timer
    1.11  
    1.12          val too_many_facts_perhaps =
    1.13            (case outcome of
    1.14 @@ -143,7 +143,7 @@
    1.15            | SOME (SMT_Failure.Other_Failure _) => true)
    1.16        in
    1.17          if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
    1.18 -           Time.> (timeout, Time.zeroTime) then
    1.19 +           timeout > Time.zeroTime then
    1.20            let
    1.21              val new_num_facts =
    1.22                Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)