Head

GCC Code Coverage Report

Directory:	.			Exec	Total	Coverage
Date:	2021-08-01		Lines:	147383	207434	71.1 %
Legend:	low: < 75.0 % medium: >= 75.0 % high: >= 90.0 %		Branches:	277738	786065	35.3 %

File

Lines

Branches

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

100.0 %

15 / 15

100.0 %

0 / 0

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

100.0 %

1 / 1

100.0 %

0 / 0

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

100.0 %

2 / 2

100.0 %

0 / 0

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

100.0 %

1 / 1

100.0 %

0 / 0

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

100.0 %

1 / 1

100.0 %

0 / 0

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

98.4 %

120 / 122

61.8 %

352 / 570

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

100.0 %

21 / 21

67.2 %

43 / 64

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

95.4 %

62 / 65

62.2 %

222 / 357

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

81.4 %

105 / 129

37.7 %

154 / 408

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

100.0 %

43 / 43

61.5 %

99 / 161

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

0.0 %

0 / 24

0.0 %

0 / 70

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

100.0 %

2 / 2

100.0 %

0 / 0

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

100.0 %

33 / 33

62.9 %

66 / 105

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

100.0 %

187 / 187

52.3 %

354 / 677

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

100.0 %

61 / 61

62.6 %

134 / 214

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

100.0 %

54 / 54

59.0 %

102 / 173

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

100.0 %

148 / 148

56.1 %

409 / 729

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

100.0 %

10 / 10

55.6 %

10 / 18

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

100.0 %

35 / 35

56.9 %

87 / 153

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

100.0 %

139 / 139

54.8 %

266 / 485

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

100.0 %

23 / 23

80.0 %

8 / 10

build-coverage/src/expr/kind.cpp

56.0 %

394 / 703

55.2 %

382 / 692

build-coverage/src/expr/kind.h

100.0 %

2 / 2

100.0 %

0 / 0

build-coverage/src/expr/metakind.cpp

78.1 %

580 / 743

46.4 %

366 / 788

build-coverage/src/expr/metakind.h

100.0 %

12 / 12

11.0 %

486 / 4400

build-coverage/src/expr/type_checker.cpp

90.4 %

852 / 942

51.8 %

1152 / 2223

build-coverage/src/expr/type_properties.h

34.9 %

37 / 106

18.5 %

47 / 254

build-coverage/src/options/arith_options.cpp

3.1 %

13 / 419

3.3 %

10 / 306

build-coverage/src/options/arith_options.h

81.2 %

95 / 117

100.0 %

0 / 0

build-coverage/src/options/arrays_options.cpp

2.7 %

1 / 37

9.1 %

2 / 22

build-coverage/src/options/arrays_options.h

100.0 %

15 / 15

100.0 %

0 / 0

build-coverage/src/options/base_options.cpp

6.3 %

7 / 111

8.3 %

6 / 72

build-coverage/src/options/base_options.h

81.0 %

17 / 21

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

16.2 %

30 / 185

17.6 %

26 / 148

build-coverage/src/options/bv_options.h

64.4 %

29 / 45

50.0 %

1 / 2

build-coverage/src/options/datatypes_options.cpp

5.6 %

6 / 107

6.9 %

5 / 72

build-coverage/src/options/datatypes_options.h

100.0 %

39 / 39

100.0 %

0 / 0

build-coverage/src/options/decision_options.cpp

8.0 %

10 / 125

7.6 %

9 / 119

build-coverage/src/options/decision_options.h

52.9 %

9 / 17

100.0 %

0 / 0

build-coverage/src/options/expr_options.cpp

7.7 %

1 / 13

20.0 %

2 / 10

build-coverage/src/options/expr_options.h

100.0 %

7 / 7

100.0 %

0 / 0

build-coverage/src/options/fp_options.cpp

11.1 %

1 / 9

25.0 %

2 / 8

build-coverage/src/options/fp_options.h

100.0 %

5 / 5

100.0 %

0 / 0

build-coverage/src/options/main_options.cpp

1.9 %

1 / 53

6.7 %

2 / 30

build-coverage/src/options/main_options.h

100.0 %

9 / 9

100.0 %

0 / 0

build-coverage/src/options/options.cpp

100.0 %

57 / 57

50.0 %

26 / 52

build-coverage/src/options/options.h

100.0 %

13 / 13

0.0 %

0 / 2

build-coverage/src/options/options_public.cpp

34.1 %

2722 / 7977

14.2 %

2629 / 18534

build-coverage/src/options/parser_options.cpp

4.0 %

1 / 25

12.5 %

2 / 16

build-coverage/src/options/parser_options.h

33.3 %

1 / 3

100.0 %

0 / 0

build-coverage/src/options/printer_options.cpp

8.8 %

5 / 57

7.1 %

4 / 56

build-coverage/src/options/printer_options.h

60.0 %

3 / 5

100.0 %

0 / 0

build-coverage/src/options/proof_options.cpp

1.4 %

1 / 69

3.1 %

2 / 65

build-coverage/src/options/proof_options.h

100.0 %

11 / 11

100.0 %

0 / 0

build-coverage/src/options/prop_options.cpp

2.7 %

1 / 37

9.1 %

2 / 22

build-coverage/src/options/prop_options.h

100.0 %

19 / 19

100.0 %

0 / 0

build-coverage/src/options/quantifiers_options.cpp

3.5 %

49 / 1399

3.0 %

32 / 1067

build-coverage/src/options/quantifiers_options.h

94.6 %

351 / 371

100.0 %

0 / 0

build-coverage/src/options/sep_options.cpp

4.0 %

1 / 25

12.5 %

2 / 16

build-coverage/src/options/sep_options.h

100.0 %

11 / 11

100.0 %

0 / 0

build-coverage/src/options/sets_options.cpp

7.7 %

1 / 13

20.0 %

2 / 10

build-coverage/src/options/sets_options.h

100.0 %

7 / 7

100.0 %

0 / 0

build-coverage/src/options/smt_options.cpp

12.6 %

54 / 427

10.0 %

34 / 340

build-coverage/src/options/smt_options.h

91.6 %

87 / 95

100.0 %

0 / 0

build-coverage/src/options/strings_options.cpp

0.7 %

1 / 137

2.0 %

2 / 101

build-coverage/src/options/strings_options.h

100.0 %

39 / 39

100.0 %

0 / 0

build-coverage/src/options/theory_options.cpp

14.7 %

