[WIP] Array theory improvements#8905

Draft

tautschnig wants to merge 18 commits intodiffblue:developfrom

tautschnig:array-fixes

Commits on Apr 8, 2026

Skip Ackermann constraints for derived arrays (weak equivalence)

tautschnig
and
kiro-agent
committed
Accept member expressions with arbitrary struct operands in array solver

tautschnig
and
kiro-agent
committed
Simplify expressions after lowering byte operators for array theory

tautschnig
and
kiro-agent
committed
Handle array typecast with different element sizes in array theory

tautschnig
and
kiro-agent
committed
Document Array_operations2 union-find conflation bug with --arrays-uf-always

tautschnig
and
kiro-agent
committed
Handle simplified equality in array theory byte operator lowering

tautschnig
and
kiro-agent
committed
Add regression test target for --arrays-uf-always

tautschnig
and
kiro-agent
committed
Make with and if array constraints lazy for --refine-arrays

tautschnig
and
kiro-agent
committed
Add regression test for --refine-arrays with --arrays-uf-always

tautschnig
and
kiro-agent
committed
Add regression test target for --arrays-uf-always --refine-arrays

tautschnig
and
kiro-agent
committed
Disable SAT simplifier when --refine-arrays is used

tautschnig
and
kiro-agent
committed
Keep with/if array constraints eager, only Ackermann lazy

tautschnig
and
kiro-agent
committed
Use array comprehension for large byte_extract lowering

tautschnig
and
kiro-agent
committed
Promote arrays-uf-always-member-crash test from KNOWNBUG to CORE

tautschnig
and
kiro-agent
committed
Fix --arrays-uf-always soundness for member-of-index array expressions

tautschnig
and
kiro-agent
committed
Regression test: --arrays-uf-always soundness issue with large struct arrays

tautschnig
and
kiro-agent
committed
Connect array symbol map literals to element-wise constraints

tautschnig
and
kiro-agent
committed
Fix array theory: add with-constraints for SSA-renamed indices

tautschnig
and
kiro-agent
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] Array theory improvements#8905

[WIP] Array theory improvements#8905
tautschnig wants to merge 18 commits intodiffblue:developfrom
tautschnig:array-fixes

Commits on Apr 8, 2026

Skip Ackermann constraints for derived arrays (weak equivalence)

Accept member expressions with arbitrary struct operands in array solver

Simplify expressions after lowering byte operators for array theory

Handle array typecast with different element sizes in array theory

Document Array_operations2 union-find conflation bug with --arrays-uf-always

Handle simplified equality in array theory byte operator lowering

Add regression test target for --arrays-uf-always

Make with and if array constraints lazy for --refine-arrays

Add regression test for --refine-arrays with --arrays-uf-always

Add regression test target for --arrays-uf-always --refine-arrays

Disable SAT simplifier when --refine-arrays is used

Keep with/if array constraints eager, only Ackermann lazy

Use array comprehension for large byte_extract lowering

Promote arrays-uf-always-member-crash test from KNOWNBUG to CORE

Fix --arrays-uf-always soundness for member-of-index array expressions

Regression test: --arrays-uf-always soundness issue with large struct arrays

Connect array symbol map literals to element-wise constraints

Fix array theory: add with-constraints for SSA-renamed indices