anchor.diff:      | _ -> false
   
   let return_value env t v =
  -//  if is_function t then failwith (Util.format1 "(%s): Returning a function!" (Range.string_of_range (Env.get_range env)));
     let c =
       if not <| Env.lid_exists env Const.effect_GTot_lid
       then mk_Total t //we're still in prims, not yet having fully defined the primitive effects
       else let m = must (Env.effect_decl_opt env Const.effect_PURE_lid) in //if Tot isn't fully defined in prims yet, then just return (Total t)
  -         let a, kwp = Env.wp_signature env Const.effect_PURE_lid in
  -         let k = SS.subst [NT(a, t)] kwp in
            let u_t = env.universe_of env t in
  -         let wp = N.normalize [N.Beta] env (mk_Tm_app (inst_effect_fun_with [u_t] env m m.ret_wp) [S.as_arg t; S.as_arg v] (Some k.n) v.pos) in
  +         let wp = 
  +            if env.lax 
  +            then S.tun
  +            else let a, kwp = Env.wp_signature env Const.effect_PURE_lid in
  +                 let k = SS.subst [NT(a, t)] kwp in
  +                 N.normalize [N.Beta] env (mk_Tm_app (inst_effect_fun_with [u_t] env m m.ret_wp) [S.as_arg t; S.as_arg v] (Some k.n) v.pos) in
            mk_comp m u_t t wp [RETURN] in
     if debug env <| Options.Other "Return"
     then Util.print3 "(%s) returning %s at comp type %s\n"
  
positive.code:     lc.comp()
  
  let ite env (guard:formula) lcomp_then lcomp_else =
    let comp () =
        let (md, _, _), (u_res_t, res_t, wp_then), (_, _, wp_else) = lift_and_destruct env (lcomp_then.comp()) (lcomp_else.comp()) in
        let ifthenelse md res_t g wp_t wp_e = mk_Tm_app (inst_effect_fun_with [u_res_t] env md md.if_then_else) [S.as_arg res_t; S.as_arg g; S.as_arg wp_t; S.as_arg wp_e] None (Range.union_ranges wp_t.pos wp_e.pos) in
        let wp = ifthenelse md res_t guard wp_then wp_else in
        if (Options.split_cases()) > 0
        then let comp = mk_comp md u_res_t res_t wp [] in
             add_equality_to_post_condition env comp res_t
        else let wp = mk_Tm_app  (inst_effect_fun_with [u_res_t] env md md.ite_wp)  [S.as_arg res_t; S.as_arg wp] None wp.pos in
             mk_comp md u_res_t res_t wp [] in
      {eff_name=join_effects env lcomp_then.eff_name lcomp_else.eff_name;
       res_typ=lcomp_then.res_typ;
       cflags=[];
       comp=comp}
  
  let fvar_const env lid =  S.fvar (Ident.set_lid_range lid (Env.get_range env)) Delta_constant None
  
  
negative.code:          let flags = lc.cflags |> List.collect (function RETURN | PARTIAL_RETURN -> [PARTIAL_RETURN] | _ -> []) in
           let strengthen () =
              let c = lc.comp () in
              if env.lax then c
              else begin
                  let g0 = Rel.simplify_guard env g0 in
                  match guard_form g0 with
                      | Trivial -> c
                      | NonTrivial f ->
                      let c =
                          if (Util.is_pure_or_ghost_comp c
                             && not (Util.is_partial_return c))
                          then let x = S.gen_bv "strengthen_pre_x" None (Util.comp_result c) in
                               let xret = Util.comp_set_flags (return_value env x.sort (S.bv_to_name x)) [PARTIAL_RETURN] in
                               let lc = bind e.pos env (Some e) (Util.lcomp_of_comp c) (Some x, Util.lcomp_of_comp xret) in
                               lc.comp()
                          else c in
  
                      if Env.debug env <| Options.Extreme
                      then Util.print2 "-------------Strengthening pre-condition of term %s with guard %s\n"
                                      (N.term_to_string env e)
                                      (N.term_to_string env f);
  
                      let c = Normalize.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 wp =  mk_Tm_app (inst_effect_fun_with [u_res_t] env md md.assert_p) [S.as_arg res_t; S.as_arg <| label_opt env reason (Env.get_range env) f; S.as_arg wp] None wp.pos in
  
                      if Env.debug env <| Options.Extreme
                      then Util.print1 "-------------Strengthened pre-condition is %s\n"
                                      (Print.term_to_string wp);
  
                      let c2 = mk_comp md u_res_t res_t wp flags in
                      c2
               end 
         in
         {lc with eff_name=norm_eff_name env lc.eff_name;
                  cflags=(if Util.is_pure_lcomp lc && not <| Util.is_function_typ lc.res_typ then flags else []);
                  comp=strengthen},
  