11 / 75

10.5 %

8 / 76

build-coverage/src/options/theory_options.h

100.0 %

13 / 13

100.0 %

0 / 0

build-coverage/src/options/uf_options.cpp

8.5 %

5 / 59

8.7 %

4 / 46

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

940 / 1584

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

72.7 %

3310 / 4554

45.4 %

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

3075 / 4840

42.5 %

2041 / 4807

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

src/api/cpp/cvc5.cpp

76.4 %

2511 / 3288

27.4 %

6906 / 25232

src/api/cpp/cvc5.h

68.4 %

13 / 19

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

76.2 %

109 / 143

40.1 %

117 / 292

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

16.3 %

146 / 894

src/context/backtrackable.h

4.9 %

2 / 41

1.2 %

1 / 84

src/context/cdhashmap.h

97.7 %

125 / 128

39.7 %

517 / 1303

src/context/cdhashset.h

83.3 %

35 / 42

9.1 %

4 / 44

src/context/cdinsert_hashmap.h

98.1 %

102 / 104

32.5 %

214 / 658

src/context/cdlist.h

96.0 %

143 / 149

37.1 %

926 / 2496

src/context/cdlist_forward.h

100.0 %

1 / 1

100.0 %

0 / 0

src/context/cdmaybe.h

100.0 %

22 / 22

20.0 %

12 / 60

src/context/cdo.h

100.0 %

33 / 33

48.3 %

84 / 174

src/context/cdqueue.h

100.0 %

48 / 48

21.6 %

113 / 524

src/context/cdtrail_queue.h

100.0 %

23 / 23

17.5 %

7 / 40

src/context/context.cpp

86.4 %

171 / 198

36.3 %

211 / 582

src/context/context.h

85.7 %

54 / 63

34.1 %

28 / 82

src/context/context_mm.cpp

93.5 %

58 / 62

36.0 %

36 / 100

src/decision/assertion_list.cpp

83.6 %

51 / 61

45.3 %

73 / 161

src/decision/assertion_list.h

100.0 %

1 / 1

100.0 %

0 / 0

src/decision/decision_engine.cpp

100.0 %

20 / 20

33.3 %

2 / 6

src/decision/decision_engine.h

100.0 %

4 / 4

100.0 %

0 / 0

src/decision/decision_engine_old.cpp

61.0 %

25 / 41

24.7 %

40 / 162

src/decision/decision_engine_old.h

66.7 %

10 / 15

34.6 %

9 / 26

src/decision/decision_strategy.h

0.0 %

0 / 8

100.0 %

0 / 0

src/decision/justification_heuristic.cpp

0.5 %

2 / 378

0.1 %

2 / 1509

src/decision/justification_heuristic.h

0.0 %

0 / 3

0.0 %

0 / 6

src/decision/justification_strategy.cpp

97.8 %

273 / 279

43.7 %

502 / 1148

src/decision/justification_strategy.h

100.0 %

1 / 1

100.0 %

0 / 0

src/decision/justify_info.cpp

80.0 %

16 / 20

20.0 %

6 / 30

src/decision/justify_stack.cpp

92.7 %

38 / 41

24.0 %

25 / 104

src/decision/justify_stats.cpp

100.0 %

16 / 16

50.0 %

14 / 28

src/expr/array_store_all.cpp

53.7 %

22 / 41

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

58.3 %

14 / 24

src/expr/kind_map.h

100.0 %

8 / 8

66.7 %

4 / 6

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

0.7 %

1 / 135

0.4 %

2 / 447

src/expr/node.cpp

84.0 %

42 / 50

50.9 %

115 / 226

src/expr/node.h

82.6 %

300 / 363

22.9 %

801 / 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_converter.cpp

0.7 %

1 / 138

0.3 %

2 / 756

src/expr/node_converter.h

0.0 %

0 / 1

100.0 %

0 / 0

src/expr/node_manager.cpp

86.2 %

500 / 580

37.0 %

655 / 1772

src/expr/node_manager.h

90.2 %

174 / 193

26.9 %

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

76.1 %

108 / 142

23.0 %

43 / 187

src/expr/node_visitor.h

100.0 %

33 / 33

50.0 %

89 / 178

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

94.2 %

161 / 171

40.7 %

319 / 783

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

73.2 %

41 / 56

51.6 %

33 / 64

src/expr/term_context.h

100.0 %

10 / 10

100.0 %

0 / 0

src/expr/term_context_node.cpp

13.3 %

4 / 30

4.3 %

6 / 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/type_checker_util.h

75.0 %

36 / 48

11.0 %

171 / 1552

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

84.2 %

283 / 336

36.7 %

383 / 1044

src/expr/type_node.h

83.3 %

160 / 192

20.7 %

150 / 723

src/expr/uninterpreted_constant.cpp

64.9 %

24 / 37

38.2 %

29 / 76

src/main/command_executor.cpp

76.3 %

74 / 97

55.8 %

106 / 190

src/main/command_executor.h

100.0 %

6 / 6

100.0 %

0 / 0

src/main/driver_unified.cpp

55.5 %

81 / 146

26.8 %

84 / 314

src/main/interactive_shell.cpp

67.4 %

60 / 89

35.3 %

100 / 283

src/main/main.cpp

87.5 %

14 / 16

50.9 %

27 / 53

src/main/main.h

100.0 %

1 / 1

100.0 %

0 / 0

src/main/signal_handlers.cpp

29.8 %

39 / 131

12.0 %

13 / 108

src/main/time_limit.cpp

72.7 %

16 / 22

27.3 %

6 / 22

src/omt/bitvector_optimizer.cpp

88.8 %

95 / 107

48.1 %

174 / 362

src/omt/bitvector_optimizer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/omt/integer_optimizer.cpp

100.0 %

28 / 28

46.4 %

39 / 84

src/omt/integer_optimizer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/omt/omt_optimizer.cpp

45.9 %

34 / 74

9.5 %

60 / 632

src/omt/omt_optimizer.h

100.0 %

2 / 2

100.0 %

0 / 0

src/options/didyoumean.cpp

1.5 %

1 / 68

2.1 %

2 / 96

src/options/didyoumean.h

0.0 %

0 / 3

100.0 %

0 / 0

src/options/language.cpp

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

3.2 %

1 / 31

2.6 %

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

41.5 %

114 / 275

22.6 %

122 / 540

src/options/options_handler.h

0.0 %

0 / 14

0.0 %

