anchor.diff:  (* 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 _z3hash_checked : ref<bool> = BU.mk_ref false
  -
  -let _z3hash_expected = "1f29cebd4df6"
  +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
  -    | x :: _ ->
  -        begin
  -            let trimmed = trim_string x in
  -            let parts = split trimmed " " in
  -            let rec aux = function
  -            | [hash] ->
  -              let n = min (String.strlen _z3hash_expected) (String.strlen hash) in
  -              let hash_prefix = String.substring hash 0 n in
  -              if hash_prefix = _z3hash_expected
  -              then begin
  -                  if Options.debug_any ()
  -                  then
  -                      let msg =
  -                          BU.format1
  -                              "Successfully found expected Z3 commit hash %s\n"
  -                              hash
  -                      in
  -                      print_string msg
  -                  else ();
  -                  None
  -              end else
  -                  let msg =
  -                      BU.format2
  -                          "Expected Z3 commit hash \"%s\", got \"%s\""
  -                          _z3hash_expected
  -                          trimmed
  -                  in
  -                  Some msg
  -            | _ :: q -> aux q
  -            | _ -> Some "No Z3 commit hash found"
  -            in
  -            aux parts
  +    | 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 z3hash_warning_message () =
  +let z3version_warning_message () =
       let run_proc_result =
           try
               Some (BU.run_process "z3_version" (Options.z3_exe()) ["-version"] None)
  
positive.code:     end
  
  let ini_params () =
    check_z3hash ();
    List.append ["-smt2";
                 "-in";
                 Util.format1 "smt.random_seed=%s" (string_of_int (Options.z3_seed ()))]
  
negative.code:         | Some msg -> Some (FStar.Errors.Warning_Z3InvocationWarning, msg)
          end
  
  let check_z3version () =
      if not !_z3version_checked
      then begin
          _z3version_checked := true;
          match z3version_warning_message () with
          | None -> ()
          | Some (e, msg) ->
            let msg =
  