[CSA] CSA Weekly Report — 2026-03-01 — 124 findings (↓6 vs last run)

[github-actions[bot]]

Build Information

Field	Value
Date	2026-03-01
Commit	dcb888d (HEAD → master)
Build type	Debug (CMake + Ninja)
Analyzer	scan-build / clang-analyzer (Ubuntu clang 18.1.3)
Build host	Ubuntu Linux, 4 cores

Summary

Metric	Count
Total findings	124
Called C++ object pointer is null (core.CallAndMessage)	55
Dereference of null pointer (core.NullDereference)	18
Dead assignment / increment / initialization (deadcode.DeadStores)	27
Bitwise shift undefined behavior (core.BitwiseShift)	9
Returning null reference (core.uninitialized.UndefReturn)	5
Branch/arg/result garbage (core.UndefinedBinaryOperatorResult, etc.)	9
Division by zero (core.DivideZero)	1
Files affected	~50+

Changes Since Last Run (vs 2026-02-24, commit c282ece)

Change	Detail
Total findings	130 → 124 (↓ 6 resolved)
called_cpp_object_null	55 → 55 (unchanged)
null_dereference	19 → 18 (↓ 1)
dead_stores	27 → 27 (unchanged)
bitwise_shift	9 → 9 (unchanged)
divide_zero	5 → 1 (↓ 4 resolved 🎉)
returning_null_reference	5 → 5 (unchanged)
uninitialized_branch	3 → 3 (unchanged)
undefined_binary_op	3 → 3 (unchanged)
uninitialized_arg	3 → 3 (unchanged)
stack_address_escape	1 → 0 (↓ 1 resolved 🎉)
result_garbage	0 → 3 (↑ 3 new)

Net improvement: −6 findings. The division-by-zero findings dropped from 5 to 1, and the stack address escape is gone. Three new "result of operation is garbage" findings appeared in act_cache.cpp and nla_core.cpp.

High-Priority Findings

These are the most likely to represent real bugs (high path length or critical checker):

#	Bug Type	File	Function	Line	Path
1	Returning null reference	sat/sat_extension.h	s	76	59
2	Branch condition evaluates to garbage	ast/rewriter/bit2int.cpp	visit	362	60
3	Dereference of null pointer	ast/euf/euf_mam.cpp	insert	3413	37
4	Called C++ object pointer is null	ast/sls/sls_arith_base.cpp	mk_term	1072	36
5	Dereference of null pointer	ast/rewriter/enum2bv_rewriter.cpp	reduce_app	100	34
6	Dereference of null pointer	smt/mam.cpp	insert	3330	34
7	Called C++ object pointer is null	ast/euf/euf_mam.cpp	linearise_multi_pattern	1167	32
8	Dereference of null pointer	util/parray.h	expand	155	32
9	Called C++ object pointer is null	ast/bv_decl_plugin.h	get_bv_size	471	32
10	Division by zero	util/util.h	operator()	356	31

Findings by Category

Core Checkers — Null Pointer Issues (73 total)

Called C++ Object Pointer is Null (55)

These represent cases where a method is called on a pointer that CSA determined could be null. Many are in Z3's type-check helper functions (e.g., is_app, is_quantifier, is_bv) where the pattern is intentional (returning false when ptr is null). Nevertheless, a few longer-path entries may warrant review.

Top affected subsystems:

• ast/ast.h (5 findings) — is_app, is_quantifier, is_app_of, is_sort_of
• ast/euf/euf_mam.cpp (5 findings) — MAM e-matching engine
• math/realclosure/realclosure.cpp (5 findings) — Real-closure arithmetic
• smt/mam.cpp (4 findings) — Legacy MAM e-matching
• ast/sls/sls_seq_plugin.cpp (3 findings) — SLS sequence plugin
• ast/rewriter/seq_axioms.cpp (3 findings) — Sequence axioms rewriter
• ast/bv_decl_plugin.h (3 findings) — Bit-vector declarations
• smt/theory_seq.cpp (3 findings) — Sequence theory

Selected notable findings:

• smt/mam.cpp:1363 — is_semi_compatible (path 23): null C++ object ptr
• ast/euf/euf_mam.cpp:1167 — linearise_multi_pattern (path 32): null C++ object ptr
• sat/smt/pb_solver.h:274 — inconsistent (path 29): null C++ object ptr
• parsers/smt2/smt2parser.cpp:588 — parse_sort_name (path 26): null C++ object ptr
• smt/theory_seq.cpp:1628,1631 — add_ubv_string (paths 23/26/27): null C++ object ptr

Dereference of Null Pointer (18)

