Head

GCC Code Coverage Report

Directory:	.			Exec	Total	Coverage
Date:	2021-05-22		Lines:	148190	205781	72.0 %
Legend:	low: < 75.0 % medium: >= 75.0 % high: >= 90.0 %		Branches:	277122	782144	35.4 %

File

Lines

Branches

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

40.0 %

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

351 / 570

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

100.0 %

21 / 21

59.4 %

38 / 64

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

95.4 %

62 / 65

63.6 %

227 / 357

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

45.7 %

59 / 129

23.5 %

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

97.3 %

182 / 187

48.9 %

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

90.5 %

134 / 148

52.4 %

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

42.5 %

65 / 153

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

100.0 %

139 / 139

54.8 %

266 / 485

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

100.0 %

23 / 23

80.0 %

8 / 10

build-coverage/src/expr/kind.cpp

55.7 %

389 / 699

54.8 %

377 / 688

build-coverage/src/expr/kind.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/src/expr/metakind.cpp

76.3 %

567 / 743

45.4 %

358 / 788

build-coverage/src/expr/metakind.h

100.0 %

12 / 12

10.8 %

474 / 4400

build-coverage/src/expr/type_checker.cpp

89.4 %

837 / 936

51.2 %

1132 / 2209

build-coverage/src/expr/type_properties.h

35.8 %

38 / 106

19.3 %

49 / 254

build-coverage/src/options/arith_options.cpp

28.2 %

136 / 483

6.8 %

9 / 133

build-coverage/src/options/arith_options.h

79.8 %

87 / 109

100.0 %

0 / 0

build-coverage/src/options/arrays_options.cpp

38.2 %

21 / 55

50.0 %

2 / 4

build-coverage/src/options/arrays_options.h

100.0 %

15 / 15

100.0 %

0 / 0

build-coverage/src/options/base_options.cpp

49.5 %

45 / 91

50.0 %

2 / 4

build-coverage/src/options/base_options.h

76.5 %

13 / 17

100.0 %

0 / 0

build-coverage/src/options/booleans_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/builtin_options.cpp

100.0 %

1 / 1

50.0 %

2 / 4

build-coverage/src/options/bv_options.cpp

38.0 %

93 / 245

23.0 %

23 / 100

build-coverage/src/options/bv_options.h

88.2 %

45 / 51

50.0 %

1 / 2

build-coverage/src/options/datatypes_options.cpp

34.5 %

50 / 145

20.6 %

7 / 34

build-coverage/src/options/datatypes_options.h

100.0 %

39 / 39

100.0 %

0 / 0

build-coverage/src/options/decision_options.cpp

23.5 %

20 / 85

9.1 %

5 / 55

build-coverage/src/options/decision_options.h

69.2 %

9 / 13

100.0 %

0 / 0

build-coverage/src/options/expr_options.cpp

57.9 %

11 / 19

50.0 %

2 / 4

build-coverage/src/options/expr_options.h

100.0 %

7 / 7

100.0 %

0 / 0

build-coverage/src/options/fp_options.cpp

42.9 %

3 / 7

50.0 %

2 / 4

build-coverage/src/options/fp_options.h

100.0 %

3 / 3

100.0 %

0 / 0

build-coverage/src/options/main_options.cpp

46.9 %

23 / 49

50.0 %

2 / 4

build-coverage/src/options/main_options.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/src/options/options.cpp

34.0 %

2705 / 7957

11.1 %

2896 / 26122

build-coverage/src/options/options.h

100.0 %

18 / 18

10.0 %

1 / 10

build-coverage/src/options/parser_options.cpp

35.1 %

13 / 37

50.0 %

2 / 4

build-coverage/src/options/parser_options.h

33.3 %

1 / 3

100.0 %

0 / 0

build-coverage/src/options/printer_options.cpp

16.4 %

11 / 67

8.7 %

4 / 46

build-coverage/src/options/printer_options.h

60.0 %

3 / 5

100.0 %

0 / 0

build-coverage/src/options/proof_options.cpp

21.5 %

17 / 79

3.6 %

2 / 55

build-coverage/src/options/proof_options.h

100.0 %

11 / 11

100.0 %

0 / 0

build-coverage/src/options/prop_options.cpp

41.8 %

23 / 55

50.0 %

2 / 4

build-coverage/src/options/prop_options.h

100.0 %

19 / 19

100.0 %

0 / 0

build-coverage/src/options/quantifiers_options.cpp

31.7 %

563 / 1775

4.9 %

34 / 691

build-coverage/src/options/quantifiers_options.h

94.6 %

353 / 373

100.0 %

0 / 0

build-coverage/src/options/resource_manager_options.cpp

35.5 %

11 / 31

50.0 %

2 / 4

build-coverage/src/options/resource_manager_options.h

100.0 %

1 / 1

100.0 %

0 / 0

build-coverage/src/options/sep_options.cpp

29.7 %

11 / 37

50.0 %

2 / 4

build-coverage/src/options/sep_options.h

100.0 %

11 / 11

100.0 %

0 / 0

build-coverage/src/options/sets_options.cpp

36.8 %

7 / 19

50.0 %

2 / 4

build-coverage/src/options/sets_options.h

100.0 %

7 / 7

100.0 %

0 / 0

build-coverage/src/options/smt_options.cpp

38.5 %

215 / 559

13.0 %

31 / 238

build-coverage/src/options/smt_options.h

92.1 %

93 / 101

100.0 %

0 / 0

build-coverage/src/options/strings_options.cpp

25.7 %

47 / 183

3.3 %

2 / 61

build-coverage/src/options/strings_options.h

100.0 %

41 / 41

100.0 %

0 / 0

build-coverage/src/options/theory_options.cpp

33.7 %

28 / 83

8.2 %

5 / 61

build-coverage/src/options/theory_options.h

100.0 %

13 / 13

100.0 %

0 / 0

build-coverage/src/options/uf_options.cpp

33.8 %

26 / 77

17.9 %

5 / 28

build-coverage/src/options/uf_options.h

100.0 %

15 / 15

100.0 %

0 / 0

build-coverage/src/parser/cvc/CvcLexer.c

45.9 %

3408 / 7418

37.2 %

1055 / 2838

build-coverage/src/parser/cvc/CvcParser.c

33.7 %

4627 / 13726

29.1 %

3790 / 13013

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

72.7 %

1958 / 2693

59.2 %

937 / 1584

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

72.5 %

3302 / 4554

45.3 %

2537 / 5595

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

76.9 %

1406 / 1828

55.7 %

494 / 887

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

63.5 %

3074 / 4839

42.5 %

2040 / 4805

build-coverage/src/theory/rewriter_tables.h

63.0 %

68 / 108

39.9 %

142 / 356

build-coverage/src/theory/theory_traits.h

97.6 %

41 / 42

65.0 %

13 / 20

build-coverage/src/theory/type_enumerator.cpp

83.8 %

31 / 37

40.4 %

42 / 104

build-coverage/src/util/floatingpoint_literal_symfpu.h

100.0 %

10 / 10

50.0 %

2 / 4

build-coverage/src/util/floatingpoint_literal_symfpu_traits.h

100.0 %

6 / 6

50.0 %

2 / 4

src/api/cpp/cvc5.cpp

75.9 %

2411 / 3175

27.3 %

6824 / 25004

src/api/cpp/cvc5.h

72.2 %

13 / 18

50.0 %

1 / 2

src/base/check.cpp

67.6 %

48 / 71

43.9 %

29 / 66

src/base/check.h

100.0 %

3 / 3

100.0 %

0 / 0

src/base/configuration.cpp

75.7 %

112 / 148

39.3 %

121 / 308

src/base/configuration.h

100.0 %

2 / 2

100.0 %

0 / 0

src/base/exception.cpp

72.8 %

59 / 81

36.2 %

42 / 116

src/base/exception.h

94.1 %

32 / 34

44.4 %

16 / 36

src/base/listener.cpp

100.0 %

2 / 2

100.0 %

0 / 0

src/base/map_util.h

100.0 %

16 / 16

40.7 %

74 / 182

src/base/modal_exception.h

66.7 %

6 / 9

100.0 %

0 / 0

src/base/output.cpp

100.0 %

13 / 13

50.0 %

3 / 6

src/base/output.h

81.3 %

104 / 128

15.9 %

142 / 894

src/context/backtrackable.h

4.9 %

2 / 41

1.2 %

1 / 84

src/context/cdhashmap.h

97.7 %

125 / 128

37.2 %

485 / 1303

src/context/cdhashset.h

88.1 %

37 / 42

11.4 %

5 / 44

src/context/cdinsert_hashmap.h

100.0 %

104 / 104

32.5 %

214 / 658

src/context/cdlist.h

95.8 %

138 / 144

37.0 %

921 / 2486

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

47.1 %

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

85.9 %

170 / 198

36.1 %

210 / 582

src/context/context.h

85.7 %

54 / 63

34.1 %

28 / 82

src/context/context_mm.cpp

93.5 %

58 / 62

36.0 %

36 / 100

src/decision/assertion_list.cpp

1.6 %

1 / 61

1.2 %

2 / 161

src/decision/assertion_list.h

0.0 %

0 / 1

100.0 %

0 / 0

src/decision/decision_engine.cpp

84.4 %

27 / 32

42.3 %

11 / 26

src/decision/decision_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/decision/decision_engine_old.cpp

79.5 %

31 / 39

31.9 %

51 / 160

src/decision/decision_engine_old.h

100.0 %

25 / 25

24.4 %

22 / 90

src/decision/decision_strategy.h

100.0 %

8 / 8

100.0 %

0 / 0

src/decision/justification_heuristic.cpp

72.5 %

274 / 378

32.1 %

484 / 1509

src/decision/justification_heuristic.h

0.0 %

0 / 3

0.0 %

0 / 6

src/decision/justify_info.cpp

5.0 %

1 / 20

6.7 %

2 / 30

src/decision/justify_stack.cpp

2.4 %

1 / 41

1.9 %

2 / 104

src/decision/justify_stats.cpp

6.3 %

1 / 16

7.1 %

2 / 28

src/expr/array_store_all.cpp

53.7 %

22 / 41

44.1 %

45 / 102

src/expr/ascription_type.cpp

57.9 %

11 / 19

31.8 %

7 / 22

src/expr/attribute.cpp

37.7 %

23 / 61

4.5 %

4 / 88

src/expr/attribute.h

76.0 %

95 / 125

46.4 %

555 / 1196

src/expr/attribute_internals.h

100.0 %

68 / 68

30.4 %

56 / 184

src/expr/attribute_unique_id.h

0.0 %

0 / 5

100.0 %

0 / 0

src/expr/bound_var_manager.cpp

63.2 %

12 / 19

29.4 %

10 / 34

src/expr/bound_var_manager.h

100.0 %

9 / 9

39.5 %

30 / 76

src/expr/buffered_proof_generator.cpp

75.0 %

33 / 44

34.8 %

55 / 158

src/expr/buffered_proof_generator.h

100.0 %

2 / 2

50.0 %

1 / 2

src/expr/datatype_index.cpp

66.7 %

4 / 6

50.0 %

4 / 8

src/expr/datatype_index.h

100.0 %

3 / 3

100.0 %

0 / 0

src/expr/dtype.cpp

87.7 %

415 / 473

36.0 %

718 / 1996

src/expr/dtype.h

50.0 %

1 / 2

45.0 %

18 / 40

src/expr/dtype_cons.cpp

93.2 %

315 / 338

37.7 %

492 / 1306

src/expr/dtype_cons.h

100.0 %

2 / 2

50.0 %

8 / 16

src/expr/dtype_selector.cpp

83.3 %

30 / 36

23.4 %

30 / 128

src/expr/dtype_selector.h

100.0 %

1 / 1

50.0 %

3 / 6

src/expr/emptybag.cpp

42.9 %

9 / 21

42.9 %

6 / 14

src/expr/emptyset.cpp

42.9 %

9 / 21

42.9 %

6 / 14

src/expr/expr_iomanip.cpp

81.5 %

44 / 54

54.2 %

13 / 24

src/expr/kind_map.h

100.0 %

8 / 8

66.7 %

4 / 6

src/expr/lazy_proof.cpp

96.9 %

94 / 97

48.0 %

169 / 352

src/expr/lazy_proof_chain.cpp

71.1 %

113 / 159

31.2 %

167 / 536

src/expr/match_trie.cpp

99.1 %

107 / 108

49.1 %

160 / 326

src/expr/match_trie.h

100.0 %

3 / 3

25.0 %

1 / 4

src/expr/node.cpp

84.0 %

42 / 50

50.9 %

115 / 226

src/expr/node.h

82.4 %

294 / 357

22.7 %

794 / 3500

src/expr/node_algorithm.cpp

84.9 %

321 / 378

49.4 %

517 / 1046

src/expr/node_builder.cpp

76.0 %

278 / 366

17.1 %

201 / 1176

src/expr/node_builder.h

100.0 %

8 / 8

25.0 %

24 / 96

src/expr/node_manager.cpp

85.4 %

497 / 582

36.6 %

649 / 1772

src/expr/node_manager.h

87.2 %

171 / 196

26.2 %

528 / 2014

src/expr/node_self_iterator.h

93.0 %

40 / 43

24.5 %

23 / 94

src/expr/node_traversal.cpp

100.0 %

60 / 60

50.5 %

53 / 105

src/expr/node_traversal.h

100.0 %

5 / 5

50.0 %

4 / 8

src/expr/node_trie.cpp

74.1 %

20 / 27

38.3 %

36 / 94

src/expr/node_trie.h

100.0 %

6 / 6

50.0 %

3 / 6

src/expr/node_value.cpp

33.3 %

11 / 33

15.9 %

13 / 82

src/expr/node_value.h

75.5 %

105 / 139

23.0 %

43 / 187

src/expr/node_visitor.h

100.0 %

33 / 33

50.0 %

89 / 178

src/expr/proof.cpp

80.2 %

170 / 212

42.4 %

391 / 922

src/expr/proof_checker.cpp

56.0 %

89 / 159

20.5 %

