GCC Code Coverage Report
Directory: . Exec Total Coverage
Date: 2021-02-20 Lines: 137857 199752 69.0 %
Legend: low: < 75.0 % medium: >= 75.0 % high: >= 90.0 % Branches: 258784 796086 32.5 %

File Lines Branches
build-coverage/src/expr/expr.cpp
12.2 % 66 / 540 3.8 % 73 / 1897
build-coverage/src/expr/expr.h
0.0 % 0 / 4 0.0 % 0 / 2
build-coverage/src/expr/expr_manager.cpp
27.4 % 139 / 508 13.0 % 280 / 2158
build-coverage/src/expr/kind.cpp
70.1 % 485 / 692 68.7 % 471 / 686
build-coverage/src/expr/kind.h
100.0 % 5 / 5 100.0 % 0 / 0
build-coverage/src/expr/metakind.cpp
75.3 % 393 / 522 44.2 % 311 / 703
build-coverage/src/expr/metakind.h
100.0 % 13 / 13 11.0 % 600 / 5456
build-coverage/src/expr/type_checker.cpp
90.0 % 558 / 620 51.4 % 1129 / 2196
build-coverage/src/expr/type_properties.h
37.1 % 36 / 97 21.0 % 57 / 271
build-coverage/src/options/arith_options.cpp
29.3 % 124 / 423 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
38.6 % 100 / 259 24.0 % 24 / 100
build-coverage/src/options/bv_options.h
60.5 % 72 / 119 100.0 % 0 / 0
build-coverage/src/options/datatypes_options.cpp
40.2 % 47 / 117 8.8 % 3 / 34
build-coverage/src/options/datatypes_options.h
100.0 % 43 / 43 100.0 % 0 / 0
build-coverage/src/options/decision_options.cpp
28.4 % 23 / 81 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.4 % 2697 / 8321 10.8 % 3117 / 28834
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
14.9 % 11 / 74 8.7 % 4 / 46
build-coverage/src/options/printer_options.h
60.0 % 6 / 10 100.0 % 0 / 0
build-coverage/src/options/proof_options.cpp
100.0 % 1 / 1 50.0 % 2 / 4
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
33.9 % 601 / 1775 4.9 % 34 / 691
build-coverage/src/options/quantifiers_options.h
91.9 % 545 / 593 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
41.3 % 270 / 653 14.7 % 35 / 238
build-coverage/src/options/smt_options.h
67.5 % 160 / 237 100.0 % 0 / 0
build-coverage/src/options/strings_options.cpp
28.6 % 50 / 175 3.3 % 2 / 61
build-coverage/src/options/strings_options.h
96.1 % 49 / 51 100.0 % 0 / 0
build-coverage/src/options/theory_options.cpp
32.6 % 29 / 89 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
36.1 % 26 / 72 10.7 % 3 / 28
build-coverage/src/options/uf_options.h
84.6 % 22 / 26 100.0 % 0 / 0
build-coverage/src/parser/cvc/CvcLexer.c
48.0 % 2575 / 5370 37.2 % 1054 / 2836
build-coverage/src/parser/cvc/CvcParser.c
35.6 % 4101 / 11516 29.2 % 3835 / 13123
build-coverage/src/parser/smt2/Smt2Lexer.c
72.3 % 1631 / 2255 62.5 % 950 / 1521
build-coverage/src/parser/smt2/Smt2Parser.c
69.9 % 2791 / 3991 45.1 % 2515 / 5573
build-coverage/src/parser/tptp/TptpLexer.c
75.0 % 1187 / 1583 55.5 % 518 / 933
build-coverage/src/parser/tptp/TptpParser.c
62.5 % 2574 / 4117 42.5 % 2072 / 4881
build-coverage/src/theory/rewriter_tables.h
63.0 % 68 / 108 39.9 % 142 / 356
build-coverage/src/theory/theory_traits.h
96.6 % 28 / 29 65.0 % 13 / 20
build-coverage/src/theory/type_enumerator.cpp
81.0 % 17 / 21 40.4 % 42 / 104
build-coverage/src/util/floatingpoint_literal_symfpu.h
100.0 % 13 / 13 50.0 % 3 / 6
build-coverage/test/unit/preprocessing/pass_bv_gauss_white.cpp
76.3 % 119 / 156 6.0 % 5 / 84
build-coverage/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
91.7 % 11 / 12 41.7 % 5 / 12
build-coverage/test/unit/printer/smt2_printer_black.cpp
87.5 % 14 / 16 35.7 % 5 / 14
build-coverage/test/unit/prop/cnf_stream_white.cpp
78.8 % 41 / 52 15.6 % 5 / 32
build-coverage/test/unit/theory/evaluator_white.cpp
83.3 % 20 / 24 27.8 % 5 / 18
build-coverage/test/unit/theory/logic_info_white.cpp
85.0 % 17 / 20 28.6 % 4 / 14
build-coverage/test/unit/theory/regexp_operation_black.cpp
87.5 % 14 / 16 35.7 % 5 / 14
build-coverage/test/unit/theory/sequences_rewriter_white.cpp
77.6 % 59 / 76 11.4 % 5 / 44
build-coverage/test/unit/theory/strings_rewriter_white.cpp
91.7 % 11 / 12 41.7 % 5 / 12
build-coverage/test/unit/theory/theory_arith_white.cpp
82.1 % 23 / 28 25.0 % 5 / 20
build-coverage/test/unit/theory/theory_bags_normal_form_white.cpp
77.8 % 56 / 72 11.9 % 5 / 42
build-coverage/test/unit/theory/theory_bags_rewriter_white.cpp
77.8 % 56 / 72 11.9 % 5 / 42
build-coverage/test/unit/theory/theory_bags_type_rules_white.cpp
82.1 % 23 / 28 25.0 % 5 / 20
build-coverage/test/unit/theory/theory_black.cpp
91.7 % 11 / 12 41.7 % 5 / 12
build-coverage/test/unit/theory/theory_bv_rewriter_white.cpp
87.5 % 14 / 16 35.7 % 5 / 14
build-coverage/test/unit/theory/theory_bv_white.cpp
87.5 % 14 / 16 35.7 % 5 / 14
build-coverage/test/unit/theory/theory_engine_white.cpp
85.0 % 17 / 20 31.3 % 5 / 16
build-coverage/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
83.3 % 20 / 24 27.8 % 5 / 18
build-coverage/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
75.2 % 776 / 1032 1.0 % 5 / 522
build-coverage/test/unit/theory/theory_sets_type_enumerator_white.cpp
83.3 % 20 / 24 27.8 % 5 / 18
build-coverage/test/unit/theory/theory_sets_type_rules_white.cpp
85.0 % 17 / 20 31.3 % 5 / 16
build-coverage/test/unit/theory/theory_strings_skolem_cache_black.cpp
91.7 % 11 / 12 41.7 % 5 / 12
build-coverage/test/unit/theory/theory_strings_word_white.cpp
91.7 % 11 / 12 41.7 % 5 / 12
build-coverage/test/unit/theory/theory_white.cpp
83.3 % 20 / 24 27.8 % 5 / 18
build-coverage/test/unit/theory/type_enumerator_white.cpp
80.6 % 29 / 36 20.8 % 5 / 24
build-coverage/test/unit/util/array_store_all_white.cpp
85.0 % 17 / 20 31.3 % 5 / 16
build-coverage/test/unit/util/assert_white.cpp
87.5 % 14 / 16 33.3 % 4 / 12
build-coverage/test/unit/util/binary_heap_black.cpp
87.5 % 14 / 16 33.3 % 4 / 12
build-coverage/test/unit/util/bitvector_black.cpp
79.2 % 38 / 48 14.3 % 4 / 28
build-coverage/test/unit/util/boolean_simplification_black.cpp
81.3 % 26 / 32 22.7 % 5 / 22
build-coverage/test/unit/util/cardinality_public.cpp
91.7 % 11 / 12 40.0 % 4 / 10
build-coverage/test/unit/util/check_white.cpp
83.3 % 20 / 24 25.0 % 4 / 16
build-coverage/test/unit/util/configuration_black.cpp
83.3 % 20 / 24 25.0 % 4 / 16
build-coverage/test/unit/util/datatype_black.cpp
79.2 % 38 / 48 16.7 % 5 / 30
build-coverage/test/unit/util/exception_black.cpp
91.7 % 11 / 12 40.0 % 4 / 10
build-coverage/test/unit/util/floatingpoint_black.cpp
83.3 % 20 / 24 25.0 % 4 / 16
build-coverage/test/unit/util/integer_black.cpp
77.2 % 71 / 92 8.0 % 4 / 50
build-coverage/test/unit/util/integer_white.cpp
87.5 % 14 / 16 33.3 % 4 / 12
build-coverage/test/unit/util/output_black.cpp
85.0 % 17 / 20 28.6 % 4 / 14
build-coverage/test/unit/util/rational_black.cpp
91.7 % 11 / 12 40.0 % 4 / 10
build-coverage/test/unit/util/rational_white.cpp
78.3 % 47 / 60 11.8 % 4 / 34
build-coverage/test/unit/util/stats_black.cpp
91.7 % 11 / 12 40.0 % 4 / 10
deps/install/include/cryptominisat5/solvertypesmini.h
40.0 % 6 / 15 100.0 % 0 / 0
deps/install/include/symfpu/core/add.h
98.3 % 116 / 118 61.8 % 359 / 581
deps/install/include/symfpu/core/classify.h
100.0 % 21 / 21 62.1 % 41 / 66
deps/install/include/symfpu/core/compare.h
95.2 % 60 / 63 67.6 % 234 / 346
deps/install/include/symfpu/core/convert.h
39.7 % 50 / 126 20.9 % 73 / 350
deps/install/include/symfpu/core/divide.h
100.0 % 43 / 43 59.1 % 97 / 164
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.3 % 66 / 106
deps/install/include/symfpu/core/operations.h
97.3 % 182 / 187 48.1 % 336 / 699
deps/install/include/symfpu/core/packing.h
100.0 % 58 / 58 62.9 % 132 / 210
deps/install/include/symfpu/core/remainder.h
100.0 % 56 / 56 59.7 % 105 / 176
deps/install/include/symfpu/core/rounder.h
90.0 % 135 / 150 53.8 % 380 / 706
deps/install/include/symfpu/core/sign.h
100.0 % 10 / 10 55.6 % 10 / 18
deps/install/include/symfpu/core/sqrt.h
100.0 % 34 / 34 42.1 % 64 / 152
deps/install/include/symfpu/core/unpackedFloat.h
100.0 % 124 / 124 55.7 % 244 / 438
deps/install/include/symfpu/utils/common.h
100.0 % 23 / 23 80.0 % 8 / 10
src/api/cvc4cpp.cpp
84.7 % 2198 / 2594 38.4 % 5795 / 15088
src/api/cvc4cpp.h
77.8 % 14 / 18 50.0 % 3 / 6
src/base/check.cpp
68.5 % 50 / 73 45.5 % 30 / 66
src/base/check.h
100.0 % 3 / 3 50.0 % 1 / 2
src/base/configuration.cpp
69.7 % 140 / 201 35.1 % 113 / 322
src/base/exception.cpp
70.4 % 57 / 81 34.7 % 41 / 118
src/base/exception.h
89.5 % 34 / 38 43.8 % 21 / 48
src/base/listener.cpp
100.0 % 2 / 2 50.0 % 1 / 2
src/base/map_util.h
100.0 % 16 / 16 39.4 % 78 / 198
src/base/modal_exception.h
66.7 % 6 / 9 50.0 % 2 / 4
src/base/output.cpp
100.0 % 13 / 13 50.0 % 3 / 6
src/base/output.h
78.9 % 101 / 128 15.5 % 140 / 902
src/context/backtrackable.h
4.9 % 2 / 41 1.0 % 1 / 100
src/context/cdhashmap.h
97.6 % 124 / 127 35.9 % 526 / 1465
src/context/cdhashset.h
90.2 % 37 / 41 31.6 % 96 / 304
src/context/cdinsert_hashmap.h
100.0 % 101 / 101 31.9 % 237 / 744
src/context/cdlist.h
95.3 % 122 / 128 34.1 % 848 / 2490
src/context/cdlist_forward.h
100.0 % 1 / 1 100.0 % 0 / 0
src/context/cdmaybe.h
100.0 % 22 / 22 19.1 % 13 / 68
src/context/cdo.h
100.0 % 33 / 33 31.8 % 62 / 195
src/context/cdqueue.h
100.0 % 47 / 47 21.7 % 133 / 612
src/context/cdtrail_queue.h
100.0 % 23 / 23 18.8 % 9 / 48
src/context/context.cpp
87.4 % 174 / 199 36.3 % 220 / 606
src/context/context.h
88.5 % 54 / 61 36.6 % 30 / 82
src/context/context_mm.cpp
96.8 % 60 / 62 34.8 % 39 / 112
src/decision/decision_engine.cpp
100.0 % 41 / 41 32.9 % 52 / 158
src/decision/decision_engine.h
100.0 % 30 / 30 24.0 % 25 / 104
src/decision/decision_strategy.h
100.0 % 8 / 8 50.0 % 2 / 4
src/decision/justification_heuristic.cpp
72.9 % 275 / 377 32.0 % 481 / 1501
src/decision/justification_heuristic.h
0.0 % 0 / 3 0.0 % 0 / 6
src/expr/array_store_all.cpp
53.7 % 22 / 41 40.7 % 44 / 108
src/expr/ascription_type.cpp
57.9 % 11 / 19 31.8 % 7 / 22
src/expr/attribute.cpp
43.4 % 23 / 53 5.2 % 5 / 96
src/expr/attribute.h
75.2 % 91 / 121 43.9 % 453 / 1031
src/expr/attribute_internals.h
100.0 % 70 / 70 30.6 % 63 / 206
src/expr/attribute_unique_id.h
0.0 % 0 / 5 100.0 % 0 / 0
src/expr/bound_var_manager.cpp
52.9 % 9 / 17 35.3 % 12 / 34
src/expr/bound_var_manager.h
88.9 % 8 / 9 33.3 % 28 / 84
src/expr/buffered_proof_generator.cpp
3.3 % 1 / 30 1.7 % 2 / 120
src/expr/buffered_proof_generator.h
0.0 % 0 / 2 0.0 % 0 / 4
src/expr/datatype_index.cpp
66.7 % 4 / 6 50.0 % 3 / 6
src/expr/datatype_index.h
100.0 % 3 / 3 100.0 % 0 / 0
src/expr/dtype.cpp
87.8 % 424 / 483 34.0 % 761 / 2236
src/expr/dtype.h
50.0 % 1 / 2 31.3 % 10 / 32
src/expr/dtype_cons.cpp
92.1 % 315 / 342 35.7 % 509 / 1424
src/expr/dtype_cons.h
100.0 % 2 / 2 50.0 % 8 / 16
src/expr/dtype_selector.cpp
87.9 % 29 / 33 29.0 % 36 / 124
src/expr/dtype_selector.h
100.0 % 1 / 1 50.0 % 2 / 4
src/expr/emptybag.cpp
42.9 % 9 / 21 41.7 % 5 / 12
src/expr/emptyset.cpp
42.9 % 9 / 21 41.7 % 5 / 12
src/expr/expr_iomanip.cpp
79.6 % 43 / 54 54.2 % 13 / 24
src/expr/expr_manager_scope.h
100.0 % 8 / 8 100.0 % 2 / 2
src/expr/kind_map.h
100.0 % 8 / 8 66.7 % 4 / 6
src/expr/lazy_proof.cpp
1.0 % 1 / 96 0.5 % 2 / 364
src/expr/lazy_proof_chain.cpp
0.7 % 1 / 150 0.4 % 2 / 548
src/expr/match_trie.cpp
94.5 % 103 / 109 47.7 % 167 / 350
src/expr/match_trie.h
100.0 % 3 / 3 50.0 % 2 / 4
src/expr/node.cpp
85.7 % 36 / 42 49.6 % 116 / 234
src/expr/node.h
82.0 % 310 / 378 22.8 % 986 / 4332
src/expr/node_algorithm.cpp
89.7 % 323 / 360 49.6 % 527 / 1062
src/expr/node_builder.h
83.9 % 303 / 361 11.2 % 959 / 8555
src/expr/node_manager.cpp
86.0 % 509 / 592 34.5 % 685 / 1986
src/expr/node_manager.h
72.3 % 211 / 292 19.1 % 582 / 3042
src/expr/node_self_iterator.h
93.0 % 40 / 43 24.5 % 27 / 110
src/expr/node_traversal.cpp
100.0 % 58 / 58 48.7 % 55 / 113
src/expr/node_traversal.h
100.0 % 5 / 5 50.0 % 5 / 10
src/expr/node_trie.cpp
74.1 % 20 / 27 41.5 % 44 / 106
src/expr/node_trie.h
100.0 % 6 / 6 50.0 % 3 / 6
src/expr/node_value.cpp
33.3 % 11 / 33 18.9 % 14 / 74
src/expr/node_value.h
77.5 % 110 / 142 18.5 % 46 / 248
src/expr/node_visitor.h
100.0 % 33 / 33 48.9 % 93 / 190
src/expr/proof.cpp
0.5 % 1 / 213 0.2 % 2 / 968
src/expr/proof_checker.cpp
0.6 % 1 / 162 0.3 % 2 / 660
src/expr/proof_checker.h
40.0 % 2 / 5 50.0 % 1 / 2
src/expr/proof_ensure_closed.cpp
11.8 % 9 / 76 2.6 % 11 / 426
src/expr/proof_generator.cpp
11.5 % 3 / 26 2.5 % 3 / 118
src/expr/proof_generator.h
0.0 % 0 / 1 100.0 % 0 / 0
src/expr/proof_node.cpp
2.9 % 1 / 34 6.7 % 2 / 30
src/expr/proof_node.h
0.0 % 0 / 4 0.0 % 0 / 4
src/expr/proof_node_algorithm.cpp
1.3 % 1 / 75 1.1 % 2 / 174
src/expr/proof_node_manager.cpp
0.6 % 1 / 158 0.3 % 2 / 784
src/expr/proof_node_manager.h
0.0 % 0 / 1 100.0 % 0 / 0
src/expr/proof_node_to_sexpr.cpp
1.3 % 1 / 78 0.7 % 2 / 282
src/expr/proof_node_to_sexpr.h
0.0 % 0 / 1 100.0 % 0 / 0
src/expr/proof_node_updater.cpp
0.8 % 1 / 130 0.6 % 2 / 360
src/expr/proof_node_updater.h
0.0 % 0 / 1 100.0 % 0 / 0
src/expr/proof_rule.cpp
3.6 % 5 / 137 3.0 % 4 / 133
src/expr/proof_rule.h
0.0 % 0 / 1 100.0 % 0 / 0
src/expr/proof_set.h
50.0 % 4 / 8 16.7 % 2 / 12
src/expr/proof_step_buffer.cpp
2.3 % 1 / 43 2.3 % 2 / 88
src/expr/proof_step_buffer.h
0.0 % 0 / 2 0.0 % 0 / 4
src/expr/record.cpp
33.3 % 1 / 3 20.0 % 2 / 10
src/expr/record.h
100.0 % 6 / 6 100.0 % 0 / 0
src/expr/sequence.cpp
54.3 % 102 / 188 19.9 % 126 / 634
src/expr/sequence.h
100.0 % 3 / 3 100.0 % 0 / 0
src/expr/skolem_manager.cpp
86.6 % 136 / 157 36.9 % 324 / 878
src/expr/skolem_manager.h
100.0 % 2 / 2 100.0 % 0 / 0
src/expr/subs.cpp
40.7 % 33 / 81 16.2 % 38 / 234
src/expr/subs.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/sygus_datatype.cpp
100.0 % 44 / 44 30.3 % 43 / 142
src/expr/sygus_datatype.h
100.0 % 3 / 3 30.0 % 3 / 10
src/expr/symbol_manager.cpp
95.5 % 128 / 134 51.8 % 118 / 228
src/expr/symbol_table.cpp
85.0 % 192 / 226 38.1 % 188 / 494
src/expr/symbol_table.h
100.0 % 1 / 1 50.0 % 1 / 2
src/expr/tconv_seq_proof_generator.cpp
1.3 % 1 / 77 0.6 % 2 / 320
src/expr/term_canonize.cpp
99.0 % 100 / 101 54.3 % 201 / 370
src/expr/term_canonize.h
100.0 % 1 / 1 100.0 % 0 / 0
src/expr/term_context.cpp
38.3 % 18 / 47 37.0 % 20 / 54
src/expr/term_context.h
85.7 % 6 / 7 37.5 % 3 / 8
src/expr/term_context_node.cpp
3.4 % 1 / 29 1.6 % 2 / 124
src/expr/term_context_stack.cpp
52.8 % 19 / 36 24.7 % 36 / 146
src/expr/term_context_stack.h
100.0 % 1 / 1 50.0 % 1 / 2
src/expr/term_conversion_proof_generator.cpp
0.3 % 1 / 295 0.1 % 2 / 1519
src/expr/type.cpp
24.5 % 88 / 359 11.5 % 74 / 644
src/expr/type.h
40.0 % 8 / 20 26.0 % 13 / 50
src/expr/type_checker_util.h
75.0 % 36 / 48 11.1 % 165 / 1482
src/expr/type_matcher.cpp
95.2 % 59 / 62 52.5 % 84 / 160
src/expr/type_matcher.h
100.0 % 2 / 2 100.0 % 0 / 0
src/expr/type_node.cpp
85.5 % 278 / 325 37.4 % 436 / 1166
src/expr/type_node.h
85.5 % 189 / 221 20.5 % 213 / 1038
src/expr/uninterpreted_constant.cpp
63.9 % 23 / 36 37.1 % 26 / 70
src/expr/variable_type_map.h
0.0 % 0 / 2 100.0 % 0 / 0
src/main/command_executor.cpp
48.7 % 73 / 150 32.1 % 123 / 383
src/main/command_executor.h
100.0 % 8 / 8 100.0 % 0 / 0
src/main/driver_unified.cpp
34.0 % 85 / 250 17.4 % 120 / 690
src/main/interactive_shell.cpp
67.0 % 59 / 88 39.5 % 103 / 261
src/main/main.cpp
87.5 % 14 / 16 47.7 % 31 / 65
src/main/signal_handlers.cpp
26.3 % 40 / 152 8.9 % 15 / 168
src/main/time_limit.cpp
72.2 % 13 / 18 29.2 % 7 / 24
src/options/base_handlers.h
0.0 % 0 / 10 0.0 % 0 / 64
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
67.1 % 53 / 79 43.8 % 91 / 208
src/options/language.h
42.9 % 15 / 35 29.4 % 5 / 17
src/options/open_ostream.cpp
6.7 % 2 / 30 4.2 % 3 / 72
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 % 4 / 8
src/options/options.h
100.0 % 11 / 11 100.0 % 0 / 0
src/options/options_handler.cpp
41.8 % 119 / 285 22.9 % 158 / 690
src/options/options_handler.h
0.0 % 0 / 6 0.0 % 0 / 8
src/options/options_listener.h
100.0 % 2 / 2 50.0 % 1 / 2
src/options/options_public_functions.cpp
87.4 % 90 / 103 32.2 % 29 / 90
src/options/printer_modes.cpp
12.5 % 1 / 8 28.6 % 2 / 7
src/options/set_language.cpp
100.0 % 29 / 29 50.0 % 8 / 16
src/parser/antlr_input.cpp
90.0 % 216 / 240 55.1 % 250 / 454
src/parser/antlr_input.h
84.4 % 27 / 32 44.1 % 30 / 68
src/parser/antlr_input_imports.cpp
68.0 % 70 / 103 31.0 % 52 / 168
src/parser/antlr_line_buffered_input.cpp
1.1 % 1 / 87 6.3 % 2 / 32
src/parser/bounded_token_buffer.cpp
55.3 % 89 / 161 52.5 % 21 / 40
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 % 10 / 20
src/parser/cvc/cvc.h
100.0 % 4 / 4 50.0 % 1 / 2
src/parser/cvc/cvc_input.cpp
91.7 % 22 / 24 43.3 % 13 / 30
src/parser/input.cpp
87.0 % 20 / 23 50.0 % 4 / 8
src/parser/input.h
77.8 % 7 / 9 33.3 % 2 / 6
src/parser/line_buffer.cpp
2.6 % 1 / 39 4.2 % 2 / 48
src/parser/memory_mapped_input_buffer.cpp
0.0 % 0 / 33 0.0 % 0 / 14
src/parser/parse_op.cpp
6.3 % 1 / 16 4.0 % 2 / 50
src/parser/parse_op.h
100.0 % 2 / 2 50.0 % 3 / 6
src/parser/parser.cpp
84.1 % 387 / 460 45.4 % 478 / 1053
src/parser/parser.h
75.0 % 30 / 40 30.0 % 3 / 10
src/parser/parser_builder.cpp
84.1 % 95 / 113 57.4 % 31 / 54
src/parser/parser_builder.h
100.0 % 1 / 1 100.0 % 0 / 0
src/parser/parser_exception.h
85.0 % 17 / 20 62.5 % 5 / 8
src/parser/smt2/smt2.cpp
87.1 % 607 / 697 48.3 % 1001 / 2074
src/parser/smt2/smt2.h
66.7 % 26 / 39 36.5 % 27 / 74
src/parser/smt2/smt2_input.cpp
91.3 % 21 / 23 43.3 % 13 / 30
src/parser/smt2/sygus_input.cpp
83.3 % 20 / 24 43.3 % 13 / 30
src/parser/tptp/tptp.cpp
80.0 % 180 / 225 40.7 % 251 / 616
src/parser/tptp/tptp.h
71.4 % 5 / 7 100.0 % 0 / 0
src/parser/tptp/tptp_input.cpp
83.3 % 20 / 24 43.3 % 13 / 30
src/preprocessing/assertion_pipeline.cpp
77.8 % 70 / 90 26.2 % 110 / 420
src/preprocessing/assertion_pipeline.h
100.0 % 14 / 14 100.0 % 4 / 4
src/preprocessing/passes/ackermann.cpp
98.2 % 111 / 113 40.2 % 227 / 564
src/preprocessing/passes/ackermann.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/apply_substs.cpp
100.0 % 21 / 21 55.2 % 32 / 58
src/preprocessing/passes/apply_substs.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/bool_to_bv.cpp
97.3 % 178 / 183 51.4 % 415 / 807
src/preprocessing/passes/bool_to_bv.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/bv_abstraction.cpp
92.9 % 13 / 14 47.5 % 19 / 40
src/preprocessing/passes/bv_abstraction.h
100.0 % 1 / 1 50.0 % 1 / 2
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 50.0 % 1 / 2
src/preprocessing/passes/bv_gauss.cpp
91.0 % 303 / 333 38.7 % 706 / 1822
src/preprocessing/passes/bv_gauss.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/bv_intro_pow2.cpp
94.4 % 34 / 36 50.4 % 60 / 119
src/preprocessing/passes/bv_intro_pow2.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/bv_to_bool.cpp
98.1 % 159 / 162 39.6 % 388 / 980
src/preprocessing/passes/bv_to_bool.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/bv_to_int.cpp
89.3 % 402 / 450 39.6 % 856 / 2162
src/preprocessing/passes/bv_to_int.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/extended_rewriter_pass.cpp
100.0 % 9 / 9 46.2 % 12 / 26
src/preprocessing/passes/extended_rewriter_pass.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/foreign_theory_rewrite.cpp
98.1 % 52 / 53 36.7 % 99 / 270
src/preprocessing/passes/foreign_theory_rewrite.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/fun_def_fmf.cpp
94.8 % 219 / 231 46.9 % 472 / 1006
src/preprocessing/passes/global_negate.cpp
98.0 % 49 / 50 51.2 % 87 / 170
src/preprocessing/passes/global_negate.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/ho_elim.cpp
97.9 % 321 / 328 45.1 % 719 / 1596
src/preprocessing/passes/ho_elim.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/int_to_bv.cpp
70.5 % 91 / 129 30.0 % 194 / 646
src/preprocessing/passes/int_to_bv.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/ite_removal.cpp
92.0 % 23 / 25 35.2 % 31 / 88
src/preprocessing/passes/ite_removal.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/ite_simp.cpp
50.4 % 62 / 123 14.3 % 73 / 510
src/preprocessing/passes/ite_simp.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/miplib_trick.cpp
12.5 % 46 / 368 2.8 % 55 / 1956
src/preprocessing/passes/nl_ext_purify.cpp
98.2 % 56 / 57 56.3 % 107 / 190
src/preprocessing/passes/nl_ext_purify.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/non_clausal_simp.cpp
91.3 % 220 / 241 37.4 % 516 / 1380
src/preprocessing/passes/non_clausal_simp.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/pseudo_boolean_processor.cpp
74.5 % 143 / 192 27.7 % 273 / 987
src/preprocessing/passes/pseudo_boolean_processor.h
100.0 % 3 / 3 56.3 % 9 / 16
src/preprocessing/passes/quantifier_macros.cpp
85.8 % 289 / 337 46.7 % 607 / 1300
src/preprocessing/passes/quantifier_macros.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/quantifiers_preprocess.cpp
100.0 % 15 / 15 52.0 % 26 / 50
src/preprocessing/passes/quantifiers_preprocess.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/real_to_int.cpp
95.9 % 93 / 97 48.9 % 226 / 462
src/preprocessing/passes/real_to_int.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/rewrite.cpp
100.0 % 7 / 7 50.0 % 8 / 16
src/preprocessing/passes/rewrite.h
100.0 % 1 / 1 50.0 % 1 / 2
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 50.0 % 1 / 2
src/preprocessing/passes/sort_infer.cpp
100.0 % 36 / 36 54.2 % 52 / 96
src/preprocessing/passes/sort_infer.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/static_learning.cpp
100.0 % 14 / 14 52.9 % 18 / 34
src/preprocessing/passes/static_learning.h
100.0 % 1 / 1 50.0 % 1 / 2
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 50.0 % 1 / 2
src/preprocessing/passes/sygus_inference.cpp
94.6 % 159 / 168 47.5 % 306 / 644
src/preprocessing/passes/sygus_inference.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/synth_rew_rules.cpp
1.2 % 3 / 252 0.4 % 4 / 1030
src/preprocessing/passes/synth_rew_rules.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/theory_preprocess.cpp
100.0 % 22 / 22 44.6 % 33 / 74
src/preprocessing/passes/theory_preprocess.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/theory_rewrite_eq.cpp
100.0 % 53 / 53 44.8 % 113 / 252
src/preprocessing/passes/theory_rewrite_eq.h
100.0 % 1 / 1 50.0 % 1 / 2
src/preprocessing/passes/unconstrained_simplifier.cpp
83.2 % 323 / 388 40.4 % 755 / 1867
src/preprocessing/preprocessing_pass.cpp
100.0 % 28 / 28 55.0 % 55 / 100
src/preprocessing/preprocessing_pass_context.cpp
69.2 % 18 / 26 46.9 % 15 / 32
src/preprocessing/preprocessing_pass_context.h
100.0 % 14 / 14 100.0 % 0 / 0
src/preprocessing/preprocessing_pass_registry.cpp
100.0 % 58 / 58 47.8 % 153 / 320
src/preprocessing/util/ite_utilities.cpp
47.2 % 467 / 990 21.1 % 812 / 3849
src/preprocessing/util/ite_utilities.h
19.0 % 8 / 42 8.3 % 4 / 48
src/printer/ast/ast_printer.cpp
16.1 % 36 / 223 16.0 % 43 / 268
src/printer/ast/ast_printer.h
100.0 % 1 / 1 50.0 % 1 / 2
src/printer/cvc/cvc_printer.cpp
31.6 % 288 / 911 20.1 % 450 / 2236
src/printer/cvc/cvc_printer.h
100.0 % 2 / 2 50.0 % 1 / 2
src/printer/let_binding.cpp
98.1 % 101 / 103 45.0 % 171 / 380
src/printer/let_binding.h
100.0 % 1 / 1 100.0 % 0 / 0
src/printer/printer.cpp
23.2 % 49 / 211 19.3 % 60 / 311
src/printer/printer.h
100.0 % 2 / 2 50.0 % 1 / 2
src/printer/smt2/smt2_printer.cpp
46.7 % 542 / 1161 28.9 % 980 / 3390
src/printer/smt2/smt2_printer.h
100.0 % 2 / 2 50.0 % 1 / 2
src/printer/tptp/tptp_printer.cpp
23.3 % 7 / 30 3.1 % 2 / 64
src/printer/tptp/tptp_printer.h
100.0 % 1 / 1 50.0 % 1 / 2
src/proof/cnf_proof.cpp
100.0 % 47 / 47 36.9 % 79 / 214
src/proof/cnf_proof.h
100.0 % 1 / 1 100.0 % 0 / 0
src/proof/proof_manager.cpp
73.6 % 81 / 110 32.5 % 174 / 536
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.7 % 382 / 556 25.2 % 464 / 1838
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 50.0 % 1 / 2
src/prop/bvminisat/bvminisat.cpp
74.1 % 129 / 174 33.6 % 96 / 286
src/prop/bvminisat/bvminisat.h
85.7 % 12 / 14 12.5 % 1 / 8
src/prop/bvminisat/core/Solver.cc
80.2 % 511 / 637 48.7 % 566 / 1163
src/prop/bvminisat/core/Solver.h
82.6 % 57 / 69 65.8 % 50 / 76
src/prop/bvminisat/core/SolverTypes.h
94.1 % 112 / 119 77.9 % 53 / 68
src/prop/bvminisat/mtl/Alg.h
100.0 % 11 / 11 85.2 % 23 / 27
src/prop/bvminisat/mtl/Alloc.h
94.9 % 37 / 39 62.5 % 15 / 24
src/prop/bvminisat/mtl/Heap.h
91.3 % 63 / 69 59.3 % 32 / 54
src/prop/bvminisat/mtl/Queue.h
94.7 % 18 / 19 77.3 % 17 / 22
src/prop/bvminisat/mtl/Sort.h
100.0 % 27 / 27 91.2 % 31 / 34
src/prop/bvminisat/mtl/Vec.h
97.3 % 36 / 37 54.4 % 130 / 239
src/prop/bvminisat/mtl/XAlloc.h
80.0 % 4 / 5 25.0 % 1 / 4
src/prop/bvminisat/simp/SimpSolver.cc
73.6 % 296 / 402 50.6 % 351 / 694
src/prop/bvminisat/simp/SimpSolver.h
88.2 % 15 / 17 67.9 % 19 / 28
src/prop/bvminisat/utils/Options.h
21.9 % 21 / 96 11.0 % 9 / 82
src/prop/bvminisat/utils/ParseUtils.h
0.0 % 0 / 6 0.0 % 0 / 4
src/prop/cadical.cpp
60.2 % 56 / 93 20.0 % 36 / 180
src/prop/cnf_stream.cpp
92.5 % 372 / 402 36.6 % 767 / 2098
src/prop/cnf_stream.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/cryptominisat.cpp
64.2 % 77 / 120 27.8 % 69 / 248
src/prop/cryptominisat.h
0.0 % 0 / 1 100.0 % 0 / 0
src/prop/minisat/core/Solver.cc
79.5 % 876 / 1102 44.9 % 1361 / 3028
src/prop/minisat/core/Solver.h
94.4 % 102 / 108 69.7 % 99 / 142
src/prop/minisat/core/SolverTypes.h
86.5 % 128 / 148 65.9 % 58 / 88
src/prop/minisat/minisat.cpp
82.0 % 132 / 161 31.7 % 97 / 306
src/prop/minisat/minisat.h
50.0 % 2 / 4 0.0 % 0 / 6
src/prop/minisat/mtl/Alg.h
100.0 % 11 / 11 85.2 % 23 / 27
src/prop/minisat/mtl/Alloc.h
94.9 % 37 / 39 62.5 % 15 / 24
src/prop/minisat/mtl/Heap.h
91.3 % 63 / 69 59.3 % 32 / 54
src/prop/minisat/mtl/Queue.h
94.7 % 18 / 19 72.7 % 16 / 22
src/prop/minisat/mtl/Sort.h
100.0 % 27 / 27 86.2 % 50 / 58
src/prop/minisat/mtl/Vec.h
94.7 % 36 / 38 65.4 % 214 / 327
src/prop/minisat/mtl/XAlloc.h
80.0 % 4 / 5 25.0 % 1 / 4
src/prop/minisat/simp/SimpSolver.cc
75.1 % 307 / 409 51.8 % 401 / 774
src/prop/minisat/simp/SimpSolver.h
82.6 % 19 / 23 67.6 % 23 / 34
src/prop/minisat/utils/Options.h
21.9 % 21 / 96 11.0 % 9 / 82
src/prop/minisat/utils/ParseUtils.h
0.0 % 0 / 6 0.0 % 0 / 4
src/prop/proof_cnf_stream.cpp
0.2 % 1 / 604 0.1 % 2 / 3424
src/prop/proof_cnf_stream.h
0.0 % 0 / 1 0.0 % 0 / 2
src/prop/proof_post_processor.cpp
2.4 % 1 / 42 1.2 % 2 / 166
src/prop/proof_post_processor.h
0.0 % 0 / 1 0.0 % 0 / 2
src/prop/prop_engine.cpp
67.0 % 199 / 297 26.5 % 294 / 1110
src/prop/prop_engine.h
100.0 % 1 / 1 100.0 % 0 / 0
src/prop/prop_proof_manager.cpp
2.0 % 1 / 51 1.1 % 2 / 190
src/prop/prop_proof_manager.h
0.0 % 0 / 1 100.0 % 0 / 0
src/prop/registrar.h
100.0 % 4 / 4 50.0 % 2 / 4
src/prop/sat_proof_manager.cpp
0.2 % 1 / 415 0.1 % 2 / 2126
src/prop/sat_proof_manager.h
0.0 % 0 / 1 100.0 % 0 / 0
src/prop/sat_solver.h
17.6 % 6 / 34 8.3 % 3 / 36
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
76.5 % 26 / 34 16.7 % 3 / 18
src/prop/theory_proxy.cpp
91.8 % 89 / 97 41.4 % 126 / 304
src/smt/abduction_solver.cpp
83.8 % 83 / 99 36.5 % 170 / 466
src/smt/abstract_values.cpp
100.0 % 16 / 16 37.1 % 26 / 70
src/smt/assertions.cpp
85.4 % 82 / 96 42.9 % 102 / 238
src/smt/check_models.cpp
72.9 % 35 / 48 26.2 % 64 / 244
src/smt/command.cpp
50.1 % 603 / 1203 29.9 % 468 / 1567
src/smt/command.h
76.9 % 60 / 78 39.5 % 49 / 124
src/smt/defined_function.h
85.7 % 6 / 7 50.0 % 4 / 8
src/smt/dump.cpp
71.4 % 50 / 70 35.6 % 47 / 132
src/smt/dump.h
100.0 % 10 / 10 55.6 % 20 / 36
src/smt/dump_manager.cpp
100.0 % 26 / 26 56.0 % 28 / 50
src/smt/expand_definitions.cpp
77.1 % 121 / 157 36.5 % 255 / 698
src/smt/interpolation_solver.cpp
79.3 % 46 / 58 39.2 % 87 / 222
src/smt/listeners.cpp
87.8 % 36 / 41 38.1 % 48 / 126
src/smt/listeners.h
100.0 % 3 / 3 50.0 % 2 / 4
src/smt/logic_exception.h
100.0 % 7 / 7 50.0 % 1 / 2
src/smt/logic_request.cpp
7.7 % 1 / 13 20.0 % 2 / 10
src/smt/logic_request.h
0.0 % 0 / 1 100.0 % 0 / 0
src/smt/managed_ostreams.cpp
30.7 % 27 / 88 21.8 % 31 / 142
src/smt/managed_ostreams.h
40.0 % 4 / 10 0.0 % 0 / 2
src/smt/model.cpp
100.0 % 24 / 24 27.3 % 12 / 44
src/smt/model.h
33.3 % 1 / 3 100.0 % 0 / 0
src/smt/model_blocker.cpp
84.7 % 122 / 144 35.6 % 291 / 818
src/smt/model_core_builder.cpp
1.9 % 1 / 52 1.1 % 2 / 186
src/smt/node_command.cpp
61.5 % 32 / 52 33.3 % 28 / 84
src/smt/node_command.h
100.0 % 5 / 5 20.0 % 8 / 40
src/smt/options_manager.cpp
62.3 % 43 / 69 28.2 % 83 / 294
src/smt/output_manager.cpp
100.0 % 6 / 6 50.0 % 2 / 4
src/smt/preprocess_proof_generator.cpp
1.0 % 1 / 105 0.4 % 2 / 516
src/smt/preprocess_proof_generator.h
0.0 % 0 / 1 0.0 % 0 / 2
src/smt/preprocessor.cpp
86.7 % 52 / 60 37.2 % 61 / 164
src/smt/process_assertions.cpp
93.0 % 174 / 187 49.9 % 365 / 732
src/smt/proof_manager.cpp
1.2 % 1 / 86 0.6 % 2 / 328
src/smt/proof_post_processor.cpp
0.2 % 1 / 552 0.1 % 2 / 2602
src/smt/proof_post_processor.h
0.0 % 0 / 1 0.0 % 0 / 2
src/smt/quant_elim_solver.cpp
92.5 % 62 / 67 42.0 % 152 / 362
src/smt/set_defaults.cpp
79.6 % 533 / 670 46.3 % 1558 / 3362
src/smt/smt_engine.cpp
75.4 % 780 / 1034 33.7 % 1246 / 3695
src/smt/smt_engine.h
100.0 % 6 / 6 100.0 % 0 / 0
src/smt/smt_engine_scope.cpp
100.0 % 25 / 25 21.2 % 22 / 104
src/smt/smt_engine_state.cpp
89.6 % 129 / 144 36.0 % 107 / 297
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.7 % 107 / 118 45.2 % 178 / 394
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 % 182 / 209 45.0 % 340 / 756
src/smt/term_formula_removal.cpp
83.7 % 242 / 289 39.1 % 428 / 1096
src/smt/unsat_core_manager.cpp
2.3 % 1 / 44 1.1 % 2 / 176
src/smt/unsat_core_manager.h
0.0 % 0 / 2 100.0 % 0 / 0
src/smt/update_ostream.h
2.4 % 1 / 41 0.0 % 0 / 56
src/smt/witness_form.cpp
1.3 % 1 / 78 0.5 % 2 / 364
src/smt/witness_form.h
0.0 % 0 / 1 0.0 % 0 / 2
src/smt_util/boolean_simplification.cpp
55.6 % 15 / 27 37.3 % 38 / 102
src/smt_util/boolean_simplification.h
84.4 % 54 / 64 38.7 % 75 / 194
src/smt_util/nary_builder.cpp
12.0 % 11 / 92 3.5 % 12 / 343
src/theory/arith/approx_simplex.cpp
2.8 % 4 / 143 0.5 % 2 / 433
src/theory/arith/approx_simplex.h
0.0 % 0 / 3 0.0 % 0 / 2
src/theory/arith/arith_ite_utils.cpp
0.4 % 1 / 276 0.1 % 2 / 1428
src/theory/arith/arith_msum.cpp
91.0 % 131 / 144 52.6 % 345 / 656
src/theory/arith/arith_msum.h
100.0 % 2 / 2 55.0 % 11 / 20
src/theory/arith/arith_preprocess.cpp
25.0 % 6 / 24 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 % 400 / 455 41.4 % 1042 / 2515
src/theory/arith/arith_rewriter.h
100.0 % 3 / 3 33.3 % 2 / 6
src/theory/arith/arith_state.cpp
100.0 % 6 / 6 50.0 % 5 / 10
src/theory/arith/arith_state.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/arith/arith_static_learner.cpp
84.5 % 125 / 148 38.1 % 386 / 1013
src/theory/arith/arith_utilities.cpp
75.8 % 116 / 153 33.6 % 225 / 670
src/theory/arith/arith_utilities.h
71.9 % 64 / 89 33.3 % 55 / 165
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.0 % 16 / 320
src/theory/arith/attempt_solution_simplex.h
16.7 % 1 / 6 16.7 % 1 / 6
src/theory/arith/bound_counts.h
85.6 % 83 / 97 28.4 % 55 / 194
src/theory/arith/bound_inference.cpp
60.3 % 79 / 131 35.7 % 158 / 443
src/theory/arith/bound_inference.h
100.0 % 2 / 2 33.3 % 10 / 30
src/theory/arith/callbacks.cpp
87.7 % 100 / 114 19.0 % 103 / 542
src/theory/arith/callbacks.h
100.0 % 13 / 13 50.0 % 9 / 18
src/theory/arith/congruence_manager.cpp
68.7 % 276 / 402 23.7 % 479 / 2022
src/theory/arith/congruence_manager.h
100.0 % 3 / 3 50.0 % 1 / 2
src/theory/arith/constraint.cpp
59.6 % 844 / 1415 19.9 % 1420 / 7137
src/theory/arith/constraint.h
93.2 % 109 / 117 16.9 % 49 / 290
src/theory/arith/cut_log.cpp
0.3 % 1 / 399 0.2 % 2 / 932
src/theory/arith/cut_log.h
0.0 % 0 / 7 0.0 % 0 / 8
src/theory/arith/delta_rational.cpp
50.0 % 26 / 52 18.3 % 44 / 240
src/theory/arith/delta_rational.h
83.3 % 80 / 96 56.8 % 42 / 74
src/theory/arith/dio_solver.cpp
87.4 % 431 / 493 34.6 % 877 / 2538
src/theory/arith/dio_solver.h
77.5 % 31 / 40 16.9 % 23 / 136
src/theory/arith/dual_simplex.cpp
91.1 % 112 / 123 37.2 % 235 / 632
src/theory/arith/dual_simplex.h
100.0 % 7 / 7 50.0 % 1 / 2
src/theory/arith/error_set.cpp
65.2 % 189 / 290 26.7 % 190 / 711
src/theory/arith/error_set.h
51.1 % 47 / 92 9.6 % 16 / 166
src/theory/arith/fc_simplex.cpp
6.0 % 29 / 484 1.8 % 45 / 2482
src/theory/arith/fc_simplex.h
2.6 % 1 / 38 3.6 % 1 / 28
src/theory/arith/infer_bounds.cpp
24.3 % 33 / 136 3.2 % 8 / 247
src/theory/arith/infer_bounds.h
0.0 % 0 / 2 100.0 % 0 / 0
src/theory/arith/inference_manager.cpp
74.2 % 49 / 66 32.6 % 47 / 144
src/theory/arith/inference_manager.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/arith/linear_equality.cpp
44.9 % 364 / 811 18.1 % 663 / 3664
src/theory/arith/linear_equality.h
27.3 % 48 / 176 4.1 % 22 / 538
src/theory/arith/matrix.cpp
50.0 % 2 / 4 50.0 % 2 / 4
src/theory/arith/matrix.h
76.6 % 307 / 401 22.3 % 284 / 1276
src/theory/arith/nl/cad_solver.cpp
31.0 % 9 / 29 15.0 % 9 / 60
src/theory/arith/nl/ext/constraint.cpp
96.4 % 53 / 55 48.4 % 89 / 184
src/theory/arith/nl/ext/constraint.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/arith/nl/ext/ext_state.cpp
91.1 % 41 / 45 44.7 % 76 / 170
src/theory/arith/nl/ext/ext_state.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/ext/factoring_check.cpp
91.9 % 102 / 111 46.2 % 192 / 416
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 % 161 / 167 46.9 % 261 / 556
src/theory/arith/nl/ext/monomial.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/arith/nl/ext/monomial_bounds_check.cpp
56.0 % 159 / 284 27.8 % 320 / 1150
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
96.2 % 353 / 367 48.0 % 739 / 1538
src/theory/arith/nl/ext/monomial_check.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/ext/proof_checker.cpp
2.3 % 1 / 44 0.5 % 2 / 376
src/theory/arith/nl/ext/proof_checker.h
100.0 % 2 / 2 25.0 % 3 / 12
src/theory/arith/nl/ext/split_zero_check.cpp
22.2 % 4 / 18 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
94.6 % 70 / 74 48.6 % 175 / 360
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 48.1 % 99 / 206
src/theory/arith/nl/ext_theory_callback.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/arith/nl/iand_solver.cpp
76.8 % 119 / 155 34.2 % 261 / 764
src/theory/arith/nl/iand_utils.cpp
93.7 % 104 / 111 38.8 % 167 / 430
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.3 % 2 / 150
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 11.1 % 2 / 18
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 40.4 % 21 / 52
src/theory/arith/nl/nl_lemma_utils.h
94.4 % 17 / 18 40.0 % 4 / 10
src/theory/arith/nl/nl_model.cpp
80.7 % 597 / 740 39.6 % 1438 / 3635
src/theory/arith/nl/nonlinear_extension.cpp
86.8 % 269 / 310 48.8 % 470 / 964
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
61.5 % 56 / 91 34.9 % 88 / 252
src/theory/arith/nl/strategy.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/arith/nl/transcendental/exponential_solver.cpp
92.5 % 99 / 107 43.1 % 199 / 462
src/theory/arith/nl/transcendental/proof_checker.cpp
2.8 % 1 / 36 0.8 % 2 / 258
src/theory/arith/nl/transcendental/proof_checker.h
0.0 % 0 / 2 0.0 % 0 / 2
src/theory/arith/nl/transcendental/sine_solver.cpp
98.0 % 195 / 199 44.6 % 447 / 1002
src/theory/arith/nl/transcendental/sine_solver.h
83.3 % 20 / 24 75.0 % 12 / 16
src/theory/arith/nl/transcendental/taylor_generator.cpp
92.6 % 163 / 176 40.4 % 366 / 906
src/theory/arith/nl/transcendental/taylor_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/arith/nl/transcendental/transcendental_solver.cpp
86.1 % 179 / 208 41.5 % 351 / 845
src/theory/arith/nl/transcendental/transcendental_state.cpp
87.6 % 156 / 178 42.8 % 418 / 976
src/theory/arith/nl/transcendental/transcendental_state.h
100.0 % 1 / 1 75.0 % 3 / 4
src/theory/arith/normal_form.cpp
82.6 % 622 / 753 36.6 % 1147 / 3130
src/theory/arith/normal_form.h
96.8 % 368 / 380 35.5 % 440 / 1240
src/theory/arith/operator_elim.cpp
94.9 % 243 / 256 46.4 % 594 / 1281
src/theory/arith/operator_elim.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/arith/partial_model.cpp
78.7 % 318 / 404 32.5 % 317 / 976
src/theory/arith/partial_model.h
100.0 % 34 / 34 50.0 % 1 / 2
src/theory/arith/proof_checker.cpp
0.8 % 1 / 122 0.3 % 2 / 660
src/theory/arith/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/arith/rewrites.cpp
5.6 % 1 / 18 12.5 % 2 / 16
src/theory/arith/simplex.cpp
35.8 % 58 / 162 14.3 % 95 / 664
src/theory/arith/simplex.h
21.4 % 3 / 14 0.0 % 0 / 2
src/theory/arith/simplex_update.cpp
0.9 % 1 / 108 0.5 % 2 / 395
src/theory/arith/simplex_update.h
0.0 % 0 / 55 0.0 % 0 / 116
src/theory/arith/soi_simplex.cpp
6.4 % 35 / 551 2.1 % 58 / 2800
src/theory/arith/soi_simplex.h
6.3 % 1 / 16 8.3 % 1 / 12
src/theory/arith/tableau.cpp
69.7 % 76 / 109 23.8 % 135 / 568
src/theory/arith/tableau.h
54.5 % 18 / 33 8.3 % 4 / 48
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
93.2 % 124 / 133 43.2 % 160 / 370
src/theory/arith/theory_arith.h
75.0 % 3 / 4 0.0 % 0 / 2
src/theory/arith/theory_arith_private.cpp
55.0 % 1732 / 3151 24.8 % 3689 / 14854
src/theory/arith/theory_arith_private.h
84.8 % 28 / 33 21.9 % 7 / 32
src/theory/arith/theory_arith_type_rules.h
87.5 % 42 / 48 36.6 % 59 / 161
src/theory/arith/type_enumerator.h
100.0 % 39 / 39 42.9 % 54 / 126
src/theory/arrays/array_info.cpp
67.6 % 207 / 306 29.7 % 295 / 994
src/theory/arrays/array_info.h
100.0 % 15 / 15 38.3 % 23 / 60
src/theory/arrays/inference_manager.cpp
34.6 % 18 / 52 20.1 % 41 / 204
src/theory/arrays/inference_manager.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/arrays/proof_checker.cpp
1.6 % 1 / 61 0.4 % 2 / 492
src/theory/arrays/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/arrays/skolem_cache.cpp
95.8 % 23 / 24 30.7 % 59 / 192
src/theory/arrays/theory_arrays.cpp
72.7 % 897 / 1233 35.7 % 2463 / 6895
src/theory/arrays/theory_arrays.h
97.4 % 38 / 39 55.6 % 60 / 108
src/theory/arrays/theory_arrays_rewriter.cpp
100.0 % 9 / 9 42.9 % 6 / 14
src/theory/arrays/theory_arrays_rewriter.h
99.3 % 285 / 287 53.1 % 786 / 1481
src/theory/arrays/theory_arrays_type_rules.h
66.4 % 87 / 131 25.4 % 172 / 676
src/theory/arrays/type_enumerator.h
90.9 % 60 / 66 49.0 % 98 / 200
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 % 14 / 14 75.0 % 3 / 4
src/theory/bags/bag_solver.cpp
92.7 % 102 / 110 37.9 % 165 / 435
src/theory/bags/bags_rewriter.cpp
94.5 % 207 / 219 45.3 % 843 / 1861
src/theory/bags/bags_rewriter.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/bags/bags_statistics.cpp
100.0 % 7 / 7 50.0 % 6 / 12
src/theory/bags/infer_info.cpp
43.8 % 14 / 32 14.7 % 20 / 136
src/theory/bags/infer_info.h
100.0 % 2 / 2 50.0 % 4 / 8
src/theory/bags/inference_generator.cpp
90.3 % 139 / 154 31.5 % 318 / 1008
src/theory/bags/inference_generator.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bags/inference_manager.cpp
78.6 % 11 / 14 46.4 % 13 / 28
src/theory/bags/inference_manager.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/bags/make_bag_op.cpp
84.6 % 11 / 13 41.7 % 5 / 12
src/theory/bags/make_bag_op.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bags/normal_form.cpp
93.5 % 245 / 262 42.8 % 607 / 1418
src/theory/bags/rewrites.cpp
2.2 % 1 / 46 4.5 % 2 / 44
src/theory/bags/solver_state.cpp
100.0 % 68 / 68 47.7 % 125 / 262
src/theory/bags/solver_state.h
100.0 % 1 / 1 50.0 % 1 / 2
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
89.9 % 107 / 119 40.2 % 165 / 410
src/theory/bags/theory_bags.h
80.0 % 4 / 5 25.0 % 1 / 4
src/theory/bags/theory_bags_type_enumerator.cpp
3.1 % 1 / 32 1.8 % 2 / 112
src/theory/bags/theory_bags_type_rules.h
72.3 % 94 / 130 25.7 % 189 / 734
src/theory/booleans/circuit_propagator.cpp
80.2 % 275 / 343 42.5 % 763 / 1794
src/theory/booleans/circuit_propagator.h
100.0 % 34 / 34 47.6 % 59 / 124
src/theory/booleans/proof_checker.cpp
0.2 % 1 / 529 0.1 % 2 / 3740
src/theory/booleans/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/booleans/proof_circuit_propagator.cpp
34.8 % 86 / 247 2.9 % 32 / 1112
src/theory/booleans/proof_circuit_propagator.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/booleans/theory_bool.cpp
90.5 % 19 / 21 47.3 % 35 / 74
src/theory/booleans/theory_bool.h
66.7 % 2 / 3 25.0 % 1 / 4
src/theory/booleans/theory_bool_rewriter.cpp
95.5 % 212 / 222 54.9 % 865 / 1575
src/theory/booleans/theory_bool_rewriter.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/booleans/theory_bool_type_rules.h
100.0 % 29 / 29 53.6 % 75 / 140
src/theory/booleans/type_enumerator.h
100.0 % 17 / 17 40.0 % 18 / 45
src/theory/builtin/proof_checker.cpp
0.4 % 1 / 269 0.2 % 2 / 1153
src/theory/builtin/proof_checker.h
100.0 % 2 / 2 50.0 % 2 / 4
src/theory/builtin/theory_builtin.cpp
72.7 % 8 / 11 31.8 % 7 / 22
src/theory/builtin/theory_builtin.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/builtin/theory_builtin_rewriter.cpp
92.0 % 230 / 250 44.3 % 710 / 1603
src/theory/builtin/theory_builtin_rewriter.h
100.0 % 2 / 2 50.0 % 2 / 4
src/theory/builtin/theory_builtin_type_rules.cpp
100.0 % 8 / 8 34.8 % 16 / 46
src/theory/builtin/theory_builtin_type_rules.h
62.1 % 72 / 116 33.4 % 165 / 494
src/theory/builtin/type_enumerator.cpp
7.1 % 1 / 14 3.3 % 2 / 60
src/theory/builtin/type_enumerator.h
88.9 % 24 / 27 39.8 % 35 / 88
src/theory/bv/abstraction.cpp
27.3 % 174 / 638 9.6 % 282 / 2936
src/theory/bv/abstraction.h
18.8 % 6 / 32 1.9 % 1 / 52
src/theory/bv/bitblast/bitblast_strategies_template.h
80.0 % 363 / 454 28.6 % 745 / 2606
src/theory/bv/bitblast/bitblast_utils.h
88.8 % 95 / 107 37.4 % 158 / 422
src/theory/bv/bitblast/bitblaster.h
95.4 % 103 / 108 39.8 % 113 / 284
src/theory/bv/bitblast/eager_bitblaster.cpp
90.0 % 117 / 130 34.7 % 207 / 597
src/theory/bv/bitblast/eager_bitblaster.h
75.0 % 3 / 4 50.0 % 2 / 4
src/theory/bv/bitblast/lazy_bitblaster.cpp
70.2 % 221 / 315 31.3 % 372 / 1189
src/theory/bv/bitblast/lazy_bitblaster.h
57.1 % 4 / 7 50.0 % 1 / 2
src/theory/bv/bitblast/simple_bitblaster.cpp
87.1 % 61 / 70 36.0 % 103 / 286
src/theory/bv/bitblast/simple_bitblaster.h
50.0 % 1 / 2 16.7 % 1 / 6
src/theory/bv/bv_eager_solver.cpp
82.6 % 38 / 46 25.0 % 57 / 228
src/theory/bv/bv_inequality_graph.cpp
94.7 % 284 / 300 39.6 % 518 / 1307
src/theory/bv/bv_inequality_graph.h
100.0 % 37 / 37 27.7 % 31 / 112
src/theory/bv/bv_quick_check.cpp
0.5 % 1 / 199 0.5 % 2 / 420
src/theory/bv/bv_quick_check.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/bv/bv_solver.h
64.0 % 16 / 25 10.0 % 1 / 10
src/theory/bv/bv_solver_bitblast.cpp
0.7 % 1 / 136 0.3 % 2 / 602
src/theory/bv/bv_solver_bitblast.h
0.0 % 0 / 6 0.0 % 0 / 4
src/theory/bv/bv_solver_lazy.cpp
88.1 % 339 / 385 44.8 % 758 / 1692
src/theory/bv/bv_solver_lazy.h
95.0 % 19 / 20 32.6 % 15 / 46
src/theory/bv/bv_solver_simple.cpp
49.2 % 30 / 61 23.8 % 51 / 214
src/theory/bv/bv_solver_simple.h
80.0 % 4 / 5 25.0 % 1 / 4
src/theory/bv/bv_subtheory.h
44.0 % 11 / 25 22.0 % 9 / 41
src/theory/bv/bv_subtheory_algebraic.cpp
0.3 % 2 / 606 0.1 % 2 / 2573
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.5 % 190 / 494
src/theory/bv/bv_subtheory_bitblast.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/bv/bv_subtheory_core.cpp
85.5 % 266 / 311 44.5 % 543 / 1221
src/theory/bv/bv_subtheory_core.h
100.0 % 8 / 8 50.0 % 2 / 4
src/theory/bv/bv_subtheory_inequality.cpp
78.2 % 111 / 142 39.2 % 257 / 656
src/theory/bv/bv_subtheory_inequality.h
100.0 % 5 / 5 50.0 % 6 / 12
src/theory/bv/proof_checker.cpp
5.3 % 1 / 19 1.6 % 2 / 124
src/theory/bv/proof_checker.h
100.0 % 2 / 2 25.0 % 1 / 4
src/theory/bv/slicer.cpp
3.1 % 1 / 32 2.7 % 2 / 74
src/theory/bv/slicer.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/bv/theory_bv.cpp
71.4 % 80 / 112 34.3 % 81 / 236
src/theory/bv/theory_bv.h
0.0 % 0 / 1 0.0 % 0 / 2
src/theory/bv/theory_bv_rewrite_rules.h
30.2 % 73 / 242 23.1 % 5064 / 21941
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
88.2 % 135 / 153 45.2 % 317 / 702
src/theory/bv/theory_bv_rewrite_rules_core.h
100.0 % 144 / 144 57.7 % 263 / 456
src/theory/bv/theory_bv_rewrite_rules_normalization.h
92.6 % 665 / 718 47.0 % 1401 / 2981
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
75.8 % 270 / 356 34.3 % 442 / 1288
src/theory/bv/theory_bv_rewrite_rules_simplification.h
88.5 % 659 / 745 45.0 % 1962 / 4356
src/theory/bv/theory_bv_rewriter.cpp
94.4 % 285 / 302 50.3 % 449 / 892
src/theory/bv/theory_bv_rewriter.h
100.0 % 1 / 1 25.0 % 1 / 4
src/theory/bv/theory_bv_type_rules.h
71.1 % 101 / 142 30.0 % 138 / 460
src/theory/bv/theory_bv_utils.cpp
91.1 % 216 / 237 40.2 % 354 / 880
src/theory/bv/theory_bv_utils.h
100.0 % 18 / 18 38.6 % 44 / 114
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
96.9 % 31 / 32 47.9 % 45 / 94
src/theory/combination_engine.cpp
92.5 % 37 / 40 19.8 % 17 / 86
src/theory/datatypes/datatypes_rewriter.cpp
92.7 % 380 / 410 45.1 % 852 / 1888
src/theory/datatypes/datatypes_rewriter.h
100.0 % 1 / 1 36.4 % 8 / 22
src/theory/datatypes/infer_proof_cons.cpp
0.8 % 1 / 132 0.2 % 2 / 934
src/theory/datatypes/infer_proof_cons.h
0.0 % 0 / 1 0.0 % 0 / 2
src/theory/datatypes/inference.cpp
73.9 % 17 / 23 33.9 % 38 / 112
src/theory/datatypes/inference.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/datatypes/inference_manager.cpp
75.8 % 50 / 66 37.0 % 94 / 254
src/theory/datatypes/proof_checker.cpp
1.4 % 1 / 72 0.4 % 2 / 518
src/theory/datatypes/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/datatypes/sygus_datatype_utils.cpp
86.1 % 327 / 380 37.9 % 689 / 1820
src/theory/datatypes/sygus_extension.cpp
85.4 % 851 / 996 39.4 % 2027 / 5146
src/theory/datatypes/sygus_extension.h
100.0 % 8 / 8 50.0 % 5 / 10
src/theory/datatypes/sygus_simple_sym.cpp
92.9 % 261 / 281 50.3 % 570 / 1134
src/theory/datatypes/sygus_simple_sym.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/datatypes/theory_datatypes.cpp
89.2 % 1081 / 1212 44.8 % 2541 / 5677
src/theory/datatypes/theory_datatypes.h
88.2 % 15 / 17 47.6 % 20 / 42
src/theory/datatypes/theory_datatypes_type_rules.h
77.3 % 208 / 269 30.5 % 394 / 1292
src/theory/datatypes/theory_datatypes_utils.cpp
83.7 % 82 / 98 41.0 % 193 / 471
src/theory/datatypes/type_enumerator.cpp
100.0 % 168 / 168 47.6 % 394 / 828
src/theory/datatypes/type_enumerator.h
100.0 % 46 / 46 54.3 % 51 / 94
src/theory/decision_manager.cpp
100.0 % 47 / 47 52.2 % 72 / 138
src/theory/decision_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/decision_strategy.cpp
95.0 % 57 / 60 52.4 % 86 / 164
src/theory/decision_strategy.h
100.0 % 5 / 5 50.0 % 3 / 6
src/theory/eager_proof_generator.cpp
6.5 % 4 / 62 3.5 % 7 / 202
src/theory/eager_proof_generator.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/ee_manager.cpp
92.3 % 12 / 13 50.0 % 10 / 20
src/theory/ee_manager.h
75.0 % 3 / 4 50.0 % 1 / 2
src/theory/ee_manager_distributed.cpp
97.8 % 45 / 46 34.9 % 44 / 126
src/theory/ee_manager_distributed.h
44.4 % 4 / 9 50.0 % 1 / 2
src/theory/ee_setup_info.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/engine_output_channel.cpp
80.7 % 96 / 119 35.5 % 117 / 330
src/theory/engine_output_channel.h
100.0 % 1 / 1 25.0 % 1 / 4
src/theory/evaluator.cpp
76.3 % 334 / 438 36.3 % 668 / 1839
src/theory/evaluator.h
83.3 % 5 / 6 100.0 % 0 / 0
src/theory/ext_theory.cpp
71.0 % 174 / 245 35.4 % 311 / 878
src/theory/ext_theory.h
87.5 % 7 / 8 50.0 % 3 / 6
src/theory/fp/fp_converter.cpp
65.5 % 448 / 684 29.8 % 1081 / 3629
src/theory/fp/fp_converter.h
100.0 % 5 / 5 100.0 % 0 / 0
src/theory/fp/theory_fp.cpp
66.7 % 404 / 606 26.2 % 890 / 3402
src/theory/fp/theory_fp.h
85.7 % 6 / 7 33.3 % 2 / 6
src/theory/fp/theory_fp_rewriter.cpp
73.8 % 532 / 721 23.4 % 947 / 4043
src/theory/fp/theory_fp_rewriter.h
100.0 % 1 / 1 50.0 % 2 / 4
src/theory/fp/theory_fp_type_rules.h
58.7 % 165 / 281 23.3 % 339 / 1458
src/theory/fp/type_enumerator.h
59.5 % 25 / 42 27.0 % 20 / 74
src/theory/inference_id.cpp
0.6 % 1 / 173 1.2 % 2 / 171
src/theory/inference_manager_buffered.cpp
92.7 % 76 / 82 34.1 % 58 / 170
src/theory/inference_manager_buffered.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/interrupted.h
0.0 % 0 / 1 0.0 % 0 / 2
src/theory/logic_info.cpp
90.7 % 390 / 430 57.6 % 418 / 726
src/theory/logic_info.h
100.0 % 21 / 21 83.3 % 15 / 18
src/theory/model_manager.cpp
95.1 % 98 / 103 50.0 % 121 / 242
src/theory/model_manager_distributed.cpp
83.3 % 40 / 48 39.4 % 37 / 94
src/theory/output_channel.cpp
41.7 % 15 / 36 13.9 % 5 / 36
src/theory/output_channel.h
50.0 % 3 / 6 50.0 % 1 / 2
src/theory/quantifiers/alpha_equivalence.cpp
98.2 % 54 / 55 42.3 % 110 / 260
src/theory/quantifiers/alpha_equivalence.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/quantifiers/bv_inverter.cpp
93.0 % 186 / 200 43.7 % 489 / 1120
src/theory/quantifiers/bv_inverter.h
100.0 % 6 / 6 50.0 % 5 / 10
src/theory/quantifiers/bv_inverter_utils.cpp
98.9 % 820 / 829 48.0 % 2653 / 5532
src/theory/quantifiers/candidate_rewrite_database.cpp
66.4 % 87 / 131 29.2 % 147 / 504
src/theory/quantifiers/candidate_rewrite_database.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/candidate_rewrite_filter.cpp
91.3 % 115 / 126 42.3 % 273 / 646
src/theory/quantifiers/candidate_rewrite_filter.h
100.0 % 6 / 6 50.0 % 3 / 6
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
85.1 % 452 / 531 41.3 % 1186 / 2874
src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
100.0 % 2 / 2 70.8 % 17 / 24
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
85.4 % 299 / 350 38.4 % 689 / 1796
src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
100.0 % 3 / 3 50.0 % 2 / 4
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
100.0 % 171 / 171 40.4 % 470 / 1164
src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
91.4 % 64 / 70 50.2 % 161 / 321
src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
100.0 % 3 / 3 50.0 % 3 / 6
src/theory/quantifiers/cegqi/ceg_instantiator.cpp
91.4 % 812 / 888 48.8 % 1697 / 3478
src/theory/quantifiers/cegqi/ceg_instantiator.h
75.4 % 43 / 57 55.3 % 21 / 38
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
92.8 % 259 / 279 47.0 % 483 / 1028
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
100.0 % 3 / 3 50.0 % 3 / 6
src/theory/quantifiers/cegqi/nested_qe.cpp
89.7 % 70 / 78 44.0 % 148 / 336
src/theory/quantifiers/cegqi/nested_qe.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/cegqi/vts_term_cache.cpp
93.9 % 138 / 147 51.2 % 310 / 606
src/theory/quantifiers/cegqi/vts_term_cache.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/conjecture_generator.cpp
88.6 % 1247 / 1407 42.0 % 2627 / 6250
src/theory/quantifiers/conjecture_generator.h
85.7 % 42 / 49 60.5 % 23 / 38
src/theory/quantifiers/dynamic_rewrite.cpp
93.0 % 80 / 86 50.5 % 184 / 364
src/theory/quantifiers/dynamic_rewrite.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/ematching/candidate_generator.cpp
96.0 % 170 / 177 41.9 % 353 / 842
src/theory/quantifiers/ematching/candidate_generator.h
100.0 % 11 / 11 50.0 % 7 / 14
src/theory/quantifiers/ematching/ho_trigger.cpp
89.1 % 228 / 256 40.1 % 475 / 1184
src/theory/quantifiers/ematching/inst_match_generator.cpp
85.6 % 297 / 347 41.8 % 607 / 1452
src/theory/quantifiers/ematching/inst_match_generator.h
50.0 % 6 / 12 50.0 % 1 / 2
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
94.5 % 138 / 146 52.2 % 214 / 410
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
98.9 % 87 / 88 46.4 % 116 / 250
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
88.6 % 78 / 88 42.2 % 195 / 462
src/theory/quantifiers/ematching/inst_match_generator_simple.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/ematching/inst_strategy.cpp
75.0 % 9 / 12 25.0 % 4 / 16
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
76.0 % 272 / 358 36.5 % 497 / 1363
src/theory/quantifiers/ematching/inst_strategy_e_matching.h
100.0 % 3 / 3 68.8 % 11 / 16
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
63.1 % 53 / 84 36.4 % 91 / 250
src/theory/quantifiers/ematching/instantiation_engine.cpp
86.3 % 113 / 131 43.4 % 179 / 412
src/theory/quantifiers/ematching/instantiation_engine.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/ematching/pattern_term_selector.cpp
91.5 % 332 / 363 48.1 % 770 / 1602
src/theory/quantifiers/ematching/trigger.cpp
89.0 % 162 / 182 41.7 % 253 / 606
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.7 % 29 / 30 52.0 % 52 / 100
src/theory/quantifiers/ematching/var_match_generator.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/equality_query.cpp
77.8 % 70 / 90 38.5 % 168 / 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 40.7 % 48 / 118
src/theory/quantifiers/expr_miner.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/expr_miner_manager.cpp
55.8 % 43 / 77 34.1 % 47 / 138
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 47.6 % 1886 / 3960
src/theory/quantifiers/extended_rewrite.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/first_order_model.cpp
93.6 % 147 / 157 45.5 % 243 / 534
src/theory/quantifiers/first_order_model.h
57.1 % 4 / 7 41.7 % 10 / 24
src/theory/quantifiers/fmf/bounded_integers.cpp
93.5 % 487 / 521 44.7 % 1245 / 2784
src/theory/quantifiers/fmf/bounded_integers.h
100.0 % 14 / 14 61.1 % 11 / 18
src/theory/quantifiers/fmf/first_order_model_fmc.cpp
100.0 % 68 / 68 48.1 % 127 / 264
src/theory/quantifiers/fmf/first_order_model_fmc.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/fmf/full_model_check.cpp
93.6 % 740 / 791 50.1 % 1624 / 3241
src/theory/quantifiers/fmf/full_model_check.h
100.0 % 13 / 13 50.0 % 4 / 8
src/theory/quantifiers/fmf/model_builder.cpp
50.8 % 32 / 63 19.5 % 44 / 226
src/theory/quantifiers/fmf/model_builder.h
80.0 % 4 / 5 50.0 % 1 / 2
src/theory/quantifiers/fmf/model_engine.cpp
70.3 % 123 / 175 33.3 % 221 / 664
src/theory/quantifiers/fmf/model_engine.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/fun_def_evaluator.cpp
91.0 % 131 / 144 41.1 % 332 / 808
src/theory/quantifiers/fun_def_evaluator.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/inst_match.cpp
56.5 % 26 / 46 17.9 % 29 / 162
src/theory/quantifiers/inst_match.h
7.1 % 1 / 14 0.0 % 0 / 12
src/theory/quantifiers/inst_match_trie.cpp
45.2 % 70 / 155 20.7 % 84 / 406
src/theory/quantifiers/inst_match_trie.h
100.0 % 10 / 10 50.0 % 1 / 2
src/theory/quantifiers/inst_strategy_enumerative.cpp
87.3 % 144 / 165 43.5 % 283 / 650
src/theory/quantifiers/inst_strategy_enumerative.h
100.0 % 3 / 3 50.0 % 2 / 4
src/theory/quantifiers/instantiate.cpp
68.5 % 200 / 292 29.9 % 373 / 1248
src/theory/quantifiers/instantiate.h
100.0 % 3 / 3 50.0 % 2 / 4
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 38.5 % 130 / 338
src/theory/quantifiers/lazy_trie.h
100.0 % 6 / 6 50.0 % 2 / 4
src/theory/quantifiers/proof_checker.cpp
1.6 % 1 / 64 0.5 % 2 / 382
src/theory/quantifiers/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/quant_conflict_find.cpp
83.0 % 1155 / 1391 45.0 % 2511 / 5579
src/theory/quantifiers/quant_conflict_find.h
100.0 % 18 / 18 52.6 % 20 / 38
src/theory/quantifiers/quant_module.cpp
91.7 % 22 / 24 43.8 % 7 / 16
src/theory/quantifiers/quant_module.h
81.8 % 9 / 11 50.0 % 1 / 2
src/theory/quantifiers/quant_relevance.cpp
95.0 % 19 / 20 58.3 % 21 / 36
src/theory/quantifiers/quant_relevance.h
50.0 % 2 / 4 25.0 % 1 / 4
src/theory/quantifiers/quant_rep_bound_ext.cpp
95.8 % 23 / 24 42.2 % 27 / 64
src/theory/quantifiers/quant_rep_bound_ext.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/quant_split.cpp
97.9 % 95 / 97 51.0 % 200 / 392
src/theory/quantifiers/quant_split.h
100.0 % 2 / 2 50.0 % 2 / 4
src/theory/quantifiers/quant_util.cpp
81.9 % 68 / 83 41.5 % 93 / 224
src/theory/quantifiers/quant_util.h
100.0 % 4 / 4 50.0 % 1 / 2
src/theory/quantifiers/quantifiers_attributes.cpp
71.8 % 148 / 206 41.1 % 344 / 838
src/theory/quantifiers/quantifiers_attributes.h
100.0 % 6 / 6 50.0 % 4 / 8
src/theory/quantifiers/quantifiers_inference_manager.cpp
100.0 % 9 / 9 41.7 % 5 / 12
src/theory/quantifiers/quantifiers_modules.cpp
100.0 % 41 / 41 65.1 % 56 / 86
src/theory/quantifiers/quantifiers_registry.cpp
73.1 % 57 / 78 33.5 % 65 / 194
src/theory/quantifiers/quantifiers_registry.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/quantifiers_rewriter.cpp
76.6 % 889 / 1161 39.8 % 2056 / 5171
src/theory/quantifiers/quantifiers_rewriter.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/quantifiers_state.cpp
46.7 % 35 / 75 24.6 % 58 / 236
src/theory/quantifiers/quantifiers_state.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/query_generator.cpp
0.9 % 2 / 219 0.3 % 2 / 704
src/theory/quantifiers/query_generator.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/relevant_domain.cpp
98.5 % 199 / 202 53.3 % 503 / 944
src/theory/quantifiers/relevant_domain.h
100.0 % 12 / 12 50.0 % 1 / 2
src/theory/quantifiers/single_inv_partition.cpp
89.0 % 276 / 310 47.3 % 511 / 1080
src/theory/quantifiers/single_inv_partition.h
100.0 % 7 / 7 83.3 % 5 / 6
src/theory/quantifiers/skolemize.cpp
78.2 % 161 / 206 35.1 % 372 / 1060
src/theory/quantifiers/skolemize.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/solution_filter.cpp
63.6 % 28 / 44 28.3 % 47 / 166
src/theory/quantifiers/solution_filter.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
96.4 % 271 / 281 44.3 % 587 / 1324
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.3 % 1330 / 3220
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.5 % 319 / 341 46.1 % 620 / 1344
src/theory/quantifiers/sygus/cegis.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/sygus/cegis_core_connective.cpp
88.8 % 404 / 455 42.2 % 818 / 1939
src/theory/quantifiers/sygus/cegis_core_connective.h
100.0 % 6 / 6 50.0 % 4 / 8
src/theory/quantifiers/sygus/cegis_unif.cpp
86.8 % 297 / 342 35.8 % 535 / 1494
src/theory/quantifiers/sygus/cegis_unif.h
100.0 % 5 / 5 50.0 % 14 / 28
src/theory/quantifiers/sygus/enum_stream_substitution.cpp
66.4 % 227 / 342 29.0 % 332 / 1146
src/theory/quantifiers/sygus/enum_stream_substitution.h
100.0 % 6 / 6 50.0 % 3 / 6
src/theory/quantifiers/sygus/example_eval_cache.cpp
98.0 % 49 / 50 37.4 % 74 / 198
src/theory/quantifiers/sygus/example_infer.cpp
84.4 % 103 / 122 36.1 % 174 / 482
src/theory/quantifiers/sygus/example_min_eval.cpp
100.0 % 30 / 30 41.4 % 48 / 116
src/theory/quantifiers/sygus/example_min_eval.h
100.0 % 5 / 5 50.0 % 3 / 6
src/theory/quantifiers/sygus/sygus_abduct.cpp
98.8 % 82 / 83 45.8 % 207 / 452
src/theory/quantifiers/sygus/sygus_enumerator.cpp
87.8 % 576 / 656 39.3 % 952 / 2420
src/theory/quantifiers/sygus/sygus_enumerator.h
100.0 % 9 / 9 50.0 % 6 / 12
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 / 4
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
97.8 % 178 / 182 41.1 % 403 / 980
src/theory/quantifiers/sygus/sygus_eval_unfold.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_explain.cpp
95.8 % 158 / 165 35.8 % 311 / 868
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 % 789 / 901 41.0 % 1472 / 3590
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.0 % 126 / 257 20.0 % 227 / 1134
src/theory/quantifiers/sygus/sygus_grammar_norm.h
40.0 % 8 / 20 6.8 % 3 / 44
src/theory/quantifiers/sygus/sygus_grammar_red.cpp
97.5 % 77 / 79 43.6 % 177 / 406
src/theory/quantifiers/sygus/sygus_grammar_red.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/sygus/sygus_interpol.cpp
84.5 % 153 / 181 39.3 % 276 / 702
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 37.7 % 208 / 552
src/theory/quantifiers/sygus/sygus_invariance.h
95.0 % 19 / 20 47.4 % 18 / 38
src/theory/quantifiers/sygus/sygus_module.cpp
100.0 % 4 / 4 33.3 % 2 / 6
src/theory/quantifiers/sygus/sygus_module.h
40.0 % 2 / 5 50.0 % 1 / 2
src/theory/quantifiers/sygus/sygus_pbe.cpp
100.0 % 118 / 118 42.4 % 233 / 550
src/theory/quantifiers/sygus/sygus_process_conj.cpp
91.0 % 354 / 389 43.1 % 644 / 1494
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 % 80 / 81 46.6 % 181 / 388
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.4 % 301 / 333 40.4 % 607 / 1504
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.7 % 55 / 154
src/theory/quantifiers/sygus/sygus_unif_io.cpp
90.6 % 750 / 828 39.7 % 1402 / 3530
src/theory/quantifiers/sygus/sygus_unif_io.h
100.0 % 13 / 13 58.3 % 7 / 12
src/theory/quantifiers/sygus/sygus_unif_rl.cpp
68.7 % 435 / 633 29.3 % 772 / 2632
src/theory/quantifiers/sygus/sygus_unif_rl.h
100.0 % 7 / 7 31.9 % 15 / 47
src/theory/quantifiers/sygus/sygus_unif_strat.cpp
83.2 % 476 / 572 42.1 % 949 / 2254
src/theory/quantifiers/sygus/sygus_unif_strat.h
100.0 % 18 / 18 50.0 % 4 / 8
src/theory/quantifiers/sygus/sygus_utils.cpp
75.0 % 57 / 76 29.1 % 114 / 392
src/theory/quantifiers/sygus/synth_conjecture.cpp
87.5 % 602 / 688 40.2 % 1320 / 3282
src/theory/quantifiers/sygus/synth_conjecture.h
100.0 % 9 / 9 50.0 % 1 / 2
src/theory/quantifiers/sygus/synth_engine.cpp
95.7 % 133 / 139 53.3 % 224 / 420
src/theory/quantifiers/sygus/synth_engine.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/quantifiers/sygus/template_infer.cpp
97.9 % 94 / 96 43.7 % 242 / 554
src/theory/quantifiers/sygus/template_infer.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/quantifiers/sygus/term_database_sygus.cpp
86.9 % 478 / 550 41.5 % 892 / 2149
src/theory/quantifiers/sygus/term_database_sygus.h
100.0 % 7 / 7 62.5 % 5 / 8
src/theory/quantifiers/sygus/transition_inference.cpp
94.3 % 282 / 299 45.8 % 534 / 1166
src/theory/quantifiers/sygus/transition_inference.h
100.0 % 12 / 12 50.0 % 4 / 8
src/theory/quantifiers/sygus/type_info.cpp
87.7 % 200 / 228 40.1 % 319 / 796
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.0 % 210 / 253 36.7 % 390 / 1064
src/theory/quantifiers/sygus_inst.h
100.0 % 2 / 2 50.0 % 2 / 4
src/theory/quantifiers/sygus_sampler.cpp
79.7 % 369 / 463 37.5 % 591 / 1578
src/theory/quantifiers/sygus_sampler.h
100.0 % 3 / 3 50.0 % 1 / 2
src/theory/quantifiers/term_database.cpp
81.6 % 551 / 675 42.2 % 1300 / 3082
src/theory/quantifiers/term_database.h
100.0 % 3 / 3 50.0 % 2 / 4
src/theory/quantifiers/term_enumeration.cpp
72.3 % 34 / 47 44.9 % 62 / 138
src/theory/quantifiers/term_enumeration.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/quantifiers/term_util.cpp
85.1 % 268 / 315 55.1 % 577 / 1048
src/theory/quantifiers/theory_quantifiers.cpp
92.8 % 64 / 69 47.9 % 69 / 144
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 31.6 % 120 / 380
src/theory/quantifiers_engine.cpp
87.8 % 417 / 475 44.5 % 751 / 1688
src/theory/relevance_manager.cpp
72.1 % 101 / 140 27.5 % 150 / 546
src/theory/relevance_manager.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/rep_set.cpp
74.1 % 186 / 251 34.1 % 280 / 820
src/theory/rep_set.h
64.3 % 9 / 14 50.0 % 1 / 2
src/theory/rewriter.cpp
62.5 % 125 / 200 27.1 % 223 / 824
src/theory/rewriter.h
100.0 % 1 / 1 75.0 % 12 / 16
src/theory/rewriter_attributes.h
100.0 % 30 / 30 42.4 % 640 / 1508
src/theory/sep/theory_sep.cpp
83.5 % 917 / 1098 40.6 % 2332 / 5748
src/theory/sep/theory_sep.h
56.3 % 18 / 32 20.4 % 22 / 108
src/theory/sep/theory_sep_rewriter.cpp
88.9 % 80 / 90 44.5 % 182 / 409
src/theory/sep/theory_sep_rewriter.h
100.0 % 4 / 4 50.0 % 11 / 22
src/theory/sep/theory_sep_type_rules.h
90.7 % 39 / 43 22.9 % 50 / 218
src/theory/sets/cardinality_extension.cpp
89.9 % 517 / 575 46.3 % 1233 / 2663
src/theory/sets/cardinality_extension.h
100.0 % 4 / 4 100.0 % 0 / 0
src/theory/sets/inference_manager.cpp
49.4 % 42 / 85 24.3 % 91 / 374
src/theory/sets/inference_manager.h
100.0 % 1 / 1 25.0 % 1 / 4
src/theory/sets/normal_form.h
97.0 % 65 / 67 48.9 % 175 / 358
src/theory/sets/rels_utils.h
100.0 % 44 / 44 49.3 % 75 / 152
src/theory/sets/singleton_op.cpp
85.7 % 12 / 14 41.7 % 5 / 12
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 % 41 / 84
src/theory/sets/skolem_cache.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/sets/solver_state.cpp
92.9 % 273 / 294 45.8 % 580 / 1266
src/theory/sets/solver_state.h
100.0 % 2 / 2 66.7 % 4 / 6
src/theory/sets/term_registry.cpp
80.0 % 60 / 75 44.3 % 116 / 262
src/theory/sets/term_registry.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/sets/theory_sets.cpp
92.5 % 99 / 107 47.2 % 151 / 320
src/theory/sets/theory_sets.h
80.0 % 4 / 5 25.0 % 1 / 4
src/theory/sets/theory_sets_private.cpp
94.1 % 659 / 700 46.2 % 1456 / 3152
src/theory/sets/theory_sets_private.h
66.7 % 2 / 3 0.0 % 0 / 2
src/theory/sets/theory_sets_rels.cpp
95.8 % 751 / 784 51.5 % 1741 / 3379
src/theory/sets/theory_sets_rels.h
100.0 % 2 / 2 100.0 % 0 / 0
src/theory/sets/theory_sets_rewriter.cpp
96.5 % 307 / 318 48.6 % 923 / 1901
src/theory/sets/theory_sets_rewriter.h
100.0 % 1 / 1 33.3 % 2 / 6
src/theory/sets/theory_sets_type_enumerator.cpp
100.0 % 61 / 61 45.4 % 89 / 196
src/theory/sets/theory_sets_type_rules.h
77.0 % 161 / 209 25.4 % 299 / 1176
src/theory/shared_solver.cpp
65.9 % 27 / 41 43.9 % 36 / 82
src/theory/shared_solver.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/shared_solver_distributed.cpp
100.0 % 34 / 34 54.9 % 56 / 102
src/theory/shared_solver_distributed.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/shared_terms_database.cpp
81.5 % 123 / 151 29.2 % 219 / 750
src/theory/shared_terms_database.h
100.0 % 24 / 24 31.6 % 12 / 38
src/theory/smt_engine_subsolver.cpp
81.3 % 39 / 48 32.9 % 48 / 146
src/theory/sort_inference.cpp
83.9 % 433 / 516 45.5 % 1024 / 2250
src/theory/sort_inference.h
83.3 % 5 / 6 100.0 % 0 / 0
src/theory/strings/arith_entail.cpp
90.5 % 344 / 380 45.4 % 892 / 1964
src/theory/strings/base_solver.cpp
78.1 % 296 / 379 38.5 % 640 / 1661
src/theory/strings/base_solver.h
100.0 % 2 / 2 50.0 % 2 / 4
src/theory/strings/core_solver.cpp
80.2 % 1109 / 1383 39.2 % 2587 / 6601
src/theory/strings/core_solver.h
100.0 % 2 / 2 40.9 % 9 / 22
src/theory/strings/eager_solver.cpp
98.5 % 66 / 67 52.5 % 124 / 236
src/theory/strings/eqc_info.cpp
100.0 % 57 / 57 43.3 % 154 / 356
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.2 % 803 / 1738
src/theory/strings/extf_solver.h
100.0 % 4 / 4 50.0 % 2 / 4
src/theory/strings/infer_info.cpp
68.8 % 22 / 32 32.5 % 39 / 120
src/theory/strings/infer_info.h
100.0 % 2 / 2 50.0 % 5 / 10
src/theory/strings/infer_proof_cons.cpp
0.2 % 1 / 500 0.1 % 2 / 2150
src/theory/strings/infer_proof_cons.h
0.0 % 0 / 1 0.0 % 0 / 2
src/theory/strings/inference_manager.cpp
85.5 % 159 / 186 42.5 % 355 / 836
src/theory/strings/inference_manager.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/strings/normal_form.cpp
100.0 % 85 / 85 42.5 % 158 / 372
src/theory/strings/normal_form.h
100.0 % 2 / 2 50.0 % 3 / 6
src/theory/strings/proof_checker.cpp
0.3 % 1 / 295 0.1 % 2 / 1982
src/theory/strings/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/strings/regexp_elim.cpp
76.8 % 225 / 293 31.8 % 452 / 1422
src/theory/strings/regexp_elim.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/regexp_entail.cpp
88.4 % 321 / 363 47.7 % 704 / 1477
src/theory/strings/regexp_operation.cpp
73.8 % 696 / 943 35.8 % 1560 / 4360
src/theory/strings/regexp_solver.cpp
90.7 % 302 / 333 47.9 % 634 / 1323
src/theory/strings/regexp_solver.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/rewrites.cpp
0.5 % 1 / 193 1.0 % 2 / 191
src/theory/strings/sequences_rewriter.cpp
96.4 % 1534 / 1591 51.1 % 4797 / 9390
src/theory/strings/sequences_rewriter.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/strings/sequences_stats.cpp
100.0 % 38 / 38 49.3 % 66 / 134
src/theory/strings/skolem_cache.cpp
91.1 % 112 / 123 48.8 % 274 / 561
src/theory/strings/skolem_cache.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/strings/solver_state.cpp
95.2 % 100 / 105 45.2 % 161 / 356
src/theory/strings/strategy.cpp
70.7 % 58 / 82 34.1 % 86 / 252
src/theory/strings/strings_entail.cpp
96.3 % 421 / 437 46.0 % 984 / 2139
src/theory/strings/strings_fmf.cpp
92.7 % 38 / 41 53.3 % 48 / 90
src/theory/strings/strings_fmf.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/strings/strings_rewriter.cpp
100.0 % 161 / 161 47.1 % 435 / 924
src/theory/strings/strings_rewriter.h
100.0 % 1 / 1 30.0 % 3 / 10
src/theory/strings/term_registry.cpp
92.6 % 276 / 298 46.9 % 657 / 1400
src/theory/strings/theory_strings.cpp
82.7 % 473 / 572 41.8 % 1024 / 2449
src/theory/strings/theory_strings.h
100.0 % 32 / 32 52.2 % 70 / 134
src/theory/strings/theory_strings_preprocess.cpp
100.0 % 486 / 486 51.2 % 1450 / 2832
src/theory/strings/theory_strings_type_rules.h
68.7 % 103 / 150 25.6 % 134 / 524
src/theory/strings/theory_strings_utils.cpp
90.6 % 174 / 192 43.7 % 334 / 764
src/theory/strings/type_enumerator.cpp
87.3 % 117 / 134 33.6 % 88 / 262
src/theory/strings/type_enumerator.h
100.0 % 7 / 7 50.0 % 5 / 10
src/theory/strings/word.cpp
82.6 % 233 / 282 28.8 % 328 / 1140
src/theory/subs_minimize.cpp
0.4 % 1 / 223 0.2 % 2 / 880
src/theory/substitutions.cpp
85.3 % 93 / 109 40.0 % 225 / 562
src/theory/substitutions.h
90.9 % 20 / 22 45.5 % 10 / 22
src/theory/term_registration_visitor.cpp
78.6 % 103 / 131 40.0 % 223 / 558
src/theory/term_registration_visitor.h
100.0 % 9 / 9 50.0 % 1 / 2
src/theory/theory.cpp
85.7 % 203 / 237 44.7 % 401 / 897
src/theory/theory.h
81.9 % 77 / 94 40.8 % 71 / 174
src/theory/theory_engine.cpp
66.2 % 566 / 855 32.9 % 1492 / 4534
src/theory/theory_engine.h
100.0 % 48 / 48 27.3 % 114 / 418
src/theory/theory_engine_proof_generator.cpp
8.5 % 5 / 59 2.6 % 7 / 272
src/theory/theory_engine_proof_generator.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/theory_eq_notify.h
78.9 % 15 / 19 57.7 % 15 / 26
src/theory/theory_id.cpp
86.1 % 68 / 79 56.2 % 59 / 105
src/theory/theory_inference.cpp
73.3 % 11 / 15 26.5 % 9 / 34
src/theory/theory_inference.h
72.7 % 8 / 11 50.0 % 4 / 8
src/theory/theory_inference_manager.cpp
75.6 % 158 / 209 33.8 % 161 / 476
src/theory/theory_model.cpp
89.7 % 374 / 417 41.9 % 817 / 1950
src/theory/theory_model.h
100.0 % 4 / 4 50.0 % 1 / 2
src/theory/theory_model_builder.cpp
94.8 % 660 / 696 42.7 % 1317 / 3084
src/theory/theory_model_builder.h
100.0 % 4 / 4 50.0 % 1 / 2
src/theory/theory_preprocessor.cpp
70.9 % 158 / 223 30.4 % 351 / 1156
src/theory/theory_proof_step_buffer.cpp
1.0 % 1 / 100 0.6 % 2 / 354
src/theory/theory_proof_step_buffer.h
0.0 % 0 / 1 100.0 % 0 / 0
src/theory/theory_rewriter.cpp
5.9 % 1 / 17 4.0 % 2 / 50
src/theory/theory_rewriter.h
66.7 % 4 / 6 50.0 % 1 / 2
src/theory/theory_state.cpp
100.0 % 64 / 64 40.0 % 84 / 210
src/theory/theory_state.h
100.0 % 1 / 1 50.0 % 1 / 2
src/theory/theory_test_utils.h
65.4 % 17 / 26 22.7 % 5 / 22
src/theory/trust_node.cpp
64.5 % 40 / 62 21.6 % 50 / 232
src/theory/trust_node.h
100.0 % 3 / 3 100.0 % 0 / 0
src/theory/trust_substitutions.cpp
35.2 % 37 / 105 15.4 % 76 / 492
src/theory/trust_substitutions.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/type_enumerator.h
94.5 % 52 / 55 28.9 % 56 / 194
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
81.0 % 821 / 1014 40.5 % 1756 / 4340
src/theory/uf/cardinality_extension.h
96.4 % 53 / 55 35.2 % 45 / 128
src/theory/uf/eq_proof.cpp
0.1 % 1 / 722 0.1 % 2 / 3944
src/theory/uf/eq_proof.h
0.0 % 0 / 2 100.0 % 0 / 0
src/theory/uf/equality_engine.cpp
83.0 % 1131 / 1363 38.1 % 2232 / 5856
src/theory/uf/equality_engine.h
94.9 % 37 / 39 16.7 % 7 / 42
src/theory/uf/equality_engine_iterator.cpp
78.3 % 47 / 60 21.4 % 47 / 220
src/theory/uf/equality_engine_notify.h
63.6 % 7 / 11 50.0 % 2 / 4
src/theory/uf/equality_engine_types.h
80.3 % 61 / 76 31.6 % 12 / 38
src/theory/uf/ho_extension.cpp
83.7 % 200 / 239 40.2 % 426 / 1060
src/theory/uf/ho_extension.h
100.0 % 1 / 1 100.0 % 0 / 0
src/theory/uf/proof_checker.cpp
0.9 % 1 / 115 0.3 % 2 / 636
src/theory/uf/proof_checker.h
100.0 % 2 / 2 50.0 % 1 / 2
src/theory/uf/proof_equality_engine.cpp
0.4 % 1 / 254 0.1 % 2 / 1352
src/theory/uf/proof_equality_engine.h
0.0 % 0 / 1 0.0 % 0 / 2
src/theory/uf/symmetry_breaker.cpp
83.5 % 411 / 492 43.3 % 989 / 2282
src/theory/uf/symmetry_breaker.h
100.0 % 7 / 7 25.0 % 5 / 20
src/theory/uf/theory_uf.cpp
86.7 % 268 / 309 47.3 % 630 / 1332
src/theory/uf/theory_uf.h
94.7 % 18 / 19 48.4 % 31 / 64
src/theory/uf/theory_uf_model.cpp
57.6 % 72 / 125 31.8 % 143 / 450
src/theory/uf/theory_uf_model.h
100.0 % 16 / 16 53.3 % 16 / 30
src/theory/uf/theory_uf_rewriter.h
91.4 % 85 / 93 48.2 % 220 / 456
src/theory/uf/theory_uf_type_rules.h
65.8 % 50 / 76 27.0 % 86 / 318
src/theory/valuation.cpp
67.8 % 59 / 87 17.0 % 58 / 341
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 % 161 / 163 22.4 % 153 / 684
src/util/bitvector.cpp
100.0 % 169 / 169 56.3 % 179 / 318
src/util/bitvector.h
91.7 % 66 / 72 63.6 % 21 / 33
src/util/bool.h
100.0 % 2 / 2 100.0 % 0 / 0
src/util/cardinality.cpp
79.3 % 115 / 145 47.1 % 229 / 486
src/util/cardinality.h
100.0 % 25 / 25 54.5 % 12 / 22
src/util/dense_map.h
82.0 % 91 / 111 13.8 % 97 / 701
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.4 % 199 / 271 28.9 % 240 / 830
src/util/floatingpoint.h
90.2 % 55 / 61 50.0 % 2 / 4
src/util/floatingpoint_literal_symfpu.cpp
92.5 % 111 / 120 25.0 % 76 / 304
src/util/floatingpoint_size.cpp
100.0 % 10 / 10 15.0 % 12 / 80
src/util/floatingpoint_size.h
100.0 % 16 / 16 50.0 % 2 / 4
src/util/hash.h
100.0 % 8 / 8 50.0 % 2 / 4
src/util/iand.h
50.0 % 2 / 4 100.0 % 0 / 0
src/util/integer_cln_imp.cpp
91.7 % 222 / 242 40.4 % 192 / 475
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 15.7 % 16 / 102
src/util/random.h
100.0 % 3 / 3 100.0 % 2 / 2
src/util/rational_cln_imp.cpp
65.9 % 27 / 41 33.7 % 33 / 98
src/util/rational_cln_imp.h
92.0 % 103 / 112 43.0 % 37 / 86
src/util/regexp.cpp
76.5 % 13 / 17 50.0 % 2 / 4
src/util/resource_manager.cpp
77.3 % 160 / 207 38.8 % 125 / 322
src/util/resource_manager.h
100.0 % 2 / 2 66.7 % 4 / 6
src/util/result.cpp
61.0 % 119 / 195 36.5 % 92 / 252
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
78.6 % 81 / 103 54.5 % 48 / 88
src/util/safe_print.h
86.7 % 13 / 15 12.5 % 5 / 40
src/util/sampler.cpp
10.6 % 7 / 66 5.9 % 12 / 203
src/util/sexpr.cpp
71.1 % 123 / 173 32.4 % 122 / 377
src/util/sexpr.h
62.5 % 5 / 8 100.0 % 0 / 0
src/util/smt2_quote_string.cpp
100.0 % 8 / 8 75.0 % 18 / 24
src/util/statistics.cpp
16.9 % 13 / 77 5.6 % 4 / 72
src/util/statistics.h
80.0 % 4 / 5 50.0 % 1 / 2
src/util/statistics_registry.cpp
81.6 % 80 / 98 26.5 % 61 / 230
src/util/statistics_registry.h
63.0 % 143 / 227 25.3 % 116 / 459
src/util/string.cpp
95.8 % 250 / 261 56.0 % 288 / 514
src/util/string.h
95.8 % 23 / 24 50.0 % 3 / 6
src/util/tuple.h
71.4 % 5 / 7 100.0 % 0 / 0
src/util/utility.cpp
5.9 % 1 / 17 5.6 % 2 / 36
src/util/utility.h
100.0 % 17 / 17 29.5 % 13 / 44
test/api/boilerplate.cpp
100.0 % 5 / 5 50.0 % 7 / 14
test/api/issue4889.cpp
100.0 % 16 / 16 50.0 % 18 / 36
test/api/issue5074.cpp
100.0 % 10 / 10 50.0 % 16 / 32
test/api/ouroborous.cpp
91.4 % 53 / 58 48.1 % 103 / 214
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 % 375 / 375 33.8 % 1015 / 3004
test/unit/api/grammar_black.cpp
100.0 % 57 / 57 36.1 % 240 / 664
test/unit/api/op_black.cpp
100.0 % 89 / 89 30.6 % 221 / 722
test/unit/api/result_black.cpp
100.0 % 75 / 75 34.6 % 206 / 596
test/unit/api/solver_black.cpp
99.3 % 1414 / 1424 36.1 % 6037 / 16732
test/unit/api/sort_black.cpp
100.0 % 244 / 244 34.3 % 778 / 2268
test/unit/api/term_black.cpp
100.0 % 692 / 692 32.0 % 2988 / 9344
test/unit/base/map_util_black.cpp
100.0 % 103 / 103 30.3 % 343 / 1132
test/unit/context/cdlist_black.cpp
100.0 % 74 / 74 31.1 % 118 / 380
test/unit/context/cdmap_black.cpp
100.0 % 80 / 80 29.0 % 251 / 865
test/unit/context/cdmap_white.cpp
100.0 % 10 / 10 25.4 % 68 / 268
test/unit/context/cdo_black.cpp
100.0 % 13 / 13 27.8 % 25 / 90
test/unit/context/context_black.cpp
97.3 % 108 / 111 24.7 % 212 / 860
test/unit/context/context_mm_black.cpp
97.1 % 34 / 35 36.9 % 41 / 111
test/unit/context/context_white.cpp
100.0 % 117 / 117 22.1 % 320 / 1448
test/unit/expr/attribute_black.cpp
100.0 % 47 / 47 33.3 % 104 / 312
test/unit/expr/attribute_white.cpp
100.0 % 314 / 314 28.6 % 1011 / 3534
test/unit/expr/kind_black.cpp
100.0 % 35 / 35 30.0 % 60 / 200
test/unit/expr/kind_map_black.cpp
100.0 % 10 / 10 30.5 % 25 / 82
test/unit/expr/node_algorithm_black.cpp
100.0 % 87 / 87 35.3 % 316 / 896
test/unit/expr/node_black.cpp
99.8 % 438 / 439 34.2 % 1539 / 4501
test/unit/expr/node_builder_black.cpp
100.0 % 324 / 324 27.9 % 1546 / 5536
test/unit/expr/node_manager_black.cpp
100.0 % 210 / 210 31.0 % 670 / 2158
test/unit/expr/node_manager_white.cpp
100.0 % 32 / 32 30.5 % 130 / 426
test/unit/expr/node_self_iterator_black.cpp
100.0 % 22 / 22 30.3 % 86 / 284
test/unit/expr/node_traversal_black.cpp
100.0 % 170 / 170 39.4 % 496 / 1260
test/unit/expr/node_white.cpp
100.0 % 35 / 35 31.9 % 113 / 354
test/unit/expr/symbol_table_black.cpp
100.0 % 74 / 74 34.9 % 213 / 610
test/unit/expr/type_cardinality_black.cpp
100.0 % 157 / 157 37.5 % 649 / 1732
test/unit/expr/type_node_white.cpp
100.0 % 49 / 49 30.1 % 182 / 604
test/unit/main/interactive_shell_black.cpp
100.0 % 58 / 58 45.7 % 63 / 138
test/unit/memory.h
100.0 % 12 / 12 21.4 % 6 / 28
test/unit/parser/parser_black.cpp
100.0 % 215 / 215 43.7 % 353 / 808
test/unit/parser/parser_builder_black.cpp
100.0 % 62 / 62 38.6 % 81 / 210
test/unit/preprocessing/pass_bv_gauss_white.h
97.6 % 1464 / 1500 47.0 % 4177 / 8878
test/unit/preprocessing/pass_foreign_theory_rewrite_white.h
96.3 % 26 / 27 47.2 % 34 / 72
test/unit/printer/smt2_printer_black.h
100.0 % 24 / 24 48.6 % 35 / 72
test/unit/prop/cnf_stream_white.h
91.8 % 134 / 146 45.8 % 152 / 332
test/unit/test.h
100.0 % 1 / 1 50.0 % 1 / 2
test/unit/test_api.h
100.0 % 1 / 1 50.0 % 2 / 4
test/unit/test_context.h
100.0 % 2 / 2 50.0 % 2 / 4
test/unit/test_expr.h
100.0 % 12 / 12 50.0 % 5 / 10
test/unit/test_node.h
100.0 % 14 / 14 50.0 % 14 / 28
test/unit/theory/evaluator_white.h
98.8 % 85 / 86 49.7 % 170 / 342
test/unit/theory/logic_info_white.h
99.7 % 1228 / 1232 21.5 % 3025 / 14051
test/unit/theory/regexp_operation_black.h
98.9 % 86 / 87 49.8 % 227 / 456
test/unit/theory/sequences_rewriter_white.h
99.9 % 885 / 886 49.4 % 2322 / 4698
test/unit/theory/strings_rewriter_white.h
96.7 % 29 / 30 48.9 % 43 / 88
test/unit/theory/theory_arith_white.h
99.4 % 175 / 176 48.9 % 342 / 700
test/unit/theory/theory_bags_normal_form_white.h
99.7 % 292 / 293 47.1 % 823 / 1748
test/unit/theory/theory_bags_rewriter_white.h