anchor.diff:  
       // Nothing special, just check the depth
       | _ ->
  -        log_unfolding cfg (fun () -> BU.print3 ">>> Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n"
  +        log_unfolding cfg (fun () -> BU.print3 " >> Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n"
                                                  (Print.fv_to_string fv)
                                                  (Print.delta_depth_to_string fv.fv_delta)
                                                  (FStar.Common.string_of_list Env.string_of_delta_level cfg.delta_level));
  
positive.code:         // Unfolding fully, use new cfg with more steps and keep old one in stack
          let cfg' =
              { cfg with steps = { cfg.steps with
                         iota         = false
                       ; zeta         = false
                       ; weak         = false
                       ; hnf          = false
                       ; primops      = false
                       ; simplify     = false
                       ; unfold_only  = None
                       ; unfold_fully = None
                       ; unfold_until = Some delta_constant } } in
          let stack' = (Cfg cfg) :: stack in
          Some (cfg', stack')
  
negative.code:              | Eager_unfolding_only -> true
               | Unfold l -> Common.delta_depth_greater_than fv.fv_delta l))
      in
      log_unfolding cfg (fun () -> BU.print3 " >> For %s (%s), unfolding res = %s\n"
                      (Print.fv_to_string fv)
                      (Range.string_of_range rng)
                      (string_of_res res));
  