anchor.diff:      | UNKNOWN (errs, msg)
       | TIMEOUT (errs, msg) -> BU.format2 "%s%s" (status_tag s) (match msg with None -> "" | Some msg -> " because " ^ msg), errs
   
  -let tid () = BU.current_tid() |> BU.string_of_int
  -let new_z3proc id =
  -    BU.start_process id (Options.z3_exe ()) (ini_params ()) (fun s -> s = "Done!")
  -let new_z3proc_with_id =
  -    let ctr = BU.mk_ref (-1) in
  -    fun () -> new_z3proc (BU.format1 "bg-%s" (incr ctr; !ctr |> string_of_int))
  -
  -type bgproc = {
  -    ask: string -> string;
  -    refresh:unit -> unit;
  -    restart:unit -> unit
  -}
   
   type query_log = {
       get_module_name: unit -> string;
  
positive.code:   in
    let stdout =
      if fresh then
        let proc = new_z3proc_with_id () in
        let kill_handler () = "\nkilled\n" in
        let out = BU.ask_process proc input kill_handler in
        BU.kill_process proc;
  
negative.code:           FStar.Errors.log_issue Range.dummyRange (e, msg)
      end
  
  type label = string
  type unsat_core = option<list<string>>
  type z3status =
  