0 / 42

src/options/options_listener.h

100.0 %

2 / 2

100.0 %

0 / 0

src/options/outputc.cpp

100.0 %

8 / 8

50.0 %

5 / 10

src/options/outputc.h

100.0 %

1 / 1

100.0 %

0 / 0

src/options/printer_modes.cpp

12.5 %

1 / 8

28.6 %

2 / 7

src/options/set_language.cpp

100.0 %

29 / 29

64.3 %

9 / 14

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 %

365 / 499

34.1 %

452 / 1327

src/parser/parser.h

69.7 %

23 / 33

16.7 %

1 / 6

src/parser/parser_builder.cpp

97.3 %

73 / 75

61.0 %

25 / 41

src/parser/parser_builder.h

100.0 %

1 / 1

100.0 %

0 / 0

src/parser/parser_exception.h

85.0 %

17 / 20

75.0 %

3 / 4

src/parser/smt2/smt2.cpp

87.4 %

591 / 676

47.6 %

1050 / 2204

src/parser/smt2/smt2.h

63.6 %

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

81.2 %

216 / 266

37.0 %

300 / 810

src/parser/tptp/tptp.h

71.4 %

5 / 7

100.0 %

0 / 0

src/parser/tptp/tptp_input.cpp

83.3 %

20 / 24

25.0 %

14 / 56

src/preprocessing/assertion_pipeline.cpp

100.0 %

86 / 86

38.6 %

135 / 350

src/preprocessing/assertion_pipeline.h

100.0 %

14 / 14

100.0 %

4 / 4

src/preprocessing/learned_literal_manager.cpp

100.0 %

18 / 18

50.0 %

27 / 54

src/preprocessing/learned_literal_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/ackermann.cpp

97.3 %

108 / 111

41.4 %

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

426 / 476

41.4 %

852 / 2060

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

87.7 %

121 / 138

41.4 %

261 / 630

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

67 / 446

src/preprocessing/passes/ite_simp.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/learned_rewrite.cpp

54.1 %

120 / 222

24.0 %

214 / 892

src/preprocessing/passes/learned_rewrite.h

100.0 %

1 / 1

100.0 %

0 / 0

src/preprocessing/passes/miplib_trick.cpp

11.6 %

42 / 363

2.4 %

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 %

217 / 225

41.5 %

490 / 1182

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

91.4 %

32 / 35

44.1 %

15 / 34

src/preprocessing/preprocessing_pass_context.h

100.0 %

8 / 8

100.0 %

0 / 0

src/preprocessing/preprocessing_pass_registry.cpp

100.0 %

56 / 56

48.1 %

152 / 316

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

357 / 1016

22.2 %

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

50.7 %

605 / 1193

31.2 %

988 / 3168

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

75.0 %

33 / 44

32.9 %

52 / 158

src/proof/buffered_proof_generator.h

100.0 %

2 / 2

50.0 %

1 / 2

src/proof/conv_proof_generator.cpp

84.1 %

265 / 315

35.0 %

559 / 1599

src/proof/conv_seq_proof_generator.cpp

70.5 %

55 / 78

23.0 %

70 / 304

src/proof/dot/dot_printer.cpp

1.2 %

2 / 167

0.8 %

3 / 396

src/proof/eager_proof_generator.cpp

93.7 %

59 / 63

40.9 %

81 / 198

src/proof/eager_proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/lazy_proof.cpp

96.9 %

94 / 97

48.0 %

168 / 350

src/proof/lazy_proof_chain.cpp

73.0 %

116 / 159

31.5 %

169 / 536

src/proof/lazy_tree_proof_generator.cpp

78.1 %

50 / 64

29.6 %

42 / 142

src/proof/lazy_tree_proof_generator.h

92.9 %

13 / 14

64.3 %

9 / 14

src/proof/lfsc/lfsc_util.cpp

2.7 %

1 / 37

5.4 %

2 / 37

src/proof/lfsc/lfsc_util.h

0.0 %

0 / 1

100.0 %

0 / 0

src/proof/method_id.cpp

55.8 %

29 / 52

45.3 %

39 / 86

src/proof/proof.cpp

80.2 %

170 / 212

42.4 %

391 / 922

src/proof/proof_checker.cpp

56.4 %

92 / 163

20.5 %

127 / 620

src/proof/proof_checker.h

75.0 %

3 / 4

100.0 %

0 / 0

src/proof/proof_ensure_closed.cpp

15.8 %

12 / 76

4.6 %

19 / 410

src/proof/proof_generator.cpp

46.2 %

12 / 26

20.0 %

24 / 120

src/proof/proof_generator.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_letify.cpp

2.2 %

1 / 46

1.8 %

2 / 110

src/proof/proof_letify.h

0.0 %

0 / 1

100.0 %

0 / 0

src/proof/proof_node.cpp

100.0 %

27 / 27

45.0 %

9 / 20

src/proof/proof_node.h

100.0 %

3 / 3

50.0 %

2 / 4

src/proof/proof_node_algorithm.cpp

72.0 %

54 / 75

36.4 %

59 / 162

src/proof/proof_node_manager.cpp

80.9 %

152 / 188

31.9 %

258 / 810

src/proof/proof_node_manager.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_node_to_sexpr.cpp

79.7 %

63 / 79

33.7 %

97 / 288

src/proof/proof_node_to_sexpr.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_node_updater.cpp

77.2 %

98 / 127

36.9 %

130 / 352

src/proof/proof_node_updater.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/proof_rule.cpp

16.9 %

30 / 178

14.3 %

23 / 161

src/proof/proof_set.h

100.0 %

7 / 7

66.7 %

10 / 15

src/proof/proof_step_buffer.cpp

59.1 %

26 / 44

20.0 %

18 / 90

src/proof/proof_step_buffer.h

100.0 %

2 / 2

25.0 %

1 / 4

src/proof/theory_proof_step_buffer.cpp

81.0 %

81 / 100

40.9 %

140 / 342

src/proof/theory_proof_step_buffer.h

100.0 %

1 / 1

100.0 %

0 / 0

src/proof/trust_node.cpp

77.4 %

48 / 62

34.7 %

70 / 202

src/proof/trust_node.h

100.0 %

3 / 3

100.0 %

0 / 0

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

48.4 %

77 / 159

23.9 %

56 / 234

src/prop/bvminisat/bvminisat.h

60.0 %

9 / 15

0.0 %

0 / 6

