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

Floating point exception when dividing large integers by zero #303

Closed
1 task done
TwoFX opened this issue Feb 5, 2021 · 0 comments
Closed
1 task done

Floating point exception when dividing large integers by zero #303

TwoFX opened this issue Feb 5, 2021 · 0 comments

Comments

@TwoFX
Copy link
Member

TwoFX commented Feb 5, 2021

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

In c4cfbce, a test was added to ensure that taking large Ints modulo zero does not crash Lean. However, the same test with % replaced by / still causes a Floating point exception.

#eval (2147483648 / 0) + (-0)

Expected behavior: The program should run sucessfully and print 0.

Actual behavior: The program exits abnormally with a Floating point exception.

Reproduces how often: 100%

Versions

Lean (version 4.0.0-nightly-2021-02-05, commit bdf7b15a4125, Release)

Ubuntu 20.04

ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 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

No branches or pull requests

1 participant