Head

GCC Code Coverage Report

Directory:	.			Exec	Total	Coverage
Date:	2021-11-07		Lines:	140877	177446	79.4 %
Legend:	low: < 75.0 % medium: >= 75.0 % high: >= 90.0 %		Branches:	278815	756667	36.8 %

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

223 / 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/base/Debug_tags.h

100.0 %

2 / 2

50.0 %

381 / 762

build-coverage/src/base/Trace_tags.h

100.0 %

2 / 2

50.0 %

1078 / 2156

build-coverage/src/expr/kind.cpp

56.1 %

398 / 709

55.3 %

386 / 698

build-coverage/src/expr/kind.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/src/expr/metakind.cpp

78.1 %

616 / 789

46.9 %

390 / 832

build-coverage/src/expr/metakind.h

100.0 %

12 / 12

11.4 %

534 / 4700

build-coverage/src/expr/type_checker.cpp

90.5 %

858 / 948

52.0 %

1162 / 2235

build-coverage/src/expr/type_properties.h

33.0 %

35 / 106

16.5 %

42 / 254

build-coverage/src/main/options.cpp

26.9 %

432 / 1603

14.9 %

801 / 5372

build-coverage/src/options/arith_options.cpp

8.2 %

9 / 110

5.6 %

10 / 178

build-coverage/src/options/arith_options.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/src/options/arrays_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/arrays_options.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/src/options/base_options.cpp

63.6 %

14 / 22

48.6 %

18 / 37

build-coverage/src/options/base_options.h

100.0 %

5 / 5

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

30.5 %

18 / 59

23.7 %

23 / 97

build-coverage/src/options/bv_options.h

100.0 %

3 / 3

100.0 %

0 / 0

build-coverage/src/options/datatypes_options.cpp

35.0 %

7 / 20

20.6 %

7 / 34

build-coverage/src/options/datatypes_options.h

100.0 %

14 / 14

100.0 %

0 / 0

build-coverage/src/options/decision_options.cpp

9.5 %

6 / 63

7.8 %

8 / 103

build-coverage/src/options/decision_options.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/src/options/expr_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/expr_options.h

100.0 %

3 / 3

100.0 %

0 / 0

build-coverage/src/options/fp_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/fp_options.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/src/options/main_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

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

77.7 %

1804 / 2323

28.9 %

2245 / 7762

build-coverage/src/options/parser_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/parser_options.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/src/options/printer_options.cpp

28.6 %

4 / 14

16.0 %

4 / 25

build-coverage/src/options/printer_options.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/src/options/proof_options.cpp

14.8 %

8 / 54

8.0 %

7 / 88

build-coverage/src/options/proof_options.h

100.0 %

3 / 3

100.0 %

0 / 0

build-coverage/src/options/prop_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/prop_options.h

100.0 %

4 / 4

100.0 %

0 / 0

build-coverage/src/options/quantifiers_options.cpp

10.3 %

46 / 447

6.2 %

44 / 715

build-coverage/src/options/quantifiers_options.h

92.6 %

87 / 94

100.0 %

0 / 0

build-coverage/src/options/sep_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/sep_options.h

100.0 %

5 / 5

100.0 %

0 / 0

build-coverage/src/options/sets_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/sets_options.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/src/options/smt_options.cpp

26.7 %

43 / 161

15.4 %

40 / 259

build-coverage/src/options/smt_options.h

100.0 %

13 / 13

100.0 %

0 / 0

build-coverage/src/options/strings_options.cpp

2.7 %

1 / 37

3.3 %

2 / 61

build-coverage/src/options/strings_options.h

100.0 %

20 / 20

100.0 %

0 / 0

build-coverage/src/options/theory_options.cpp

18.4 %

7 / 38

12.5 %

8 / 64

build-coverage/src/options/theory_options.h

100.0 %

3 / 3

100.0 %

0 / 0

build-coverage/src/options/uf_options.cpp

18.8 %

3 / 16

10.7 %

3 / 28

build-coverage/src/options/uf_options.h

100.0 %

7 / 7

100.0 %

0 / 0

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

73.1 %

1969 / 2693

59.5 %

948 / 1592

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

72.7 %

3265 / 4493

45.3 %

2487 / 5487

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

61 / 101

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

79.5 %

31 / 39

39.3 %

42 / 107

src/api/cpp/cvc5.cpp

75.2 %

2530 / 3366

26.9 %

6830 / 25352

src/api/cpp/cvc5.h

90.6 %

29 / 32

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

86.8 %

92 / 106

41.1 %

101 / 246

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

93.8 %

30 / 32

50.0 %

17 / 34

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 %

11 / 11

50.0 %

3 / 6

src/base/output.h

83.3 %

90 / 108

13.5 %

117 / 867

src/context/cdhashmap.h

97.6 %

121 / 124

39.7 %

510 / 1285

src/context/cdhashset.h

87.5 %

35 / 40

2.8 %

1 / 36

src/context/cdinsert_hashmap.h

100.0 %

102 / 102

32.5 %

214 / 658

src/context/cdlist.h

95.3 %

143 / 150

37.6 %

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

18 / 18

50.0 %

2 / 4

src/decision/decision_engine.h

80.0 %

4 / 5

100.0 %

0 / 0

src/decision/decision_engine_old.cpp

71.8 %

28 / 39

25.0 %

38 / 152

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

0.1 %

2 / 1509

src/decision/justification_heuristic.h

0.0 %

0 / 3

0.0 %

0 / 6

src/decision/justification_strategy.cpp

97.9 %

274 / 280

43.5 %

499 / 1148

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

551 / 1184

src/expr/attribute_internals.h

100.0 %

68 / 68

34.1 %

56 / 164

src/expr/attribute_unique_id.h

0.0 %

0 / 5

100.0 %

0 / 0

src/expr/bound_var_manager.cpp

89.5 %

17 / 19

40.6 %

13 / 32

src/expr/bound_var_manager.h

100.0 %

13 / 13

40.8 %

53 / 130

src/expr/cardinality_constraint.cpp

75.6 %

31 / 41

33.3 %

16 / 48

src/expr/codatatype_bound_variable.cpp

48.7 %

19 / 39

22.6 %

19 / 84

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

88.7 %

424 / 478

36.6 %

733 / 2000

src/expr/dtype.h

50.0 %

1 / 2

45.0 %

18 / 40

src/expr/dtype_cons.cpp

94.4 %

318 / 337

38.9 %

504 / 1296

src/expr/dtype_cons.h

100.0 %

2 / 2

50.0 %

8 / 16

src/expr/dtype_selector.cpp

82.9 %

29 / 35

23.0 %

28 / 122

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