src/prop/bvminisat/core/Solver.cc

55.5 %

361 / 651

25.2 %

356 / 1413

src/prop/bvminisat/core/Solver.h

76.7 %

56 / 73

46.5 %

40 / 86

src/prop/bvminisat/core/SolverTypes.h

94.7 %

124 / 131

35.9 %

61 / 170

src/prop/bvminisat/mtl/Alg.h

100.0 %

11 / 11

45.5 %

25 / 55

src/prop/bvminisat/mtl/Alloc.h

95.7 %

45 / 47

19.4 %

21 / 108

src/prop/bvminisat/mtl/Heap.h

89.6 %

69 / 77

28.2 %

35 / 124

src/prop/bvminisat/mtl/Queue.h

96.4 %

27 / 28

25.6 %

20 / 78

src/prop/bvminisat/mtl/Sort.h

92.6 %

25 / 27

46.9 %

15 / 32

src/prop/bvminisat/mtl/Vec.h

97.8 %

45 / 46

38.6 %

132 / 342

src/prop/bvminisat/mtl/XAlloc.h

80.0 %

4 / 5

25.0 %

1 / 4

src/prop/bvminisat/simp/SimpSolver.cc

72.2 %

293 / 406

36.1 %

352 / 974

src/prop/bvminisat/simp/SimpSolver.h

89.5 %

17 / 19

44.1 %

15 / 34

src/prop/bvminisat/utils/Options.h

23.9 %

22 / 92

5.6 %

4 / 72

src/prop/bvminisat/utils/ParseUtils.h

0.0 %

0 / 6

0.0 %

0 / 4

src/prop/cadical.cpp

76.5 %

65 / 85

27.1 %

39 / 144

src/prop/cnf_stream.cpp

93.7 %

386 / 412

37.9 %

756 / 1997

src/prop/cnf_stream.h

100.0 %

1 / 1

100.0 %

0 / 0

src/prop/cryptominisat.cpp

66.7 %

72 / 108

26.0 %

53 / 204

src/prop/cryptominisat.h

0.0 %

0 / 1

100.0 %

0 / 0

src/prop/minisat/core/Solver.cc

83.3 %

855 / 1026

42.1 %

1185 / 2814

src/prop/minisat/core/Solver.h

94.7 %

108 / 114

44.1 %

98 / 222

src/prop/minisat/core/SolverTypes.h

87.5 %

140 / 160

35.3 %

67 / 190

src/prop/minisat/minisat.cpp

81.3 %

143 / 176

32.2 %

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

416 / 1068

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

75.3 %

262 / 348

31.7 %

388 / 1224

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 %

308 / 427

30.1 %

627 / 2080

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

98.8 %

82 / 83

43.5 %

108 / 248

src/prop/theory_proxy.cpp

94.2 %

98 / 104

42.0 %

136 / 324

src/smt/abduction_solver.cpp

83.8 %

83 / 99

38.8 %

167 / 430

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

696 / 1274

33.0 %

519 / 1575

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

95.3 %

41 / 43

32.9 %

23 / 70

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

27.3 %

24 / 88

18.0 %

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

0.0 %

0 / 8

src/smt/optimization_solver.cpp

64.2 %

120 / 187

36.2 %

143 / 395

src/smt/optimization_solver.h

100.0 %

20 / 20

50.0 %

5 / 10

src/smt/options_manager.cpp

77.0 %

47 / 61

35.2 %

62 / 176

src/smt/output_manager.cpp

100.0 %

5 / 5

50.0 %

2 / 4

src/smt/preprocess_proof_generator.cpp

93.1 %

108 / 116

43.9 %

243 / 554

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

93.0 %

173 / 186

49.6 %

385 / 776

src/smt/proof_manager.cpp

76.7 %

69 / 90

30.5 %

100 / 328

src/smt/proof_post_processor.cpp

91.9 %

554 / 603

38.7 %

1081 / 2790

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

81.9 %

598 / 730

52.5 %

1390 / 2648

src/smt/smt_engine.cpp

82.3 %

854 / 1038

37.5 %

1238 / 3301

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 %

17 / 17

50.0 %

12 / 24

src/smt/smt_mode.cpp

8.3 %

1 / 12

16.7 %

2 / 12

src/smt/smt_solver.cpp

89.6 %

95 / 106

46.8 %

148 / 316

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 %

328 / 726

src/smt/term_formula_removal.cpp

96.9 %

218 / 225

49.0 %

443 / 904

src/smt/unsat_core_manager.cpp

93.3 %

42 / 45

36.9 %

62 / 168

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

0.1 %

2 / 1336

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

461 / 520

42.1 %

1082 / 2569

src/theory/arith/arith_rewriter.h

100.0 %

3 / 3

25.0 %

1 / 4

src/theory/arith/arith_state.cpp

100.0 %

8 / 8

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

28.6 %

16 / 56

src/theory/arith/bound_counts.h

85.6 %

83 / 97

29.6 %

48 / 162

src/theory/arith/bound_inference.cpp

64.7 %

88 / 136

37.6 %

171 / 455

src/theory/arith/bound_inference.h

100.0 %

2 / 2

50.0 %

15 / 30

src/theory/arith/branch_and_bound.cpp

95.4 %

62 / 65

44.2 %

206 / 466

src/theory/arith/branch_and_bound.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/callbacks.cpp

87.7 %

100 / 114

24.0 %

112 / 466

src/theory/arith/callbacks.h

100.0 %

13 / 13

50.0 %

5 / 10

src/theory/arith/congruence_manager.cpp

87.1 %

358 / 411

37.5 %

718 / 1914

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

84.8 %

78 / 92

53.5 %

46 / 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/equality_solver.cpp

69.6 %

39 / 56

32.9 %

46 / 140

src/theory/arith/equality_solver.h

100.0 %

6 / 6

100.0 %

0 / 0

src/theory/arith/error_set.cpp

64.0 %

197 / 308

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

76.7 %

56 / 73

33.0 %

60 / 182

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

70.4 %

238 / 338

34.8 %

412 / 1184

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

100.0 %

2 / 2

100.0 %

0 / 0

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

80.1 %

133 / 166

41.9 %

192 / 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/lazard_evaluation.cpp

35.3 %

6 / 17

6.7 %

2 / 30

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

100.0 %

42 / 42

55.3 %

52 / 94

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

33.3 %

2 / 6

0.0 %

0 / 4

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

93.8 %

