anchor.diff:           | RETURN -> [PARTIAL_RETURN; TRIVIAL_POSTCONDITION]
            | f -> [f])
   
  -let weaken_comp env (c:comp) (formula:term) : comp =
  -    if U.is_ml_comp c
  -    then c
  -    else let c = Env.unfold_effect_abbrev env c in
  -         let u_res_t, res_t, wp = destruct_comp c in
  -         let md = Env.get_effect_decl env c.effect_name in
  -         let r = Env.get_range env in
  -
  -         (*
  -          * The following code does:
  -          *   M.bind_wp (lift_pure_M (Prims.pure_assume_wp f)) (fun _ -> wp)
  -          *)
  -
  -         (*
  -          * lookup the pure_assume_wp from prims
  -          * its type is p:Type -> pure_wp unit
  -          *  and it is not universe polymorphic
  -          *)
  -         let pure_assume_wp = S.fv_to_tm (S.lid_as_fv C.pure_assume_wp_lid (Delta_constant_at_level 1) None) in
  -
  -         (* apply it to f, after decorating f with the reason *)
  -         let pure_assume_wp = mk_Tm_app
  -           pure_assume_wp
  -           [ S.as_arg <| formula ]
  -           None
  -           r
  -         in
  +let weaken_comp env (c:comp) (formula:term) : comp * guard_t =
  +  if U.is_ml_comp c
  +  then c, Env.trivial_guard
  +  else let ct = Env.unfold_effect_abbrev env c in
  +
  +       (*
  +        * The following code does:
  +        *   M.bind_wp (lift_pure_M (Prims.pure_assume_wp f)) (fun _ -> wp)
  +        *)
  +
  +       (*
  +        * lookup the pure_assume_wp from prims
  +        * its type is p:Type -> pure_wp unit
  +        *  and it is not universe polymorphic
  +        *)
  +       let pure_assume_wp = S.fv_to_tm (S.lid_as_fv C.pure_assume_wp_lid (Delta_constant_at_level 1) None) in
  +
  +       (* apply it to f, after decorating f with the reason *)
  +       let pure_assume_wp = mk_Tm_app
  +         pure_assume_wp
  +         [ S.as_arg <| formula ]
  +         None
  +         (Env.get_range env)
  +       in
            
  -         let w_wp = lift_wp_and_bind_with env pure_assume_wp md u_res_t res_t wp in
  -         mk_comp md u_res_t res_t w_wp (weaken_flags c.flags)
  +       lift_wp_and_bind_with env pure_assume_wp c (weaken_flags ct.flags)
   
   let weaken_precondition env lc (f:guard_formula) : lcomp =
     let weaken () =
         let c, g_c = TcComm.lcomp_comp lc in
  -      (if env.lax
  -       && Options.ml_ish() //NS: Disabling this optimization temporarily
  -       then c
  -       else match f with
  -            | Trivial -> c
  -            | NonTrivial f ->
  -              weaken_comp env c f), g_c
  +      if env.lax
  +      && Options.ml_ish() //NS: Disabling this optimization temporarily
  +      then c, g_c
  +      else match f with
  +           | Trivial -> c, g_c
  +           | NonTrivial f ->
  +             let c, g_w = weaken_comp env c f in
  +             c, Env.conj_guard g_c g_w
     in
     TcComm.mk_lcomp lc.eff_name lc.res_typ (weaken_flags lc.cflags) weaken
   
   
  -let strengthen_comp env (reason:option<(unit -> string)>) (c:comp) (f:formula) flags =
  +let strengthen_comp env (reason:option<(unit -> string)>) (c:comp) (f:formula) flags : comp * guard_t =
       if env.lax
  -    then c
  -    else let c = Env.unfold_effect_abbrev env c in
  -         let r = Env.get_range env in
  -         let u_res_t, res_t, wp = destruct_comp c in
  -         let md = Env.get_effect_decl env c.effect_name in
  -
  +    then c, Env.trivial_guard
  +    else let r = Env.get_range env in
            (*
             * The following code does:
             *   M.bind_wp (lift_pure_M (Prims.pure_assert_wp f)) (fun _ -> wp)
  
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:            r
           in
  
           lift_wp_and_bind_with env pure_assert_wp c flags
  
  let strengthen_precondition
              (reason:option<(unit -> string)>)
  