yet another attempt at avoiding zombies

src/core/CVC4.ml

@@ -582,12 +582,11 @@ module Make(FO_T : FO.S) = struct
 
   (* the command line to invoke CVC4 *)
   let mk_cvc4_cmd_ timeout options =
-    let timeout_hard = int_of_float (timeout +. 1.) in
     let timeout_ms = int_of_float (timeout *. 1000.) in
     Printf.sprintf
-      "ulimit -t %d; exec cvc4 --tlimit-per=%d --lang smt --finite-model-find \
+      "cvc4 --tlimit-per=%d --lang smt --finite-model-find \
        --uf-ss-fair-monotone --no-condense-function-values %s"
-      timeout_hard timeout_ms options
+      timeout_ms options
 
   let solve ?(options="") ?(timeout=30.) ?(print=false) problem =
     let symbols, problem' = preprocess_pb_ problem in

src/core/Utils.ml

@@ -247,3 +247,4 @@ let not_implementedf fmt = exn_ksprintf fmt ~f:not_implemented
 let ignore_catch f x =
   try ignore (f x)
   with _ -> ()
+

src/main/nunchaku.ml

@@ -275,6 +275,7 @@ let main_model ~output statements =
 (* main *)
 let main () =
   CCFormat.set_color_default true; (* default: enable colors *)
+  let _ = Unix.alarm (!timeout_ + 2) in (* die after a while *)
   Arg.parse options set_file "usage: nunchaku [options] file";
   print_version_if_needed ();
   (* parse *)