15 / 16

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 %

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

30.0 %

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

50 / 54

48.5 %

96 / 198

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

100.0 %

1 / 1

41.2 %

14 / 34

src/theory/arith/nl/nonlinear_extension.cpp

89.5 %

291 / 325

50.6 %

495 / 979

src/theory/arith/nl/nonlinear_extension.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/poly_conversion.cpp

58.2 %

231 / 397

22.1 %

384 / 1738

src/theory/arith/nl/poly_conversion.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/arith/nl/pow2_solver.cpp

95.7 %

89 / 93

48.2 %

189 / 392

src/theory/arith/nl/stats.cpp

100.0 %

5 / 5

50.0 %

6 / 12

src/theory/arith/nl/strategy.cpp

61.1 %

66 / 108

41.8 %

124 / 297

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 %

644 / 795

36.9 %

1099 / 2978

src/theory/arith/normal_form.h

98.2 %

375 / 382

38.0 %

421 / 1107

src/theory/arith/operator_elim.cpp

93.3 %

182 / 195

49.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/pp_rewrite_eq.cpp

100.0 %

19 / 19

40.8 %

53 / 130

src/theory/arith/pp_rewrite_eq.h

100.0 %

1 / 1

100.0 %

0 / 0

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

91.2 %

134 / 147

42.7 %

165 / 386

src/theory/arith/theory_arith.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/arith/theory_arith_private.cpp

59.2 %

1752 / 2958

27.4 %

3430 / 12530

src/theory/arith/theory_arith_private.h

85.3 %

29 / 34

35.7 %

15 / 42

src/theory/arith/theory_arith_type_rules.cpp

76.1 %

54 / 71

32.2 %

73 / 227

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

69.2 %

45 / 65

23.4 %

108 / 462

src/theory/arrays/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/arrays/skolem_cache.cpp

96.4 %

27 / 28

30.8 %

61 / 198

src/theory/arrays/theory_arrays.cpp

71.8 %

867 / 1207

36.2 %

2338 / 6451

src/theory/arrays/theory_arrays.h

97.6 %

41 / 42

55.6 %

60 / 108

src/theory/arrays/theory_arrays_rewriter.cpp

98.6 %

351 / 356

52.8 %

852 / 1615

src/theory/arrays/theory_arrays_rewriter.h

100.0 %

3 / 3

50.0 %

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

71.3 %

92 / 129

26.2 %

179 / 684

src/theory/booleans/circuit_propagator.cpp

93.0 %

348 / 374

48.9 %

875 / 1790

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 %

230 / 251

49.6 %

547 / 1102

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 %

223 / 231

55.4 %

884 / 1597

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

74.7 %

174 / 233

31.0 %

313 / 1010

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 %

17 / 17

41.9 %

26 / 62

src/theory/builtin/theory_builtin_type_rules.h

73.6 %

64 / 87

37.4 %

152 / 406

src/theory/builtin/type_enumerator.cpp

6.7 %

1 / 15

3.6 %

2 / 56

src/theory/builtin/type_enumerator.h

88.9 %

24 / 27

41.7 %

35 / 84

src/theory/bv/abstraction.cpp

1.1 %

7 / 626

0.3 %

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

62.6 %

67 / 107

5.0 %

13 / 262

src/theory/bv/bitblast/eager_bitblaster.cpp

52.3 %

69 / 132

16.9 %

96 / 569

src/theory/bv/bitblast/eager_bitblaster.h

75.0 %

3 / 4

50.0 %

1 / 2

src/theory/bv/bitblast/lazy_bitblaster.cpp

0.3 %

1 / 304

0.2 %

2 / 1105

src/theory/bv/bitblast/lazy_bitblaster.h

0.0 %

0 / 7

100.0 %

0 / 0

src/theory/bv/bitblast/node_bitblaster.cpp

94.7 %

72 / 76

39.9 %

118 / 296

src/theory/bv/bitblast/node_bitblaster.h

50.0 %

1 / 2

0.0 %

0 / 4

src/theory/bv/bitblast/proof_bitblaster.cpp

100.0 %

76 / 76

56.3 %

151 / 268

src/theory/bv/bv_eager_solver.cpp

14.9 %

7 / 47

2.5 %

5 / 200

src/theory/bv/bv_inequality_graph.cpp

0.3 %

1 / 300

0.2 %

2 / 1247

src/theory/bv/bv_inequality_graph.h

0.0 %

0 / 41

0.0 %

0 / 82

src/theory/bv/bv_quick_check.cpp

0.5 %

1 / 189

0.6 %

2 / 348

src/theory/bv/bv_quick_check.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/bv/bv_solver.h

75.0 %

21 / 28

12.5 %

1 / 8

src/theory/bv/bv_solver_bitblast.cpp

95.2 %

157 / 165

48.1 %

297 / 618

src/theory/bv/bv_solver_bitblast.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/bv/bv_solver_bitblast_internal.cpp

97.4 %

76 / 78

56.3 %

144 / 256

src/theory/bv/bv_solver_bitblast_internal.h

75.0 %

3 / 4

0.0 %

0 / 2

src/theory/bv/bv_solver_layered.cpp

10.0 %

32 / 320

2.7 %

36 / 1340

src/theory/bv/bv_solver_layered.h

0.0 %

0 / 21

0.0 %

0 / 42

src/theory/bv/bv_subtheory.h

0.0 %

0 / 30

0.0 %

0 / 35

src/theory/bv/bv_subtheory_algebraic.cpp

0.2 %

1 / 600

0.1 %

2 / 2425

src/theory/bv/bv_subtheory_algebraic.h

0.0 %

0 / 18

0.0 %

0 / 10

src/theory/bv/bv_subtheory_bitblast.cpp

0.7 %

1 / 142

0.4 %

2 / 484

src/theory/bv/bv_subtheory_bitblast.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/bv/bv_subtheory_core.cpp

0.5 %

1 / 198

0.3 %

2 / 729

src/theory/bv/bv_subtheory_core.h

0.0 %

0 / 6

100.0 %

0 / 0

src/theory/bv/bv_subtheory_inequality.cpp

0.7 %

1 / 139

0.3 %

2 / 640

src/theory/bv/bv_subtheory_inequality.h

0.0 %

0 / 6

0.0 %

0 / 10

src/theory/bv/int_blaster.cpp

1.2 %

1 / 81

0.9 %

2 / 228

src/theory/bv/proof_checker.cpp

