 in
    match uu____1349 with
    | FStar_Pervasives_Native.None -> new_log_file ()
    | FStar_Pervasives_Native.Some fh -> fh in
  let append_to_log str =
    let uu____1420 = get_log_file () in
    match uu____1420 with | (f, nm) -> (FStar_Util.append_to_file f str; nm) in
  let write_to_new_log str =
    let file_name = next_file_name () in
    FStar_Util.write_file file_name str; file_name in
  let write_to_log fresh str =
    if fresh then write_to_new_log str else append_to_log str in
  let close_log uu____1469 =
    let uu____1470 = FStar_ST.op_Bang log_file_opt in
    match uu____1470 with
    | FStar_Pervasives_Native.None -> ()
    | FStar_Pervasives_Native.Some (fh, uu____1517) ->
        (FStar_Util.close_file fh;
         FStar_ST.op_Colon_Equals log_file_opt FStar_Pervasives_Native.None) in
  let log_file_name uu____1570 =
    let uu____1571 = FStar_ST.op_Bang current_file_name in
    match uu____1571 with
    | FStar_Pervasives_Native.None -> failwith "no log file"
    | FStar_Pervasives_Native.Some n -> n in
  { get_module_name; set_module_name; write_to_log; close_log }
let (z3_cmd_and_args : unit -> (Prims.string * Prims.string Prims.list)) =
  fun uu____1620 ->
    let cmd = FStar_Options.z3_exe () in
    let cmd_args =
      let uu____1627 =
        let uu____1631 =
          let uu____1635 =
            let uu____1639 =
              let uu____1641 =
                let uu____1643 = FStar_Options.z3_seed () in
                FStar_Util.string_of_int uu____1643 in
              FStar_Util.format1 "smt.random_seed=%s" uu____1641 in
            [uu____1639] in
          "-in" :: uu____1635 in
        "-smt2" :: uu____1631 in
      let uu____1652 = FStar_Options.z3_cliopt () in
      FStar_List.append uu____1627 uu____1652 in
    (cmd, cmd_args)
let (new_z3proc :
  Prims.string -> (Prims.string * Prims.string Prims.list) -> FStar_Util.proc)
  =
  fun id ->
    fun cmd_and_args ->
      check_z3version ();
      FStar_Util.start_process id (FStar_Pervasives_Native.fst cmd_and_args)
        (FStar_Pervasives_Native.snd cmd_and_args) (fun s -> s = "Done!")
let (new_z3proc_with_id :
  (Prims.string * Prims.string Prims.list) -> FStar_Util.proc) =
  let ctr = FStar_Util.mk_ref (~- Prims.int_one) in
  fun cmd_and_args ->
    let uu____1732 =
      let uu____1734 =
        FStar_Util.incr ctr;
        (let uu____1737 = FStar_ST.op_Bang ctr in
         FStar_All.pipe_right uu____1737 FStar_Util.string_of_int) in
      FStar_Util.format1 "bg-%s" uu____1734 in
    new_z3proc uu____1732 cmd_and_args
type bgproc =
  {
  ask: Prims.string -> Prims.string ;
  refresh: unit -> unit ;
  restart: unit -> unit }
let (__proj__Mkbgproc__item__ask : bgproc -> Prims.string -> Prims.string) =
  fun projectee -> match projectee with | { ask; refresh; restart;_} -> ask
let (__proj__Mkbgproc__item__refresh : bgproc -> unit -> unit) =
  fun projectee ->
    match projectee with | { ask; refresh; restart;_} -> refresh
let (__proj__Mkbgproc__item__restart : bgproc -> unit -> unit) =
  fun projectee ->
    match projectee with | { ask; refresh; restart;_} -> restart
let (cmd_and_args_to_string :
  (Prims.string * Prims.string Prims.list) -> Prims.string) =
  fun cmd_and_args ->
    FStar_String.concat ""
      ["cmd=";
      FStar_Pervasives_Native.fst cmd_and_args;
      " args=[";
      FStar_String.concat ", " (FStar_Pervasives_Native.snd cmd_and_args);
      "]"]
let (bg_z3_proc : bgproc FStar_ST.ref) =
  let the_z3proc = FStar_Util.mk_ref FStar_Pervasives_Native.None in
  let the_z3proc_params =
    FStar_Util.mk_ref (FStar_Pervasives_Native.Some ("", [""])) in
  let the_z3proc_ask_count = FStar_Util.mk_ref Prims.int_zero in
  let make_new_z3_proc cmd_and_args =
    (let uu____2000 =
       let uu____2003 = new_z3proc_with_id cmd_and_args in
       FStar_Pervasives_Native.Some uu____2003 in
     FStar_ST.op_Colon_Equals the_z3proc uu____2000);
    FStar_ST.op_Colon_Equals the_z3proc_params
      (FStar_Pervasives_Native.Some cmd_and_args);
    FStar_ST.op_Colon_Equals the_z3proc_ask_count Prims.int_zero in
  let z3proc uu____2102 =
    (let uu____2104 =
       let uu____2106 = FStar_ST.op_Bang the_z3proc in
       uu____2106 = FStar_Pervasives_Native.None in
     if uu____2104
     then let uu____2135 = z3_cmd_and_args () in make_new_z3_proc uu____2135
     else ());
    (let uu____2146 = FStar_ST.op_Bang the_z3proc in
     FStar_Util.must uu____2146) in
  let ask input =
    FStar_Util.incr the_z3proc_ask_count;
    (let kill_handler uu____2188 = "\nkilled\n" in
     let uu____2190 = z3proc () in
     FStar_Util.ask_process uu____2190 input kill_handler) in
  let refresh uu____2196 =
    let next_params = z3_cmd_and_args () in
    let old_params =
      let uu____2215 = FStar_ST.op_Bang the_z3proc_params in
      FStar_Util.must uu____2215 in
    (let uu____2274 =
       ((FStar_Options.log_queries ()) ||
          (let uu____2277 = FStar_ST.op_Bang the_z3proc_ask_count in
           uu____2277 > Prims.int_zero))
         || (Prims.op_Negation (old_params = next_params)) in
     if uu____2274
     then
       ((let uu____2311 =
           (FStar_Options.query_stats ()) &&
             (let uu____2314 =
                let uu____2316 = FStar_ST.op_Bang the_z3proc in
                uu____2316 = FStar_Pervasives_Native.