From 748420d0b033ad10bf925c7538c71cc735187eb0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 26 Jun 2009 15:38:02 +0000 Subject: [PATCH] the timeout is passed to test last chance --- .../software/components/binaries/matitaprover/matitaprover.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 " ^ -- 2.39.2