// CLASS or STRUCT 
X(Global, Global, "Unknown Class")

X(arith_bounds_tactic, arith_bounds_tactic, "arith bounds tactic")
X(add_bounds_tactic, add_bounds_tactic, "add bounds tactic")
X(parser, parser, "parser")
X(ctx_propagate_assertions, ctx_propagate_assertions, "ctx propagate assertions")
X(bv_size_reduction_tactic, bv_size_reduction_tactic, "bv size reduction tactic")
X(lar_solver, lar_solver, "lar solver")
X(imp, imp, "imp")
X(auf_solver, auf_solver, "auf solver")
X(split_clause_tactic, split_clause_tactic, "split clause tactic")
X(check_sat_using_tactic_cmd, check_sat_using_tactic_cmd, "check sat using tactic command")
X(rw_cfg, rw_cfg, "rw cfg")
X(bv_bound_chk_rewriter_cfg, bv_bound_chk_rewriter_cfg, "bv bound chk rewriter cfg")
X(eq_der, eq_der, "eq der")
X(elim_uncnstr_tactic, elim_uncnstr_tactic, "elim uncnstr tactic")
X(fm_model_converter, fm_model_converter, "fm model converter")
X(get_implied_equalities_impl, get_implied_equalities_impl, "get implied equalities impl")
X(ackermannize_bv_tactic, ackermannize_bv_tactic, "ackermannize bv tactic")
X(inc_sat_solver, inc_sat_solver, "inc sat solver")
X(create_cut, create_cut, "create cut")
X(mam_impl, mam_impl, "mam impl")
X(lemma_inductive_generalizer, lemma_inductive_generalizer, "lemma inductive generalizer")
X(injectivity_tactic, injectivity_tactic, "injectivity tactic")
X(bounded_int2bv_solver, bounded_int2bv_solver, "bounded int2bv solver")
X(quantifier_analyzer, quantifier_analyzer, "quantifier analyzer")
X(ite_term_relevancy_eh, ite_term_relevancy_eh, "ite term relevancy eh")
X(smt2_printer, smt2_printer, "smt2 printer")
X(combined_solver, combined_solver, "combined solver")
X(lia_rewriter_cfg, lia_rewriter_cfg, "lia rewriter cfg")
X(relevancy_propagator_imp, relevancy_propagator_imp, "relevancy propagator imp")
X(is_non_nira_functor, is_non_nira_functor, "is non nira functor")
X(push_instantiations_up_cl, push_instantiations_up_cl, "push instantiations up cl")
X(nlarith_plugin, nlarith_plugin, "nlarith plugin")
X(tangent_imp, tangent_imp, "tangent imp")
X(th_rewriter_cfg, th_rewriter_cfg, "th rewriter cfg")
X(purify_arith_proc, purify_arith_proc, "purify arith proc")
X(qsat, qsat, "qsat")
X(lex_lt2, lex_lt2, "lex lt2")
X(trace_tactic, trace_tactic, "trace tactic")
X(compiler, compiler, "compiler")
X(interpreter, interpreter, "interpreter")
X(default_qm_plugin, default_qm_plugin, "default qm plugin")
X(name_nested_formulas, name_nested_formulas, "name nested formulas")
X(monomial_manager, monomial_manager, "monomial manager")
X(nary_tactical, nary_tactical, "nary tactical")
X(propagate_values_tactic, propagate_values_tactic, "propagate values tactic")
X(expr_substitution_simplifier, expr_substitution_simplifier, "expr substitution simplifier")
X(kernel, kernel, "kernel")
X(ast_pp_dot_st, ast_pp_dot_st, "ast pp dot st")
X(sls_tactic, sls_tactic, "sls tactic")
X(reduce_args_simplifier, reduce_args_simplifier, "reduce args simplifier")
X(join_planner, join_planner, "join planner")
X(well_sorted_proc, well_sorted_proc, "well sorted proc")
X(using_params_tactical, using_params_tactical, "using params tactical")
X(theory_aware_branching_queue, theory_aware_branching_queue, "theory aware branching queue")
X(pool_solver, pool_solver, "pool solver")
X(conv_rewriter_cfg, conv_rewriter_cfg, "conv rewriter cfg")
X(simplifier_solver, simplifier_solver, "simplifier solver")
X(bool_plugin, bool_plugin, "bool plugin")
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")

