From: Andrea Asperti Date: Fri, 26 Jun 2009 15:38:02 +0000 (+0000) Subject: the timeout is passed to test last chance X-Git-Tag: make_still_working~3781 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=748420d0b033ad10bf925c7538c71cc735187eb0;p=helm.git the timeout is passed to test last chance --- diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index 92de3c4c5..2e69e08d7 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -111,8 +111,8 @@ usage: matitaprover [options] problemfile"; List.iter (fun x -> prerr_endline (" " ^ Pp.pp_unit_clause x)) passives; prerr_endline "Goal"; prerr_endline (" " ^ Pp.pp_unit_clause g_passives); - let _ = Unix.alarm !seconds in - match P.paramod ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with + (* let _ = Unix.alarm !seconds in *) + match P.paramod ~timeout:(Unix.gettimeofday () +. float_of_int !seconds) ~max_steps:max_int bag ~g_passives:[g_passives] ~passives with | [] -> fail_msg () | (bag,_,l)::_ -> print_endline ("% SZS status Unsatisfiable for " ^