anchor.diff:  
   exception Let_rec_unencodeable
   
  +let copy_env (en:env_t) = { en with cache = BU.smap_copy en.cache }  //Make a copy of all the mutable state of env_t, central place for keeping track of mutable fields in env_t
  +
   let encode_top_level_let :
       env_t -> (bool * list<letbinding>) -> list<qualifier> -> list<decl> * env_t =
       fun env (is_rec, bindings) quals ->
  
positive.code:         if quals |> BU.for_some (function HasMaskedEffect -> true | _ -> false)
          || typs  |> BU.for_some (fun t -> not <| (U.is_pure_or_ghost_function t ||
                                                    is_reifiable_function env.tcenv t))
          then decls, env
          else
            try
              if not is_rec
  
negative.code:               encode_non_rec_lbdef bindings typs toks_fvbs env
              else
                encode_rec_lbdefs bindings typs toks_fvbs env
            with Inner_let_rec -> decls, env_decls  //decls are type declarations for the lets, if there is an inner let rec, only those are encoded to the solver
  
      with Let_rec_unencodeable ->
        let msg = bindings |> List.map (fun lb -> Print.lbname_to_string lb.lbname) |> String.concat " and " in
  