Description	File	Line
Dereference from field use_list	sat/sat_npn3_finder.cpp	219, 250, 292
Forming reference to null pointer	nlsat/nlsat_solver.cpp	1256
Array access on null domain	cmd_context/cmd_context.cpp	237
Forming reference to null	smt/mam.cpp	3330
Forming reference to null	util/obj_mark.h	38
Array access on null as	math/realclosure/realclosure.cpp	1118
Access to m_next via null m_del_eh	math/polynomial/polynomial.cpp	2581, 2587
Array access on null args	ast/rewriter/enum2bv_rewriter.cpp	92, 100
Dereference of null use_list	sat/sat_aig_finder.cpp	198
Dereference of null x	util/debug.cpp	163
Array access on null vs	util/parray.h	155
Array access on null args	cmd_context/cmd_context.cpp	1335
Forming reference to null	ast/euf/euf_mam.cpp	3413, 1708

C++ Undefined Behavior / Bitwise Shift (9)

Description	File	Line
Right shift by 4294967295 (overflow)	util/sorting_network.h	415
Left shift overflows 32-bit int	ast/rewriter/enum2bv_rewriter.cpp	67
Left shift overflows unsigned int (×2)	util/bit_util.cpp	286, 338
Right shift by negative	util/mpff.cpp	164, 178
Right shift by 32 on unsigned int	util/bit_util.cpp	222
Left shift by 32 overflows int	math/simplex/bit_matrix.cpp	128
Left shift overflow uint64_t	muz/rel/dl_sparse_table.h	331

Returning Null Reference (5)

File	Function	Line
ast/euf/euf_ac_plugin.cpp	backward_iterator	805
util/util.h	operator*	259
sat/sat_extension.h	s	76
util/ref.h	operator*	80
cmd_context/cmd_context.h	pm	428

Logic / Garbage Value Errors (9)

Branch condition evaluates to garbage (3):

• muz/spacer/spacer_context.cpp:3596 — expand_pob (path 36)
• ast/rewriter/bit2int.cpp:362 — visit (path 60) ⚠️ longest path in entire report
• muz/spacer/spacer_context.cpp:3347 — is_reachable (path 25)

Result of operation is garbage or undefined (3) — NEW since last run:

• ast/act_cache.cpp:175 — insert: left operand of & is garbage
• ast/act_cache.cpp:197 — find: left operand of & is garbage
• math/lp/nla_core.cpp:556 — is_octagon_term: left operand of != is garbage

Uninitialized argument (3):

• math/lp/nla_core.cpp:567,569 — add_equivalence_maybe: 2nd arg uninitialized
• math/lp/nla_core.cpp:309 — explain_by_equiv: 1st arg uninitialized

Division by Zero (1) — reduced from 5 ✅

• util/util.h:356 — operator() (path 31)

Dead Code / Unused Variables (27)

18 dead assignments, 3 dead increments, 6 dead initializations. These are low severity but indicate cleanup opportunities.

Complete dead code findings

Dead assignments:

• datalog_parser.cpp:1329 — tok stored, never read
• sls_bv_engine.cpp:454 — score
• spacer_quant_generalizer.cpp:535 — ub
• user_solver.cpp:363 — n
• model_based_opt.cpp:76 — sign
• mbp_term_graph.cpp:222 — a
• hilbert_basis.cpp:1013,1014 — prod, non_zeros
• dl_bound_relation.cpp:473 — col1
• realclosure.cpp:4109 — sign
• dl_compiler.cpp:390 — curr_sig
• bv_rewriter.cpp:2169 — bv_size
• ho_matcher.cpp:560 — p1
• horn_tactic.cpp:271 — is_reachable
• clp_context.cpp:187 — status
• pb_sls.cpp:651 — args
• optsmt.cpp:184 — num_scopes
• euf_model.cpp:372 — first

Dead increments:

• util.cpp:79,108 — v (in log2, uint64_log2)
• udoc_relation.cpp:721 — hi2

Dead initializations:

• sat_local_search.cpp:569 — is_core
• lackr_model_constructor.cpp:314 — fid
• opt_context.cpp:1273 — name
• polynomial.cpp:1740 — m
• theory_finite_set_size.cpp:204 — d
• theory_finite_set.cpp:174 — set1

Top Affected Files

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

Full CSA Report Content

Complete findings extracted from the CSA HTML report — click to expand

## Summary Table (from index.html)

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