8.1 %

11 / 135

2.0 %

9 / 445

src/expr/node.cpp

84.0 %

42 / 50

51.8 %

115 / 222

src/expr/node.h

85.6 %

291 / 340

33.5 %

614 / 1832

src/expr/node_algorithm.cpp

88.9 %

338 / 380

51.0 %

535 / 1050

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

85.2 %

127 / 149

32.9 %

272 / 826

src/expr/node_converter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/node_manager.cpp

85.3 %

466 / 546

35.7 %

597 / 1672

src/expr/node_manager.h

90.6 %

145 / 160

26.3 %

511 / 1940

src/expr/node_self_iterator.h

100.0 %

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

22.5 %

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

187 / 198

42.9 %

346 / 807

src/expr/skolem_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/subs.cpp

49.5 %

45 / 91

20.5 %

48 / 234

src/expr/subs.h

100.0 %

1 / 1

50.0 %

1 / 2

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

81.8 %

189 / 231

37.6 %

185 / 492

src/expr/symbol_table.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/term_canonize.cpp

99.1 %

111 / 112

53.8 %

210 / 390

src/expr/term_canonize.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/term_context.cpp

71.4 %

40 / 56

58.6 %

34 / 58

src/expr/term_context.h

88.9 %

8 / 9

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

289 / 334

38.1 %

391 / 1026

src/expr/type_node.h

85.3 %

157 / 184

23.9 %

130 / 545

src/expr/uninterpreted_constant.cpp

65.8 %

25 / 38

36.9 %

31 / 84

src/expr/variadic_trie.cpp

100.0 %

18 / 18

73.1 %

19 / 26

src/expr/variadic_trie.h

100.0 %

1 / 1

50.0 %

1 / 2

src/main/command_executor.cpp

75.2 %

76 / 101

43.4 %

178 / 410

src/main/command_executor.h

100.0 %

5 / 5

100.0 %

0 / 0

src/main/driver_unified.cpp

54.8 %

69 / 126

29.1 %

121 / 416

src/main/interactive_shell.cpp

66.7 %

56 / 84

35.3 %

102 / 289

src/main/main.cpp

56.0 %

14 / 25

28.3 %

30 / 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/language.cpp

82.6 %

19 / 23

61.4 %

35 / 57

src/options/language.h

100.0 %

4 / 4

100.0 %

0 / 0

src/options/managed_streams.cpp

45.3 %

24 / 53

18.3 %

15 / 82

src/options/managed_streams.h

70.8 %

17 / 24

37.5 %

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

53.2 %

115 / 216

23.8 %

111 / 466

src/options/options_handler.h

42.9 %

6 / 14

2.5 %

2 / 80

src/options/options_public.h

100.0 %

10 / 10

0.8 %

4 / 520

src/options/set_language.cpp

63.0 %

17 / 27

75.0 %

9 / 12

src/parser/antlr_input.cpp

93.4 %

199 / 213

47.8 %

221 / 462

src/parser/antlr_input.h

89.3 %

25 / 28

38.5 %

30 / 78

src/parser/antlr_input_imports.cpp

71.2 %

79 / 111

26.9 %

64 / 238

src/parser/antlr_line_buffered_input.cpp

83.0 %

73 / 88

21.6 %

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

82.1 %

32 / 39

34.3 %

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

69.1 %

357 / 517

32.1 %

442 / 1377

src/parser/parser.h

69.7 %

23 / 33

16.7 %

1 / 6

src/parser/parser_builder.cpp

96.9 %

63 / 65

49.0 %

47 / 96

src/parser/parser_builder.h

100.0 %

1 / 1

100.0 %

0 / 0

src/parser/parser_exception.h

65.0 %

13 / 20

50.0 %

2 / 4

src/parser/smt2/smt2.cpp

86.5 %

591 / 683

47.2 %

1053 / 2230

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

137 / 352

src/preprocessing/assertion_pipeline.h

100.0 %

14 / 14

100.0 %

4 / 4

src/preprocessing/learned_literal_manager.cpp

100.0 %

18 / 18

51.8 %

29 / 56

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

56.5 %

26 / 46

src/preprocessing/passes/apply_substs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bool_to_bv.cpp

96.6 %

173 / 179

52.1 %

409 / 785

src/preprocessing/passes/bool_to_bv.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.1 %

64 / 68

45.8 %

136 / 297

src/preprocessing/passes/bv_intro_pow2.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_to_bool.cpp

97.4 %

149 / 153

40.6 %

371 / 914

src/preprocessing/passes/bv_to_bool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_to_int.cpp

89.6 %

430 / 480

41.4 %

845 / 2042

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

57.1 %

8 / 14

src/preprocessing/passes/extended_rewriter_pass.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/foreign_theory_rewrite.cpp

98.3 %

58 / 59

38.6 %

98 / 254

src/preprocessing/passes/foreign_theory_rewrite.h

100.0 %

2 / 2

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 %

20 / 20

60.0 %

24 / 40

src/preprocessing/passes/ite_removal.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ite_simp.cpp

48.7 %

57 / 117

16.1 %

64 / 398

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

81.9 %

304 / 371

39.6 %

734 / 1852

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 %

214 / 222

41.5 %

491 / 1182

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 %

16 / 16

54.0 %

27 / 50

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

89.1 %

49 / 55

49.5 %

98 / 198

src/preprocessing/passes/sep_skolem_emp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/sort_infer.cpp

100.0 %

31 / 31

56.4 %

44 / 78

src/preprocessing/passes/sort_infer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/static_learning.cpp

100.0 %

33 / 33

58.5 %

55 / 94

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 %

156 / 163

48.9 %

304 / 622

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 %

17 / 17

61.8 %

21 / 34

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 %

13 / 13

52.1 %

25 / 48

src/preprocessing/preprocessing_pass_context.cpp

90.9 %

30 / 33

47.1 %

16 / 34

src/preprocessing/preprocessing_pass_context.h

100.0 %

6 / 6

100.0 %

0 / 0

src/preprocessing/preprocessing_pass_registry.cpp

96.4 %

53 / 55

48.0 %

147 / 306

src/preprocessing/util/ite_utilities.cpp

46.4 %

457 / 984

21.2 %

777 / 3659

src/preprocessing/util/ite_utilities.h

18.6 %

8 / 43

9.1 %

4 / 44

src/printer/ast/ast_printer.cpp

23.3 %

50 / 215

20.4 %

51 / 250

src/printer/ast/ast_printer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/printer/let_binding.cpp

98.1 %

103 / 105

47.0 %

170 / 362

src/printer/let_binding.h

100.0 %

1 / 1

100.0 %

0 / 0

