Head

GCC Code Coverage Report

Directory:	.			Exec	Total	Coverage
Date:	2021-09-06		Lines:	147874	205644	71.9 %
Legend:	low: < 75.0 % medium: >= 75.0 % high: >= 90.0 %		Branches:	279479	784045	35.6 %

File

Lines

Branches

build-coverage/deps/include/cryptominisat5/solvertypesmini.h

100.0 %

15 / 15

100.0 %

0 / 0

build-coverage/deps/include/poly/polyxx/assignment.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/deps/include/poly/polyxx/integer.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/deps/include/poly/polyxx/polynomial.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/deps/include/poly/polyxx/upolynomial.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/deps/include/symfpu/core/add.h

98.4 %

120 / 122

61.8 %

352 / 570

build-coverage/deps/include/symfpu/core/classify.h

100.0 %

21 / 21

67.2 %

43 / 64

build-coverage/deps/include/symfpu/core/compare.h

95.4 %

62 / 65

62.2 %

222 / 357

build-coverage/deps/include/symfpu/core/convert.h

81.4 %

105 / 129

37.7 %

154 / 408

build-coverage/deps/include/symfpu/core/divide.h

100.0 %

43 / 43

61.5 %

99 / 161

build-coverage/deps/include/symfpu/core/fma.h

0.0 %

0 / 24

0.0 %

0 / 70

build-coverage/deps/include/symfpu/core/ite.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/deps/include/symfpu/core/multiply.h

100.0 %

33 / 33

62.9 %

66 / 105

build-coverage/deps/include/symfpu/core/operations.h

100.0 %

187 / 187

52.3 %

354 / 677

build-coverage/deps/include/symfpu/core/packing.h

100.0 %

61 / 61

62.6 %

134 / 214

build-coverage/deps/include/symfpu/core/remainder.h

100.0 %

54 / 54

59.0 %

102 / 173

build-coverage/deps/include/symfpu/core/rounder.h

100.0 %

148 / 148

56.1 %

409 / 729

build-coverage/deps/include/symfpu/core/sign.h

100.0 %

10 / 10

55.6 %

10 / 18

build-coverage/deps/include/symfpu/core/sqrt.h

100.0 %

35 / 35

56.9 %

87 / 153

build-coverage/deps/include/symfpu/core/unpackedFloat.h

100.0 %

139 / 139

54.8 %

266 / 485

build-coverage/deps/include/symfpu/utils/common.h

100.0 %

23 / 23

80.0 %

8 / 10

build-coverage/src/expr/kind.cpp

56.2 %

396 / 705

55.3 %

384 / 694

build-coverage/src/expr/kind.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/src/expr/metakind.cpp

78.1 %

580 / 743

46.6 %

366 / 786

build-coverage/src/expr/metakind.h

100.0 %

12 / 12

11.0 %

486 / 4400

build-coverage/src/expr/type_checker.cpp

90.5 %

855 / 945

52.0 %

1158 / 2228

build-coverage/src/expr/type_properties.h

33.0 %

35 / 106

16.5 %

42 / 254

build-coverage/src/main/options.cpp

24.3 %

603 / 2486

13.9 %

785 / 5634

build-coverage/src/options/arith_options.cpp

2.9 %

12 / 419

2.9 %

9 / 306

build-coverage/src/options/arith_options.h

81.3 %

13 / 16

100.0 %

0 / 0

build-coverage/src/options/arrays_options.cpp

2.7 %

1 / 37

9.1 %

2 / 22

build-coverage/src/options/arrays_options.h

100.0 %

7 / 7

100.0 %

0 / 0

build-coverage/src/options/base_options.cpp

10.4 %

12 / 115

10.7 %

8 / 75

build-coverage/src/options/base_options.h

77.8 %

7 / 9

50.0 %

2 / 4

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

15.7 %

29 / 185

16.9 %

25 / 148

build-coverage/src/options/bv_options.h

65.2 %

15 / 23

50.0 %

1 / 2

build-coverage/src/options/datatypes_options.cpp

6.5 %

7 / 107

8.3 %

6 / 72

build-coverage/src/options/datatypes_options.h

100.0 %

20 / 20

100.0 %

0 / 0

build-coverage/src/options/decision_options.cpp

8.0 %

10 / 125

7.6 %

9 / 119

build-coverage/src/options/decision_options.h

55.6 %

5 / 9

100.0 %

0 / 0

build-coverage/src/options/expr_options.cpp

7.7 %

1 / 13

20.0 %

2 / 10

build-coverage/src/options/expr_options.h

100.0 %

4 / 4

100.0 %

0 / 0

build-coverage/src/options/fp_options.cpp

11.1 %

1 / 9

25.0 %

2 / 8

build-coverage/src/options/fp_options.h

100.0 %

3 / 3

100.0 %

0 / 0

build-coverage/src/options/main_options.cpp

1.8 %

1 / 57

6.3 %

2 / 32

build-coverage/src/options/main_options.h

100.0 %

3 / 3

100.0 %

0 / 0

build-coverage/src/options/options.cpp

100.0 %

52 / 52

50.0 %

25 / 50

build-coverage/src/options/options.h

100.0 %

13 / 13

100.0 %

0 / 0

build-coverage/src/options/options_public.cpp

75.2 %

1858 / 2471

27.1 %

2661 / 9814

build-coverage/src/options/parser_options.cpp

4.0 %

1 / 25

12.5 %

2 / 16

build-coverage/src/options/parser_options.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/src/options/printer_options.cpp

9.4 %

5 / 53

7.4 %

4 / 54

build-coverage/src/options/printer_options.h

66.7 %

2 / 3

100.0 %

0 / 0

build-coverage/src/options/proof_options.cpp

4.0 %

4 / 99

3.2 %

3 / 95

build-coverage/src/options/proof_options.h

100.0 %

5 / 5

100.0 %

0 / 0

build-coverage/src/options/prop_options.cpp

2.7 %

1 / 37

9.1 %

2 / 22

build-coverage/src/options/prop_options.h

100.0 %

10 / 10

100.0 %

0 / 0

build-coverage/src/options/quantifiers_options.cpp

3.7 %

52 / 1399

3.3 %

35 / 1068

build-coverage/src/options/quantifiers_options.h

94.4 %

170 / 180

100.0 %

0 / 0

build-coverage/src/options/sep_options.cpp

4.0 %

1 / 25

12.5 %

2 / 16

build-coverage/src/options/sep_options.h

100.0 %

6 / 6

100.0 %

0 / 0

build-coverage/src/options/sets_options.cpp

7.7 %

1 / 13

20.0 %

2 / 10

build-coverage/src/options/sets_options.h

100.0 %

4 / 4

100.0 %

0 / 0

build-coverage/src/options/smt_options.cpp

14.0 %

58 / 415

11.4 %

38 / 333

build-coverage/src/options/smt_options.h

97.2 %

35 / 36

100.0 %

0 / 0

build-coverage/src/options/strings_options.cpp

0.7 %

1 / 137

2.0 %

2 / 101

build-coverage/src/options/strings_options.h

100.0 %

20 / 20

100.0 %

0 / 0

build-coverage/src/options/theory_options.cpp

14.7 %

11 / 75

10.5 %

8 / 76

build-coverage/src/options/theory_options.h

100.0 %

7 / 7

100.0 %

0 / 0

build-coverage/src/options/uf_options.cpp

10.2 %

6 / 59

10.9 %

5 / 46

build-coverage/src/options/uf_options.h

100.0 %

8 / 8

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.7 %

4627 / 13726

29.1 %

3790 / 13013

build-coverage/src/parser/smt2/Smt2Lexer.c

73.6 %

1981 / 2693

59.8 %

947 / 1584

build-coverage/src/parser/smt2/Smt2Parser.c

72.9 %

3327 / 4566

45.6 %

2561 / 5619

build-coverage/src/parser/tptp/TptpLexer.c

76.9 %

1406 / 1828

55.7 %

494 / 887

build-coverage/src/parser/tptp/TptpParser.c

63.5 %

3075 / 4840

42.5 %

2041 / 4807

build-coverage/src/theory/rewriter_tables.h

60.8 %

62 / 102

37.8 %

130 / 344

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

41.2 %

42 / 102

src/api/cpp/cvc5.cpp

76.0 %

2614 / 3440

27.2 %

7049 / 25902

src/api/cpp/cvc5.h

89.3 %

25 / 28

50.0 %

3 / 6

src/base/check.cpp

67.6 %

48 / 71

45.3 %

29 / 64

src/base/check.h

100.0 %

3 / 3

100.0 %

0 / 0

src/base/configuration.cpp

76.2 %

109 / 143

40.1 %

117 / 292

src/base/configuration.h

100.0 %

2 / 2

100.0 %

0 / 0

src/base/exception.cpp

73.2 %

60 / 82

36.2 %

42 / 116

src/base/exception.h

90.9 %

30 / 33

47.2 %

17 / 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

79.3 %

96 / 121

15.6 %

140 / 895

src/context/cdhashmap.h

97.6 %

120 / 123

39.7 %

510 / 1285

src/context/cdhashset.h

83.3 %

35 / 42

2.8 %

1 / 36

src/context/cdinsert_hashmap.h

98.1 %

102 / 104

32.5 %

214 / 658

src/context/cdlist.h

96.0 %

143 / 149

37.1 %

926 / 2496

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

48.3 %

84 / 174

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

86.4 %

171 / 198

36.3 %

211 / 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/assertion_list.cpp

83.6 %

51 / 61

45.9 %

73 / 159

src/decision/assertion_list.h

100.0 %

1 / 1

100.0 %

0 / 0

src/decision/decision_engine.cpp

100.0 %

20 / 20

50.0 %

2 / 4

src/decision/decision_engine.h

100.0 %

4 / 4

100.0 %

0 / 0

src/decision/decision_engine_old.cpp

61.0 %

25 / 41

23.3 %

35 / 150

src/decision/decision_engine_old.h

66.7 %

10 / 15

34.6 %

9 / 26

src/decision/decision_strategy.h

0.0 %

0 / 8

100.0 %

0 / 0

src/decision/justification_heuristic.cpp

0.5 %

2 / 378

0.1 %

2 / 1489

src/decision/justification_heuristic.h

0.0 %

0 / 3

0.0 %

0 / 6

src/decision/justification_strategy.cpp

97.8 %

273 / 279

43.9 %

494 / 1126

src/decision/justification_strategy.h

100.0 %

1 / 1

100.0 %

0 / 0

src/decision/justify_info.cpp

80.0 %

16 / 20

20.0 %

6 / 30

src/decision/justify_stack.cpp

92.7 %

38 / 41

24.0 %

25 / 104

src/decision/justify_stats.cpp

100.0 %

16 / 16

50.0 %

14 / 28

src/expr/array_store_all.cpp

53.7 %

22 / 41

45.0 %

45 / 100

src/expr/ascription_type.cpp

57.9 %

11 / 19

35.0 %

7 / 20

src/expr/attribute.cpp

37.7 %

23 / 61

4.7 %

4 / 86

src/expr/attribute.h

74.8 %

95 / 127

46.4 %

557 / 1201

src/expr/attribute_internals.h

100.0 %

68 / 68

30.4 %

56 / 184

src/expr/attribute_unique_id.h

0.0 %

0 / 5

100.0 %

0 / 0

src/expr/bound_var_manager.cpp

63.2 %

12 / 19

31.3 %

10 / 32

src/expr/bound_var_manager.h

100.0 %

9 / 9

39.5 %

45 / 114

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.7 %

415 / 473

36.0 %

718 / 1994

src/expr/dtype.h

50.0 %

1 / 2

45.0 %

18 / 40

src/expr/dtype_cons.cpp

93.2 %

315 / 338

37.8 %

492 / 1300

src/expr/dtype_cons.h

100.0 %

2 / 2

50.0 %

8 / 16

src/expr/dtype_selector.cpp

83.3 %

30 / 36

23.8 %

30 / 126

src/expr/dtype_selector.h

100.0 %

1 / 1

50.0 %

3 / 6

src/expr/emptybag.cpp

42.9 %

9 / 21

50.0 %

6 / 12

src/expr/emptyset.cpp

42.9 %

9 / 21

50.0 %

6 / 12

src/expr/expr_iomanip.cpp

81.5 %

44 / 54

72.2 %

13 / 18

src/expr/kind_map.h

100.0 %

8 / 8

66.7 %

4 / 6

src/expr/match_trie.cpp