127 / 620

src/expr/proof_checker.h

80.0 %

4 / 5

100.0 %

0 / 0

src/expr/proof_ensure_closed.cpp

15.8 %

12 / 76

4.4 %

18 / 410

src/expr/proof_generator.cpp

11.5 %

3 / 26

1.7 %

2 / 120

src/expr/proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/proof_node.cpp

100.0 %

27 / 27

45.0 %

9 / 20

src/expr/proof_node.h

100.0 %

3 / 3

50.0 %

2 / 4

src/expr/proof_node_algorithm.cpp

72.0 %

54 / 75

36.4 %

59 / 162

src/expr/proof_node_manager.cpp

77.2 %

146 / 189

29.4 %

238 / 810

src/expr/proof_node_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/proof_node_to_sexpr.cpp

79.7 %

63 / 79

33.7 %

97 / 288

src/expr/proof_node_to_sexpr.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/proof_node_updater.cpp

77.2 %

98 / 127

36.9 %

130 / 352

src/expr/proof_node_updater.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/proof_rule.cpp

14.1 %

30 / 213

11.7 %

23 / 196

src/expr/proof_set.h

100.0 %

7 / 7

66.7 %

10 / 15

src/expr/proof_step_buffer.cpp

59.1 %

26 / 44

20.0 %

18 / 90

src/expr/proof_step_buffer.h

100.0 %

2 / 2

25.0 %

1 / 4

src/expr/sequence.cpp

55.0 %

105 / 191

20.7 %

117 / 564

src/expr/sequence.h

100.0 %

3 / 3

100.0 %

0 / 0

src/expr/skolem_manager.cpp

98.1 %

155 / 158

41.4 %

309 / 746

src/expr/skolem_manager.h

100.0 %

2 / 2

100.0 %

0 / 0

src/expr/subs.cpp

35.4 %

29 / 82

14.0 %

30 / 214

src/expr/subs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/sygus_datatype.cpp

100.0 %

44 / 44

31.0 %

39 / 126

src/expr/sygus_datatype.h

100.0 %

3 / 3

30.0 %

3 / 10

src/expr/symbol_manager.cpp

96.6 %

144 / 149

53.8 %

127 / 236

src/expr/symbol_table.cpp

84.0 %

194 / 231

38.2 %

188 / 492

src/expr/symbol_table.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/tconv_seq_proof_generator.cpp

70.5 %

55 / 78

23.0 %

70 / 304

src/expr/term_canonize.cpp

99.0 %

100 / 101

54.6 %

200 / 366

src/expr/term_canonize.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/term_context.cpp

71.7 %

38 / 53

55.6 %

30 / 54

src/expr/term_context.h

100.0 %

8 / 8

100.0 %

0 / 0

src/expr/term_context_node.cpp

13.3 %

4 / 30

4.3 %

6 / 140

src/expr/term_context_stack.cpp

72.2 %

26 / 36

28.4 %

38 / 134

src/expr/term_context_stack.h

100.0 %

1 / 1

100.0 %

0 / 0

src/expr/term_conversion_proof_generator.cpp

82.5 %

260 / 315

34.1 %

546 / 1599

src/expr/type_checker_util.h

75.0 %

36 / 48

11.1 %

164 / 1478

src/expr/type_matcher.cpp

95.2 %

59 / 62

53.2 %

84 / 158

src/expr/type_matcher.h

100.0 %

2 / 2

100.0 %

0 / 0

src/expr/type_node.cpp

85.5 %

282 / 330

37.4 %

383 / 1024

src/expr/type_node.h

85.1 %

165 / 194

21.2 %

154 / 727

src/expr/uninterpreted_constant.cpp

64.9 %

24 / 37

38.2 %

29 / 76

src/main/command_executor.cpp

74.7 %

74 / 99

53.8 %

113 / 210

src/main/command_executor.h

100.0 %

6 / 6

100.0 %

0 / 0

src/main/driver_unified.cpp

33.1 %

83 / 251

16.7 %

111 / 664

src/main/interactive_shell.cpp

67.0 %

59 / 88

34.9 %

103 / 295

src/main/main.cpp

87.5 %

14 / 16

49.2 %

31 / 63

src/main/main.h

100.0 %

1 / 1

100.0 %

0 / 0

src/main/signal_handlers.cpp

29.8 %

39 / 131

13.4 %

15 / 112

src/main/time_limit.cpp

72.7 %

16 / 22

29.2 %

7 / 24

src/omt/bitvector_optimizer.cpp

91.6 %

87 / 95

50.9 %

174 / 342

src/omt/bitvector_optimizer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/omt/integer_optimizer.cpp

96.0 %

24 / 25

41.9 %

31 / 74

src/omt/integer_optimizer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/omt/omt_optimizer.cpp

10.1 %

7 / 69

2.0 %

12 / 604

src/omt/omt_optimizer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/options/base_handlers.h

0.0 %

0 / 10

0.0 %

0 / 48

src/options/didyoumean.cpp

1.5 %

1 / 68

2.1 %

2 / 96

src/options/didyoumean.h

0.0 %

0 / 3

100.0 %

0 / 0

src/options/language.cpp

62.7 %

42 / 67

43.0 %

68 / 158

src/options/language.h

40.0 %

12 / 30

33.3 %

4 / 12

src/options/open_ostream.cpp

6.5 %

2 / 31

3.9 %

3 / 76

src/options/open_ostream.h

0.0 %

0 / 1

100.0 %

0 / 0

src/options/option_exception.cpp

100.0 %

2 / 2

50.0 %

3 / 6

src/options/option_exception.h

100.0 %

7 / 7

50.0 %

2 / 4

src/options/options_handler.cpp

38.6 %

108 / 280

21.2 %

143 / 676

src/options/options_handler.h

0.0 %

0 / 6

0.0 %

0 / 8

src/options/options_listener.h

100.0 %

2 / 2

100.0 %

0 / 0

src/options/options_public_functions.cpp

90.9 %

90 / 99

32.6 %

28 / 86

src/options/printer_modes.cpp

12.5 %

1 / 8

28.6 %

2 / 7

src/options/set_language.cpp

100.0 %

29 / 29

56.3 %

9 / 16

src/parser/antlr_input.cpp

94.6 %

209 / 221

50.0 %

234 / 468

src/parser/antlr_input.h

89.3 %

25 / 28

38.5 %

30 / 78

src/parser/antlr_input_imports.cpp

65.8 %

73 / 111

23.1 %

55 / 238

src/parser/antlr_line_buffered_input.cpp

67.0 %

59 / 88

17.0 %

15 / 88

src/parser/bounded_token_buffer.cpp

52.7 %

88 / 167

9.9 %

25 / 252

src/parser/bounded_token_factory.cpp

87.5 %

42 / 48

59.1 %

13 / 22

src/parser/cvc/cvc.cpp

100.0 %

10 / 10

50.0 %

9 / 18

src/parser/cvc/cvc.h

100.0 %

4 / 4

100.0 %

0 / 0

src/parser/cvc/cvc_input.cpp

91.7 %

22 / 24

25.0 %

14 / 56

src/parser/input.cpp

87.0 %

20 / 23

50.0 %

3 / 6

src/parser/input.h

77.8 %

7 / 9

50.0 %

1 / 2

src/parser/line_buffer.cpp

74.4 %

29 / 39

32.9 %

23 / 70

src/parser/memory_mapped_input_buffer.cpp

0.0 %

0 / 33

0.0 %

0 / 14

src/parser/parse_op.cpp

0.0 %

0 / 15

0.0 %

0 / 46

src/parser/parse_op.h

100.0 %

2 / 2

50.0 %

3 / 6

src/parser/parser.cpp

73.1 %

364 / 498

34.2 %

454 / 1329

src/parser/parser.h

69.7 %

23 / 33

16.7 %

1 / 6

src/parser/parser_builder.cpp

97.4 %

74 / 76

60.5 %

26 / 43

src/parser/parser_builder.h

100.0 %

1 / 1

100.0 %

0 / 0

src/parser/parser_exception.h

85.0 %

17 / 20

75.0 %

3 / 4

src/parser/smt2/smt2.cpp

87.5 %

590 / 674

47.4 %

979 / 2064

src/parser/smt2/smt2.h

66.7 %

22 / 33

36.5 %

27 / 74

src/parser/smt2/smt2_input.cpp

91.3 %

21 / 23

25.0 %

14 / 56

src/parser/smt2/sygus_input.cpp

83.3 %

20 / 24

25.0 %

14 / 56

src/parser/tptp/tptp.cpp

80.8 %

211 / 261

36.8 %

296 / 804

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

135 / 350

src/preprocessing/assertion_pipeline.h

100.0 %

14 / 14

100.0 %

4 / 4

src/preprocessing/passes/ackermann.cpp

97.3 %

108 / 111

41.3 %

217 / 526

src/preprocessing/passes/ackermann.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/apply_substs.cpp

100.0 %

21 / 21

55.6 %

30 / 54

src/preprocessing/passes/apply_substs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bool_to_bv.cpp

96.7 %

176 / 182

51.8 %

410 / 791

src/preprocessing/passes/bool_to_bv.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_abstraction.cpp

100.0 %

12 / 12

50.0 %

13 / 26

src/preprocessing/passes/bv_abstraction.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_eager_atoms.cpp

100.0 %

12 / 12

57.1 %

16 / 28

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

676 / 1688

src/preprocessing/passes/bv_gauss.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_intro_pow2.cpp

94.9 %

37 / 39

50.4 %

61 / 121

src/preprocessing/passes/bv_intro_pow2.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_to_bool.cpp

97.4 %

152 / 156

40.5 %

370 / 914

src/preprocessing/passes/bv_to_bool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/bv_to_int.cpp

89.4 %

421 / 471

41.3 %

844 / 2045

src/preprocessing/passes/bv_to_int.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/extended_rewriter_pass.cpp

100.0 %

9 / 9

46.4 %

13 / 28

src/preprocessing/passes/extended_rewriter_pass.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/foreign_theory_rewrite.cpp

98.1 %

52 / 53

37.7 %

92 / 244

src/preprocessing/passes/foreign_theory_rewrite.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/fun_def_fmf.cpp

94.8 %

220 / 232

47.5 %

462 / 972

src/preprocessing/passes/global_negate.cpp

98.0 %

48 / 49

51.2 %

85 / 166

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

708 / 1538

src/preprocessing/passes/ho_elim.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/int_to_bv.cpp

70.1 %

94 / 134

31.5 %

193 / 612

src/preprocessing/passes/int_to_bv.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ite_removal.cpp

100.0 %

22 / 22

44.8 %

26 / 58

src/preprocessing/passes/ite_removal.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ite_simp.cpp

49.2 %

59 / 120

15.1 %

67 / 444

src/preprocessing/passes/ite_simp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/miplib_trick.cpp

11.6 %

42 / 363

2.4 %

45 / 1842

src/preprocessing/passes/nl_ext_purify.cpp

98.3 %

57 / 58

58.5 %

110 / 188

src/preprocessing/passes/nl_ext_purify.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/non_clausal_simp.cpp

96.4 %

216 / 224

41.4 %

488 / 1178

src/preprocessing/passes/non_clausal_simp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/pseudo_boolean_processor.cpp

75.0 %

147 / 196

28.1 %

262 / 933

src/preprocessing/passes/pseudo_boolean_processor.h

100.0 %

3 / 3

57.1 %

8 / 14

src/preprocessing/passes/quantifiers_preprocess.cpp

100.0 %

15 / 15

52.0 %

26 / 50

src/preprocessing/passes/quantifiers_preprocess.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/real_to_int.cpp

95.8 %

92 / 96

48.1 %

224 / 466

src/preprocessing/passes/real_to_int.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/rewrite.cpp

100.0 %

7 / 7

50.0 %

8 / 16

src/preprocessing/passes/rewrite.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/sep_skolem_emp.cpp

96.1 %

49 / 51

50.5 %

93 / 184

src/preprocessing/passes/sep_skolem_emp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/sort_infer.cpp

100.0 %

36 / 36

54.0 %

54 / 100

src/preprocessing/passes/sort_infer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/static_learning.cpp

100.0 %

15 / 15

52.6 %

20 / 38

src/preprocessing/passes/static_learning.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/strings_eager_pp.cpp

100.0 %

19 / 19

54.5 %

24 / 44

src/preprocessing/passes/strings_eager_pp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/sygus_inference.cpp

95.7 %

155 / 162

48.7 %

301 / 618

src/preprocessing/passes/sygus_inference.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/synth_rew_rules.cpp

1.2 %

3 / 250

0.4 %

4 / 1002

src/preprocessing/passes/synth_rew_rules.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/theory_preprocess.cpp

100.0 %

19 / 19

44.2 %

23 / 52

src/preprocessing/passes/theory_preprocess.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/theory_rewrite_eq.cpp

100.0 %

53 / 53

46.2 %

109 / 236

src/preprocessing/passes/theory_rewrite_eq.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/unconstrained_simplifier.cpp

83.4 %

336 / 403

42.1 %

724 / 1719

src/preprocessing/passes/unconstrained_simplifier.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/preprocessing_pass.cpp

100.0 %

26 / 26

55.7 %

49 / 88

src/preprocessing/preprocessing_pass_context.cpp

90.0 %

27 / 30

42.9 %

12 / 28

src/preprocessing/preprocessing_pass_context.h

100.0 %

8 / 8

100.0 %

0 / 0

src/preprocessing/preprocessing_pass_registry.cpp

100.0 %

55 / 55

48.4 %

148 / 306

src/preprocessing/util/ite_utilities.cpp

46.5 %

458 / 986

21.1 %

780 / 3689

src/preprocessing/util/ite_utilities.h

18.6 %

8 / 43

9.1 %

4 / 44

src/printer/ast/ast_printer.cpp

17.4 %

39 / 224

17.4 %

45 / 258

src/printer/ast/ast_printer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/printer/cvc/cvc_printer.cpp

35.4 %

360 / 1016

22.6 %

473 / 2095

src/printer/cvc/cvc_printer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/printer/let_binding.cpp

