diff --git a/src/util/trace_tags.def b/src/util/trace_tags.def
index 7f8b6988a..92152d2b9 100644
--- a/src/util/trace_tags.def
+++ b/src/util/trace_tags.def
@@ -63,8 +63,32 @@ X(get_uninterp_proc, get_uninterp_proc, "get uninterp proc")
 X(berlekamp_matrix, berlekamp_matrix, "berlekamp matrix")
 X(pob, pob, "pob")
 X(theory_str, theory_str, "theory str")
+X(smt_internalize, smt_internalize, "smt internalize")
 
 // TAG
+X(add_watch_literal_bug, smt_internalize, "add watch literal bug")
+X(internalize_bug, smt_internalize, "internalize bug")
+X(internalize_ite_term_bug, smt_internalize, "internalize ite term bug")
+X(incompleteness_bug, smt_internalize, "incompleteness bug")
+X(generation, smt_internalize, "generation")
+X(gate_clause, smt_internalize, "gate clause")
+X(deep_internalize, smt_internalize, "deep internalize")
+X(assert_distinct, smt_internalize, "assert distinct")
+X(internalize_assertion, smt_internalize, "internalize assertion")
+X(internalize_assertion_ll, smt_internalize, "internalize assertion ll")
+X(internalize_quantifier, smt_internalize, "internalize quantifier")
+X(internalize_quantifier_zero, smt_internalize, "internalize quantifier zero")
+X(internalize_theory_atom, smt_internalize, "internalize theory atom")
+X(undo_mk_bool_var, smt_internalize, "undo mk bool var")
+X(undo_mk_enode, smt_internalize, "undo mk enode")
+X(simplify_aux_clause_literals, smt_internalize, "simplify aux clause literals")
+X(simplify_aux_lemma_literals, smt_internalize, "simplify aux lemma literals")
+X(resolve_conflict_crash, smt_internalize, "resolve conflict crash")
+X(mk_clause_result, smt_internalize, "mk clause result")
+X(mk_and_cnstr, smt_internalize, "mk and cnstr")
+X(mk_iff_cnstr, smt_internalize, "mk iff cnstr")
+X(mk_th_axiom, smt_internalize, "mk th axiom")
+
 X(t_str_dump_assign, theory_str, "dump assign")
 X(t_str_dump_assign_on_scope_change, theory_str, "dump assign on scope change")
 X(qe_def, eq_der, "qe def")
@@ -91,7 +115,6 @@ X(add_eq_bug, Global, "add eq bug")
 X(add_eq_detail, Global, "add eq detail")
 X(add_eq_parents, Global, "add eq parents")
 X(add_var, lar_solver, "add var")
-X(add_watch_literal_bug, Global, "add watch literal bug")
 X(after_bit_blaster, imp, "after bit blaster")
 X(after_bv_size_reduction, bv_size_reduction_tactic, "after bv size reduction")
 X(after_cleanup, Global, "after cleanup")
@@ -178,7 +201,6 @@ X(array_map_bug, Global, "array map bug")
 X(array_rewriter, Global, "array rewriter")
 X(artih, Global, "artih")
 X(assert_bound, Global, "assert bound")
-X(assert_distinct, Global, "assert distinct")
 X(assert_eq_bug, ctx_propagate_assertions, "assert eq bug")
 X(assert_expr_bug, Global, "assert expr bug")
 X(assert_k_diseq_exceptions, auf_solver, "assert k diseq exceptions")
@@ -341,7 +363,6 @@ X(decide, Global, "decide")
 X(decide_detail, Global, "decide detail")
 X(declare_const, parser, "declare const")
 X(declare_datatypes, parser, "declare datatypes")
-X(deep_internalize, Global, "deep internalize")
 X(degree_shift, imp, "degree shift")
 X(del_atoms, Global, "del atoms")
 X(del_inactive_lemmas, Global, "del inactive lemmas")
@@ -505,13 +526,11 @@ X(func_decl_alias, Global, "func decl alias")
 X(func_decls, Global, "func decls")
 X(func_interp, Global, "func interp")
 X(func_interp_bug, Global, "func interp bug")
-X(gate_clause, Global, "gate clause")
 X(gb_bug, Global, "gb bug")
 X(gcd, Global, "gcd")
 X(gcd_calls, Global, "gcd calls")
 X(gcd_test, Global, "gcd test")
 X(gcd_test_bug, Global, "gcd test bug")
-X(generation, Global, "generation")
 X(get_assignment_bug, Global, "get assignment bug")
 X(get_implied_equalities, get_implied_equalities_impl, "get implied equalities")
 X(get_macro, Global, "get macro")
@@ -549,7 +568,6 @@ X(horner_bug, Global, "horner bug")
 X(hyper_res, Global, "hyper res")
 X(imply_eq, Global, "imply eq")
 X(in_monovariate_monomials, Global, "in monovariate monomials")