99.1 %

107 / 108

49.4 %

160 / 324

src/expr/match_trie.h

100.0 %

3 / 3

25.0 %

1 / 4

src/expr/nary_match_trie.cpp

0.7 %

1 / 143

0.4 %

2 / 451

src/expr/nary_match_trie.h

0.0 %

0 / 1

0.0 %

0 / 2

src/expr/nary_term_util.cpp

0.7 %

1 / 135

0.4 %

2 / 445

src/expr/node.cpp

84.0 %

42 / 50

51.8 %

115 / 222

src/expr/node.h

84.5 %

300 / 355

23.0 %

803 / 3496

src/expr/node_algorithm.cpp

84.9 %

321 / 378

49.5 %

517 / 1044

src/expr/node_builder.cpp

76.0 %

278 / 366

17.1 %

201 / 1174

src/expr/node_builder.h

100.0 %

8 / 8

25.0 %

24 / 96

src/expr/node_converter.cpp

0.7 %

1 / 138

0.3 %

2 / 754

src/expr/node_converter.h

0.0 %

0 / 1

100.0 %

0 / 0

src/expr/node_manager.cpp

86.2 %

500 / 580

37.0 %

655 / 1772

src/expr/node_manager.h

90.2 %

174 / 193

26.9 %

541 / 2012

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

39.1 %

36 / 92

src/expr/node_trie.h

100.0 %

6 / 6

50.0 %

3 / 6

src/expr/node_value.cpp

31.3 %

10 / 32

16.2 %

12 / 74

src/expr/node_value.h

76.6 %

108 / 141

23.0 %

43 / 187

src/expr/node_visitor.h

100.0 %

33 / 33

50.0 %

89 / 178

src/expr/sequence.cpp

53.9 %

103 / 191

19.8 %

111 / 562

src/expr/sequence.h

100.0 %

3 / 3

100.0 %

0 / 0

src/expr/skolem_manager.cpp

94.2 %

162 / 172

40.9 %

320 / 782

src/expr/skolem_manager.h

100.0 %

2 / 2

100.0 %

0 / 0

src/expr/subs.cpp

39.5 %

34 / 86

15.1 %

32 / 212

src/expr/subs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/sygus_datatype.cpp

100.0 %

44 / 44

31.5 %

39 / 124

src/expr/sygus_datatype.h

100.0 %

3 / 3

30.0 %

3 / 10

src/expr/symbol_manager.cpp

96.6 %

144 / 149

53.8 %

127 / 236

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/term_canonize.cpp

99.1 %

108 / 109

53.9 %

208 / 386

src/expr/term_canonize.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/term_context.cpp

73.2 %

41 / 56

56.9 %

33 / 58

src/expr/term_context.h

100.0 %

10 / 10

100.0 %

0 / 0

src/expr/term_context_node.cpp

13.3 %

4 / 30

4.3 %

6 / 138

src/expr/term_context_stack.cpp

72.2 %

26 / 36

28.8 %

38 / 132

src/expr/term_context_stack.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/type_checker_util.h

75.0 %

36 / 48

11.0 %

171 / 1552

src/expr/type_matcher.cpp

95.2 %

59 / 62

53.8 %

84 / 156

src/expr/type_matcher.h

100.0 %

2 / 2

100.0 %

0 / 0

src/expr/type_node.cpp

86.0 %

289 / 336

37.5 %

391 / 1044

src/expr/type_node.h

83.3 %

160 / 192

20.2 %

150 / 743

src/expr/uninterpreted_constant.cpp

64.9 %

24 / 37

39.2 %

29 / 74

src/main/command_executor.cpp

74.0 %

71 / 96

44.8 %

163 / 364

src/main/command_executor.h

100.0 %

5 / 5

100.0 %

0 / 0

src/main/driver_unified.cpp

54.0 %

74 / 137

30.1 %

138 / 458

src/main/interactive_shell.cpp

67.1 %

57 / 85

35.4 %

103 / 291

src/main/main.cpp

75.0 %

18 / 24

36.8 %

39 / 106

src/main/signal_handlers.cpp

30.0 %

39 / 130

11.3 %

12 / 106

src/main/time_limit.cpp

70.0 %

14 / 20

22.2 %

4 / 18

src/omt/bitvector_optimizer.cpp

88.8 %

95 / 107

48.3 %

174 / 360

src/omt/bitvector_optimizer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/omt/integer_optimizer.cpp

100.0 %

28 / 28

47.6 %

39 / 82

src/omt/integer_optimizer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/omt/omt_optimizer.cpp

45.9 %

34 / 74

9.5 %

60 / 630

src/omt/omt_optimizer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/options/didyoumean.cpp

1.5 %

1 / 68

2.1 %

2 / 96

src/options/didyoumean.h

0.0 %

0 / 3

100.0 %

0 / 0

src/options/language.cpp

85.7 %

24 / 28

62.9 %

44 / 70

src/options/language.h

100.0 %

4 / 4

100.0 %

0 / 0

src/options/managed_streams.cpp

8.1 %

3 / 37

2.8 %

2 / 72

src/options/managed_streams.h

66.7 %

12 / 18

12.5 %

1 / 8

src/options/option_exception.cpp

100.0 %

2 / 2

50.0 %

3 / 6

src/options/option_exception.h

100.0 %

2 / 2

50.0 %

1 / 2

src/options/options_handler.cpp

44.7 %

134 / 300

23.9 %

140 / 586

src/options/options_handler.h

21.4 %

3 / 14

1.7 %

1 / 60

src/options/options_public.h

100.0 %

10 / 10

0.8 %

4 / 512

src/options/outputc.cpp

100.0 %

8 / 8

66.7 %

4 / 6

src/options/outputc.h

100.0 %

1 / 1

100.0 %

0 / 0

src/options/set_language.cpp

100.0 %

27 / 27

75.0 %

9 / 12

src/parser/antlr_input.cpp

95.3 %

205 / 215

50.6 %

236 / 466

src/parser/antlr_input.h

89.3 %

25 / 28

38.5 %

30 / 78

src/parser/antlr_input_imports.cpp

65.8 %

73 / 111

23.1 %

55 / 238

src/parser/antlr_line_buffered_input.cpp

67.0 %

59 / 88

17.0 %

15 / 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

74.4 %

29 / 39

32.9 %

23 / 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.1 %

364 / 498

34.1 %

452 / 1327

src/parser/parser.h

69.7 %

23 / 33

16.7 %

1 / 6

src/parser/parser_builder.cpp

97.0 %

64 / 66

58.1 %

50 / 86

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.4 %

587 / 672

47.6 %

1054 / 2212

src/parser/smt2/smt2.h

63.6 %

21 / 33

37.2 %

29 / 78

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

81.2 %

216 / 266

37.0 %

300 / 810

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 %

86 / 86

38.8 %

135 / 348

src/preprocessing/assertion_pipeline.h

100.0 %

14 / 14

100.0 %

4 / 4

src/preprocessing/learned_literal_manager.cpp

100.0 %

18 / 18

51.9 %

27 / 52

src/preprocessing/learned_literal_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ackermann.cpp

97.3 %

110 / 113

41.7 %

216 / 518

src/preprocessing/passes/ackermann.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/apply_substs.cpp

100.0 %

21 / 21

57.7 %

30 / 52

src/preprocessing/passes/apply_substs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bool_to_bv.cpp

96.7 %

176 / 182

52.1 %

408 / 783

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

54.2 %

13 / 24

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

61.5 %

16 / 26

src/preprocessing/passes/bv_eager_atoms.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_gauss.cpp

90.9 %

311 / 342

40.1 %

676 / 1686

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

51.3 %

61 / 119

src/preprocessing/passes/bv_intro_pow2.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_to_bool.cpp

97.4 %

152 / 156

40.6 %

370 / 912

src/preprocessing/passes/bv_to_bool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_to_int.cpp

89.6 %

429 / 479

41.4 %

844 / 2040

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

55.0 %

11 / 20

src/preprocessing/passes/extended_rewriter_pass.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/foreign_theory_rewrite.cpp

98.1 %

53 / 54

38.0 %

92 / 242

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.6 %

462 / 970

src/preprocessing/passes/global_negate.cpp

98.0 %

48 / 49

51.8 %

85 / 164

src/preprocessing/passes/global_negate.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ho_elim.cpp

97.9 %

323 / 330

46.1 %

700 / 1518

src/preprocessing/passes/ho_elim.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/int_to_bv.cpp

88.0 %

125 / 142

42.2 %

274 / 650

src/preprocessing/passes/int_to_bv.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ite_removal.cpp

100.0 %

22 / 22

46.4 %

26 / 56

src/preprocessing/passes/ite_removal.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ite_simp.cpp

48.7 %

58 / 119

14.6 %

63 / 432

src/preprocessing/passes/ite_simp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/learned_rewrite.cpp

54.1 %

120 / 222

24.0 %

214 / 890

src/preprocessing/passes/learned_rewrite.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/miplib_trick.cpp

11.6 %

42 / 363

2.4 %

43 / 1828

src/preprocessing/passes/nl_ext_purify.cpp

98.3 %

57 / 58

59.1 %

110 / 186

src/preprocessing/passes/nl_ext_purify.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/non_clausal_simp.cpp

96.4 %

215 / 223

41.5 %

490 / 1180

src/preprocessing/passes/non_clausal_simp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/pseudo_boolean_processor.cpp

75.3 %

149 / 198

28.1 %

261 / 929

src/preprocessing/passes/pseudo_boolean_processor.h

100.0 %

3 / 3

57.1 %

8 / 14

src/preprocessing/passes/quantifiers_preprocess.cpp

100.0 %

15 / 15

54.2 %

26 / 48

src/preprocessing/passes/quantifiers_preprocess.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/real_to_int.cpp

95.8 %

92 / 96

48.3 %

224 / 464

src/preprocessing/passes/real_to_int.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/rewrite.cpp

100.0 %

7 / 7

57.1 %

8 / 14

src/preprocessing/passes/rewrite.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/sep_skolem_emp.cpp

96.1 %

49 / 51

51.1 %

93 / 182

src/preprocessing/passes/sep_skolem_emp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/sort_infer.cpp

100.0 %

35 / 35

56.7 %

51 / 90

src/preprocessing/passes/sort_infer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/static_learning.cpp

100.0 %

15 / 15

55.6 %

20 / 36

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

57.1 %

24 / 42

src/preprocessing/passes/strings_eager_pp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/sygus_inference.cpp

95.7 %

155 / 162

48.9 %

303 / 620

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 / 988

src/preprocessing/passes/synth_rew_rules.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/theory_preprocess.cpp

100.0 %

19 / 19

46.0 %

23 / 50

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.6 %

109 / 234

src/preprocessing/passes/theory_rewrite_eq.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/unconstrained_simplifier.cpp

83.4 %

336 / 403

42.2 %

724 / 1717

src/preprocessing/passes/unconstrained_simplifier.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/preprocessing_pass.cpp

100.0 %

25 / 25

56.8 %

50 / 88

src/preprocessing/preprocessing_pass_context.cpp

91.4 %

32 / 35

47.5 %

19 / 40

src/preprocessing/preprocessing_pass_context.h

100.0 %

6 / 6

100.0 %

0 / 0

src/preprocessing/preprocessing_pass_registry.cpp

100.0 %

56 / 56

48.4 %

152 / 314

src/preprocessing/util/ite_utilities.cpp

46.5 %

458 / 986

21.2 %

782 / 3689

src/preprocessing/util/ite_utilities.h

18.6 %

8 / 43

9.1 %

4 / 44

src/printer/ast/ast_printer.cpp

22.3 %

50 / 224

19.9 %

51 / 256

src/printer/ast/ast_printer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/printer/cvc/cvc_printer.cpp

35.2 %

347 / 986

22.3 %

446 / 1997

src/printer/cvc/cvc_printer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/printer/let_binding.cpp

98.1 %

103 / 105

46.7 %

169 / 362

src/printer/let_binding.h

100.0 %

1 / 1

100.0 %

0 / 0

src/printer/printer.cpp

25.3 %

56 / 221

18.1 %

58 / 320

src/printer/printer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/printer/smt2/smt2_printer.cpp

51.0 %

600 / 1176

31.5 %

954 / 3030

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.2 %

2 / 62

src/printer/tptp/tptp_printer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/assumption_proof_generator.cpp

100.0 %

8 / 8

50.0 %

4 / 8

