anchor.diff:              let bind_c, g_bind = TcComm.lcomp_comp (bind e.pos env None (TcComm.lcomp_of_comp c) (Some x, eq_ret)) in
               U.comp_set_flags bind_c flags, Env.conj_guards [g_c; g_ret; g_bind]
     in
  -  if not should_return then lc
  +
  +  if should_not_inline_lc lc
  +  then raise_error (Errors.Fatal_UnexpectedTerm,
  +         BU.format1 "assume_result_eq_pure_term cannot inline an non-inlineable lc : %s"
  +           (Print.term_to_string e)) e.pos
     else let c, g = refine () in
          TcComm.lcomp_of_comp_guard c g
  +
  +let maybe_assume_result_eq_pure_term_in_m env (m_opt:option<lident>) (e:term) (lc:lcomp) : lcomp =
  +  let should_return =
  +      not (env.lax)
  +   && Env.lid_exists env C.effect_GTot_lid //we're not too early in prims
  +   && should_return env (Some e) lc
  +   && not (TcComm.is_lcomp_partial_return lc)
  +  in
  +  if not should_return then lc
  +  else assume_result_eq_pure_term_in_m env m_opt e lc
   
   let maybe_assume_result_eq_pure_term env e lc =
     maybe_assume_result_eq_pure_term_in_m env None e lc
  
positive.code:     if m_opt |> is_none || Options.ml_ish () || is_ghost_effect env lc.eff_name
      then C.effect_PURE_lid
      else m_opt |> must in
    let flags =
      if should_return
      then if TcComm.is_total_lcomp lc
           then RETURN::lc.cflags
           else PARTIAL_RETURN::lc.cflags
      else lc.cflags
    in
    let refine () : comp * guard_t =
        let c, g_c = TcComm.lcomp_comp lc in
        let u_t =
  
negative.code:  *
   * This forces the lcomp thunk and recreates it to keep the callers same
   *)
  let assume_result_eq_pure_term_in_m env (m_opt:option<lident>) (e:term) (lc:lcomp) : lcomp =
    (*
     * AR: m is the effect that we are going to do return in
     *)
  