anchor.diff:                        let c2 = SS.subst_comp [NT(x,e1)] c2 in
                         let x_eq_e = U.mk_eq2 u_res_t1 res_t1 e1 (bv_to_name x) in
                         let c2, g_w = weaken_comp (Env.push_binders env [S.mk_binder x]) c2 x_eq_e in
  -                      let c, g_bind = mk_bind c1 b c2 in
  +                      let g = Env.conj_guard g_c1
  +                        (Env.close_guard env [S.mk_binder x] (TcComm.weaken_guard_formula g_c2 x_eq_e)) in
  +                      let c, g_bind = mk_bind c1 b c2 g in
                         c, Env.conj_guard g_w g_bind
                   //Caution: here we keep the flags for c2 as is, these flags will be overwritten later when we do md.bind below
                   //If we decide to return c2 as is (after inlining), we should reset these flags else bad things will happen
  -            else mk_bind c1 b c2
  +            else mk_bind c1 b c2 trivial_guard
         end
     in TcComm.mk_lcomp joined_eff
                        lc2.res_typ
  
positive.code:                   * When c1's return type is of the form _:t{phi}, is is useful to know
                    *   that t{phi} is inhabited, even if c1 is inlined etc.
                    *)
                   let close (x:bv) (reason:string) (c:comp) =
                     let x = { x with sort = U.comp_result c1 } in
                     let c, g_c = maybe_capture_unit_refinement env x.sort x c in
                     Inl (c, g_c, reason) in
                   match e1opt, b with
                   | Some e, Some x ->
                     c2 |> SS.subst_comp [NT (x, e)] |> close x "c1 Tot"
                   | _, Some x -> c2 |> close x "c1 Tot only close"
                   | _, _ -> aux_with_trivial_guard ()
              else if U.is_tot_or_gtot_comp c1
                   && U.is_tot_or_gtot_comp c2
              then Inl (S.mk_GTotal (U.comp_result c2), Env.trivial_guard, "both GTot")
              else aux_with_trivial_guard ()
            in
            match try_simplify () with
            | Inl (c, g_c, reason) ->
              debug (fun () ->
                  BU.print2 "(2) bind: Simplified (because %s) to\n\t%s\n"
                              reason
                              (Print.comp_to_string c));
              c, Env.conj_guard g_c (Env.conj_guard g_c1 g_c2)
            | Inr reason ->
              debug (fun () ->
                  BU.print1 "(2) bind: Not simplified because %s\n" reason);
              
              let mk_bind c1 b c2 =  (* AR: end code for inlining pure and ghost terms *)
                let c, g_bind = mk_bind env c1 b c2 bind_flags r1 in
                c, Env.conj_guard (Env.conj_guard g_c1 g_c2) g_bind in
  
              let mk_seq c1 b c2 =
                  //c1 is PURE or GHOST
  
negative.code:                       let _ = debug (fun () ->
                          BU.print2 "(3) bind (case a): Substituting %s for %s" (N.term_to_string env e1) (Print.bv_to_string x)) in
                        let c2 = SS.subst_comp [NT(x,e1)] c2 in
                        let g = Env.conj_guard g_c1 (Env.map_guard g_c2 (SS.subst [NT (x, e1)])) in
                        mk_bind c1 b c2 g
                   else if Options.vcgen_optimize_bind_as_seq()
                        && lcomp_has_trivial_postcondition lc1
                        && Option.isSome (Env.try_lookup_lid env C.with_type_lid) //and we're not very early in prims
  