95.7 %

22 / 23

16.5 %

26 / 158

src/theory/bv/proof_checker.h

100.0 %

2 / 2

0.0 %

0 / 6

src/theory/bv/slicer.cpp

3.1 %

1 / 32

3.1 %

2 / 64

src/theory/bv/slicer.h

0.0 %

0 / 1

100.0 %

0 / 0

src/theory/bv/theory_bv.cpp

98.9 %

180 / 182

48.6 %

301 / 619

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

5104 / 21797

src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h

87.7 %

135 / 154

44.3 %

334 / 754

src/theory/bv/theory_bv_rewrite_rules_core.h

100.0 %

144 / 144

57.6 %

265 / 460

src/theory/bv/theory_bv_rewrite_rules_normalization.h

76.6 %

556 / 726

38.4 %

1121 / 2919

src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h

75.8 %

270 / 356

34.3 %

441 / 1284

src/theory/bv/theory_bv_rewrite_rules_simplification.h

82.9 %

619 / 747

42.2 %

1810 / 4290

src/theory/bv/theory_bv_rewriter.cpp

95.9 %

324 / 338

51.2 %

483 / 944

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

83.3 %

5 / 6

40.0 %

8 / 20

src/theory/bv/theory_bv_utils.cpp

64.3 %

153 / 238

28.1 %

228 / 812

src/theory/bv/theory_bv_utils.h

22.2 %

4 / 18

16.7 %

17 / 102

src/theory/bv/type_enumerator.h

100.0 %

13 / 13

55.0 %

11 / 20

src/theory/care_graph.h

100.0 %

10 / 10

83.3 %

15 / 18

src/theory/combination_care_graph.cpp

100.0 %

34 / 34

52.2 %

48 / 92

src/theory/combination_engine.cpp

95.6 %

43 / 45

31.8 %

35 / 110

src/theory/datatypes/datatypes_rewriter.cpp

93.8 %

480 / 512

46.2 %

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

35.1 %

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

65 / 65

54.9 %

135 / 246

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

88.3 %

309 / 350

39.7 %

628 / 1582

src/theory/datatypes/sygus_extension.cpp

85.0 %

857 / 1008

40.2 %

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

560 / 1106

src/theory/datatypes/sygus_simple_sym.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/datatypes/theory_datatypes.cpp

85.5 %

962 / 1125

43.4 %

2237 / 5150

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

92.3 %

12 / 13

50.0 %

10 / 20

src/theory/ee_manager.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/ee_manager_central.cpp

97.9 %

138 / 141

48.2 %

214 / 444

src/theory/ee_manager_central.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/ee_manager_distributed.cpp

97.7 %

43 / 44

36.2 %

42 / 116

src/theory/ee_setup_info.h

100.0 %

8 / 8

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

64.8 %

162 / 250

38.7 %

276 / 713

src/theory/ext_theory.h

100.0 %

7 / 7

50.0 %

1 / 2

src/theory/fp/fp_converter.cpp

86.5 %

521 / 602

32.6 %

1386 / 4255

src/theory/fp/fp_converter.h

100.0 %

5 / 5

100.0 %

0 / 0

src/theory/fp/fp_expand_defs.cpp

62.0 %

80 / 129

24.1 %

152 / 630

src/theory/fp/fp_expand_defs.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/fp/theory_fp.cpp

71.7 %

335 / 467

27.6 %

717 / 2600

src/theory/fp/theory_fp.h

85.7 %

6 / 7

0.0 %

0 / 2

src/theory/fp/theory_fp_rewriter.cpp

77.9 %

594 / 763

25.9 %

1032 / 3981

src/theory/fp/theory_fp_rewriter.h

100.0 %

1 / 1

50.0 %

2 / 4

src/theory/fp/theory_fp_type_rules.cpp

72.2 %

208 / 288

29.8 %

456 / 1530

src/theory/fp/type_enumerator.h

50.0 %

27 / 54

24.3 %

17 / 70

src/theory/incomplete_id.cpp

3.7 %

1 / 27

9.5 %

2 / 21

src/theory/inference_id.cpp

0.8 %

3 / 358

1.1 %

3 / 282

src/theory/inference_manager_buffered.cpp

93.1 %

81 / 87

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

90.8 %

385 / 424

57.9 %

411 / 710

src/theory/logic_info.h

100.0 %

23 / 23

83.3 %

15 / 18

src/theory/model_manager.cpp

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

475 / 1060

src/theory/quantifiers/bv_inverter.h

100.0 %

6 / 6

50.0 %

4 / 8

src/theory/quantifiers/bv_inverter_utils.cpp

98.9 %

811 / 820

48.7 %

2608 / 5352

src/theory/quantifiers/candidate_rewrite_database.cpp

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

86.3 %

455 / 527

42.5 %

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

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

816 / 891

49.5 %

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

263 / 281

47.5 %

471 / 992

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 %

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

96.2 %

178 / 185

42.6 %

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

40.9 %

466 / 1138

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

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

25.0 %

4 / 16

src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp

75.4 %

267 / 354

36.9 %

496 / 1345

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

81.7 %

94 / 115

36.5 %

167 / 458

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

75.4 %

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

88.9 %

40 / 45

38.3 %

49 / 128

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

86.0 %

723 / 841

46.4 %

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

495 / 529

45.3 %

1230 / 2716

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

95.1 %

763 / 802

51.2 %

1671 / 3265

src/theory/quantifiers/fmf/full_model_check.h

100.0 %

13 / 13

50.0 %

3 / 6

src/theory/quantifiers/fmf/model_builder.cpp

54.2 %

39 / 72

18.8 %

45 / 240

src/theory/quantifiers/fmf/model_builder.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/quantifiers/fmf/model_engine.cpp

70.3 %

137 / 195

33.8 %

235 / 695

src/theory/quantifiers/fmf/model_engine.h

100.0 %

1 / 1

50.0 %

1 / 2

src/theory/quantifiers/fun_def_evaluator.cpp

90.8 %

138 / 152

42.3 %

328 / 776

src/theory/quantifiers/fun_def_evaluator.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/index_trie.cpp

97.7 %

42 / 43

56.1 %

55 / 98

src/theory/quantifiers/index_trie.h

100.0 %

9 / 9

100.0 %

0 / 0

src/theory/quantifiers/inst_match.cpp

56.5 %

26 / 46

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 %

143 / 322

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

74 / 189