src/printer/printer.cpp

23.5 %

59 / 251

15.0 %

63 / 419

src/printer/printer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/printer/smt2/smt2_printer.cpp

73.5 %

869 / 1183

45.8 %

1391 / 3038

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/alethe/alethe_node_converter.cpp

14.3 %

1 / 7

10.0 %

2 / 20

src/proof/alethe/alethe_node_converter.h

0.0 %

0 / 1

100.0 %

0 / 0

src/proof/alethe/alethe_post_processor.cpp

0.2 %

1 / 427

0.1 %

2 / 2101

src/proof/alethe/alethe_post_processor.h

0.0 %

0 / 2

100.0 %

0 / 0

src/proof/alethe/alethe_proof_rule.cpp

1.0 %

1 / 98

2.1 %

2 / 96

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

83.3 %

145 / 174

39.0 %

227 / 582

src/proof/lazy_tree_proof_generator.cpp

73.8 %

48 / 65

22.9 %

32 / 140

src/proof/lazy_tree_proof_generator.h

78.6 %

11 / 14

50.0 %

7 / 14

src/proof/lfsc/lfsc_list_sc_node_converter.cpp

1.7 %

1 / 60

0.8 %

2 / 266

src/proof/lfsc/lfsc_list_sc_node_converter.h

0.0 %

0 / 1

100.0 %

0 / 0

src/proof/lfsc/lfsc_node_converter.cpp

37.2 %

221 / 594

17.2 %

436 / 2536

src/proof/lfsc/lfsc_node_converter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/lfsc/lfsc_post_processor.cpp

50.2 %

102 / 203

21.0 %

189 / 898

src/proof/lfsc/lfsc_post_processor.h

100.0 %

2 / 2

100.0 %

0 / 0

src/proof/lfsc/lfsc_print_channel.cpp

92.0 %

81 / 88

51.6 %

32 / 62

src/proof/lfsc/lfsc_print_channel.h

57.1 %

8 / 14

100.0 %

0 / 0

src/proof/lfsc/lfsc_printer.cpp

61.9 %

237 / 383

25.0 %

367 / 1469

src/proof/lfsc/lfsc_printer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/lfsc/lfsc_util.cpp

67.6 %

25 / 37

42.9 %

15 / 35

src/proof/lfsc/lfsc_util.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/method_id.cpp

69.2 %

36 / 52

48.8 %

41 / 84

src/proof/print_expr.cpp

85.0 %

17 / 20

31.8 %

14 / 44

src/proof/print_expr.h

85.7 %

6 / 7

33.3 %

4 / 12

src/proof/proof.cpp

81.2 %

177 / 218

43.0 %

397 / 924

src/proof/proof_checker.cpp

55.2 %

91 / 165

20.9 %

128 / 612

src/proof/proof_checker.h

75.0 %

3 / 4

100.0 %

0 / 0

src/proof/proof_ensure_closed.cpp

63.2 %

48 / 76

21.4 %

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

84.8 %

39 / 46

39.1 %

43 / 110

src/proof/proof_letify.h

100.0 %

2 / 2

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

92.0 %

126 / 137

50.6 %

166 / 328

src/proof/proof_node_manager.cpp

82.7 %

182 / 220

32.7 %

292 / 894

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

21.2 %

38 / 179

19.1 %

31 / 162

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

76.5 %

65 / 85

27.5 %

39 / 142

src/prop/cnf_stream.cpp

98.5 %

394 / 400

39.3 %

764 / 1943

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 %

856 / 1027

42.3 %

1178 / 2784

src/prop/minisat/core/Solver.h

92.1 %

105 / 114

42.8 %

95 / 222

src/prop/minisat/core/SolverTypes.h

87.5 %

140 / 160

35.3 %

67 / 190

src/prop/minisat/minisat.cpp

81.9 %

145 / 177

33.1 %

92 / 278

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

47.5 %

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

97.7 %

605 / 619

46.7 %

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

76.4 %

259 / 339

32.7 %

378 / 1156

src/prop/prop_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/prop_proof_manager.cpp

58.0 %

29 / 50

19.4 %

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

314 / 435

30.1 %

627 / 2086

src/prop/sat_proof_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/sat_solver.h

10.5 %

4 / 38

0.0 %

0 / 30

src/prop/sat_solver_factory.cpp

84.6 %

11 / 13

31.3 %

5 / 16

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

90 / 91

46.5 %

131 / 282

src/prop/theory_proxy.cpp

94.7 %

108 / 114

41.4 %

140 / 338

src/smt/abduction_solver.cpp

85.1 %

86 / 101

39.1 %

162 / 414

src/smt/abstract_values.cpp

100.0 %

16 / 16

39.7 %

23 / 58

src/smt/assertions.cpp

87.3 %

89 / 102

46.8 %

102 / 218

src/smt/check_models.cpp

75.0 %

36 / 48

40.1 %

81 / 202

src/smt/check_models.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/command.cpp

56.1 %

690 / 1231

32.7 %

489 / 1497

src/smt/command.h

80.3 %

61 / 76

25.0 %

4 / 16

src/smt/difficulty_post_processor.cpp

3.7 %

1 / 27

2.3 %

2 / 86

src/smt/difficulty_post_processor.h

0.0 %

0 / 1

100.0 %

0 / 0

src/smt/env.cpp

96.0 %

95 / 99

46.5 %

67 / 144

src/smt/env_obj.cpp

100.0 %

26 / 26

50.0 %

7 / 14

src/smt/env_obj.h

100.0 %

2 / 2

100.0 %

0 / 0

src/smt/expand_definitions.cpp

98.5 %

67 / 68

47.0 %

126 / 268

src/smt/interpolation_solver.cpp

78.6 %

44 / 56

40.0 %

80 / 200

src/smt/listeners.cpp

28.6 %

2 / 7

7.7 %

2 / 26

src/smt/listeners.h

100.0 %

1 / 1

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

123 / 145

36.5 %

279 / 764

src/smt/model_blocker.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/model_core_builder.cpp

79.6 %

43 / 54

35.5 %

66 / 186

src/smt/model_core_builder.h

100.0 %

1 / 1

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

93.2 %

110 / 118

44.4 %

245 / 552

src/smt/preprocess_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/preprocessor.cpp

98.3 %

58 / 59

43.4 %

53 / 122

src/smt/print_benchmark.cpp

41.7 %

50 / 120

13.2 %

43 / 326

src/smt/print_benchmark.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/process_assertions.cpp

92.9 %

195 / 210

52.6 %

362 / 688

src/smt/proof_final_callback.cpp

93.0 %

40 / 43

46.9 %

46 / 98

src/smt/proof_final_callback.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/proof_manager.cpp

