[CSA] CSA Weekly Report 2026-02-27 — 124 findings (↓6 from last run)

[github-actions[bot]]

Date: 2026-02-27
Commit: ea87367 (ea87367)
Build type: Debug (CMake + Ninja, -DCMAKE_BUILD_TYPE=Debug)
Analyzer: scan-build / clang-analyzer (Ubuntu clang 18.1.3)
Previous run: 2026-02-24 @ c282ece — 130 findings

---

Summary

Metric	Count
Total findings	124
Called C++ object pointer is null	55
Dereference of null pointer	18
Dead assignment	18
Bitwise shift (overflow/undefined)	9
Dead initialization	6
Returning null reference	5
Branch condition evaluates to garbage value	3
Dead increment	3
Result of operation is garbage/undefined	3
Uninitialized argument value	3
Division by zero	1
Files affected	~50

---

Changes Since Last Run

Previous run (2026-02-24, commit c282ece): 130 findings
This run (2026-02-27, commit ea87367): 124 findings
Net change: −6 findings (improvement)

Resolved since last run:

• Division by zero count reduced (5 → 1): significant improvement in util/util.h and related arithmetic code
• Stack address escape issue appears resolved (was 1, now 0)
• Null dereference count slightly reduced (19 → 18)

New or unchanged findings:

• The core null pointer / called-C++-object-null category remains at 55+18=73 — same as before
• Dead code findings slightly increased (27 → 27) — roughly stable

---

High-Priority Findings

These findings are most likely to represent real bugs (not false positives):

#	Checker	File	Line	Description
1	core.NullDereference	util/debug.cpp	163	Dereference of null pointer loaded from variable x
2	core.NullDereference	math/realclosure/realclosure.cpp	1118	Null pointer dereference via array access from variable as
3	core.NullDereference	math/polynomial/polynomial.cpp	2581	Access to field m_next — null ptr from field m_del_eh
4	core.NullDereference	math/polynomial/polynomial.cpp	2587	Access to field m_next — null ptr from field m_next
5	core.NullDereference	ast/rewriter/enum2bv_rewriter.cpp	92	Array access from variable args — null pointer dereference
6	core.NullDereference	ast/rewriter/enum2bv_rewriter.cpp	100	Array access from variable args — null pointer dereference
7	core.NullDereference	util/obj_mark.h	38	Forming reference to null pointer
8	core.NullDereference	util/parray.h	155	Array access from variable vs — null pointer dereference
9	core.NullDereference	nlsat/nlsat_solver.cpp	1256	Forming reference to null pointer
10	core.NullDereference	smt/mam.cpp	3330	Forming reference to null pointer
11	core.NullDereference	cmd_context/cmd_context.cpp	237	Array access from domain — null pointer dereference
12	core.NullDereference	sat/sat_npn3_finder.cpp	219/250/292	Dereference of null pointer from field use_list (3 locations)
13	core.NullDereference	ast/euf/euf_mam.cpp	1708/3413	Null pointer dereference via field m_opcode / forming reference
14	core.UndefinedBinaryOperatorResult	ast/act_cache.cpp	175/197	Left operand of & is a garbage value
15	core.uninitialized.Branch	muz/spacer/spacer_context.cpp	3347/3596	Branch condition evaluates to garbage value
16	core.DivideZero	util/util.h	356	Division by zero
17	core.BitwiseShift	util/sorting_network.h	415	Left shift by 4294967295 — extreme overflow

---

Findings by Category

Core Checkers — Null Pointer Issues (73 total)

Called C++ object pointer is null (55 findings)

Most are in AST/SMT infrastructure where to_app(), to_quantifier() etc. return potentially null casts, then methods are immediately called on the result. Many of these may be false positives due to guarded control flow not visible to the analyzer.

Top affected areas:

• src/ast/ast.h — lines 947, 950, 1399, 1400, 1401 (5 findings — same inline helper functions)
• src/ast/euf/euf_mam.cpp — lines 1167, 1405, 2160 (3 findings)
• src/smt/mam.cpp — lines 1120, 1363, 2144 (3 findings)
• src/ast/sls/sls_arith_base.cpp — lines 1072, 1093 (2 findings)
• src/ast/sls/sls_euf_plugin.cpp — lines 292, 299 (2 findings)
• src/ast/sls/sls_seq_plugin.cpp — lines 264, 302, 340 (3 findings)
• src/ast/rewriter/seq_axioms.cpp — lines 81, 299, 1088 (3 findings)
• src/smt/theory_seq.cpp — lines 1628, 1628, 1631 (3 findings)
• src/math/realclosure/realclosure.cpp — lines 3461, 3477, 3494 (3 findings)
• src/ast/bv_decl_plugin.h — lines 313, 469, 471 (3 findings)
• src/opt/totalizer.cpp — line 40 (2 findings — duplicate path)

Dereference of null pointer (18 findings)

• src/sat/sat_npn3_finder.cpp — lines 219, 250, 292 (3 findings — use_list field)
• src/math/polynomial/polynomial.cpp — lines 2581, 2587 (2 findings — linked-list traversal)
• src/ast/rewriter/enum2bv_rewriter.cpp — lines 92, 100 (2 findings — args array)
• src/ast/euf/euf_mam.cpp — lines 1708, 3413 (2 findings)
• src/cmd_context/cmd_context.cpp — lines 237, 1335 (2 findings)
• src/math/realclosure/realclosure.cpp — line 1118
• src/nlsat/nlsat_solver.cpp — line 1256
• src/smt/mam.cpp — line 3330
• src/sat/sat_aig_finder.cpp — line 198
• src/util/debug.cpp — line 163 (intentional — debugger trap)
• src/util/obj_mark.h — line 38
• src/util/parray.h — line 155

C++ Specific — Returning Null Reference (5 findings)

• src/ast/euf/euf_ac_plugin.cpp:805 — backward_iterator returns null ref
• src/util/util.h:259 — operator* returns null ref
• src/sat/sat_extension.h:76 — s() returns null ref (path length 59 — likely complex control flow)
• src/util/ref.h:80 — operator* returns null ref
• src/cmd_context/cmd_context.h:428 — pm() returns null ref

Suspicious Operations — Bitwise Shift (9 findings)

All are genuine undefined behavior in C++:

• src/util/sorting_network.h:415 — shift by 4294967295 (wraps around, very suspicious)
• src/util/bit_util.cpp:222 — right shift by 32 of unsigned int (UB)
• src/util/bit_util.cpp:286,338 — left shift overflow of unsigned int
• src/util/mpff.cpp:164,178 — right shift by negative value (UB)
• src/math/simplex/bit_matrix.cpp:128 — left shift by 32 of int (UB)
• src/ast/rewriter/enum2bv_rewriter.cpp:67 — left shift overflow of int
• src/muz/rel/dl_sparse_table.h:331 — left shift by ≥65 of uint64_t

Logic Errors — Uninitialized / Garbage Values (9 findings)

• src/muz/spacer/spacer_context.cpp:3347,3596 — 2 branch-on-garbage findings
• src/ast/rewriter/bit2int.cpp:362 — branch-on-garbage (path length 60 — complex)
• src/math/lp/nla_core.cpp:309,567,569 — 3 uninitialized argument values
• src/ast/act_cache.cpp:175,197 — garbage value in binary & operation
• src/math/lp/nla_core.cpp:556 — garbage value in != comparison

Division by Zero (1 finding)

• src/util/util.h:356 — operator() — division by zero (path length 31)

Dead Code (27 findings)

These are lower severity; most represent missed assignments or unused temporaries:

Dead assignments (18): datalog_parser.cpp:1329, sls_bv_engine.cpp:454, spacer_quant_generalizer.cpp:535, user_solver.cpp:363, model_based_opt.cpp:76, mbp_term_graph.cpp:222, hilbert_basis.cpp:1013,1014, realclosure.cpp:4109, dl_compiler.cpp:390, bv_rewriter.cpp:2169, ho_matcher.cpp:560, horn_tactic.cpp:271, clp_context.cpp:187, pb_sls.cpp:651, optsmt.cpp:184, euf_model.cpp:372, dl_bound_relation.cpp:473

