| .. | | 03-May-2022 | - |
| params/ | H | 03-May-2022 | - | 1,919 | 1,188 |
| proto_model/ | H | 03-May-2022 | - | 523 | 347 |
| tactic/ | H | 03-May-2022 | - | 884 | 638 |
| arith_eq_adapter.cpp | H A D | 20-Jan-2021 | 12.3 KiB | 285 | 199 |
| arith_eq_adapter.h | H A D | 20-Jan-2021 | 2.4 KiB | 91 | 45 |
| arith_eq_solver.cpp | H A D | 20-Jan-2021 | 17 KiB | 630 | 441 |
| arith_eq_solver.h | H A D | 20-Jan-2021 | 2.5 KiB | 107 | 44 |
| asserted_formulas.cpp | H A D | 20-Jan-2021 | 22.2 KiB | 724 | 625 |
| asserted_formulas.h | H A D | 20-Jan-2021 | 13.1 KiB | 287 | 230 |
| cached_var_subst.cpp | H A D | 20-Jan-2021 | 2.7 KiB | 95 | 60 |
| cached_var_subst.h | H A D | 20-Jan-2021 | 1.2 KiB | 52 | 29 |
| cost_evaluator.cpp | H A D | 20-Jan-2021 | 2.9 KiB | 101 | 76 |
| cost_evaluator.h | H A D | 20-Jan-2021 | 800 | 42 | 13 |
| database.h | H A D | 20-Jan-2021 | 9.5 KiB | 323 | 316 |
| database.smt | H A D | 20-Jan-2021 | 14.4 KiB | 315 | 260 |
| diff_logic.h | H A D | 20-Jan-2021 | 66.9 KiB | 1,904 | 1,554 |
| dyn_ack.cpp | H A D | 20-Jan-2021 | 22.1 KiB | 586 | 488 |
| dyn_ack.h | H A D | 20-Jan-2021 | 4.2 KiB | 136 | 78 |
| expr_context_simplifier.cpp | H A D | 20-Jan-2021 | 21.7 KiB | 736 | 602 |
| expr_context_simplifier.h | H A D | 20-Jan-2021 | 2.4 KiB | 82 | 53 |
| fingerprints.cpp | H A D | 20-Jan-2021 | 4.8 KiB | 151 | 114 |
| fingerprints.h | H A D | 20-Jan-2021 | 3.1 KiB | 91 | 61 |
| mam.cpp | H A D | 20-Jan-2021 | 164.6 KiB | 4,035 | 3,279 |
| mam.h | H A D | 20-Jan-2021 | 1.4 KiB | 75 | 33 |
| old_interval.cpp | H A D | 20-Jan-2021 | 23.6 KiB | 668 | 546 |
| old_interval.h | H A D | 20-Jan-2021 | 7 KiB | 132 | 102 |
| qi_queue.cpp | H A D | 20-Jan-2021 | 20.4 KiB | 490 | 419 |
| qi_queue.h | H A D | 20-Jan-2021 | 3.5 KiB | 103 | 72 |
| seq_axioms.cpp | H A D | 20-Jan-2021 | 31.2 KiB | 975 | 607 |
| seq_axioms.h | H A D | 20-Jan-2021 | 3.8 KiB | 105 | 71 |
| seq_eq_solver.cpp | H A D | 20-Jan-2021 | 50.6 KiB | 1,634 | 1,350 |
| seq_ne_solver.cpp | H A D | 20-Jan-2021 | 9.1 KiB | 321 | 273 |
| seq_offset_eq.cpp | H A D | 20-Jan-2021 | 3.6 KiB | 135 | 95 |
| seq_offset_eq.h | H A D | 20-Jan-2021 | 1.3 KiB | 56 | 27 |
| seq_regex.cpp | H A D | 20-Jan-2021 | 34.9 KiB | 933 | 576 |
| seq_regex.h | H A D | 20-Jan-2021 | 7.3 KiB | 213 | 77 |
| seq_skolem.cpp | H A D | 20-Jan-2021 | 6.4 KiB | 204 | 166 |
| seq_skolem.h | H A D | 20-Jan-2021 | 9.3 KiB | 162 | 124 |
| seq_unicode.cpp | H A D | 20-Jan-2021 | 5.5 KiB | 174 | 129 |
| seq_unicode.h | H A D | 20-Jan-2021 | 3 KiB | 116 | 68 |
| smt2_extra_cmds.cpp | H A D | 20-Jan-2021 | 1.4 KiB | 48 | 27 |
| smt2_extra_cmds.h | H A D | 20-Jan-2021 | 276 | 25 | 3 |
| smt_almost_cg_table.cpp | H A D | 20-Jan-2021 | 3.3 KiB | 128 | 97 |
| smt_almost_cg_table.h | H A D | 20-Jan-2021 | 1.7 KiB | 71 | 35 |
| smt_arith_value.cpp | H A D | 20-Jan-2021 | 6 KiB | 167 | 132 |
| smt_arith_value.h | H A D | 20-Jan-2021 | 1.3 KiB | 53 | 31 |
| smt_b_justification.h | H A D | 20-Jan-2021 | 2.7 KiB | 105 | 62 |
| smt_bool_var_data.h | H A D | 20-Jan-2021 | 3.8 KiB | 137 | 90 |
| smt_case_split_queue.cpp | H A D | 20-Jan-2021 | 44.9 KiB | 1,283 | 1,054 |
| smt_case_split_queue.h | H A D | 20-Jan-2021 | 1.4 KiB | 58 | 28 |
| smt_cg_table.cpp | H A D | 20-Jan-2021 | 7.7 KiB | 263 | 218 |
| smt_cg_table.h | H A D | 20-Jan-2021 | 6.9 KiB | 222 | 156 |
| smt_checker.cpp | H A D | 20-Jan-2021 | 6 KiB | 187 | 153 |
| smt_checker.h | H A D | 20-Jan-2021 | 1.2 KiB | 56 | 26 |
| smt_clause.cpp | H A D | 20-Jan-2021 | 4.6 KiB | 130 | 99 |
| smt_clause.h | H A D | 20-Jan-2021 | 8.9 KiB | 285 | 190 |
| smt_clause_proof.cpp | H A D | 20-Jan-2021 | 5.5 KiB | 175 | 142 |
| smt_clause_proof.h | H A D | 20-Jan-2021 | 2.1 KiB | 76 | 42 |
| smt_conflict_resolution.cpp | H A D | 20-Jan-2021 | 58.3 KiB | 1,490 | 1,181 |
| smt_conflict_resolution.h | H A D | 20-Jan-2021 | 9.5 KiB | 282 | 197 |
| smt_consequences.cpp | H A D | 20-Jan-2021 | 23.2 KiB | 670 | 584 |
| smt_context.cpp | H A D | 20-Jan-2021 | 182.6 KiB | 4,632 | 3,673 |
| smt_context.h | H A D | 20-Jan-2021 | 61.2 KiB | 1,807 | 1,121 |
| smt_context_inv.cpp | H A D | 20-Jan-2021 | 16.6 KiB | 425 | 357 |
| smt_context_pp.cpp | H A D | 20-Jan-2021 | 27.1 KiB | 748 | 661 |
| smt_context_stat.cpp | H A D | 20-Jan-2021 | 4.6 KiB | 149 | 115 |
| smt_enode.cpp | H A D | 20-Jan-2021 | 12.1 KiB | 376 | 285 |
| smt_enode.h | H A D | 20-Jan-2021 | 14.7 KiB | 462 | 298 |
| smt_eq_justification.h | H A D | 20-Jan-2021 | 2.3 KiB | 84 | 40 |
| smt_failure.h | H A D | 20-Jan-2021 | 652 | 39 | 13 |
| smt_farkas_util.cpp | H A D | 20-Jan-2021 | 10.4 KiB | 369 | 312 |
| smt_farkas_util.h | H A D | 20-Jan-2021 | 2.7 KiB | 96 | 40 |
| smt_for_each_relevant_expr.cpp | H A D | 20-Jan-2021 | 9 KiB | 299 | 245 |
| smt_for_each_relevant_expr.h | H A D | 20-Jan-2021 | 2.8 KiB | 113 | 58 |
| smt_implied_equalities.cpp | H A D | 20-Jan-2021 | 21.4 KiB | 583 | 412 |
| smt_implied_equalities.h | H A D | 20-Jan-2021 | 565 | 42 | 11 |
| smt_induction.cpp | H A D | 20-Jan-2021 | 17.5 KiB | 590 | 452 |
| smt_induction.h | H A D | 20-Jan-2021 | 4.8 KiB | 152 | 101 |
| smt_internalizer.cpp | H A D | 20-Jan-2021 | 67.7 KiB | 1,772 | 1,364 |
| smt_justification.cpp | H A D | 20-Jan-2021 | 14.8 KiB | 411 | 346 |
| smt_justification.h | H A D | 20-Jan-2021 | 14.5 KiB | 414 | 240 |
| smt_kernel.cpp | H A D | 20-Jan-2021 | 13.3 KiB | 481 | 351 |
| smt_kernel.h | H A D | 20-Jan-2021 | 8.8 KiB | 316 | 80 |
| smt_literal.cpp | H A D | 20-Jan-2021 | 3.3 KiB | 116 | 81 |
| smt_literal.h | H A D | 20-Jan-2021 | 3.1 KiB | 123 | 70 |
| smt_lookahead.cpp | H A D | 20-Jan-2021 | 5.2 KiB | 188 | 156 |
| smt_lookahead.h | H A D | 20-Jan-2021 | 648 | 46 | 16 |
| smt_model_checker.cpp | H A D | 20-Jan-2021 | 21 KiB | 568 | 442 |
| smt_model_checker.h | H A D | 20-Jan-2021 | 3.7 KiB | 110 | 70 |
| smt_model_finder.cpp | H A D | 20-Jan-2021 | 98.3 KiB | 2,541 | 1,986 |
| smt_model_finder.h | H A D | 20-Jan-2021 | 4.5 KiB | 128 | 63 |
| smt_model_generator.cpp | H A D | 20-Jan-2021 | 20.3 KiB | 511 | 420 |
| smt_model_generator.h | H A D | 20-Jan-2021 | 9.5 KiB | 245 | 124 |
| smt_parallel.cpp | H A D | 20-Jan-2021 | 8.6 KiB | 259 | 203 |
| smt_parallel.h | H A D | 20-Jan-2021 | 436 | 35 | 10 |
| smt_quantifier.cpp | H A D | 20-Jan-2021 | 30.6 KiB | 816 | 660 |
| smt_quantifier.h | H A D | 20-Jan-2021 | 5.7 KiB | 183 | 92 |
| smt_quantifier_instances.h | H A D | 20-Jan-2021 | 1.7 KiB | 65 | 35 |
| smt_quantifier_stat.cpp | H A D | 20-Jan-2021 | 3.7 KiB | 120 | 92 |
| smt_quantifier_stat.h | H A D | 20-Jan-2021 | 4.1 KiB | 155 | 102 |
| smt_quick_checker.cpp | H A D | 20-Jan-2021 | 15.9 KiB | 409 | 350 |
| smt_quick_checker.h | H A D | 20-Jan-2021 | 3.6 KiB | 104 | 62 |
| smt_relevancy.cpp | H A D | 20-Jan-2021 | 23.5 KiB | 678 | 565 |
| smt_relevancy.h | H A D | 20-Jan-2021 | 6 KiB | 204 | 67 |
| smt_setup.cpp | H A D | 20-Jan-2021 | 39.2 KiB | 1,061 | 911 |
| smt_setup.h | H A D | 20-Jan-2021 | 3.8 KiB | 126 | 86 |
| smt_solver.cpp | H A D | 20-Jan-2021 | 16.7 KiB | 503 | 409 |
| smt_solver.h | H A D | 20-Jan-2021 | 513 | 32 | 7 |
| smt_statistics.cpp | H A D | 20-Jan-2021 | 347 | 30 | 7 |
| smt_statistics.h | H A D | 20-Jan-2021 | 1.2 KiB | 61 | 34 |
| smt_theory.cpp | H A D | 20-Jan-2021 | 8 KiB | 256 | 213 |
| smt_theory.h | H A D | 20-Jan-2021 | 20 KiB | 617 | 290 |
| smt_types.h | H A D | 20-Jan-2021 | 1.5 KiB | 77 | 38 |
| smt_value_sort.cpp | H A D | 20-Jan-2021 | 1.7 KiB | 75 | 44 |
| smt_value_sort.h | H A D | 20-Jan-2021 | 402 | 36 | 6 |
| spanning_tree.h | H A D | 20-Jan-2021 | 2.3 KiB | 81 | 44 |
| spanning_tree_base.h | H A D | 20-Jan-2021 | 1.2 KiB | 52 | 26 |
| spanning_tree_def.h | H A D | 20-Jan-2021 | 15.6 KiB | 488 | 341 |
| theory_arith.cpp | H A D | 20-Jan-2021 | 467 | 31 | 6 |
| theory_arith.h | H A D | 20-Jan-2021 | 58.6 KiB | 1,291 | 949 |
| theory_arith_aux.h | H A D | 20-Jan-2021 | 84.5 KiB | 2,293 | 1,780 |
| theory_arith_core.h | H A D | 20-Jan-2021 | 136.7 KiB | 3,560 | 2,811 |
| theory_arith_def.h | H A D | 20-Jan-2021 | 473 | 31 | 9 |
| theory_arith_eq.h | H A D | 20-Jan-2021 | 13 KiB | 361 | 250 |
| theory_arith_int.h | H A D | 20-Jan-2021 | 44 KiB | 1,134 | 913 |
| theory_arith_inv.h | H A D | 20-Jan-2021 | 7.9 KiB | 235 | 174 |
| theory_arith_nl.h | H A D | 20-Jan-2021 | 84.1 KiB | 2,400 | 1,789 |
| theory_arith_pp.h | H A D | 20-Jan-2021 | 19.2 KiB | 563 | 510 |
| theory_array.cpp | H A D | 20-Jan-2021 | 16.5 KiB | 475 | 394 |
| theory_array.h | H A D | 20-Jan-2021 | 4.3 KiB | 118 | 78 |
| theory_array_bapa.cpp | H A D | 20-Jan-2021 | 23.5 KiB | 645 | 486 |
| theory_array_bapa.h | H A D | 20-Jan-2021 | 702 | 44 | 18 |
| theory_array_base.cpp | H A D | 20-Jan-2021 | 39.2 KiB | 1,054 | 862 |
| theory_array_base.h | H A D | 20-Jan-2021 | 8.8 KiB | 217 | 137 |
| theory_array_full.cpp | H A D | 20-Jan-2021 | 29.7 KiB | 834 | 687 |
| theory_array_full.h | H A D | 20-Jan-2021 | 3.4 KiB | 111 | 63 |
| theory_bv.cpp | H A D | 20-Jan-2021 | 77.5 KiB | 1,897 | 1,600 |
| theory_bv.h | H A D | 20-Jan-2021 | 12.3 KiB | 292 | 225 |
| theory_datatype.cpp | H A D | 20-Jan-2021 | 40.4 KiB | 1,011 | 804 |
| theory_datatype.h | H A D | 20-Jan-2021 | 5.7 KiB | 151 | 108 |
| theory_dense_diff_logic.cpp | H A D | 20-Jan-2021 | 473 | 27 | 7 |
| theory_dense_diff_logic.h | H A D | 20-Jan-2021 | 10.4 KiB | 299 | 202 |
| theory_dense_diff_logic_def.h | H A D | 20-Jan-2021 | 43.3 KiB | 1,134 | 967 |
| theory_diff_logic.cpp | H A D | 20-Jan-2021 | 675 | 40 | 14 |
| theory_diff_logic.h | H A D | 20-Jan-2021 | 13 KiB | 421 | 267 |
| theory_diff_logic_def.h | H A D | 20-Jan-2021 | 44.1 KiB | 1,472 | 1,252 |
| theory_dl.cpp | H A D | 20-Jan-2021 | 9.4 KiB | 294 | 221 |
| theory_dl.h | H A D | 20-Jan-2021 | 290 | 29 | 4 |
| theory_dummy.cpp | H A D | 20-Jan-2021 | 1.4 KiB | 74 | 42 |
| theory_dummy.h | H A D | 20-Jan-2021 | 1.4 KiB | 58 | 26 |
| theory_fpa.cpp | H A D | 20-Jan-2021 | 24.1 KiB | 678 | 529 |
| theory_fpa.h | H A D | 20-Jan-2021 | 4.1 KiB | 136 | 90 |
| theory_lra.cpp | H A D | 20-Jan-2021 | 141.1 KiB | 3,899 | 3,373 |
| theory_lra.h | H A D | 20-Jan-2021 | 2.7 KiB | 108 | 52 |
| theory_opt.cpp | H A D | 20-Jan-2021 | 1.8 KiB | 78 | 52 |
| theory_opt.h | H A D | 20-Jan-2021 | 795 | 40 | 16 |
| theory_pb.cpp | H A D | 20-Jan-2021 | 77 KiB | 2,400 | 1,990 |
| theory_pb.h | H A D | 20-Jan-2021 | 15.7 KiB | 435 | 302 |
| theory_recfun.cpp | H A D | 20-Jan-2021 | 17.2 KiB | 533 | 412 |
| theory_recfun.h | H A D | 20-Jan-2021 | 6.3 KiB | 170 | 124 |
| theory_seq.cpp | H A D | 20-Jan-2021 | 100.6 KiB | 3,317 | 2,878 |
| theory_seq.h | H A D | 20-Jan-2021 | 28.9 KiB | 640 | 536 |
| theory_seq_empty.h | H A D | 20-Jan-2021 | 1.4 KiB | 49 | 23 |
| theory_special_relations.cpp | H A D | 20-Jan-2021 | 42 KiB | 1,152 | 950 |
| theory_special_relations.h | H A D | 20-Jan-2021 | 7.8 KiB | 206 | 159 |
| theory_str.cpp | H A D | 20-Jan-2021 | 404.3 KiB | 9,305 | 7,261 |
| theory_str.h | H A D | 20-Jan-2021 | 32.1 KiB | 835 | 604 |
| theory_str_mc.cpp | H A D | 20-Jan-2021 | 65.9 KiB | 1,451 | 1,191 |
| theory_str_regex.cpp | H A D | 20-Jan-2021 | 77.8 KiB | 1,563 | 1,253 |
| theory_utvpi.cpp | H A D | 20-Jan-2021 | 4.4 KiB | 156 | 123 |
| theory_utvpi.h | H A D | 20-Jan-2021 | 10.5 KiB | 367 | 231 |
| theory_utvpi_def.h | H A D | 20-Jan-2021 | 32.2 KiB | 976 | 773 |
| theory_wmaxsat.cpp | H A D | 20-Jan-2021 | 11.9 KiB | 367 | 304 |
| theory_wmaxsat.h | H A D | 20-Jan-2021 | 4.8 KiB | 142 | 104 |
| user_propagator.cpp | H A D | 20-Jan-2021 | 4.5 KiB | 155 | 119 |
| user_propagator.h | H A D | 20-Jan-2021 | 4.5 KiB | 127 | 86 |
| uses_theory.cpp | H A D | 20-Jan-2021 | 865 | 49 | 26 |
| uses_theory.h | H A D | 20-Jan-2021 | 643 | 36 | 4 |
| watch_list.cpp | H A D | 20-Jan-2021 | 4 KiB | 132 | 100 |
| watch_list.h | H A D | 20-Jan-2021 | 5.6 KiB | 199 | 127 |