anchor.diff:  let bind r1 env e1opt (lc1:lcomp) ((b, lc2):lcomp_with_binder) : lcomp =
     let lc1 = N.ghost_to_pure_lcomp env lc1 in //downgrade from ghost to pure, if possible
     let lc2 = N.ghost_to_pure_lcomp env lc2 in
  +  let joined_eff = join_lcomp env lc1 lc2 in
     if debug env Options.Extreme
     then
       (let bstr = match b with
  
positive.code:         | NonTrivial f ->
            let g = {g with guard_f=Trivial} in
            let strengthen () =
                //try to normalize one more time, since more unification variables may be resolved now
                let f = N.normalize [N.Beta; N.Eager_unfolding; N.Simplify] env f in
                match (SS.compress f).n with
                    | Tm_abs(_, {n=Tm_fvar fv}, _) when S.fv_eq_lid fv Const.true_lid ->
                      //it's trivial
                      let lc = {lc with res_typ=t} in
                      lc.comp()
  
                    | _ ->
                        let c = lc.comp() in
                        if Env.debug env <| Options.Extreme
                        then Util.print4 "Weakened from %s to %s\nStrengthening %s with guard %s\n"
                                (N.term_to_string env lc.res_typ)
                                (N.term_to_string env t)
                                (N.comp_to_string env c)
                                (N.term_to_string env f);
  
                        let ct = Normalize.unfold_effect_abbrev env c in
                        let a, kwp = Env.wp_signature env Const.effect_PURE_lid in
                        let k = SS.subst [NT(a, t)] kwp in
                        let md = Env.get_effect_decl env ct.effect_name in
                        let x = S.new_bv (Some t.pos) t in
                        let xexp = S.bv_to_name x in
                        let u_t, _, _ = destruct_comp ct in
                        let wp = mk_Tm_app (inst_effect_fun_with [u_t] env md md.ret_wp)
                                           [S.as_arg t; S.as_arg xexp]
                                           (Some k.n) xexp.pos
                        in
                        let cret = Util.lcomp_of_comp <| mk_comp md u_t t wp [RETURN] in
                        let guard = if apply_guard
                                    then mk_Tm_app f [S.as_arg xexp] (Some U.ktype0.n) f.pos
                                    else f
                        in
                        let eq_ret, _trivial_so_ok_to_discard =
                            strengthen_precondition (Some <| Errors.subtyping_failed env lc.res_typ t)
                                                    (Env.set_range env e.pos) e cret
                                                    (guard_of_guard_formula <| NonTrivial guard)
                        in
                        let x = {x with sort=lc.res_typ} in
                        let c = bind e.pos env (Some e) (Util.lcomp_of_comp <| mk_Comp ct) (Some x, eq_ret) in
                        let c = c.comp () in
                        if Env.debug env <| Options.Extreme
                        then Util.print1 "Strengthened to %s\n" (Normalize.comp_to_string env c);
                        c
            in
            let flags = lc.cflags |> List.collect (function
                                                   | RETURN | PARTIAL_RETURN -> [PARTIAL_RETURN]
  
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},
  