anchor.diff:        : (S.binders    //arguments of the lambda abstraction
         * S.term        //body of the lambda abstraction
         * S.binders     //arguments of the function type, length of this component is equal to the first
  -      * S.typ)        //result type
  +      * S.comp)       //result comp
         * bool          //if set, we should generate a curried application of f
       =
         (* The input type [t_norm] might contain reifiable computation type which must be reified at this point *)
  -      let get_result_type c =
  +      let get_result_comp c =
             if is_reifiable_comp env.tcenv c
  -          then reify_comp ({env.tcenv with lax = true}) c U_unknown
  -          else U.comp_result c
  +          then S.mk_Total <| reify_comp ({env.tcenv with lax = true}) c U_unknown
  +          else c
         in
   
         let rec aux norm t_norm =
  
positive.code:               let formals, c = SS.open_comp formals c in
                let nformals = List.length formals in
                let nbinders = List.length binders in
                let tres = get_result_type c in
                if nformals < nbinders && U.is_total_comp c (* explicit currying *)
                then let bs0, rest = BU.first_N nformals binders in
                        let c =
                            let subst = List.map2 (fun (x, _) (b, _) -> NT(x, S.bv_to_name b)) formals bs0 in
                            SS.subst_comp subst c in
                        let body = U.abs rest body lopt in
                        (bs0, body, bs0, get_result_type c), false
                else if nformals > nbinders (* eta-expand before translating it *)
                then let binders, body = eta_expand binders formals body tres in
                        (binders, body, formals, tres), false
                else (binders, body, formals, tres), false
  
              | Tm_refine(x, _) ->
                  fst (aux norm x.sort), true
  
negative.code:                 in
  
                  (* Open binders *)
                  let (binders, body, _, t_body_comp), curry = destruct_bound_function flid t_norm e in
                  let t_body = U.comp_result t_body_comp in
                  if Env.debug env.tcenv <| Options.Other "SMTEncoding"
                  then BU.print2 "Encoding let : binders=[%s], body=%s\n"
                                  (Print.binders_to_string ", " binders)
  