anchor.diff:        (n, x), [], env
   
   
  -let encode_top_level_val env lid t quals =
  +let encode_top_level_val uninterpreted env lid t quals =
       let tt = norm env t in
   //        if Env.debug env.tcenv <| Options.Other "SMTEncoding"
   //        then Printf.printf "Encoding top-level val %s : %s\Normalized to is %s\n"
   //            (Print.lid_to_string lid)
   //            (Print.term_to_string t)
   //            (Print.term_to_string tt);
  -    let decls, env = encode_free_var env lid t tt quals in
  +    let decls, env = encode_free_var uninterpreted env lid t tt quals in
       if U.is_smt_lemma t
       then decls@encode_smt_lemma env lid tt, env
       else decls, env
   
   let encode_top_level_vals env bindings quals =
       bindings |> List.fold_left (fun (decls, env) lb ->
  -        let decls', env = encode_top_level_val env (BU.right lb.lbname) lb.lbtyp quals in
  +        let decls', env = encode_top_level_val false env (BU.right lb.lbname) lb.lbtyp quals in
           decls@decls', env) ([], env)
   
   let is_tactic t =
  
positive.code:     let form, decls = encode_function_type_as_formula t env in
      decls@[Util.mkAssume(form, Some ("Lemma: " ^ lid.str), ("lemma_"^lid.str))]
  
  let encode_free_var env fv tt t_norm quals =
      let lid = fv.fv_name.v in
      if not <| (U.is_pure_or_ghost_function t_norm || is_reifiable_function env.tcenv t_norm)
      || U.is_lemma t_norm
      then let vname, vtok, env = new_term_constant_and_tok_from_lid env lid in
           let arg_sorts = match (SS.compress t_norm).n with
              | Tm_arrow(binders, _) -> binders |> List.map (fun _ -> Term_sort)
  
negative.code:           BU.string_of_bytes bytes = "opaque_to_smt"
          | _ -> false
      in
      let is_uninterpreted_by_smt (t:S.term) =
          match (SS.compress t).n with
          | Tm_constant (Const_string(bytes, _)) ->
            BU.string_of_bytes bytes = "uninterpreted_by_smt"
          | _ -> false
      in
      match se.sigel with
       | Sig_new_effect_for_free _ ->
           failwith "impossible -- removed by tc.fs"
  