anchor.diff:                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 are type declarations for the lets, if there is an inner let rec, only those are encoded to the solver
  +          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
  
positive.code:         in
          let toks_fvbs = List.rev toks in
          let decls = List.rev decls |> List.flatten in
          let typs = List.rev typs in
  
          let mk_app rng curry fvb vars =
  
negative.code: 
  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 ->
  