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