anchor.diff:                                     "Non-trivial pre-conditions very early in prims, even before we have defined the PURE monad")
                                      (Env.get_range env)
               else if U.is_total_comp c1
  -                 && U.is_total_comp c2
  -            then subst_c2 e1opt "both total"
  +            then (*
  +                  * Helper routine to close the compuation c with c1's return type
  +                  * 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
  +                   Inl (close_comp_if_refinement_t env x.sort x 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 ()
               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), "both gtot")
  -            else match e1opt, b with
  -                   | Some e, Some x ->
  -                     if U.is_total_comp c1
  -                     && not (Syntax.is_null_bv x)
  -                     then let c2 = SS.subst_comp [NT(x,e)] c2 in
  -                          let x = {x with sort = U.comp_result c1} in
  -                          Inl (maybe_close x.sort x c2, "c1 Tot")
  -                          //forall (_:t). c2[e/x]
  -                          //It's important to have that (forall (_:t)) since
  -                          //if x does not appear free in e,
  -                          //then it may still be important to know that t is inhabited
  -                     else aux ()
  -                   | _ -> aux ()
  +            then Inl (S.mk_GTotal (U.comp_result c2), "both GTot")
  +            else aux ()
             in
             match try_simplify () with
             | Inl (c, reason) ->
  
positive.code: let close_lcomp env bvs (lc:lcomp) =
      S.mk_lcomp lc.eff_name lc.res_typ lc.cflags
                 (fun () -> close_comp env bvs (lcomp_comp lc))
  
  let should_not_inline_lc (lc:lcomp) =
      lc.cflags |> BU.for_some (function SHOULD_NOT_INLINE -> true | _ -> false)
  
negative.code:           let strengthen_trivial () =
              let c = lcomp_comp lc in
              let res_t = Util.comp_result c in
  
              let set_result_typ (c:comp) :comp = Util.set_result_typ c t in
  
              if Util.eq_tm t res_t = Util.Equal then begin  //if the two types res_t and t are same, then just set the result type
                if Env.debug env <| Options.Extreme
                then BU.print2 "weaken_result_type::strengthen_trivial: res_t:%s is same as t:%s\n"
                               (Print.term_to_string res_t) (Print.term_to_string t);
                set_result_typ c
              end
              else
                let is_res_t_refinement =
                  let res_t = N.normalize_refinement N.whnf_steps env res_t in
                  match res_t.n with
                  | Tm_refine _ -> true
                  | _ -> false
                in
                //if t is a refinement, insert a return to capture the return type res_t
                //we are not inlining e, rather just adding (fun (x:res_t) -> p x) at the end
                if is_res_t_refinement then
                  let x = S.new_bv (Some res_t.pos) res_t in
                  let cret = return_value env (comp_univ_opt c) res_t (S.bv_to_name x) in
                  let lc = bind e.pos env (Some e) (U.lcomp_of_comp c) (Some x, Util.lcomp_of_comp cret) in
                  if Env.debug env <| Options.Extreme
                  then BU.print4 "weaken_result_type::strengthen_trivial: inserting a return for e: %s, c: %s, t: %s, and then post return lc: %s\n"
                                 (Print.term_to_string e) (Print.comp_to_string c) (Print.term_to_string t) (Print.lcomp_to_string lc);
                  set_result_typ (lcomp_comp lc)
                else begin
                  if Env.debug env <| Options.Extreme
                  then BU.print2 "weaken_result_type::strengthen_trivial: res_t:%s is not a refinement, leaving c:%s as is\n"
                                 (Print.term_to_string res_t) (Print.comp_to_string c);
                  set_result_typ c
                end
            in
            let lc = S.mk_lcomp lc.eff_name t lc.cflags strengthen_trivial in
            e, lc, g
  