Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fixes issue #6119 #6120

Merged
merged 1 commit into from
Jun 29, 2022
Merged

fixes issue #6119 #6120

merged 1 commit into from
Jun 29, 2022

Conversation

joe-hauns
Copy link
Contributor

Makes sure that two equal integers always have the same hash value, even in corner cases where they are represented differently.
The issue observed was that the integer -2147483647 was hashed to different values depending on being represented as small or large integer.
In the small case it used to be hashed to unsigned(-2147483647) which is 2147483649, and in the large case it was hashed to 2147483647, as the digits are all represented as unsigneds anyways.

@NikolajBjorner NikolajBjorner merged commit 03287d6 into Z3Prover:master Jun 29, 2022
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.

2 participants