Dead increments (3): util.cpp:79,108, udoc_relation.cpp:721

Dead initializations (6): sat_local_search.cpp:569, lackr_model_constructor.cpp:314, opt_context.cpp:1273, polynomial.cpp:1740, theory_finite_set_size.cpp:204, theory_finite_set.cpp:174

---

Top Affected Files

File	Findings
src/ast/ast.h	7
src/ast/euf/euf_mam.cpp	5
src/math/realclosure/realclosure.cpp	5
src/ast/sls/sls_seq_plugin.cpp	4
src/smt/mam.cpp	4
src/ast/rewriter/seq_axioms.cpp	3
src/smt/theory_seq.cpp	3
src/math/lp/nla_core.cpp	3
src/sat/sat_npn3_finder.cpp	3
src/ast/bv_decl_plugin.h	3
src/ast/rewriter/enum2bv_rewriter.cpp	3
src/util/bit_util.cpp	3

---

Full CSA Report Content

Complete findings extracted from the CSA HTML report (click to expand)

## Summary Table

Bug Type | Quantity
All Bugs | 124
Branch condition evaluates to a garbage value | 3
Called C++ object pointer is null | 55
Dereference of null pointer | 18
Division by zero | 1
Result of operation is garbage or undefined | 3
Returning null reference | 5
Uninitialized argument value | 3
Bitwise shift | 9
Dead assignment | 18
Dead increment | 3
Dead initialization | 6

## Individual Findings (124 total)

1. [Dead assignment] Value stored to 'tok' is never read
   File: datalog_parser.cpp, Line: 1329
2. [Called C++ object pointer is null] Called C++ object pointer is null
   File: ast.h, Line: 950
3. [Called C++ object pointer is null] Called C++ object pointer is null
   File: ast.h, Line: 1400
4. [Returning null reference] Returning null reference
   File: euf_ac_plugin.cpp, Line: 805
5. [Dead increment] Value stored to 'v' is never read
   File: util.cpp, Line: 108
6. [Uninitialized argument value] 2nd function call argument is an uninitialized value
   File: nla_core.cpp, Line: 569
7. [Division by zero] Division by zero
   File: util.h, Line: 356
8. [Dead assignment] Value stored to 'score' is never read
   File: sls_bv_engine.cpp, Line: 454
9. [Bitwise shift] Left shift by '4294967295' overflows the capacity of 'unsigned long'
   File: sorting_network.h, Line: 415
10. [Called C++ object pointer is null] Called C++ object pointer is null
    File: mam.cpp, Line: 1363
11. [Dereference of null pointer] Dereference of null pointer (loaded from field 'use_list')
    File: sat_npn3_finder.cpp, Line: 219
12. [Result of operation is garbage or undefined] The left operand of '&' is a garbage value
    File: act_cache.cpp, Line: 175
13. [Bitwise shift] Left shift overflows the capacity of 'int'
    File: enum2bv_rewriter.cpp, Line: 67
14. [Dereference of null pointer] Forming reference to null pointer
    File: nlsat_solver.cpp, Line: 1256
15. [Called C++ object pointer is null] Called C++ object pointer is null
    File: euf_mam.cpp, Line: 1167
16. [Dead assignment] Value stored to 'ub' is never read
    File: spacer_quant_generalizer.cpp, Line: 535
17. [Dereference of null pointer] Array access (from variable 'domain') results in a null pointer dereference
    File: cmd_context.cpp, Line: 237
18. [Called C++ object pointer is null] Called C++ object pointer is null
    File: seq_axioms.cpp, Line: 1088
19. [Called C++ object pointer is null] Called C++ object pointer is null
    File: seq_eq_solver.cpp, Line: 1037
20. [Dereference of null pointer] Forming reference to null pointer
    File: mam.cpp, Line: 3330
21. [Dead initialization] Value stored to 'is_core' during its initialization is never read
    File: sat_local_search.cpp, Line: 569
22. [Called C++ object pointer is null] Called C++ object pointer is null
    File: sls_arith_base.cpp, Line: 1093