98.1 %

103 / 105

46.4 %

169 / 364

src/printer/let_binding.h

100.0 %

1 / 1

100.0 %

0 / 0

src/printer/printer.cpp

24.4 %

52 / 213

18.8 %

57 / 304

src/printer/printer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/printer/smt2/smt2_printer.cpp

52.1 %

634 / 1218

31.6 %

1032 / 3262

src/printer/smt2/smt2_printer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/printer/tptp/tptp_printer.cpp

23.3 %

7 / 30

3.1 %

2 / 64

src/printer/tptp/tptp_printer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/dot/dot_printer.cpp

1.1 %

1 / 88

1.0 %

2 / 203

src/proof/unsat_core.cpp

82.6 %

19 / 23

42.9 %

18 / 42

src/proof/unsat_core.h

100.0 %

2 / 2

100.0 %

0 / 0

src/prop/bv_sat_solver_notify.h

100.0 %

2 / 2

100.0 %

0 / 0

src/prop/bvminisat/bvminisat.cpp

71.7 %

114 / 159

29.9 %

70 / 234

src/prop/bvminisat/bvminisat.h

86.7 %

13 / 15

0.0 %

0 / 6

src/prop/bvminisat/core/Solver.cc

80.0 %

521 / 651

41.0 %

579 / 1413

src/prop/bvminisat/core/Solver.h

83.6 %

61 / 73

52.3 %

45 / 86

src/prop/bvminisat/core/SolverTypes.h

94.7 %

124 / 131

36.5 %

62 / 170

src/prop/bvminisat/mtl/Alg.h

100.0 %

11 / 11

45.5 %

25 / 55

src/prop/bvminisat/mtl/Alloc.h

95.7 %

45 / 47

19.4 %

21 / 108

src/prop/bvminisat/mtl/Heap.h

89.6 %

69 / 77

28.2 %

35 / 124

src/prop/bvminisat/mtl/Queue.h

96.4 %

27 / 28

26.9 %

21 / 78

src/prop/bvminisat/mtl/Sort.h

100.0 %

27 / 27

93.8 %

30 / 32

src/prop/bvminisat/mtl/Vec.h

97.8 %

45 / 46

39.2 %

134 / 342

src/prop/bvminisat/mtl/XAlloc.h

80.0 %

4 / 5

25.0 %

1 / 4

src/prop/bvminisat/simp/SimpSolver.cc

73.9 %

300 / 406

38.0 %

370 / 974

src/prop/bvminisat/simp/SimpSolver.h

89.5 %

17 / 19

47.1 %

16 / 34

src/prop/bvminisat/utils/Options.h

23.9 %

22 / 92

5.6 %

4 / 72

src/prop/bvminisat/utils/ParseUtils.h

0.0 %

0 / 6

0.0 %

0 / 4

src/prop/cadical.cpp

64.7 %

55 / 85

21.5 %

31 / 144

src/prop/cnf_stream.cpp

93.1 %

367 / 394

37.3 %

709 / 1902

src/prop/cnf_stream.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/cryptominisat.cpp

64.8 %

70 / 108

27.5 %

56 / 204

src/prop/cryptominisat.h

0.0 %

0 / 1

100.0 %

0 / 0

src/prop/minisat/core/Solver.cc

83.3 %

854 / 1025

42.0 %

1180 / 2808

src/prop/minisat/core/Solver.h

94.7 %

108 / 114

44.1 %

98 / 222

src/prop/minisat/core/SolverTypes.h

87.5 %

140 / 160

35.3 %

67 / 190

src/prop/minisat/minisat.cpp

78.4 %

138 / 176

31.8 %

100 / 314

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

418 / 1072

src/prop/minisat/simp/SimpSolver.h

86.2 %

25 / 29

50.0 %

20 / 40

src/prop/minisat/utils/Options.h

23.9 %

22 / 92

5.6 %

4 / 72

src/prop/minisat/utils/ParseUtils.h

0.0 %

0 / 6

0.0 %

0 / 4

src/prop/proof_cnf_stream.cpp

93.7 %

580 / 619

45.0 %

1499 / 3332

src/prop/proof_cnf_stream.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/proof_post_processor.cpp

90.9 %

40 / 44

33.1 %

51 / 154

src/prop/proof_post_processor.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/prop_engine.cpp

72.4 %

247 / 341

30.0 %

361 / 1202

src/prop/prop_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/prop_proof_manager.cpp

38.0 %

19 / 50

10.4 %

19 / 182

src/prop/prop_proof_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/registrar.h

100.0 %

4 / 4

100.0 %

0 / 0

src/prop/sat_proof_manager.cpp

72.1 %

305 / 423

30.1 %

632 / 2098

src/prop/sat_proof_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/sat_solver.h

15.0 %

6 / 40

0.0 %

0 / 30

src/prop/sat_solver_factory.cpp

86.7 %

13 / 15

30.0 %

6 / 20

src/prop/sat_solver_types.cpp

33.3 %

1 / 3

50.0 %

2 / 4

src/prop/sat_solver_types.h

87.9 %

29 / 33

31.3 %

5 / 16

src/prop/skolem_def_manager.cpp

84.3 %

70 / 83

37.1 %

92 / 248

src/prop/theory_proxy.cpp

94.2 %

97 / 103

42.1 %

138 / 328

src/smt/abduction_solver.cpp

83.8 %

83 / 99

37.4 %

166 / 444

src/smt/abstract_values.cpp

100.0 %

16 / 16

37.9 %

25 / 66

src/smt/assertions.cpp

87.9 %

80 / 91

45.2 %

103 / 228

src/smt/check_models.cpp

65.1 %

28 / 43

27.7 %

51 / 184

src/smt/command.cpp

54.3 %

687 / 1266

32.4 %

502 / 1551

src/smt/command.h

79.5 %

62 / 78

25.0 %

4 / 16

src/smt/dump.cpp

70.3 %

52 / 74

36.2 %

47 / 130

100.0 %

10 / 10

57.1 %

16 / 28

src/smt/dump_manager.cpp

100.0 %

26 / 26

56.0 %

28 / 50

src/smt/env.cpp

97.6 %

41 / 42

31.9 %

23 / 72

100.0 %

2 / 2

100.0 %

0 / 0

src/smt/expand_definitions.cpp

98.6 %

69 / 70

46.0 %

126 / 274

src/smt/interpolation_solver.cpp

79.3 %

46 / 58

39.8 %

86 / 216

src/smt/listeners.cpp

83.7 %

36 / 43

34.2 %

41 / 120

src/smt/listeners.h

100.0 %

3 / 3

100.0 %

0 / 0

src/smt/logic_exception.h

100.0 %

7 / 7

100.0 %

0 / 0

src/smt/managed_ostreams.cpp

30.7 %

27 / 88

20.3 %

26 / 128

src/smt/managed_ostreams.h

40.0 %

4 / 10

0.0 %

0 / 2

src/smt/model.cpp

100.0 %

24 / 24

27.5 %

11 / 40

src/smt/model.h

33.3 %

1 / 3

100.0 %

0 / 0

src/smt/model_blocker.cpp

84.7 %

122 / 144

36.4 %

279 / 766

src/smt/model_core_builder.cpp

2.0 %

1 / 50

1.1 %

2 / 182

src/smt/node_command.cpp

50.0 %

28 / 56

18.2 %

16 / 88

src/smt/node_command.h

100.0 %

5 / 5

8.8 %

3 / 34

src/smt/optimization_solver.cpp

100.0 %

35 / 35

37.8 %

34 / 90

src/smt/optimization_solver.h

95.0 %

19 / 20

100.0 %

0 / 0

src/smt/options_manager.cpp

77.0 %

47 / 61

37.7 %

80 / 212

src/smt/output_manager.cpp

100.0 %

5 / 5

50.0 %

2 / 4

src/smt/preprocess_proof_generator.cpp

92.5 %

99 / 107

42.5 %

209 / 492

src/smt/preprocess_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/preprocessor.cpp

94.8 %

55 / 58

39.2 %

51 / 130

src/smt/process_assertions.cpp

92.9 %

171 / 184

49.3 %

378 / 766

src/smt/proof_manager.cpp

77.3 %

68 / 88

30.6 %

101 / 330

src/smt/proof_post_processor.cpp

91.4 %

545 / 596

37.9 %

1058 / 2788

src/smt/proof_post_processor.h

100.0 %

2 / 2

100.0 %

0 / 0

src/smt/quant_elim_solver.cpp

91.7 %

55 / 60

42.5 %

136 / 320

src/smt/set_defaults.cpp

82.7 %

586 / 709

49.6 %

1811 / 3650

src/smt/smt_engine.cpp

82.5 %

824 / 999

37.4 %

1236 / 3303

src/smt/smt_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/smt_engine_scope.cpp

100.0 %

21 / 21

22.2 %

16 / 72

src/smt/smt_engine_state.cpp

89.4 %

126 / 141

36.4 %

92 / 253

src/smt/smt_engine_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt/smt_engine_stats.cpp

100.0 %

18 / 18

50.0 %

13 / 26

src/smt/smt_mode.cpp

8.3 %

1 / 12

16.7 %

2 / 12

src/smt/smt_solver.cpp

89.7 %

96 / 107

46.9 %

149 / 318

src/smt/smt_statistics_registry.cpp

100.0 %

3 / 3

50.0 %

2 / 4

src/smt/smt_statistics_registry.h

100.0 %

1 / 1

33.3 %

2 / 6

src/smt/sygus_solver.cpp

88.2 %

180 / 204

45.2 %

333 / 736

src/smt/term_formula_removal.cpp

96.9 %

218 / 225

49.0 %

443 / 904

src/smt/unsat_core_manager.cpp

93.2 %

41 / 44

36.6 %

60 / 164

src/smt/unsat_core_manager.h

100.0 %

2 / 2

100.0 %

0 / 0

src/smt/update_ostream.h

2.4 %

1 / 41

0.0 %

0 / 38

src/smt/witness_form.cpp

69.8 %

44 / 63

26.6 %

77 / 290

src/smt/witness_form.h

100.0 %

1 / 1

100.0 %

0 / 0

src/smt_util/boolean_simplification.cpp

55.6 %

15 / 27

37.3 %

38 / 102

src/smt_util/boolean_simplification.h

79.4 %

54 / 68

39.4 %

74 / 188

src/smt_util/nary_builder.cpp

11.1 %

11 / 99

3.5 %

11 / 315

src/theory/arith/approx_simplex.cpp

2.8 %

4 / 145

0.5 %

2 / 427

src/theory/arith/approx_simplex.h

0.0 %

0 / 3

100.0 %

0 / 0

src/theory/arith/arith_ite_utils.cpp

0.4 %

1 / 279

0.1 %

2 / 1342

src/theory/arith/arith_msum.cpp

90.3 %

130 / 144

50.9 %

327 / 642

src/theory/arith/arith_msum.h

100.0 %

2 / 2

55.0 %

11 / 20

src/theory/arith/arith_preprocess.cpp

25.0 %

7 / 28

5.1 %

4 / 78

src/theory/arith/arith_preprocess.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/arith_rewriter.cpp

88.1 %

443 / 503

41.9 %

1023 / 2443

src/theory/arith/arith_rewriter.h

100.0 %

3 / 3

25.0 %

1 / 4

src/theory/arith/arith_state.cpp

100.0 %

7 / 7

60.0 %

6 / 10

src/theory/arith/arith_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/arith_static_learner.cpp

87.2 %

136 / 156

41.5 %

376 / 907

src/theory/arith/arith_utilities.cpp

78.9 %

127 / 161

35.2 %

230 / 654

src/theory/arith/arith_utilities.h

66.7 %

74 / 111

37.4 %

52 / 139

src/theory/arith/arithvar.cpp

100.0 %

4 / 4

50.0 %

3 / 6

src/theory/arith/attempt_solution_simplex.cpp

15.6 %

12 / 77

3.5 %

10 / 288

src/theory/arith/attempt_solution_simplex.h

16.7 %

1 / 6

29.3 %

17 / 58

src/theory/arith/bound_counts.h

85.6 %

83 / 97

29.6 %

48 / 162

src/theory/arith/bound_inference.cpp

61.0 %

83 / 136

36.5 %

166 / 455

src/theory/arith/bound_inference.h

100.0 %

2 / 2

33.3 %

10 / 30

src/theory/arith/callbacks.cpp

87.7 %

100 / 114

24.0 %

112 / 466

src/theory/arith/callbacks.h

100.0 %

13 / 13

25.0 %

2 / 8

src/theory/arith/congruence_manager.cpp

88.5 %

355 / 401

38.0 %

715 / 1884

src/theory/arith/congruence_manager.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/arith/constraint.cpp

72.8 %

1072 / 1472

28.1 %

1804 / 6411

src/theory/arith/constraint.h

95.0 %

114 / 120

17.6 %

42 / 238

src/theory/arith/cut_log.cpp

0.2 %

1 / 405

0.2 %

2 / 850

src/theory/arith/cut_log.h

0.0 %

0 / 7

0.0 %

0 / 6

src/theory/arith/delta_rational.cpp

50.0 %

26 / 52

17.6 %

37 / 210

src/theory/arith/delta_rational.h

88.0 %

81 / 92

57.0 %

49 / 86

src/theory/arith/dio_solver.cpp

87.2 %

422 / 484

35.4 %

833 / 2350

src/theory/arith/dio_solver.h

76.9 %

30 / 39

16.1 %

18 / 112

src/theory/arith/dual_simplex.cpp

90.8 %

109 / 120

37.6 %

212 / 564

src/theory/arith/dual_simplex.h

100.0 %

8 / 8

100.0 %

0 / 0

src/theory/arith/error_set.cpp

64.0 %

197 / 308

26.6 %

167 / 627

src/theory/arith/error_set.h

51.1 %

47 / 92

8.7 %

12 / 138

src/theory/arith/fc_simplex.cpp

4.3 %

21 / 487

0.7 %

16 / 2152

src/theory/arith/fc_simplex.h

5.1 %

2 / 39

0.0 %

0 / 26