src/proof/assumption_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/buffered_proof_generator.cpp

75.0 %

33 / 44

33.3 %

52 / 156

src/proof/buffered_proof_generator.h

100.0 %

2 / 2

50.0 %

1 / 2

src/proof/conv_proof_generator.cpp

84.4 %

266 / 315

35.1 %

561 / 1597

src/proof/conv_seq_proof_generator.cpp

70.5 %

55 / 78

23.2 %

70 / 302

src/proof/dot/dot_printer.cpp

0.6 %

1 / 167

0.5 %

2 / 386

src/proof/eager_proof_generator.cpp

93.7 %

59 / 63

41.3 %

81 / 196

src/proof/eager_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/lazy_proof.cpp

97.0 %

96 / 99

48.6 %

173 / 356

src/proof/lazy_proof_chain.cpp

72.3 %

115 / 159

31.7 %

168 / 530

src/proof/lazy_tree_proof_generator.cpp

78.1 %

50 / 64

30.0 %

42 / 140

src/proof/lazy_tree_proof_generator.h

92.9 %

13 / 14

64.3 %

9 / 14

src/proof/lfsc/lfsc_node_converter.cpp

0.2 %

1 / 585

0.1 %

2 / 2478

src/proof/lfsc/lfsc_node_converter.h

0.0 %

0 / 1

100.0 %

0 / 0

src/proof/lfsc/lfsc_util.cpp

2.7 %

1 / 37

5.7 %

2 / 35

src/proof/lfsc/lfsc_util.h

0.0 %

0 / 1

100.0 %

0 / 0

src/proof/method_id.cpp

69.2 %

36 / 52

48.8 %

41 / 84

src/proof/proof.cpp

80.7 %

176 / 218

42.7 %

395 / 924

src/proof/proof_checker.cpp

56.7 %

93 / 164

20.5 %

125 / 610

src/proof/proof_checker.h

75.0 %

3 / 4

100.0 %

0 / 0

src/proof/proof_ensure_closed.cpp

15.8 %

12 / 76

4.0 %

16 / 398

src/proof/proof_generator.cpp

46.2 %

12 / 26

20.3 %

24 / 118

src/proof/proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_letify.cpp

2.2 %

1 / 46

1.8 %

2 / 110

src/proof/proof_letify.h

0.0 %

0 / 1

100.0 %

0 / 0

src/proof/proof_node.cpp

100.0 %

28 / 28

50.0 %

9 / 18

src/proof/proof_node.h

100.0 %

3 / 3

50.0 %

2 / 4

src/proof/proof_node_algorithm.cpp

78.0 %

85 / 109

42.2 %

86 / 204

src/proof/proof_node_manager.cpp

80.7 %

176 / 218

31.2 %

278 / 892

src/proof/proof_node_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_node_to_sexpr.cpp

69.2 %

119 / 172

25.8 %

154 / 598

src/proof/proof_node_to_sexpr.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_node_updater.cpp

78.7 %

107 / 136

37.0 %

139 / 376

src/proof/proof_node_updater.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_rule.cpp

20.5 %

36 / 176

18.2 %

29 / 159

src/proof/proof_set.h

100.0 %

7 / 7

66.7 %

10 / 15

src/proof/proof_step_buffer.cpp

59.1 %

26 / 44

20.5 %

18 / 88

src/proof/proof_step_buffer.h

100.0 %

2 / 2

25.0 %

1 / 4

src/proof/theory_proof_step_buffer.cpp

90.0 %

90 / 100

44.1 %

150 / 340

src/proof/theory_proof_step_buffer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/trust_node.cpp

75.0 %

48 / 64

34.3 %

70 / 204

src/proof/trust_node.h

100.0 %

3 / 3

100.0 %

0 / 0

src/proof/unsat_core.cpp

82.6 %

19 / 23

50.0 %

17 / 34

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

48.4 %

77 / 159

24.1 %

56 / 232

src/prop/bvminisat/bvminisat.h

60.0 %

9 / 15

0.0 %

0 / 6

src/prop/bvminisat/core/Solver.cc

55.5 %

361 / 651

25.2 %

354 / 1407

src/prop/bvminisat/core/Solver.h

76.7 %

56 / 73

46.5 %

40 / 86

src/prop/bvminisat/core/SolverTypes.h

94.7 %

124 / 131

35.9 %

61 / 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

25.6 %

20 / 78

src/prop/bvminisat/mtl/Sort.h

92.6 %

25 / 27

46.9 %

15 / 32

src/prop/bvminisat/mtl/Vec.h

97.8 %

45 / 46

38.6 %

132 / 342

src/prop/bvminisat/mtl/XAlloc.h

80.0 %

4 / 5

25.0 %

1 / 4

src/prop/bvminisat/simp/SimpSolver.cc

72.2 %

293 / 406

36.1 %

348 / 964

src/prop/bvminisat/simp/SimpSolver.h

89.5 %

17 / 19

44.1 %

15 / 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

76.5 %

65 / 85

27.5 %

39 / 142

src/prop/cnf_stream.cpp

93.7 %

386 / 412

38.0 %

756 / 1991

src/prop/cnf_stream.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/cryptominisat.cpp

66.7 %

72 / 108

26.2 %

53 / 202

src/prop/cryptominisat.h

0.0 %

0 / 1

100.0 %

0 / 0

src/prop/minisat/core/Solver.cc

83.3 %

855 / 1026

42.3 %

1177 / 2782

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

81.3 %

143 / 176

32.4 %

92 / 284

src/prop/minisat/minisat.h

60.0 %

3 / 5

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 %

410 / 1048

src/prop/minisat/simp/SimpSolver.h

86.2 %

25 / 29

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.7 %

580 / 619

45.1 %

1499 / 3326

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.6 %

51 / 152

src/prop/proof_post_processor.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/prop_engine.cpp

75.1 %

260 / 346

31.6 %

377 / 1194

src/prop/prop_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/prop_proof_manager.cpp

38.0 %

19 / 50

10.6 %

19 / 180

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

72.3 %

311 / 430

30.3 %

629 / 2076

src/prop/sat_proof_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/sat_solver.h

15.0 %

6 / 40

0.0 %

0 / 30

src/prop/sat_solver_factory.cpp

86.7 %

13 / 15

33.3 %

6 / 18

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/skolem_def_manager.cpp

98.8 %

82 / 83

43.9 %

108 / 246

src/prop/theory_proxy.cpp

94.2 %

97 / 103

42.3 %

131 / 310

src/smt/abduction_solver.cpp

83.7 %

82 / 98

38.9 %

161 / 414

src/smt/abstract_values.cpp

100.0 %

16 / 16

39.7 %

23 / 58

src/smt/assertions.cpp

86.0 %

80 / 93

46.7 %

98 / 210

src/smt/check_models.cpp

65.1 %

28 / 43

28.0 %

51 / 182

src/smt/command.cpp

54.3 %

670 / 1233

32.7 %

487 / 1491

src/smt/command.h

79.2 %

61 / 77

25.0 %

4 / 16

src/smt/dump.cpp

67.1 %

49 / 73

35.9 %

46 / 128

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

98.1 %

53 / 54

41.9 %

36 / 86

src/smt/env_obj.cpp

100.0 %

8 / 8

50.0 %

4 / 8

src/smt/env_obj.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/expand_definitions.cpp

98.6 %

69 / 70

47.0 %

126 / 268

src/smt/interpolation_solver.cpp

78.6 %

44 / 56

40.0 %

80 / 200

src/smt/listeners.cpp

83.7 %

36 / 43

34.7 %

41 / 118

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/model.cpp

81.6 %

31 / 38

29.0 %

18 / 62

src/smt/model.h

33.3 %

1 / 3

100.0 %

0 / 0

src/smt/model_blocker.cpp

84.7 %

122 / 144

36.5 %

279 / 764

src/smt/model_core_builder.cpp

78.8 %

41 / 52

35.3 %

65 / 184

src/smt/node_command.cpp

50.0 %

28 / 56

18.6 %

16 / 86

src/smt/node_command.h

100.0 %

5 / 5

100.0 %

0 / 0

src/smt/optimization_solver.cpp

64.6 %

122 / 189

36.6 %

144 / 393

src/smt/optimization_solver.h

100.0 %

20 / 20

50.0 %

5 / 10

src/smt/output_manager.cpp

40.0 %

2 / 5

50.0 %

2 / 4

src/smt/preprocess_proof_generator.cpp

93.3 %

111 / 119

44.4 %

245 / 552

src/smt/preprocess_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/preprocessor.cpp

95.2 %

60 / 63

41.5 %

54 / 130

src/smt/process_assertions.cpp

93.0 %

173 / 186

51.2 %

355 / 694

src/smt/proof_final_callback.cpp

93.0 %

40 / 43

44.9 %

44 / 98

src/smt/proof_final_callback.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/proof_manager.cpp

75.0 %

72 / 96

29.7 %

98 / 330

src/smt/proof_post_processor.cpp

91.8 %

529 / 576

38.7 %

1062 / 2744

src/smt/proof_post_processor.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/quant_elim_solver.cpp

91.5 %

54 / 59

42.5 %

130 / 306

src/smt/set_defaults.cpp

80.2 %

647 / 807

56.5 %

929 / 1644

src/smt/smt_engine.cpp

83.4 %

855 / 1025

38.4 %

1282 / 3337

src/smt/smt_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/smt_engine_scope.cpp

100.0 %

21 / 21

23.5 %

16 / 68

src/smt/smt_engine_state.cpp

90.5 %

124 / 137

37.1 %

93 / 251

src/smt/smt_engine_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/smt_engine_stats.cpp

100.0 %

17 / 17

50.0 %

12 / 24

src/smt/smt_mode.cpp

8.3 %

1 / 12

16.7 %

2 / 12

src/smt/smt_solver.cpp

88.8 %

87 / 98

48.6 %

139 / 286

src/smt/smt_statistics_registry.cpp

100.0 %

3 / 3

50.0 %

2 / 4

src/smt/smt_statistics_registry.h

100.0 %

1 / 1

50.0 %

2 / 4

src/smt/sygus_solver.cpp

89.4 %

202 / 226

45.4 %

369 / 812

src/smt/term_formula_removal.cpp

92.9 %

209 / 225

46.8 %

422 / 902

src/smt/unsat_core_manager.cpp

84.2 %

48 / 57

35.9 %

71 / 198

src/smt/unsat_core_manager.h

100.0 %

2 / 2

100.0 %

0 / 0

src/smt/witness_form.cpp

69.8 %

44 / 63

26.7 %

77 / 288

src/smt/witness_form.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt_util/boolean_simplification.cpp

55.6 %

15 / 27

38.0 %

38 / 100

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 / 313

src/theory/arith/approx_simplex.cpp

2.8 %

4 / 145

0.5 %

2 / 423

src/theory/arith/approx_simplex.h

0.0 %

0 / 3

100.0 %

0 / 0

src/theory/arith/arith_ite_utils.cpp

0.4 %

1 / 276

0.2 %

2 / 1330

src/theory/arith/arith_msum.cpp

90.3 %

130 / 144

51.1 %

327 / 640

src/theory/arith/arith_msum.h

100.0 %

2 / 2

55.0 %

11 / 20

src/theory/arith/arith_preprocess.cpp

25.0 %

7 / 28

5.3 %

4 / 76

src/theory/arith/arith_preprocess.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/arith_rewriter.cpp

88.7 %

461 / 520

42.2 %

1082 / 2567

src/theory/arith/arith_rewriter.h

100.0 %

3 / 3

50.0 %

1 / 2

src/theory/arith/arith_state.cpp

100.0 %

7 / 7

75.0 %

6 / 8

src/theory/arith/arith_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/arith_static_learner.cpp

87.2 %

136 / 156

41.5 %

376 / 905

src/theory/arith/arith_utilities.cpp

78.9 %

127 / 161

35.3 %

230 / 652

src/theory/arith/arith_utilities.h

66.7 %

74 / 111

37.4 %

52 / 139

src/theory/arith/arithvar.cpp

100.0 %

4 / 4

50.0 %

3 / 6

src/theory/arith/attempt_solution_simplex.cpp

15.6 %

12 / 77

3.5 %

10 / 286

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

64.7 %

88 / 136

37.7 %

171 / 453

src/theory/arith/bound_inference.h

100.0 %

2 / 2

50.0 %

15 / 30

src/theory/arith/branch_and_bound.cpp

95.4 %

62 / 65

44.7 %