58.1 %

86 / 148

21.9 %

117 / 534

src/smt/proof_post_processor.cpp

92.5 %

552 / 597

39.0 %

1122 / 2874

src/smt/proof_post_processor.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/quant_elim_solver.cpp

91.8 %

56 / 61

45.2 %

141 / 312

src/smt/set_defaults.cpp

82.2 %

674 / 820

62.5 %

961 / 1538

src/smt/set_defaults.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/smt_mode.cpp

8.3 %

1 / 12

16.7 %

2 / 12

src/smt/smt_solver.cpp

90.0 %

90 / 100

47.9 %

137 / 286

src/smt/smt_statistics_registry.cpp

100.0 %

3 / 3

50.0 %

2 / 4

src/smt/solver_engine.cpp

84.5 %

808 / 956

39.4 %

1180 / 2995

src/smt/solver_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/solver_engine_scope.cpp

90.5 %

19 / 21

21.9 %

14 / 64

src/smt/solver_engine_state.cpp

91.1 %

123 / 135

37.5 %

94 / 251

src/smt/solver_engine_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/solver_engine_stats.cpp

100.0 %

17 / 17

50.0 %

12 / 24

src/smt/sygus_solver.cpp

90.6 %

211 / 233

45.8 %

391 / 854

src/smt/term_formula_removal.cpp

93.9 %

217 / 231

47.5 %

444 / 934

src/smt/unsat_core_manager.cpp

83.9 %

47 / 56

37.9 %

69 / 182

src/smt/unsat_core_manager.h

100.0 %

2 / 2

100.0 %

0 / 0

src/smt/witness_form.cpp

70.3 %

45 / 64

27.4 %

81 / 296

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

88.2 %

60 / 68

41.0 %

77 / 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 / 278

0.1 %

2 / 1334

src/theory/arith/arith_msum.cpp

89.6 %

129 / 144

50.3 %

322 / 640

src/theory/arith/arith_msum.h

100.0 %

2 / 2

55.0 %

11 / 20

src/theory/arith/arith_poly_norm.cpp

96.8 %

121 / 125

45.7 %

184 / 403

src/theory/arith/arith_poly_norm.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/arith_preprocess.cpp

25.0 %

7 / 28

7.5 %

6 / 80

src/theory/arith/arith_preprocess.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/arith_rewriter.cpp

88.5 %

460 / 520

42.0 %

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

85.9 %

134 / 156

40.7 %

368 / 905

src/theory/arith/arith_utilities.cpp

80.9 %

127 / 157

36.8 %

233 / 634

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

16.7 %

13 / 78

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

87 / 136

37.5 %

170 / 453

src/theory/arith/bound_inference.h

100.0 %

2 / 2

50.0 %

15 / 30

src/theory/arith/branch_and_bound.cpp

96.9 %

63 / 65

49.3 %

226 / 458

src/theory/arith/branch_and_bound.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/callbacks.cpp

88.0 %

103 / 117

22.9 %

100 / 436

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 %

729 / 1926

src/theory/arith/congruence_manager.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/arith/constraint.cpp

73.2 %

1088 / 1487

28.2 %

1814 / 6431

src/theory/arith/constraint.h

94.4 %

101 / 107

16.7 %

36 / 216

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

423 / 482

35.6 %

845 / 2376

src/theory/arith/dio_solver.h

76.9 %

30 / 39

16.1 %

18 / 112

src/theory/arith/dual_simplex.cpp

87.5 %

105 / 120

36.2 %

195 / 538

src/theory/arith/dual_simplex.h

100.0 %

8 / 8

100.0 %

0 / 0

src/theory/arith/equality_solver.cpp

70.2 %

40 / 57

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 %

201 / 314

26.6 %

164 / 617

src/theory/arith/error_set.h

51.1 %

47 / 92

8.7 %

12 / 138

src/theory/arith/fc_simplex.cpp

4.5 %

21 / 471

0.8 %

16 / 2092

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

46.5 %

368 / 791

19.1 %

620 / 3246

src/theory/arith/linear_equality.h

26.3 %

49 / 186

4.2 %

19 / 452

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

251 / 354

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

78.9 %

131 / 166

43.0 %

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

75.0 %

12 / 16

19.4 %

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

91.8 %

78 / 85

44.9 %

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

50 / 86

26.4 %

87 / 330

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 %

110 / 111

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

61.3 %

195 / 318

34.6 %

508 / 1468

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 %

360 / 371

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

8.0 %

4 / 50

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

74 / 75

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

117 / 153

34.8 %

253 / 726

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

171 / 203

43.7 %

268 / 613

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

100.0 %

10 / 10

50.0 %

1 / 2

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

100.0 %

18 / 18

50.0 %

3 / 6

src/theory/arith/nl/nl_model.cpp

69.9 %

432 / 618

33.2 %

941 / 2833

src/theory/arith/nl/nl_model.h

100.0 %

1 / 1

50.0 %

12 / 24

src/theory/arith/nl/nonlinear_extension.cpp

89.5 %

280 / 313

51.2 %

483 / 943

src/theory/arith/nl/nonlinear_extension.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/poly_conversion.cpp

60.7 %

241 / 397

23.4 %

411 / 1754

src/theory/arith/nl/poly_conversion.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/pow2_solver.cpp

95.7 %

90 / 94

48.5 %

194 / 400

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 %

225 / 227

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 %

239 / 552

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

100.0 %

2 / 2

30.0 %

3 / 10

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

85.9 %

177 / 206

42.1 %

349 / 829

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

183 / 195

49.5 %

488 / 986

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 %

19 / 19

42.4 %

56 / 132

src/theory/arith/pp_rewrite_eq.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/proof_checker.cpp

67.2 %

123 / 183

27.7 %

253 / 912

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

36.2 %

59 / 163

14.1 %

83 / 590

src/theory/arith/simplex.h

18.2 %

2 / 11

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

23 / 523

0.9 %

20 / 2300

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

7.5 %

3 / 40

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

90.1 %

163 / 181

41.6 %

208 / 500

src/theory/arith/theory_arith.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/arith/theory_arith_private.cpp

58.6 %

1712 / 2920

27.5 %

3434 / 12510

src/theory/arith/theory_arith_private.h

84.4 %

27 / 32

35.7 %

15 / 42

src/theory/arith/theory_arith_type_rules.cpp

76.1 %

54 / 71

30.0 %

73 / 243

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

51 / 61

38.8 %

80 / 206

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

73.1 %

896 / 1225

36.6 %

2364 / 6457

src/theory/arrays/theory_arrays.h

97.9 %

46 / 47

55.3 %

63 / 114

src/theory/arrays/theory_arrays_rewriter.cpp

98.6 %

352 / 357

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

92 / 138

26.2 %

179 / 684

src/theory/arrays/type_enumerator.cpp

91.9 %

68 / 74

49.0 %

101 / 206

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

98.5 %

128 / 130

41.8 %

203 / 486

src/theory/bags/bags_rewriter.cpp

91.5 %

227 / 248

44.9 %

864 / 1925

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

91.7 %

222 / 242

34.8 %

556 / 1598

src/theory/bags/inference_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/inference_manager.cpp

78.6 %

11 / 14

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

273 / 291

43.3 %

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

20.0 %

6 / 30

src/theory/bags/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/theory_bags.cpp

89.7 %

105 / 117

40.1 %

154 / 384

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

95.7 %

358 / 374

51.3 %

919 / 1792

src/theory/booleans/circuit_propagator.h

100.0 %

29 / 29

52.0 %

52 / 100

src/theory/booleans/proof_checker.cpp

79.8 %

419 / 525

28.4 %

950 / 3350

src/theory/booleans/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/booleans/proof_circuit_propagator.cpp

95.7 %

245 / 256

53.0 %

588 / 1110

src/theory/booleans/proof_circuit_propagator.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/booleans/theory_bool.cpp

91.3 %

21 / 23

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

170 / 219

31.7 %

304 / 960

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

82.9 %

34 / 41

30.1 %

81 / 269

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 %

10 / 10

54.2 %

13 / 24

src/theory/builtin/theory_builtin_type_rules.h

71.4 %

35 / 49

37.3 %

62 / 166

src/theory/builtin/type_enumerator.cpp

96.2 %

25 / 26

43.8 %

35 / 80

src/theory/builtin/type_enumerator.h

100.0 %

1 / 1

50.0 %

2 / 4

src/theory/bv/bitblast/bitblast_proof_generator.cpp

100.0 %

27 / 27

54.1 %

53 / 98

src/theory/bv/bitblast/bitblast_proof_generator.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/bv/bitblast/bitblast_strategies_template.h

79.8 %

359 / 450

27.9 %

678 / 2432

src/theory/bv/bitblast/bitblast_utils.h

88.9 %

96 / 108

37.7 %

144 / 382

src/theory/bv/bitblast/bitblaster.h

95.3 %

61 / 64

36.1 %

13 / 36

src/theory/bv/bitblast/node_bitblaster.cpp

95.1 %

77 / 81

38.0 %

124 / 326

src/theory/bv/bitblast/node_bitblaster.h

50.0 %

1 / 2

0.0 %

0 / 4

src/theory/bv/bitblast/proof_bitblaster.cpp

100.0 %

83 / 83

52.9 %

164 / 310

src/theory/bv/bv_solver.h

70.8 %

17 / 24

0.0 %

0 / 6

src/theory/bv/bv_solver_bitblast.cpp

95.2 %

157 / 165

48.2 %

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

80 / 82

56.7 %

152 / 268

src/theory/bv/bv_solver_bitblast_internal.h

66.7 %

2 / 3

0.0 %

0 / 2

src/theory/bv/int_blaster.cpp

59.9 %

226 / 377

24.8 %

410 / 1652

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

97.2 %

207 / 213

47.8 %

418 / 874

src/theory/bv/theory_bv.h

0.0 %

0 / 1

0.0 %

0 / 2

src/theory/bv/theory_bv_rewrite_rules.h

30.5 %

74 / 243

26.9 %

4711 / 17531

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

91.6 %

609 / 665

48.1 %

1214 / 2525

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

85.7 %

613 / 715

44.1 %

1806 / 4098

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

36.4 %

4 / 11

25.0 %

17 / 68

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

44 / 46

35.5 %

39 / 110

src/theory/datatypes/datatypes_rewriter.cpp

94.2 %

549 / 583

45.3 %

1201 / 2649

src/theory/datatypes/datatypes_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/infer_proof_cons.cpp

83.6 %

122 / 146

40.1 %

350 / 873

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 %

69 / 69

55.1 %

141 / 256

src/theory/datatypes/proof_checker.cpp

77.6 %

52 / 67

25.9 %

111 / 428

src/theory/datatypes/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/datatypes/sygus_datatype_utils.cpp

85.7 %

246 / 287

38.9 %

495 / 1274

src/theory/datatypes/sygus_extension.cpp

85.8 %

866 / 1009

40.6 %

2000 / 4932

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

90.3 %

1029 / 1139

45.7 %

2336 / 5108

src/theory/datatypes/theory_datatypes.h

88.2 %

15 / 17

47.5 %

19 / 40

src/theory/datatypes/theory_datatypes_type_rules.cpp

77.9 %

219 / 281

32.7 %

445 / 1360

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

58 / 61

53.7 %

87 / 162

src/theory/decision_strategy.h

100.0 %

5 / 5

100.0 %

0 / 0

src/theory/difficulty_manager.cpp

24.4 %

11 / 45

3.2 %

6 / 188

src/theory/difficulty_manager.h

100.0 %

1 / 1

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

125 / 140

44.0 %

190 / 432

src/theory/ee_manager_central.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/ee_manager_distributed.cpp

97.7 %

42 / 43

36.1 %

39 / 108

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

81.5 %

405 / 497

40.2 %

712 / 1769

src/theory/evaluator.h

100.0 %

6 / 6

100.0 %

0 / 0

src/theory/ext_theory.cpp

64.9 %

163 / 251

39.0 %

283 / 725

src/theory/ext_theory.h

100.0 %

7 / 7

50.0 %

1 / 2

src/theory/fp/fp_expand_defs.cpp

62.2 %

79 / 127

24.2 %

152 / 628

src/theory/fp/fp_expand_defs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/fp/fp_word_blaster.cpp

87.4 %

521 / 596

32.9 %

1398 / 4249

src/theory/fp/fp_word_blaster.h

100.0 %

5 / 5

100.0 %

0 / 0

src/theory/fp/theory_fp.cpp

94.4 %

424 / 449

39.6 %

977 / 2468

src/theory/fp/theory_fp.h

85.7 %

6 / 7

0.0 %

0 / 2

src/theory/fp/theory_fp_rewriter.cpp

78.9 %

602 / 763

26.4 %

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

30.9 %

471 / 1524

src/theory/fp/type_enumerator.h

50.0 %

27 / 54

24.3 %

17 / 70

src/theory/incomplete_id.cpp

3.4 %

1 / 29

9.1 %

2 / 22

src/theory/inference_id.cpp

1.6 %

7 / 430

1.9 %

6 / 324

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

58.0 %

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

97.5 %

117 / 120

47.9 %

223 / 466

src/theory/quantifiers/alpha_equivalence.h

100.0 %

6 / 6

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 %

456 / 526

43.0 %

1177 / 2740

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

818 / 899

48.8 %

1642 / 3362

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 %

465 / 972

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 %

1255 / 1416

42.6 %

2547 / 5974

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 %

16 / 16

50.0 %

6 / 12

src/theory/quantifiers/ematching/ho_trigger.cpp

89.5 %

230 / 257

41.1 %

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

302 / 353

43.1 %

618 / 1434

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

78.6 %

11 / 14

30.0 %

3 / 10

src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp

75.8 %

276 / 364

37.5 %

500 / 1335

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

67.1 %

53 / 79

38.1 %

91 / 239

src/theory/quantifiers/ematching/instantiation_engine.cpp

89.9 %

116 / 129

48.6 %

177 / 364

src/theory/quantifiers/ematching/instantiation_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/ematching/pattern_term_selector.cpp

93.0 %

334 / 359

49.9 %

761 / 1524

src/theory/quantifiers/ematching/relational_match_generator.cpp

98.2 %

55 / 56

39.9 %

107 / 268

src/theory/quantifiers/ematching/relational_match_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/ematching/trigger.cpp

85.2 %

98 / 115

38.3 %

171 / 446

src/theory/quantifiers/ematching/trigger_database.cpp

91.4 %

74 / 81

49.5 %

90 / 182

src/theory/quantifiers/ematching/trigger_term_info.cpp

100.0 %

61 / 61

69.4 %

172 / 248

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

96.9 %

31 / 32

53.1 %

52 / 98

src/theory/quantifiers/ematching/var_match_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/entailment_check.cpp

98.4 %

181 / 184

56.5 %

450 / 796

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

86.5 %

32 / 37

37.8 %

37 / 98

src/theory/quantifiers/expr_miner.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/expr_miner_manager.cpp

68.3 %

69 / 101

40.3 %

62 / 154

src/theory/quantifiers/expr_miner_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/extended_rewrite.cpp

93.0 %

803 / 863

50.0 %

1963 / 3928

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 %

247 / 536

src/theory/quantifiers/first_order_model.h

66.7 %

4 / 6

40.9 %

9 / 22

src/theory/quantifiers/fmf/bounded_integers.cpp

93.7 %

507 / 541

45.5 %

1247 / 2740

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 %

1664 / 3241

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

140 / 198

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

82 / 390

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

80.1 %

278 / 347

38.3 %

537 / 1402

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

72.9 %

62 / 85

26.2 %

99 / 378

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

82 / 142

src/theory/quantifiers/quant_bound_inference.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quant_conflict_find.cpp

83.1 %

1158 / 1393

45.5 %

2453 / 5389

src/theory/quantifiers/quant_conflict_find.h

100.0 %

18 / 18

52.8 %

19 / 36

src/theory/quantifiers/quant_module.cpp

92.0 %

23 / 25

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

20 / 21

61.8 %

21 / 34

src/theory/quantifiers/quant_relevance.h

33.3 %

1 / 3

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

99.0 %

101 / 102

53.3 %

209 / 392

src/theory/quantifiers/quant_split.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/quant_util.cpp

82.1 %

69 / 84

41.9 %

93 / 222

src/theory/quantifiers/quant_util.h

66.7 %

4 / 6

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_attributes.cpp

74.3 %

171 / 230

43.0 %

396 / 922

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

134 / 144

44.6 %

292 / 654

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_preprocess.cpp

54.6 %

71 / 130

26.6 %

168 / 632

src/theory/quantifiers/quantifiers_preprocess.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_registry.cpp

91.3 %

94 / 103

33.7 %

114 / 338

src/theory/quantifiers/quantifiers_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_rewriter.cpp

80.6 %

875 / 1086

42.8 %

1893 / 4423

src/theory/quantifiers/quantifiers_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_state.cpp

52.9 %

45 / 85

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

1 / 223

0.3 %

2 / 674

src/theory/quantifiers/query_generator.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/quantifiers/query_generator_unsat.cpp

96.6 %

86 / 89

39.1 %

136 / 348

src/theory/quantifiers/query_generator_unsat.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/relevant_domain.cpp

96.6 %

226 / 234

50.6 %

452 / 894

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

188 / 210

42.1 %

420 / 998

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

96.8 %

275 / 284

46.7 %

572 / 1224

src/theory/quantifiers/sygus/ce_guided_single_inv.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/sygus/cegis.cpp

94.5 %

327 / 346

47.8 %

618 / 1294

src/theory/quantifiers/sygus/cegis.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/cegis_core_connective.cpp

88.3 %

370 / 419

41.7 %

755 / 1809

src/theory/quantifiers/sygus/cegis_core_connective.h

100.0 %

5 / 5

50.0 %

2 / 4

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 %

228 / 342

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

93 / 111

40.7 %

180 / 442

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 %

32 / 32

54.2 %

39 / 72

src/theory/quantifiers/sygus/rcons_type_info.h

100.0 %

1 / 1

100.0 %

0 / 0

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 %

40 / 40

50.0 %

65 / 130

src/theory/quantifiers/sygus/sygus_enumerator_callback.h

50.0 %

2 / 4

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_eval_unfold.cpp

94.0 %

172 / 183

39.9 %

366 / 918

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

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

798 / 909

42.1 %

1470 / 3488

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 %

152 / 180

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

87.5 %

119 / 136

42.2 %

223 / 528

src/theory/quantifiers/sygus/sygus_invariance.h

100.0 %

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

90.1 %

183 / 203

50.4 %

394 / 782

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

91.4 %

53 / 58

35.7 %

50 / 140

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

65.9 %

419 / 636

27.9 %

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

6 / 12

src/theory/quantifiers/sygus/sygus_utils.cpp

74.4 %

58 / 78

30.2 %

110 / 364

src/theory/quantifiers/sygus/synth_conjecture.cpp

90.2 %

486 / 539

42.1 %

997 / 2366

src/theory/quantifiers/sygus/synth_conjecture.h

100.0 %

7 / 7

100.0 %

0 / 0

src/theory/quantifiers/sygus/synth_engine.cpp

95.0 %

114 / 120

55.0 %

187 / 340

src/theory/quantifiers/sygus/synth_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/sygus/synth_verify.cpp

91.7 %

44 / 48

44.4 %

87 / 196

src/theory/quantifiers/sygus/template_infer.cpp

97.9 %

95 / 97

44.9 %

236 / 526

src/theory/quantifiers/sygus/template_infer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/term_database_sygus.cpp

86.6 %

446 / 515

41.7 %

784 / 1879

src/theory/quantifiers/sygus/term_database_sygus.h

100.0 %

5 / 5

62.5 %

5 / 8

src/theory/quantifiers/sygus/transition_inference.cpp

95.0 %

283 / 298

47.7 %

532 / 1116

src/theory/quantifiers/sygus/transition_inference.h

100.0 %

12 / 12

50.0 %

5 / 10

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 %

213 / 258

37.1 %

370 / 998

src/theory/quantifiers/sygus_inst.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/sygus_sampler.cpp

80.7 %

369 / 457

39.2 %

591 / 1508

src/theory/quantifiers/sygus_sampler.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/term_database.cpp

75.4 %

285 / 378

37.1 %

578 / 1556

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

74 / 76

41.2 %

93 / 226

src/theory/quantifiers/term_pools.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/term_registry.cpp

90.8 %

59 / 65

48.1 %

75 / 156

src/theory/quantifiers/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/term_tuple_enumerator.cpp

75.8 %

157 / 207

36.2 %

241 / 666

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

91 / 174

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

520 / 1220

src/theory/relevance_manager.cpp

70.8 %

119 / 168

29.2 %

161 / 552

src/theory/relevance_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/rep_set.cpp

74.4 %

189 / 254

35.6 %

291 / 818

src/theory/rep_set.h

64.3 %

9 / 14

100.0 %

0 / 0

src/theory/rewriter.cpp

90.2 %

156 / 173

41.8 %

302 / 722

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

910 / 1081

41.4 %

2233 / 5388

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

527 / 577

47.8 %

1240 / 2595

src/theory/sets/cardinality_extension.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/sets/inference_manager.cpp

55.1 %

49 / 89

28.3 %

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

81.5 %

22 / 27

42.6 %

52 / 122

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

133 / 290

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 %

138 / 310

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 %

1471 / 3127

src/theory/sets/theory_sets_private.h

66.7 %

2 / 3

0.0 %

0 / 2

src/theory/sets/theory_sets_rels.cpp

94.9 %

738 / 778

52.1 %

1659 / 3185

src/theory/sets/theory_sets_rels.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/sets/theory_sets_rewriter.cpp

95.6 %

329 / 344

49.5 %

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

60 / 60

50.0 %

82 / 164

src/theory/sets/theory_sets_type_rules.cpp

78.5 %

161 / 205

26.1 %

280 / 1072

src/theory/shared_solver.cpp

92.2 %

47 / 51

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 %

34 / 34

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

133 / 156

32.4 %

228 / 704

src/theory/shared_terms_database.h

100.0 %

25 / 25

31.3 %

10 / 32

src/theory/skolem_lemma.cpp

100.0 %

15 / 15

33.8 %

25 / 74

src/theory/skolem_lemma.h

100.0 %

1 / 1

50.0 %

2 / 4

src/theory/smt_engine_subsolver.cpp

87.0 %

60 / 69

39.7 %

62 / 156

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

90.2 %

385 / 427

46.2 %

941 / 2036

src/theory/strings/arith_entail.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/array_solver.cpp

0.9 %

1 / 107

0.4 %

2 / 510

src/theory/strings/base_solver.cpp

85.5 %

331 / 387

42.1 %

685 / 1629

src/theory/strings/base_solver.h

100.0 %

2 / 2

50.0 %

2 / 4

src/theory/strings/core_solver.cpp

79.8 %

1117 / 1400

39.7 %

2562 / 6461

src/theory/strings/core_solver.h

100.0 %

2 / 2

40.9 %

9 / 22

src/theory/strings/eager_solver.cpp

98.6 %

136 / 138

46.4 %

336 / 724

src/theory/strings/eqc_info.cpp

100.0 %

59 / 59

44.6 %

148 / 332

src/theory/strings/eqc_info.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/extf_solver.cpp

84.3 %

305 / 362

44.2 %

789 / 1786

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

546 / 643

40.8 %

1065 / 2612

src/theory/strings/infer_proof_cons.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/inference_manager.cpp

86.9 %

159 / 183

44.7 %

352 / 788

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

92.5 %

283 / 306

44.9 %

631 / 1404

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_enumerator.cpp

6.7 %

1 / 15

11.1 %

2 / 18

src/theory/strings/regexp_enumerator.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/strings/regexp_operation.cpp

71.6 %

702 / 981

36.3 %

1480 / 4076

src/theory/strings/regexp_solver.cpp

89.1 %

295 / 331

48.3 %

589 / 1219

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

1602 / 1655

52.2 %

5017 / 9618

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

87.5 %

133 / 152

47.0 %

294 / 625

src/theory/strings/skolem_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/solver_state.cpp

96.2 %

100 / 104

46.4 %

154 / 332

src/theory/strings/strategy.cpp

70.7 %

58 / 82

34.1 %

71 / 208

src/theory/strings/strings_entail.cpp

94.8 %

422 / 445

46.5 %

942 / 2027

src/theory/strings/strings_fmf.cpp

92.7 %

38 / 41

54.4 %

49 / 90

src/theory/strings/strings_fmf.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/strings_rewriter.cpp

100.0 %

162 / 162

48.3 %

421 / 872

src/theory/strings/strings_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/term_registry.cpp

87.5 %

286 / 327

46.3 %

689 / 1488

src/theory/strings/theory_strings.cpp

82.1 %

481 / 586

41.6 %

1018 / 2445

src/theory/strings/theory_strings.h

100.0 %

32 / 32

52.3 %

69 / 132

src/theory/strings/theory_strings_preprocess.cpp

100.0 %

522 / 522

51.1 %

1574 / 3078

src/theory/strings/theory_strings_type_rules.cpp

70.8 %

97 / 137

26.4 %

122 / 462

src/theory/strings/theory_strings_utils.cpp

91.8 %

178 / 194

47.6 %

331 / 696

src/theory/strings/type_enumerator.cpp

83.9 %

125 / 149

32.0 %

85 / 266

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

49.3 %

110 / 223

25.5 %

212 / 830

src/theory/subs_minimize.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/substitutions.cpp

85.3 %

93 / 109

41.1 %

218 / 530

src/theory/substitutions.h

80.0 %

12 / 15

12.5 %

2 / 16

src/theory/term_registration_visitor.cpp

81.0 %

115 / 142

41.2 %

235 / 570

src/theory/term_registration_visitor.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/theory.cpp

85.0 %

272 / 320

49.2 %

551 / 1119

src/theory/theory.h

71.0 %

49 / 69

47.4 %

54 / 114

src/theory/theory_engine.cpp

83.8 %

715 / 853

41.3 %

1802 / 4362

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

89.8 %

219 / 244

42.5 %

359 / 844

src/theory/theory_model.cpp

87.3 %

370 / 424

42.1 %

764 / 1815

src/theory/theory_model.h

100.0 %

4 / 4

50.0 %

1 / 2

src/theory/theory_model_builder.cpp

93.3 %

623 / 668

42.2 %

1203 / 2851

src/theory/theory_model_builder.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/theory_preprocessor.cpp

96.3 %

208 / 216

45.5 %

410 / 902

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

66 / 68

41.6 %

79 / 190

src/theory/theory_state.h

100.0 %

1 / 1

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

93.1 %

54 / 58

23.7 %

37 / 156

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

813 / 1012

40.8 %

1661 / 4068

src/theory/uf/cardinality_extension.h

96.3 %

52 / 54

36.5 %

38 / 104

src/theory/uf/eq_proof.cpp

86.5 %

627 / 725

39.9 %

1506 / 3772

src/theory/uf/eq_proof.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/uf/equality_engine.cpp

91.7 %

1264 / 1378

43.6 %

2435 / 5586

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

90.7 %

185 / 204

45.8 %

490 / 1070

src/theory/uf/ho_extension.cpp

77.4 %

192 / 248

38.8 %

402 / 1036

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

207 / 264

35.8 %

482 / 1348

src/theory/uf/proof_equality_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/uf/symmetry_breaker.cpp

84.3 %

409 / 485

43.4 %

943 / 2172

src/theory/uf/symmetry_breaker.h

100.0 %

7 / 7

50.0 %

4 / 8

src/theory/uf/theory_uf.cpp

87.6 %

305 / 348

50.0 %

676 / 1352

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

87.6 %

106 / 121

42.5 %

295 / 694

src/theory/uf/theory_uf_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/uf/theory_uf_type_rules.cpp

68.1 %

77 / 113

31.6 %

151 / 478

src/theory/uf/type_enumerator.cpp

6.7 %

1 / 15

3.7 %

2 / 54

src/theory/uf/type_enumerator.h

0.0 %

0 / 2

0.0 %

0 / 4

src/theory/valuation.cpp

66.7 %

76 / 114

16.0 %

57 / 357

src/theory/valuation.h

100.0 %

3 / 3

100.0 %

0 / 0

src/util/abstract_value.cpp

100.0 %

6 / 6

31.3 %

5 / 16

src/util/abstract_value.h

100.0 %

6 / 6

50.0 %

1 / 2

src/util/bin_heap.h

98.8 %

163 / 165

21.8 %

123 / 564

src/util/bitvector.cpp

100.0 %

171 / 171

56.3 %

178 / 316

src/util/bitvector.h

91.9 %

68 / 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/didyoumean.cpp

98.5 %

64 / 65

69.5 %

57 / 82

src/util/didyoumean.h

80.0 %

4 / 5

50.0 %

1 / 2

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

86.4 %

191 / 221

42.7 %

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

63.2 %

103 / 163

33.9 %

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

58.2 %

114 / 196

32.5 %

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

15 / 15

71.9 %

23 / 32

src/util/statistics_public.cpp

100.0 %

13 / 13

52.4 %

22 / 42

src/util/statistics_registry.cpp

25.8 %

16 / 62

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

94.7 %

251 / 265

56.6 %

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

29.2 %

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

89.2 %

58 / 65

46.5 %

101 / 217

test/api/proj-issue306.cpp

100.0 %

16 / 16

50.0 %

22 / 44

test/api/proj-issue334.cpp

100.0 %

15 / 15

50.0 %

16 / 32

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

99.9 %

1775 / 1777

36.0 %

6700 / 18596

test/unit/api/solver_white.cpp

100.0 %

21 / 21

41.0 %

55 / 134

test/unit/api/sort_black.cpp

100.0 %

383 / 383

33.1 %

1214 / 3668

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 %

475 / 476

33.8 %

1568 / 4637

test/unit/node/node_builder_black.cpp

100.0 %

223 / 223

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 %

222 / 222

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 %

138 / 138

41.3 %

248 / 600

test/unit/parser/parser_builder_black.cpp

100.0 %

72 / 72

41.3 %

95 / 230

test/unit/preprocessing/pass_bv_gauss_white.cpp

97.6 %

1416 / 1451

42.6 %

4788 / 11231

test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp

100.0 %

17 / 17

42.5 %

45 / 106

test/unit/printer/smt2_printer_black.cpp

100.0 %

20 / 20

45.2 %

38 / 84

test/unit/prop/cnf_stream_white.cpp

89.8 %

106 / 118

38.9 %

182 / 468

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_env.h

100.0 %

6 / 6

50.0 %

2 / 4

test/unit/test_node.h

100.0 %

10 / 10

50.0 %

4 / 8

test/unit/test_smt.h

57.4 %

39 / 68

17.7 %

25 / 141

test/unit/theory/arith_poly_white.cpp

100.0 %

70 / 70

41.8 %

287 / 686

test/unit/theory/evaluator_white.cpp

100.0 %

79 / 79

43.7 %

223 / 510

test/unit/theory/logic_info_white.cpp

100.0 %

1230 / 1230

32.6 %

4138 / 12708

test/unit/theory/regexp_operation_black.cpp

100.0 %

78 / 78

48.3 %

231 / 478

test/unit/theory/sequences_rewriter_white.cpp

100.0 %

855 / 855

46.9 %

2459 / 5238

test/unit/theory/strings_rewriter_white.cpp

100.0 %

15 / 15

42.6 %

46 / 108

test/unit/theory/theory_arith_cad_white.cpp

92.2 %

214 / 232

41.8 %

625 / 1494

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 %

341 / 341

42.1 %

1078 / 2562

test/unit/theory/theory_bags_rewriter_white.cpp

100.0 %

478 / 478

41.7 %

1435 / 3442

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 %

142 / 142

40.3 %

484 / 1202

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 %

41 / 41

45.1 %

111 / 246

test/unit/theory/theory_bv_white.cpp

100.0 %

19 / 19

47.3 %

52 / 110

test/unit/theory/theory_engine_white.cpp

98.8 %

82 / 83

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 %

149 / 149

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 %

929 / 945

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 %

16 / 16

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 %

36 / 36

31.4 %

54 / 172

test/unit/theory/type_enumerator_white.cpp

100.0 %

207 / 207

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 %

23 / 23

25.9 %

30 / 116

test/unit/util/datatype_black.cpp

100.0 %

353 / 353

35.4 %

1099 / 3104

test/unit/util/didyoumean_black.cpp

100.0 %

24 / 24

34.1 %

60 / 176

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 %

62 / 62

37.6 %

146 / 388

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)