src/theory/arith/infer_bounds.cpp

24.1 %

33 / 137

3.2 %

7 / 217

src/theory/arith/infer_bounds.h

0.0 %

0 / 2

100.0 %

0 / 0

src/theory/arith/inference_manager.cpp

73.8 %

48 / 65

32.9 %

48 / 146

src/theory/arith/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/linear_equality.cpp

45.7 %

368 / 806

18.8 %

624 / 3318

src/theory/arith/linear_equality.h

26.2 %

48 / 183

4.2 %

19 / 454

src/theory/arith/matrix.cpp

50.0 %

2 / 4

50.0 %

2 / 4

src/theory/arith/matrix.h

76.6 %

307 / 401

22.6 %

252 / 1116

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

84.1 %

228 / 271

42.7 %

395 / 924

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

40.8 %

187 / 458

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

57.7 %

15 / 26

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

100.0 %

2 / 2

100.0 %

0 / 0

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

66.7 %

28 / 42

33.0 %

31 / 94

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

33.3 %

2 / 6

0.0 %

0 / 4

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

93.8 %

15 / 16

32.8 %

21 / 64

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

100.0 %

2 / 2

100.0 %

0 / 0

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

83.3 %

70 / 84

37.1 %

103 / 278

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

59.1 %

52 / 88

26.2 %

86 / 328

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

96.4 %

53 / 55

48.3 %

87 / 180

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

100.0 %

2 / 2

50.0 %

1 / 2

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

100.0 %

46 / 46

49.4 %

82 / 166

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

100.0 %

1 / 1

100.0 %

0 / 0

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

99.1 %

109 / 110

54.4 %

224 / 412

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

100.0 %

1 / 1

100.0 %

0 / 0

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

96.4 %

162 / 168

48.1 %

251 / 522

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

100.0 %

2 / 2

100.0 %

0 / 0

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

57.1 %

168 / 294

29.5 %

353 / 1198

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

100.0 %

1 / 1

100.0 %

0 / 0

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

97.0 %

359 / 370

50.4 %

748 / 1484

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

100.0 %

1 / 1

100.0 %

0 / 0

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

93.1 %

81 / 87

30.5 %

219 / 718

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

100.0 %

2 / 2

20.0 %

2 / 10

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

23.5 %

4 / 17

4.2 %

2 / 48

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

100.0 %

1 / 1

100.0 %

0 / 0

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

98.6 %

72 / 73

53.7 %

189 / 352

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

100.0 %

1 / 1

75.0 %

3 / 4

src/theory/arith/nl/ext_theory_callback.cpp

92.5 %

49 / 53

48.5 %

95 / 196

src/theory/arith/nl/ext_theory_callback.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/iand_solver.cpp

76.3 %

116 / 152

34.7 %

257 / 740

src/theory/arith/nl/iand_utils.cpp

93.7 %

104 / 111

40.3 %

166 / 412

src/theory/arith/nl/iand_utils.h

100.0 %

1 / 1

100.0 %

0 / 0

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

70.4 %

38 / 54

38.8 %

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

45 / 136

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

100.0 %

2 / 2

100.0 %

0 / 0

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

79.0 %

158 / 200

40.6 %

249 / 613

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

100.0 %

11 / 11

50.0 %

2 / 4

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

39.4 %

41 / 104

21.1 %

78 / 370

src/theory/arith/nl/nl_lemma_utils.cpp

75.0 %

21 / 28

41.7 %

20 / 48

src/theory/arith/nl/nl_lemma_utils.h

94.7 %

18 / 19

37.5 %

3 / 8

src/theory/arith/nl/nl_model.cpp

80.1 %

597 / 745

39.3 %

1394 / 3549

src/theory/arith/nl/nonlinear_extension.cpp

89.3 %

285 / 319

50.4 %

487 / 966

src/theory/arith/nl/nonlinear_extension.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/poly_conversion.cpp

39.5 %

157 / 397

14.7 %

255 / 1738

src/theory/arith/nl/poly_conversion.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/stats.cpp

100.0 %

5 / 5

50.0 %

6 / 12

src/theory/arith/nl/strategy.cpp

61.8 %

63 / 102

41.5 %

118 / 284

src/theory/arith/nl/strategy.h

100.0 %

4 / 4

100.0 %

0 / 0

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

93.4 %

113 / 121

45.8 %

248 / 542

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

99.2 %

260 / 262

32.6 %

744 / 2284

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

100.0 %

2 / 2

100.0 %

0 / 0

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

99.1 %

223 / 225

47.7 %

547 / 1146

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

85.7 %

24 / 28

75.0 %

12 / 16

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

93.7 %

118 / 126

43.1 %

238 / 552

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

100.0 %

2 / 2

30.0 %

3 / 10

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

86.1 %

179 / 208

41.9 %

347 / 829

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

93.8 %

181 / 193

46.3 %

493 / 1064

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

100.0 %

1 / 1

75.0 %

3 / 4

src/theory/arith/normal_form.cpp

81.0 %

642 / 793

36.9 %

1091 / 2958

src/theory/arith/normal_form.h

98.2 %

374 / 381

38.0 %

419 / 1104

src/theory/arith/operator_elim.cpp

93.3 %

182 / 195

49.3 %

490 / 994

src/theory/arith/operator_elim.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/partial_model.cpp

78.8 %

320 / 406

33.6 %

294 / 874

src/theory/arith/partial_model.h

100.0 %

34 / 34

50.0 %

1 / 2

src/theory/arith/proof_checker.cpp

68.3 %

127 / 186

27.9 %

261 / 934

src/theory/arith/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arith/rewrites.cpp

5.6 %

1 / 18

12.5 %

2 / 16

src/theory/arith/simplex.cpp

35.8 %

58 / 162

13.9 %

82 / 592

src/theory/arith/simplex.h

15.4 %

2 / 13

0.0 %

0 / 2

src/theory/arith/simplex_update.cpp

0.9 %

1 / 116

0.6 %

2 / 321

src/theory/arith/simplex_update.h

0.0 %

0 / 57

0.0 %

0 / 102

src/theory/arith/soi_simplex.cpp

4.2 %

23 / 543

0.8 %

20 / 2402

src/theory/arith/soi_simplex.h

11.8 %

2 / 17

0.0 %

0 / 10

src/theory/arith/tableau.cpp

69.7 %

76 / 109

23.8 %

117 / 492

src/theory/arith/tableau.h

54.5 %

18 / 33

8.3 %

3 / 36

src/theory/arith/tableau_sizes.cpp

20.0 %

1 / 5

50.0 %

2 / 4

src/theory/arith/tableau_sizes.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/theory_arith.cpp

99.2 %

130 / 131

46.5 %

175 / 376

src/theory/arith/theory_arith.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/arith/theory_arith_private.cpp

59.9 %

1805 / 3013

27.8 %

3614 / 12992

src/theory/arith/theory_arith_private.h

85.3 %

29 / 34

35.7 %

15 / 42

src/theory/arith/theory_arith_type_rules.cpp

85.7 %

54 / 63

36.0 %

73 / 203

src/theory/arith/type_enumerator.h

100.0 %

37 / 37

44.0 %

51 / 116

src/theory/arrays/array_info.cpp

67.2 %

203 / 302

30.4 %

292 / 962

src/theory/arrays/array_info.h

100.0 %

14 / 14

39.3 %

22 / 56

src/theory/arrays/inference_manager.cpp

86.0 %

49 / 57

38.6 %

78 / 202

src/theory/arrays/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arrays/proof_checker.cpp

67.2 %

41 / 61

22.7 %

103 / 454

src/theory/arrays/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arrays/skolem_cache.cpp

95.8 %

23 / 24

31.8 %

56 / 176

src/theory/arrays/theory_arrays.cpp

72.0 %

867 / 1204

36.2 %

2347 / 6475

src/theory/arrays/theory_arrays.h

97.5 %

39 / 40

55.7 %

59 / 106

src/theory/arrays/theory_arrays_rewriter.cpp

98.6 %

341 / 346

53.2 %

832 / 1565

src/theory/arrays/theory_arrays_rewriter.h

100.0 %

3 / 3

33.3 %

4 / 12

src/theory/arrays/theory_arrays_type_rules.cpp

66.4 %

89 / 134

26.3 %

173 / 658

src/theory/arrays/type_enumerator.h

91.3 %

63 / 69

49.0 %

99 / 202

src/theory/arrays/union_find.cpp

7.7 %

1 / 13

1.4 %

2 / 142

src/theory/assertion.cpp

33.3 %

1 / 3

33.3 %

2 / 6

src/theory/assertion.h

83.3 %

5 / 6

100.0 %

0 / 0

src/theory/atom_requests.cpp

87.1 %

27 / 31

40.2 %

45 / 112

src/theory/atom_requests.h

100.0 %

13 / 13

75.0 %

3 / 4

src/theory/bags/bag_solver.cpp

92.8 %

103 / 111

39.3 %

159 / 405

src/theory/bags/bags_rewriter.cpp

94.5 %

207 / 219

46.0 %

827 / 1797

src/theory/bags/bags_rewriter.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/bags/bags_statistics.cpp

100.0 %

5 / 5

50.0 %

4 / 8

src/theory/bags/infer_info.cpp

43.8 %

14 / 32

16.4 %

20 / 122

src/theory/bags/infer_info.h

100.0 %

2 / 2

50.0 %

3 / 6

src/theory/bags/inference_generator.cpp

90.3 %

139 / 154

32.3 %

301 / 932

src/theory/bags/inference_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/inference_manager.cpp

80.0 %

12 / 15

46.4 %

13 / 28

src/theory/bags/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/make_bag_op.cpp

84.6 %

11 / 13

42.9 %

6 / 14

src/theory/bags/make_bag_op.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/normal_form.cpp

93.1 %

243 / 261

43.0 %

556 / 1292

src/theory/bags/rewrites.cpp

2.0 %

1 / 49

4.5 %

2 / 44

src/theory/bags/solver_state.cpp

100.0 %

69 / 69

48.4 %

123 / 254

src/theory/bags/solver_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/term_registry.cpp

41.7 %

5 / 12

14.3 %

4 / 28

src/theory/bags/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bags/theory_bags.cpp

90.1 %

109 / 121

40.5 %

161 / 398

src/theory/bags/theory_bags.h

80.0 %

4 / 5

0.0 %

0 / 2

src/theory/bags/theory_bags_type_enumerator.cpp

3.1 %

1 / 32

1.9 %

2 / 106

src/theory/bags/theory_bags_type_rules.cpp

72.4 %

92 / 127

26.2 %

179 / 684

src/theory/bags/theory_bags_type_rules.h

0.0 %

0 / 2

100.0 %

0 / 0

src/theory/booleans/circuit_propagator.cpp

93.0 %

348 / 374

48.9 %

871 / 1782

src/theory/booleans/circuit_propagator.h

100.0 %

29 / 29

52.0 %

52 / 100

src/theory/booleans/proof_checker.cpp

78.5 %

419 / 534

28.0 %

932 / 3332

src/theory/booleans/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/booleans/proof_circuit_propagator.cpp

91.6 %

228 / 249

49.5 %

544 / 1098

src/theory/booleans/proof_circuit_propagator.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/booleans/theory_bool.cpp

90.9 %

20 / 22

48.5 %

33 / 68

src/theory/booleans/theory_bool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/booleans/theory_bool_rewriter.cpp

96.5 %

221 / 229

55.3 %

866 / 1565

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

52.9 %

74 / 140

src/theory/booleans/type_enumerator.h

100.0 %

19 / 19

40.0 %

14 / 35

src/theory/builtin/proof_checker.cpp

70.8 %

199 / 281

31.9 %

346 / 1086

src/theory/builtin/proof_checker.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/builtin/theory_builtin.cpp

81.8 %

9 / 11

35.7 %

5 / 14

src/theory/builtin/theory_builtin.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/builtin/theory_builtin_rewriter.cpp

90.0 %

225 / 250

42.5 %

655 / 1541

src/theory/builtin/theory_builtin_rewriter.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/builtin/theory_builtin_type_rules.cpp

100.0 %

9 / 9

35.7 %

15 / 42

src/theory/builtin/theory_builtin_type_rules.h

75.8 %

72 / 95

38.3 %

163 / 426

src/theory/builtin/type_enumerator.cpp

6.7 %

1 / 15

3.6 %

2 / 56

src/theory/builtin/type_enumerator.h

88.9 %

24 / 27

41.7 %

35 / 84

src/theory/bv/abstraction.cpp

26.4 %

165 / 626

9.8 %

270 / 2750

src/theory/bv/abstraction.h

22.9 %

8 / 35

4.0 %

2 / 50

src/theory/bv/bitblast/bitblast_strategies_template.h

80.0 %

364 / 455

29.0 %

699 / 2412

src/theory/bv/bitblast/bitblast_utils.h

88.9 %

96 / 108

37.7 %

144 / 382

src/theory/bv/bitblast/bitblaster.h

95.3 %

102 / 107

40.8 %

107 / 262

src/theory/bv/bitblast/eager_bitblaster.cpp

90.1 %

118 / 131

34.8 %

198 / 569

src/theory/bv/bitblast/eager_bitblaster.h

75.0 %

3 / 4

50.0 %

1 / 2

src/theory/bv/bitblast/lazy_bitblaster.cpp

68.8 %

209 / 304

31.3 %

346 / 1105

src/theory/bv/bitblast/lazy_bitblaster.h

57.1 %

4 / 7

100.0 %

0 / 0

src/theory/bv/bitblast/proof_bitblaster.cpp

60.3 %

44 / 73

25.6 %

67 / 262

src/theory/bv/bitblast/simple_bitblaster.cpp

87.1 %

61 / 70

37.0 %

100 / 270

src/theory/bv/bitblast/simple_bitblaster.h

50.0 %

1 / 2

0.0 %

0 / 4

src/theory/bv/bv_eager_solver.cpp

84.8 %

39 / 46

26.0 %

52 / 200

src/theory/bv/bv_inequality_graph.cpp

94.7 %

284 / 300

40.9 %

510 / 1247