204 / 456

src/theory/arith/branch_and_bound.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/callbacks.cpp

87.7 %

100 / 114

23.7 %

106 / 448

src/theory/arith/callbacks.h

100.0 %

13 / 13

100.0 %

0 / 0

src/theory/arith/congruence_manager.cpp

87.3 %

359 / 411

37.9 %

723 / 1910

src/theory/arith/congruence_manager.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/arith/constraint.cpp

72.8 %

1072 / 1473

28.1 %

1801 / 6403

src/theory/arith/constraint.h

95.0 %

114 / 120

17.4 %

41 / 236

src/theory/arith/cut_log.cpp

0.2 %

1 / 405

0.2 %

2 / 848

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

84.8 %

78 / 92

53.5 %

46 / 86

src/theory/arith/dio_solver.cpp

87.2 %

422 / 484

35.5 %

832 / 2344

src/theory/arith/dio_solver.h

76.9 %

30 / 39

16.1 %

18 / 112

src/theory/arith/dual_simplex.cpp

90.8 %

109 / 120

37.5 %

204 / 544

src/theory/arith/dual_simplex.h

100.0 %

8 / 8

100.0 %

0 / 0

src/theory/arith/equality_solver.cpp

69.6 %

39 / 56

33.3 %

46 / 138

src/theory/arith/equality_solver.h

100.0 %

6 / 6

100.0 %

0 / 0

src/theory/arith/error_set.cpp

64.0 %

197 / 308

26.7 %

167 / 625

src/theory/arith/error_set.h

51.1 %

47 / 92

8.7 %

12 / 138

src/theory/arith/fc_simplex.cpp

4.3 %

21 / 487

0.7 %

16 / 2142

src/theory/arith/fc_simplex.h

5.1 %

2 / 39

0.0 %

0 / 26

src/theory/arith/infer_bounds.cpp

23.9 %

33 / 138

3.3 %

7 / 215

src/theory/arith/infer_bounds.h

33.3 %

1 / 3

100.0 %

0 / 0

src/theory/arith/inference_manager.cpp

76.7 %

56 / 73

34.3 %

59 / 172

src/theory/arith/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/linear_equality.cpp

45.8 %

368 / 804

18.8 %

621 / 3298

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/cdcac.cpp

70.7 %

241 / 341

34.9 %

410 / 1176

src/theory/arith/nl/cad/cdcac.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arith/nl/cad/cdcac_utils.cpp

80.1 %

133 / 166

42.1 %

192 / 456

src/theory/arith/nl/cad/cdcac_utils.h

100.0 %

1 / 1

50.0 %

5 / 10

src/theory/arith/nl/cad/constraints.cpp

100.0 %

29 / 29

62.5 %

15 / 24

src/theory/arith/nl/cad/constraints.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arith/nl/cad/lazard_evaluation.cpp

35.3 %

6 / 17

6.7 %

2 / 30

src/theory/arith/nl/cad/projections.cpp

100.0 %

42 / 42

55.3 %

52 / 94

src/theory/arith/nl/cad/projections.h

33.3 %

2 / 6

0.0 %

0 / 4

src/theory/arith/nl/cad/proof_checker.cpp

93.8 %

15 / 16

33.9 %

21 / 62

src/theory/arith/nl/cad/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arith/nl/cad/proof_generator.cpp

83.3 %

70 / 84

37.3 %

103 / 276

src/theory/arith/nl/cad/proof_generator.h

100.0 %

5 / 5

50.0 %

1 / 2

src/theory/arith/nl/cad/variable_ordering.cpp

60.0 %

33 / 55

32.1 %

25 / 78

src/theory/arith/nl/cad_solver.cpp

58.6 %

51 / 87

26.2 %

86 / 328

src/theory/arith/nl/ext/constraint.cpp

96.4 %

53 / 55

48.9 %

87 / 178

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

50.0 %

86 / 172

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.6 %

224 / 410

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.3 %

251 / 520

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.6 %

352 / 1190

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.5 %

748 / 1482

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.6 %

219 / 716

src/theory/arith/nl/ext/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arith/nl/ext/split_zero_check.cpp

23.5 %

4 / 17

4.3 %

2 / 46

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

54.0 %

189 / 350

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

92.6 %

50 / 54

49.0 %

96 / 196

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.8 %

252 / 724

src/theory/arith/nl/iand_utils.cpp

93.7 %

104 / 111

40.5 %

166 / 410

src/theory/arith/nl/iand_utils.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/icp/candidate.cpp

70.4 %

38 / 54

37.6 %

67 / 178

src/theory/arith/nl/icp/candidate.h

100.0 %

1 / 1

50.0 %

3 / 6

src/theory/arith/nl/icp/contraction_origins.cpp

79.1 %

34 / 43

33.6 %

45 / 134

src/theory/arith/nl/icp/contraction_origins.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arith/nl/icp/icp_solver.cpp

84.0 %

168 / 200

43.7 %

267 / 611

src/theory/arith/nl/icp/icp_solver.h

100.0 %

11 / 11

50.0 %

2 / 4

src/theory/arith/nl/icp/intersection.cpp

42.3 %

44 / 104

23.2 %

86 / 370

src/theory/arith/nl/nl_lemma_utils.cpp

75.0 %

21 / 28

43.5 %

20 / 46

src/theory/arith/nl/nl_lemma_utils.h

94.7 %

18 / 19

37.5 %

3 / 8

src/theory/arith/nl/nl_model.cpp

80.1 %

597 / 745

39.2 %

1389 / 3539

src/theory/arith/nl/nl_model.h

100.0 %

1 / 1

41.2 %

14 / 34

src/theory/arith/nl/nonlinear_extension.cpp

89.7 %

296 / 330

50.7 %

493 / 973

src/theory/arith/nl/nonlinear_extension.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/poly_conversion.cpp

58.2 %

231 / 397

22.1 %

384 / 1736

src/theory/arith/nl/poly_conversion.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/pow2_solver.cpp

95.7 %

89 / 93

48.5 %

189 / 390

src/theory/arith/nl/stats.cpp

100.0 %

5 / 5

50.0 %

6 / 12

src/theory/arith/nl/strategy.cpp

61.1 %

66 / 108

38.3 %

77 / 201

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.9 %

248 / 540

src/theory/arith/nl/transcendental/proof_checker.cpp

82.1 %

215 / 262

26.4 %

602 / 2282

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 %

223 / 225

47.8 %

547 / 1144

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.3 %

238 / 550

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

42.0 %

345 / 821

src/theory/arith/nl/transcendental/transcendental_state.cpp

93.8 %

182 / 194

46.5 %

498 / 1072

src/theory/arith/nl/transcendental/transcendental_state.h

100.0 %

1 / 1

75.0 %

3 / 4

src/theory/arith/normal_form.cpp

81.0 %

644 / 795

37.0 %

1099 / 2972

src/theory/arith/normal_form.h

98.2 %

375 / 382

38.0 %

421 / 1107

src/theory/arith/operator_elim.cpp

93.3 %

182 / 195

49.5 %

487 / 984

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.7 %

294 / 872

src/theory/arith/partial_model.h

100.0 %

34 / 34

50.0 %

1 / 2

src/theory/arith/pp_rewrite_eq.cpp

100.0 %

21 / 21

42.1 %

53 / 126

src/theory/arith/pp_rewrite_eq.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/proof_checker.cpp

70.1 %

122 / 174

29.5 %

253 / 857

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.8 %

81 / 586

src/theory/arith/simplex.h

15.4 %

2 / 13

0.0 %

0 / 2

src/theory/arith/simplex_update.cpp

0.8 %

1 / 118

0.6 %

2 / 323

src/theory/arith/simplex_update.h

0.0 %

0 / 57

0.0 %

0 / 98

src/theory/arith/soi_simplex.cpp

4.2 %

23 / 543

0.8 %

20 / 2392

src/theory/arith/soi_simplex.h

11.8 %

2 / 17

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

85.4 %

152 / 178

37.6 %

194 / 516

src/theory/arith/theory_arith.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/arith/theory_arith_private.cpp

59.3 %

1759 / 2965

27.5 %

3438 / 12520

src/theory/arith/theory_arith_private.h

85.3 %

29 / 34

35.7 %

15 / 42

src/theory/arith/theory_arith_type_rules.cpp

76.1 %

54 / 71

32.4 %

73 / 225

src/theory/arith/type_enumerator.h

100.0 %

37 / 37

44.0 %

51 / 116

src/theory/arrays/array_info.cpp

68.8 %

203 / 295

31.3 %

292 / 932

src/theory/arrays/array_info.h

100.0 %

14 / 14

39.3 %

22 / 56

src/theory/arrays/inference_manager.cpp

83.1 %

49 / 59

38.6 %

78 / 202

src/theory/arrays/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arrays/proof_checker.cpp

73.3 %

44 / 60

25.5 %

108 / 424

src/theory/arrays/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arrays/skolem_cache.cpp

96.4 %

27 / 28

31.1 %

61 / 196

src/theory/arrays/theory_arrays.cpp

71.8 %

865 / 1205

36.3 %

2356 / 6489

src/theory/arrays/theory_arrays.h

97.6 %

41 / 42

55.3 %

63 / 114

src/theory/arrays/theory_arrays_rewriter.cpp

98.6 %

351 / 356

52.8 %

852 / 1613

src/theory/arrays/theory_arrays_rewriter.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/arrays/theory_arrays_type_rules.cpp

66.4 %

89 / 134

26.4 %

173 / 656

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 / 140

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.9 %

45 / 110

src/theory/atom_requests.h

100.0 %

13 / 13

75.0 %

3 / 4

src/theory/bags/bag_solver.cpp

92.8 %

103 / 111

39.5 %

159 / 403

src/theory/bags/bags_rewriter.cpp

89.0 %

218 / 245

44.5 %

845 / 1901

src/theory/bags/bags_rewriter.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/bags/bags_statistics.cpp

100.0 %

5 / 5

50.0 %

4 / 8

src/theory/bags/infer_info.cpp

43.8 %

14 / 32

16.7 %

20 / 120

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.4 %

301 / 930

src/theory/bags/inference_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/inference_manager.cpp

80.0 %

12 / 15

50.0 %

13 / 26

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

50.0 %

6 / 12

src/theory/bags/make_bag_op.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/normal_form.cpp

93.5 %

257 / 275

43.0 %

577 / 1341

src/theory/bags/rewrites.cpp

1.9 %

1 / 52

4.3 %

2 / 47

src/theory/bags/solver_state.cpp

100.0 %

67 / 67

48.8 %

123 / 252

src/theory/bags/solver_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/term_registry.cpp

41.7 %

5 / 12

15.4 %

4 / 26

src/theory/bags/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/theory_bags.cpp

90.0 %

108 / 120

40.7 %

161 / 396

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 / 104

src/theory/bags/theory_bags_type_rules.cpp

72.5 %

111 / 153

27.6 %

220 / 796

src/theory/booleans/circuit_propagator.cpp

93.0 %

348 / 374

49.0 %

875 / 1784

src/theory/booleans/circuit_propagator.h

100.0 %

29 / 29

52.0 %

52 / 100

src/theory/booleans/proof_checker.cpp

78.5 %

419 / 534

28.0 %

932 / 3330

src/theory/booleans/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/booleans/proof_circuit_propagator.cpp

91.6 %

230 / 251

49.7 %

547 / 1100

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

50.0 %

33 / 66

src/theory/booleans/theory_bool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/booleans/theory_bool_rewriter.cpp

96.5 %

223 / 231

55.4 %

884 / 1595

src/theory/booleans/theory_bool_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/booleans/theory_bool_type_rules.cpp

100.0 %

30 / 30

53.6 %

74 / 138

src/theory/booleans/type_enumerator.h

100.0 %

19 / 19

40.0 %

14 / 35

src/theory/builtin/proof_checker.cpp

77.7 %

171 / 220

31.6 %

303 / 958

src/theory/builtin/proof_checker.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/builtin/theory_builtin.cpp

83.3 %

10 / 12

44.4 %

8 / 18

src/theory/builtin/theory_builtin.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/builtin/theory_builtin_rewriter.cpp

90.0 %

225 / 250

42.6 %

655 / 1539

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 %

17 / 17

43.3 %

26 / 60

src/theory/builtin/theory_builtin_type_rules.h

73.6 %

64 / 87

37.4 %

152 / 406

src/theory/builtin/type_enumerator.cpp

6.7 %

