anchor.diff:        | ["sat"]     -> SAT     (labels, reason_unknown)
         | ["unknown"] -> UNKNOWN (labels, reason_unknown)
         | ["timeout"] -> TIMEOUT (labels, reason_unknown)
  -      | ["killed"]  -> bg_z3_proc.restart(); KILLED
  +      | ["killed"]  -> (!bg_z3_proc).restart(); KILLED
         | _ ->
           failwith (format1 "Unexpected output from Z3: got output result: %s\n"
                             (String.concat "\n" smt_output.smt_result))
  
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 =
  