Skip to content

Reference concerning union types#85

Open
vhavlena wants to merge 3 commits into
mainfrom
ref-index
Open

Reference concerning union types#85
vhavlena wants to merge 3 commits into
mainfrom
ref-index

Conversation

@vhavlena

@vhavlena vhavlena commented Jun 23, 2026

Copy link
Copy Markdown
Collaborator

This pull request improves support for nested indexing into heterogeneous (union-typed) arrays in the SMT translation layer, and adds a corresponding end-to-end test. The main change is the implementation of logic to correctly handle references that index into arrays nested inside union-typed arrays, which previously was not supported. Several helper functions were added and minor code cleanups were made.

@vhavlena vhavlena linked an issue Jun 23, 2026 that may be closed by this pull request
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

SMT translation fails for heterogeneous (mixed-type) array indexing

1 participant