1 / 15

3.7 %

2 / 54

src/theory/builtin/type_enumerator.h

88.9 %

24 / 27

41.7 %

35 / 84

src/theory/bv/abstraction.cpp

1.1 %

7 / 626

0.3 %

9 / 2734

src/theory/bv/abstraction.h

22.9 %

8 / 35

4.0 %

2 / 50

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

62.6 %

67 / 107

5.0 %

13 / 262

src/theory/bv/bitblast/eager_bitblaster.cpp

52.3 %

69 / 132

16.8 %

93 / 553

src/theory/bv/bitblast/eager_bitblaster.h

75.0 %

3 / 4

50.0 %

1 / 2

src/theory/bv/bitblast/lazy_bitblaster.cpp

0.3 %

1 / 304

0.2 %

2 / 1089

src/theory/bv/bitblast/lazy_bitblaster.h

0.0 %

0 / 7

100.0 %

0 / 0

src/theory/bv/bitblast/node_bitblaster.cpp

94.7 %

72 / 76

40.7 %

118 / 290

src/theory/bv/bitblast/node_bitblaster.h

50.0 %

1 / 2

0.0 %

0 / 4

src/theory/bv/bitblast/proof_bitblaster.cpp

100.0 %

76 / 76

57.6 %

151 / 262

src/theory/bv/bv_eager_solver.cpp

14.9 %

7 / 47

2.1 %

4 / 190

src/theory/bv/bv_inequality_graph.cpp

0.3 %

1 / 300

0.2 %

2 / 1245

src/theory/bv/bv_inequality_graph.h

0.0 %

0 / 41

0.0 %

0 / 82

src/theory/bv/bv_quick_check.cpp

0.5 %

1 / 189

0.6 %

2 / 342

src/theory/bv/bv_quick_check.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/bv/bv_solver.h

75.0 %

21 / 28

12.5 %

1 / 8

src/theory/bv/bv_solver_bitblast.cpp

95.2 %

157 / 165

48.3 %

293 / 606

src/theory/bv/bv_solver_bitblast.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/bv/bv_solver_bitblast_internal.cpp

97.5 %

79 / 81

56.4 %

150 / 266

src/theory/bv/bv_solver_bitblast_internal.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/bv/bv_solver_layered.cpp

10.0 %

32 / 320

2.7 %

35 / 1306

src/theory/bv/bv_solver_layered.h

0.0 %

0 / 21

0.0 %

0 / 42

src/theory/bv/bv_subtheory.h

0.0 %

0 / 30

0.0 %

0 / 35

src/theory/bv/bv_subtheory_algebraic.cpp

0.2 %

1 / 600

0.1 %

2 / 2403

src/theory/bv/bv_subtheory_algebraic.h

0.0 %

0 / 18

0.0 %

0 / 10

src/theory/bv/bv_subtheory_bitblast.cpp

0.7 %

1 / 142

0.4 %

2 / 452

src/theory/bv/bv_subtheory_bitblast.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/bv/bv_subtheory_core.cpp

0.5 %

1 / 198

0.3 %

2 / 727

src/theory/bv/bv_subtheory_core.h

0.0 %

0 / 6

100.0 %

0 / 0

src/theory/bv/bv_subtheory_inequality.cpp

0.7 %

1 / 139

0.3 %

2 / 638

src/theory/bv/bv_subtheory_inequality.h

0.0 %

0 / 6

0.0 %

0 / 10

src/theory/bv/int_blaster.cpp

59.3 %

220 / 371

24.6 %

403 / 1638

src/theory/bv/int_blaster.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bv/proof_checker.cpp

56.5 %

13 / 23

6.4 %

10 / 156

src/theory/bv/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

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

98.9 %

181 / 183

49.1 %

302 / 615

src/theory/bv/theory_bv.h

0.0 %

0 / 1

0.0 %

0 / 2

src/theory/bv/theory_bv_rewrite_rules.h

30.3 %

74 / 244

26.8 %

4708 / 17542

src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h

87.7 %

135 / 154

44.3 %

334 / 754

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

76.6 %

556 / 726

38.4 %

1121 / 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

82.9 %

619 / 747

42.2 %

1810 / 4290

src/theory/bv/theory_bv_rewriter.cpp

95.9 %

324 / 338

51.4 %

481 / 936

src/theory/bv/theory_bv_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bv/theory_bv_type_rules.cpp

73.5 %

100 / 136

30.5 %

149 / 488

src/theory/bv/theory_bv_type_rules.h

83.3 %

5 / 6

40.0 %

8 / 20

src/theory/bv/theory_bv_utils.cpp

64.3 %

153 / 238

28.1 %

228 / 810

src/theory/bv/theory_bv_utils.h

22.2 %

4 / 18

16.7 %

17 / 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 %

34 / 34

53.3 %

48 / 90

src/theory/combination_engine.cpp

95.6 %

43 / 45

33.7 %

35 / 104

src/theory/datatypes/datatypes_rewriter.cpp

93.8 %

482 / 514

46.0 %

1074 / 2333

src/theory/datatypes/datatypes_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/infer_proof_cons.cpp

77.1 %

111 / 144

33.3 %

298 / 895

src/theory/datatypes/infer_proof_cons.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/inference.cpp

75.0 %

18 / 24

36.5 %

38 / 104

src/theory/datatypes/inference.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/inference_manager.cpp

100.0 %

65 / 65

55.3 %

135 / 244

src/theory/datatypes/proof_checker.cpp

77.6 %

52 / 67

26.2 %

113 / 432

src/theory/datatypes/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/datatypes/sygus_datatype_utils.cpp

88.5 %

315 / 356

39.9 %

634 / 1590

src/theory/datatypes/sygus_extension.cpp

85.0 %

857 / 1008

40.2 %

1980 / 4930

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.7 %

560 / 1104

src/theory/datatypes/sygus_simple_sym.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/theory_datatypes.cpp

88.6 %

1009 / 1139

44.9 %

2305 / 5134

src/theory/datatypes/theory_datatypes.h

88.2 %

15 / 17

47.5 %

19 / 40

src/theory/datatypes/theory_datatypes_type_rules.cpp

77.9 %

218 / 280

32.8 %

447 / 1364

src/theory/datatypes/theory_datatypes_utils.cpp

84.3 %

86 / 102

38.4 %

186 / 485

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.7 %

389 / 798

src/theory/datatypes/type_enumerator.h

100.0 %

49 / 49

54.3 %

50 / 92

src/theory/decision_manager.cpp

100.0 %

47 / 47

53.7 %

72 / 134

src/theory/decision_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/decision_strategy.cpp

95.2 %

59 / 62

53.8 %

85 / 158

src/theory/decision_strategy.h

100.0 %

5 / 5

100.0 %

0 / 0

src/theory/ee_manager.cpp

92.3 %

12 / 13

55.6 %

10 / 18

src/theory/ee_manager.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/ee_manager_central.cpp

89.4 %

126 / 141

43.4 %

192 / 442

src/theory/ee_manager_central.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/ee_manager_distributed.cpp

97.7 %

43 / 44

36.8 %

42 / 114

src/theory/ee_setup_info.h

100.0 %

8 / 8

100.0 %

0 / 0

src/theory/engine_output_channel.cpp

74.4 %

67 / 90

32.5 %

74 / 228

src/theory/engine_output_channel.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/evaluator.cpp

78.1 %

386 / 494

38.9 %

689 / 1771

src/theory/evaluator.h

83.3 %

5 / 6

100.0 %

0 / 0

src/theory/ext_theory.cpp

64.8 %

162 / 250

38.8 %

276 / 711

src/theory/ext_theory.h

100.0 %

7 / 7

50.0 %

1 / 2

src/theory/fp/fp_converter.cpp

86.5 %

521 / 602

32.6 %

1386 / 4249

src/theory/fp/fp_converter.h

100.0 %

5 / 5

100.0 %

0 / 0

src/theory/fp/fp_expand_defs.cpp

62.0 %

80 / 129

24.2 %

152 / 628

src/theory/fp/fp_expand_defs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/fp/theory_fp.cpp

71.9 %

338 / 470

27.7 %

721 / 2602

src/theory/fp/theory_fp.h

85.7 %

6 / 7

0.0 %

0 / 2

src/theory/fp/theory_fp_rewriter.cpp

77.9 %

594 / 763

25.9 %

1032 / 3979

src/theory/fp/theory_fp_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/fp/theory_fp_type_rules.cpp

72.2 %

208 / 288

29.9 %

456 / 1524

src/theory/fp/type_enumerator.h

50.0 %

27 / 54

24.3 %

17 / 70

src/theory/incomplete_id.cpp

3.7 %

1 / 27

9.5 %

2 / 21

src/theory/inference_id.cpp

1.7 %

7 / 417

1.9 %

6 / 316

src/theory/inference_manager_buffered.cpp

93.1 %

81 / 87

36.2 %

55 / 152

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/logic_info.cpp

90.8 %

385 / 424

57.9 %

411 / 710

src/theory/logic_info.h

100.0 %

23 / 23

83.3 %

15 / 18

src/theory/model_manager.cpp

90.3 %

65 / 72

41.9 %

78 / 186

src/theory/model_manager_distributed.cpp

85.7 %

48 / 56

43.3 %

45 / 104

src/theory/output_channel.cpp

40.0 %

14 / 35

7.1 %

2 / 28

src/theory/output_channel.h

50.0 %

3 / 6

100.0 %

0 / 0

src/theory/quantifiers/alpha_equivalence.cpp

96.2 %

51 / 53

43.8 %

106 / 242

src/theory/quantifiers/alpha_equivalence.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/quantifiers/bv_inverter.cpp

93.0 %

187 / 201

45.0 %

473 / 1052

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 / 5350

src/theory/quantifiers/candidate_rewrite_database.cpp

77.7 %

101 / 130

33.3 %

159 / 478

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.8 %

255 / 596

src/theory/quantifiers/candidate_rewrite_filter.h

100.0 %

6 / 6

50.0 %

2 / 4

src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp

86.7 %

457 / 527

42.9 %

1181 / 2752

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.2 %

299 / 351

39.1 %

658 / 1684

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.9 %

445 / 1062

src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp

91.4 %

64 / 70

50.5 %

159 / 315

src/theory/quantifiers/cegqi/ceg_dt_instantiator.h

100.0 %

3 / 3

50.0 %

2 / 4

src/theory/quantifiers/cegqi/ceg_instantiator.cpp

91.6 %

816 / 891

49.7 %

1656 / 3332

src/theory/quantifiers/cegqi/ceg_instantiator.h

75.4 %

43 / 57

57.1 %

16 / 28

src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp

93.6 %

263 / 281

47.8 %

466 / 974

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.8 %

146 / 326

src/theory/quantifiers/cegqi/nested_qe.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/cegqi/vts_term_cache.cpp

93.8 %

137 / 146

51.9 %

306 / 590

src/theory/quantifiers/cegqi/vts_term_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/conjecture_generator.cpp

88.6 %

1248 / 1409

42.6 %

2548 / 5976

src/theory/quantifiers/conjecture_generator.h

86.0 %

43 / 50

61.1 %

22 / 36

src/theory/quantifiers/dynamic_rewrite.cpp

85.4 %

76 / 89

45.5 %

162 / 356

src/theory/quantifiers/dynamic_rewrite.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/ematching/candidate_generator.cpp

94.6 %

175 / 185

41.7 %

326 / 782

src/theory/quantifiers/ematching/candidate_generator.h

100.0 %

10 / 10

50.0 %

1 / 2

src/theory/quantifiers/ematching/ho_trigger.cpp

89.1 %

229 / 257

41.0 %

463 / 1128

src/theory/quantifiers/ematching/im_generator.cpp

100.0 %

6 / 6

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.2 %

293 / 344

42.9 %

589 / 1374

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 %

132 / 140

52.8 %

207 / 392

src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp

98.9 %

87 / 88

48.7 %

113 / 232

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

43.6 %

184 / 422

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

30.0 %

3 / 10

src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp

75.3 %

268 / 356

36.8 %

482 / 1309

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

65.8 %

52 / 79

37.7 %

90 / 239

src/theory/quantifiers/ematching/instantiation_engine.cpp

89.8 %

115 / 128

48.6 %

176 / 362

src/theory/quantifiers/ematching/instantiation_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/ematching/pattern_term_selector.cpp

93.1 %

335 / 360

49.9 %

766 / 1534

src/theory/quantifiers/ematching/trigger.cpp

