anchor.diff:      | NotForFree ->
           ed
       | ForFree ->
  -        let wp_if_then_else, wp_binop, wp_assert, wp_assume = gen_wps_for_free env binders a wp_a in {
  -          ed with
  +        let
  +          wp_if_then_else,
  +          wp_binop,
  +          wp_assert,
  +          wp_assume,
  +          wp_close
  +        = gen_wps_for_free env binders a wp_a in
  +        { ed with
             if_then_else = wp_if_then_else;
             wp_binop = wp_binop;
             assert_p = wp_assert;
  -          assume_p = wp_assume
  +          assume_p = wp_assume;
  +          close_wp = wp_close
           }
     in
   
  
positive.code:   let wp_assume =
      let q = S.gen_bv "q" None Util.ktype0 in
      let wp = S.gen_bv "wp" None wp_a in
      let l_imp = fvar Const.and_lid (S.Delta_unfoldable 1) None in
      let body =
        Util.mk_app c_app (List.map S.as_arg [
          unknown; unknown;
  
negative.code:     let ret = Some (Inl (Util.lcomp_of_comp (mk_Total (mk_gctx (S.bv_to_name t2))))) in
      let outer_body =
        let gamma = mk_gamma () in
        let gamma_as_args = args_of_bv gamma in
        let inner_body =
          Util.mk_app
            (S.bv_to_name l)
  