Commit 6fe88dfc authored by MARCHE Claude's avatar MARCHE Claude

Do not set timelimit to 0 when steps are there,

since it is not interpreted as infinite by CVC4
parent cec3a970
......@@ -184,6 +184,7 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
let actualcommand command timelimit memlimit stepslimit file =
let arglist = Cmdline.cmdline_split command in
let use_stdin = ref true in
(* FIXME: use_stdin is never modified below ?? *)
let on_timelimit = ref false in
let cmd_regexp = Str.regexp "%\\(.\\)" in
let replace s = match Str.matched_group 1 s with
......@@ -199,8 +200,9 @@ let actualcommand command timelimit memlimit stepslimit file =
| "l" -> Config.libdir
| "d" -> Config.datadir
| "S" -> string_of_int stepslimit
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, or %d"
| _ -> failwith "unknown specifier, use %%, %f, %t, %T, %U, %m, %l, %d or %S"
in
(* FIXME: are we sure that tuples are evaluated from left to right ? *)
List.map (Str.global_substitute cmd_regexp replace) arglist,
!use_stdin, !on_timelimit
......
......@@ -462,13 +462,13 @@ let run_external_proof_v3 eS eT a callback =
end else begin
let previous_result = a.proof_state in
let timelimit, memlimit = adapt_limits a in
let stepslimit, timelimit =
let stepslimit =
match a with
| { proof_state =
Done { Call_provers.pr_answer = Call_provers.Valid;
Call_provers.pr_steps = s };
proof_obsolete = false } when s >= 0 -> s, 0
| _ -> -1, timelimit
proof_obsolete = false } when s >= 0 -> s
| _ -> -1
in
let inplace = npc.prover_config.Whyconf.in_place in
let command = Whyconf.get_complete_command npc.prover_config in
......
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