Skip to content

Conversation

kroening
Copy link
Collaborator

No description provided.

This adds a test for an assignment to an indexed part select with constant
indices.  The test yields invalid SMT-LIB.
This fixes an off-by-one error in the synthesis for indexed part select
expressions.
@kroening kroening force-pushed the synth-indexed-part-select branch from f0519d9 to de838e5 Compare August 15, 2024 16:37
This uses the synthesis_constant(...) method to enable the synthesis of
assignments to indexed part select LHSs that have a variable (but known at
synthesis time) index.
@kroening kroening force-pushed the synth-indexed-part-select branch from de838e5 to 86a6be6 Compare August 15, 2024 20:50
@kroening kroening marked this pull request as ready for review August 15, 2024 20:51
@tautschnig tautschnig merged commit 3d4b5d4 into main Aug 16, 2024
8 checks passed
@tautschnig tautschnig deleted the synth-indexed-part-select branch August 16, 2024 12:34
Romy15200 pushed a commit to Romy15200/nws that referenced this pull request Aug 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants