anchor.diff:      let x : list<unit> = [] in
       let grab () = BU.monitor_enter x; z3proc () in
       let release () = BU.monitor_exit(x) in
  +    let ask input =
  +        let proc = grab() in
  +        let stdout = BU.ask_process proc input in
  +        release (); stdout in
       let refresh () =
           let proc = grab() in
           BU.kill_process proc;
  
positive.code:         the_z3proc := None;
          the_z3proc := Some (new_proc ());
          BU.monitor_exit() in
      {grab=grab;
       release=release;
       refresh=refresh;
       restart=restart}
  
  let at_log_file () =
    if Options.log_queries()
  
negative.code: //refresh: create a new z3 process, and reset the bg_scope
  let refresh () =
      if (Options.n_cores() < 2) then
          (!bg_z3_proc).refresh();
          bg_scope := List.flatten (List.rev !fresh_scope)
  
  let mk_input theory =
  