### Called C++ object pointer is null (55)
- [Logic error] Called C++ object pointer is null  `ast.h:950`
- [Logic error] Called C++ object pointer is null  `ast.h:1400`
- [Logic error] Called C++ object pointer is null  `mam.cpp:1363`
- [Logic error] Called C++ object pointer is null  `euf_mam.cpp:1167`
- [Logic error] Called C++ object pointer is null  `seq_axioms.cpp:1088`
- [Logic error] Called C++ object pointer is null  `seq_eq_solver.cpp:1037`
- [Logic error] Called C++ object pointer is null  `sls_arith_base.cpp:1093`
- [Logic error] Called C++ object pointer is null  `smtfd_solver.cpp:172`
- [Logic error] Called C++ object pointer is null  `bv_decl_plugin.h:313`
- [Logic error] Called C++ object pointer is null  `seq_regex.cpp:62`
- [Logic error] Called C++ object pointer is null  `smt_relevancy.cpp:309`
- [Logic error] Called C++ object pointer is null  `grobner.cpp:513`
- [Logic error] Called C++ object pointer is null  `euf_mam.cpp:1405`
- [Logic error] Called C++ object pointer is null  `mam.cpp:2144`
- [Logic error] Called C++ object pointer is null  `sls_arith_base.cpp:1072`
- [Logic error] Called C++ object pointer is null  `theory_seq.cpp:1631`
- [Logic error] Called C++ object pointer is null  `udoc_relation.cpp:58`
- [Logic error] Called C++ object pointer is null  `ast.h:1401`
- [Logic error] Called C++ object pointer is null  `dl_finite_product_relation.cpp:943`
- [Logic error] Called C++ object pointer is null  `smt2parser.cpp:588`
- [Logic error] Called C++ object pointer is null  `sls_euf_plugin.cpp:292`
- [Logic error] Called C++ object pointer is null  `sls_datatype_plugin.cpp:965`
- [Logic error] Called C++ object pointer is null  `totalizer.cpp:40`
- [Logic error] Called C++ object pointer is null  `array_internalize.cpp:134`
- [Logic error] Called C++ object pointer is null  `euf_mam.cpp:2160`
- [Logic error] Called C++ object pointer is null  `bv_decl_plugin.h:471`
- [Logic error] Called C++ object pointer is null  `seq_skolem.cpp:191`
- [Logic error] Called C++ object pointer is null  `value_sweep.cpp:72`
- [Logic error] Called C++ object pointer is null  `smt_context.h:319`
- [Logic error] Called C++ object pointer is null  `seq_axioms.cpp:299`
- [Logic error] Called C++ object pointer is null  `degree_shift_tactic.cpp:204`
- [Logic error] Called C++ object pointer is null  `euf_egraph.h:273`
- [Logic error] Called C++ object pointer is null  `mam.cpp:1120`
- [Logic error] Called C++ object pointer is null  `theory_seq.cpp:1628`
- [Logic error] Called C++ object pointer is null  `ast.h:947`
- [Logic error] Called C++ object pointer is null  `smt_context.h:743`
- [Logic error] Called C++ object pointer is null  `realclosure.cpp:3477`
- [Logic error] Called C++ object pointer is null  `bv2int_translator.cpp:58`
- [Logic error] Called C++ object pointer is null  `seq_skolem.cpp:52`
- [Logic error] Called C++ object pointer is null  `datatype_decl_plugin.cpp:188`
- [Logic error] Called C++ object pointer is null  `sls_seq_plugin.cpp:302`
- [Logic error] Called C++ object pointer is null  `totalizer.cpp:40`
- [Logic error] Called C++ object pointer is null  `realclosure.cpp:3494`
- [Logic error] Called C++ object pointer is null  `bv_decl_plugin.h:469`
- [Logic error] Called C++ object pointer is null  `intblast_solver.cpp:517`
- [Logic error] Called C++ object pointer is null  `sls_euf_plugin.cpp:299`
- [Logic error] Called C++ object pointer is null  `seq_eq_solver.cpp:1053`
- [Logic error] Called C++ object pointer is null  `pb_solver.h:274`
- [Logic error] Called C++ object pointer is null  `ast.h:1399`
- [Logic error] Called C++ object pointer is null  `sls_seq_plugin.cpp:340`
- [Logic error] Called C++ object pointer is null  `seq_axioms.cpp:81`
- [Logic error] Called C++ object pointer is null  `sls_seq_plugin.cpp:264`
- [Logic error] Called C++ object pointer is null  `seq_decl_plugin.h:244`
- [Logic error] Called C++ object pointer is null  `theory_seq.cpp:1628`
- [Logic error] Called C++ object pointer is null  `realclosure.cpp:3461`

