anchor.diff:      | _, Some _, _, _
       | _, _, Some _, _
       | _, _, _, Some _ ->
  -        log_unfolding cfg (fun () -> BU.print1 ">>> Reached a %s with selective unfolding\n"
  +        log_unfolding cfg (fun () -> BU.print1 " >> Reached a %s with selective unfolding\n"
                                                  (Print.fv_to_string fv));
           // How does the following code work?
           // We are doing selective unfolding so, by default, we assume everything
  
positive.code:             else let us = UnivArgs(List.map (norm_universe cfg env) us, t.pos) in
                   let stack = us::stack in
                   norm cfg env stack t'
  
            | Tm_fvar fv ->
              let qninfo = Env.lookup_qname cfg.tcenv (S.lid_of_fv fv) in
              begin match decide_unfolding cfg env stack t.pos fv qninfo with
              | Some (cfg, stack) -> do_unfold_fv cfg env stack t qninfo fv
              | None -> rebuild cfg env stack t
              end
  
            | Tm_bvar x ->
              begin match lookup_bvar env x with
  
negative.code: 
      // 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"
                                                 (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));
  