anchor.diff:    match se.sigel with
     | Sig_inductive_typ _ -> failwith "add_sigelt_to_env: Impossible, bare data constructor"
     | Sig_datacon _ -> failwith "add_sigelt_to_env: Impossible, bare data constructor"
  -  | Sig_pragma (ResetOptions _) ->
  -    let env = Env.set_proof_ns (Options.using_facts_from ()) env in
  -    env.solver.refresh();
  -    env
  +  | Sig_pragma (ResetOptions _) -> z3_reset_options env
     | Sig_pragma _
     | Sig_new_effect_for_free _ -> env
     | Sig_new_effect ne ->
  
positive.code:     ignore (Env.pop env "tc_inductive");
      res
  
  
  (* [tc_decl env se] typechecks [se] in environment [env] and returns *)
  (* the list of typechecked sig_elts, and a list of new sig_elts elaborated during typechecking but not yet typechecked *)
  
negative.code:     //for hints, we want to use the same id counter as was used in typechecking the module itself, so use the tbl from env
      let en0 = { en0 with qtbl_name_and_index = en.qtbl_name_and_index |> fst, None } in
  
      let en0 =
        if not (Options.interactive ()) then begin  //we should not have this case actually since extracted interfaces are not supported in ide yet
          Options.restore_cmd_line_options true |> ignore;
          z3_reset_options en0
        end
        else en0
      in
  
      //extract the interface in new environment en, since we may need to unfold effect abbreviations for the current module to decide what to keep in the interface
      let modul_iface = extract_interface en m in
  