23. [Called C++ object pointer is null] Called C++ object pointer is null
    File: smtfd_solver.cpp, Line: 172
24. [Called C++ object pointer is null] Called C++ object pointer is null
    File: bv_decl_plugin.h, Line: 313
25. [Dereference of null pointer] Forming reference to null pointer
    File: obj_mark.h, Line: 38
26. [Bitwise shift] Left shift overflows 'unsigned int' (right operand >= 32)
    File: bit_util.cpp, Line: 286
27. [Called C++ object pointer is null] Called C++ object pointer is null
    File: seq_regex.cpp, Line: 62
28. [Branch condition evaluates to a garbage value] Branch condition evaluates to a garbage value
    File: spacer_context.cpp, Line: 3596
29. [Dead initialization] Value stored to 'fid' during its initialization is never read
    File: lackr_model_constructor.cpp, Line: 314
30. [Called C++ object pointer is null] Called C++ object pointer is null
    File: smt_relevancy.cpp, Line: 309
31. [Dereference of null pointer] Array access (from variable 'as') results in a null pointer dereference
    File: realclosure.cpp, Line: 1118
32. [Called C++ object pointer is null] Called C++ object pointer is null
    File: grobner.cpp, Line: 513
33. [Branch condition evaluates to a garbage value] Branch condition evaluates to a garbage value
    File: bit2int.cpp, Line: 362
34. [Dead assignment] Value stored to 'n' is never read
    File: user_solver.cpp, Line: 363
35. [Dead initialization] Value stored to 'name' during its initialization is never read
    File: opt_context.cpp, Line: 1273
36. [Called C++ object pointer is null] Called C++ object pointer is null
    File: euf_mam.cpp, Line: 1405
37. [Called C++ object pointer is null] Called C++ object pointer is null
    File: mam.cpp, Line: 2144
38. [Called C++ object pointer is null] Called C++ object pointer is null
    File: sls_arith_base.cpp, Line: 1072
39. [Called C++ object pointer is null] Called C++ object pointer is null
    File: theory_seq.cpp, Line: 1631
40. [Dead assignment] Value stored to 'sign' is never read
    File: model_based_opt.cpp, Line: 76
41. [Dead initialization] Value stored to 'm' during its initialization is never read
    File: polynomial.cpp, Line: 1740
42. [Called C++ object pointer is null] Called C++ object pointer is null
    File: udoc_relation.cpp, Line: 58
43. [Dereference of null pointer] Access to field 'm_next' results in a dereference of a null pointer (loaded from field 'm_del_eh')
    File: polynomial.cpp, Line: 2581
44. [Called C++ object pointer is null] Called C++ object pointer is null
    File: ast.h, Line: 1401
45. [Bitwise shift] Right shift by negative value
    File: mpff.cpp, Line: 178
46. [Called C++ object pointer is null] Called C++ object pointer is null
    File: dl_finite_product_relation.cpp, Line: 943
47. [Bitwise shift] Right shift by negative value
    File: mpff.cpp, Line: 164
48. [Called C++ object pointer is null] Called C++ object pointer is null
    File: smt2parser.cpp, Line: 588
49. [Dereference of null pointer] Array access (from variable 'args') results in a null pointer dereference
    File: enum2bv_rewriter.cpp, Line: 92
50. [Called C++ object pointer is null] Called C++ object pointer is null
    File: sls_euf_plugin.cpp, Line: 292
51. [Called C++ object pointer is null] Called C++ object pointer is null
    File: sls_datatype_plugin.cpp, Line: 965
52. [Called C++ object pointer is null] Called C++ object pointer is null
    File: totalizer.cpp, Line: 40
53. [Dead assignment] Value stored to 'a' is never read
    File: mbp_term_graph.cpp, Line: 222
54. [Dead increment] Value stored to 'v' is never read
    File: util.cpp, Line: 79
55. [Returning null reference] Returning null reference
    File: util.h, Line: 259
56. [Dereference of null pointer] Dereference of null pointer (loaded from field 'use_list')
    File: sat_aig_finder.cpp, Line: 198
