anchor.diff:   }
   exception Let_rec_unencodeable
   
  +exception Inner_let_rec
  +
   let encode_const = function
       | Const_unit -> mk_Term_unit
       | Const_bool true -> boxBool mkTrue
  
positive.code:         encode_let x t1 e1 e2 env encode_term
  
        | Tm_let _ ->
          Errors.diag t0.pos "Non-top-level recursive functions are not yet fully encoded to the SMT solver; you may not be able to prove some facts";
          let e = varops.fresh "let-rec" in
          let decl_e = Term.DeclFun(e, [], Term_sort, None) in
          mkFreeV(e, Term_sort), [decl_e]
  
        | Tm_match(e, pats) ->
          encode_match e pats mk_Term_unit env encode_term
  
negative.code:                     | [e; t_norm] -> e, t_norm
                      | _ -> failwith "Impossible" in
                  {env with tcenv=tcenv'}, e, t_norm
                  in
  
                  (* Open binders *)
                  let (binders, 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)
                                  (Print.term_to_string body);
                  (* Encode binders *)
                  let vars, guards, env', binder_decls, _ = encode_binders None binders env' in
  
                  let body =
                  (* Reify the body if needed *)
                  if is_reifiable_function env'.tcenv t_norm
                  then TcUtil.reify_body env'.tcenv body
                  else body
                  in
                  let app = mk_app curry f ftok vars in
                  let app, (body, decls2) =
                      if quals |> List.contains Logic
                      then mk_Valid app, encode_formula body env'
                      else app, encode_term body env'
                  in
  
                  //NS 05.25: This used to be mkImp(mk_and_l guards, mkEq(app, body))),
                  //But the guard is unnecessary given the pattern
                  let eqn = Util.mkAssume(mkForall([[app]], vars, mkEq(app,body)),
                                      Some (BU.format1 "Equation for %s" flid.str),
                                      ("equation_"^f)) in
                  decls@binder_decls@decls2@[eqn]@primitive_type_axioms env.tcenv flid f app,
                  env
              | _ -> failwith "Impossible"
          in
  
          let encode_rec_lbdefs (bindings:list<letbinding>) (typs:list<S.term>) (toks:list<(S.fv * (string * option<term>))>) (env:env_t) =
            (* encoding recursive definitions using fuel to throttle unfoldings *)
            (* We create a new variable corresponding to the current fuel *)
            let fuel = varops.fresh "fuel", Fuel_sort in
  