anchor.diff:            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"
  
positive.code:    match f.tm with
     | App(TrueOp, _) -> true
     | _ -> false
  
  
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)
  