-X(incompleteness_bug, Global, "incompleteness bug")
 X(incremental_matcher, mam_impl, "incremental matcher")
 X(indgen, lemma_inductive_generalizer, "indgen")
 X(inf_rational, Global, "inf rational")
@@ -566,15 +584,8 @@ X(int_solver, Global, "int solver")
 X(interface_eq, Global, "interface eq")
 X(internalize, Global, "internalize")
 X(internalize_add_bug, Global, "internalize add bug")
-X(internalize_assertion, Global, "internalize assertion")
-X(internalize_assertion_ll, Global, "internalize assertion ll")
 X(internalize_assertions, Global, "internalize assertions")
-X(internalize_bug, Global, "internalize bug")
-X(internalize_ite_term_bug, Global, "internalize ite term bug")
 X(internalize_mul_core, Global, "internalize mul core")
-X(internalize_quantifier, Global, "internalize quantifier")
-X(internalize_quantifier_zero, Global, "internalize quantifier zero")
-X(internalize_theory_atom, Global, "internalize theory atom")
 X(interpolator, Global, "interpolator")
 X(interval, Global, "interval")
 X(interval_bug, Global, "interval bug")
@@ -672,7 +683,6 @@ X(missing_instance, mam_impl, "missing instance")
 X(missing_instance_detail, Global, "missing instance detail")
 X(missing_propagation, Global, "missing propagation")
 X(mk_and_bug, Global, "mk and bug")
-X(mk_and_cnstr, Global, "mk and cnstr")
 X(mk_and_elim, Global, "mk and elim")
 X(mk_arith_var, Global, "mk arith var")
 X(mk_asserted_bug, Global, "mk asserted bug")
@@ -680,14 +690,12 @@ X(mk_axioms_bug, Global, "mk axioms bug")
 X(mk_bool_var, Global, "mk bool var")
 X(mk_bound_axioms, Global, "mk bound axioms")
 X(mk_clause, Global, "mk clause")
-X(mk_clause_result, Global, "mk clause result")
 X(mk_conflict_proof, Global, "mk conflict proof")
 X(mk_constraint_bug, imp, "mk constraint bug")
 X(mk_definition_bug, Global, "mk definition bug")
 X(mk_enode, Global, "mk enode")
 X(mk_enode_detail, Global, "mk enode detail")
 X(mk_filter_rules, Global, "mk filter rules")
-X(mk_iff_cnstr, Global, "mk iff cnstr")
 X(mk_le_bug, Global, "mk le bug")
 X(mk_lemma, Global, "mk lemma")
 X(mk_modus_ponens, Global, "mk modus ponens")
@@ -695,7 +703,6 @@ X(mk_mul_eq, Global, "mk mul eq")
 X(mk_pbc, imp, "mk pbc")
 X(mk_proof, Global, "mk proof")
 X(mk_quantifier, parser, "mk quantifier")
-X(mk_th_axiom, Global, "mk th axiom")
 X(mk_th_lemma, Global, "mk th lemma")
 X(mk_transitivity, Global, "mk transitivity")
 X(mk_unit_resolution_bug, Global, "mk unit resolution bug")
@@ -1007,7 +1014,6 @@ X(reorder, Global, "reorder")
 X(report_costs, join_planner, "report costs")
 X(resolve_bug, Global, "resolve bug")
 X(resolve_conflict_bug, Global, "resolve conflict bug")
-X(resolve_conflict_crash, Global, "resolve conflict crash")
 X(restore_assignment_bug, Global, "restore assignment bug")
 X(resultant, Global, "resultant")
 X(rewriter, Global, "rewriter")
@@ -1086,8 +1092,6 @@ X(simple_parser, Global, "simple parser")
 X(simplex, Global, "simplex")
 X(simplifier, Global, "simplifier")
 X(simplify, Global, "simplify")
-X(simplify_aux_clause_literals, Global, "simplify aux clause literals")
-X(simplify_aux_lemma_literals, Global, "simplify aux lemma literals")
 X(simplify_clauses, Global, "simplify clauses")
 X(simplify_clauses_bug, Global, "simplify clauses bug")
 X(simplify_clauses_detail, Global, "simplify clauses detail")
@@ -1207,8 +1211,6 @@ X(try_ite_value, Global, "try ite value")
 X(tseitin_cnf, imp, "tseitin cnf")
 X(tseitin_cnf_bug, imp, "tseitin cnf bug")
 X(unassigned_atoms, Global, "unassigned atoms")
-X(undo_mk_bool_var, Global, "undo mk bool var")
-X(undo_mk_enode, Global, "undo mk enode")
 X(unifier, Global, "unifier")
 X(union_find, Global, "union find")
 X(unit_bug, Global, "unit bug")