// TAG
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")
X(spacer_timeit, pob, "spacer timeit")
X(polynomial_factorization__bughunt, berlekamp_matrix, "polynomial factorization bug hunt")
X(qe_debug, Global, "qe debug")
X(old_interval, Global, "old interval")
X(CRA, Global, "CRA")
X(Lazard, Global, "Lazard")
X(QF_AUFLIA, Global, "QF AUFLIA")
X(TAG, Global, "TAG")
X(ac_sharing_detail, Global, "ac sharing detail")
X(ack, Global, "ack")
X(ackermannize, Global, "ackermannize")
X(activity_profile, Global, "activity profile")
X(add_bound, Global, "add bound")
X(add_bounds, add_bounds_tactic, "add bounds")
X(add_bug, Global, "add bug")
X(add_constraint_bug, imp, "add constraint bug")
X(add_diseq, Global, "add diseq")
X(add_diseq_inconsistent, Global, "add diseq inconsistent")
X(add_eq, Global, "add eq")
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")
X(after_first_propagate, Global, "after first propagate")
X(after_init_search, Global, "after init search")
X(after_internalization, Global, "after internalization")
X(after_internalize_assertions, Global, "after internalize assertions")
X(after_pop, parser, "after pop")
X(after_quasi_macros, Global, "after quasi macros")
X(after_reduce, Global, "after reduce")
X(after_reduce_ll, Global, "after reduce ll")
X(after_search, Global, "after search")
X(after_simplifier, Global, "after simplifier")
X(after_simplifier_detail, Global, "after simplifier detail")
X(aig2expr, Global, "aig2expr")
X(aig_lit_count, Global, "aig lit count")
X(aig_simplifier, Global, "aig simplifier")
X(algebraic, Global, "algebraic")
X(algebraic2expr, Global, "algebraic2expr")
X(algebraic_bug, Global, "algebraic bug")
X(algebraic_select, Global, "algebraic select")
X(anf_simplifier, Global, "anf simplifier")
X(anum_detail, Global, "anum detail")
X(anum_eval_sign, Global, "anum eval sign")
X(anum_mk_binary, Global, "anum mk binary")
X(app_ground, Global, "app ground")
X(are_distinct_bug, Global, "are distinct bug")
X(arith, Global, "arith")
X(arith_adaptive, Global, "arith adaptive")
X(arith_bound, Global, "arith bound")
X(arith_bug, Global, "arith bug")
X(arith_conflict, Global, "arith conflict")
X(arith_eq, Global, "arith eq")
X(arith_eq_adapter, Global, "arith eq adapter")
X(arith_eq_adapter_bug, Global, "arith eq adapter bug")
X(arith_eq_adapter_detail, Global, "arith eq adapter detail")
X(arith_eq_adapter_info, Global, "arith eq adapter info")
X(arith_eq_adapter_mk_axioms, Global, "arith eq adapter mk axioms")
X(arith_eq_adapter_perf, Global, "arith eq adapter perf")
X(arith_eq_adapter_profile, Global, "arith eq adapter profile")
X(arith_eq_adapter_profile_detail, Global, "arith eq adapter profile detail")
X(arith_eq_adapter_relevancy, Global, "arith eq adapter relevancy")
X(arith_eq_solver, Global, "arith eq solver")
X(arith_eq_verbose, Global, "arith eq verbose")
X(arith_final, Global, "arith final")
X(arith_imply_bound, Global, "arith imply bound")
X(arith_init_search, Global, "arith init search")
X(arith_int, Global, "arith int")
X(arith_int_detail, Global, "arith int detail")
X(arith_int_fracs_min_max, Global, "arith int fracs min max")
X(arith_int_freedom, Global, "arith int freedom")
X(arith_int_incomp, Global, "arith int incomp")
X(arith_int_inf, Global, "arith int inf")
X(arith_int_rows, Global, "arith int rows")
X(arith_internalize, Global, "arith internalize")
X(arith_internalize_detail, Global, "arith internalize detail")
X(arith_make_feasible, Global, "arith make feasible")
X(arith_make_feasible_detail, Global, "arith make feasible detail")
X(arith_mk_polynomial, Global, "arith mk polynomial")
X(arith_mod, Global, "arith mod")
X(arith_new_diseq_eh, Global, "arith new diseq eh")
X(arith_new_eq_eh, Global, "arith new eq eh")
X(arith_pivot, Global, "arith pivot")
X(arith_pivoting, Global, "arith pivoting")
X(arith_pop_scope_bug, Global, "arith pop scope bug")
X(arith_proof, Global, "arith proof")
X(arith_prop, Global, "arith prop")
X(arith_rand, Global, "arith rand")
X(arith_relevant_eh, Global, "arith relevant eh")
X(arith_rewriter, Global, "arith rewriter")
X(arith_rewriter_gcd, Global, "arith rewriter gcd")
X(arith_subsumption, arith_bounds_tactic, "arith subsumption")
X(arith_value, Global, "arith value")
X(arith_verbose, Global, "arith verbose")
X(array, Global, "array")
X(array_axiom, Global, "array axiom")
X(array_axiom2b, Global, "array axiom2b")
X(array_bug, Global, "array bug")
X(array_decl_plugin_bug, Global, "array decl plugin bug")
X(array_ext, Global, "array ext")
X(array_factory, Global, "array factory")
X(array_factory_bug, Global, "array factory bug")
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")
X(asserted_formulas, Global, "asserted formulas")
X(asserted_formulas_bug, Global, "asserted formulas bug")
X(asserted_formulas_scopes, Global, "asserted formulas scopes")
X(assign_bit_bug, Global, "assign bit bug")
X(assign_core, Global, "assign core")
X(assign_profile, Global, "assign profile")
X(assign_quantifier_bug, Global, "assign quantifier bug")
X(assigned_literals_per_lvl, Global, "assigned literals per lvl")
X(assume_eq, Global, "assume eq")
X(assume_eq_int, Global, "assume eq int")
X(assume_eqs, Global, "assume eqs")
X(assumption, Global, "assumption")
X(assumptions, Global, "assumptions")
X(ast, Global, "ast")
X(ast_delete_node, Global, "ast delete node")
X(ast_translation, Global, "ast translation")
X(asymm_branch, Global, "asymm branch")
X(asymm_branch_detail, Global, "asymm branch detail")
X(ba, Global, "ba")
X(ba_verbose, Global, "ba verbose")
X(bcd, Global, "bcd")
X(bcp_bug, Global, "bcp bug")
X(bdd, Global, "bdd")
X(before_bit_blaster, imp, "before bit blaster")
X(before_bv_size_reduction, bv_size_reduction_tactic, "before bv size reduction")
X(before_check_sat, Global, "before check sat")
X(before_quasi_macros, Global, "before quasi macros")
X(before_reduce, Global, "before reduce")
X(before_sat_solver, imp, "before sat solver")
X(before_search, Global, "before search")
X(before_split_clause, split_clause_tactic, "before split clause")
X(begin_assert_expr, Global, "begin assert expr")
X(begin_assert_expr_ll, Global, "begin assert expr ll")
X(bin_clause_bug, Global, "bin clause bug")
X(bindings, Global, "bindings")
X(bit2int, Global, "bit2int")
X(bit2int_verbose, Global, "bit2int verbose")
X(bit_blaster, Global, "bit blaster")
X(bit_vector, Global, "bit vector")
X(bitwise_not, Global, "bitwise not")
X(blands_rule, Global, "blands rule")
X(blast_eq_value, Global, "blast eq value")
X(blast_term_ite, rw_cfg, "blast term ite")
X(blocked_clause, Global, "blocked clause")
X(blocked_clause_bug, Global, "blocked clause bug")
X(bmc, Global, "bmc")
X(bound_analyzer, Global, "bound analyzer")
X(bound_bug, Global, "bound bug")
X(bound_manager, Global, "bound manager")
X(bound_propagator, Global, "bound propagator")
X(bound_propagator_derived, Global, "bound propagator derived")
X(bound_propagator_detail, Global, "bound propagator detail")
X(bound_propagator_step, Global, "bound propagator step")
X(bound_propagator_step_detail, Global, "bound propagator step detail")
X(bound_relation, Global, "bound relation")
X(bounded_search, Global, "bounded search")
X(bv, Global, "bv")
X(bv2fpa, Global, "bv2fpa")
X(bv2fpa_rebuild, Global, "bv2fpa rebuild")
X(bv2int_bug, Global, "bv2int bug")
X(bv2int_rewriter, Global, "bv2int rewriter")
X(bv2real_rewriter, Global, "bv2real rewriter")
X(bv_are_distinct, Global, "bv are distinct")
X(bv_bit_prop, Global, "bv bit prop")
X(bv_bound_chk_step, bv_bound_chk_rewriter_cfg, "bv bound chk step")
X(bv_bounds, Global, "bv bounds")
X(bv_bug, Global, "bv bug")
X(bv_diseq_axiom, Global, "bv diseq axiom")
X(bv_eq, Global, "bv eq")
X(bv_ite, Global, "bv ite")
X(bv_op, Global, "bv op")
X(bv_size_reduction, bv_size_reduction_tactic, "bv size reduction")
X(bv_udiv, Global, "bv udiv")
X(bv_verbose, Global, "bv verbose")
X(bvarray2uf_rw, Global, "bvarray2uf rw")
X(bvarray2uf_rw_q, Global, "bvarray2uf rw q")
X(cached_generation, Global, "cached generation")
X(card, Global, "card")
X(card2bv, Global, "card2bv")
X(carry, Global, "carry")
X(carry_sorted, Global, "carry sorted")
X(case_split, Global, "case split")
X(causality, Global, "causality")
X(cg, Global, "cg")
X(cg_table, Global, "cg table")
X(chainable, Global, "chainable")
X(change_x_del, Global, "change x del")
X(chashtable, Global, "chashtable")
X(check_enode, Global, "check enode")
X(check_explanation, Global, "check explanation")
X(check_logic, Global, "check logic")
X(check_main_int, Global, "check main int")
X(check_relevancy, Global, "check relevancy")
X(check_sat_using, check_sat_using_tactic_cmd, "check sat using")
X(check_th_diseq_propagation, Global, "check th diseq propagation")
X(checker, Global, "checker")
X(clause_proof, Global, "clause proof")
X(clause_use_list_bug, Global, "clause use list bug")
X(cleanup_bug, Global, "cleanup bug")
X(cluster_stats, Global, "cluster stats")
X(cluster_stats_verb, Global, "cluster stats verb")
X(cmd_context, Global, "cmd context")
X(cmd_context_detail, Global, "cmd context detail")
X(coeff_bug, Global, "coeff bug")
X(cofactor, Global, "cofactor")
X(cofactor_bug, Global, "cofactor bug")
X(cofactor_ite, Global, "cofactor ite")
X(collect, Global, "collect")
X(collect_info, Global, "collect info")
X(collector, Global, "collector")
X(comm_proof_bug, Global, "comm proof bug")
X(concretize, Global, "concretize")
X(conflict, Global, "conflict")
X(conflict_, Global, "conflict ")
X(conflict_bug, Global, "conflict bug")
X(conflict_detail, Global, "conflict detail")
X(conflict_detail_verbose, Global, "conflict detail verbose")
X(conflict_smt2, Global, "conflict smt2")
X(conflict_verbose, Global, "conflict verbose")
X(consume_attributes, parser, "consume attributes")
X(content_bug, Global, "content bug")
X(context, Global, "context")
X(context_lemma, Global, "context lemma")
X(context_proof, Global, "context proof")
X(context_proof_hack, Global, "context proof hack")
X(convert_bug, Global, "convert bug")
X(copy_families_plugins, Global, "copy families plugins")
X(core_array_eq, Global, "core array eq")
X(core_eq, Global, "core eq")
X(cosine, Global, "cosine")
X(cross_nested, Global, "cross nested")
X(cross_nested_bug, Global, "cross nested bug")
X(ctx_simplify_tactic, Global, "ctx simplify tactic")
X(ctx_simplify_tactic_bug, Global, "ctx simplify tactic bug")
X(ctx_simplify_tactic_cache, Global, "ctx simplify tactic cache")
X(ctx_simplify_tactic_detail, Global, "ctx simplify tactic detail")
X(ctx_simplify_tactic_ite_bug, Global, "ctx simplify tactic ite bug")
X(ctx_solver_simplify_tactic, ctx_solver_simplify_tactic, "ctx solver simplify tactic")
X(cube, lar_solver, "cube")
X(current_solution_is_inf_on_cut, Global, "current solution is inf on cut")
X(cut_simplifier, Global, "cut simplifier")
X(cvx_dbg, Global, "cvx dbg")
X(cvx_dbg_verb, Global, "cvx dbg verb")
X(d_undo, Global, "d undo")
X(datatype, Global, "datatype")
X(datatype_bug, Global, "datatype bug")
X(datatype_conflict, Global, "datatype conflict")
X(datatype_detail, Global, "datatype detail")
X(datatype_parser_bug, parser, "datatype parser bug")
X(datatype_verbose, Global, "datatype verbose")
X(dd_solver, Global, "dd.solver")
X(dd_solver_d, Global, "dd.solver d")
X(ddl, Global, "ddl")
X(ddl_detail, Global, "ddl detail")
X(ddl_model, Global, "ddl model")
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")
X(del_quantifier, Global, "del quantifier")
X(delete_node_bug, Global, "delete node bug")
X(demodulator, Global, "demodulator")
X(demodulator_bug, Global, "demodulator bug")
X(demodulator_fwd, Global, "demodulator fwd")
X(demodulator_stack, Global, "demodulator stack")
X(dep_intervals, Global, "dep intervals")
X(der, Global, "der")
X(der_bug, eq_der, "der bug")
X(derived_bound, Global, "derived bound")
X(diff_atom, Global, "diff atom")
X(diff_logic, Global, "diff logic")
X(diff_logic_traverse, Global, "diff logic traverse")
X(diff_logic_vars, Global, "diff logic vars")
X(diff_neq_tactic, imp, "diff neq tactic")
X(diff_term, Global, "diff term")
X(dio, Global, "dio")
X(dio_br, Global, "dio br")
X(dio_entry, Global, "dio entry")
X(dio_reg, Global, "dio reg")
X(dio_remove_fresh, Global, "dio remove fresh")
X(dio_s, Global, "dio s")
X(dioph_eq_deb, Global, "dioph eq deb")
X(diseq_bug, Global, "diseq bug")
X(distinct, Global, "distinct")
X(distribute_forall, Global, "distribute forall")
X(div_axiom_bug, Global, "div axiom bug")
X(div_bug, Global, "div bug")
X(divides, Global, "divides")
X(divides_bug, Global, "divides bug")
X(dl, Global, "dl")
X(dl_activity, Global, "dl activity")
X(dl_bfs, Global, "dl bfs")
X(dl_bug, Global, "dl bug")
X(dl_compiler, Global, "dl compiler")
X(dl_decl_plugin, Global, "dl decl plugin")
X(dl_eq_bug, Global, "dl eq bug")
X(dl_interp_tail_simplifier_propagation, Global, "dl interp tail simplifier propagation")
X(dl_interp_tail_simplifier_propagation_pre, Global, "dl interp tail simplifier propagation pre")
X(dl_relation, Global, "dl relation")
X(dl_rule, Global, "dl rule")
X(dl_rule_transf, Global, "dl rule transf")
X(dl_rule_unbound_fix, Global, "dl rule unbound fix")
X(dl_rule_unbound_fix_pre_qe, Global, "dl rule unbound fix pre qe")
X(dl_table_relation, Global, "dl table relation")
X(dl_verbose, Global, "dl verbose")
X(doc, Global, "doc")
X(dt, Global, "dt")
X(dt_is_value, Global, "dt is value")
X(dt_verbose, Global, "dt verbose")
X(dummy, Global, "dummy")
X(dump_terms, lar_solver, "dump terms")
X(dyn_ack, Global, "dyn ack")
X(dyn_ack_clause, Global, "dyn ack clause")
X(dyn_ack_inst, Global, "dyn ack inst")
X(dyn_ack_target, Global, "dyn ack target")
X(elim_bounds, Global, "elim bounds")
X(elim_eqs, Global, "elim eqs")
X(elim_eqs_bug, Global, "elim eqs bug")
X(elim_lit, Global, "elim lit")
X(elim_predicates, Global, "elim predicates")
X(elim_rem, Global, "elim rem")
X(elim_small_bv, rw_cfg, "elim small bv")
X(elim_small_bv_app, rw_cfg, "elim small bv app")
X(elim_small_bv_pre, rw_cfg, "elim small bv pre")
X(elim_term_ite_bug, Global, "elim term ite bug")
X(elim_to_real, Global, "elim to real")
X(elim_uncnstr, elim_uncnstr_tactic, "elim uncnstr")
X(elim_uncnstr_bug, rw_cfg, "elim uncnstr bug")
X(elim_uncnstr_bug_ll, rw_cfg, "elim uncnstr bug ll")
X(elim_unconstrained, Global, "elim unconstrained")
X(elim_unused_vars, Global, "elim unused vars")
X(eliminate, Global, "eliminate")
X(empty_pol, Global, "empty pol")
X(end_assert_expr_ll, Global, "end assert expr ll")
X(epsilon_bug, Global, "epsilon bug")
X(eq, Global, "eq")
X(eq_scc, Global, "eq scc")
X(eq_to_bug, Global, "eq to bug")
X(eqc_bool, Global, "eqc bool")
X(equiv, Global, "equiv")
X(euf, Global, "euf")
X(euf_completion, Global, "euf completion")
X(euf_verbose, Global, "euf verbose")
X(eval_bug, Global, "eval bug")
X(expand_bnd, Global, "expand bnd")
X(expand_bnd_verb, Global, "expand bnd verb")
X(expr2aig, Global, "expr2aig")
X(expr2polynomial, Global, "expr2polynomial")
X(expr2var, Global, "expr2var")
X(expr_abstract, Global, "expr abstract")
X(expr_context_simplifier, Global, "expr context simplifier")
X(expr_pattern_match, Global, "expr pattern match")
X(ext, Global, "ext")
X(ext_gcd_test, Global, "ext gcd test")
X(extract_prop, Global, "extract prop")
X(fact_bug, Global, "fact bug")
X(factor, Global, "factor")
X(factor_bug, Global, "factor bug")
X(factor_rewriter, Global, "factor rewriter")
X(factor_tactic_bug, rw_cfg, "factor tactic bug")
X(farkas_learner2, Global, "farkas learner2")
X(feas_bug, Global, "feas bug")
X(final_check, Global, "final check")
X(final_check_result, Global, "final check result")
X(final_check_stats, Global, "final check stats")
X(final_check_step, Global, "final check step")
X(find_feas_stats, Global, "find feas stats")
X(find_infeasible_int_base_var, Global, "find infeasible int base var")
X(find_ite_bounds, Global, "find ite bounds")
X(find_ite_bounds_bug, Global, "find ite bounds bug")
X(find_wpos, Global, "find wpos")
X(fingerprint_bug, Global, "fingerprint bug")
X(fits, Global, "fits")
X(fix_dl_var, imp, "fix dl var")
X(fix_missing_refs, Global, "fix missing refs")
X(fixed_var_eh, Global, "fixed var eh")
X(flush, Global, "flush")
X(fm, imp, "fm")
X(fm_bug, imp, "fm bug")
X(fm_mc, fm_model_converter, "fm mc")
X(fm_subsumption, imp, "fm subsumption")
X(for_each_ast, Global, "for each ast")
X(for_each_relevant_expr, Global, "for each relevant expr")
X(forget_phase, Global, "forget phase")
X(fp, Global, "fp")
X(fp_rewriter, Global, "fp rewriter")
X(fpa2bv, Global, "fpa2bv")
X(fpa2bv_add, Global, "fpa2bv add")
X(fpa2bv_add_core, Global, "fpa2bv add core")
X(fpa2bv_dbg, Global, "fpa2bv dbg")
X(fpa2bv_div, Global, "fpa2bv div")
X(fpa2bv_float_eq, Global, "fpa2bv float eq")
X(fpa2bv_fma_, Global, "fpa2bv fma ")
X(fpa2bv_is_negative, Global, "fpa2bv is negative")
X(fpa2bv_mc, Global, "fpa2bv mc")
X(fpa2bv_mk_fp, Global, "fpa2bv mk fp")
X(fpa2bv_mul, Global, "fpa2bv mul")
X(fpa2bv_rem, Global, "fpa2bv rem")
X(fpa2bv_round, Global, "fpa2bv round")
X(fpa2bv_round_to_integral, Global, "fpa2bv round to integral")
X(fpa2bv_rw, Global, "fpa2bv rw")
X(fpa2bv_to_bv, Global, "fpa2bv to bv")
X(fpa2bv_to_bv_unspecified, Global, "fpa2bv to bv unspecified")
X(fpa2bv_to_fp, Global, "fpa2bv to fp")
X(fpa2bv_to_fp_real, Global, "fpa2bv to fp real")
X(fpa2bv_to_fp_signed, Global, "fpa2bv to fp signed")
X(fpa2bv_to_fp_unsigned, Global, "fpa2bv to fp unsigned")
X(fpa2bv_to_ieee_bv, Global, "fpa2bv to ieee bv")
X(fpa2bv_to_ieee_bv_unspecified, Global, "fpa2bv to ieee bv unspecified")
X(fpa2bv_to_real, Global, "fpa2bv to real")
X(fpa2bv_to_sbv, Global, "fpa2bv to sbv")
X(fpa2bv_to_ubv, Global, "fpa2bv to ubv")
X(fpa2bv_unpack, Global, "fpa2bv unpack")
X(fpa_util, Global, "fpa util")
X(freedom_interval, Global, "freedom interval")
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")
X(get_model, Global, "get model")
X(get_proof, Global, "get proof")
X(get_proof_bug, Global, "get proof bug")
X(get_proof_bug_after, Global, "get proof bug after")
X(gg, Global, "gg")
X(global, Global, "global")
X(global_verbose, Global, "global verbose")
X(goal, ackermannize_bv_tactic, "goal")
X(goal2nlsat, Global, "goal2nlsat")
X(goal2nlsat_bug, Global, "goal2nlsat bug")
X(goal2sat, inc_sat_solver, "goal2sat")
X(goal2sat_bug, Global, "goal2sat bug")
X(goal2sat_not_handled, Global, "goal2sat not handled")
X(gomory_cut, Global, "gomory cut")
X(gomory_cut_detail, create_cut, "gomory cut detail")
X(gomory_cut_detail_real, create_cut, "gomory cut detail real")
X(gparams, Global, "gparams")
X(grobner, Global, "grobner")
X(grobner_bug, Global, "grobner bug")
X(grobner_d, Global, "grobner d")
X(grobner_d_, Global, "grobner d ")
X(grobner_stats_d, Global, "grobner stats d")
X(guessed_literals, Global, "guessed literals")
X(heap, Global, "heap")
X(hilbert_basis, Global, "hilbert basis")
X(hilbert_basis_verbose, Global, "hilbert basis verbose")
X(hnf, Global, "hnf")
X(hnf_calc, Global, "hnf calc")
X(hnf_cut, Global, "hnf cut")
X(horn, imp, "horn")
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")
X(inherit_bug, Global, "inherit bug")
X(init_bits, Global, "init bits")
X(init_row_bug, Global, "init row bug")
X(inj_axiom, Global, "inj axiom")
X(injectivity, injectivity_tactic, "injectivity")
X(insert_macro, Global, "insert macro")
X(instance, Global, "instance")
X(instantiate_bug, Global, "instantiate bug")
X(int2bv, bounded_int2bv_solver, "int2bv")
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")
X(interval_nth_root, Global, "interval nth root")
X(interval_relation, Global, "interval relation")
X(interval_xn_eq_y, Global, "interval xn eq y")
X(interval_zero_bug, Global, "interval zero bug")
X(inv_algebraic, Global, "inv algebraic")
X(invalid_ptr, Global, "invalid ptr")
X(is_allone, Global, "is allone")
X(is_bv_num, parser, "is bv num")
X(is_diseq, Global, "is diseq")
X(is_diseq_bug, Global, "is diseq bug")
X(is_eq_vector, imp, "is eq vector")
X(is_ext_diseq, Global, "is ext diseq")
X(is_inconsistent, Global, "is inconsistent")
X(is_occ_bug, imp, "is occ bug")
X(is_row_useful, Global, "is row useful")
X(is_shared, Global, "is shared")
X(is_var_and_ground, quantifier_analyzer, "is var and ground")
X(is_var_plus_ground, quantifier_analyzer, "is var plus ground")
X(is_x_gle_t, quantifier_analyzer, "is x gle t")
X(isolate_roots, Global, "isolate roots")
X(isolate_roots_bug, Global, "isolate roots bug")
X(ite_bug, Global, "ite bug")
X(ite_term_relevancy, ite_term_relevancy_eh, "ite term relevancy")
X(lar_solver_details, lar_solver, "lar solver details")
X(lar_solver_feas, Global, "lar solver feas")
X(lar_solver_improve_bounds, lar_solver, "lar solver improve bounds")
X(lar_solver_inf_heap, Global, "lar solver inf heap")
X(lar_solver_model, lar_solver, "lar solver model")
X(lar_solver_rand, lar_solver, "lar solver rand")
X(lar_solver_terms, lar_solver, "lar solver terms")
X(lar_solver_validate, lar_solver, "lar solver validate")
X(lcm_bug, Global, "lcm bug")
X(le_bug, Global, "le bug")
X(le_extra, Global, "le extra")
X(lemma, Global, "lemma")
X(let_frame, parser, "let frame")
X(lex_bug, lex_lt2, "lex bug")
X(lia2pb, imp, "lia2pb")
X(linear_eq_solver, Global, "linear eq solver")
X(linear_equation_bug, Global, "linear equation bug")
X(linear_equation_mk, Global, "linear equation mk")
X(list, Global, "list")
X(literal_occ, Global, "literal occ")
X(lp_core, Global, "lp core")
X(m_tag, trace_tactic, "m tag")
X(macro_bug, Global, "macro bug")
X(macro_finder, Global, "macro finder")
X(macro_insert, Global, "macro insert")
X(macro_manager, Global, "macro manager")
X(macro_manager_bug, Global, "macro manager bug")
X(macro_util, Global, "macro util")
X(macros, Global, "macros")
X(make_var_feasible, Global, "make var feasible")
X(mam, mam_impl, "mam")
X(mam_bug, mam_impl, "mam bug")
X(mam_candidate, mam_impl, "mam candidate")
X(mam_compiler, compiler, "mam compiler")
X(mam_compiler_bug, compiler, "mam compiler bug")
X(mam_compiler_detail, compiler, "mam compiler detail")
X(mam_execute_core, interpreter, "mam execute core")
X(mam_inc_bug, mam_impl, "mam inc bug")
X(mam_inc_bug_detail, mam_impl, "mam inc bug detail")
X(mam_info, mam_impl, "mam info")
X(mam_int, interpreter, "mam int")
X(mam_lbl_bug, compiler, "mam lbl bug")
X(mam_new_pat, mam_impl, "mam new pat")
X(mam_pat, mam_impl, "mam pat")
X(mam_path_tree, mam_impl, "mam path tree")
X(mam_path_tree_updt, mam_impl, "mam path tree updt")
X(mam_stats, default_qm_plugin, "mam stats")
X(mask_bug, Global, "mask bug")
X(max_sharing, Global, "max sharing")
X(may_propagate_bug, Global, "may propagate bug")
X(mbc, Global, "mbc")
X(mbi, Global, "mbi")
X(mbp_tg, Global, "mbp tg")
X(mbp_tg_verbose, Global, "mbp tg verbose")
X(mbqi_bug, Global, "mbqi bug")
X(mbqi_bug_detail, Global, "mbqi bug detail")
X(mbqi_project, Global, "mbqi project")
X(mbqi_project_verbose, Global, "mbqi project verbose")
X(mc, Global, "mc")
X(memory, Global, "memory")
X(merge_theory_vars, Global, "merge theory vars")
X(mf_simp_bug, auf_solver, "mf simp bug")
X(mg_top_sort, Global, "mg top sort")
X(mgcd, Global, "mgcd")
X(mgcd_bug, Global, "mgcd bug")
X(mgcd_call, Global, "mgcd call")
X(mgcd_detail, Global, "mgcd detail")
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")
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")
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")
X(mk_var_bug, Global, "mk var bug")
X(mod_bug, Global, "mod bug")
X(model, Global, "model")
X(model_bug, Global, "model bug")
X(model_checker, Global, "model checker")
X(model_checker_bug_detail, Global, "model checker bug detail")
X(model_constructor, Global, "model constructor")
X(model_converter, Global, "model converter")
X(model_evaluator, Global, "model evaluator")
X(model_finder, Global, "model finder")
X(model_finder_bug, quantifier_analyzer, "model finder bug")
X(model_finder_bug_detail, Global, "model finder bug detail")
X(model_finder_hint, Global, "model finder hint")
X(model_fresh_bug, Global, "model fresh bug")
X(model_generator_bug, Global, "model generator bug")
X(model_smt2_pp, Global, "model smt2 pp")
X(model_validate, Global, "model validate")
X(model_verbose, Global, "model verbose")
X(monomial_mul_bug, monomial_manager, "monomial mul bug")
X(move_unconstrained_to_base, Global, "move unconstrained to base")
X(mp_iff_justification, Global, "mp iff justification")
X(mpbq_bug, Global, "mpbq bug")
X(mpf_dbg, Global, "mpf dbg")
X(mpf_dbg_rem, Global, "mpf dbg rem")
X(mpf_dbg_sbv, Global, "mpf dbg sbv")
X(mpf_mul_bug, Global, "mpf mul bug")
X(mpff, Global, "mpff")
X(mpff_bug, Global, "mpff bug")
X(mpff_div, Global, "mpff div")
X(mpff_power, Global, "mpff power")
X(mpff_to_mpq, Global, "mpff to mpq")
X(mpff_trace, Global, "mpff trace")
X(mpfx, Global, "mpfx")
X(mpfx_power, Global, "mpfx power")
X(mpfx_trace, Global, "mpfx trace")
X(mpn, Global, "mpn")
X(mpn_dbg, Global, "mpn dbg")
X(mpn_div, Global, "mpn div")
X(mpn_div1, Global, "mpn div1")
X(mpn_norm, Global, "mpn norm")
X(mpn_to_string, Global, "mpn to string")
X(mpq, Global, "mpq")
X(mpq_set, Global, "mpq set")
X(mpz, Global, "mpz")
X(mpz_2k, Global, "mpz 2k")
X(mpz_gcd, Global, "mpz gcd")
X(mpz_matrix, Global, "mpz matrix")
X(mpz_mul2k, Global, "mpz mul2k")
X(mpzp_inv_bug, Global, "mpzp inv bug")
X(mpzzp, Global, "mpzzp")
X(mul_bug, Global, "mul bug")
X(mus, Global, "mus")
X(name_expr, parser, "name expr")
X(name_exprs, name_nested_formulas, "name exprs")
X(nary_tactical_updt_params, nary_tactical, "nary tactical updt params")
X(network_flow, Global, "network flow")
X(new_bound, Global, "new bound")
X(new_dt_eh, Global, "new dt eh")
X(new_entries_bug, Global, "new entries bug")
X(newton, Global, "newton")
X(nex_details, Global, "nex details")
X(nex_gt, Global, "nex gt")
X(nl_arith_bug, Global, "nl arith bug")
X(nl_branching, Global, "nl branching")
X(nl_evaluate, Global, "nl evaluate")
X(nl_info, Global, "nl info")
X(nl_value, Global, "nl value")
X(nla, Global, "nla")
X(nla2bv, get_uninterp_proc, "nla2bv")
X(nla2bv_verbose, imp, "nla2bv verbose")
X(nla_cn, Global, "nla cn")
X(nla_cn_, Global, "nla cn ")
X(nla_cn_common_factor, Global, "nla cn common factor")
X(nla_cn_details, Global, "nla cn details")
X(nla_cn_test, Global, "nla cn test")
X(nla_grobner, Global, "nla grobner")
X(nla_horner, Global, "nla horner")
X(nla_intervals, Global, "nla intervals")
X(nla_intervals_details, Global, "nla intervals details")
X(nla_solver, Global, "nla solver")
X(nla_solver_bl, Global, "nla solver bl")
X(nla_solver_check_monic, Global, "nla solver check monic")
X(nla_solver_details, Global, "nla solver details")
X(nla_solver_div, Global, "nla solver div")
X(nla_solver_eq, Global, "nla solver eq")
X(nla_solver_mons, Global, "nla solver mons")
X(nla_solver_tp, tangent_imp, "nla solver tp")
X(nla_solver_verbose, Global, "nla solver verbose")
X(nla_test, Global, "nla test")
X(nla_test_, Global, "nla test ")
X(nlarith, nlarith_plugin, "nlarith")
X(nlarith_verbose, Global, "nlarith verbose")
X(nlsat, imp, "nlsat")
X(nlsat_assign, Global, "nlsat assign")
X(nlsat_bool_assignment, Global, "nlsat bool assignment")
X(nlsat_bool_assignment_bug, Global, "nlsat bool assignment bug")
X(nlsat_bug, Global, "nlsat bug")
X(nlsat_evaluator, Global, "nlsat evaluator")
X(nlsat_evaluator_bug, Global, "nlsat evaluator bug")
X(nlsat_explain, Global, "nlsat explain")
X(nlsat_factor, Global, "nlsat factor")
X(nlsat_fd, Global, "nlsat fd")
X(nlsat_inf_set, Global, "nlsat inf set")
X(nlsat_interval, Global, "nlsat interval")
X(nlsat_lazy, Global, "nlsat lazy")
X(nlsat_mathematica, Global, "nlsat mathematica")
X(nlsat_minimize, Global, "nlsat minimize")
X(nlsat_model, Global, "nlsat model")
X(nlsat_proof, Global, "nlsat proof")
X(nlsat_proof_sk, Global, "nlsat proof sk")
X(nlsat_reorder, Global, "nlsat reorder")
X(nlsat_reorder_clauses, Global, "nlsat reorder clauses")
X(nlsat_resolve, Global, "nlsat resolve")
X(nlsat_resolve_done, Global, "nlsat resolve done")
X(nlsat_root, Global, "nlsat root")
X(nlsat_simpilfy_core, Global, "nlsat simpilfy core")
X(nlsat_simplify_core, Global, "nlsat simplify core")
X(nlsat_smt2, Global, "nlsat smt2")
X(nlsat_solver, Global, "nlsat solver")
X(nlsat_sort, Global, "nlsat sort")
X(nlsat_table_bug, Global, "nlsat table bug")
X(nlsat_verbose, Global, "nlsat verbose")
X(nnf, nnf, "nnf")
X(nnf_bug, Global, "nnf bug")
X(nnf_result, Global, "nnf result")
X(no_overflow, Global, "no overflow")
X(non_diff_logic, Global, "non diff logic")
X(non_linear, Global, "non linear")
X(non_linear_bug, Global, "non linear bug")
X(non_linear_gb, Global, "non linear gb")
X(non_linear_verbose, Global, "non linear verbose")
X(nondet_bug, Global, "nondet bug")
X(norm_eq_proof, Global, "norm eq proof")
X(norm_eq_proof_bug, Global, "norm eq proof bug")
X(normalize_bounds_tactic, imp, "normalize bounds tactic")
X(normalize_fraction_bug, Global, "normalize fraction bug")
X(nra, Global, "nra")
X(nth_root, Global, "nth root")
X(nth_root_bug, Global, "nth root bug")
X(nth_root_trace, Global, "nth root trace")
X(num_bits_bug, imp, "num bits bug")
X(object_allocator, Global, "object allocator")
X(old_spacer, Global, "old spacer")
X(opt, Global, "opt")
X(opt1, Global, "opt1")
X(opt_verbose, Global, "opt verbose")
X(optional, Global, "optional")
X(p2expr_bug, Global, "p2expr bug")
X(parent_bug, Global, "parent bug")
X(parray, Global, "parray")
X(parray_mem, Global, "parray mem")
X(parse_bv_numeral, parser, "parse bv numeral")
X(parse_expr, parser, "parse expr")
X(parse_numeral, parser, "parse numeral")
X(parse_qualified_name, parser, "parse qualified name")
X(parse_quantifier, parser, "parse quantifier")
X(parse_sorted_vars, parser, "parse sorted vars")
X(parser_error, parser, "parser error")
X(patch_int, Global, "patch int")
X(pattern_inference, Global, "pattern inference")
X(pattern_inference_skolem, Global, "pattern inference skolem")
X(pb, Global, "pb")
X(pb2bv, imp, "pb2bv")
X(pb2bv_bug, imp, "pb2bv bug")
X(pb2bv_bv, imp, "pb2bv bv")
X(pb2bv_bv_detail, imp, "pb2bv bv detail")
X(pb2bv_convert, imp, "pb2bv convert")
X(pb_validate, Global, "pb validate")
X(pb_verbose, Global, "pb verbose")
X(pbsum, lia_rewriter_cfg, "pbsum")
X(pconstructor_decl, Global, "pconstructor decl")
X(pcs, Global, "pcs")
X(pdecl_manager, Global, "pdecl manager")
X(pdr, Global, "pdr")
X(pdr_verbose, Global, "pdr verbose")
X(phase_selection, Global, "phase selection")
X(pi_failed, Global, "pi failed")
X(pivot_bignums, Global, "pivot bignums")
X(pivot_bug, Global, "pivot bug")
X(pivot_shape, Global, "pivot shape")
X(pivot_stats, Global, "pivot stats")
X(plugin, Global, "plugin")
X(pob_queue, Global, "pob queue")
X(poly_bug, polynomial, "poly bug")
X(poly_rewriter, Global, "poly rewriter")
X(polynomial, Global, "polynomial")
X(polynomial_factorization, Global, "polynomial::factorization")
X(polynomial_factorization_bughunt, Global, "polynomial::factorization::bughunt")
X(polynomial_gcd, Global, "polynomial gcd")
X(polynomial_gcd_detail, Global, "polynomial gcd detail")
X(polynorm, polynorm, "polynorm")
X(pop, combined_solver, "pop")
X(pop_app_frame, parser, "pop app frame")
X(pop_scope, Global, "pop scope")
X(pop_scope_detail, Global, "pop scope detail")
X(pp_ast_dot_step, ast_pp_dot_st, "pp ast dot step")
X(pp_let, smt2_printer, "pp let")
X(pp_scope, smt2_printer, "pp scope")
X(pr_lemma_bug, Global, "pr lemma bug")
X(pr_unit_bug, Global, "pr unit bug")
X(probe, is_non_nira_functor, "probe")
X(probing, Global, "probing")
X(process_non_linear, Global, "process non linear")
X(proof_checker, Global, "proof checker")
X(proof_converter, Global, "proof converter")
X(proof_gen_bug, Global, "proof gen bug")
X(proof_utils, push_instantiations_up_cl, "proof utils")
X(propagate, Global, "propagate")
X(propagate_ineqs, Global, "propagate-ineqs")
X(propagate_atoms, Global, "propagate atoms")
X(propagate_bool_var_enode_bug, Global, "propagate bool var enode bug")
X(propagate_bounds, Global, "propagate bounds")
X(propagate_bounds_bug, Global, "propagate bounds bug")
X(propagate_bounds_detail, Global, "propagate bounds detail")
X(propagate_bug, Global, "propagate bug")
X(propagate_clause, Global, "propagate clause")
X(propagate_clause_bug, Global, "propagate clause bug")
X(propagate_monomial, Global, "propagate monomial")
X(propagate_nl_bound, Global, "propagate nl bound")
X(propagate_polynomial, Global, "propagate polynomial")
X(propagate_polynomial_bug, Global, "propagate polynomial bug")
X(propagate_polynomial_detail, Global, "propagate polynomial detail")
X(propagate_relevancy, Global, "propagate relevancy")
X(propagate_relevancy_to_args, relevancy_propagator_imp, "propagate relevancy to args")
X(propagate_relevant_ite, relevancy_propagator_imp, "propagate relevant ite")
X(propagate_values, expr_substitution_simplifier, "propagate values")
X(propagate_values_core, propagate_values_tactic, "propagate values core")
X(proto_model, Global, "proto model")
X(psc, Global, "psc")
X(psc_chain_classic, Global, "psc chain classic")
X(pseudo_remainder, Global, "pseudo remainder")
X(psolve, Global, "psolve")
X(psolve_verbose, Global, "psolve verbose")
X(pull_quant, Global, "pull quant")
X(purify_arith, purify_arith_proc, "purify arith")
X(push_app_ite, Global, "push app ite")
X(push_expr_frame, parser, "push expr frame")
X(push_ite, th_rewriter_cfg, "push ite")
X(push_new_th_diseqs, Global, "push new th diseqs")
X(q, mam_impl, "q")
X(q_detail, Global, "q detail")
X(qe, Global, "qe")
X(qe_assumptions, Global, "qe assumptions")
X(qe_block, qsat, "qe block")
X(qe_core, kernel, "qe core")
X(qe_lite, Global, "qe lite")
X(qe_verbose, Global, "qe verbose")
X(qi_cost, Global, "qi cost")
X(qi_queue, Global, "qi queue")
X(qi_queue_bug, Global, "qi queue bug")
X(qi_queue_detail, Global, "qi queue detail")
X(qi_queue_min_cost, Global, "qi queue min cost")
X(qi_queue_profile, Global, "qi queue profile")
X(qi_queue_profile_detail, Global, "qi queue profile detail")
X(qi_unsat, Global, "qi unsat")
X(quant_elim, bool_plugin, "quant elim")
X(quantifier, default_qm_plugin, "quantifier")
X(quasi_base_bug_detail, Global, "quasi base bug detail")
X(quasi_base_row2base_row, Global, "quasi base row2base row")
X(quasi_macros, Global, "quasi macros")
X(quick_checker, Global, "quick checker")
X(quick_checker_candidates, Global, "quick checker candidates")
X(quick_checker_canonizer, Global, "quick checker canonizer")
X(quick_checker_sizes, Global, "quick checker sizes")
X(random, Global, "random")
X(random_split, Global, "random split")
X(random_update, Global, "random update")
X(rat_mpq, Global, "rat mpq")
X(rational, Global, "rational")
X(rcf_TaQ, Global, "rcf TaQ")
X(rcf_algebraic, Global, "rcf algebraic")
X(rcf_algebraic_sign, Global, "rcf algebraic sign")
X(rcf_arith, Global, "rcf arith")
X(rcf_clean, Global, "rcf clean")
X(rcf_clean_bug, Global, "rcf clean bug")
X(rcf_count_signs, Global, "rcf count signs")
X(rcf_determine_sign_bug, Global, "rcf determine sign bug")
X(rcf_gcd, Global, "rcf gcd")
X(rcf_isolate, Global, "rcf isolate")
X(rcf_isolate_bug, Global, "rcf isolate bug")
X(rcf_prem, Global, "rcf prem")
X(rcf_rem, Global, "rcf rem")
X(rcf_sign_det, Global, "rcf sign det")
X(rcf_sturm_seq, Global, "rcf sturm seq")
X(rcf_transcendental, Global, "rcf transcendental")
X(rdl_bug, Global, "rdl bug")
X(re_info, Global, "re info")
X(reassert_units, Global, "reassert units")
X(recfun, Global, "recfun")
X(recognizer_conflict, Global, "recognizer conflict")
X(recover_01, imp, "recover 01")
X(reduce_app, Global, "reduce app")
X(reduce_args, reduce_args_simplifier, "reduce args")
X(reduce_quantifier, th_rewriter_cfg, "reduce quantifier")
X(reduce_quantifier_bug, Global, "reduce quantifier bug")
X(reduce_step_ll, Global, "reduce step ll")
X(ref, Global, "ref")
X(refine_epsilon, Global, "refine epsilon")
X(reinit_clauses, Global, "reinit clauses")
X(reinit_clauses_bug, Global, "reinit clauses bug")
X(relevancy, Global, "relevancy")
X(relevancy_bug, Global, "relevancy bug")
X(rem_bug, Global, "rem bug")
X(rename, Global, "rename")
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")
X(rewriter_bug, Global, "rewriter bug")
X(rewriter_cache_result, Global, "rewriter cache result")
X(rewriter_const, Global, "rewriter const")
X(rewriter_reuse, Global, "rewriter reuse")
X(rewriter_step, Global, "rewriter step")
X(rewriter_subst, Global, "rewriter subst")
X(rewriter_visit, Global, "rewriter visit")
X(root_core, Global, "root core")
X(row_bug, Global, "row bug")
X(sat, inc_sat_solver, "sat")
X(sat_assign, Global, "sat assign")
X(sat_assign_core, Global, "sat assign core")
X(sat_bug, Global, "sat bug")
X(sat_clause, Global, "sat clause")
X(sat_cleaner_bug, Global, "sat cleaner bug")
X(sat_cleaner_frozen, Global, "sat cleaner frozen")
X(sat_conflict, Global, "sat conflict")
X(sat_conflict_detail, Global, "sat conflict detail")
X(sat_decide, Global, "sat decide")
X(sat_dimacs, imp, "sat dimacs")
X(sat_drat, Global, "sat drat")
X(sat_frozen, Global, "sat frozen")
X(sat_gc, Global, "sat gc")
X(sat_lemma, Global, "sat lemma")
X(sat_mc, Global, "sat mc")
X(sat_mc_bug, Global, "sat mc bug")
X(sat_missed_prop, Global, "sat missed prop")
X(sat_mk_clause, Global, "sat mk clause")
X(sat_model_bug, Global, "sat model bug")
X(sat_model_converter, Global, "sat model converter")
X(sat_propagate, Global, "sat propagate")
X(sat_reinit, Global, "sat reinit")
X(sat_simplifier, Global, "sat simplifier")
X(sat_stats, sat_tactic, "sat stats")
X(sat_tactic, imp, "sat tactic")
X(sat_verbose, Global, "sat verbose")
X(sat_watched_bug, Global, "sat watched bug")
X(sat_xor, Global, "sat xor")
X(sats, Global, "sats")
X(save_elim, Global, "save elim")
X(save_value, Global, "save value")
X(scanner, Global, "scanner")
X(scc, Global, "scc")
X(scc_cycle, Global, "scc cycle")
X(scc_detail, Global, "scc detail")
X(scc_details, Global, "scc details")
X(search, Global, "search")
X(search_bug, Global, "search bug")
X(search_detail, Global, "search detail")
X(search_lite, Global, "search lite")
X(select_pivot, Global, "select pivot")
X(select_pivot_info, Global, "select pivot info")
X(select_small, Global, "select small")
X(select_var, select_var, "select var")
X(seq, Global, "seq")
X(seq_regex, Global, "seq regex")
X(seq_regex_brief, Global, "seq regex brief")
X(seq_regex_verbose, Global, "seq regex verbose")
X(seq_verbose, Global, "seq verbose")
X(set_conflict, Global, "set conflict")
X(set_not_learned_bug, Global, "set not learned bug")
X(setup, Global, "setup")
X(sf_array, Global, "sf array")
X(shallow_context_simplifier_bug, propagate_values_tactic, "shallow context simplifier bug")
X(shared, Global, "shared")
X(sign, Global, "sign")
X(sign_row_conflict, Global, "sign row conflict")
X(simp_counter, Global, "simp counter")
X(simple_check, Global, "simple check")
X(simple_checker, Global, "simple checker")
X(simple_checker_learned, Global, "simple checker learned")
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")
X(sine, Global, "sine")
X(sine_bug, Global, "sine bug")
X(skeleton, Global, "skeleton")
X(skid, parser, "skid")
X(skolemizer, skolemizer, "skolemizer")
X(sls, Global, "sls")
X(sls_eval, Global, "sls eval")
X(sls_model, sls_tactic, "sls model")
X(sls_opt, Global, "sls opt")
X(sls_score, Global, "sls score")
X(sls_top, Global, "sls top")
X(sls_verbose, Global, "sls verbose")
X(sls_whatif, Global, "sls whatif")
X(sls_whatif_failed, Global, "sls whatif failed")
X(small_object_allocator, Global, "small object allocator")
X(smaller_pattern_proc, Global, "smaller pattern proc")
X(smt2_pp, smt2_printer, "smt2 pp")
X(smt2parser, parser, "smt2parser")
X(smt_context, Global, "smt context")
X(smt_kernel, Global, "smt kernel")
X(smt_params, Global, "smt params")
X(smt_tactic, smt_tactic, "smt tactic")
X(smt_tactic_detail, smt_tactic, "smt tactic detail")
X(smt_tactic_memory, smt_tactic, "smt tactic memory")
X(smt_tactic_params, smt_tactic, "smt tactic params")
X(smtfd, solver, "smtfd")
X(smtfd_verbose, solver, "smtfd verbose")
X(solve_eqs, Global, "solve eqs")
X(solve_eqs_check_occs, Global, "solve eqs check occs")
X(solver, simplifier_solver, "solver")
X(solver2tactic, solver2tactic, "solver2tactic")
X(solver_na2as, Global, "solver na2as")
X(som, Global, "som")
X(sorted_sources, Global, "sorted sources")
X(spacer, conv_rewriter_cfg, "spacer")
X(spacer_farkas, Global, "spacer.farkas")
X(spacer_fkab, Global, "spacer.fkab")
X(spacer_ind_gen, pool_solver, "spacer.ind gen")
X(spacer_limnum, Global, "spacer.limnum")
X(spacer_mincut, Global, "spacer.mincut")
X(spacer_detail, Global, "spacer detail")
X(spacer_expand, Global, "spacer expand")
X(spacer_init_rule, Global, "spacer init rule")
X(spacer_mbp, Global, "spacer mbp")
X(spacer_normalize, Global, "spacer normalize")
X(spacer_normalize_order, Global, "spacer normalize order")
X(spacer_pdr, Global, "spacer pdr")
X(spacer_progress, Global, "spacer progress")
X(spacer_qgen, Global, "spacer qgen")
X(spacer_sat, Global, "spacer sat")
X(spacer_verbose, Global, "spacer verbose")
X(sparse_interpolator, Global, "sparse interpolator")
X(special_relations, Global, "special relations")
X(special_relations_verbose, Global, "special relations verbose")
X(specrel, Global, "specrel")
X(split_bug, imp, "split bug")
X(spol_bug, Global, "spol bug")
X(sqrt_bug, Global, "sqrt bug")
X(st, Global, "st")
X(st_bug, Global, "st bug")
X(state_graph, Global, "state graph")
X(str, Global, "str")
X(str_fl, Global, "str fl")
X(string_buffer, Global, "string buffer")
X(subpaving, Global, "subpaving")
X(subpaving_clause, Global, "subpaving clause")
X(subpaving_init, Global, "subpaving init")
X(subpaving_int_split, Global, "subpaving int split")
X(subpaving_is_int, Global, "subpaving is int")
X(subpaving_main, Global, "subpaving main")
X(subpaving_mk_bound, Global, "subpaving mk bound")
X(subpaving_mk_sum, Global, "subpaving mk sum")
X(subpaving_propagate, Global, "subpaving propagate")
X(subpaving_ref_count, Global, "subpaving ref count")
X(subpaving_relevant_bound, Global, "subpaving relevant bound")
X(subpaving_relevant_bound_bug, Global, "subpaving relevant bound bug")
X(subpaving_stats, Global, "subpaving stats")
X(subpaving_tactic, imp, "subpaving tactic")
X(subst_bug, Global, "subst bug")
X(subst_insert, Global, "subst insert")
X(subst_tree_bug, Global, "subst tree bug")
X(substitution, Global, "substitution")
X(substitution_tree_bug, Global, "substitution tree bug")
X(subsume, Global, "subsume")
X(subsume_verb, Global, "subsume verb")
X(subsumption, Global, "subsumption")
X(subsumption_bug, Global, "subsumption bug")
X(subsumption_resolution, Global, "subsumption resolution")
X(symmetry_reduce, imp, "symmetry reduce")
X(sync, parser, "sync")
X(t_fpa, Global, "t fpa")
X(t_fpa_detail, Global, "t fpa detail")
X(t_fpa_internalize, Global, "t fpa internalize")
X(t_str, Global, "t str")
X(t_str_binary_search, Global, "t str binary search")
X(t_str_detail, theory_str, "t str detail")
X(tactic, tactic2solver, "tactic")
X(tactic2solver, tactic2solver, "tactic2solver")
X(tan, Global, "tan")
X(tc, well_sorted_proc, "tc")
X(th_rewriter_step, th_rewriter_cfg, "th rewriter step")
X(theory_arith, Global, "theory arith")
X(theory_aware_branching, theory_aware_branching_queue, "theory aware branching")
X(theory_case_split, Global, "theory case split")
X(theory_dl, theory_dl, "theory dl")
X(to_patch_bug, Global, "to patch bug")
X(to_real_bug, Global, "to real bug")
X(to_var_bug, imp, "to var bug")
X(top_sort, eq_der, "top sort")
X(total_order, Global, "total order")
X(trigger_bug, mam_impl, "trigger bug")
X(triggers, Global, "triggers")
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")
X(unit_resolution, Global, "unit resolution")
X(unit_resolution_justification_bug, Global, "unit resolution justification bug")
X(unit_subsumption_tactic, unit_subsumption_tactic, "unit subsumption tactic")
X(unsat_core, Global, "unsat core")
X(unsat_core_bug, Global, "unsat core bug")
X(unsat_core_trail, Global, "unsat core trail")
X(unsupported, imp, "unsupported")
X(update_and_pivot_bug, Global, "update and pivot bug")
X(update_and_pivot_bug_detail, Global, "update and pivot bug detail")
X(update_quantifier_weight, Global, "update quantifier weight")
X(upolynomial, Global, "upolynomial")
X(user_propagate, Global, "user propagate")
X(using_params, using_params_tactical, "using params")
X(util_bug, Global, "util bug")
X(utvpi, Global, "utvpi")
X(valid_row_assignment, Global, "valid row assignment")
X(valid_row_assignment_bug, Global, "valid row assignment bug")
X(value_bug, Global, "value bug")
X(value_sweep, Global, "value sweep")
X(var2basic, Global, "var2basic")
X(var_subst, Global, "var subst")
X(var_subst_bug, Global, "var subst bug")
X(proof_virtual, Global, "proof_virtual")
X(visit_b_justification_bug, Global, "visit b justification bug")
X(watch_list, Global, "watch list")
X(wf_column, Global, "wf column")
X(ws, well_sorted_proc, "ws")
X(xor3, Global, "xor3")
X(xor3_sorted, Global, "xor3 sorted")
X(z3_replayer, Global, "z3 replayer")
X(z3_replayer_bug, Global, "z3 replayer bug")
X(z3_replayer_cmd, Global, "z3 replayer cmd")
X(z3_replayer_escape, Global, "z3 replayer escape")
X(coming_from_quant, Global, "coming from quant")