src/theory/bv/bv_inequality_graph.h

100.0 %

41 / 41

28.0 %

23 / 82

src/theory/bv/bv_quick_check.cpp

0.5 %

1 / 189

0.6 %

2 / 348

src/theory/bv/bv_quick_check.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/bv/bv_solver.h

61.5 %

16 / 26

0.0 %

0 / 8

src/theory/bv/bv_solver_bitblast.cpp

0.5 %

1 / 185

0.3 %

2 / 778

src/theory/bv/bv_solver_bitblast.h

0.0 %

0 / 4

0.0 %

0 / 2

src/theory/bv/bv_solver_lazy.cpp

88.6 %

295 / 333

44.9 %

611 / 1360

src/theory/bv/bv_solver_lazy.h

95.0 %

19 / 20

33.3 %

14 / 42

src/theory/bv/bv_solver_simple.cpp

86.7 %

52 / 60

47.8 %

88 / 184

src/theory/bv/bv_solver_simple.h

66.7 %

2 / 3

0.0 %

0 / 2

src/theory/bv/bv_subtheory.h

36.7 %

11 / 30

20.0 %

7 / 35

src/theory/bv/bv_subtheory_algebraic.cpp

0.3 %

2 / 600

0.1 %

3 / 2425

src/theory/bv/bv_subtheory_algebraic.h

0.0 %

0 / 18

0.0 %

0 / 10

src/theory/bv/bv_subtheory_bitblast.cpp

69.7 %

99 / 142

37.6 %

182 / 484

src/theory/bv/bv_subtheory_bitblast.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/bv/bv_subtheory_core.cpp

85.4 %

263 / 308

45.3 %

538 / 1187

src/theory/bv/bv_subtheory_core.h

100.0 %

8 / 8

100.0 %

0 / 0

src/theory/bv/bv_subtheory_inequality.cpp

77.7 %

108 / 139

39.8 %

255 / 640

src/theory/bv/bv_subtheory_inequality.h

100.0 %

6 / 6

50.0 %

5 / 10

src/theory/bv/proof_checker.cpp

54.8 %

46 / 84

1.1 %

2 / 186

src/theory/bv/proof_checker.h

100.0 %

2 / 2

0.0 %

0 / 4

src/theory/bv/slicer.cpp

3.1 %

1 / 32

3.1 %

2 / 64

src/theory/bv/slicer.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/bv/theory_bv.cpp

92.6 %

113 / 122

47.3 %

186 / 393

src/theory/bv/theory_bv.h

0.0 %

0 / 1

0.0 %

0 / 2

src/theory/bv/theory_bv_rewrite_rules.h

29.2 %

74 / 253

23.6 %

5145 / 21799

src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h

88.3 %

136 / 154

44.6 %

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

92.3 %

670 / 726

47.7 %

1392 / 2919

src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h

75.8 %

270 / 356

34.3 %

441 / 1284

src/theory/bv/theory_bv_rewrite_rules_simplification.h

89.6 %

669 / 747

45.9 %

1968 / 4290

src/theory/bv/theory_bv_rewriter.cpp

95.7 %

315 / 329

50.9 %

475 / 934

src/theory/bv/theory_bv_rewriter.h

100.0 %

1 / 1

0.0 %

0 / 2

src/theory/bv/theory_bv_type_rules.cpp

72.8 %

99 / 136

29.6 %

145 / 490

src/theory/bv/theory_bv_type_rules.h

0.0 %

0 / 6

0.0 %

0 / 20

src/theory/bv/theory_bv_utils.cpp

91.6 %

218 / 238

42.0 %

341 / 812

src/theory/bv/theory_bv_utils.h

100.0 %

18 / 18

40.2 %

41 / 102

src/theory/bv/type_enumerator.h

100.0 %

13 / 13

55.0 %

11 / 20

src/theory/care_graph.h

100.0 %

10 / 10

83.3 %

15 / 18

src/theory/combination_care_graph.cpp

100.0 %

33 / 33

52.2 %

48 / 92

src/theory/combination_engine.cpp

95.2 %

40 / 42

27.7 %

26 / 94

src/theory/datatypes/datatypes_rewriter.cpp

93.8 %

480 / 512

46.1 %

1070 / 2319

src/theory/datatypes/datatypes_rewriter.h

100.0 %

1 / 1

43.8 %

7 / 16

src/theory/datatypes/infer_proof_cons.cpp

80.4 %

115 / 143

34.8 %

311 / 893

src/theory/datatypes/infer_proof_cons.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/inference.cpp

75.0 %

18 / 24

35.5 %

39 / 110

src/theory/datatypes/inference.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/inference_manager.cpp

100.0 %

62 / 62

54.5 %

133 / 244

src/theory/datatypes/proof_checker.cpp

80.6 %

58 / 72

26.8 %

126 / 470

src/theory/datatypes/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/datatypes/sygus_datatype_utils.cpp

87.9 %

298 / 339

39.7 %

613 / 1544

src/theory/datatypes/sygus_extension.cpp

85.0 %

857 / 1008

40.2 %

1996 / 4968

src/theory/datatypes/sygus_extension.h

100.0 %

5 / 5

50.0 %

1 / 2

src/theory/datatypes/sygus_simple_sym.cpp

92.9 %

261 / 281

50.9 %

563 / 1106

src/theory/datatypes/sygus_simple_sym.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/theory_datatypes.cpp

88.4 %

999 / 1130

45.3 %

2313 / 5110

src/theory/datatypes/theory_datatypes.h

88.2 %

15 / 17

47.5 %

19 / 40

src/theory/datatypes/theory_datatypes_type_rules.cpp

77.9 %

218 / 280

32.7 %

447 / 1366

src/theory/datatypes/theory_datatypes_utils.cpp

83.8 %

83 / 99

41.5 %

188 / 453

src/theory/datatypes/tuple_project_op.cpp

100.0 %

16 / 16

62.5 %

10 / 16

src/theory/datatypes/tuple_project_op.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/datatypes/type_enumerator.cpp

100.0 %

168 / 168

48.6 %

389 / 800

src/theory/datatypes/type_enumerator.h

100.0 %

49 / 49

54.3 %

50 / 92

src/theory/decision_manager.cpp

100.0 %

47 / 47

52.9 %

72 / 136

src/theory/decision_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/decision_strategy.cpp

95.2 %

59 / 62

53.1 %

85 / 160

src/theory/decision_strategy.h

100.0 %

5 / 5

100.0 %

0 / 0

src/theory/eager_proof_generator.cpp

93.7 %

59 / 63

40.9 %

81 / 198

src/theory/eager_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/ee_manager.cpp

92.3 %

12 / 13

50.0 %

10 / 20

src/theory/ee_manager.h

75.0 %

3 / 4

100.0 %

0 / 0

src/theory/ee_manager_distributed.cpp

97.9 %

46 / 47

36.2 %

42 / 116

src/theory/ee_manager_distributed.h

44.4 %

4 / 9

100.0 %

0 / 0

src/theory/ee_setup_info.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/engine_output_channel.cpp

71.8 %

79 / 110

30.1 %

89 / 296

src/theory/engine_output_channel.h

100.0 %

1 / 1

0.0 %

0 / 4

src/theory/evaluator.cpp

78.3 %

387 / 494

39.1 %

694 / 1777

src/theory/evaluator.h

83.3 %

5 / 6

100.0 %

0 / 0

src/theory/ext_theory.cpp

73.2 %

183 / 250

43.8 %

312 / 713

src/theory/ext_theory.h

100.0 %

7 / 7

50.0 %

1 / 2

src/theory/fp/fp_converter.cpp

64.9 %

491 / 757

30.8 %

1024 / 3327

src/theory/fp/fp_converter.h

100.0 %

5 / 5

100.0 %

0 / 0

src/theory/fp/fp_expand_defs.cpp

42.6 %

55 / 129

16.5 %

104 / 630

src/theory/fp/fp_expand_defs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/fp/theory_fp.cpp

71.8 %

324 / 451

29.6 %

718 / 2424

src/theory/fp/theory_fp.h

85.7 %

6 / 7

0.0 %

0 / 2

src/theory/fp/theory_fp_rewriter.cpp

78.0 %

595 / 763

25.9 %

1033 / 3981

src/theory/fp/theory_fp_rewriter.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/fp/theory_fp_type_rules.cpp

66.7 %

192 / 288

27.4 %

419 / 1530

src/theory/fp/type_enumerator.h

61.4 %

27 / 44

24.3 %

17 / 70

src/theory/incomplete_id.cpp

4.0 %

1 / 25

10.0 %

2 / 20

src/theory/inference_id.cpp

0.3 %

1 / 343

0.7 %

2 / 271

src/theory/inference_manager_buffered.cpp

92.8 %

77 / 83

35.7 %

55 / 154

src/theory/inference_manager_buffered.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/interrupted.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/lazy_tree_proof_generator.cpp

78.1 %

50 / 64

29.6 %

42 / 142

src/theory/lazy_tree_proof_generator.h

92.9 %

13 / 14

64.3 %

9 / 14

src/theory/logic_info.cpp

90.5 %

390 / 431

57.9 %

412 / 712

src/theory/logic_info.h

100.0 %

23 / 23

83.3 %

15 / 18

src/theory/model_manager.cpp

95.1 %

98 / 103

48.2 %

131 / 272

src/theory/model_manager_distributed.cpp

90.0 %

45 / 50

45.6 %

41 / 90

src/theory/output_channel.cpp

41.7 %

15 / 36

13.9 %

5 / 36

src/theory/output_channel.h

50.0 %

3 / 6

100.0 %

0 / 0

src/theory/quantifiers/alpha_equivalence.cpp

96.2 %

51 / 53

43.4 %

106 / 244

src/theory/quantifiers/alpha_equivalence.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/quantifiers/bv_inverter.cpp

93.0 %

187 / 201

44.9 %

476 / 1060

src/theory/quantifiers/bv_inverter.h

100.0 %

6 / 6

50.0 %

4 / 8

src/theory/quantifiers/bv_inverter_utils.cpp

98.9 %

811 / 820

48.7 %

2608 / 5352

src/theory/quantifiers/candidate_rewrite_database.cpp

78.5 %

102 / 130

34.2 %

164 / 480

src/theory/quantifiers/candidate_rewrite_database.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/candidate_rewrite_filter.cpp

91.3 %

115 / 126

42.7 %

269 / 630

src/theory/quantifiers/candidate_rewrite_filter.h

100.0 %

6 / 6

50.0 %

2 / 4

src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp

85.2 %

449 / 527

41.7 %

1172 / 2808

src/theory/quantifiers/cegqi/ceg_arith_instantiator.h

100.0 %

2 / 2

72.7 %

16 / 22

src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp

85.5 %

300 / 351

39.1 %

671 / 1718

src/theory/quantifiers/cegqi/ceg_bv_instantiator.h

100.0 %

3 / 3

50.0 %

1 / 2

src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp

100.0 %

171 / 171

41.8 %

445 / 1064

src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp

91.4 %

64 / 70

50.2 %

159 / 317

src/theory/quantifiers/cegqi/ceg_dt_instantiator.h

100.0 %

3 / 3

50.0 %

2 / 4

src/theory/quantifiers/cegqi/ceg_instantiator.cpp

91.6 %

815 / 890

49.5 %

1662 / 3360

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 %

262 / 280

47.5 %

470 / 990

src/theory/quantifiers/cegqi/inst_strategy_cegqi.h

100.0 %

3 / 3

50.0 %

2 / 4

src/theory/quantifiers/cegqi/nested_qe.cpp

89.7 %

70 / 78

44.5 %

146 / 328

src/theory/quantifiers/cegqi/nested_qe.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/cegqi/vts_term_cache.cpp

93.8 %

137 / 146

51.7 %

306 / 592

src/theory/quantifiers/cegqi/vts_term_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/conjecture_generator.cpp

88.6 %

1248 / 1409

42.6 %

2561 / 6014

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

162 / 358

src/theory/quantifiers/dynamic_rewrite.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/ematching/candidate_generator.cpp

95.7 %

177 / 185

42.2 %

335 / 794

src/theory/quantifiers/ematching/candidate_generator.h

100.0 %

10 / 10

50.0 %

1 / 2

src/theory/quantifiers/ematching/ho_trigger.cpp

89.1 %

229 / 257

41.0 %

465 / 1134

src/theory/quantifiers/ematching/im_generator.cpp

100.0 %

6 / 6

50.0 %

2 / 4

src/theory/quantifiers/ematching/im_generator.h

33.3 %

2 / 6

100.0 %

0 / 0

src/theory/quantifiers/ematching/inst_match_generator.cpp

85.2 %

293 / 344

42.7 %

590 / 1382

src/theory/quantifiers/ematching/inst_match_generator.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/ematching/inst_match_generator_multi.cpp

94.3 %

132 / 140

52.5 %

207 / 394

src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp

98.9 %

87 / 88

47.9 %

114 / 238

src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/ematching/inst_match_generator_simple.cpp

87.8 %

79 / 90

43.0 %

185 / 430

src/theory/quantifiers/ematching/inst_match_generator_simple.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/ematching/inst_strategy.cpp

76.9 %

10 / 13

18.8 %

3 / 16

src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp

75.3 %

265 / 352

36.9 %

494 / 1337

src/theory/quantifiers/ematching/inst_strategy_e_matching.h

100.0 %

3 / 3

71.4 %

10 / 14

src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp

65.8 %

52 / 79

37.3 %

90 / 241

src/theory/quantifiers/ematching/instantiation_engine.cpp

86.4 %

114 / 132

43.0 %

179 / 416

src/theory/quantifiers/ematching/instantiation_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/ematching/pattern_term_selector.cpp

93.1 %

335 / 360

49.7 %

769 / 1548

src/theory/quantifiers/ematching/trigger.cpp

86.8 %

92 / 106

39.2 %

160 / 408

src/theory/quantifiers/ematching/trigger_database.cpp

91.3 %

73 / 80

48.9 %

89 / 182

src/theory/quantifiers/ematching/trigger_term_info.cpp

100.0 %