85.2 %

98 / 115

38.5 %

171 / 444

src/theory/quantifiers/ematching/trigger_database.cpp

91.3 %

73 / 80

49.4 %

89 / 180

src/theory/quantifiers/ematching/trigger_term_info.cpp

100.0 %

42 / 42

76.5 %

101 / 132

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

62.5 %

25 / 40

src/theory/quantifiers/ematching/var_match_generator.cpp

84.4 %

27 / 32

48.0 %

47 / 98

src/theory/quantifiers/ematching/var_match_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/equality_query.cpp

76.4 %

68 / 89

39.0 %

163 / 418

src/theory/quantifiers/equality_query.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/expr_miner.cpp

85.3 %

29 / 34

37.5 %

36 / 96

src/theory/quantifiers/expr_miner.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/expr_miner_manager.cpp

57.1 %

44 / 77

34.9 %

44 / 126

src/theory/quantifiers/expr_miner_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/extended_rewrite.cpp

86.8 %

730 / 841

47.2 %

1789 / 3794

src/theory/quantifiers/extended_rewrite.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/first_order_model.cpp

89.4 %

161 / 180

46.1 %

246 / 534

src/theory/quantifiers/first_order_model.h

66.7 %

4 / 6

40.9 %

9 / 22

src/theory/quantifiers/fmf/bounded_integers.cpp

93.6 %

495 / 529

45.4 %

1229 / 2706

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 %

70 / 70

49.6 %

124 / 250

src/theory/quantifiers/fmf/full_model_check.cpp

95.1 %

763 / 802

51.3 %

1665 / 3243

src/theory/quantifiers/fmf/full_model_check.h

100.0 %

13 / 13

50.0 %

3 / 6

src/theory/quantifiers/fmf/model_builder.cpp

54.2 %

39 / 72

19.7 %

45 / 228

src/theory/quantifiers/fmf/model_builder.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/quantifiers/fmf/model_engine.cpp

70.3 %

137 / 195

34.4 %

233 / 677

src/theory/quantifiers/fmf/model_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/fun_def_evaluator.cpp

90.8 %

138 / 152

42.4 %

326 / 768

src/theory/quantifiers/fun_def_evaluator.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/ho_term_database.cpp

87.6 %

106 / 121

47.0 %

202 / 430

src/theory/quantifiers/ho_term_database.h

100.0 %

1 / 1

50.0 %

1 / 2

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

17.1 %

24 / 140

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.2 %

83 / 392

src/theory/quantifiers/inst_match_trie.h

100.0 %

10 / 10

50.0 %

1 / 2

src/theory/quantifiers/inst_strategy_enumerative.cpp

84.0 %

79 / 94

44.6 %

131 / 294

src/theory/quantifiers/inst_strategy_enumerative.h

100.0 %

3 / 3

50.0 %

1 / 2

src/theory/quantifiers/inst_strategy_pool.cpp

79.7 %

55 / 69

40.3 %

73 / 181

src/theory/quantifiers/inst_strategy_pool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/instantiate.cpp

79.9 %

274 / 343

38.2 %

528 / 1384

src/theory/quantifiers/instantiate.h

100.0 %

5 / 5

50.0 %

2 / 4

src/theory/quantifiers/instantiation_list.cpp

100.0 %

12 / 12

50.0 %

3 / 6

src/theory/quantifiers/instantiation_list.h

100.0 %

4 / 4

50.0 %

3 / 6

src/theory/quantifiers/lazy_trie.cpp

93.6 %

73 / 78

39.7 %

124 / 312

src/theory/quantifiers/lazy_trie.h

100.0 %

6 / 6

50.0 %

1 / 2

src/theory/quantifiers/master_eq_notify.cpp

100.0 %

5 / 5

50.0 %

3 / 6

src/theory/quantifiers/master_eq_notify.h

37.5 %

3 / 8

100.0 %

0 / 0

src/theory/quantifiers/proof_checker.cpp

68.3 %

43 / 63

22.4 %

69 / 308

src/theory/quantifiers/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/quant_bound_inference.cpp

100.0 %

52 / 52

57.0 %

81 / 142

src/theory/quantifiers/quant_bound_inference.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quant_conflict_find.cpp

83.0 %

1159 / 1397

45.5 %

2464 / 5417

src/theory/quantifiers/quant_conflict_find.h

100.0 %

18 / 18

52.8 %

19 / 36

src/theory/quantifiers/quant_module.cpp

100.0 %

23 / 23

50.0 %

7 / 14

src/theory/quantifiers/quant_module.h

81.8 %

9 / 11

100.0 %

0 / 0

src/theory/quantifiers/quant_relevance.cpp

95.0 %

19 / 20

61.8 %

21 / 34

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

44.6 %

25 / 56

src/theory/quantifiers/quant_rep_bound_ext.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quant_split.cpp

98.0 %

100 / 102

51.3 %

201 / 392

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.9 %

93 / 222

src/theory/quantifiers/quant_util.h

71.4 %

5 / 7

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_attributes.cpp

74.2 %

170 / 229

42.9 %

395 / 920

src/theory/quantifiers/quantifiers_attributes.h

100.0 %

7 / 7

50.0 %

4 / 8

src/theory/quantifiers/quantifiers_inference_manager.cpp

100.0 %

15 / 15

50.0 %

8 / 16

src/theory/quantifiers/quantifiers_macros.cpp

93.0 %

133 / 143

46.0 %

288 / 626

src/theory/quantifiers/quantifiers_macros.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_modules.cpp

100.0 %

44 / 44

69.1 %

65 / 94

src/theory/quantifiers/quantifiers_registry.cpp

90.5 %

86 / 95

45.4 %

98 / 216

src/theory/quantifiers/quantifiers_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_rewriter.cpp

77.1 %

915 / 1187

40.7 %

2059 / 5059

src/theory/quantifiers/quantifiers_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_state.cpp

50.6 %

41 / 81

23.6 %

52 / 220

src/theory/quantifiers/quantifiers_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_statistics.cpp

100.0 %

22 / 22

50.0 %

22 / 44

src/theory/quantifiers/query_generator.cpp

0.9 %

2 / 223

0.3 %

2 / 674

src/theory/quantifiers/query_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/relevant_domain.cpp

96.8 %

215 / 222

51.7 %

492 / 952

src/theory/quantifiers/relevant_domain.h

100.0 %

12 / 12

50.0 %

1 / 2

src/theory/quantifiers/single_inv_partition.cpp

88.8 %

270 / 304

49.3 %

509 / 1032

src/theory/quantifiers/single_inv_partition.h

100.0 %

7 / 7

83.3 %

5 / 6

src/theory/quantifiers/skolemize.cpp

89.2 %

182 / 204

41.8 %

410 / 980

src/theory/quantifiers/skolemize.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/solution_filter.cpp

63.8 %

30 / 47

28.4 %

46 / 162

src/theory/quantifiers/solution_filter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/ce_guided_single_inv.cpp

95.7 %

270 / 282

46.1 %

561 / 1218

src/theory/quantifiers/sygus/ce_guided_single_inv.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/sygus/cegis.cpp

94.7 %

323 / 341

47.7 %

613 / 1284

src/theory/quantifiers/sygus/cegis.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/cegis_core_connective.cpp

88.4 %

403 / 456

42.6 %

798 / 1873

src/theory/quantifiers/sygus/cegis_core_connective.h

100.0 %

6 / 6

50.0 %

3 / 6

src/theory/quantifiers/sygus/cegis_unif.cpp

86.9 %

304 / 350

36.8 %

510 / 1384

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.3 %

325 / 1110

src/theory/quantifiers/sygus/enum_stream_substitution.h

100.0 %

6 / 6

50.0 %

2 / 4

src/theory/quantifiers/sygus/enum_val_generator.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/sygus/enum_value_manager.cpp

83.5 %

91 / 109

40.7 %

179 / 440

src/theory/quantifiers/sygus/example_eval_cache.cpp

97.9 %

47 / 48

39.9 %

59 / 148

src/theory/quantifiers/sygus/example_infer.cpp

83.7 %

103 / 123

35.7 %

165 / 462

src/theory/quantifiers/sygus/example_min_eval.cpp

100.0 %

30 / 30

43.4 %

46 / 106

src/theory/quantifiers/sygus/example_min_eval.h

100.0 %

5 / 5

50.0 %

1 / 2

src/theory/quantifiers/sygus/rcons_obligation.cpp

30.4 %

17 / 56

7.3 %

11 / 150

src/theory/quantifiers/sygus/rcons_obligation.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/rcons_type_info.cpp

100.0 %

31 / 31

54.3 %

38 / 70

src/theory/quantifiers/sygus/rcons_type_info.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/sygus/sygus_abduct.cpp

98.8 %

85 / 86

49.3 %

221 / 448

src/theory/quantifiers/sygus/sygus_enumerator.cpp

97.2 %

627 / 645

43.8 %

991 / 2260

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

5.3 %

2 / 38

src/theory/quantifiers/sygus/sygus_enumerator_basic.h

0.0 %

0 / 4

0.0 %

0 / 2

src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp

100.0 %

42 / 42

50.0 %

72 / 144

src/theory/quantifiers/sygus/sygus_enumerator_callback.h

50.0 %

2 / 4

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_eval_unfold.cpp

97.3 %

180 / 185

42.2 %

389 / 922

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.2 %

292 / 786

src/theory/quantifiers/sygus/sygus_explain.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_grammar_cons.cpp

87.7 %

790 / 901

42.1 %

1457 / 3458

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.2 %

219 / 1086

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

45.0 %

171 / 380

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

40.2 %

271 / 674

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.3 %

203 / 530

src/theory/quantifiers/sygus/sygus_invariance.h

90.0 %

18 / 20

56.3 %

9 / 16

src/theory/quantifiers/sygus/sygus_module.cpp

100.0 %

5 / 5

50.0 %

2 / 4

src/theory/quantifiers/sygus/sygus_module.h

40.0 %

2 / 5

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_pbe.cpp

99.2 %

122 / 123

43.8 %

224 / 512

src/theory/quantifiers/sygus/sygus_process_conj.cpp

90.7 %

351 / 387

44.2 %

621 / 1406

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 %

82 / 83

47.6 %

178 / 374

src/theory/quantifiers/sygus/sygus_qe_preproc.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_reconstruct.cpp

89.8 %

184 / 205

49.7 %

394 / 792

src/theory/quantifiers/sygus/sygus_reconstruct.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_repair_const.cpp

90.4 %

300 / 332

41.2 %

588 / 1426

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 %

13 / 13

50.0 %

14 / 28

src/theory/quantifiers/sygus/sygus_unif.cpp

90.9 %

50 / 55

35.5 %

49 / 138

src/theory/quantifiers/sygus/sygus_unif_io.cpp

90.8 %

747 / 823

40.8 %

1343 / 3290

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.5 %

437 / 638

29.8 %

735 / 2466

src/theory/quantifiers/sygus/sygus_unif_rl.h

100.0 %

7 / 7

50.0 %

6 / 12

src/theory/quantifiers/sygus/sygus_unif_strat.cpp

83.9 %

479 / 571

43.2 %

933 / 2162

src/theory/quantifiers/sygus/sygus_unif_strat.h

100.0 %

18 / 18

50.0 %

3 / 6

src/theory/quantifiers/sygus/sygus_utils.cpp

74.4 %

58 / 78

30.2 %

110 / 364

src/theory/quantifiers/sygus/synth_conjecture.cpp

89.0 %

524 / 589

41.0 %

1047 / 2556

src/theory/quantifiers/sygus/synth_conjecture.h

100.0 %

7 / 7

100.0 %

0 / 0

src/theory/quantifiers/sygus/synth_engine.cpp

95.2 %

120 / 126

55.3 %

197 / 356

src/theory/quantifiers/sygus/synth_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/sygus/synth_verify.cpp

91.8 %

45 / 49

44.2 %

84 / 190

src/theory/quantifiers/sygus/template_infer.cpp

97.9 %

94 / 96

44.8 %

234 / 522

src/theory/quantifiers/sygus/template_infer.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/sygus/term_database_sygus.cpp

86.4 %

469 / 543

42.5 %

847 / 1991

src/theory/quantifiers/sygus/term_database_sygus.h

100.0 %

7 / 7

62.5 %

5 / 8

src/theory/quantifiers/sygus/transition_inference.cpp

94.0 %

280 / 298

46.7 %

521 / 1116

