Skip to content

Conversation

@kroening
Copy link
Collaborator

This switches the range annotation on primitive gates to the unpacked array as required by 1800-2017.

This switches the "range" annotation on primitive gates to the unpacked
array as required by 1800-2017.
@kroening kroening force-pushed the primitive-gates-instance-array branch from 087d6bf to c6d43ab Compare December 20, 2025 00:06
@kroening kroening marked this pull request as ready for review December 20, 2025 00:13
auto &array_type = to_array_type(inst.instance_array());
auto width =
numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
inst.type() = unsignedbv_typet{width};
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I understand that this isn't any different from what it was before, but still: why is unsignedbv_typet the right type here? I would have picked bv_typet.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants