anchor.diff:                      expected: %s, found: %s\n"
                       checked_fn fn current_dig dig;
                     let msg = BU.format2 "checked file %s is stale (digest mismatch for %s)" checked_fn fn in
  -                  BU.smap_add mcache checked_fn (Invalid msg, Inl msg)
  +                  add_and_return (Invalid msg, Inl msg)
                   end
  -                else BU.smap_add mcache checked_fn (Unknown (deps_dig, tc_result), Inr parsing_data)
  +                else add_and_return (Unknown (deps_dig, tc_result), Inr parsing_data)
   
   (*
    * Second step for loading checked files, validates the tc data
    *)
  -let load_checked_file_with_tc_result (deps:Dep.deps) (fn:string) (checked_fn:string) :unit =
  -  load_checked_file fn checked_fn;  //first step, in case some client calls it directly
  -  match BU.smap_try_find mcache checked_fn with
  -  | None -> failwith "Impossible, load_checked_file must add an entry to mcache"
  -  | Some (Invalid _, _)
  -  | Some (Valid _, _) -> ()  //already marked Valid or Invalid
  -  | Some (Unknown (deps_dig, tc_result), parsing_data) ->
  +let load_checked_file_with_tc_result (deps:Dep.deps) (fn:string) (checked_fn:string) :cache_t =
  +  let elt = load_checked_file fn checked_fn in
  +  match elt with  //first step, in case some client calls it directly
  +  | Invalid _, _
  +  | Valid _, _ -> elt  //already marked Valid or Invalid
  +  | Unknown (deps_dig, tc_result), parsing_data ->
       match hash_dependences deps fn with
       | Inl msg ->
  -      BU.smap_add mcache checked_fn (Invalid msg, parsing_data)
  +      let elt = (Invalid msg, parsing_data) in
  +      BU.smap_add mcache checked_fn elt;
  +      elt
       | Inr deps_dig' ->
         if deps_dig = deps_dig'
         then begin
           //mark the tc data of the file as valid
  -        BU.smap_add mcache
  -          checked_fn
  -          (Valid (BU.digest_of_file checked_fn, tc_result), parsing_data);
  -        //if there exists an interface for it, mark that too as valid
  -        //validity of implementaton tc data implies validity of iface tc data
  +        let elt = (Valid (BU.digest_of_file checked_fn, tc_result), parsing_data) in 
  +        BU.smap_add mcache checked_fn elt;
  +        (*
  +         * if there exists an interface for it, mark that too as valid
  +         * this is specially needed for extraction invocations of F* with --cmi flag
  +         * for example, consider a scenario:
  +         * A.fst -> B.fsti -> prims.fst
  +         *            ^      ^
  +         *            |     /
  +         *             B.fst
  +         *
  +         * when all the checked files are present and F* is invoked with --extract A --cmi
  +         * during parsing, all checked files are loaded with tc data statemachine as Unknown
  +         * since it is cmi (and say B has an inline_for_extraction symbol), the client
  +         * then loads B.fst.checked BUT NOT B.fsti.checked
  +         * this advances the state machine for B.fst, but not for B.fsti
  +         * so when client loads A.fst.checked, B.fsti -- a dependence of A -- is still in Unknown
  +         * following code relies on the invariant that:
  +         * validity of implementaton tc data implies validity of iface tc data
  +         *
  +         * an alternative is to not do this, but in hash_dependences, if some dependence
  +         * is in Unknown state, it could call load_checked_file_with_tc_result
  +         *)
           let validate_iface_cache () =
             let iface = fn |> Dep.lowercase_module_name |> Dep.interface_of deps in
             match iface with
  
positive.code:             with
                | _ -> ()
          in
          validate_iface_cache ()
        end
        else begin
          if Options.debug_any()
  
negative.code:             "checked file %s is stale (dependence hash mismatch, use --debug yes for more details)"
              checked_fn
          in
          let elt = (Invalid msg, Inl msg) in
          BU.smap_add mcache checked_fn elt;
          elt
        end
  
  
  