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 92de3c4c5489c8d00de94b1204d5ce53c0078fd8..2e69e08d73f54398f54fbf4e56c5fac294187426 100644 (file)
--- 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 " ^