anchor.diff:      | TIMEOUT -> "timeout"
   
   let tid () = Util.current_tid() |> Util.string_of_int
  -let new_z3proc id =
  -   let cond pid (s:string) =
  -    (let x = Util.trim_string s = "Done!" in
  +let new_z3proc id timeout =
  +    let cond pid (s:string) =
  +        (let x = Util.trim_string s = "Done!" in
   //     Util.print5 "On thread %s, Z3 %s (%s) says: %s\n\t%s\n" (tid()) id pid s (if x then "finished" else "waiting for more output");
  -     x) in
  -   Util.start_process id (!Options.z3_exe) (ini_params()) cond
  +         x) in
  +    let args = ini_params timeout in
  +    (* we log the following information with `--print_fuels` because lack of a timeout is only associated with fuel tracing *)
  +    if !Options.print_fuels then
  +        match timeout with
  +        | Some n ->
  +            Util.print2 "Starting z3 process `%s` with a timeout of %s.\n" id <| string_of_int n
  +        | None ->
  +            Util.print1 "Starting z3 process `%s` without a timeout.\n" id
  +    else
  +        ();
  +    Util.start_process id (!Options.z3_exe) args cond
   
   type bgproc = {
       grab:unit -> proc;
  
positive.code: let doZ3Exe =
      let ctr = Util.mk_ref 0 in
      fun (fresh:bool) (input:string) ->
          let z3proc = if fresh then (incr ctr; new_z3proc (Util.string_of_int !ctr)) else bg_z3_proc.grab() in
          let res = doZ3Exe' input z3proc in
          //Printf.printf "z3-%A says %s\n"  (get_z3version()) (status_to_string (fst res));
          if fresh then Util.kill_process z3proc else bg_z3_proc.release();
  
negative.code: let ctr = Util.mk_ref (-1)
  
  let new_proc () =
    let timeout = 
      if is_replaying_fuel_trace () then
        None
      else
        Some !Options.z3timeout
    in
    new_z3proc (Util.format1 "bg-%s" (incr ctr; !ctr |> string_of_int)) timeout
  
  let z3proc () =
    if !the_z3proc = None then
  