anchor.diff:      end
   
   let ini_params () =
  -  check_z3hash ();
  +  check_z3version ();
     List.append ["-smt2";
                  "-in";
                  Util.format1 "smt.random_seed=%s" (string_of_int (Options.z3_seed ()))]
  
positive.code:         | Some msg -> Some (FStar.Errors.Warning_Z3InvocationWarning, msg)
          end
  
  let check_z3hash () =
      if not !_z3hash_checked
      then begin
          _z3hash_checked := true;
          match z3hash_warning_message () with
          | None -> ()
          | Some (e, msg) ->
            let msg =
  
negative.code: (* Check the Z3 commit hash once, and issue a warning if it is not
     equal to the one that we are expecting from the Z3 url below
  *)
  let _z3version_checked : ref<bool> = BU.mk_ref false
  
  let _z3version_expected = "Z3 version 4.8.5"
  
  let _z3url = "https://github.com/FStarLang/binaries/tree/master/z3-tested"
  
  let parse_z3_version_lines out =
      match splitlines out with
      | version :: _ ->
        if BU.starts_with version _z3version_expected
        then begin
            if Options.debug_any ()
            then
              print_string
                (BU.format1
                    "Successfully found expected Z3 version %s\n"
                    version);
            None
          end
        else
          let msg =
              BU.format2
                  "Expected Z3 version \"%s\", got \"%s\""
                  _z3version_expected
                  version
          in
          Some msg
      | _ -> Some "No Z3 version string found"
  
  let z3version_warning_message () =
      let run_proc_result =
          try
              Some (BU.run_process "z3_version" (Options.z3_exe()) ["-version"] None)
  