X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Fmatitaprover%2Fmatitaprover.ml;h=2e69e08d73f54398f54fbf4e56c5fac294187426;hb=748420d0b033ad10bf925c7538c71cc735187eb0;hp=499ecb2738343e127c1f12709a4a214955408d4f;hpb=4de22917afd18df543e3281bb463ed51f2cfab61;p=helm.git

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 499ecb273..2e69e08d7 100644
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -56,6 +56,12 @@ Matita interactive theorem prover (http://matita.cs.unibo.it).
 
 Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1
 
+If --tptppath is given, instead of the problem file you can just give the 
+problem name with the .p suffix (e.g. BOO001-1.p)
+
+If --tptppath is not given, included files (i.e. axiom sets) are searched 
+in the current directory only.
+
 usage: matitaprover [options] problemfile";
   let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
   let goal = match goals with [x] -> x | _ -> assert false in
@@ -105,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 " ^