42 / 42

76.1 %

102 / 134

src/theory/quantifiers/ematching/trigger_term_info.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/ematching/trigger_trie.cpp

100.0 %

29 / 29

59.5 %

25 / 42

src/theory/quantifiers/ematching/var_match_generator.cpp

96.9 %

31 / 32

52.0 %

52 / 100

src/theory/quantifiers/ematching/var_match_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/equality_query.cpp

77.5 %

69 / 89

38.4 %

168 / 438

src/theory/quantifiers/equality_query.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/expr_miner.cpp

90.9 %

40 / 44

39.4 %

52 / 132

src/theory/quantifiers/expr_miner.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/expr_miner_manager.cpp

56.0 %

42 / 75

34.3 %

48 / 140

src/theory/quantifiers/expr_miner_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/extended_rewrite.cpp

90.8 %

764 / 841

48.4 %

1841 / 3800

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

45.8 %

248 / 542

src/theory/quantifiers/first_order_model.h

66.7 %

4 / 6

40.9 %

9 / 22

src/theory/quantifiers/fmf/bounded_integers.cpp

93.5 %

490 / 524

45.3 %

1220 / 2694

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

124 / 252

src/theory/quantifiers/fmf/full_model_check.cpp

93.7 %

749 / 799

50.4 %

1631 / 3239

src/theory/quantifiers/fmf/full_model_check.h

100.0 %

13 / 13

50.0 %

3 / 6

src/theory/quantifiers/fmf/model_builder.cpp

53.5 %

38 / 71

19.2 %

45 / 234

src/theory/quantifiers/fmf/model_builder.h

80.0 %

4 / 5

100.0 %

0 / 0

src/theory/quantifiers/fmf/model_engine.cpp

68.1 %

124 / 182

32.8 %

222 / 676

src/theory/quantifiers/fmf/model_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/fun_def_evaluator.cpp

90.2 %

129 / 143

42.0 %

321 / 764

src/theory/quantifiers/fun_def_evaluator.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/index_trie.cpp

97.7 %

42 / 43

56.1 %

55 / 98

src/theory/quantifiers/index_trie.h

100.0 %

9 / 9

100.0 %

0 / 0

src/theory/quantifiers/inst_match.cpp

56.5 %

26 / 46

16.9 %

24 / 142

src/theory/quantifiers/inst_match.h

7.1 %

1 / 14

0.0 %

0 / 8

src/theory/quantifiers/inst_match_trie.cpp

45.2 %

70 / 155

21.1 %

83 / 394

src/theory/quantifiers/inst_match_trie.h

100.0 %

10 / 10

50.0 %

1 / 2

src/theory/quantifiers/inst_strategy_enumerative.cpp

84.0 %

79 / 94

44.4 %

142 / 320

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

39.0 %

73 / 187

src/theory/quantifiers/inst_strategy_pool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/instantiate.cpp

79.3 %

268 / 338

37.4 %

516 / 1380

src/theory/quantifiers/instantiate.h

100.0 %

5 / 5

50.0 %

2 / 4

src/theory/quantifiers/instantiation_list.cpp

100.0 %

7 / 7

20.0 %

2 / 10

src/theory/quantifiers/instantiation_list.h

100.0 %

6 / 6

50.0 %

2 / 4

src/theory/quantifiers/lazy_trie.cpp

93.6 %

73 / 78

39.5 %

124 / 314

src/theory/quantifiers/lazy_trie.h

100.0 %

6 / 6

50.0 %

1 / 2

src/theory/quantifiers/proof_checker.cpp

72.4 %

42 / 58

24.8 %

67 / 270

src/theory/quantifiers/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/quant_bound_inference.cpp

100.0 %

52 / 52

56.3 %

81 / 144

src/theory/quantifiers/quant_bound_inference.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quant_conflict_find.cpp

82.9 %

1158 / 1397

45.4 %

2476 / 5457

src/theory/quantifiers/quant_conflict_find.h

100.0 %

18 / 18

52.8 %

19 / 36

src/theory/quantifiers/quant_module.cpp

100.0 %

23 / 23

43.8 %

7 / 16

src/theory/quantifiers/quant_module.h

81.8 %

9 / 11

100.0 %

0 / 0

src/theory/quantifiers/quant_relevance.cpp

95.0 %

19 / 20

58.3 %

21 / 36

src/theory/quantifiers/quant_relevance.h

50.0 %

2 / 4

0.0 %

0 / 2

src/theory/quantifiers/quant_rep_bound_ext.cpp

96.2 %

25 / 26

43.1 %

25 / 58

src/theory/quantifiers/quant_rep_bound_ext.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quant_split.cpp

98.0 %

99 / 101

52.1 %

199 / 382

src/theory/quantifiers/quant_split.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/quant_util.cpp

81.9 %

68 / 83

41.5 %

93 / 224

src/theory/quantifiers/quant_util.h

66.7 %

4 / 6

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_attributes.cpp

72.5 %

153 / 211

41.8 %

333 / 796

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

44.4 %

8 / 18

src/theory/quantifiers/quantifiers_macros.cpp

93.0 %

133 / 143

45.7 %

290 / 634

src/theory/quantifiers/quantifiers_macros.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_modules.cpp

100.0 %

44 / 44

64.1 %

59 / 92

src/theory/quantifiers/quantifiers_registry.cpp

77.9 %

74 / 95

36.8 %

84 / 228

src/theory/quantifiers/quantifiers_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_rewriter.cpp

76.5 %

893 / 1168

40.3 %

2048 / 5079

src/theory/quantifiers/quantifiers_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_state.cpp

50.6 %

41 / 81

25.2 %

62 / 246

src/theory/quantifiers/quantifiers_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/quantifiers_statistics.cpp

100.0 %

22 / 22

50.0 %

22 / 44

src/theory/quantifiers/query_generator.cpp

0.9 %

2 / 223

0.3 %

2 / 684

src/theory/quantifiers/query_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/relevant_domain.cpp

96.8 %

215 / 222

51.6 %

492 / 954

src/theory/quantifiers/relevant_domain.h

100.0 %

12 / 12

50.0 %

1 / 2

src/theory/quantifiers/single_inv_partition.cpp

89.0 %

274 / 308

48.1 %

497 / 1034

src/theory/quantifiers/single_inv_partition.h

100.0 %

7 / 7

83.3 %

5 / 6

src/theory/quantifiers/skolemize.cpp

89.2 %

182 / 204

41.6 %

416 / 1000

src/theory/quantifiers/skolemize.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/solution_filter.cpp

62.2 %

28 / 45

27.9 %

48 / 172

src/theory/quantifiers/solution_filter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/ce_guided_single_inv.cpp

95.7 %

270 / 282

45.9 %

565 / 1230

src/theory/quantifiers/sygus/ce_guided_single_inv.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/sygus/cegis.cpp

93.9 %

323 / 344

47.1 %

611 / 1298

src/theory/quantifiers/sygus/cegis.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/cegis_core_connective.cpp

88.6 %

403 / 455

42.5 %

796 / 1871

src/theory/quantifiers/sygus/cegis_core_connective.h

100.0 %

6 / 6

50.0 %

3 / 6

src/theory/quantifiers/sygus/cegis_unif.cpp

87.1 %

304 / 349

36.8 %

510 / 1386

src/theory/quantifiers/sygus/cegis_unif.h

100.0 %

5 / 5

50.0 %

13 / 26

src/theory/quantifiers/sygus/enum_stream_substitution.cpp

66.7 %

230 / 345

29.2 %

326 / 1118

src/theory/quantifiers/sygus/enum_stream_substitution.h

100.0 %

6 / 6

50.0 %

2 / 4

src/theory/quantifiers/sygus/example_eval_cache.cpp

98.0 %

50 / 51

38.5 %

70 / 182

src/theory/quantifiers/sygus/example_infer.cpp

83.7 %

103 / 123

35.6 %

165 / 464

src/theory/quantifiers/sygus/example_min_eval.cpp

100.0 %

30 / 30

42.6 %

46 / 108

src/theory/quantifiers/sygus/example_min_eval.h

100.0 %

5 / 5

50.0 %

1 / 2

src/theory/quantifiers/sygus/rcons_obligation.cpp

30.4 %

17 / 56

7.2 %

11 / 152

src/theory/quantifiers/sygus/rcons_obligation.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/rcons_type_info.cpp

100.0 %

31 / 31

52.8 %

38 / 72

src/theory/quantifiers/sygus/rcons_type_info.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/sygus/sygus_abduct.cpp

98.8 %

85 / 86

46.7 %

210 / 450

src/theory/quantifiers/sygus/sygus_enumerator.cpp

97.4 %

642 / 659

45.0 %

1036 / 2302

src/theory/quantifiers/sygus/sygus_enumerator.h

100.0 %

9 / 9

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp

5.9 %

1 / 17

4.8 %

2 / 42

src/theory/quantifiers/sygus/sygus_enumerator_basic.h

0.0 %

0 / 4

0.0 %

0 / 2

src/theory/quantifiers/sygus/sygus_eval_unfold.cpp

97.3 %

180 / 185

42.0 %

392 / 934

src/theory/quantifiers/sygus/sygus_eval_unfold.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_explain.cpp

95.7 %

157 / 164

37.1 %

292 / 788

src/theory/quantifiers/sygus/sygus_explain.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_grammar_cons.cpp

87.7 %

790 / 901

42.1 %

1462 / 3472

src/theory/quantifiers/sygus/sygus_grammar_cons.h

100.0 %

4 / 4

50.0 %

2 / 4

src/theory/quantifiers/sygus/sygus_grammar_norm.cpp

49.2 %

126 / 256

20.3 %

223 / 1098

src/theory/quantifiers/sygus/sygus_grammar_norm.h

40.0 %

8 / 20

2.6 %

1 / 38

src/theory/quantifiers/sygus/sygus_grammar_red.cpp

97.5 %

77 / 79

44.8 %

171 / 382

src/theory/quantifiers/sygus/sygus_grammar_red.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_interpol.cpp

84.4 %

151 / 179

39.9 %

271 / 680

src/theory/quantifiers/sygus/sygus_interpol.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_invariance.cpp

80.4 %

111 / 138

38.2 %

203 / 532

src/theory/quantifiers/sygus/sygus_invariance.h

95.0 %

19 / 20

50.0 %

14 / 28

src/theory/quantifiers/sygus/sygus_module.cpp

100.0 %

5 / 5

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

100.0 %

119 / 119

43.6 %

223 / 512

src/theory/quantifiers/sygus/sygus_process_conj.cpp

90.7 %

351 / 387

44.0 %

622 / 1414

src/theory/quantifiers/sygus/sygus_process_conj.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_qe_preproc.cpp

98.8 %

82 / 83

47.3 %

178 / 376

src/theory/quantifiers/sygus/sygus_qe_preproc.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_reconstruct.cpp

89.7 %

183 / 204

49.6 %

394 / 794

src/theory/quantifiers/sygus/sygus_reconstruct.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_repair_const.cpp

90.3 %

299 / 331

41.2 %

591 / 1436

src/theory/quantifiers/sygus/sygus_repair_const.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/sygus_stats.cpp

100.0 %

17 / 17

50.0 %

20 / 40

src/theory/quantifiers/sygus/sygus_unif.cpp

90.9 %

50 / 55

35.0 %

49 / 140

src/theory/quantifiers/sygus/sygus_unif_io.cpp

90.5 %

744 / 822

40.6 %

1337 / 3296

src/theory/quantifiers/sygus/sygus_unif_io.h

100.0 %

13 / 13

60.0 %

6 / 10

src/theory/quantifiers/sygus/sygus_unif_rl.cpp

68.5 %

437 / 638

29.7 %

738 / 2486

src/theory/quantifiers/sygus/sygus_unif_rl.h

100.0 %

7 / 7

30.4 %

14 / 46

src/theory/quantifiers/sygus/sygus_unif_strat.cpp

83.2 %

475 / 571

42.8 %

927 / 2164

src/theory/quantifiers/sygus/sygus_unif_strat.h

100.0 %

18 / 18

50.0 %

3 / 6

src/theory/quantifiers/sygus/sygus_utils.cpp

74.4 %

58 / 78

30.1 %

110 / 366

src/theory/quantifiers/sygus/synth_conjecture.cpp

87.3 %

607 / 695

40.8 %

1289 / 3160

src/theory/quantifiers/sygus/synth_conjecture.h

100.0 %

9 / 9

100.0 %

0 / 0

src/theory/quantifiers/sygus/synth_engine.cpp

95.5 %

127 / 133

55.4 %

214 / 386

src/theory/quantifiers/sygus/synth_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/sygus/template_infer.cpp

97.9 %

94 / 96

44.4 %

239 / 538

src/theory/quantifiers/sygus/template_infer.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/sygus/term_database_sygus.cpp

86.5 %

479 / 554

42.2 %

865 / 2051

src/theory/quantifiers/sygus/term_database_sygus.h

100.0 %

7 / 7

62.5 %

5 / 8

src/theory/quantifiers/sygus/transition_inference.cpp

94.0 %

280 / 298

46.6 %

521 / 1118

src/theory/quantifiers/sygus/transition_inference.h

100.0 %

12 / 12

50.0 %

4 / 8

src/theory/quantifiers/sygus/type_info.cpp

84.6 %

203 / 240

41.1 %

336 / 818

src/theory/quantifiers/sygus/type_info.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus/type_node_id_trie.cpp

100.0 %

15 / 15

66.7 %

12 / 18

src/theory/quantifiers/sygus/type_node_id_trie.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/sygus_inst.cpp

83.1 %

212 / 255

37.2 %

379 / 1020

src/theory/quantifiers/sygus_inst.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/sygus_sampler.cpp

79.5 %

368 / 463

38.2 %

589 / 1542

src/theory/quantifiers/sygus_sampler.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/term_database.cpp

81.5 %

552 / 677

42.7 %

1274 / 2982

src/theory/quantifiers/term_database.h

100.0 %

3 / 3

50.0 %

2 / 4

src/theory/quantifiers/term_enumeration.cpp

55.2 %

