anchor.diff:                     let stack =
                        stack |>
                        List.fold_right (fun (a, aq) stack ->
  -                       Arg (Clos(env, a, BU.mk_ref (Some ([], a)), false),aq,t.pos)::stack)
  +                       Arg (Clos(env, a, BU.mk_ref (Some (cfg, ([], a))), false),aq,t.pos)::stack)
                        norm_args
                      in
                      log cfg  (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args));
  
positive.code: 
  let head_of t = let hd, _ = U.head_and_args' t in hd
  
  let set_memo cfg (r:memo<'a>) (t:'a) =
    if cfg.memoize_lazy then
      match !r with
      | Some _ -> failwith "Unexpected set_memo: thunk already evaluated"
      | None -> r := Some t
  
  let closure_to_string = function
      | Clos (env, t, _, _) -> BU.format2 "(env=%s elts; %s)" (List.length env |> string_of_int) (Print.term_to_string t)
  
negative.code: type stack_elt =
   | Arg      of closure * aqual * Range.range
   | UnivArgs of list<universe> * Range.range
   | MemoLazy of cfg_memo<(env * term)>
   | Match    of env * branches * cfg * Range.range
   | Abs      of env * binders * env * option<residual_comp> * Range.range //the second env is the first one extended with the binders, for reducing the option<lcomp>
   | App      of env * term * aqual * Range.range
  