57. [Called C++ object pointer is null] Called C++ object pointer is null
    File: array_internalize.cpp, Line: 134
58. [Called C++ object pointer is null] Called C++ object pointer is null
    File: euf_mam.cpp, Line: 2160
59. [Dead increment] Value stored to 'hi2' is never read
    File: udoc_relation.cpp, Line: 721
60. [Dereference of null pointer] Dereference of null pointer (loaded from variable 'x')
    File: debug.cpp, Line: 163
61. [Dereference of null pointer] Array access (from variable 'vs') results in a null pointer dereference
    File: parray.h, Line: 155
62. [Called C++ object pointer is null] Called C++ object pointer is null
    File: bv_decl_plugin.h, Line: 471
63. [Called C++ object pointer is null] Called C++ object pointer is null
    File: seq_skolem.cpp, Line: 191
64. [Result of operation is garbage or undefined] The left operand of '&' is a garbage value
    File: act_cache.cpp, Line: 197
65. [Called C++ object pointer is null] Called C++ object pointer is null
    File: value_sweep.cpp, Line: 72
66. [Dead assignment] Value stored to 'non_zeros' is never read
    File: hilbert_basis.cpp, Line: 1014
67. [Called C++ object pointer is null] Called C++ object pointer is null
    File: smt_context.h, Line: 319
68. [Dead initialization] Value stored to 'd' during its initialization is never read
    File: theory_finite_set_size.cpp, Line: 204
69. [Bitwise shift] Left shift overflows 'unsigned int' (right operand >= 32)
    File: bit_util.cpp, Line: 338
70. [Dead assignment] Value stored to 'col1' is never read
    File: dl_bound_relation.cpp, Line: 473
71. [Called C++ object pointer is null] Called C++ object pointer is null
    File: seq_axioms.cpp, Line: 299
72. [Bitwise shift] Right shift by '32' overflows 'unsigned int'
    File: bit_util.cpp, Line: 222
73. [Called C++ object pointer is null] Called C++ object pointer is null
    File: degree_shift_tactic.cpp, Line: 204
74. [Dead assignment] Value stored to 'sign' is never read
    File: realclosure.cpp, Line: 4109
75. [Called C++ object pointer is null] Called C++ object pointer is null
    File: euf_egraph.h, Line: 273
76. [Called C++ object pointer is null] Called C++ object pointer is null
    File: mam.cpp, Line: 1120
77. [Dead assignment] Value stored to 'curr_sig' is never read
    File: dl_compiler.cpp, Line: 390
78. [Called C++ object pointer is null] Called C++ object pointer is null
    File: theory_seq.cpp, Line: 1628
79. [Called C++ object pointer is null] Called C++ object pointer is null
    File: ast.h, Line: 947
80. [Dereference of null pointer] Dereference of null pointer (loaded from field 'use_list')
    File: sat_npn3_finder.cpp, Line: 250
81. [Called C++ object pointer is null] Called C++ object pointer is null
    File: smt_context.h, Line: 743
82. [Uninitialized argument value] 2nd function call argument is an uninitialized value
    File: nla_core.cpp, Line: 567
83. [Called C++ object pointer is null] Called C++ object pointer is null
    File: realclosure.cpp, Line: 3477
84. [Called C++ object pointer is null] Called C++ object pointer is null
    File: bv2int_translator.cpp, Line: 58
85. [Called C++ object pointer is null] Called C++ object pointer is null
    File: seq_skolem.cpp, Line: 52
86. [Dead initialization] Value stored to 'set1' during its initialization is never read
    File: theory_finite_set.cpp, Line: 174
87. [Uninitialized argument value] 1st function call argument is an uninitialized value
    File: nla_core.cpp, Line: 309
88. [Called C++ object pointer is null] Called C++ object pointer is null
    File: datatype_decl_plugin.cpp, Line: 188
89. [Called C++ object pointer is null] Called C++ object pointer is null
    File: sls_seq_plugin.cpp, Line: 302
90. [Called C++ object pointer is null] Called C++ object pointer is null
    File: totalizer.cpp, Line: 40