src/theory/quantifiers/sygus/transition_inference.h

100.0 %

12 / 12

50.0 %

4 / 8

src/theory/quantifiers/sygus/type_info.cpp

82.6 %

204 / 247

39.7 %

339 / 854

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

75.0 %

12 / 16

src/theory/quantifiers/sygus/type_node_id_trie.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus_inst.cpp

82.6 %

214 / 259

37.2 %

374 / 1006

src/theory/quantifiers/sygus_inst.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/sygus_sampler.cpp

79.7 %

369 / 463

38.6 %

588 / 1522

src/theory/quantifiers/sygus_sampler.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/term_database.cpp

80.6 %

460 / 571

41.9 %

1023 / 2440

src/theory/quantifiers/term_database.h

100.0 %

3 / 3

50.0 %

2 / 4

src/theory/quantifiers/term_enumeration.cpp

55.2 %

16 / 29

32.1 %

27 / 84

src/theory/quantifiers/term_enumeration.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/term_pools.cpp

97.3 %

72 / 74

41.2 %

93 / 226

src/theory/quantifiers/term_pools.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/term_registry.cpp

89.8 %

53 / 59

48.0 %

73 / 152

src/theory/quantifiers/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/term_tuple_enumerator.cpp

75.6 %

155 / 205

37.8 %

236 / 624

src/theory/quantifiers/term_tuple_enumerator.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/term_util.cpp

83.8 %

259 / 309

54.9 %

560 / 1020

src/theory/quantifiers/theory_quantifiers.cpp

94.5 %

69 / 73

52.4 %

89 / 170

src/theory/quantifiers/theory_quantifiers.h

33.3 %

1 / 3

0.0 %

0 / 2

src/theory/quantifiers/theory_quantifiers_type_rules.cpp

83.3 %

40 / 48

36.6 %

96 / 262

src/theory/quantifiers_engine.cpp

84.3 %

295 / 350

42.8 %

527 / 1232

src/theory/relevance_manager.cpp

77.7 %

115 / 148

32.0 %

162 / 506

src/theory/relevance_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/rep_set.cpp

74.4 %

189 / 254

35.5 %

290 / 818

src/theory/rep_set.h

64.3 %

9 / 14

100.0 %

0 / 0

src/theory/rewriter.cpp

87.6 %

162 / 185

41.4 %

304 / 734

src/theory/rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/rewriter_attributes.h

100.0 %

30 / 30

43.9 %

616 / 1404

src/theory/sep/theory_sep.cpp

84.8 %

923 / 1089

41.8 %

2283 / 5462

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

45.1 %

180 / 399

src/theory/sep/theory_sep_rewriter.h

100.0 %

4 / 4

50.0 %

6 / 12

src/theory/sep/theory_sep_type_rules.cpp

90.9 %

40 / 44

23.5 %

46 / 196

src/theory/sets/cardinality_extension.cpp

91.0 %

525 / 577

47.4 %

1229 / 2593

src/theory/sets/cardinality_extension.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/sets/inference_manager.cpp

52.2 %

47 / 90

25.8 %

102 / 396

src/theory/sets/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

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

50.0 %

6 / 12

src/theory/sets/singleton_op.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/sets/skolem_cache.cpp

80.8 %

21 / 26

42.5 %

51 / 120

src/theory/sets/skolem_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/sets/solver_state.cpp

94.2 %

275 / 292

47.6 %

579 / 1216

src/theory/sets/solver_state.h

100.0 %

2 / 2

75.0 %

3 / 4

src/theory/sets/term_registry.cpp

80.7 %

67 / 83

45.8 %

131 / 286

src/theory/sets/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/sets/theory_sets.cpp

91.7 %

100 / 109

44.5 %

137 / 308

src/theory/sets/theory_sets.h

80.0 %

4 / 5

0.0 %

0 / 2

src/theory/sets/theory_sets_private.cpp

94.0 %

671 / 714

47.0 %

1470 / 3125

src/theory/sets/theory_sets_private.h

66.7 %

2 / 3

0.0 %

0 / 2

src/theory/sets/theory_sets_rels.cpp

94.6 %

740 / 782

51.4 %

1668 / 3245

src/theory/sets/theory_sets_rels.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/sets/theory_sets_rewriter.cpp

95.3 %

328 / 344

49.3 %

928 / 1883

src/theory/sets/theory_sets_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/sets/theory_sets_type_enumerator.cpp

100.0 %

61 / 61

46.7 %

86 / 184

src/theory/sets/theory_sets_type_rules.cpp

78.5 %

161 / 205

26.1 %

280 / 1072

src/theory/shared_solver.cpp

92.5 %

49 / 53

57.6 %

68 / 118

src/theory/shared_solver.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/shared_solver_distributed.cpp

100.0 %

35 / 35

56.0 %

56 / 100

src/theory/shared_solver_distributed.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/shared_terms_database.cpp

85.4 %

135 / 158

32.2 %

224 / 696

src/theory/shared_terms_database.h

100.0 %

25 / 25

31.3 %

10 / 32

src/theory/skolem_lemma.cpp

100.0 %

14 / 14

33.8 %

25 / 74

src/theory/skolem_lemma.h

100.0 %

1 / 1

50.0 %

2 / 4

src/theory/smt_engine_subsolver.cpp

82.0 %

41 / 50

34.6 %

45 / 130

src/theory/sort_inference.cpp

84.5 %

447 / 529

45.8 %

1005 / 2194

src/theory/sort_inference.h

83.3 %

5 / 6

100.0 %

0 / 0

src/theory/strings/arith_entail.cpp

89.6 %

344 / 384

46.0 %

879 / 1912

src/theory/strings/base_solver.cpp

78.4 %

294 / 375

39.1 %

618 / 1581

src/theory/strings/base_solver.h

100.0 %

2 / 2

50.0 %

2 / 4

src/theory/strings/core_solver.cpp

81.5 %

1117 / 1371

40.6 %

2562 / 6307

src/theory/strings/core_solver.h

100.0 %

2 / 2

40.9 %

9 / 22

src/theory/strings/eager_solver.cpp

98.5 %

65 / 66

54.0 %

122 / 226

src/theory/strings/eqc_info.cpp

100.0 %

57 / 57

44.8 %

148 / 330

src/theory/strings/eqc_info.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/extf_solver.cpp

84.1 %

301 / 358

44.4 %

779 / 1754

src/theory/strings/extf_solver.h

100.0 %

4 / 4

50.0 %

1 / 2

src/theory/strings/infer_info.cpp

69.7 %

23 / 33

35.8 %

38 / 106

src/theory/strings/infer_info.h

100.0 %

2 / 2

50.0 %

4 / 8

src/theory/strings/infer_proof_cons.cpp

84.7 %

524 / 619

41.1 %

1040 / 2528

src/theory/strings/infer_proof_cons.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/inference_manager.cpp

86.7 %

156 / 180

44.4 %

343 / 772

src/theory/strings/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/normal_form.cpp

100.0 %

84 / 84

44.3 %

149 / 336

src/theory/strings/normal_form.h

100.0 %

2 / 2

50.0 %

3 / 6

src/theory/strings/proof_checker.cpp

83.7 %

247 / 295

35.2 %

643 / 1826

src/theory/strings/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/strings/regexp_elim.cpp

93.0 %

278 / 299

45.2 %

620 / 1372

src/theory/strings/regexp_elim.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/regexp_entail.cpp

88.2 %

350 / 397

48.7 %

727 / 1493

src/theory/strings/regexp_operation.cpp

71.4 %

698 / 977

36.2 %

1485 / 4104

src/theory/strings/regexp_solver.cpp

89.4 %

296 / 331

48.5 %

587 / 1211

src/theory/strings/regexp_solver.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/rewrites.cpp

0.5 %

1 / 200

1.0 %

2 / 196

src/theory/strings/sequences_rewriter.cpp

96.7 %

1600 / 1654

52.2 %

5061 / 9696

src/theory/strings/sequences_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/sequences_stats.cpp

100.0 %

21 / 21

50.0 %

22 / 44

src/theory/strings/skolem_cache.cpp

91.4 %

127 / 139

48.9 %

288 / 589

src/theory/strings/skolem_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/solver_state.cpp

96.2 %

101 / 105

47.1 %

161 / 342

src/theory/strings/strategy.cpp

70.7 %

58 / 82

34.1 %

71 / 208

src/theory/strings/strings_entail.cpp

94.8 %

420 / 443

46.5 %

942 / 2027

src/theory/strings/strings_fmf.cpp

93.0 %

40 / 43

54.5 %

48 / 88

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.3 %

422 / 874

src/theory/strings/strings_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/term_registry.cpp

92.0 %

286 / 311

48.4 %

687 / 1420

src/theory/strings/theory_strings.cpp

82.1 %

482 / 587

41.7 %

1021 / 2451

src/theory/strings/theory_strings.h

100.0 %

32 / 32

52.3 %

69 / 132

src/theory/strings/theory_strings_preprocess.cpp

100.0 %

518 / 518

51.1 %

1566 / 3062

src/theory/strings/theory_strings_type_rules.cpp

70.8 %

97 / 137

26.4 %

122 / 462

src/theory/strings/theory_strings_utils.cpp

92.2 %

188 / 204

47.8 %

351 / 734

src/theory/strings/type_enumerator.cpp

85.4 %

117 / 137

33.3 %

78 / 234

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 / 1026

src/theory/subs_minimize.cpp

48.9 %

109 / 223

25.5 %

212 / 830

src/theory/substitutions.cpp

85.3 %

93 / 109

41.1 %

218 / 530

src/theory/substitutions.h

73.3 %

11 / 15

12.5 %

2 / 16

src/theory/term_registration_visitor.cpp

80.1 %

109 / 136

41.3 %

232 / 562

src/theory/term_registration_visitor.h

100.0 %

9 / 9

50.0 %

1 / 2

src/theory/theory.cpp

84.9 %

265 / 312

49.6 %

537 / 1083

src/theory/theory.h

76.5 %

65 / 85

44.3 %

70 / 158

src/theory/theory_engine.cpp

80.6 %

719 / 892

40.7 %

1802 / 4428

src/theory/theory_engine.h

100.0 %

42 / 42

27.5 %

100 / 364

src/theory/theory_engine_proof_generator.cpp

80.0 %

48 / 60

35.5 %

93 / 262

src/theory/theory_engine_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/theory_eq_notify.h

100.0 %

19 / 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

28.6 %

8 / 28

src/theory/theory_inference.h

72.7 %

8 / 11

50.0 %

1 / 2

src/theory/theory_inference_manager.cpp

91.1 %

224 / 246

42.4 %

358 / 844

src/theory/theory_model.cpp

89.3 %

382 / 428

43.1 %

796 / 1849

src/theory/theory_model.h

100.0 %

4 / 4

50.0 %

1 / 2

src/theory/theory_model_builder.cpp

93.5 %

628 / 672

42.5 %

1215 / 2859

src/theory/theory_model_builder.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/theory_preprocessor.cpp

93.1 %

201 / 216

45.4 %

476 / 1048

src/theory/theory_rewriter.cpp

90.0 %

18 / 20

47.9 %

23 / 48

src/theory/theory_rewriter.h

83.3 %

5 / 6

100.0 %

0 / 0

src/theory/theory_state.cpp

97.3 %

71 / 73

41.7 %

80 / 192

src/theory/theory_state.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/trust_substitutions.cpp

99.2 %

119 / 120

47.0 %

253 / 538

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

58.8 %

60 / 102

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 %

1673 / 4096

src/theory/uf/cardinality_extension.h

96.4 %

53 / 55

36.5 %

38 / 104

src/theory/uf/eq_proof.cpp

81.4 %

587 / 721

37.3 %

1401 / 3758

src/theory/uf/eq_proof.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/uf/equality_engine.cpp

91.8 %

1265 / 1378

43.6 %

2431 / 5570

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.9 %

38 / 182

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

82.9 %

204 / 246

41.1 %

423 / 1030

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.1 %

175 / 562

src/theory/uf/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/uf/proof_equality_engine.cpp

78.3 %

206 / 263

35.5 %

472 / 1328

src/theory/uf/proof_equality_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/uf/symmetry_breaker.cpp

82.7 %

401 / 485

43.1 %

951 / 2206

src/theory/uf/symmetry_breaker.h

100.0 %

7 / 7

50.0 %

4 / 8

src/theory/uf/theory_uf.cpp

87.1 %

298 / 342