16 / 29

31.4 %

27 / 86

src/theory/quantifiers/term_enumeration.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/term_pools.cpp

97.3 %

72 / 74

40.9 %

94 / 230

src/theory/quantifiers/term_pools.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/term_registry.cpp

89.8 %

53 / 59

42.8 %

71 / 166

src/theory/quantifiers/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/term_tuple_enumerator.cpp

75.6 %

155 / 205

37.2 %

235 / 632

src/theory/quantifiers/term_tuple_enumerator.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/term_util.cpp

84.8 %

262 / 309

55.7 %

569 / 1022

src/theory/quantifiers/theory_quantifiers.cpp

95.0 %

76 / 80

51.1 %

97 / 190

src/theory/quantifiers/theory_quantifiers.h

33.3 %

1 / 3

0.0 %

0 / 2

src/theory/quantifiers/theory_quantifiers_type_rules.cpp

84.1 %

37 / 44

36.0 %

90 / 250

src/theory/quantifiers_engine.cpp

84.0 %

289 / 344

42.5 %

530 / 1248

src/theory/relevance_manager.cpp

74.3 %

110 / 148

30.1 %

153 / 508

src/theory/relevance_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/rep_set.cpp

74.1 %

186 / 251

34.8 %

276 / 792

src/theory/rep_set.h

64.3 %

9 / 14

100.0 %

0 / 0

src/theory/rewriter.cpp

87.7 %

171 / 195

43.2 %

331 / 766

src/theory/rewriter.h

100.0 %

1 / 1

75.0 %

12 / 16

src/theory/rewriter_attributes.h

100.0 %

30 / 30

43.9 %

616 / 1404

src/theory/sep/theory_sep.cpp

84.7 %

921 / 1087

41.7 %

2274 / 5448

src/theory/sep/theory_sep.h

56.3 %

18 / 32

20.6 %

21 / 102

src/theory/sep/theory_sep_rewriter.cpp

88.4 %

84 / 95

44.9 %

180 / 401

src/theory/sep/theory_sep_rewriter.h

100.0 %

4 / 4

50.0 %

10 / 20

src/theory/sep/theory_sep_type_rules.cpp

90.9 %

40 / 44

23.2 %

46 / 198

src/theory/sets/cardinality_extension.cpp

91.1 %

525 / 576

47.4 %

1234 / 2603

src/theory/sets/cardinality_extension.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/sets/inference_manager.cpp

50.0 %

43 / 86

24.3 %

92 / 378

src/theory/sets/inference_manager.h

100.0 %

1 / 1

0.0 %

0 / 2

src/theory/sets/normal_form.h

97.0 %

65 / 67

49.7 %

170 / 342

src/theory/sets/rels_utils.h

100.0 %

44 / 44

50.0 %

73 / 146

src/theory/sets/singleton_op.cpp

85.7 %

12 / 14

42.9 %

6 / 14

src/theory/sets/singleton_op.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/sets/skolem_cache.cpp

80.8 %

21 / 26

41.8 %

51 / 122

src/theory/sets/skolem_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/sets/solver_state.cpp

94.2 %

276 / 293

47.5 %

579 / 1220

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

131 / 288

src/theory/sets/term_registry.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/sets/theory_sets.cpp

92.5 %

99 / 107

47.5 %

150 / 316

src/theory/sets/theory_sets.h

80.0 %

4 / 5

0.0 %

0 / 2

src/theory/sets/theory_sets_private.cpp

94.0 %

670 / 713

46.9 %

1463 / 3119

src/theory/sets/theory_sets_private.h

66.7 %

2 / 3

0.0 %

0 / 2

src/theory/sets/theory_sets_rels.cpp

94.6 %

740 / 782

51.4 %

1668 / 3247

src/theory/sets/theory_sets_rels.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/sets/theory_sets_rewriter.cpp

95.1 %

327 / 344

48.9 %

922 / 1885

src/theory/sets/theory_sets_rewriter.h

100.0 %

1 / 1

25.0 %

1 / 4

src/theory/sets/theory_sets_type_enumerator.cpp

100.0 %

61 / 61

46.2 %

86 / 186

src/theory/sets/theory_sets_type_rules.cpp

78.5 %

161 / 205

26.1 %

280 / 1074

src/theory/shared_solver.cpp

67.4 %

29 / 43

45.2 %

47 / 104

src/theory/shared_solver.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/shared_solver_distributed.cpp

100.0 %

35 / 35

54.9 %

56 / 102

src/theory/shared_solver_distributed.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/shared_terms_database.cpp

85.3 %

128 / 150

32.0 %

221 / 690

src/theory/shared_terms_database.h

100.0 %

25 / 25

33.3 %

12 / 36

src/theory/skolem_lemma.cpp

100.0 %

14 / 14

32.9 %

25 / 76

src/theory/skolem_lemma.h

100.0 %

1 / 1

50.0 %

2 / 4

src/theory/smt_engine_subsolver.cpp

81.3 %

39 / 48

34.1 %

45 / 132

src/theory/sort_inference.cpp

84.5 %

447 / 529

45.6 %

1007 / 2206

src/theory/sort_inference.h

83.3 %

5 / 6

100.0 %

0 / 0

src/theory/strings/arith_entail.cpp

89.6 %

344 / 384

45.8 %

878 / 1918

src/theory/strings/base_solver.cpp

78.6 %

297 / 378

39.2 %

626 / 1595

src/theory/strings/base_solver.h

100.0 %

2 / 2

50.0 %

2 / 4

src/theory/strings/core_solver.cpp

80.6 %

1105 / 1371

40.1 %

2537 / 6323

src/theory/strings/core_solver.h

100.0 %

2 / 2

40.9 %

9 / 22

src/theory/strings/eager_solver.cpp

98.5 %

65 / 66

53.5 %

122 / 228

src/theory/strings/eqc_info.cpp

100.0 %

57 / 57

44.6 %

148 / 332

src/theory/strings/eqc_info.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/extf_solver.cpp

87.9 %

311 / 354

45.7 %

788 / 1726

src/theory/strings/extf_solver.h

100.0 %

4 / 4

50.0 %

1 / 2

src/theory/strings/infer_info.cpp

69.7 %

23 / 33

36.8 %

39 / 106

src/theory/strings/infer_info.h

100.0 %

2 / 2

50.0 %

4 / 8

src/theory/strings/infer_proof_cons.cpp

84.0 %

451 / 537

40.8 %

891 / 2182

src/theory/strings/infer_proof_cons.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/inference_manager.cpp

91.1 %

164 / 180

46.3 %

359 / 776

src/theory/strings/inference_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/normal_form.cpp

100.0 %

84 / 84

43.9 %

150 / 342

src/theory/strings/normal_form.h

100.0 %

2 / 2

50.0 %

3 / 6

src/theory/strings/proof_checker.cpp

80.4 %

238 / 296

31.0 %

573 / 1846

src/theory/strings/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/strings/regexp_elim.cpp

78.3 %

231 / 295

34.3 %

465 / 1356

src/theory/strings/regexp_elim.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/regexp_entail.cpp

88.4 %

349 / 395

48.8 %

728 / 1493

src/theory/strings/regexp_operation.cpp

72.3 %

723 / 1000

36.2 %

1525 / 4218

src/theory/strings/regexp_solver.cpp

88.9 %

296 / 333

48.0 %

596 / 1241

src/theory/strings/regexp_solver.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/rewrites.cpp

0.5 %

1 / 196

1.0 %

2 / 192

src/theory/strings/sequences_rewriter.cpp

96.4 %

1557 / 1615

51.9 %

4893 / 9422

src/theory/strings/sequences_rewriter.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/sequences_stats.cpp

100.0 %

23 / 23

48.0 %

24 / 50

src/theory/strings/skolem_cache.cpp

91.0 %

122 / 134

48.7 %

283 / 581

src/theory/strings/skolem_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/solver_state.cpp

95.3 %

101 / 106

46.2 %

156 / 338

src/theory/strings/strategy.cpp

70.7 %

58 / 82

35.1 %

87 / 248

src/theory/strings/strings_entail.cpp

96.4 %

425 / 441

47.4 %

957 / 2017

src/theory/strings/strings_fmf.cpp

93.0 %

40 / 43

53.3 %

48 / 90

src/theory/strings/strings_fmf.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/strings_rewriter.cpp

100.0 %

161 / 161

48.2 %

422 / 876

src/theory/strings/strings_rewriter.h

100.0 %

1 / 1

25.0 %

2 / 8

src/theory/strings/term_registry.cpp

90.6 %

279 / 308

47.2 %

670 / 1418

src/theory/strings/theory_strings.cpp

81.1 %

451 / 556

41.2 %

953 / 2311

src/theory/strings/theory_strings.h

100.0 %

32 / 32

52.3 %

69 / 132

src/theory/strings/theory_strings_preprocess.cpp

100.0 %

488 / 488

51.2 %

1440 / 2812

src/theory/strings/theory_strings_type_rules.cpp

70.8 %

97 / 137

26.3 %

122 / 464

src/theory/strings/theory_strings_utils.cpp

91.6 %

175 / 191

47.3 %

327 / 692

src/theory/strings/type_enumerator.cpp

85.4 %

117 / 137

33.1 %

78 / 236

src/theory/strings/type_enumerator.h

100.0 %

7 / 7

100.0 %

0 / 0

src/theory/strings/word.cpp

82.6 %

233 / 282

29.7 %

305 / 1028

src/theory/subs_minimize.cpp

0.4 %

1 / 223

0.2 %

2 / 832

src/theory/substitutions.cpp

85.3 %

93 / 109

41.0 %

218 / 532

src/theory/substitutions.h

73.3 %

11 / 15

12.5 %

2 / 16

src/theory/term_registration_visitor.cpp

80.1 %

109 / 136

41.1 %

232 / 564

src/theory/term_registration_visitor.h

100.0 %

9 / 9

50.0 %

1 / 2

src/theory/theory.cpp

84.7 %

216 / 255

47.6 %

447 / 939

src/theory/theory.h

75.5 %

71 / 94

41.2 %

70 / 170

src/theory/theory_engine.cpp

80.9 %

722 / 892

40.7 %

1814 / 4452

src/theory/theory_engine.h

100.0 %

43 / 43

27.7 %

101 / 364

src/theory/theory_engine_proof_generator.cpp

80.0 %

48 / 60

35.2 %

93 / 264

src/theory/theory_engine_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/theory_eq_notify.h

78.9 %

15 / 19

58.3 %

14 / 24

src/theory/theory_id.cpp

85.9 %

67 / 78

57.7 %

56 / 97

src/theory/theory_inference.cpp

76.5 %

13 / 17

26.7 %

8 / 30

src/theory/theory_inference.h

72.7 %

8 / 11

50.0 %

1 / 2

src/theory/theory_inference_manager.cpp

82.8 %

178 / 215

41.9 %

217 / 518

src/theory/theory_model.cpp

88.1 %

376 / 427

42.3 %

784 / 1853

src/theory/theory_model.h

100.0 %

4 / 4

50.0 %

1 / 2

src/theory/theory_model_builder.cpp

94.3 %

629 / 667

43.9 %

1227 / 2795

src/theory/theory_model_builder.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/theory_preprocessor.cpp

93.1 %

201 / 216

45.2 %

476 / 1054

src/theory/theory_proof_step_buffer.cpp

81.0 %

81 / 100

40.9 %

140 / 342

src/theory/theory_proof_step_buffer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/theory_rewriter.cpp

90.0 %

18 / 20

46.0 %

23 / 50

src/theory/theory_rewriter.h

83.3 %

5 / 6

100.0 %

0 / 0

src/theory/theory_state.cpp

100.0 %

73 / 73

41.7 %

80 / 192

src/theory/theory_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/trust_node.cpp

77.4 %

48 / 62

34.7 %

70 / 202

src/theory/trust_node.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/trust_substitutions.cpp

99.2 %

120 / 121

46.9 %

253 / 540

src/theory/trust_substitutions.h

100.0 %

1 / 1

0.0 %

0 / 2

src/theory/type_enumerator.h

92.7 %

51 / 55

25.0 %

41 / 164

src/theory/type_set.cpp

96.6 %

57 / 59

57.7 %

60 / 104

src/theory/type_set.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/uf/cardinality_extension.cpp

80.5 %

815 / 1013

40.8 %

1685 / 4130

src/theory/uf/cardinality_extension.h

96.4 %

53 / 55

36.5 %

38 / 104

src/theory/uf/eq_proof.cpp

86.2 %

618 / 717

39.4 %

1490 / 3784

src/theory/uf/eq_proof.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/uf/equality_engine.cpp

91.7 %

1256 / 1370

43.8 %

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

38 / 184

src/theory/uf/equality_engine_notify.h

63.6 %

7 / 11

100.0 %

0 / 0

src/theory/uf/equality_engine_types.h

75.3 %

61 / 81

32.4 %

11 / 34

src/theory/uf/ho_extension.cpp

82.9 %

204 / 246

40.9 %

425 / 1038

src/theory/uf/ho_extension.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/uf/proof_checker.cpp

88.7 %

102 / 115

31.0 %

175 / 564

src/theory/uf/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/uf/proof_equality_engine.cpp

69.5 %

182 / 262

31.3 %

411 / 1314

src/theory/uf/proof_equality_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/uf/symmetry_breaker.cpp

82.7 %

401 / 485

43.4 %

958 / 2208

src/theory/uf/symmetry_breaker.h

100.0 %

7 / 7

50.0 %

4 / 8

src/theory/uf/theory_uf.cpp

87.1 %

290 / 333

47.6 %

643 / 1350

src/theory/uf/theory_uf.h

94.7 %

18 / 19

48.4 %

30 / 62

src/theory/uf/theory_uf_model.cpp

57.8 %

74 / 128

32.1 %

142 / 442

src/theory/uf/theory_uf_model.h

100.0 %

16 / 16

53.3 %

16 / 30

src/theory/uf/theory_uf_rewriter.cpp

83.5 %

76 / 91

43.4 %

209 / 482

src/theory/uf/theory_uf_rewriter.h