91. [Bitwise shift] Left shift by '32' overflows 'int'
    File: bit_matrix.cpp, Line: 128
92. [Dead assignment] Value stored to 'bv_size' is never read
    File: bv_rewriter.cpp, Line: 2169
93. [Called C++ object pointer is null] Called C++ object pointer is null
    File: realclosure.cpp, Line: 3494
94. [Dead assignment] Value stored to 'prod' is never read
    File: hilbert_basis.cpp, Line: 1013
95. [Called C++ object pointer is null] Called C++ object pointer is null
    File: bv_decl_plugin.h, Line: 469
96. [Called C++ object pointer is null] Called C++ object pointer is null
    File: intblast_solver.cpp, Line: 517
97. [Called C++ object pointer is null] Called C++ object pointer is null
    File: sls_euf_plugin.cpp, Line: 299
98. [Returning null reference] Returning null reference
    File: sat_extension.h, Line: 76
99. [Bitwise shift] Left shift by >=65 overflows 'uint64_t'
    File: dl_sparse_table.h, Line: 331
100. [Dereference of null pointer] Dereference of null pointer (loaded from field 'use_list')
     File: sat_npn3_finder.cpp, Line: 292
101. [Dead assignment] Value stored to 'p1' is never read
     File: ho_matcher.cpp, Line: 560
102. [Called C++ object pointer is null] Called C++ object pointer is null
     File: seq_eq_solver.cpp, Line: 1053
103. [Called C++ object pointer is null] Called C++ object pointer is null
     File: pb_solver.h, Line: 274
104. [Called C++ object pointer is null] Called C++ object pointer is null
     File: ast.h, Line: 1399
105. [Dereference of null pointer] Access to field 'm_next' results in a dereference of a null pointer (loaded from field 'm_next')
     File: polynomial.cpp, Line: 2587
106. [Called C++ object pointer is null] Called C++ object pointer is null
     File: sls_seq_plugin.cpp, Line: 340
107. [Dereference of null pointer] Array access (from variable 'args') results in a null pointer dereference
     File: cmd_context.cpp, Line: 1335
108. [Dereference of null pointer] Array access (from variable 'args') results in a null pointer dereference
     File: enum2bv_rewriter.cpp, Line: 100
109. [Dead assignment] Value stored to 'is_reachable' is never read
     File: horn_tactic.cpp, Line: 271
110. [Branch condition evaluates to a garbage value] Branch condition evaluates to a garbage value
     File: spacer_context.cpp, Line: 3347
111. [Dereference of null pointer] Forming reference to null pointer
     File: euf_mam.cpp, Line: 3413
112. [Returning null reference] Returning null reference
     File: ref.h, Line: 80
113. [Dead assignment] Value stored to 'status' is never read
     File: clp_context.cpp, Line: 187
114. [Called C++ object pointer is null] Called C++ object pointer is null
     File: seq_axioms.cpp, Line: 81
115. [Called C++ object pointer is null] Called C++ object pointer is null
     File: sls_seq_plugin.cpp, Line: 264
116. [Called C++ object pointer is null] Called C++ object pointer is null
     File: seq_decl_plugin.h, Line: 244
117. [Dead assignment] Value stored to 'args' is never read
     File: pb_sls.cpp, Line: 651
118. [Called C++ object pointer is null] Called C++ object pointer is null
     File: theory_seq.cpp, Line: 1628
119. [Dead assignment] Value stored to 'num_scopes' is never read
     File: optsmt.cpp, Line: 184
120. [Called C++ object pointer is null] Called C++ object pointer is null
     File: realclosure.cpp, Line: 3461
121. [Returning null reference] Returning null reference
     File: cmd_context.h, Line: 428
122. [Dead assignment] Value stored to 'first' is never read
     File: euf_model.cpp, Line: 372
123. [Result of operation is garbage or undefined] The left operand of '!=' is a garbage value
     File: nla_core.cpp, Line: 556
124. [Dereference of null pointer] Access to field 'm_opcode' results in a dereference of a null pointer (loaded from variable 'curr')
     File: euf_mam.cpp, Line: 1708
