Commit fa40a1be authored by MARCHE Claude's avatar MARCHE Claude

as for failure, an unknown answer just before the time limit should be considered as a timeout

this allows to provide the time limit on the command of CVC4, and perhaps Z3 later.
parent 519e823c
......@@ -154,7 +154,7 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time,steps = Opt.get_def (time,-1) (grep_time out res_parser.prp_timeregexps) in
let ans = match ans with
| HighFailure when on_timelimit && timelimit > 0
| Unknown _ | HighFailure when on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
| _ -> ans
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