Z3 overrides signal handlers

[filipeom]

When solving, signals raised in ocaml are typically ignored.

Code that creates signals:

let run_with_timeout limit f =
  let set_timer limit =
    ignore
    @@ Unix.setitimer Unix.ITIMER_REAL
         Unix.{ it_value = limit; it_interval = 0.01 }
  in
  let unset () =
    ignore
    @@ Unix.setitimer Unix.ITIMER_REAL Unix.{ it_value = 0.; it_interval = 0. }
  in
  set_timer limit;
  Sys.set_signal Sys.sigalrm (Sys.Signal_handle (fun _ -> raise Out_of_time));
  let f () = try `Ok (f ()) with Out_of_time -> `Timeout in
  Fun.protect f ~finally:unset

[zapashcanon]

Is this introduced by the Z3 ocaml bindings or by Z3 itself?

[filipeom]

It seems to be by Z3 itself. I had similar issues with the Z3 binary as well