anchor.diff:                           | _ -> failwith "Impossible: gamma contains leaked names"
                    in
                    let modul, env = Tc.check_module tcenv fmod (is_some pre_fn) in
  -                 if (not (Options.lax())) then begin
  -                   ignore (FStar.SMTEncoding.Encode.encode_modul env modul);
  -                   FStar.SMTEncoding.Z3.refresh ()
  -                 end;
  -                 (modul, env)
  +                 let smt_decls =
  +                   if (not (Options.lax()))
  +                   then let smt_decls = FStar.SMTEncoding.Encode.encode_modul env modul in
  +                        FStar.SMTEncoding.Z3.refresh ();
  +                        smt_decls
  +                   else [], []
  +                 in
  +                 ((modul, smt_decls), env)
               ))
             in
             let extracted_defs, extract_time = with_env env (maybe_extract_mldefs tcmod) in
  
positive.code:           {
              checked_module=tcmod;
              tc_time=tc_time;
  
              extraction_time = extract_time + iface_extraction_time;
              mii = mii
  
negative.code: type tc_result = {
    checked_module: Syntax.modul; //persisted
    mii:module_inclusion_info; //persisted
    smt_decls:(FStar.SMTEncoding.Term.decls_t * list<FStar.SMTEncoding.Env.fvar_binding>); //persisted
  
    tc_time:int;
    extraction_time:int
  