100.0 %

1 / 1

0.0 %

0 / 12

src/theory/uf/theory_uf_type_rules.cpp

68.0 %

51 / 75

27.5 %

88 / 320

src/theory/valuation.cpp

62.1 %

72 / 116

14.4 %

52 / 361

src/theory/valuation.h

100.0 %

3 / 3

100.0 %

0 / 0

src/util/abstract_value.cpp

100.0 %

6 / 6

31.3 %

5 / 16

src/util/abstract_value.h

100.0 %

6 / 6

50.0 %

1 / 2

src/util/bin_heap.h

98.8 %

163 / 165

21.8 %

123 / 564

src/util/bitvector.cpp

100.0 %

171 / 171

56.3 %

178 / 316

src/util/bitvector.h

94.4 %

68 / 72

69.7 %

23 / 33

src/util/bool.h

100.0 %

2 / 2

100.0 %

0 / 0

src/util/cardinality.cpp

79.2 %

114 / 144

48.3 %

223 / 462

src/util/cardinality.h

100.0 %

25 / 25

54.5 %

12 / 22

src/util/cardinality_class.cpp

39.1 %

9 / 23

52.0 %

13 / 25

src/util/dense_map.h

82.0 %

91 / 111

13.0 %

75 / 577

src/util/divisible.cpp

100.0 %

4 / 4

35.7 %

5 / 14

src/util/divisible.h

71.4 %

5 / 7

100.0 %

0 / 0

src/util/floatingpoint.cpp

81.9 %

181 / 221

38.9 %

203 / 522

src/util/floatingpoint.h

90.8 %

59 / 65

50.0 %

9 / 18

src/util/floatingpoint_literal_symfpu.cpp

84.2 %

101 / 120

20.3 %

61 / 300

src/util/floatingpoint_literal_symfpu_traits.cpp

92.5 %

111 / 120

25.0 %

67 / 268

src/util/floatingpoint_size.cpp

100.0 %

10 / 10

12.5 %

8 / 64

src/util/floatingpoint_size.h

100.0 %

16 / 16

50.0 %

2 / 4

src/util/hash.h

100.0 %

7 / 7

50.0 %

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/maybe.h

59.3 %

16 / 27

9.1 %

2 / 22

src/util/ostream_util.cpp

0.0 %

0 / 7

100.0 %

0 / 0

src/util/poly_util.cpp

45.4 %

74 / 163

17.0 %

62 / 364

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

31.7 %

38 / 120

src/util/rational_cln_imp.h

90.4 %

94 / 104

43.1 %

44 / 102

src/util/real_algebraic_number_poly_imp.cpp

44.0 %

33 / 75

14.5 %

22 / 152

src/util/real_algebraic_number_poly_imp.h

60.0 %

3 / 5

100.0 %

0 / 0

src/util/regexp.cpp

76.5 %

13 / 17

50.0 %

2 / 4

src/util/resource_manager.cpp

53.5 %

76 / 142

21.7 %

46 / 212

src/util/resource_manager.h

100.0 %

2 / 2

50.0 %

2 / 4

src/util/result.cpp

62.6 %

124 / 198

34.6 %

79 / 228

src/util/result.h

100.0 %

14 / 14

75.0 %

9 / 12

src/util/roundingmode.h

100.0 %

1 / 1

100.0 %

0 / 0

src/util/safe_print.cpp

0.0 %

0 / 102

0.0 %

0 / 84

src/util/safe_print.h

0.0 %

0 / 15

0.0 %

0 / 32

src/util/sampler.cpp

9.5 %

7 / 74

5.9 %

12 / 203

src/util/sexpr.cpp

64.7 %

11 / 17

40.9 %

9 / 22

src/util/sexpr.h

79.3 %

23 / 29

22.2 %

12 / 54

src/util/smt2_quote_string.cpp

100.0 %

8 / 8

77.3 %

17 / 22

src/util/statistics_public.cpp

100.0 %

14 / 14

52.2 %

24 / 46

src/util/statistics_registry.cpp

24.6 %

15 / 61

3.5 %

7 / 200

src/util/statistics_registry.h

96.9 %

31 / 32

29.3 %

55 / 188

src/util/statistics_stats.cpp

100.0 %

45 / 45

28.0 %

14 / 50

src/util/statistics_stats.h

100.0 %

31 / 31

100.0 %

0 / 0

src/util/statistics_value.cpp

71.1 %

27 / 38

36.1 %

13 / 36

src/util/statistics_value.h

45.5 %

40 / 88

28.7 %

37 / 129

src/util/string.cpp

95.8 %

254 / 265

58.2 %

283 / 486

src/util/string.h

95.8 %

23 / 24

50.0 %

4 / 8

src/util/utility.cpp

0.0 %

0 / 16

0.0 %

0 / 26

src/util/utility.h

100.0 %

15 / 15

34.6 %

18 / 52

test/api/boilerplate.cpp

100.0 %

5 / 5

50.0 %

7 / 14

test/api/issue4889.cpp

100.0 %

15 / 15

50.0 %

16 / 32

test/api/issue5074.cpp

100.0 %

9 / 9

50.0 %

14 / 28

test/api/ouroborous.cpp

90.8 %

69 / 76

50.6 %

127 / 251

test/api/reset_assertions.cpp

100.0 %

20 / 20

50.0 %

28 / 56

test/api/sep_log_api.cpp

84.7 %

83 / 98

50.9 %

115 / 226

test/api/smt2_compliance.cpp

100.0 %

33 / 33

50.0 %

45 / 90

test/api/two_solvers.cpp

100.0 %

7 / 7

50.0 %

12 / 24

test/unit/api/datatype_api_black.cpp

100.0 %

378 / 378

33.7 %

1022 / 3034

test/unit/api/grammar_black.cpp

100.0 %

62 / 62

35.7 %

250 / 700

test/unit/api/op_black.cpp

100.0 %

123 / 123

30.2 %

278 / 920

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

1604 / 1616

36.0 %

6199 / 17210

test/unit/api/solver_white.cpp

100.0 %

21 / 21

41.0 %

55 / 134

test/unit/api/sort_black.cpp

100.0 %

382 / 382

33.2 %

1207 / 3638

test/unit/api/term_black.cpp

100.0 %

881 / 881

31.6 %

3579 / 11342

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

96.7 %

87 / 90

23.7 %

167 / 706

test/unit/context/context_mm_black.cpp

97.1 %

34 / 35

36.4 %

39 / 107

test/unit/context/context_white.cpp

100.0 %

117 / 117

22.0 %

318 / 1444

test/unit/main/interactive_shell_black.cpp

100.0 %

58 / 58

45.2 %

56 / 124

test/unit/memory.h

100.0 %

12 / 12

21.4 %

6 / 28

test/unit/node/attribute_black.cpp

100.0 %

47 / 47

32.3 %

95 / 294

test/unit/node/attribute_white.cpp

100.0 %

314 / 314

28.6 %

1007 / 3526

test/unit/node/kind_black.cpp

100.0 %

32 / 32

28.9 %

55 / 190

test/unit/node/kind_map_black.cpp

100.0 %

10 / 10

29.5 %

23 / 78

test/unit/node/node_algorithm_black.cpp

100.0 %

93 / 93

35.1 %

311 / 886

test/unit/node/node_black.cpp

99.8 %

461 / 462

33.7 %

1524 / 4517

test/unit/node/node_builder_black.cpp

100.0 %

222 / 222

29.2 %

910 / 3117

test/unit/node/node_manager_black.cpp

100.0 %

197 / 197

30.5 %

595 / 1952

test/unit/node/node_manager_white.cpp

100.0 %

32 / 32

30.1 %

126 / 418

test/unit/node/node_self_iterator_black.cpp

100.0 %

22 / 22

30.0 %

84 / 280

test/unit/node/node_traversal_black.cpp

100.0 %

170 / 170

39.1 %

478 / 1224

test/unit/node/node_white.cpp

100.0 %

35 / 35

31.4 %

108 / 344

test/unit/node/symbol_table_black.cpp

100.0 %

74 / 74

34.4 %

203 / 590

test/unit/node/type_cardinality_black.cpp

100.0 %

210 / 210

35.5 %

532 / 1498

test/unit/node/type_node_white.cpp

100.0 %

49 / 49

30.0 %

180 / 600

test/unit/parser/parser_black.cpp

100.0 %

202 / 202

43.7 %

351 / 804

test/unit/parser/parser_builder_black.cpp

100.0 %

70 / 70

41.5 %

78 / 188

test/unit/preprocessing/pass_bv_gauss_white.cpp

97.3 %

1279 / 1314

42.6 %

4785 / 11225

test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp

100.0 %

16 / 16

42.2 %

43 / 102

test/unit/printer/smt2_printer_black.cpp

100.0 %

18 / 18

45.3 %

39 / 86

test/unit/prop/cnf_stream_white.cpp

90.7 %

117 / 129

39.9 %

205 / 514

test/unit/test.h

100.0 %

1 / 1

100.0 %

0 / 0

test/unit/test_api.h

100.0 %

1 / 1

50.0 %

1 / 2

test/unit/test_context.h

100.0 %

2 / 2

50.0 %

1 / 2

test/unit/test_node.h

100.0 %

10 / 10

50.0 %

6 / 12

test/unit/test_smt.h

54.8 %

40 / 73

19.9 %

30 / 151

test/unit/theory/evaluator_white.cpp

100.0 %

68 / 68

43.5 %

216 / 496

test/unit/theory/logic_info_white.cpp

99.8 %

1233 / 1236

32.5 %

4144 / 12768

test/unit/theory/regexp_operation_black.cpp

100.0 %

72 / 72

48.3 %

234 / 484

test/unit/theory/sequences_rewriter_white.cpp

100.0 %

760 / 760

46.7 %

2467 / 5286

test/unit/theory/strings_rewriter_white.cpp

100.0 %

15 / 15

42.7 %

47 / 110

test/unit/theory/theory_arith_white.cpp

100.0 %

52 / 52

38.6 %

155 / 402

test/unit/theory/theory_bags_normal_form_white.cpp

100.0 %

283 / 283

42.1 %

1079 / 2564

test/unit/theory/theory_bags_rewriter_white.cpp

100.0 %

433 / 433

41.4 %

1347 / 3250

test/unit/theory/theory_bags_type_rules_white.cpp

100.0 %

52 / 52

38.6 %

136 / 352

test/unit/theory/theory_black.cpp

100.0 %

86 / 86

34.7 %

328 / 944

test/unit/theory/theory_bv_int_blaster_white.cpp

100.0 %

1 / 1

50.0 %

3 / 6

test/unit/theory/theory_bv_opt_white.cpp

100.0 %

73 / 73

40.3 %

167 / 414

test/unit/theory/theory_bv_rewriter_white.cpp

100.0 %

30 / 30

45.8 %

87 / 190

test/unit/theory/theory_bv_white.cpp

100.0 %

37 / 37

46.9 %

105 / 224

test/unit/theory/theory_engine_white.cpp

98.7 %

78 / 79

45.8 %

198 / 432

test/unit/theory/theory_int_opt_white.cpp

100.0 %

65 / 65

41.6 %

139 / 334

test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp

100.0 %

285 / 285

33.1 %

1398 / 4228

test/unit/theory/theory_quantifiers_bv_inverter_white.cpp

98.3 %

927 / 943

44.4 %

637 / 1434

test/unit/theory/theory_sets_type_enumerator_white.cpp

100.0 %

80 / 80

34.4 %

259 / 752

test/unit/theory/theory_sets_type_rules_white.cpp

100.0 %

32 / 32

33.0 %

104 / 315

test/unit/theory/theory_strings_skolem_cache_black.cpp

100.0 %

15 / 15

46.8 %

58 / 124

test/unit/theory/theory_strings_utils_white.cpp

100.0 %

22 / 22

37.9 %

50 / 132

test/unit/theory/theory_strings_word_white.cpp

100.0 %

73 / 73

30.7 %

351 / 1142

test/unit/theory/theory_white.cpp

100.0 %

46 / 46

28.9 %

66 / 228

test/unit/theory/type_enumerator_white.cpp

100.0 %

201 / 201

33.9 %

962 / 2838

test/unit/util/array_store_all_white.cpp

100.0 %

31 / 31

40.9 %

108 / 264

test/unit/util/assert_white.cpp

100.0 %

27 / 27

23.3 %

179 / 768

test/unit/util/binary_heap_black.cpp

100.0 %

149 / 149

25.7 %

468 / 1818

test/unit/util/bitvector_black.cpp

100.0 %

124 / 124

28.1 %

476 / 1696

test/unit/util/boolean_simplification_black.cpp

100.0 %

131 / 131

47.4 %

502 / 1060

test/unit/util/cardinality_black.cpp

100.0 %

207 / 207

27.6 %

932 / 3374

test/unit/util/check_white.cpp

100.0 %

16 / 16

19.5 %

34 / 174

test/unit/util/configuration_black.cpp

100.0 %

26 / 26

25.9 %

30 / 116

test/unit/util/datatype_black.cpp

100.0 %

353 / 353

35.4 %

1100 / 3106

test/unit/util/exception_black.cpp

100.0 %

19 / 19

34.6 %

54 / 156

test/unit/util/floatingpoint_black.cpp

100.0 %

86 / 86

31.1 %

210 / 676

test/unit/util/integer_black.cpp

100.0 %

371 / 371

30.6 %

1164 / 3806

test/unit/util/integer_white.cpp

100.0 %

16 / 16

31.0 %

39 / 126

test/unit/util/output_black.cpp

100.0 %

76 / 76

37.0 %

182 / 492

test/unit/util/rational_black.cpp

100.0 %

16 / 16

30.7 %

83 / 270

test/unit/util/rational_white.cpp

100.0 %

288 / 288

30.5 %

770 / 2528

test/unit/util/real_algebraic_number_black.cpp

100.0 %

40 / 40

30.4 %

136 / 448

test/unit/util/stats_black.cpp

100.0 %

43 / 43

36.8 %

112 / 304


Generated by: GCOVR (Version 3.2)