Commit 18e1c2ce authored by Sylvain Dailler's avatar Sylvain Dailler

Change steps used when replaying a proof (add one step).

parent 25fa146f
......@@ -275,7 +275,15 @@ let adapt_limits ~interactive ~use_steps limits a =
| Call_provers.Timeout -> timelimit, increased_mem, steplimit
| Call_provers.Valid ->
let steplimit =
if use_steps && not a.proof_obsolete then s else 0
if use_steps && not a.proof_obsolete then
(* We need to allow at least one more step than what was used to
prove the same statement. Otherwise, the prover run out of
steps: this happens with cvc4 on some very fast proofs
(steps = 28).
*)
s + 1
else
0
in
increased_time, increased_mem, steplimit
| Call_provers.Unknown _
......
Markdown is supported
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