### Dereference of null pointer (18)
- Dereference of null pointer (loaded from field 'use_list')  `sat_npn3_finder.cpp:219`
- Forming reference to null pointer  `nlsat_solver.cpp:1256`
- Array access (from variable 'domain') results in a null pointer dereference  `cmd_context.cpp:237`
- Forming reference to null pointer  `mam.cpp:3330`
- Forming reference to null pointer  `obj_mark.h:38`
- Array access (from variable 'as') results in a null pointer dereference  `realclosure.cpp:1118`
- Access to field 'm_next' results in a dereference of a null pointer (loaded from field 'm_del_eh')  `polynomial.cpp:2581`
- Array access (from variable 'args') results in a null pointer dereference  `enum2bv_rewriter.cpp:92`
- Dereference of null pointer (loaded from field 'use_list')  `sat_aig_finder.cpp:198`
- Dereference of null pointer (loaded from variable 'x')  `debug.cpp:163`
- Array access (from variable 'vs') results in a null pointer dereference  `parray.h:155`
- Dereference of null pointer (loaded from field 'use_list')  `sat_npn3_finder.cpp:250`
- Dereference of null pointer (loaded from field 'use_list')  `sat_npn3_finder.cpp:292`
- Access to field 'm_next' results in a dereference of a null pointer (loaded from field 'm_next')  `polynomial.cpp:2587`
- Array access (from variable 'args') results in a null pointer dereference  `cmd_context.cpp:1335`
- Array access (from variable 'args') results in a null pointer dereference  `enum2bv_rewriter.cpp:100`
- Forming reference to null pointer  `euf_mam.cpp:3413`
- Access to field 'm_opcode' results in a dereference of a null pointer (loaded from variable 'curr')  `euf_mam.cpp:1708`

### Bitwise shift (9)
- The result of left shift is undefined because the right operand '4294967295' is not smaller than 64  `sorting_network.h:415`
- The result of left shift is undefined because the right operand is not smaller than 32  `enum2bv_rewriter.cpp:67`
- Left shift overflows the capacity of 'unsigned int' (>= 32)  `bit_util.cpp:286`
- The result of right shift is undefined because the right operand is negative  `mpff.cpp:178`
- The result of right shift is undefined because the right operand is negative  `mpff.cpp:164`
- Left shift overflows the capacity of 'unsigned int' (>= 32)  `bit_util.cpp:338`
- Right shift by '32' overflows the capacity of 'unsigned int'  `bit_util.cpp:222`
- Left shift by '32' overflows the capacity of 'int'  `bit_matrix.cpp:128`
- Left shift >= 65, not smaller than 64, capacity of 'uint64_t'  `dl_sparse_table.h:331`

### Branch condition evaluates to a garbage value (3)
- Branch condition evaluates to a garbage value  `spacer_context.cpp:3596`
- Branch condition evaluates to a garbage value  `bit2int.cpp:362`
- Branch condition evaluates to a garbage value  `spacer_context.cpp:3347`

### Returning null reference (5)
- Returning null reference  `euf_ac_plugin.cpp:805`
- Returning null reference  `util.h:259`
- Returning null reference  `sat_extension.h:76`
- Returning null reference  `ref.h:80`
- Returning null reference  `cmd_context.h:428`

### Uninitialized argument value (3)
- 2nd function call argument is an uninitialized value  `nla_core.cpp:569`
- 2nd function call argument is an uninitialized value  `nla_core.cpp:567`
- 1st function call argument is an uninitialized value  `nla_core.cpp:309`

### Result of operation is garbage or undefined (3)  [NEW]
- The left operand of '&' is a garbage value  `act_cache.cpp:175`
- The left operand of '&' is a garbage value  `act_cache.cpp:197`
- The left operand of '!=' is a garbage value  `nla_core.cpp:556`

### Division by zero (1)
- Division by zero  `util.h:356`
```

</details>

## Build Log Excerpt

<details>
<summary>Key warnings 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,108: 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 results in a null pointer dereference [core.NullDereference]
/src/math/realclosure/realclosure.cpp:3461,3477,3494: warning: Called C++ object pointer is null [core.CallAndMessage]
/src/math/polynomial/polynomial.cpp:2581,2587: warning: Access to field results in null pointer dereference [core.NullDereference]
/src/ast/act_cache.cpp:178,179,200: 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]

scan-build: Analysis run complete.
scan-build: 124 bugs found.

Notes

• This report was generated automatically by the Z3 CSA Analysis workflow.
• False positives are likely for core.CallAndMessage findings in inline helper functions like is_app(), is_quantifier() etc. in ast.h — these patterns are intentional in Z3's type-checking API.
• The longest analysis path (60 steps) is in bit2int.cpp:362 and warrants human review.
• 3 new core.UndefinedBinaryOperatorResult findings in act_cache.cpp are worth investigating.
• To reproduce locally: scan-build -o /tmp/csa-report cmake -DCMAKE_BUILD_TYPE=Debug -G Ninja . && scan-build ninja

AI generated by Clang Static Analyzer (CSA) Report

• expires on Mar 8, 2026, 10:06 PM UTC

[github-actions[bot]]

This discussion was automatically closed because it expired on 2026-03-08T22:06:45.899Z.

Closed by Workflow