Commit cbfb1d83 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Change time limit computation.

For a measured time of 0.49 second, a prover would only get 1 second to
replay the proof, i.e., half of the expected 1.98 seconds. The time limit
is now rounded to nearest to prevent this underestimation on fast proofs.
parent 5776bfc0
......@@ -332,7 +332,7 @@ let adapt_limits ~interactive ~use_steps limits a =
(* increased time limit is 1 + twice the previous running time,
but enforced to remain inside the interval [l,2l] where l is
the previous time limit *)
let t = truncate (1.0 +. 2.0 *. t) in
let t = truncate (1.5 +. 2.0 *. t) in
let increased_time = if interactive then 0
else max timelimit (min t (2 * timelimit)) in
(* increased mem limit is just 1.5 times the previous mem limit *)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment