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.

Sign up for GitHub

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

Jump to bottom

[FEATURE] Make sure that apalache works with math over big integers #450

Closed
konnov opened this issue Jan 19, 2021 · 0 comments
Closed

[FEATURE] Make sure that apalache works with math over big integers #450

konnov opened this issue Jan 19, 2021 · 0 comments
Assignees
@konnov
Labels
new New issue to be triaged. usability UX improvements
Milestone
January iteration...

Comments

@konnov
Copy link
Collaborator

konnov commented Jan 19, 2021

SMT does not restrict the size of the integers. Neither should do apalache. We have to make sure that the preprocessing does not accidentally truncate big integers.
@konnov konnov added new New issue to be triaged. usability UX improvements labels Jan 19, 2021
@konnov konnov added this to the January iteration milestone Jan 19, 2021
@konnov konnov self-assigned this Jan 19, 2021
konnov added a commit that referenced this issue Jan 19, 2021
@konnov
closed #450 and #197: handling big integers and better preprocessing
5da4558
@konnov konnov mentioned this issue Jan 19, 2021
Merged
3 tasks
@konnov konnov closed this as completed Jan 19, 2021
konnov added a commit that referenced this issue Jan 21, 2021
@konnov
closed #450 and #197: handling big integers and better preprocessing (#…
de4505d 
…452)

* closed #450 and #197: handling big integers and better preprocessing

Co-authored-by: Shon Feder <shon@informal.systems>
This was referenced Jan 25, 2021
Closed
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@konnov konnov

Labels
new New issue to be triaged. usability UX improvements
Projects
None yet
Milestone
January iteration 2021
Development

No branches or pull requests
1 participant
@konnov