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

assume works incorrectly with very negative integer #6

Open
joonazan opened this issue May 23, 2024 · 1 comment
Open

assume works incorrectly with very negative integer #6

joonazan opened this issue May 23, 2024 · 1 comment

Comments

@joonazan
Copy link

use symex_lib::{any, assume};

fn main() {
    let x: i128 = i128::MIN;
    assume(x < 0);
    assert_eq!(-x.abs(), x);
}

This code produces Encountered an unsatisfiable assumption, ignoring this path, even though the smallest value of i128 is definitely less than zero.

@joonazan
Copy link
Author

i64 works fine, so I would assume the VM has some problem with 128 bit integers.

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