anchor.diff:    match try_lookup_lid env x.fv_name.v with
     (* Need to introduce a new name decl *)
     | None ->
  -      let decls, env = encode_free_var env x t t_norm [] in
  +      let decls, env = encode_free_var false env x t t_norm [] in
         let n, x', _ = lookup_lid env x.fv_name.v in
         (n, x'), decls, env
   
  
positive.code:       (n, x), [], env
  
  
  let encode_top_level_val 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
      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
          decls@decls', env) ([], env)
  
  let is_tactic t =
  
negative.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 uninterpreted 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
      || uninterpreted
      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)
  