410   fprintf(f, "boolean variables       : %"PRIu32"\n", core->nvars);  in print_presearch_stats()
411   fprintf(f, "atoms                   : %"PRIu32"\n", core->atoms.natoms);  in print_presearch_stats()
413     fprintf(f, "egraph terms            : %"PRIu32"\n", egraph->terms.nterms);  in print_presearch_stats()
414     fprintf(f, "app/update reductions   : %"PRIu32"\n", egraph->stats.app_reductions);  in print_presearch_stats()
479         fprintf(f, " --simplex-prop --prop-threshold=%"PRIu32, params.max_prop_row_size);  in print_options()
485       fprintf(f, " --bland-threshold=%"PRIu32, params.bland_threshold);  in print_options()
497         fprintf(f, " --dyn-ack --max-ack=%"PRIu32" --dyn-ack-threshold=%"PRIu32,  in print_options()
501         fprintf(f, " --dyn-bool-ack --max-bool-ack=%"PRIu32" --dyn-bool-ack-threshold=%"PRIu32,  in print_options()
504 …fprintf(f, " --aux-eq-quota=%"PRIu32" --aux-eq-ratio=%.3f\n", params.aux_eq_quota, params.aux_eq_r…  in print_options()
506     fprintf(f, " --max-interface-eqs=%"PRIu32"\n", params.max_interface_eqs);  in print_options()
510     fprintf(f, "Array solver: --max-update-conflicts=%"PRIu32" --max-extensionality=%"PRIu32"\n",  in print_options()
520       fprintf(f, " --cache-tclauses --tclause-size=%"PRIu32, params.tclause_size);  in print_options()
561   fprintf(stderr, " restarts                : %"PRIu32"\n", stat->restarts);  in show_stats()
562   fprintf(stderr, " simplify db             : %"PRIu32"\n", stat->simplify_calls);  in show_stats()
563   fprintf(stderr, " reduce db               : %"PRIu32"\n", stat->reduce_calls);  in show_stats()
568   fprintf(stderr, " theory propagations     : %"PRIu32"\n", stat->th_props);  in show_stats()
569   fprintf(stderr, " propagation-lemmas      : %"PRIu32"\n", stat->th_prop_lemmas);  in show_stats()
570   fprintf(stderr, " theory conflicts        : %"PRIu32"\n", stat->th_conflicts);  in show_stats()
571   fprintf(stderr, " conflict-lemmas         : %"PRIu32"\n", stat->th_conflict_lemmas);  in show_stats()
588   fprintf(stderr, " eq from simplex         : %"PRIu32"\n", stat->eq_props);  in show_egraph_stats()
589   fprintf(stderr, " prop. to core           : %"PRIu32"\n", stat->th_props);  in show_egraph_stats()
590   fprintf(stderr, " conflicts               : %"PRIu32"\n", stat->th_conflicts);  in show_egraph_stats()
591   fprintf(stderr, " non-distinct lemmas     : %"PRIu32"\n", stat->nd_lemmas);  in show_egraph_stats()
592   fprintf(stderr, " auxiliary eqs. created  : %"PRIu32"\n", stat->aux_eqs);  in show_egraph_stats()
593   fprintf(stderr, " dyn boolack. lemmas     : %"PRIu32"\n", stat->boolack_lemmas);  in show_egraph_stats()
594   fprintf(stderr, " other dyn ack.lemmas    : %"PRIu32"\n", stat->ack_lemmas);  in show_egraph_stats()
595   fprintf(stderr, " final checks            : %"PRIu32"\n", stat->final_checks);  in show_egraph_stats()
596   fprintf(stderr, " interface equalities    : %"PRIu32"\n", stat->interface_eqs);  in show_egraph_stats()
605   fprintf(stderr, " init. variables         : %"PRIu32"\n", stat->num_init_vars);  in show_funsolver_stats()
606   fprintf(stderr, " init. edges             : %"PRIu32"\n", stat->num_init_edges);  in show_funsolver_stats()
607   fprintf(stderr, " update axiom1           : %"PRIu32"\n", stat->num_update_axiom1);  in show_funsolver_stats()
608   fprintf(stderr, " update axiom2           : %"PRIu32"\n", stat->num_update_axiom2);  in show_funsolver_stats()
609   fprintf(stderr, " extensionality axioms   : %"PRIu32"\n", stat->num_extensionality_axiom);  in show_funsolver_stats()
618   fprintf(stderr, " init. variables         : %"PRIu32"\n", stat->num_init_vars);  in show_simplex_stats()
619   fprintf(stderr, " init. rows              : %"PRIu32"\n", stat->num_init_rows);  in show_simplex_stats()
620   fprintf(stderr, " init. atoms             : %"PRIu32"\n", stat->num_atoms);  in show_simplex_stats()
621   fprintf(stderr, " end atoms               : %"PRIu32"\n", stat->num_end_atoms);  in show_simplex_stats()
622   fprintf(stderr, " elim. candidates        : %"PRIu32"\n", stat->num_elim_candidates);  in show_simplex_stats()
623   fprintf(stderr, " elim. rows              : %"PRIu32"\n", stat->num_elim_rows);  in show_simplex_stats()
624   fprintf(stderr, " fixed vars after simpl. : %"PRIu32"\n", stat->num_simpl_fvars);  in show_simplex_stats()
625   fprintf(stderr, " rows after simpl.       : %"PRIu32"\n", stat->num_simpl_rows);  in show_simplex_stats()
626   fprintf(stderr, " fixed vars              : %"PRIu32"\n", stat->num_fixed_vars);  in show_simplex_stats()
627   fprintf(stderr, " rows in init. tableau   : %"PRIu32"\n", stat->num_rows);  in show_simplex_stats()
628   fprintf(stderr, " rows in final tableau   : %"PRIu32"\n", stat->num_end_rows);  in show_simplex_stats()
629   fprintf(stderr, " calls to make_feasible  : %"PRIu32"\n", stat->num_make_feasible);  in show_simplex_stats()
630   fprintf(stderr, " pivots                  : %"PRIu32"\n", stat->num_pivots);  in show_simplex_stats()
631   fprintf(stderr, " bland-rule activations  : %"PRIu32"\n", stat->num_blands);  in show_simplex_stats()
632   fprintf(stderr, " simple lemmas           : %"PRIu32"\n", stat->num_binary_lemmas);  in show_simplex_stats()
633   fprintf(stderr, " prop. to core           : %"PRIu32"\n", stat->num_props);  in show_simplex_stats()
634   fprintf(stderr, " derived bounds          : %"PRIu32"\n", stat->num_bound_props);  in show_simplex_stats()
635   fprintf(stderr, " productive propagations : %"PRIu32"\n", stat->num_prop_expl);  in show_simplex_stats()
636   fprintf(stderr, " conflicts               : %"PRIu32"\n", stat->num_conflicts);  in show_simplex_stats()
637   fprintf(stderr, " interface lemmas        : %"PRIu32"\n", stat->num_interface_lemmas);  in show_simplex_stats()
638   fprintf(stderr, " reduced inter. lemmas   : %"PRIu32"\n", stat->num_reduced_inter_lemmas);  in show_simplex_stats()
639   fprintf(stderr, " trichotomy lemmas       : %"PRIu32"\n", stat->num_tricho_lemmas);  in show_simplex_stats()
640   fprintf(stderr, " reduced tricho. lemmas  : %"PRIu32"\n", stat->num_reduced_tricho);  in show_simplex_stats()
643     fprintf(stderr, " make integer feasible   : %"PRIu32"\n", stat->num_make_intfeasible);  in show_simplex_stats()
644     fprintf(stderr, " branch atoms            : %"PRIu32"\n", stat->num_branch_atoms);  in show_simplex_stats()
645     fprintf(stderr, " Gomory cuts             : %"PRIu32"\n", stat->num_gomory_cuts);  in show_simplex_stats()
647     fprintf(stderr, " conflicts               : %"PRIu32"\n", stat->num_bound_conflicts);  in show_simplex_stats()
648     fprintf(stderr, " recheck conflicts       : %"PRIu32"\n", stat->num_bound_recheck_conflicts);  in show_simplex_stats()
650     fprintf(stderr, " conflicts               : %"PRIu32"\n", stat->num_itest_conflicts);  in show_simplex_stats()
651     fprintf(stderr, " bound conflicts         : %"PRIu32"\n", stat->num_itest_bound_conflicts);  in show_simplex_stats()
652     fprintf(stderr, " recheck conflicts       : %"PRIu32"\n", stat->num_itest_recheck_conflicts);  in show_simplex_stats()
654     fprintf(stderr, " gcd conflicts           : %"PRIu32"\n", stat->num_dioph_gcd_conflicts);  in show_simplex_stats()
655     fprintf(stderr, " dioph checks            : %"PRIu32"\n", stat->num_dioph_checks);  in show_simplex_stats()
656     fprintf(stderr, " dioph conflicts         : %"PRIu32"\n", stat->num_dioph_conflicts);  in show_simplex_stats()
657     fprintf(stderr, " bound conflicts         : %"PRIu32"\n", stat->num_dioph_bound_conflicts);  in show_simplex_stats()
658     fprintf(stderr, " recheck conflicts       : %"PRIu32"\n", stat->num_dioph_recheck_conflicts);  in show_simplex_stats()
668   fprintf(stderr, " variables               : %"PRIu32"\n", bv_solver_num_vars(solver));  in show_bvsolver_stats()
669   fprintf(stderr, " atoms                   : %"PRIu32"\n", bv_solver_num_atoms(solver));  in show_bvsolver_stats()
670   fprintf(stderr, " eq. atoms               : %"PRIu32"\n", bv_solver_num_eq_atoms(solver));  in show_bvsolver_stats()
671   fprintf(stderr, " dyn eq. atoms           : %"PRIu32"\n", solver->stats.on_the_fly_atoms);  in show_bvsolver_stats()
672   fprintf(stderr, " ge atoms                : %"PRIu32"\n", bv_solver_num_ge_atoms(solver));  in show_bvsolver_stats()
673   fprintf(stderr, " sge atoms               : %"PRIu32"\n", bv_solver_num_sge_atoms(solver));  in show_bvsolver_stats()
674   fprintf(stderr, " equiv lemmas            : %"PRIu32"\n", solver->stats.equiv_lemmas);  in show_bvsolver_stats()
675   fprintf(stderr, " equiv conflictss        : %"PRIu32"\n", solver->stats.equiv_conflicts);  in show_bvsolver_stats()
676   fprintf(stderr, " semi-equiv lemmas       : %"PRIu32"\n", solver->stats.half_equiv_lemmas);  in show_bvsolver_stats()
677   fprintf(stderr, " interface lemmas        : %"PRIu32"\n", solver->stats.interface_lemmas);  in show_bvsolver_stats()
702     fprintf(stderr, " boolean variables       : %"PRIu32"\n", core->nvars);  in print_results()
703     fprintf(stderr, " atoms                   : %"PRIu32"\n", core->atoms.natoms);  in print_results()
708       fprintf(stderr, " egraph terms            : %"PRIu32"\n", egraph->terms.nterms);  in print_results()
709       fprintf(stderr, " egraph eq_quota         : %"PRIu32"\n", egraph->aux_eq_quota);  in print_results()
824       fprintf(f, "\n==== Assertion[%"PRIu32"] ====\n", i);  in check_model()