src/theory/quantifiers/inst_strategy_pool.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/quantifiers/instantiate.cpp

80.0 %

276 / 345

38.0 %

535 / 1408

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

100.0 %

5 / 5

37.5 %

3 / 8

src/theory/quantifiers/master_eq_notify.h

37.5 %

3 / 8

100.0 %

0 / 0

src/theory/quantifiers/proof_checker.cpp

68.3 %

43 / 63

22.3 %

69 / 310

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

83.0 %

1159 / 1397

45.4 %

2480 / 5459

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

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

71.4 %

5 / 7

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

66.3 %

65 / 98

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

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

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

28.2 %

48 / 170

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

326 / 1120

src/theory/quantifiers/sygus/enum_stream_substitution.h

100.0 %

6 / 6

50.0 %

2 / 4

src/theory/quantifiers/sygus/enum_val_generator.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/quantifiers/sygus/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

49.1 %

221 / 450

src/theory/quantifiers/sygus/sygus_enumerator.cpp

97.3 %

649 / 667

44.3 %

1045 / 2358

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

2 / 44

src/theory/quantifiers/sygus/sygus_enumerator_basic.h

0.0 %

0 / 4

0.0 %

0 / 2

src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp

2.4 %

1 / 41

1.5 %

2 / 130

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

589 / 1432

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 %

745 / 823

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

33.3 %

14 / 42

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

594 / 677

40.8 %

1233 / 3020

src/theory/quantifiers/sygus/synth_conjecture.h

100.0 %

7 / 7

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

91.3 %

42 / 46

42.5 %

85 / 200

src/theory/quantifiers/sygus/template_infer.cpp

97.9 %

94 / 96

44.6 %

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

468 / 543

42.3 %

855 / 2021

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

380 / 1026

src/theory/quantifiers/sygus_inst.h

100.0 %

2 / 2

50.0 %

1 / 2

src/theory/quantifiers/sygus_sampler.cpp

79.3 %

367 / 463

38.2 %

588 / 1540

src/theory/quantifiers/sygus_sampler.h

100.0 %

3 / 3

100.0 %

0 / 0

src/theory/quantifiers/term_database.cpp

81.5 %

551 / 676

42.7 %

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

52 / 58

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

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

54.9 %

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

295 / 350

42.7 %

536 / 1254

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

189 / 254

35.4 %

290 / 820

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 %

922 / 1088

41.8 %

2282 / 5464

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 %

1229 / 2595

src/theory/sets/cardinality_extension.h

100.0 %

4 / 4

100.0 %

0 / 0

src/theory/sets/inference_manager.cpp

52.2 %

47 / 90

25.7 %

104 / 404

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

91.8 %

101 / 110

43.7 %

138 / 316

src/theory/sets/theory_sets.h

80.0 %

4 / 5

0.0 %

0 / 2

src/theory/sets/theory_sets_private.cpp

94.0 %

671 / 714

47.0 %

1470 / 3129

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

328 / 344

49.2 %

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

92.0 %

46 / 50

56.0 %

75 / 134

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

135 / 158

32.1 %

224 / 698

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

82.0 %

41 / 50

35.1 %

47 / 134

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 %

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

1103 / 1371

40.1 %

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

84.1 %

301 / 358

44.3 %

781 / 1762

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

453 / 537

40.9 %

892 / 2180

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

84.8 %

251 / 296

34.9 %

645 / 1846

src/theory/strings/proof_checker.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/strings/regexp_elim.cpp

93.0 %

278 / 299

45.1 %

620 / 1374

src/theory/strings/regexp_elim.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/regexp_entail.cpp

87.4 %

347 / 397

48.2 %

721 / 1495

src/theory/strings/regexp_operation.cpp

71.4 %

698 / 977

36.2 %

1485 / 4106

src/theory/strings/regexp_solver.cpp

89.4 %

296 / 331

48.2 %

592 / 1227

src/theory/strings/regexp_solver.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/rewrites.cpp

0.5 %

1 / 200

1.0 %

2 / 196

src/theory/strings/sequences_rewriter.cpp

96.5 %

1592 / 1649

52.1 %

5039 / 9664

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

127 / 139

48.7 %

288 / 591

src/theory/strings/skolem_cache.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/strings/solver_state.cpp

96.2 %

102 / 106

46.7 %

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

88.4 %

275 / 311

45.6 %

655 / 1436

src/theory/strings/theory_strings.cpp

82.0 %

479 / 584

41.4 %

1006 / 2429

src/theory/strings/theory_strings.h

100.0 %

32 / 32

52.3 %

69 / 132

src/theory/strings/theory_strings_preprocess.cpp

100.0 %

518 / 518

51.1 %

1566 / 3064

src/theory/strings/theory_strings_type_rules.cpp

70.8 %

97 / 137

26.3 %

122 / 464

src/theory/strings/theory_strings_utils.cpp

92.2 %

188 / 204

47.7 %

351 / 736

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

83.8 %

233 / 278

48.3 %

482 / 997

src/theory/theory.h

75.5 %

71 / 94

41.2 %

70 / 170

src/theory/theory_engine.cpp

81.3 %

739 / 909

40.9 %

1825 / 4458

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

100.0 %

19 / 19

58.3 %

14 / 24

src/theory/theory_id.cpp

85.9 %

67 / 78

57.7 %

56 / 97

src/theory/theory_inference.cpp

76.5 %

13 / 17

26.7 %

8 / 30

src/theory/theory_inference.h

72.7 %

8 / 11

50.0 %

1 / 2

src/theory/theory_inference_manager.cpp

91.0 %

223 / 245

42.8 %

351 / 820

src/theory/theory_model.cpp

87.7 %

378 / 431

42.4 %

793 / 1869

src/theory/theory_model.h

100.0 %

4 / 4

50.0 %

1 / 2

src/theory/theory_model_builder.cpp

93.5 %

628 / 672

42.3 %

1220 / 2883

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_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

97.3 %

71 / 73

41.1 %

79 / 192

src/theory/theory_state.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/trust_substitutions.cpp

99.2 %

119 / 120

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

622 / 721

39.5 %

1488 / 3766

src/theory/uf/eq_proof.h

100.0 %

2 / 2

100.0 %

0 / 0

src/theory/uf/equality_engine.cpp

91.8 %

1265 / 1378

43.6 %

2431 / 5572

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

78.2 %

205 / 262

35.1 %

462 / 1316

src/theory/uf/proof_equality_engine.h

