GCC Code Coverage Report
Directory: . Exec Total Coverage
Date: 2021-03-21 Lines: 147283 206053 71.5 %
Legend: low: < 75.0 % medium: >= 75.0 % high: >= 90.0 % Branches: 276147 785061 35.2 %

File Lines Branches
build-coverage/src/expr/kind.cpp
55.7 % 390 / 700 54.8 % 376 / 686
build-coverage/src/expr/kind.h
100.0 % 4 / 4 100.0 % 0 / 0
build-coverage/src/expr/metakind.cpp
74.2 % 575 / 775 44.3 % 357 / 805
build-coverage/src/expr/metakind.h
100.0 % 12 / 12 10.0 % 462 / 4600
build-coverage/src/expr/type_checker.cpp
89.1 % 831 / 933 51.0 % 1123 / 2204
build-coverage/src/expr/type_properties.h
36.2 % 38 / 105 19.4 % 49 / 253
build-coverage/src/options/arith_options.cpp
28.1 % 124 / 442 5.5 % 6 / 109
build-coverage/src/options/arith_options.h
69.6 % 117 / 168 100.0 % 0 / 0
build-coverage/src/options/arrays_options.cpp
35.9 % 23 / 64 50.0 % 2 / 4
build-coverage/src/options/arrays_options.h
84.6 % 22 / 26 100.0 % 0 / 0
build-coverage/src/options/base_options.cpp
60.7 % 51 / 84 50.0 % 2 / 4
build-coverage/src/options/base_options.h
62.8 % 27 / 43 100.0 % 0 / 0
build-coverage/src/options/booleans_options.cpp
100.0 % 1 / 1 50.0 % 2 / 4
build-coverage/src/options/builtin_options.cpp
100.0 % 1 / 1 50.0 % 2 / 4
build-coverage/src/options/bv_options.cpp
36.0 % 99 / 275 21.0 % 21 / 100
build-coverage/src/options/bv_options.h
62.2 % 74 / 119 100.0 % 0 / 0
build-coverage/src/options/datatypes_options.cpp
39.8 % 49 / 123 14.7 % 5 / 34
build-coverage/src/options/datatypes_options.h
100.0 % 43 / 43 100.0 % 0 / 0
build-coverage/src/options/decision_options.cpp
25.6 % 23 / 90 10.9 % 6 / 55
build-coverage/src/options/decision_options.h
80.0 % 16 / 20 100.0 % 0 / 0
build-coverage/src/options/expr_options.cpp
84.6 % 11 / 13 50.0 % 2 / 4
build-coverage/src/options/expr_options.h
100.0 % 10 / 10 100.0 % 0 / 0
build-coverage/src/options/fp_options.cpp
37.5 % 3 / 8 50.0 % 2 / 4
build-coverage/src/options/fp_options.h
100.0 % 2 / 2 100.0 % 0 / 0
build-coverage/src/options/main_options.cpp
66.7 % 24 / 36 50.0 % 2 / 4
build-coverage/src/options/main_options.h
12.5 % 2 / 16 100.0 % 0 / 0
build-coverage/src/options/options.cpp
32.0 % 2926 / 9150 11.0 % 3193 / 28919
build-coverage/src/options/options_holder.h
100.0 % 1 / 1 50.0 % 6 / 12
build-coverage/src/options/parser_options.cpp
52.0 % 13 / 25 50.0 % 2 / 4
build-coverage/src/options/parser_options.h
0.0 % 0 / 12 100.0 % 0 / 0
build-coverage/src/options/printer_options.cpp
12.5 % 10 / 80 6.5 % 3 / 46
build-coverage/src/options/printer_options.h
60.0 % 6 / 10 100.0 % 0 / 0
build-coverage/src/options/proof_options.cpp
14.3 % 12 / 84 3.8 % 2 / 52
build-coverage/src/options/proof_options.h
84.6 % 11 / 13 100.0 % 0 / 0
build-coverage/src/options/prop_options.cpp
49.0 % 24 / 49 50.0 % 2 / 4
build-coverage/src/options/prop_options.h
100.0 % 23 / 23 100.0 % 0 / 0
build-coverage/src/options/quantifiers_options.cpp
32.0 % 608 / 1900 5.6 % 39 / 691
build-coverage/src/options/quantifiers_options.h
91.9 % 547 / 595 100.0 % 0 / 0
build-coverage/src/options/sep_options.cpp
44.0 % 11 / 25 50.0 % 2 / 4
build-coverage/src/options/sep_options.h
83.3 % 10 / 12 100.0 % 0 / 0
build-coverage/src/options/sets_options.cpp
53.8 % 7 / 13 50.0 % 2 / 4
build-coverage/src/options/sets_options.h
100.0 % 6 / 6 100.0 % 0 / 0
build-coverage/src/options/smt_options.cpp
42.6 % 276 / 648 16.1 % 34 / 211
build-coverage/src/options/smt_options.h
71.6 % 166 / 232 100.0 % 0 / 0
build-coverage/src/options/strings_options.cpp
26.8 % 48 / 179 3.3 % 2 / 61
build-coverage/src/options/strings_options.h
95.9 % 47 / 49 100.0 % 0 / 0
build-coverage/src/options/theory_options.cpp
30.2 % 29 / 96 4.9 % 3 / 61
build-coverage/src/options/theory_options.h
100.0 % 25 / 25 100.0 % 0 / 0
build-coverage/src/options/uf_options.cpp
35.5 % 27 / 76 14.3 % 4 / 28
build-coverage/src/options/uf_options.h
84.6 % 22 / 26 100.0 % 0 / 0
build-coverage/src/parser/cvc/CvcLexer.c
45.9 % 3408 / 7418 37.2 % 1055 / 2838
build-coverage/src/parser/cvc/CvcParser.c
33.6 % 4663 / 13874 29.1 % 3819 / 13139
build-coverage/src/parser/smt2/Smt2Lexer.c
71.8 % 1866 / 2598 58.8 % 899 / 1530
build-coverage/src/parser/smt2/Smt2Parser.c
72.0 % 3205 / 4453 44.8 % 2464 / 5503
build-coverage/src/parser/tptp/TptpLexer.c
77.0 % 1415 / 1837 55.4 % 521 / 941
build-coverage/src/parser/tptp/TptpParser.c
63.5 % 3074 / 4839 42.5 % 2040 / 4805
build-coverage/src/theory/rewriter_tables.h
60.7 % 68 / 112 39.9 % 142 / 356
build-coverage/src/theory/theory_traits.h
97.6 % 41 / 42 65.0 % 13 / 20
build-coverage/src/theory/type_enumerator.cpp
83.8 % 31 / 37 40.4 % 42 / 104
build-coverage/src/util/floatingpoint_literal_symfpu.h
100.0 % 13 / 13 50.0 % 4 / 8
deps/install/include/cryptominisat5/solvertypesmini.h
40.0 % 6 / 15 100.0 % 0 / 0
deps/install/include/symfpu/core/add.h
98.4 % 120 / 122 61.4 % 350 / 570
deps/install/include/symfpu/core/classify.h
100.0 % 21 / 21 59.4 % 38 / 64
deps/install/include/symfpu/core/compare.h
95.4 % 62 / 65 63.9 % 228 / 357
deps/install/include/symfpu/core/convert.h
36.8 % 46 / 125 20.0 % 74 / 370
deps/install/include/symfpu/core/divide.h
100.0 % 43 / 43 61.3 % 100 / 163
deps/install/include/symfpu/core/fma.h
0.0 % 0 / 24 0.0 % 0 / 70
deps/install/include/symfpu/core/ite.h
100.0 % 2 / 2 100.0 % 0 / 0
deps/install/include/symfpu/core/multiply.h
100.0 % 33 / 33 62.9 % 66 / 105
deps/install/include/symfpu/core/operations.h
97.3 % 182 / 187 48.6 % 329 / 677
deps/install/include/symfpu/core/packing.h
100.0 % 58 / 58 62.6 % 129 / 206
deps/install/include/symfpu/core/remainder.h
100.0 % 54 / 54 59.0 % 102 / 173
deps/install/include/symfpu/core/rounder.h
90.5 % 133 / 147 53.0 % 377 / 711
deps/install/include/symfpu/core/sign.h
100.0 % 10 / 10 55.6 % 10 / 18
deps/install/include/symfpu/core/sqrt.h
100.0 % 35 / 35 42.5 % 65 / 153
deps/install/include/symfpu/core/unpackedFloat.h
100.0 % 133 / 133 54.6 % 247 / 452
deps/install/include/symfpu/utils/common.h
100.0 % 23 / 23 80.0 % 8 / 10
src/api/cvc4cpp.cpp
78.5 % 2217 / 2825 28.8 % 6463 / 22465
src/api/cvc4cpp.h
72.2 % 13 / 18 50.0 % 1 / 2
src/base/check.cpp
67.6 % 48 / 71 43.9 % 29 / 66
src/base/check.h
100.0 % 3 / 3 100.0 % 0 / 0
src/base/configuration.cpp
72.0 % 118 / 164 35.1 % 113 / 322
src/base/exception.cpp
72.8 % 59 / 81 36.2 % 42 / 116
src/base/exception.h
94.1 % 32 / 34 44.4 % 16 / 36
src/base/listener.cpp
100.0 % 2 / 2 100.0 % 0 / 0
src/base/map_util.h
100.0 % 16 / 16 40.7 % 74 / 182
src/base/modal_exception.h
66.7 % 6 / 9 100.0 % 0 / 0
src/base/output.cpp
100.0 % 13 / 13 50.0 % 3 / 6
src/base/output.h
81.3 % 104 / 128 16.0 % 141 / 884
src/context/backtrackable.h
4.9 % 2 / 41 1.2 % 1 / 84
src/context/cdhashmap.h
97.7 % 125 / 128 37.5 % 489 / 1304
src/context/cdhashset.h
88.1 % 37 / 42 9.1 % 4 / 44
src/context/cdinsert_hashmap.h
100.0 % 104 / 104 32.5 % 214 / 658
src/context/cdlist.h
95.3 % 123 / 129 36.7 % 878 / 2390
src/context/cdlist_forward.h
100.0 % 1 / 1 100.0 % 0 / 0
src/context/cdmaybe.h
100.0 % 22 / 22 20.0 % 12 / 60
src/context/cdo.h
100.0 % 33 / 33 36.4 % 64 / 176
src/context/cdqueue.h
100.0 % 48 / 48 21.6 % 113 / 524
src/context/cdtrail_queue.h
100.0 % 23 / 23 17.5 % 7 / 40
src/context/context.cpp
85.9 % 170 / 198 36.1 % 210 / 582
src/context/context.h
85.7 % 54 / 63 34.1 % 28 / 82
src/context/context_mm.cpp
93.5 % 58 / 62 36.0 % 36 / 100
src/decision/decision_engine.cpp
95.2 % 40 / 42 35.1 % 54 / 154
src/decision/decision_engine.h
100.0 % 30 / 30 24.4 % 22 / 90
src/decision/decision_strategy.h
100.0 % 8 / 8 100.0 % 0 / 0
src/decision/justification_heuristic.cpp
72.8 % 278 / 382 32.2 % 485 / 1507
src/decision/justification_heuristic.h
0.0 % 0 / 3 0.0 % 0 / 6
src/expr/array_store_all.cpp
53.7 % 22 / 41 44.3 % 47 / 106
src/expr/ascription_type.cpp
57.9 % 11 / 19 31.8 % 7 / 22
src/expr/attribute.cpp
37.7 % 23 / 61 4.5 % 4 / 88
src/expr/attribute.h
76.0 % 95 / 125 46.7 % 567 / 1213
src/expr/attribute_internals.h
100.0 % 68 / 68 31.5 % 58 / 184
src/expr/attribute_unique_id.h
0.0 % 0 / 5 100.0 % 0 / 0
src/expr/bound_var_manager.cpp
70.6 % 12 / 17 32.1 % 9 / 28
src/expr/bound_var_manager.h
100.0 % 9 / 9 39.5 % 30 / 76
src/expr/buffered_proof_generator.cpp
67.6 % 23 / 34 28.7 % 39 / 136
src/expr/buffered_proof_generator.h
100.0 % 2 / 2 50.0 % 1 / 2
src/expr/datatype_index.cpp
66.7 % 4 / 6 50.0 % 4 / 8
src/expr/datatype_index.h
100.0 % 3 / 3 100.0 % 0 / 0
src/expr/dtype.cpp
87.4 % 423 / 484 35.4 % 732 / 2066
src/expr/dtype.h
50.0 % 1 / 2 45.7 % 16 / 35
src/expr/dtype_cons.cpp
92.0 % 311 / 338 37.0 % 493 / 1332
src/expr/dtype_cons.h
100.0 % 2 / 2 50.0 % 8 / 16
src/expr/dtype_selector.cpp
81.8 % 27 / 33 24.5 % 27 / 110
src/expr/dtype_selector.h
100.0 % 1 / 1 50.0 % 2 / 4
src/expr/emptybag.cpp
42.9 % 9 / 21 43.8 % 7 / 16
src/expr/emptyset.cpp
42.9 % 9 / 21 43.8 % 7 / 16
src/expr/expr_iomanip.cpp
81.5 % 44 / 54 54.2 % 13 / 24
src/expr/kind_map.h
100.0 % 8 / 8 66.7 % 4 / 6
src/expr/lazy_proof.cpp
96.9 % 94 / 97 48.0 % 169 / 352
src/expr/lazy_proof_chain.cpp
74.8 % 113 / 151 32.2 % 167 / 518
src/expr/match_trie.cpp
94.4 % 102 / 108 48.5 % 158 / 326
src/expr/match_trie.h
100.0 % 3 / 3 50.0 % 1 / 2
src/expr/node.cpp
82.6 % 38 / 46 50.9 % 115 / 226
src/expr/node.h
82.2 % 296 / 360 22.0 % 754 / 3434
src/expr/node_algorithm.cpp
89.4 % 321 / 359 50.8 % 517 / 1018
src/expr/node_builder.h
83.4 % 307 / 368 12.1 % 761 / 6309
src/expr/node_manager.cpp
82.8 % 486 / 587 35.2 % 649 / 1844
src/expr/node_manager.h
88.0 % 184 / 209 26.3 % 567 / 2154
src/expr/node_self_iterator.h
93.0 % 40 / 43 24.5 % 23 / 94
src/expr/node_traversal.cpp
100.0 % 60 / 60 50.5 % 53 / 105
src/expr/node_traversal.h
100.0 % 5 / 5 50.0 % 4 / 8
src/expr/node_trie.cpp
74.1 % 20 / 27 38.3 % 36 / 94
src/expr/node_trie.h
100.0 % 6 / 6 50.0 % 3 / 6
src/expr/node_value.cpp
33.3 % 11 / 33 15.9 % 13 / 82
src/expr/node_value.h
77.2 % 105 / 136 25.1 % 43 / 171
src/expr/node_visitor.h
100.0 % 33 / 33 50.0 % 89 / 178
src/expr/proof.cpp
80.2 % 170 / 212 42.5 % 392 / 922
src/expr/proof_checker.cpp
56.8 % 92 / 162 20.9 % 131 / 626
src/expr/proof_checker.h
80.0 % 4 / 5 100.0 % 0 / 0
src/expr/proof_ensure_closed.cpp
15.8 % 12 / 76 4.4 % 18 / 410
src/expr/proof_generator.cpp
11.5 % 3 / 26 1.7 % 2 / 120
src/expr/proof_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/proof_node.cpp
91.2 % 31 / 34 50.0 % 15 / 30
src/expr/proof_node.h
100.0 % 3 / 3 50.0 % 2 / 4
src/expr/proof_node_algorithm.cpp
72.0 % 54 / 75 36.4 % 59 / 162
src/expr/proof_node_manager.cpp
72.8 % 115 / 158 28.7 % 207 / 722
src/expr/proof_node_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/proof_node_to_sexpr.cpp
79.3 % 65 / 82 33.3 % 96 / 288
src/expr/proof_node_to_sexpr.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/proof_node_updater.cpp
73.8 % 96 / 130 35.0 % 124 / 354
src/expr/proof_node_updater.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/proof_rule.cpp
13.0 % 22 / 169 10.5 % 16 / 153
src/expr/proof_set.h
100.0 % 7 / 7 57.1 % 8 / 14
src/expr/proof_step_buffer.cpp
59.1 % 26 / 44 20.0 % 18 / 90
src/expr/proof_step_buffer.h
100.0 % 2 / 2 25.0 % 1 / 4
src/expr/record.cpp
33.3 % 1 / 3 25.0 % 2 / 8
src/expr/record.h
100.0 % 6 / 6 50.0 % 1 / 2
src/expr/sequence.cpp
55.0 % 105 / 191 20.8 % 118 / 566
src/expr/sequence.h
100.0 % 3 / 3 100.0 % 0 / 0
src/expr/skolem_manager.cpp
97.0 % 130 / 134 40.0 % 287 / 718
src/expr/skolem_manager.h
100.0 % 2 / 2 100.0 % 0 / 0
src/expr/subs.cpp
40.7 % 33 / 81 16.8 % 36 / 214
src/expr/subs.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/sygus_datatype.cpp
100.0 % 43 / 43 31.0 % 39 / 126
src/expr/sygus_datatype.h
100.0 % 3 / 3 30.0 % 3 / 10
src/expr/symbol_manager.cpp
96.3 % 131 / 136 52.7 % 116 / 220
src/expr/symbol_table.cpp
84.0 % 194 / 231 38.2 % 188 / 492
src/expr/symbol_table.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/tconv_seq_proof_generator.cpp
70.5 % 55 / 78 23.0 % 70 / 304
src/expr/term_canonize.cpp
99.0 % 100 / 101 54.6 % 200 / 366
src/expr/term_canonize.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/term_context.cpp
39.6 % 21 / 53 40.7 % 22 / 54
src/expr/term_context.h
85.7 % 6 / 7 100.0 % 0 / 0
src/expr/term_context_node.cpp
13.3 % 4 / 30 4.3 % 6 / 140
src/expr/term_context_stack.cpp
72.2 % 26 / 36 28.4 % 38 / 134
src/expr/term_context_stack.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/term_conversion_proof_generator.cpp
84.1 % 249 / 296 35.7 % 520 / 1457
src/expr/type_checker_util.h
75.0 % 36 / 48 11.1 % 164 / 1478
src/expr/type_matcher.cpp
95.2 % 59 / 62 53.2 % 84 / 158
src/expr/type_matcher.h
100.0 % 2 / 2 100.0 % 0 / 0
src/expr/type_node.cpp
85.0 % 284 / 334 38.4 % 430 / 1120
src/expr/type_node.h
85.4 % 181 / 212 20.9 % 173 / 827
src/expr/uninterpreted_constant.cpp
64.9 % 24 / 37 38.5 % 30 / 78
src/main/command_executor.cpp
48.0 % 72 / 150 32.9 % 116 / 353
src/main/command_executor.h
100.0 % 8 / 8 100.0 % 0 / 0
src/main/driver_unified.cpp
34.0 % 85 / 250 18.0 % 119 / 662
src/main/interactive_shell.cpp
67.0 % 59 / 88 35.1 % 105 / 299
src/main/main.cpp
87.5 % 14 / 16 47.7 % 31 / 65
src/main/signal_handlers.cpp
31.5 % 39 / 124 11.9 % 15 / 126
src/main/time_limit.cpp
72.7 % 16 / 22 29.2 % 7 / 24
src/options/base_handlers.h
0.0 % 0 / 10 0.0 % 0 / 48
src/options/didyoumean.cpp
1.5 % 1 / 68 2.0 % 2 / 98
src/options/didyoumean.h
0.0 % 0 / 3 100.0 % 0 / 0
src/options/language.cpp
63.4 % 45 / 71 43.3 % 71 / 164
src/options/language.h
43.2 % 16 / 37 30.8 % 4 / 13
src/options/open_ostream.cpp
6.5 % 2 / 31 3.9 % 3 / 76
src/options/open_ostream.h
0.0 % 0 / 1 100.0 % 0 / 0
src/options/option_exception.cpp
100.0 % 2 / 2 50.0 % 3 / 6
src/options/option_exception.h
100.0 % 6 / 6 50.0 % 2 / 4
src/options/options.h
100.0 % 11 / 11 100.0 % 0 / 0
src/options/options_handler.cpp
42.7 % 120 / 281 23.4 % 155 / 662
src/options/options_handler.h
0.0 % 0 / 6 0.0 % 0 / 8
src/options/options_listener.h
100.0 % 2 / 2 100.0 % 0 / 0
src/options/options_public_functions.cpp
87.4 % 90 / 103 31.1 % 28 / 90
src/options/printer_modes.cpp
12.5 % 1 / 8 28.6 % 2 / 7
src/options/set_language.cpp
100.0 % 29 / 29 56.3 % 9 / 16
src/parser/antlr_input.cpp
90.2 % 221 / 245 46.4 % 245 / 528
src/parser/antlr_input.h
84.4 % 27 / 32 37.8 % 31 / 82
src/parser/antlr_input_imports.cpp
65.8 % 73 / 111 23.1 % 55 / 238
src/parser/antlr_line_buffered_input.cpp
1.1 % 1 / 88 2.3 % 2 / 88
src/parser/bounded_token_buffer.cpp
52.7 % 88 / 167 9.9 % 25 / 252
src/parser/bounded_token_factory.cpp
87.5 % 42 / 48 59.1 % 13 / 22
src/parser/cvc/cvc.cpp
100.0 % 10 / 10 50.0 % 9 / 18
src/parser/cvc/cvc.h
100.0 % 4 / 4 100.0 % 0 / 0
src/parser/cvc/cvc_input.cpp
91.7 % 22 / 24 25.0 % 14 / 56
src/parser/input.cpp
87.0 % 20 / 23 50.0 % 3 / 6
src/parser/input.h
77.8 % 7 / 9 50.0 % 1 / 2
src/parser/line_buffer.cpp
2.6 % 1 / 39 2.9 % 2 / 70
src/parser/memory_mapped_input_buffer.cpp
0.0 % 0 / 33 0.0 % 0 / 14
src/parser/parse_op.cpp
0.0 % 0 / 15 0.0 % 0 / 46
src/parser/parse_op.h
100.0 % 2 / 2 50.0 % 3 / 6
src/parser/parser.cpp
73.0 % 360 / 493 34.3 % 446 / 1299
src/parser/parser.h
71.4 % 25 / 35 25.0 % 2 / 8
src/parser/parser_builder.cpp
84.6 % 104 / 123 34.4 % 33 / 96
src/parser/parser_builder.h
100.0 % 1 / 1 100.0 % 0 / 0
src/parser/parser_exception.h
85.0 % 17 / 20 75.0 % 3 / 4
src/parser/smt2/smt2.cpp
87.5 % 587 / 671 47.4 % 975 / 2058
src/parser/smt2/smt2.h
66.7 % 22 / 33 36.5 % 27 / 74
src/parser/smt2/smt2_input.cpp
91.3 % 21 / 23 25.0 % 14 / 56
src/parser/smt2/sygus_input.cpp
83.3 % 20 / 24 25.0 % 14 / 56
src/parser/tptp/tptp.cpp
80.1 % 185 / 231 35.5 % 255 / 718
src/parser/tptp/tptp.h
71.4 % 5 / 7 100.0 % 0 / 0
src/parser/tptp/tptp_input.cpp
83.3 % 20 / 24 25.0 % 14 / 56
src/preprocessing/assertion_pipeline.cpp
100.0 % 90 / 90 39.7 % 151 / 380
src/preprocessing/assertion_pipeline.h
100.0 % 14 / 14 100.0 % 4 / 4
src/preprocessing/passes/ackermann.cpp
97.2 % 106 / 109 41.3 % 217 / 526
src/preprocessing/passes/ackermann.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/apply_substs.cpp
100.0 % 21 / 21 55.6 % 30 / 54
src/preprocessing/passes/apply_substs.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/bool_to_bv.cpp
96.8 % 179 / 185 52.0 % 420 / 807
src/preprocessing/passes/bool_to_bv.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/bv_abstraction.cpp
100.0 % 12 / 12 50.0 % 13 / 26
src/preprocessing/passes/bv_abstraction.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/bv_eager_atoms.cpp
100.0 % 12 / 12 50.0 % 14 / 28
src/preprocessing/passes/bv_eager_atoms.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/bv_gauss.cpp
91.0 % 313 / 344 40.0 % 676 / 1688
src/preprocessing/passes/bv_gauss.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/bv_intro_pow2.cpp
94.9 % 37 / 39 50.4 % 61 / 121
src/preprocessing/passes/bv_intro_pow2.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/bv_to_bool.cpp
98.1 % 158 / 161 40.8 % 378 / 926
src/preprocessing/passes/bv_to_bool.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/bv_to_int.cpp
88.7 % 414 / 467 41.1 % 837 / 2037
src/preprocessing/passes/bv_to_int.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/extended_rewriter_pass.cpp
100.0 % 9 / 9 46.4 % 13 / 28
src/preprocessing/passes/extended_rewriter_pass.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/foreign_theory_rewrite.cpp
98.1 % 52 / 53 37.7 % 92 / 244
src/preprocessing/passes/foreign_theory_rewrite.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/fun_def_fmf.cpp
94.8 % 219 / 231 47.5 % 462 / 972
src/preprocessing/passes/global_negate.cpp
98.0 % 48 / 49 51.8 % 86 / 166
src/preprocessing/passes/global_negate.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/ho_elim.cpp
97.9 % 320 / 327 46.0 % 709 / 1540
src/preprocessing/passes/ho_elim.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/int_to_bv.cpp
69.9 % 93 / 133 31.5 % 193 / 612
src/preprocessing/passes/int_to_bv.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/ite_removal.cpp
95.8 % 23 / 24 35.2 % 31 / 88
src/preprocessing/passes/ite_removal.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/ite_simp.cpp
50.8 % 63 / 124 15.1 % 69 / 458
src/preprocessing/passes/ite_simp.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/miplib_trick.cpp
12.3 % 45 / 367 2.7 % 51 / 1882
src/preprocessing/passes/nl_ext_purify.cpp
98.2 % 55 / 56 56.3 % 107 / 190
src/preprocessing/passes/nl_ext_purify.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/non_clausal_simp.cpp
96.2 % 230 / 239 41.0 % 525 / 1280
src/preprocessing/passes/non_clausal_simp.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/pseudo_boolean_processor.cpp
75.0 % 147 / 196 28.1 % 262 / 933
src/preprocessing/passes/pseudo_boolean_processor.h
100.0 % 3 / 3 57.1 % 8 / 14
src/preprocessing/passes/quantifier_macros.cpp
85.8 % 289 / 337 46.7 % 595 / 1274
src/preprocessing/passes/quantifier_macros.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/quantifiers_preprocess.cpp
100.0 % 15 / 15 52.0 % 26 / 50
src/preprocessing/passes/quantifiers_preprocess.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/real_to_int.cpp
96.9 % 93 / 96 49.3 % 225 / 456
src/preprocessing/passes/real_to_int.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/rewrite.cpp
100.0 % 7 / 7 50.0 % 8 / 16
src/preprocessing/passes/rewrite.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/sep_skolem_emp.cpp
95.9 % 47 / 49 50.5 % 98 / 194
src/preprocessing/passes/sep_skolem_emp.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/sort_infer.cpp
100.0 % 36 / 36 54.0 % 54 / 100
src/preprocessing/passes/sort_infer.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/static_learning.cpp
100.0 % 15 / 15 52.6 % 20 / 38
src/preprocessing/passes/static_learning.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/strings_eager_pp.cpp
100.0 % 19 / 19 54.5 % 24 / 44
src/preprocessing/passes/strings_eager_pp.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/sygus_inference.cpp
95.8 % 160 / 167 49.0 % 306 / 624
src/preprocessing/passes/sygus_inference.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/synth_rew_rules.cpp
1.2 % 3 / 250 0.4 % 4 / 1002
src/preprocessing/passes/synth_rew_rules.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/theory_preprocess.cpp
100.0 % 21 / 21 44.4 % 32 / 72
src/preprocessing/passes/theory_preprocess.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/theory_rewrite_eq.cpp
100.0 % 53 / 53 46.2 % 109 / 236
src/preprocessing/passes/theory_rewrite_eq.h
100.0 % 1 / 1 100.0 % 0 / 0
src/preprocessing/passes/unconstrained_simplifier.cpp
83.4 % 337 / 404 42.1 % 725 / 1721
src/preprocessing/preprocessing_pass.cpp
100.0 % 29 / 29 55.4 % 51 / 92
src/preprocessing/preprocessing_pass_context.cpp
100.0 % 19 / 19 53.6 % 15 / 28
src/preprocessing/preprocessing_pass_context.h
100.0 % 14 / 14 100.0 % 0 / 0
src/preprocessing/preprocessing_pass_registry.cpp
100.0 % 56 / 56 48.4 % 152 / 314
src/preprocessing/util/ite_utilities.cpp
47.2 % 471 / 998 21.5 % 800 / 3729
src/preprocessing/util/ite_utilities.h
18.6 % 8 / 43 9.1 % 4 / 44
src/printer/ast/ast_printer.cpp
16.5 % 37 / 224 16.7 % 43 / 258
src/printer/ast/ast_printer.h
100.0 % 1 / 1 100.0 % 0 / 0
src/printer/cvc/cvc_printer.cpp
34.8 % 360 / 1035 22.0 % 473 / 2152
src/printer/cvc/cvc_printer.h
100.0 % 2 / 2 100.0 % 0 / 0
src/printer/let_binding.cpp
98.1 % 103 / 105 46.4 % 169 / 364
src/printer/let_binding.h
100.0 % 1 / 1 100.0 % 0 / 0
src/printer/printer.cpp
24.2 % 52 / 215 18.7 % 57 / 305
src/printer/printer.h
100.0 % 2 / 2 100.0 % 0 / 0
src/printer/smt2/smt2_printer.cpp
50.7 % 605 / 1193 31.2 % 1007 / 3230
src/printer/smt2/smt2_printer.h
100.0 % 2 / 2 100.0 % 0 / 0
src/printer/tptp/tptp_printer.cpp
23.3 % 7 / 30 3.1 % 2 / 64
src/printer/tptp/tptp_printer.h
100.0 % 1 / 1 100.0 % 0 / 0
src/proof/cnf_proof.cpp
100.0 % 47 / 47 38.4 % 73 / 190
src/proof/cnf_proof.h
100.0 % 1 / 1 100.0 % 0 / 0
src/proof/dot/dot_printer.cpp
2.4 % 1 / 41 2.1 % 2 / 94
src/proof/proof_manager.cpp
73.4 % 80 / 109 33.5 % 162 / 484
src/proof/proof_manager.h
100.0 % 5 / 5 100.0 % 0 / 0
src/proof/sat_proof.h
90.0 % 9 / 10 66.7 % 4 / 6
src/proof/sat_proof_implementation.h
68.5 % 383 / 559 25.7 % 424 / 1652
src/proof/unsat_core.cpp
82.6 % 19 / 23 42.9 % 18 / 42
src/proof/unsat_core.h
100.0 % 2 / 2 100.0 % 0 / 0
src/prop/bv_sat_solver_notify.h
100.0 % 2 / 2 100.0 % 0 / 0
src/prop/bvminisat/bvminisat.cpp
74.3 % 130 / 175 33.3 % 94 / 282
src/prop/bvminisat/bvminisat.h
85.7 % 12 / 14 0.0 % 0 / 6
src/prop/bvminisat/core/Solver.cc
80.0 % 521 / 651 41.0 % 579 / 1413
src/prop/bvminisat/core/Solver.h
83.6 % 61 / 73 52.3 % 45 / 86
src/prop/bvminisat/core/SolverTypes.h
94.7 % 124 / 131 36.5 % 62 / 170
src/prop/bvminisat/mtl/Alg.h
100.0 % 11 / 11 45.5 % 25 / 55
src/prop/bvminisat/mtl/Alloc.h
95.7 % 45 / 47 19.4 % 21 / 108
src/prop/bvminisat/mtl/Heap.h
89.6 % 69 / 77 28.2 % 35 / 124
src/prop/bvminisat/mtl/Queue.h
96.4 % 27 / 28 26.9 % 21 / 78
src/prop/bvminisat/mtl/Sort.h
100.0 % 27 / 27 93.8 % 30 / 32
src/prop/bvminisat/mtl/Vec.h
97.8 % 45 / 46 39.2 % 134 / 342
src/prop/bvminisat/mtl/XAlloc.h
80.0 % 4 / 5 25.0 % 1 / 4
src/prop/bvminisat/simp/SimpSolver.cc
74.2 % 299 / 403 37.6 % 366 / 974
src/prop/bvminisat/simp/SimpSolver.h
89.5 % 17 / 19 47.1 % 16 / 34
src/prop/bvminisat/utils/Options.h
23.9 % 22 / 92 5.6 % 4 / 72
src/prop/bvminisat/utils/ParseUtils.h
0.0 % 0 / 6 0.0 % 0 / 4
src/prop/cadical.cpp
69.5 % 66 / 95 25.3 % 42 / 166
src/prop/cnf_stream.cpp
93.4 % 381 / 408 37.6 % 729 / 1940
src/prop/cnf_stream.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/cryptominisat.cpp
70.5 % 86 / 122 30.7 % 73 / 238
src/prop/cryptominisat.h
0.0 % 0 / 1 100.0 % 0 / 0
src/prop/minisat/core/Solver.cc
81.9 % 920 / 1123 43.6 % 1459 / 3346
src/prop/minisat/core/Solver.h
94.7 % 108 / 114 44.1 % 98 / 222
src/prop/minisat/core/SolverTypes.h
87.5 % 140 / 160 35.3 % 67 / 190
src/prop/minisat/minisat.cpp
83.9 % 135 / 161 31.9 % 97 / 304
src/prop/minisat/minisat.h
50.0 % 2 / 4 0.0 % 0 / 6
src/prop/minisat/mtl/Alg.h
100.0 % 11 / 11 45.5 % 25 / 55
src/prop/minisat/mtl/Alloc.h
95.7 % 45 / 47 19.4 % 21 / 108
src/prop/minisat/mtl/Heap.h
89.6 % 69 / 77 28.2 % 35 / 124
src/prop/minisat/mtl/Queue.h
96.4 % 27 / 28 25.6 % 20 / 78
src/prop/minisat/mtl/Sort.h
100.0 % 27 / 27 87.5 % 49 / 56
src/prop/minisat/mtl/Vec.h
95.7 % 45 / 47 42.4 % 222 / 524
src/prop/minisat/mtl/XAlloc.h
80.0 % 4 / 5 25.0 % 1 / 4
src/prop/minisat/simp/SimpSolver.cc
75.8 % 313 / 413 39.1 % 418 / 1070
src/prop/minisat/simp/SimpSolver.h
84.0 % 21 / 25 50.0 % 20 / 40
src/prop/minisat/utils/Options.h
23.9 % 22 / 92 5.6 % 4 / 72
src/prop/minisat/utils/ParseUtils.h
0.0 % 0 / 6 0.0 % 0 / 4
src/prop/proof_cnf_stream.cpp
93.0 % 571 / 614 44.6 % 1481 / 3324
src/prop/proof_cnf_stream.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/proof_post_processor.cpp
90.9 % 40 / 44 33.1 % 51 / 154
src/prop/proof_post_processor.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/prop_engine.cpp
72.1 % 217 / 301 29.7 % 308 / 1038
src/prop/prop_engine.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/prop_proof_manager.cpp
38.0 % 19 / 50 10.4 % 19 / 182
src/prop/prop_proof_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/registrar.h
100.0 % 4 / 4 100.0 % 0 / 0
src/prop/sat_proof_manager.cpp
71.2 % 299 / 420 29.4 % 610 / 2078
src/prop/sat_proof_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/sat_solver.h
15.8 % 6 / 38 0.0 % 0 / 30
src/prop/sat_solver_factory.cpp
86.7 % 13 / 15 30.0 % 6 / 20
src/prop/sat_solver_types.cpp
33.3 % 1 / 3 50.0 % 2 / 4
src/prop/sat_solver_types.h
87.9 % 29 / 33 31.3 % 5 / 16
src/prop/theory_proxy.cpp
93.9 % 92 / 98 42.6 % 126 / 296
src/smt/abduction_solver.cpp
83.8 % 83 / 99 37.2 % 163 / 438
src/smt/abstract_values.cpp
100.0 % 16 / 16 37.9 % 25 / 66
src/smt/assertions.cpp
89.5 % 85 / 95 43.4 % 99 / 228
src/smt/check_models.cpp
68.1 % 32 / 47 27.6 % 58 / 210
src/smt/command.cpp
50.6 % 621 / 1228 30.0 % 452 / 1509
src/smt/command.h
75.6 % 59 / 78 25.0 % 4 / 16
src/smt/defined_function.h
85.7 % 6 / 7 40.0 % 4 / 10
src/smt/dump.cpp
69.9 % 51 / 73 36.2 % 47 / 130
src/smt/dump.h
100.0 % 10 / 10 57.1 % 16 / 28
src/smt/dump_manager.cpp
100.0 % 26 / 26 56.0 % 28 / 50
src/smt/env.cpp
94.6 % 35 / 37 46.9 % 15 / 32
src/smt/expand_definitions.cpp
89.2 % 140 / 157 42.4 % 285 / 672
src/smt/interpolation_solver.cpp
79.3 % 46 / 58 39.5 % 83 / 210
src/smt/listeners.cpp
88.4 % 38 / 43 40.0 % 48 / 120
src/smt/listeners.h
100.0 % 3 / 3 100.0 % 0 / 0
src/smt/logic_exception.h
100.0 % 7 / 7 100.0 % 0 / 0
src/smt/managed_ostreams.cpp
30.7 % 27 / 88 20.3 % 26 / 128
src/smt/managed_ostreams.h
40.0 % 4 / 10 0.0 % 0 / 2
src/smt/model.cpp
100.0 % 24 / 24 27.5 % 11 / 40
src/smt/model.h
33.3 % 1 / 3 100.0 % 0 / 0
src/smt/model_blocker.cpp
84.7 % 122 / 144 36.4 % 279 / 766
src/smt/model_core_builder.cpp
2.0 % 1 / 50 1.1 % 2 / 182
src/smt/node_command.cpp
64.3 % 36 / 56 34.1 % 30 / 88
src/smt/node_command.h
100.0 % 5 / 5 9.4 % 3 / 32
src/smt/optimization_solver.cpp
97.7 % 43 / 44 36.5 % 57 / 156
src/smt/optimization_solver.h
100.0 % 2 / 2 100.0 % 0 / 0
src/smt/options_manager.cpp
75.0 % 51 / 68 34.9 % 88 / 252
src/smt/output_manager.cpp
100.0 % 5 / 5 50.0 % 2 / 4
src/smt/preprocess_proof_generator.cpp
92.5 % 99 / 107 42.5 % 209 / 492
src/smt/preprocess_proof_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/smt/preprocessor.cpp
95.1 % 58 / 61 39.7 % 62 / 156
src/smt/process_assertions.cpp
93.0 % 173 / 186 49.5 % 381 / 770
src/smt/proof_manager.cpp
70.0 % 63 / 90 28.8 % 94 / 326
src/smt/proof_post_processor.cpp
91.8 % 504 / 549 38.4 % 941 / 2448
src/smt/proof_post_processor.h
100.0 % 1 / 1 100.0 % 0 / 0
src/smt/quant_elim_solver.cpp
92.4 % 61 / 66 43.3 % 148 / 342
src/smt/set_defaults.cpp
80.4 % 558 / 694 47.8 % 1700 / 3556
src/smt/smt_engine.cpp
80.8 % 817 / 1011 36.8 % 1248 / 3395
src/smt/smt_engine.h
100.0 % 3 / 3 100.0 % 0 / 0
src/smt/smt_engine_scope.cpp
100.0 % 24 / 24 20.5 % 18 / 88
src/smt/smt_engine_state.cpp
89.4 % 126 / 141 36.4 % 92 / 253
src/smt/smt_engine_state.h
100.0 % 1 / 1 100.0 % 0 / 0
src/smt/smt_engine_stats.cpp
100.0 % 28 / 28 50.0 % 46 / 92
src/smt/smt_mode.cpp
8.3 % 1 / 12 16.7 % 2 / 12
src/smt/smt_solver.cpp
90.8 % 108 / 119 46.0 % 163 / 354
src/smt/smt_statistics_registry.cpp
100.0 % 3 / 3 50.0 % 2 / 4
src/smt/smt_statistics_registry.h
100.0 % 1 / 1 33.3 % 2 / 6
src/smt/sygus_solver.cpp
87.1 % 183 / 210 44.7 % 331 / 740
src/smt/term_formula_removal.cpp
94.0 % 268 / 285 47.1 % 499 / 1060
src/smt/unsat_core_manager.cpp
54.5 % 24 / 44 14.0 % 23 / 164
src/smt/unsat_core_manager.h
100.0 % 2 / 2 100.0 % 0 / 0
src/smt/update_ostream.h
2.4 % 1 / 41 0.0 % 0 / 38
src/smt/witness_form.cpp
69.8 % 44 / 63 26.6 % 77 / 290
src/smt/witness_form.h
100.0 % 1 / 1 100.0 % 0 / 0
src/smt_util/boolean_simplification.cpp
55.6 % 15 / 27 37.3 % 38 / 102
src/smt_util/boolean_simplification.h
79.4 % 54 / 68 39.4 % 74 / 188
src/smt_util/nary_builder.cpp
11.1 % 11 / 99 3.5 % 11 / 315
src/theory/arith/approx_simplex.cpp
2.6 % 4 / 151 0.4 % 2 / 447
src/theory/arith/approx_simplex.h
0.0 % 0 / 3 100.0 % 0 / 0
src/theory/arith/arith_ite_utils.cpp
0.4 % 1 / 279 0.1 % 2 / 1346
src/theory/arith/arith_msum.cpp
91.0 % 131 / 144 51.2 % 329 / 642
src/theory/arith/arith_msum.h
100.0 % 2 / 2 55.0 % 11 / 20
src/theory/arith/arith_preprocess.cpp
25.0 % 7 / 28 7.3 % 6 / 82
src/theory/arith/arith_preprocess.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/arith_rewriter.cpp
87.9 % 437 / 497 42.2 % 1022 / 2423
src/theory/arith/arith_rewriter.h
100.0 % 3 / 3 25.0 % 1 / 4
src/theory/arith/arith_state.cpp
100.0 % 7 / 7 60.0 % 6 / 10
src/theory/arith/arith_state.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/arith_static_learner.cpp
83.9 % 130 / 155 38.8 % 355 / 915
src/theory/arith/arith_utilities.cpp
78.9 % 127 / 161 35.2 % 230 / 654
src/theory/arith/arith_utilities.h
64.3 % 74 / 115 33.5 % 52 / 155
src/theory/arith/arithvar.cpp
100.0 % 4 / 4 50.0 % 3 / 6
src/theory/arith/attempt_solution_simplex.cpp
18.8 % 15 / 80 5.4 % 16 / 298
src/theory/arith/attempt_solution_simplex.h
16.7 % 1 / 6 0.0 % 0 / 4
src/theory/arith/bound_counts.h
85.6 % 83 / 97 29.6 % 48 / 162
src/theory/arith/bound_inference.cpp
60.3 % 82 / 136 34.6 % 161 / 465
src/theory/arith/bound_inference.h
100.0 % 2 / 2 33.3 % 10 / 30
src/theory/arith/callbacks.cpp
89.3 % 100 / 112 24.3 % 112 / 460
src/theory/arith/callbacks.h
100.0 % 13 / 13 50.0 % 1 / 2
src/theory/arith/congruence_manager.cpp
88.6 % 358 / 404 38.1 % 729 / 1912
src/theory/arith/congruence_manager.h
100.0 % 3 / 3 100.0 % 0 / 0
src/theory/arith/constraint.cpp
72.9 % 1075 / 1475 28.2 % 1808 / 6419
src/theory/arith/constraint.h
95.0 % 114 / 120 17.6 % 42 / 238
src/theory/arith/cut_log.cpp
0.2 % 1 / 405 0.2 % 2 / 850
src/theory/arith/cut_log.h
0.0 % 0 / 7 0.0 % 0 / 6
src/theory/arith/delta_rational.cpp
50.0 % 26 / 52 17.6 % 37 / 210
src/theory/arith/delta_rational.h
85.4 % 82 / 96 55.7 % 49 / 88
src/theory/arith/dio_solver.cpp
87.3 % 427 / 489 35.6 % 844 / 2372
src/theory/arith/dio_solver.h
76.9 % 30 / 39 16.1 % 18 / 112
src/theory/arith/dual_simplex.cpp
91.1 % 112 / 123 38.2 % 224 / 586
src/theory/arith/dual_simplex.h
100.0 % 7 / 7 100.0 % 0 / 0
src/theory/arith/error_set.cpp
64.4 % 201 / 312 27.6 % 179 / 649
src/theory/arith/error_set.h
51.1 % 47 / 92 8.7 % 12 / 138
src/theory/arith/fc_simplex.cpp
5.9 % 29 / 495 2.0 % 45 / 2208
src/theory/arith/fc_simplex.h
2.6 % 1 / 38 0.0 % 0 / 26
src/theory/arith/infer_bounds.cpp
24.1 % 33 / 137 3.2 % 7 / 217
src/theory/arith/infer_bounds.h
0.0 % 0 / 2 100.0 % 0 / 0
src/theory/arith/inference_manager.cpp
73.8 % 48 / 65 32.9 % 48 / 146
src/theory/arith/inference_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/linear_equality.cpp
46.2 % 376 / 814 19.2 % 642 / 3352
src/theory/arith/linear_equality.h
26.2 % 48 / 183 4.2 % 19 / 454
src/theory/arith/matrix.cpp
50.0 % 2 / 4 50.0 % 2 / 4
src/theory/arith/matrix.h
76.6 % 307 / 401 22.6 % 252 / 1116
src/theory/arith/nl/cad/proof_checker.cpp
6.3 % 1 / 16 3.1 % 2 / 64
src/theory/arith/nl/cad/proof_checker.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/arith/nl/cad_solver.cpp
33.3 % 10 / 30 20.5 % 9 / 44
src/theory/arith/nl/ext/constraint.cpp
96.4 % 53 / 55 48.3 % 87 / 180
src/theory/arith/nl/ext/constraint.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/arith/nl/ext/ext_state.cpp
100.0 % 46 / 46 49.4 % 82 / 166
src/theory/arith/nl/ext/ext_state.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/ext/factoring_check.cpp
99.1 % 109 / 110 54.4 % 224 / 412
src/theory/arith/nl/ext/factoring_check.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/ext/monomial.cpp
96.4 % 162 / 168 48.1 % 251 / 522
src/theory/arith/nl/ext/monomial.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/arith/nl/ext/monomial_bounds_check.cpp
57.1 % 168 / 294 29.5 % 353 / 1198
src/theory/arith/nl/ext/monomial_bounds_check.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/ext/monomial_check.cpp
97.0 % 359 / 370 50.4 % 748 / 1484
src/theory/arith/nl/ext/monomial_check.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/ext/proof_checker.cpp
93.1 % 81 / 87 30.5 % 219 / 718
src/theory/arith/nl/ext/proof_checker.h
100.0 % 2 / 2 20.0 % 2 / 10
src/theory/arith/nl/ext/split_zero_check.cpp
23.5 % 4 / 17 4.2 % 2 / 48
src/theory/arith/nl/ext/split_zero_check.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/ext/tangent_plane_check.cpp
98.6 % 72 / 73 53.7 % 189 / 352
src/theory/arith/nl/ext/tangent_plane_check.h
100.0 % 1 / 1 75.0 % 3 / 4
src/theory/arith/nl/ext_theory_callback.cpp
91.8 % 45 / 49 47.9 % 93 / 194
src/theory/arith/nl/ext_theory_callback.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/iand_solver.cpp
76.3 % 116 / 152 34.7 % 257 / 740
src/theory/arith/nl/iand_utils.cpp
93.7 % 104 / 111 40.3 % 166 / 412
src/theory/arith/nl/iand_utils.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/icp/contraction_origins.cpp
2.3 % 1 / 43 1.5 % 2 / 136
src/theory/arith/nl/icp/contraction_origins.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/arith/nl/icp/icp_solver.cpp
20.0 % 1 / 5 12.5 % 2 / 16
src/theory/arith/nl/icp/icp_solver.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/nl_lemma_utils.cpp
75.0 % 21 / 28 41.7 % 20 / 48
src/theory/arith/nl/nl_lemma_utils.h
94.7 % 18 / 19 37.5 % 3 / 8
src/theory/arith/nl/nl_model.cpp
80.0 % 596 / 745 39.7 % 1408 / 3549
src/theory/arith/nl/nonlinear_extension.cpp
83.3 % 269 / 323 46.4 % 454 / 978
src/theory/arith/nl/nonlinear_extension.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/stats.cpp
100.0 % 10 / 10 50.0 % 10 / 20
src/theory/arith/nl/strategy.cpp
56.7 % 55 / 97 34.3 % 87 / 254
src/theory/arith/nl/strategy.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/arith/nl/transcendental/exponential_solver.cpp
93.4 % 113 / 121 45.8 % 248 / 542
src/theory/arith/nl/transcendental/proof_checker.cpp
99.2 % 260 / 262 32.6 % 744 / 2284
src/theory/arith/nl/transcendental/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/arith/nl/transcendental/sine_solver.cpp
99.1 % 222 / 224 47.7 % 547 / 1146
src/theory/arith/nl/transcendental/sine_solver.h
85.7 % 24 / 28 75.0 % 12 / 16
src/theory/arith/nl/transcendental/taylor_generator.cpp
93.7 % 118 / 126 43.1 % 238 / 552
src/theory/arith/nl/transcendental/taylor_generator.h
100.0 % 2 / 2 30.0 % 3 / 10
src/theory/arith/nl/transcendental/transcendental_solver.cpp
86.0 % 178 / 207 41.9 % 347 / 829
src/theory/arith/nl/transcendental/transcendental_state.cpp
93.8 % 181 / 193 46.3 % 493 / 1064
src/theory/arith/nl/transcendental/transcendental_state.h
100.0 % 1 / 1 75.0 % 3 / 4
src/theory/arith/normal_form.cpp
80.8 % 641 / 793 36.8 % 1088 / 2958
src/theory/arith/normal_form.h
96.9 % 371 / 383 36.6 % 406 / 1108
src/theory/arith/operator_elim.cpp
93.5 % 202 / 216 48.8 % 497 / 1019
src/theory/arith/operator_elim.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/partial_model.cpp
78.8 % 320 / 406 33.6 % 294 / 874
src/theory/arith/partial_model.h
100.0 % 34 / 34 50.0 % 1 / 2
src/theory/arith/proof_checker.cpp
59.1 % 110 / 186 25.5 % 238 / 934
src/theory/arith/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/arith/rewrites.cpp
5.6 % 1 / 18 12.5 % 2 / 16
src/theory/arith/simplex.cpp
35.8 % 58 / 162 13.9 % 82 / 590
src/theory/arith/simplex.h
15.4 % 2 / 13 0.0 % 0 / 2
src/theory/arith/simplex_update.cpp
0.9 % 1 / 116 0.6 % 2 / 321
src/theory/arith/simplex_update.h
0.0 % 0 / 57 0.0 % 0 / 102
src/theory/arith/soi_simplex.cpp
6.3 % 35 / 555 2.3 % 58 / 2476
src/theory/arith/soi_simplex.h
6.3 % 1 / 16 0.0 % 0 / 10
src/theory/arith/tableau.cpp
69.7 % 76 / 109 23.8 % 117 / 492
src/theory/arith/tableau.h
54.5 % 18 / 33 8.3 % 3 / 36
src/theory/arith/tableau_sizes.cpp
20.0 % 1 / 5 50.0 % 2 / 4
src/theory/arith/tableau_sizes.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/theory_arith.cpp
99.2 % 132 / 133 46.8 % 176 / 376
src/theory/arith/theory_arith.h
75.0 % 3 / 4 0.0 % 0 / 2
src/theory/arith/theory_arith_private.cpp
57.0 % 1833 / 3213 27.2 % 3838 / 14108
src/theory/arith/theory_arith_private.h
84.8 % 28 / 33 21.4 % 6 / 28
src/theory/arith/theory_arith_type_rules.h
74.6 % 44 / 59 31.1 % 57 / 183
src/theory/arith/type_enumerator.h
100.0 % 37 / 37 44.0 % 51 / 116
src/theory/arrays/array_info.cpp
68.2 % 212 / 311 30.7 % 300 / 978
src/theory/arrays/array_info.h
100.0 % 14 / 14 39.3 % 22 / 56
src/theory/arrays/inference_manager.cpp
86.2 % 50 / 58 38.6 % 78 / 202
src/theory/arrays/inference_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arrays/proof_checker.cpp
67.2 % 41 / 61 22.7 % 103 / 454
src/theory/arrays/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/arrays/skolem_cache.cpp
95.8 % 23 / 24 31.8 % 56 / 176
src/theory/arrays/theory_arrays.cpp
72.9 % 907 / 1245 36.5 % 2426 / 6641
src/theory/arrays/theory_arrays.h
97.5 % 39 / 40 55.7 % 59 / 106
src/theory/arrays/theory_arrays_rewriter.cpp
100.0 % 9 / 9 42.9 % 6 / 14
src/theory/arrays/theory_arrays_rewriter.h
99.3 % 293 / 295 53.9 % 773 / 1433
src/theory/arrays/theory_arrays_type_rules.h
66.9 % 87 / 130 26.2 % 171 / 652
src/theory/arrays/type_enumerator.h
91.3 % 63 / 69 49.0 % 99 / 202
src/theory/arrays/union_find.cpp
7.7 % 1 / 13 1.4 % 2 / 142
src/theory/assertion.cpp
33.3 % 1 / 3 33.3 % 2 / 6
src/theory/assertion.h
83.3 % 5 / 6 100.0 % 0 / 0
src/theory/atom_requests.cpp
87.1 % 27 / 31 40.2 % 45 / 112
src/theory/atom_requests.h
100.0 % 13 / 13 75.0 % 3 / 4
src/theory/bags/bag_solver.cpp
92.8 % 103 / 111 39.3 % 159 / 405
src/theory/bags/bags_rewriter.cpp
94.5 % 207 / 219 46.0 % 827 / 1797
src/theory/bags/bags_rewriter.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/bags/bags_statistics.cpp
100.0 % 7 / 7 50.0 % 6 / 12
src/theory/bags/infer_info.cpp
43.8 % 14 / 32 16.4 % 20 / 122
src/theory/bags/infer_info.h
100.0 % 2 / 2 50.0 % 3 / 6
src/theory/bags/inference_generator.cpp
90.3 % 139 / 154 32.3 % 301 / 932
src/theory/bags/inference_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bags/inference_manager.cpp
80.0 % 12 / 15 46.4 % 13 / 28
src/theory/bags/inference_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bags/make_bag_op.cpp
84.6 % 11 / 13 43.8 % 7 / 16
src/theory/bags/make_bag_op.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bags/normal_form.cpp
93.5 % 244 / 261 43.1 % 557 / 1292
src/theory/bags/rewrites.cpp
2.0 % 1 / 49 4.5 % 2 / 44
src/theory/bags/solver_state.cpp
100.0 % 69 / 69 48.4 % 123 / 254
src/theory/bags/solver_state.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bags/term_registry.cpp
41.7 % 5 / 12 14.3 % 4 / 28
src/theory/bags/term_registry.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bags/theory_bags.cpp
88.5 % 108 / 122 40.5 % 161 / 398
src/theory/bags/theory_bags.h
80.0 % 4 / 5 0.0 % 0 / 2
src/theory/bags/theory_bags_type_enumerator.cpp
3.1 % 1 / 32 1.9 % 2 / 106
src/theory/bags/theory_bags_type_rules.h
71.7 % 91 / 127 26.1 % 177 / 678
src/theory/booleans/circuit_propagator.cpp
93.0 % 346 / 372 48.6 % 854 / 1756
src/theory/booleans/circuit_propagator.h
100.0 % 29 / 29 52.0 % 52 / 100
src/theory/booleans/proof_checker.cpp
87.2 % 462 / 530 31.5 % 1039 / 3294
src/theory/booleans/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/booleans/proof_circuit_propagator.cpp
91.6 % 228 / 249 49.5 % 544 / 1098
src/theory/booleans/proof_circuit_propagator.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/booleans/theory_bool.cpp
95.5 % 21 / 22 52.7 % 39 / 74
src/theory/booleans/theory_bool.h
66.7 % 2 / 3 0.0 % 0 / 2
src/theory/booleans/theory_bool_rewriter.cpp
96.1 % 220 / 229 55.1 % 863 / 1565
src/theory/booleans/theory_bool_rewriter.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/booleans/theory_bool_type_rules.h
100.0 % 29 / 29 53.6 % 75 / 140
src/theory/booleans/type_enumerator.h
100.0 % 19 / 19 40.0 % 14 / 35
src/theory/builtin/proof_checker.cpp
67.2 % 182 / 271 29.5 % 312 / 1057
src/theory/builtin/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/builtin/theory_builtin.cpp
83.3 % 10 / 12 50.0 % 11 / 22
src/theory/builtin/theory_builtin.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/builtin/theory_builtin_rewriter.cpp
90.0 % 225 / 250 42.5 % 655 / 1541
src/theory/builtin/theory_builtin_rewriter.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/builtin/theory_builtin_type_rules.cpp
100.0 % 8 / 8 35.7 % 15 / 42
src/theory/builtin/theory_builtin_type_rules.h
61.9 % 73 / 118 33.9 % 164 / 484
src/theory/builtin/type_enumerator.cpp
6.7 % 1 / 15 3.6 % 2 / 56
src/theory/builtin/type_enumerator.h
88.9 % 24 / 27 41.7 % 35 / 84
src/theory/bv/abstraction.cpp
27.4 % 173 / 631 10.0 % 275 / 2758
src/theory/bv/abstraction.h
20.6 % 7 / 34 2.1 % 1 / 48
src/theory/bv/bitblast/bitblast_strategies_template.h
80.0 % 364 / 455 29.0 % 699 / 2412
src/theory/bv/bitblast/bitblast_utils.h
88.9 % 96 / 108 37.7 % 144 / 382
src/theory/bv/bitblast/bitblaster.h
95.3 % 102 / 107 40.8 % 107 / 262
src/theory/bv/bitblast/eager_bitblaster.cpp
90.1 % 118 / 131 35.0 % 199 / 569
src/theory/bv/bitblast/eager_bitblaster.h
75.0 % 3 / 4 50.0 % 1 / 2
src/theory/bv/bitblast/lazy_bitblaster.cpp
70.0 % 222 / 317 31.9 % 364 / 1141
src/theory/bv/bitblast/lazy_bitblaster.h
57.1 % 4 / 7 100.0 % 0 / 0
src/theory/bv/bitblast/proof_bitblaster.cpp
100.0 % 30 / 30 54.0 % 54 / 100
src/theory/bv/bitblast/proof_bitblaster.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bv/bitblast/simple_bitblaster.cpp
87.1 % 61 / 70 37.0 % 100 / 270
src/theory/bv/bitblast/simple_bitblaster.h
50.0 % 1 / 2 0.0 % 0 / 4
src/theory/bv/bv_eager_solver.cpp
82.6 % 38 / 46 25.5 % 51 / 200
src/theory/bv/bv_inequality_graph.cpp
94.7 % 284 / 300 40.9 % 510 / 1247
src/theory/bv/bv_inequality_graph.h
100.0 % 41 / 41 28.0 % 23 / 82
src/theory/bv/bv_quick_check.cpp
0.5 % 1 / 200 0.5 % 2 / 388
src/theory/bv/bv_quick_check.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/bv/bv_solver.h
61.5 % 16 / 26 0.0 % 0 / 8
src/theory/bv/bv_solver_bitblast.cpp
0.7 % 1 / 138 0.3 % 2 / 584
src/theory/bv/bv_solver_bitblast.h
0.0 % 0 / 6 0.0 % 0 / 2
src/theory/bv/bv_solver_lazy.cpp
88.2 % 343 / 389 45.6 % 756 / 1658
src/theory/bv/bv_solver_lazy.h
95.0 % 19 / 20 33.3 % 14 / 42
src/theory/bv/bv_solver_simple.cpp
53.2 % 33 / 62 29.8 % 62 / 208
src/theory/bv/bv_solver_simple.h
80.0 % 4 / 5 0.0 % 0 / 2
src/theory/bv/bv_subtheory.h
36.7 % 11 / 30 20.0 % 7 / 35
src/theory/bv/bv_subtheory_algebraic.cpp
0.3 % 2 / 604 0.1 % 3 / 2457
src/theory/bv/bv_subtheory_algebraic.h
0.0 % 0 / 18 0.0 % 0 / 10
src/theory/bv/bv_subtheory_bitblast.cpp
70.3 % 102 / 145 38.4 % 186 / 484
src/theory/bv/bv_subtheory_bitblast.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bv/bv_subtheory_core.cpp
85.5 % 265 / 310 45.4 % 539 / 1187
src/theory/bv/bv_subtheory_core.h
100.0 % 8 / 8 100.0 % 0 / 0
src/theory/bv/bv_subtheory_inequality.cpp
78.2 % 111 / 142 40.0 % 259 / 648
src/theory/bv/bv_subtheory_inequality.h
100.0 % 6 / 6 50.0 % 5 / 10
src/theory/bv/proof_checker.cpp
26.3 % 5 / 19 1.9 % 2 / 104
src/theory/bv/proof_checker.h
100.0 % 2 / 2 0.0 % 0 / 2
src/theory/bv/slicer.cpp
3.1 % 1 / 32 3.1 % 2 / 64
src/theory/bv/slicer.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/bv/theory_bv.cpp
85.4 % 76 / 89 39.1 % 59 / 151
src/theory/bv/theory_bv.h
0.0 % 0 / 1 0.0 % 0 / 2
src/theory/bv/theory_bv_rewrite_rules.h
29.6 % 74 / 250 23.4 % 5021 / 21496
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
87.9 % 131 / 149 44.4 % 322 / 726
src/theory/bv/theory_bv_rewrite_rules_core.h
100.0 % 144 / 144 57.6 % 265 / 460
src/theory/bv/theory_bv_rewrite_rules_normalization.h
92.3 % 671 / 727 47.7 % 1392 / 2919
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
75.8 % 270 / 356 34.3 % 441 / 1284
src/theory/bv/theory_bv_rewrite_rules_simplification.h
89.6 % 669 / 747 45.9 % 1968 / 4290
src/theory/bv/theory_bv_rewriter.cpp
94.6 % 297 / 314 50.5 % 446 / 884
src/theory/bv/theory_bv_rewriter.h
100.0 % 1 / 1 0.0 % 0 / 2
src/theory/bv/theory_bv_type_rules.h
71.1 % 101 / 142 30.5 % 145 / 476
src/theory/bv/theory_bv_utils.cpp
91.6 % 217 / 237 42.0 % 341 / 812
src/theory/bv/theory_bv_utils.h
100.0 % 18 / 18 40.2 % 41 / 102
src/theory/bv/type_enumerator.h
100.0 % 13 / 13 55.0 % 11 / 20
src/theory/care_graph.h
100.0 % 10 / 10 83.3 % 15 / 18
src/theory/combination_care_graph.cpp
100.0 % 33 / 33 52.2 % 48 / 92
src/theory/combination_engine.cpp
95.1 % 39 / 41 25.0 % 20 / 80
src/theory/datatypes/datatypes_rewriter.cpp
93.1 % 404 / 434 46.1 % 889 / 1928
src/theory/datatypes/datatypes_rewriter.h
100.0 % 1 / 1 35.0 % 7 / 20
src/theory/datatypes/infer_proof_cons.cpp
89.9 % 125 / 139 41.3 % 367 / 888
src/theory/datatypes/infer_proof_cons.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/datatypes/inference.cpp
75.0 % 18 / 24 35.5 % 39 / 110
src/theory/datatypes/inference.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/datatypes/inference_manager.cpp
100.0 % 62 / 62 54.5 % 133 / 244
src/theory/datatypes/proof_checker.cpp
80.6 % 58 / 72 26.8 % 126 / 470
src/theory/datatypes/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/datatypes/sygus_datatype_utils.cpp
85.9 % 324 / 377 38.4 % 661 / 1722
src/theory/datatypes/sygus_extension.cpp
85.1 % 854 / 1004 40.2 % 1992 / 4958
src/theory/datatypes/sygus_extension.h
100.0 % 5 / 5 50.0 % 1 / 2
src/theory/datatypes/sygus_simple_sym.cpp
92.9 % 261 / 281 50.9 % 563 / 1106
src/theory/datatypes/sygus_simple_sym.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/datatypes/theory_datatypes.cpp
89.2 % 1075 / 1205 45.3 % 2515 / 5547
src/theory/datatypes/theory_datatypes.h
88.2 % 15 / 17 47.5 % 19 / 40
src/theory/datatypes/theory_datatypes_type_rules.h
77.5 % 231 / 298 31.6 % 447 / 1416
src/theory/datatypes/theory_datatypes_utils.cpp
83.8 % 83 / 99 41.5 % 188 / 453
src/theory/datatypes/tuple_project_op.cpp
100.0 % 16 / 16 62.5 % 10 / 16
src/theory/datatypes/tuple_project_op.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/datatypes/type_enumerator.cpp
100.0 % 168 / 168 48.6 % 389 / 800
src/theory/datatypes/type_enumerator.h
100.0 % 48 / 48 54.3 % 50 / 92
src/theory/decision_manager.cpp
100.0 % 47 / 47 52.9 % 72 / 136
src/theory/decision_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/decision_strategy.cpp
95.2 % 59 / 62 53.1 % 85 / 160
src/theory/decision_strategy.h
100.0 % 5 / 5 100.0 % 0 / 0
src/theory/eager_proof_generator.cpp
93.7 % 59 / 63 40.9 % 81 / 198
src/theory/eager_proof_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/ee_manager.cpp
92.3 % 12 / 13 50.0 % 10 / 20
src/theory/ee_manager.h
75.0 % 3 / 4 100.0 % 0 / 0
src/theory/ee_manager_distributed.cpp
97.9 % 46 / 47 35.7 % 40 / 112
src/theory/ee_manager_distributed.h
44.4 % 4 / 9 100.0 % 0 / 0
src/theory/ee_setup_info.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/engine_output_channel.cpp
82.2 % 97 / 118 36.1 % 120 / 332
src/theory/engine_output_channel.h
100.0 % 1 / 1 0.0 % 0 / 2
src/theory/evaluator.cpp
76.3 % 377 / 494 38.2 % 678 / 1777
src/theory/evaluator.h
83.3 % 5 / 6 100.0 % 0 / 0
src/theory/ext_theory.cpp
71.1 % 175 / 246 35.9 % 307 / 854
src/theory/ext_theory.h
87.5 % 7 / 8 50.0 % 1 / 2
src/theory/fp/fp_converter.cpp
63.1 % 478 / 757 30.3 % 1007 / 3327
src/theory/fp/fp_converter.h
100.0 % 5 / 5 100.0 % 0 / 0
src/theory/fp/theory_fp.cpp
62.8 % 375 / 597 26.2 % 841 / 3214
src/theory/fp/theory_fp.h
85.7 % 6 / 7 0.0 % 0 / 2
src/theory/fp/theory_fp_rewriter.cpp
73.1 % 527 / 721 23.7 % 867 / 3655
src/theory/fp/theory_fp_rewriter.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/fp/theory_fp_type_rules.h
58.7 % 165 / 281 23.8 % 346 / 1452
src/theory/fp/type_enumerator.h
61.4 % 27 / 44 24.3 % 17 / 70
src/theory/inference_id.cpp
0.4 % 1 / 279 0.9 % 2 / 212
src/theory/inference_manager_buffered.cpp
92.8 % 77 / 83 35.7 % 55 / 154
src/theory/inference_manager_buffered.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/interrupted.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/lazy_tree_proof_generator.cpp
1.6 % 1 / 64 1.4 % 2 / 142
src/theory/lazy_tree_proof_generator.h
0.0 % 0 / 3 0.0 % 0 / 8
src/theory/logic_info.cpp
90.5 % 390 / 431 57.9 % 412 / 712
src/theory/logic_info.h
100.0 % 23 / 23 83.3 % 15 / 18
src/theory/model_manager.cpp
95.4 % 103 / 108 48.2 % 131 / 272
src/theory/model_manager_distributed.cpp
89.8 % 44 / 49 45.6 % 41 / 90
src/theory/output_channel.cpp
41.7 % 15 / 36 13.9 % 5 / 36
src/theory/output_channel.h
50.0 % 3 / 6 100.0 % 0 / 0
src/theory/quantifiers/alpha_equivalence.cpp
96.4 % 53 / 55 43.4 % 106 / 244
src/theory/quantifiers/alpha_equivalence.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/quantifiers/bv_inverter.cpp
93.0 % 186 / 200 44.8 % 475 / 1060
src/theory/quantifiers/bv_inverter.h
100.0 % 6 / 6 50.0 % 4 / 8
src/theory/quantifiers/bv_inverter_utils.cpp
98.9 % 811 / 820 48.7 % 2608 / 5352
src/theory/quantifiers/candidate_rewrite_database.cpp
66.7 % 88 / 132 29.8 % 143 / 480
src/theory/quantifiers/candidate_rewrite_database.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/candidate_rewrite_filter.cpp
91.3 % 115 / 126 42.7 % 269 / 630
src/theory/quantifiers/candidate_rewrite_filter.h
100.0 % 6 / 6 50.0 % 2 / 4
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
84.4 % 445 / 527 41.2 % 1156 / 2808
src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
100.0 % 2 / 2 72.7 % 16 / 22
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
85.4 % 299 / 350 39.1 % 671 / 1718
src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
100.0 % 3 / 3 50.0 % 1 / 2
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
100.0 % 171 / 171 41.8 % 445 / 1064
src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
91.4 % 64 / 70 50.2 % 159 / 317
src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
100.0 % 3 / 3 50.0 % 2 / 4
src/theory/quantifiers/cegqi/ceg_instantiator.cpp
91.2 % 817 / 896 49.0 % 1652 / 3372
src/theory/quantifiers/cegqi/ceg_instantiator.h
75.4 % 43 / 57 57.1 % 16 / 28
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
92.8 % 257 / 277 47.4 % 474 / 1000
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
100.0 % 3 / 3 50.0 % 2 / 4
src/theory/quantifiers/cegqi/nested_qe.cpp
89.7 % 70 / 78 44.5 % 146 / 328
src/theory/quantifiers/cegqi/nested_qe.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/cegqi/vts_term_cache.cpp
89.7 % 130 / 145 48.6 % 288 / 592
src/theory/quantifiers/cegqi/vts_term_cache.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/conjecture_generator.cpp
88.6 % 1246 / 1407 42.5 % 2560 / 6020
src/theory/quantifiers/conjecture_generator.h
86.0 % 43 / 50 61.1 % 22 / 36
src/theory/quantifiers/dynamic_rewrite.cpp
85.1 % 74 / 87 45.3 % 163 / 360
src/theory/quantifiers/dynamic_rewrite.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/ematching/candidate_generator.cpp
96.1 % 172 / 179 42.7 % 339 / 794
src/theory/quantifiers/ematching/candidate_generator.h
100.0 % 11 / 11 50.0 % 1 / 2
src/theory/quantifiers/ematching/ho_trigger.cpp
89.1 % 230 / 258 41.0 % 466 / 1136
src/theory/quantifiers/ematching/im_generator.cpp
100.0 % 8 / 8 50.0 % 2 / 4
src/theory/quantifiers/ematching/im_generator.h
33.3 % 2 / 6 100.0 % 0 / 0
src/theory/quantifiers/ematching/inst_match_generator.cpp
85.1 % 291 / 342 42.7 % 590 / 1382
src/theory/quantifiers/ematching/inst_match_generator.h
100.0 % 3 / 3 100.0 % 0 / 0
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
94.3 % 133 / 141 52.5 % 207 / 394
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
98.9 % 88 / 89 47.9 % 114 / 238
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
87.8 % 79 / 90 42.9 % 187 / 436
src/theory/quantifiers/ematching/inst_match_generator_simple.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/ematching/inst_strategy.cpp
76.9 % 10 / 13 18.8 % 3 / 16
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
75.3 % 265 / 352 36.9 % 494 / 1337
src/theory/quantifiers/ematching/inst_strategy_e_matching.h
100.0 % 3 / 3 71.4 % 10 / 14
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
63.8 % 51 / 80 36.4 % 86 / 236
src/theory/quantifiers/ematching/instantiation_engine.cpp
86.4 % 114 / 132 43.0 % 178 / 414
src/theory/quantifiers/ematching/instantiation_engine.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/ematching/pattern_term_selector.cpp
91.4 % 329 / 360 48.6 % 753 / 1548
src/theory/quantifiers/ematching/trigger.cpp
89.4 % 161 / 180 42.5 % 249 / 586
src/theory/quantifiers/ematching/trigger_term_info.cpp
100.0 % 42 / 42 76.1 % 102 / 134
src/theory/quantifiers/ematching/trigger_term_info.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/ematching/trigger_trie.cpp
100.0 % 29 / 29 59.5 % 25 / 42
src/theory/quantifiers/ematching/var_match_generator.cpp
96.9 % 31 / 32 52.0 % 52 / 100
src/theory/quantifiers/ematching/var_match_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/equality_query.cpp
78.0 % 71 / 91 38.3 % 167 / 436
src/theory/quantifiers/equality_query.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/expr_miner.cpp
92.7 % 38 / 41 41.2 % 47 / 114
src/theory/quantifiers/expr_miner.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/expr_miner_manager.cpp
55.8 % 43 / 77 34.3 % 48 / 140
src/theory/quantifiers/expr_miner_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/extended_rewrite.cpp
90.7 % 763 / 841 48.4 % 1840 / 3800
src/theory/quantifiers/extended_rewrite.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/first_order_model.cpp
92.5 % 149 / 161 46.3 % 241 / 520
src/theory/quantifiers/first_order_model.h
66.7 % 4 / 6 40.9 % 9 / 22
src/theory/quantifiers/fmf/bounded_integers.cpp
93.5 % 487 / 521 45.3 % 1218 / 2690
src/theory/quantifiers/fmf/bounded_integers.h
100.0 % 14 / 14 62.5 % 10 / 16
src/theory/quantifiers/fmf/first_order_model_fmc.cpp
100.0 % 69 / 69 48.8 % 124 / 254
src/theory/quantifiers/fmf/full_model_check.cpp
93.6 % 743 / 794 50.2 % 1614 / 3213
src/theory/quantifiers/fmf/full_model_check.h
100.0 % 13 / 13 50.0 % 3 / 6
src/theory/quantifiers/fmf/model_builder.cpp
50.0 % 32 / 64 19.0 % 44 / 232
src/theory/quantifiers/fmf/model_builder.h
83.3 % 5 / 6 100.0 % 0 / 0
src/theory/quantifiers/fmf/model_engine.cpp
70.1 % 124 / 177 33.0 % 218 / 660
src/theory/quantifiers/fmf/model_engine.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/fun_def_evaluator.cpp
90.2 % 129 / 143 42.0 % 321 / 764
src/theory/quantifiers/fun_def_evaluator.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/index_trie.cpp
97.7 % 42 / 43 56.1 % 55 / 98
src/theory/quantifiers/index_trie.h
100.0 % 9 / 9 100.0 % 0 / 0
src/theory/quantifiers/inst_match.cpp
56.5 % 26 / 46 16.9 % 24 / 142
src/theory/quantifiers/inst_match.h
7.1 % 1 / 14 0.0 % 0 / 8
src/theory/quantifiers/inst_match_trie.cpp
45.2 % 70 / 155 21.1 % 83 / 394
src/theory/quantifiers/inst_match_trie.h
100.0 % 10 / 10 50.0 % 1 / 2
src/theory/quantifiers/inst_strategy_enumerative.cpp
84.2 % 80 / 95 43.8 % 133 / 304
src/theory/quantifiers/inst_strategy_enumerative.h
100.0 % 3 / 3 50.0 % 1 / 2
src/theory/quantifiers/instantiate.cpp
76.7 % 257 / 335 36.1 % 492 / 1364
src/theory/quantifiers/instantiate.h
100.0 % 3 / 3 50.0 % 1 / 2
src/theory/quantifiers/instantiation_list.cpp
100.0 % 7 / 7 20.0 % 2 / 10
src/theory/quantifiers/instantiation_list.h
100.0 % 6 / 6 50.0 % 2 / 4
src/theory/quantifiers/lazy_trie.cpp
93.6 % 73 / 78 39.5 % 124 / 314
src/theory/quantifiers/lazy_trie.h
100.0 % 6 / 6 50.0 % 1 / 2
src/theory/quantifiers/proof_checker.cpp
72.4 % 42 / 58 24.8 % 67 / 270
src/theory/quantifiers/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/quant_bound_inference.cpp
100.0 % 50 / 50 56.8 % 83 / 146
src/theory/quantifiers/quant_bound_inference.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/quant_conflict_find.cpp
82.9 % 1157 / 1395 45.5 % 2475 / 5441
src/theory/quantifiers/quant_conflict_find.h
100.0 % 18 / 18 52.8 % 19 / 36
src/theory/quantifiers/quant_module.cpp
92.0 % 23 / 25 43.8 % 7 / 16
src/theory/quantifiers/quant_module.h
81.8 % 9 / 11 100.0 % 0 / 0
src/theory/quantifiers/quant_relevance.cpp
95.0 % 19 / 20 58.3 % 21 / 36
src/theory/quantifiers/quant_relevance.h
50.0 % 2 / 4 0.0 % 0 / 2
src/theory/quantifiers/quant_rep_bound_ext.cpp
96.2 % 25 / 26 43.1 % 25 / 58
src/theory/quantifiers/quant_rep_bound_ext.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/quant_split.cpp
98.0 % 98 / 100 51.3 % 198 / 386
src/theory/quantifiers/quant_split.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/quant_util.cpp
81.9 % 68 / 83 41.5 % 93 / 224
src/theory/quantifiers/quant_util.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/quantifiers/quantifiers_attributes.cpp
71.8 % 148 / 206 41.7 % 344 / 824
src/theory/quantifiers/quantifiers_attributes.h
100.0 % 7 / 7 50.0 % 4 / 8
src/theory/quantifiers/quantifiers_inference_manager.cpp
100.0 % 10 / 10 40.0 % 4 / 10
src/theory/quantifiers/quantifiers_modules.cpp
100.0 % 55 / 55 61.8 % 84 / 136
src/theory/quantifiers/quantifiers_registry.cpp
77.9 % 74 / 95 36.8 % 84 / 228
src/theory/quantifiers/quantifiers_registry.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/quantifiers_rewriter.cpp
76.4 % 892 / 1167 40.2 % 2043 / 5077
src/theory/quantifiers/quantifiers_rewriter.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/quantifiers_state.cpp
50.0 % 40 / 80 25.0 % 61 / 244
src/theory/quantifiers/quantifiers_state.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/query_generator.cpp
0.9 % 2 / 223 0.3 % 2 / 684
src/theory/quantifiers/query_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/relevant_domain.cpp
98.5 % 198 / 201 54.1 % 491 / 908
src/theory/quantifiers/relevant_domain.h
100.0 % 12 / 12 50.0 % 1 / 2
src/theory/quantifiers/single_inv_partition.cpp
88.9 % 273 / 307 48.2 % 498 / 1034
src/theory/quantifiers/single_inv_partition.h
100.0 % 7 / 7 83.3 % 5 / 6
src/theory/quantifiers/skolemize.cpp
89.4 % 185 / 207 41.8 % 429 / 1026
src/theory/quantifiers/skolemize.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/solution_filter.cpp
62.2 % 28 / 45 27.9 % 48 / 172
src/theory/quantifiers/solution_filter.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
96.8 % 272 / 281 45.5 % 576 / 1266
src/theory/quantifiers/sygus/ce_guided_single_inv.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
81.3 % 496 / 610 41.8 % 1314 / 3146
src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/cegis.cpp
93.9 % 323 / 344 47.1 % 612 / 1300
src/theory/quantifiers/sygus/cegis.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/cegis_core_connective.cpp
88.6 % 403 / 455 42.5 % 796 / 1871
src/theory/quantifiers/sygus/cegis_core_connective.h
100.0 % 6 / 6 50.0 % 3 / 6
src/theory/quantifiers/sygus/cegis_unif.cpp
87.1 % 303 / 348 36.8 % 511 / 1388
src/theory/quantifiers/sygus/cegis_unif.h
100.0 % 5 / 5 50.0 % 13 / 26
src/theory/quantifiers/sygus/enum_stream_substitution.cpp
66.7 % 230 / 345 29.2 % 326 / 1118
src/theory/quantifiers/sygus/enum_stream_substitution.h
100.0 % 6 / 6 50.0 % 2 / 4
src/theory/quantifiers/sygus/example_eval_cache.cpp
98.0 % 50 / 51 38.5 % 70 / 182
src/theory/quantifiers/sygus/example_infer.cpp
83.7 % 103 / 123 35.6 % 165 / 464
src/theory/quantifiers/sygus/example_min_eval.cpp
100.0 % 30 / 30 42.6 % 46 / 108
src/theory/quantifiers/sygus/example_min_eval.h
100.0 % 5 / 5 50.0 % 1 / 2
src/theory/quantifiers/sygus/sygus_abduct.cpp
98.8 % 82 / 83 46.6 % 208 / 446
src/theory/quantifiers/sygus/sygus_enumerator.cpp
87.9 % 579 / 659 40.3 % 928 / 2300
src/theory/quantifiers/sygus/sygus_enumerator.h
100.0 % 9 / 9 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
5.9 % 1 / 17 4.8 % 2 / 42
src/theory/quantifiers/sygus/sygus_enumerator_basic.h
0.0 % 0 / 4 0.0 % 0 / 2
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
97.3 % 180 / 185 42.0 % 392 / 934
src/theory/quantifiers/sygus/sygus_eval_unfold.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_explain.cpp
95.7 % 157 / 164 37.1 % 292 / 788
src/theory/quantifiers/sygus/sygus_explain.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
87.6 % 787 / 898 41.9 % 1458 / 3478
src/theory/quantifiers/sygus/sygus_grammar_cons.h
100.0 % 4 / 4 50.0 % 2 / 4
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
49.2 % 126 / 256 20.3 % 223 / 1098
src/theory/quantifiers/sygus/sygus_grammar_norm.h
40.0 % 8 / 20 2.6 % 1 / 38
src/theory/quantifiers/sygus/sygus_grammar_red.cpp
97.5 % 77 / 79 44.8 % 171 / 382
src/theory/quantifiers/sygus/sygus_grammar_red.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_interpol.cpp
84.4 % 151 / 179 39.9 % 271 / 680
src/theory/quantifiers/sygus/sygus_interpol.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_invariance.cpp
80.4 % 111 / 138 38.2 % 203 / 532
src/theory/quantifiers/sygus/sygus_invariance.h
95.0 % 19 / 20 50.0 % 14 / 28
src/theory/quantifiers/sygus/sygus_module.cpp
100.0 % 5 / 5 33.3 % 2 / 6
src/theory/quantifiers/sygus/sygus_module.h
40.0 % 2 / 5 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_pbe.cpp
100.0 % 119 / 119 43.6 % 223 / 512
src/theory/quantifiers/sygus/sygus_process_conj.cpp
90.7 % 353 / 389 44.0 % 622 / 1414
src/theory/quantifiers/sygus/sygus_process_conj.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
98.8 % 81 / 82 47.3 % 178 / 376
src/theory/quantifiers/sygus/sygus_qe_preproc.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_repair_const.cpp
90.3 % 299 / 331 41.2 % 591 / 1436
src/theory/quantifiers/sygus/sygus_repair_const.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_stats.cpp
100.0 % 24 / 24 50.0 % 38 / 76
src/theory/quantifiers/sygus/sygus_unif.cpp
91.4 % 53 / 58 35.0 % 49 / 140
src/theory/quantifiers/sygus/sygus_unif_io.cpp
90.8 % 746 / 822 40.8 % 1344 / 3296
src/theory/quantifiers/sygus/sygus_unif_io.h
100.0 % 13 / 13 60.0 % 6 / 10
src/theory/quantifiers/sygus/sygus_unif_rl.cpp
68.4 % 436 / 637 29.7 % 738 / 2486
src/theory/quantifiers/sygus/sygus_unif_rl.h
100.0 % 7 / 7 30.4 % 14 / 46
src/theory/quantifiers/sygus/sygus_unif_strat.cpp
83.2 % 474 / 570 42.8 % 928 / 2166
src/theory/quantifiers/sygus/sygus_unif_strat.h
100.0 % 18 / 18 50.0 % 3 / 6
src/theory/quantifiers/sygus/sygus_utils.cpp
75.0 % 57 / 76 30.1 % 110 / 366
src/theory/quantifiers/sygus/synth_conjecture.cpp
87.4 % 601 / 688 40.8 % 1283 / 3146
src/theory/quantifiers/sygus/synth_conjecture.h
100.0 % 9 / 9 100.0 % 0 / 0
src/theory/quantifiers/sygus/synth_engine.cpp
95.7 % 134 / 140 53.9 % 220 / 408
src/theory/quantifiers/sygus/synth_engine.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/sygus/template_infer.cpp
97.9 % 93 / 95 44.4 % 239 / 538
src/theory/quantifiers/sygus/template_infer.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/sygus/term_database_sygus.cpp
86.6 % 479 / 553 42.2 % 869 / 2061
src/theory/quantifiers/sygus/term_database_sygus.h
100.0 % 7 / 7 62.5 % 5 / 8
src/theory/quantifiers/sygus/transition_inference.cpp
93.9 % 278 / 296 46.6 % 521 / 1118
src/theory/quantifiers/sygus/transition_inference.h
100.0 % 12 / 12 50.0 % 4 / 8
src/theory/quantifiers/sygus/type_info.cpp
84.5 % 197 / 233 39.8 % 311 / 782
src/theory/quantifiers/sygus/type_info.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/type_node_id_trie.cpp
100.0 % 15 / 15 66.7 % 12 / 18
src/theory/quantifiers/sygus/type_node_id_trie.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus_inst.cpp
83.1 % 211 / 254 37.2 % 379 / 1020
src/theory/quantifiers/sygus_inst.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/sygus_sampler.cpp
79.5 % 368 / 463 38.1 % 587 / 1542
src/theory/quantifiers/sygus_sampler.h
100.0 % 3 / 3 100.0 % 0 / 0
src/theory/quantifiers/term_database.cpp
81.5 % 549 / 674 42.7 % 1274 / 2982
src/theory/quantifiers/term_database.h
100.0 % 3 / 3 50.0 % 2 / 4
src/theory/quantifiers/term_enumeration.cpp
55.2 % 16 / 29 31.4 % 27 / 86
src/theory/quantifiers/term_enumeration.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/term_registry.cpp
84.6 % 33 / 39 40.5 % 51 / 126
src/theory/quantifiers/term_registry.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/term_tuple_enumerator.cpp
74.0 % 142 / 192 39.2 % 224 / 572
src/theory/quantifiers/term_tuple_enumerator.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/term_util.cpp
84.9 % 264 / 311 55.5 % 567 / 1022
src/theory/quantifiers/theory_quantifiers.cpp
95.3 % 81 / 85 51.9 % 110 / 212
src/theory/quantifiers/theory_quantifiers.h
33.3 % 1 / 3 0.0 % 0 / 2
src/theory/quantifiers/theory_quantifiers_type_rules.h
81.6 % 40 / 49 32.2 % 114 / 354
src/theory/quantifiers_engine.cpp
85.8 % 321 / 374 42.2 % 527 / 1248
src/theory/relevance_manager.cpp
71.8 % 102 / 142 28.1 % 142 / 506
src/theory/relevance_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/rep_set.cpp
74.1 % 186 / 251 34.8 % 276 / 792
src/theory/rep_set.h
64.3 % 9 / 14 100.0 % 0 / 0
src/theory/rewriter.cpp
87.6 % 169 / 193 43.2 % 331 / 766
src/theory/rewriter.h
100.0 % 1 / 1 75.0 % 12 / 16
src/theory/rewriter_attributes.h
100.0 % 30 / 30 43.9 % 616 / 1404
src/theory/sep/theory_sep.cpp
84.4 % 916 / 1085 41.7 % 2281 / 5476
src/theory/sep/theory_sep.h
56.3 % 18 / 32 20.6 % 21 / 102
src/theory/sep/theory_sep_rewriter.cpp
88.4 % 84 / 95 44.9 % 180 / 401
src/theory/sep/theory_sep_rewriter.h
100.0 % 4 / 4 50.0 % 10 / 20
src/theory/sep/theory_sep_type_rules.h
90.7 % 39 / 43 22.9 % 44 / 192
src/theory/sets/cardinality_extension.cpp
89.7 % 514 / 573 46.6 % 1215 / 2605
src/theory/sets/cardinality_extension.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/sets/inference_manager.cpp
50.0 % 43 / 86 24.3 % 92 / 378
src/theory/sets/inference_manager.h
100.0 % 1 / 1 0.0 % 0 / 2
src/theory/sets/normal_form.h
97.0 % 65 / 67 49.7 % 170 / 342
src/theory/sets/rels_utils.h
100.0 % 44 / 44 50.0 % 73 / 146
src/theory/sets/singleton_op.cpp
85.7 % 12 / 14 43.8 % 7 / 16
src/theory/sets/singleton_op.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/sets/skolem_cache.cpp
100.0 % 19 / 19 48.8 % 40 / 82
src/theory/sets/skolem_cache.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/sets/solver_state.cpp
92.8 % 272 / 293 46.7 % 570 / 1220
src/theory/sets/solver_state.h
100.0 % 2 / 2 75.0 % 3 / 4
src/theory/sets/term_registry.cpp
80.3 % 61 / 76 44.3 % 117 / 264
src/theory/sets/term_registry.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/sets/theory_sets.cpp
92.6 % 100 / 108 47.5 % 150 / 316
src/theory/sets/theory_sets.h
80.0 % 4 / 5 0.0 % 0 / 2
src/theory/sets/theory_sets_private.cpp
94.2 % 654 / 694 47.0 % 1432 / 3048
src/theory/sets/theory_sets_private.h
66.7 % 2 / 3 0.0 % 0 / 2
src/theory/sets/theory_sets_rels.cpp
95.6 % 755 / 790 52.0 % 1709 / 3285
src/theory/sets/theory_sets_rels.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/sets/theory_sets_rewriter.cpp
94.8 % 326 / 344 48.5 % 915 / 1885
src/theory/sets/theory_sets_rewriter.h
100.0 % 1 / 1 25.0 % 1 / 4
src/theory/sets/theory_sets_type_enumerator.cpp
100.0 % 61 / 61 46.2 % 86 / 186
src/theory/sets/theory_sets_type_rules.h
77.2 % 159 / 206 26.2 % 291 / 1112
src/theory/shared_solver.cpp
67.4 % 29 / 43 45.0 % 45 / 100
src/theory/shared_solver.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/shared_solver_distributed.cpp
100.0 % 35 / 35 54.9 % 56 / 102
src/theory/shared_solver_distributed.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/shared_terms_database.cpp
85.6 % 131 / 153 32.1 % 222 / 692
src/theory/shared_terms_database.h
100.0 % 24 / 24 31.3 % 10 / 32
src/theory/skolem_lemma.cpp
100.0 % 14 / 14 32.9 % 25 / 76
src/theory/skolem_lemma.h
100.0 % 1 / 1 50.0 % 2 / 4
src/theory/smt_engine_subsolver.cpp
81.3 % 39 / 48 34.1 % 45 / 132
src/theory/sort_inference.cpp
84.2 % 437 / 519 45.7 % 1016 / 2224
src/theory/sort_inference.h
83.3 % 5 / 6 100.0 % 0 / 0
src/theory/strings/arith_entail.cpp
89.6 % 344 / 384 45.8 % 878 / 1918
src/theory/strings/base_solver.cpp
78.6 % 297 / 378 39.2 % 625 / 1593
src/theory/strings/base_solver.h
100.0 % 2 / 2 50.0 % 2 / 4
src/theory/strings/core_solver.cpp
80.6 % 1104 / 1370 40.1 % 2534 / 6319
src/theory/strings/core_solver.h
100.0 % 2 / 2 40.9 % 9 / 22
src/theory/strings/eager_solver.cpp
98.5 % 65 / 66 53.5 % 122 / 228
src/theory/strings/eqc_info.cpp
100.0 % 57 / 57 44.6 % 148 / 332
src/theory/strings/eqc_info.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/extf_solver.cpp
91.5 % 311 / 340 46.7 % 788 / 1686
src/theory/strings/extf_solver.h
100.0 % 4 / 4 50.0 % 1 / 2
src/theory/strings/infer_info.cpp
69.7 % 23 / 33 36.8 % 39 / 106
src/theory/strings/infer_info.h
100.0 % 2 / 2 50.0 % 4 / 8
src/theory/strings/infer_proof_cons.cpp
83.8 % 449 / 536 40.7 % 888 / 2182
src/theory/strings/infer_proof_cons.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/inference_manager.cpp
88.2 % 164 / 186 44.8 % 358 / 800
src/theory/strings/inference_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/normal_form.cpp
100.0 % 84 / 84 43.9 % 150 / 342
src/theory/strings/normal_form.h
100.0 % 2 / 2 50.0 % 3 / 6
src/theory/strings/proof_checker.cpp
80.4 % 238 / 296 31.0 % 573 / 1846
src/theory/strings/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/strings/regexp_elim.cpp
78.3 % 231 / 295 34.3 % 465 / 1356
src/theory/strings/regexp_elim.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/regexp_entail.cpp
87.3 % 330 / 378 47.7 % 683 / 1431
src/theory/strings/regexp_operation.cpp
72.2 % 721 / 998 36.1 % 1525 / 4222
src/theory/strings/regexp_solver.cpp
89.4 % 305 / 341 48.4 % 610 / 1261
src/theory/strings/regexp_solver.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/rewrites.cpp
0.5 % 1 / 195 1.0 % 2 / 191
src/theory/strings/sequences_rewriter.cpp
95.8 % 1524 / 1591 51.3 % 4734 / 9230
src/theory/strings/sequences_rewriter.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/sequences_stats.cpp
100.0 % 28 / 28 48.9 % 46 / 94
src/theory/strings/skolem_cache.cpp
90.8 % 118 / 130 49.6 % 286 / 577
src/theory/strings/skolem_cache.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/solver_state.cpp
95.3 % 101 / 106 46.2 % 156 / 338
src/theory/strings/strategy.cpp
70.7 % 58 / 82 35.1 % 87 / 248
src/theory/strings/strings_entail.cpp
96.4 % 425 / 441 47.3 % 955 / 2017
src/theory/strings/strings_fmf.cpp
93.0 % 40 / 43 53.3 % 48 / 90
src/theory/strings/strings_fmf.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/strings_rewriter.cpp
100.0 % 161 / 161 48.2 % 422 / 876
src/theory/strings/strings_rewriter.h
100.0 % 1 / 1 25.0 % 2 / 8
src/theory/strings/term_registry.cpp
91.3 % 272 / 298 47.5 % 646 / 1360
src/theory/strings/theory_strings.cpp
82.0 % 469 / 572 42.3 % 1008 / 2383
src/theory/strings/theory_strings.h
100.0 % 32 / 32 52.3 % 69 / 132
src/theory/strings/theory_strings_preprocess.cpp
100.0 % 490 / 490 51.2 % 1447 / 2826
src/theory/strings/theory_strings_type_rules.h
68.7 % 103 / 150 26.0 % 134 / 516
src/theory/strings/theory_strings_utils.cpp
90.6 % 174 / 192 44.9 % 320 / 712
src/theory/strings/type_enumerator.cpp
85.4 % 117 / 137 33.1 % 78 / 236
src/theory/strings/type_enumerator.h
100.0 % 7 / 7 100.0 % 0 / 0
src/theory/strings/word.cpp
82.6 % 233 / 282 29.7 % 305 / 1028
src/theory/subs_minimize.cpp
0.4 % 1 / 223 0.2 % 2 / 832
src/theory/substitutions.cpp
85.6 % 95 / 111 41.4 % 226 / 546
src/theory/substitutions.h
91.3 % 21 / 23 45.0 % 9 / 20
src/theory/term_registration_visitor.cpp
80.1 % 109 / 136 40.8 % 226 / 554
src/theory/term_registration_visitor.h
100.0 % 9 / 9 50.0 % 1 / 2
src/theory/theory.cpp
84.2 % 208 / 247 45.4 % 391 / 861
src/theory/theory.h
77.3 % 75 / 97 41.2 % 70 / 170
src/theory/theory_engine.cpp
80.7 % 692 / 857 40.7 % 1791 / 4402
src/theory/theory_engine.h
100.0 % 47 / 47 28.0 % 103 / 368
src/theory/theory_engine_proof_generator.cpp
80.0 % 48 / 60 35.2 % 93 / 264
src/theory/theory_engine_proof_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/theory_eq_notify.h
78.9 % 15 / 19 58.3 % 14 / 24
src/theory/theory_id.cpp
85.9 % 67 / 78 57.7 % 56 / 97
src/theory/theory_inference.cpp
76.5 % 13 / 17 26.7 % 8 / 30
src/theory/theory_inference.h
72.7 % 8 / 11 50.0 % 1 / 2
src/theory/theory_inference_manager.cpp
82.1 % 170 / 207 40.6 % 185 / 456
src/theory/theory_model.cpp
88.1 % 378 / 429 41.8 % 792 / 1895
src/theory/theory_model.h
100.0 % 4 / 4 50.0 % 1 / 2
src/theory/theory_model_builder.cpp
94.3 % 626 / 664 43.9 % 1224 / 2789
src/theory/theory_model_builder.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/theory_preprocessor.cpp
93.1 % 201 / 216 45.2 % 476 / 1054
src/theory/theory_proof_step_buffer.cpp
83.0 % 83 / 100 41.5 % 142 / 342
src/theory/theory_proof_step_buffer.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/theory_rewriter.cpp
88.9 % 16 / 18 46.0 % 23 / 50
src/theory/theory_rewriter.h
83.3 % 5 / 6 100.0 % 0 / 0
src/theory/theory_state.cpp
100.0 % 71 / 71 41.6 % 79 / 190
src/theory/theory_state.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/trust_node.cpp
77.4 % 48 / 62 34.7 % 70 / 202
src/theory/trust_node.h
100.0 % 3 / 3 100.0 % 0 / 0
src/theory/trust_substitutions.cpp
92.2 % 95 / 103 48.9 % 228 / 466
src/theory/trust_substitutions.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/type_enumerator.h
92.7 % 51 / 55 25.0 % 41 / 164
src/theory/type_set.cpp
96.6 % 57 / 59 57.7 % 60 / 104
src/theory/type_set.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/uf/cardinality_extension.cpp
80.5 % 815 / 1013 40.8 % 1694 / 4150
src/theory/uf/cardinality_extension.h
96.4 % 53 / 55 36.5 % 38 / 104
src/theory/uf/eq_proof.cpp
78.1 % 560 / 717 35.5 % 1345 / 3784
src/theory/uf/eq_proof.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/uf/equality_engine.cpp
91.7 % 1263 / 1378 43.8 % 2454 / 5608
src/theory/uf/equality_engine.h
94.9 % 37 / 39 14.7 % 5 / 34
src/theory/uf/equality_engine_iterator.cpp
78.3 % 47 / 60 20.7 % 38 / 184
src/theory/uf/equality_engine_notify.h
63.6 % 7 / 11 100.0 % 0 / 0
src/theory/uf/equality_engine_types.h
75.3 % 61 / 81 32.4 % 11 / 34
src/theory/uf/ho_extension.cpp
83.7 % 200 / 239 41.0 % 420 / 1024
src/theory/uf/ho_extension.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/uf/proof_checker.cpp
88.7 % 102 / 115 31.0 % 175 / 564
src/theory/uf/proof_checker.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/uf/proof_equality_engine.cpp
69.5 % 182 / 262 31.3 % 411 / 1314
src/theory/uf/proof_equality_engine.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/uf/symmetry_breaker.cpp
83.1 % 414 / 498 43.5 % 978 / 2248
src/theory/uf/symmetry_breaker.h
100.0 % 7 / 7 22.2 % 4 / 18
src/theory/uf/theory_uf.cpp
87.5 % 274 / 313 48.4 % 623 / 1288
src/theory/uf/theory_uf.h
94.7 % 18 / 19 48.4 % 30 / 62
src/theory/uf/theory_uf_model.cpp
57.8 % 74 / 128 32.1 % 142 / 442
src/theory/uf/theory_uf_model.h
100.0 % 16 / 16 53.3 % 16 / 30
src/theory/uf/theory_uf_rewriter.h
91.3 % 84 / 92 48.4 % 214 / 442
src/theory/uf/theory_uf_type_rules.h
67.6 % 50 / 74 27.4 % 86 / 314
src/theory/valuation.cpp
64.8 % 70 / 108 15.8 % 51 / 323
src/theory/valuation.h
100.0 % 3 / 3 100.0 % 0 / 0
src/util/abstract_value.cpp
100.0 % 6 / 6 31.3 % 5 / 16
src/util/abstract_value.h
100.0 % 6 / 6 50.0 % 1 / 2
src/util/bin_heap.h
98.8 % 163 / 165 21.8 % 123 / 564
src/util/bitvector.cpp
100.0 % 171 / 171 56.3 % 178 / 316
src/util/bitvector.h
91.7 % 66 / 72 66.7 % 22 / 33
src/util/bool.h
100.0 % 2 / 2 100.0 % 0 / 0
src/util/cardinality.cpp
79.2 % 114 / 144 48.3 % 223 / 462
src/util/cardinality.h
100.0 % 25 / 25 54.5 % 12 / 22
src/util/dense_map.h
82.0 % 91 / 111 13.0 % 75 / 577
src/util/divisible.cpp
100.0 % 4 / 4 35.7 % 5 / 14
src/util/divisible.h
71.4 % 5 / 7 100.0 % 0 / 0
src/util/floatingpoint.cpp
73.6 % 206 / 280 29.6 % 235 / 794
src/util/floatingpoint.h
90.2 % 55 / 61 50.0 % 2 / 4
src/util/floatingpoint_literal_symfpu.cpp
92.5 % 111 / 120 25.0 % 67 / 268
src/util/floatingpoint_size.cpp
100.0 % 10 / 10 12.5 % 8 / 64
src/util/floatingpoint_size.h
100.0 % 16 / 16 50.0 % 2 / 4
src/util/hash.h
100.0 % 7 / 7 50.0 % 4 / 8
src/util/iand.h
50.0 % 2 / 4 100.0 % 0 / 0
src/util/indexed_root_predicate.h
0.0 % 0 / 6 100.0 % 0 / 0
src/util/integer_cln_imp.cpp
91.6 % 219 / 239 41.9 % 224 / 535
src/util/integer_cln_imp.h
100.0 % 18 / 18 83.3 % 5 / 6
src/util/maybe.h
51.9 % 14 / 27 9.1 % 2 / 22
src/util/ostream_util.cpp
100.0 % 7 / 7 100.0 % 0 / 0
src/util/random.cpp
100.0 % 24 / 24 13.4 % 11 / 82
src/util/random.h
100.0 % 3 / 3 100.0 % 2 / 2
src/util/rational_cln_imp.cpp
70.8 % 34 / 48 31.7 % 38 / 120
src/util/rational_cln_imp.h
91.4 % 96 / 105 43.4 % 46 / 106
src/util/regexp.cpp
76.5 % 13 / 17 50.0 % 2 / 4
src/util/resource_manager.cpp
77.2 % 176 / 228 38.4 % 113 / 294
src/util/resource_manager.h
100.0 % 2 / 2 66.7 % 4 / 6
src/util/result.cpp
62.6 % 124 / 198 34.6 % 79 / 228
src/util/result.h
100.0 % 14 / 14 75.0 % 9 / 12
src/util/roundingmode.h
100.0 % 1 / 1 100.0 % 0 / 0
src/util/safe_print.cpp
71.6 % 73 / 102 51.2 % 43 / 84
src/util/safe_print.h
86.7 % 13 / 15 15.6 % 5 / 32
src/util/sampler.cpp
9.5 % 7 / 74 5.9 % 12 / 203
src/util/sexpr.cpp
53.6 % 97 / 181 25.1 % 91 / 363
src/util/sexpr.h
62.5 % 5 / 8 100.0 % 0 / 0
src/util/smt2_quote_string.cpp
100.0 % 8 / 8 77.3 % 17 / 22
src/util/statistics.cpp
17.1 % 12 / 70 4.8 % 3 / 62
src/util/statistics.h
80.0 % 4 / 5 100.0 % 0 / 0
src/util/statistics_registry.cpp
60.7 % 17 / 28 16.0 % 8 / 50
src/util/statistics_registry.h
16.7 % 2 / 12 0.0 % 0 / 2
src/util/stats_base.cpp
80.6 % 29 / 36 30.8 % 8 / 26
src/util/stats_base.h
87.0 % 40 / 46 36.8 % 39 / 106
src/util/stats_histogram.h
97.5 % 39 / 40 53.4 % 31 / 58
src/util/stats_timer.cpp
95.2 % 40 / 42 36.1 % 26 / 72
src/util/stats_timer.h
100.0 % 6 / 6 50.0 % 6 / 12
src/util/stats_utils.cpp
100.0 % 6 / 6 50.0 % 11 / 22
src/util/string.cpp
95.8 % 249 / 260 58.1 % 280 / 482
src/util/string.h
95.8 % 23 / 24 50.0 % 4 / 8
src/util/tuple.h
71.4 % 5 / 7 100.0 % 0 / 0
src/util/utility.cpp
0.0 % 0 / 16 0.0 % 0 / 26
src/util/utility.h
100.0 % 15 / 15 35.3 % 18 / 51
test/api/boilerplate.cpp
100.0 % 5 / 5 50.0 % 7 / 14
test/api/issue4889.cpp
100.0 % 15 / 15 50.0 % 16 / 32
test/api/issue5074.cpp
100.0 % 9 / 9 50.0 % 14 / 28
test/api/ouroborous.cpp
91.1 % 72 / 79 50.2 % 127 / 253
test/api/reset_assertions.cpp
100.0 % 20 / 20 50.0 % 28 / 56
test/api/sep_log_api.cpp
84.7 % 83 / 98 50.9 % 115 / 226
test/api/smt2_compliance.cpp
100.0 % 33 / 33 50.0 % 45 / 90
test/api/two_solvers.cpp
100.0 % 7 / 7 50.0 % 12 / 24
test/unit/api/datatype_api_black.cpp
100.0 % 376 / 376 33.7 % 1009 / 2992
test/unit/api/grammar_black.cpp
100.0 % 60 / 60 35.9 % 235 / 654
test/unit/api/op_black.cpp
100.0 % 94 / 94 30.4 % 196 / 644
test/unit/api/op_white.cpp
100.0 % 7 / 7 30.0 % 18 / 60
test/unit/api/result_black.cpp
100.0 % 75 / 75 34.1 % 198 / 580
test/unit/api/solver_black.cpp
99.2 % 1536 / 1548 35.9 % 6007 / 16742
test/unit/api/solver_white.cpp
100.0 % 21 / 21 41.0 % 55 / 134
test/unit/api/sort_black.cpp
100.0 % 370 / 370 33.2 % 1170 / 3524
test/unit/api/term_black.cpp
100.0 % 699 / 699 31.9 % 2924 / 9160
test/unit/api/term_white.cpp
100.0 % 42 / 42 40.6 % 121 / 298
test/unit/base/map_util_black.cpp
100.0 % 103 / 103 29.9 % 332 / 1110
test/unit/context/cdhashmap_black.cpp
100.0 % 88 / 88 28.8 % 247 / 857
test/unit/context/cdhashmap_white.cpp
100.0 % 10 / 10 25.0 % 66 / 264
test/unit/context/cdlist_black.cpp
100.0 % 75 / 75 29.9 % 107 / 358
test/unit/context/cdo_black.cpp
100.0 % 13 / 13 26.7 % 23 / 86
test/unit/context/context_black.cpp
96.7 % 87 / 90 23.7 % 167 / 706
test/unit/context/context_mm_black.cpp
97.1 % 34 / 35 36.4 % 39 / 107
test/unit/context/context_white.cpp
100.0 % 117 / 117 22.0 % 318 / 1444
test/unit/main/interactive_shell_black.cpp
100.0 % 58 / 58 45.2 % 56 / 124
test/unit/memory.h
100.0 % 12 / 12 21.4 % 6 / 28
test/unit/node/attribute_black.cpp
100.0 % 47 / 47 32.3 % 95 / 294
test/unit/node/attribute_white.cpp
100.0 % 314 / 314 28.6 % 1007 / 3526
test/unit/node/kind_black.cpp
100.0 % 32 / 32 28.9 % 55 / 190
test/unit/node/kind_map_black.cpp
100.0 % 10 / 10 29.5 % 23 / 78
test/unit/node/node_algorithm_black.cpp
100.0 % 93 / 93 35.1 % 311 / 886
test/unit/node/node_black.cpp
99.8 % 446 / 447 33.7 % 1522 / 4513
test/unit/node/node_builder_black.cpp
100.0 % 326 / 326 27.8 % 1532 / 5508
test/unit/node/node_manager_black.cpp
100.0 % 210 / 210 30.7 % 651 / 2120
test/unit/node/node_manager_white.cpp
100.0 % 32 / 32 30.1 % 126 / 418
test/unit/node/node_self_iterator_black.cpp
100.0 % 22 / 22 30.0 % 84 / 280
test/unit/node/node_traversal_black.cpp
100.0 % 170 / 170 39.1 % 478 / 1224
test/unit/node/node_white.cpp
100.0 % 35 / 35 31.4 % 108 / 344
test/unit/node/symbol_table_black.cpp
100.0 % 74 / 74 34.4 % 203 / 590
test/unit/node/type_cardinality_black.cpp
100.0 % 210 / 210 35.5 % 532 / 1498
test/unit/node/type_node_white.cpp
100.0 % 49 / 49 30.0 % 180 / 600
test/unit/parser/parser_black.cpp
100.0 % 206 / 206 43.5 % 342 / 786
test/unit/parser/parser_builder_black.cpp
100.0 % 56 / 56 37.8 % 74 / 196
test/unit/preprocessing/pass_bv_gauss_white.cpp
97.3 % 1279 / 1314 42.6 % 4785 / 11225
test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
100.0 % 16 / 16 42.2 % 43 / 102
test/unit/printer/smt2_printer_black.cpp
100.0 % 18 / 18 45.3 % 39 / 86
test/unit/prop/cnf_stream_white.cpp
90.7 % 117 / 129 39.9 % 205 / 514
test/unit/test.h
100.0 % 1 / 1 100.0 % 0 / 0
test/unit/test_api.h
100.0 % 1 / 1 50.0 % 1 / 2
test/unit/test_context.h
100.0 % 2 / 2 50.0 % 1 / 2
test/unit/test_node.h
100.0 % 9 / 9 50.0 % 6 / 12
test/unit/test_smt.h
55.4 % 36 / 65 19.9 % 30 / 151
test/unit/theory/evaluator_white.cpp
100.0 % 68 / 68 43.5 % 216 / 496
test/unit/theory/logic_info_white.cpp
99.8 % 1233 / 1236 32.5 % 4144 / 12768
test/unit/theory/regexp_operation_black.cpp
100.0 % 72 / 72 48.2 % 220 / 456
test/unit/theory/sequences_rewriter_white.cpp
100.0 % 775 / 775 46.7 % 2500 / 5352
test/unit/theory/strings_rewriter_white.cpp
100.0 % 15 / 15 42.7 % 47 / 110
test/unit/theory/theory_arith_white.cpp
100.0 % 52 / 52 38.6 % 155 / 402
test/unit/theory/theory_bags_normal_form_white.cpp
100.0 % 283 / 283 42.1 % 1079 / 2564
test/unit/theory/theory_bags_rewriter_white.cpp
100.0 % 432 / 432 41.4 % 1347 / 3250
test/unit/theory/theory_bags_type_rules_white.cpp
100.0 % 52 / 52 38.6 % 136 / 352
test/unit/theory/theory_black.cpp
100.0 % 86 / 86 34.7 % 328 / 944
test/unit/theory/theory_bv_rewriter_white.cpp
100.0 % 30 / 30 45.8 % 87 / 190
test/unit/theory/theory_bv_white.cpp
100.0 % 37 / 37 46.9 % 105 / 224
test/unit/theory/theory_engine_white.cpp
98.7 % 78 / 79 45.8 % 198 / 432
test/unit/theory/theory_int_opt_white.cpp
100.0 % 54 / 54 44.7 % 102 / 228
test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
100.0 % 285 / 285 33.1 % 1398 / 4228
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
98.3 % 927 / 943 44.4 % 631 / 1422
test/unit/theory/theory_sets_type_enumerator_white.cpp
100.0 % 80 / 80 34.4 % 259 / 752
test/unit/theory/theory_sets_type_rules_white.cpp
100.0 % 32 / 32 33.0 % 104 / 315
test/unit/theory/theory_strings_skolem_cache_black.cpp
100.0 % 15 / 15 46.8 % 58 / 124
test/unit/theory/theory_strings_word_white.cpp
100.0 % 73 / 73 30.7 % 351 / 1142
test/unit/theory/theory_white.cpp
100.0 % 46 / 46 28.9 % 66 / 228
test/unit/theory/type_enumerator_white.cpp
100.0 % 201 / 201 33.9 % 962 / 2838
test/unit/util/array_store_all_white.cpp
100.0 % 31 / 31 40.9 % 108 / 264
test/unit/util/assert_white.cpp
100.0 % 27 / 27 23.3 % 179 / 768
test/unit/util/binary_heap_black.cpp
100.0 % 149 / 149 25.7 % 468 / 1818
test/unit/util/bitvector_black.cpp
100.0 % 124 / 124 28.1 % 476 / 1696
test/unit/util/boolean_simplification_black.cpp
100.0 %