47.5 %

642 / 1351

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.3 %

142 / 440

src/theory/uf/theory_uf_model.h

100.0 %

16 / 16

53.3 %

16 / 30

src/theory/uf/theory_uf_rewriter.cpp

84.0 %

79 / 94

43.8 %

205 / 468

src/theory/uf/theory_uf_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/uf/theory_uf_type_rules.cpp

68.0 %

51 / 75

27.7 %

88 / 318

src/theory/valuation.cpp

67.2 %

78 / 116

16.2 %

58 / 359

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

94.6 %

70 / 74

70.7 %

29 / 41

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/cardinality_class.cpp

39.1 %

9 / 23

52.0 %

13 / 25

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

74.2 %

164 / 221

32.0 %

167 / 522

src/util/floatingpoint.h

95.4 %

62 / 65

50.0 %

9 / 18

src/util/floatingpoint_literal_symfpu.cpp

84.2 %

101 / 120

20.3 %

61 / 300

src/util/floatingpoint_literal_symfpu.h

100.0 %

9 / 9

50.0 %

2 / 4

src/util/floatingpoint_literal_symfpu_traits.cpp

92.6 %

113 / 122

25.0 %

67 / 268

src/util/floatingpoint_literal_symfpu_traits.h

100.0 %

6 / 6

50.0 %

2 / 4

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 %

2 / 4

src/util/iand.h

50.0 %

2 / 4

100.0 %

0 / 0

src/util/indexed_root_predicate.h

71.4 %

5 / 7

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 %

19 / 19

83.3 %

5 / 6

src/util/ostream_util.cpp

0.0 %

0 / 7

100.0 %

0 / 0

src/util/poly_util.cpp

62.6 %

102 / 163

31.9 %

115 / 360

src/util/poly_util.h

100.0 %

1 / 1

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

33.3 %

38 / 114

src/util/rational_cln_imp.h

90.4 %

94 / 104

43.1 %

44 / 102

src/util/real_algebraic_number_poly_imp.cpp

60.0 %

45 / 75

29.6 %

45 / 152

src/util/real_algebraic_number_poly_imp.h

80.0 %

4 / 5

100.0 %

0 / 0

src/util/regexp.cpp

76.5 %

13 / 17

50.0 %

2 / 4

src/util/resource_manager.cpp

52.8 %

75 / 142

20.0 %

40 / 200

src/util/resource_manager.h

100.0 %

2 / 2

50.0 %

2 / 4

src/util/result.cpp

62.2 %

122 / 196

34.6 %

79 / 228

src/util/result.h

100.0 %

14 / 14

75.0 %

9 / 12

src/util/roundingmode.cpp

5.6 %

1 / 18

14.3 %

2 / 14

src/util/roundingmode.h

100.0 %

1 / 1

100.0 %

0 / 0

src/util/safe_print.cpp

0.0 %

0 / 102

0.0 %

0 / 84

src/util/safe_print.h

0.0 %

0 / 15

0.0 %

0 / 32

src/util/sampler.cpp

9.5 %

7 / 74

5.9 %

12 / 203

src/util/sexpr.cpp

64.7 %

11 / 17

40.9 %

9 / 22

src/util/sexpr.h

79.3 %

23 / 29

22.2 %

12 / 54

src/util/smt2_quote_string.cpp

100.0 %

8 / 8

77.3 %

17 / 22

src/util/statistics_public.cpp

100.0 %

13 / 13

52.4 %

22 / 42

src/util/statistics_registry.cpp

24.6 %

15 / 61

3.9 %

7 / 178

src/util/statistics_registry.h

96.9 %

31 / 32

28.6 %

54 / 189

src/util/statistics_stats.cpp

100.0 %

45 / 45

34.0 %

17 / 50

src/util/statistics_stats.h

100.0 %

31 / 31

100.0 %

0 / 0

src/util/statistics_value.cpp

73.7 %

28 / 38

41.7 %

15 / 36

src/util/statistics_value.h

45.5 %

40 / 88

28.7 %

37 / 129

src/util/string.cpp

95.8 %

254 / 265

58.2 %

283 / 486

src/util/string.h

95.8 %

23 / 24

50.0 %

4 / 8

src/util/utility.cpp

0.0 %

0 / 16

0.0 %

0 / 26

src/util/utility.h

65.2 %

15 / 23

27.7 %

18 / 65

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/issue6111.cpp

100.0 %

28 / 28

50.0 %

36 / 72

test/api/ouroborous.cpp

91.0 %

71 / 78

50.6 %

130 / 257

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 %

32 / 32

50.0 %

47 / 94

test/api/two_solvers.cpp

100.0 %

7 / 7

50.0 %

12 / 24

test/unit/api/datatype_api_black.cpp

100.0 %

402 / 402

33.5 %

1085 / 3240

test/unit/api/grammar_black.cpp

100.0 %

62 / 62

35.7 %

250 / 700

test/unit/api/op_black.cpp

100.0 %

169 / 169

30.8 %

432 / 1402

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

100.0 %

1719 / 1719

36.1 %

6580 / 18232

test/unit/api/solver_white.cpp

100.0 %

21 / 21

41.0 %

55 / 134

test/unit/api/sort_black.cpp

100.0 %

378 / 378

33.1 %

1203 / 3630

test/unit/api/term_black.cpp

100.0 %

884 / 884

31.5 %

3578 / 11356

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 %

94 / 94

30.8 %

146 / 474

test/unit/context/cdo_black.cpp

100.0 %

13 / 13

26.7 %

23 / 86

test/unit/context/context_black.cpp

97.5 %

115 / 118

24.4 %

221 / 905

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 %

56 / 56

44.2 %

46 / 104

test/unit/memory.h

100.0 %

12 / 12

21.4 %

6 / 28

test/unit/node/attribute_black.cpp

100.0 %

47 / 47

32.2 %

94 / 292

test/unit/node/attribute_white.cpp

100.0 %

314 / 314

28.5 %

1006 / 3524

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 %

310 / 884

test/unit/node/node_black.cpp

99.8 %

470 / 471

33.8 %

1568 / 4637

test/unit/node/node_builder_black.cpp

100.0 %

222 / 222

29.2 %

909 / 3115

test/unit/node/node_manager_black.cpp

100.0 %

197 / 197

30.5 %

594 / 1950

test/unit/node/node_manager_white.cpp

100.0 %

32 / 32

30.0 %

125 / 416

test/unit/node/node_self_iterator_black.cpp

100.0 %

22 / 22

29.9 %

83 / 278

test/unit/node/node_traversal_black.cpp

100.0 %

170 / 170

39.0 %

477 / 1222

test/unit/node/node_white.cpp

100.0 %

35 / 35

31.3 %

107 / 342

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 %

531 / 1496

test/unit/node/type_node_white.cpp

100.0 %

49 / 49

29.9 %

179 / 598

test/unit/parser/parser_black.cpp

100.0 %

198 / 198

43.7 %

351 / 804

test/unit/parser/parser_builder_black.cpp

100.0 %

70 / 70

42.5 %

90 / 212

test/unit/preprocessing/pass_bv_gauss_white.cpp

97.3 %

1281 / 1316

42.6 %

4785 / 11225

test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp

100.0 %

16 / 16

42.0 %

42 / 100

test/unit/printer/smt2_printer_black.cpp

100.0 %

18 / 18

45.2 %

38 / 84

test/unit/prop/cnf_stream_white.cpp

90.7 %

117 / 129

39.8 %

204 / 512

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 %

10 / 10

50.0 %

6 / 12

test/unit/test_smt.h

57.4 %

39 / 68

19.5 %

29 / 149

test/unit/theory/evaluator_white.cpp

100.0 %

68 / 68

43.5 %

215 / 494

test/unit/theory/logic_info_white.cpp

100.0 %

1230 / 1230

32.6 %

4138 / 12708

test/unit/theory/regexp_operation_black.cpp

100.0 %

72 / 72

48.3 %

233 / 482

test/unit/theory/sequences_rewriter_white.cpp

100.0 %

760 / 760

46.7 %

2466 / 5284

test/unit/theory/strings_rewriter_white.cpp

100.0 %

15 / 15

42.6 %

46 / 108

test/unit/theory/theory_arith_cad_white.cpp

92.6 %

213 / 230

41.8 %

626 / 1496

test/unit/theory/theory_arith_pow2_white.cpp

100.0 %

1 / 1

50.0 %

2 / 4

test/unit/theory/theory_arith_white.cpp

100.0 %

52 / 52

38.5 %

154 / 400

test/unit/theory/theory_bags_normal_form_white.cpp

100.0 %

283 / 283

42.1 %

1078 / 2562

test/unit/theory/theory_bags_rewriter_white.cpp

100.0 %

457 / 457

41.6 %

1427 / 3434

test/unit/theory/theory_bags_type_rules_white.cpp

100.0 %

79 / 79

38.9 %

218 / 560

test/unit/theory/theory_black.cpp

100.0 %

85 / 85

35.2 %

322 / 916

test/unit/theory/theory_bv_int_blaster_white.cpp

100.0 %

126 / 126

39.9 %

464 / 1162

test/unit/theory/theory_bv_opt_white.cpp

100.0 %

73 / 73

40.6 %

172 / 424

test/unit/theory/theory_bv_rewriter_white.cpp

100.0 %

39 / 39

45.1 %

111 / 246

test/unit/theory/theory_bv_white.cpp

100.0 %

38 / 38

46.9 %

107 / 228

test/unit/theory/theory_engine_white.cpp

98.7 %

78 / 79

45.8 %

197 / 430

test/unit/theory/theory_int_opt_white.cpp

100.0 %

65 / 65

41.8 %

143 / 342

test/unit/theory/theory_opt_multigoal_white.cpp

100.0 %

143 / 143

39.3 %

356 / 906

test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp

100.0 %

285 / 285

33.1 %

1397 / 4226

test/unit/theory/theory_quantifiers_bv_inverter_white.cpp

98.3 %

927 / 943

44.4 %

636 / 1432

test/unit/theory/theory_sets_type_enumerator_white.cpp

100.0 %

80 / 80

34.4 %

258 / 750

test/unit/theory/theory_sets_type_rules_white.cpp

100.0 %

32 / 32

32.9 %

103 / 313

test/unit/theory/theory_strings_skolem_cache_black.cpp

100.0 %

15 / 15

46.7 %

57 / 122

test/unit/theory/theory_strings_utils_white.cpp

100.0 %

22 / 22

37.7 %

49 / 130

test/unit/theory/theory_strings_word_white.cpp

100.0 %

73 / 73

30.7 %

350 / 1140

test/unit/theory/theory_white.cpp

100.0 %

40 / 40

28.9 %

66 / 228

test/unit/theory/type_enumerator_white.cpp

100.0 %

201 / 201

33.9 %

961 / 2836

test/unit/util/array_store_all_white.cpp

100.0 %

31 / 31

40.8 %

107 / 262

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 %

128 / 128

28.3 %

506 / 1788

test/unit/util/boolean_simplification_black.cpp

100.0 %

131 / 131

47.4 %

501 / 1058

test/unit/util/cardinality_black.cpp

100.0 %

207 / 207

27.6 %

932 / 3374

test/unit/util/check_white.cpp

100.0 %

16 / 16

19.5 %

34 / 174

test/unit/util/configuration_black.cpp

100.0 %

26 / 26

25.9 %

30 / 116

test/unit/util/datatype_black.cpp

100.0 %

353 / 353

35.4 %

1099 / 3104

test/unit/util/exception_black.cpp

100.0 %

19 / 19

34.6 %

54 / 156

test/unit/util/floatingpoint_black.cpp

100.0 %

86 / 86

31.1 %

210 / 676

test/unit/util/integer_black.cpp

100.0 %

371 / 371

30.6 %

1164 / 3806

test/unit/util/integer_white.cpp

100.0 %

16 / 16

31.0 %

39 / 126

test/unit/util/output_black.cpp

100.0 %

76 / 76

37.0 %

182 / 492

test/unit/util/rational_black.cpp

100.0 %

16 / 16

30.7 %

83 / 270

test/unit/util/rational_white.cpp

100.0 %

288 / 288

30.5 %

770 / 2528

test/unit/util/real_algebraic_number_black.cpp

100.0 %

40 / 40

30.4 %

136 / 448

test/unit/util/stats_black.cpp

100.0 %

43 / 43

36.8 %

112 / 304


Generated by: GCOVR (Version 3.2)