anchor.diff:             r
            in
   
  -         let s_wp = lift_wp_and_bind_with env pure_assert_wp md u_res_t res_t wp in
  -         mk_comp md u_res_t res_t s_wp flags
  +         lift_wp_and_bind_with env pure_assert_wp c flags
   
   let strengthen_precondition
               (reason:option<(unit -> string)>)
  
positive.code: 
  
  (* private *)
  (*
   * Helper function used by weaken_comp and strengthen_comp
   * wp1 is a (pure_wp unit), md is an effect, wp2 is a (M.wp res_t)
   * The code basically does M.bind_wp (lift_PURE_M wp1) (fun _ -> wp2)
   *)
  let lift_wp_and_bind_with env (wp1:typ) (md:eff_decl) (u_res_t:universe) (res_t:typ) (wp2:term) : term =
    let r = Env.get_range env in
    (* lift wp1 to c.effect_name *)
    let edge =
      match Env.monad_leq env C.effect_PURE_lid md.mname with
      | Some edge -> edge
      | None -> failwith ("Impossible! lift_wp_and_bind_with: did not find a lift from PURE to " ^ md.mname.str)
    in
  
    
    let wp1 =
      let c = S.mk_Comp ({
        comp_univs = [S.U_zero];
        effect_name = C.effect_PURE_lid;
        result_typ = S.t_unit;
        effect_args = [wp1 |> S.as_arg];
        flags = []
      }) in
      c |> edge.mlift.mlift_wp env |> (fun (c, g) -> c |> U.comp_to_comp_typ |> (fun ct -> ct.effect_args |> List.hd |> fst)) in  //AR: TODO: FIXME handle g
  
    (* now bind it with fun _ -> wp *)
    mk_Tm_app
      (inst_effect_fun_with [S.U_zero; u_res_t] env md md.bind_wp)
      [ S.as_arg <| S.mk (S.Tm_constant (FStar.Const.Const_range r)) None r;
        S.as_arg <| S.t_unit;
        S.as_arg res_t;
        S.as_arg wp1;
        S.as_arg <| U.abs [null_binder S.t_unit] wp2 (Some (U.mk_residual_comp C.effect_Tot_lid None [TOTAL])) ]
      None
      wp2.pos
  
  
  let weaken_flags flags =
      if flags |> BU.for_some (function SHOULD_NOT_INLINE -> true | _ -> false)
  
negative.code:             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
                  let c1 = Env.unfold_effect_abbrev env c1 in
  