anchor.diff:              //But, the pattern ensures that this only applies to well-typed terms
               //NS 08/10: Setting the weight of this quantifier to 0, since its instantiations are controlled by F* fuel
               //NS 11/28/2018: Restoring the mkImp (mk_and_l guards, mkEq(gsapp, body_tm))
  -            let eqn_g = Util.mkAssume(mkForall' (U.range_of_lbname lbn) ([[gsapp]], Some 0, fuel::vars, mkImp(mk_and_l guards, mkEq(gsapp, body_tm))),
  -                                    Some (BU.format1 "Equation for fuel-instrumented recursive function: %s" fvb.fvar_lid.str),
  -                                    ("equation_with_fuel_" ^g)) in
  +            //   11/29/2018: Also guarding by the precondition of a Pure/Ghost function in addition to typing guards
  +            let eqn_g =
  +                Util.mkAssume
  +                    (mkForall' (U.range_of_lbname lbn)
  +                               ([[gsapp]], Some 0, fuel::vars, mkImp(guard, mkEq(gsapp, body_tm))),
  +                     Some (BU.format1 "Equation for fuel-instrumented recursive function: %s" fvb.fvar_lid.str),
  +                     "equation_with_fuel_" ^g) in
               let eqn_f = Util.mkAssume(mkForall (U.range_of_lbname lbn) ([[app]], vars, mkEq(app, gmax)),
                                       Some "Correspondence of recursive function to instrumented version",
                                       ("@fuel_correspondence_"^g)) in
  
positive.code:                 in
  
                  (* Open binders *)
                  let (binders, body, _, t_body), curry = destruct_bound_function flid t_norm e in
                  if Env.debug env.tcenv <| Options.Other "SMTEncoding"
                  then BU.print2 "Encoding let : binders=[%s], body=%s\n"
                                  (Print.binders_to_string ", " binders)
  
negative.code:               match (SS.compress t_norm).n with
                | Tm_arrow(formals, c) ->
                  let formals, c = SS.open_comp formals c in
                  let tres_comp = get_result_comp c in
                  let binders, body = eta_expand [] formals e (U.comp_result tres_comp) in
                  (binders, body, formals, tres_comp), false
                | Tm_refine (bv, _) -> aux' bv.sort
                | _ -> ([], e, [], S.mk_Total t_norm), false
              in
              aux' t_norm
            end
  