Suspicious timeout manipulations

There are several suspicious timeout manipulations in the code. I think we should remove them, but not before having tested their impact on a realistic project.

Runner

At runner.ml lines 286-291, we have a + 0.5:

let limit wmain t =
  Why3.Call_provers.{
    limit_time = t +. 0.5 ;
    limit_mem = memlimit wmain ;
    limit_steps = (-1) ;
  }

Later on, at line 466, we see that the clockwall which is used to enforce the timeout is also set to a suspicious value:

clockwall := Unix.gettimeofday () +. timeout *. 1.5 ;

(This one might make sense if the limit one was correct, meaning we let Why3 enforce the timeout but interrupting ourselves if it delays the interruption to much)

Those two combined means that the timeout which is really applied is min (timeout * 1.5) (timeout + 0.5) and not the one the user specified

Hammer

At hammer.ml lines 200-206, we have:

let overhead t = max (t *. 2.0) 1.0

let replay_prover h d t =
  let client = if t > h.time *. 0.2 then h.client else None in
  match Prover.check_and_get_prover h.env.wenv ~patterns:h.patterns d with
  | None -> stuck
  | Some p -> prove h.env ?client p (overhead t)

The leeway in replaying a prover results make sense but * 2.0 is perhaps a lot and it seems somewhat redondant with calibration (if a 9s prover run doesn't replay, it's probably unwise to wait 9 extra seconds to be sure it doesn't)