```

</details>

## Build Log Excerpt

<details>
<summary>Key warnings and errors from the build log (click to expand)</summary>

```
src/util/bit_util.cpp:222:41: warning: Right shift by '32' overflows the capacity of 'unsigned int' [core.BitwiseShift]
src/util/bit_util.cpp:286:37: warning: Left shift overflows the capacity of 'unsigned int' [core.BitwiseShift]
src/util/bit_util.cpp:338:33: warning: Left shift overflows the capacity of 'unsigned int' [core.BitwiseShift]
src/util/debug.cpp:163:16: warning: Dereference of null pointer (loaded from variable 'x') [core.NullDereference]
src/util/mpff.cpp:164:15: warning: Right operand is negative in right shift [core.BitwiseShift]
src/util/mpff.cpp:178:24: warning: Right operand is negative in right shift [core.BitwiseShift]
src/util/util.cpp:79:9: warning: Value stored to 'v' is never read [deadcode.DeadStores]
src/util/util.cpp:108:9: warning: Value stored to 'v' is never read [deadcode.DeadStores]
src/math/simplex/bit_matrix.cpp:128:36: warning: Left shift by '32' overflows the capacity of 'int' [core.BitwiseShift]
src/math/realclosure/realclosure.cpp:1118:30: warning: Array access (from variable 'as') results in a null pointer dereference [core.NullDereference]
src/math/realclosure/realclosure.cpp:3461:37: warning: Called C++ object pointer is null [core.CallAndMessage]
src/math/polynomial/polynomial.cpp:2581:28: warning: Access to field 'm_next' results in a dereference of a null pointer [core.NullDereference]
src/math/polynomial/polynomial.cpp:2587:40: warning: Access to field 'm_next' results in a dereference of a null pointer [core.NullDereference]
src/ast/act_cache.cpp:178:22: warning: The left operand of '&' is a garbage value [core.UndefinedBinaryOperatorResult]
src/ast/datatype_decl_plugin.cpp:188:36: warning: Called C++ object pointer is null [core.CallAndMessage]
src/ast/rewriter/bit2int.cpp:362:17: warning: Branch condition evaluates to a garbage value [core.uninitialized.Branch]
src/ast/rewriter/enum2bv_rewriter.cpp:67:52: warning: Left shift overflows the capacity of 'int' [core.BitwiseShift]
src/ast/rewriter/enum2bv_rewriter.cpp:92:42: warning: Array access (from variable 'args') results in a null pointer dereference [core.NullDereference]
src/util/sorting_network.h:415:33: warning: Left shift by '4294967295' overflows the capacity of 'unsigned long' [core.BitwiseShift]
src/ast/ast.h:947:51: warning: Called C++ object pointer is null [core.CallAndMessage]
src/ast/euf/euf_egraph.h:273:62: warning: Called C++ object pointer is null [core.CallAndMessage]

(162 total warning lines in build log)

---

Notes

• This report was generated automatically by the Z3 CSA Analysis workflow on commit ea87367.
• False positives are expected — many "Called C++ object pointer is null" findings arise because the analyzer cannot track Z3's internal invariants that ensure to_app(), to_quantifier() etc. are only called when safe. These are guarded by is_app(), is_quantifier() etc. checks elsewhere.
• The util/debug.cpp:163 null dereference is intentional — it's a debugger trap that intentionally dereferences null to trigger a breakpoint/crash for debugging.
• The bitwise shift findings in bit_util.cpp and bit_matrix.cpp represent real undefined behavior in C++ (though they may work correctly in practice on typical platforms with clang/gcc).
• To reproduce locally: scan-build -o /tmp/csa-report cmake -DCMAKE_BUILD_TYPE=Debug -G Ninja . && scan-build ninja
• Trend: 124 findings this run vs 130 last run (2026-02-24) — improvement of 6 findings. Division-by-zero category dropped significantly (5→1).

AI generated by Clang Static Analyzer (CSA) Report

• expires on Mar 6, 2026, 12:48 PM UTC

[github-actions[bot]]

This discussion was automatically closed because it expired on 2026-03-06T12:48:25.474Z.

Closed by Workflow