100.0 %

1 / 1

100.0 %

0 / 0

src/theory/uf/symmetry_breaker.cpp

82.7 %

401 / 485

43.1 %

951 / 2208

src/theory/uf/symmetry_breaker.h

100.0 %

7 / 7

50.0 %

4 / 8

src/theory/uf/theory_uf.cpp

87.2 %

294 / 337

47.4 %

638 / 1347

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

10.0 %

1 / 10

src/theory/uf/theory_uf_type_rules.cpp

68.0 %

51 / 75

27.5 %

88 / 320

src/theory/valuation.cpp

67.2 %

78 / 116

16.1 %

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

74.2 %

164 / 221

32.0 %

167 / 522

src/util/floatingpoint.h

95.4 %

62 / 65

50.0 %

9 / 18

src/util/floatingpoint_literal_symfpu.cpp

84.2 %

101 / 120

20.3 %

61 / 300

src/util/floatingpoint_literal_symfpu.h

100.0 %

9 / 9

50.0 %

2 / 4

src/util/floatingpoint_literal_symfpu_traits.cpp

92.6 %

113 / 122

25.0 %

67 / 268

src/util/floatingpoint_literal_symfpu_traits.h

100.0 %

6 / 6

50.0 %

2 / 4

src/util/floatingpoint_size.cpp

100.0 %

10 / 10

12.5 %

8 / 64

src/util/floatingpoint_size.h

100.0 %

16 / 16

50.0 %

2 / 4

src/util/hash.h

100.0 %

7 / 7

50.0 %

2 / 4

src/util/iand.h

50.0 %

2 / 4

100.0 %

0 / 0

src/util/indexed_root_predicate.h

71.4 %

5 / 7

100.0 %

0 / 0

src/util/integer_cln_imp.cpp

91.6 %

219 / 239

41.9 %

224 / 535

src/util/integer_cln_imp.h

100.0 %

19 / 19

83.3 %

5 / 6

src/util/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

62.6 %

102 / 163

31.9 %

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

60.0 %

45 / 75

29.6 %

45 / 152

src/util/real_algebraic_number_poly_imp.h

80.0 %

4 / 5

100.0 %

0 / 0

src/util/regexp.cpp

76.5 %

13 / 17

50.0 %

2 / 4

src/util/resource_manager.cpp

52.8 %

75 / 142

20.0 %

40 / 200

src/util/resource_manager.h

100.0 %

2 / 2

50.0 %

2 / 4

src/util/result.cpp

62.6 %

124 / 198

34.6 %

79 / 228

src/util/result.h

100.0 %

14 / 14

75.0 %

9 / 12

src/util/roundingmode.cpp

5.6 %

1 / 18

14.3 %

2 / 14

src/util/roundingmode.h

100.0 %

1 / 1

100.0 %

0 / 0

src/util/safe_print.cpp

0.0 %

0 / 102

0.0 %

0 / 84

src/util/safe_print.h

0.0 %

0 / 15

0.0 %

0 / 32

src/util/sampler.cpp

9.5 %

7 / 74

5.9 %

12 / 203

src/util/sexpr.cpp

64.7 %

11 / 17

40.9 %

9 / 22

src/util/sexpr.h

79.3 %

23 / 29

22.2 %

12 / 54

src/util/smt2_quote_string.cpp

100.0 %

8 / 8

77.3 %

17 / 22

src/util/statistics_public.cpp

100.0 %

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

34.0 %

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

31.6 %

18 / 57

test/api/boilerplate.cpp

100.0 %

5 / 5

50.0 %

7 / 14

test/api/issue4889.cpp

100.0 %

15 / 15

50.0 %

16 / 32

test/api/issue5074.cpp

100.0 %

9 / 9

50.0 %

14 / 28

test/api/issue6111.cpp

100.0 %

28 / 28

50.0 %

36 / 72

test/api/ouroborous.cpp

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 %

43 / 86

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 %

169 / 169

30.8 %

432 / 1402

test/unit/api/op_white.cpp

100.0 %

7 / 7

30.0 %

18 / 60

test/unit/api/result_black.cpp

100.0 %

75 / 75

34.1 %

198 / 580

test/unit/api/solver_black.cpp

100.0 %

1591 / 1591

36.4 %

6184 / 16980

test/unit/api/solver_white.cpp

100.0 %

21 / 21

41.0 %

55 / 134

test/unit/api/sort_black.cpp

100.0 %

378 / 378

33.1 %

1203 / 3630

test/unit/api/term_black.cpp

100.0 %

884 / 884

31.5 %

3578 / 11356

test/unit/api/term_white.cpp

100.0 %

42 / 42

40.6 %

121 / 298

test/unit/base/map_util_black.cpp

100.0 %

103 / 103

29.9 %

332 / 1110

test/unit/context/cdhashmap_black.cpp

100.0 %

88 / 88

28.8 %

247 / 857

test/unit/context/cdhashmap_white.cpp

100.0 %

10 / 10

25.0 %

66 / 264

test/unit/context/cdlist_black.cpp

100.0 %

94 / 94

30.8 %

146 / 474

test/unit/context/cdo_black.cpp

100.0 %

13 / 13

26.7 %

23 / 86

test/unit/context/context_black.cpp

97.5 %

115 / 118

24.4 %

221 / 905

test/unit/context/context_mm_black.cpp

97.1 %

34 / 35

36.4 %

39 / 107

test/unit/context/context_white.cpp

100.0 %

117 / 117

22.0 %

318 / 1444

test/unit/main/interactive_shell_black.cpp

100.0 %

62 / 62

44.0 %

44 / 100

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 %

474 / 475

33.8 %

1570 / 4641

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

348 / 798

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

57.1 %

40 / 70

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

100.0 %

1230 / 1230

32.6 %

4138 / 12708

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

92.3 %

203 / 220

41.7 %

612 / 1468

test/unit/theory/theory_arith_pow2_white.cpp

100.0 %

1 / 1

50.0 %

3 / 6

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 %

85 / 85

35.2 %

323 / 918

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

173 / 426

test/unit/theory/theory_bv_rewriter_white.cpp

100.0 %

39 / 39

45.2 %

112 / 248

test/unit/theory/theory_bv_white.cpp

100.0 %

38 / 38

47.0 %

108 / 230

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

144 / 344

test/unit/theory/theory_opt_multigoal_white.cpp

100.0 %

143 / 143

39.3 %

357 / 908

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)