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

Incomplete simplification in smtml #212

Open
epatrizio opened this issue Mar 12, 2024 · 2 comments
Open

Incomplete simplification in smtml #212

epatrizio opened this issue Mar 12, 2024 · 2 comments
Assignees
Labels
bug Something isn't working pending smtml

Comments

@epatrizio
Copy link
Collaborator

Context : Symbolic fuzzing #189
Similar errors occur during fuzzing :

Failure("(i64.eq (i64.extend_i48_s (extract (i64 -5690315267789494568) 0 2)) (i64 0))")

Failure("(i32.eq (i32.extend_i16_s (extract (i32 916602011) 0 2)) (i32 0))")

Failure("(i32.to_bool (i32.extend_i16_s (extract (i32 1815251545) 0 2)))")

Failure("(bool.or ([i32.lt](http://i32.lt/) (i32 0) (i32.add (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 925874591))) (bool.or ([i32.lt](http://i32.lt/) (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 0)) (bool.or ([i32.lt](http://i32.lt/) (i32.add (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 925874591)) (i32 0)) ([i32.lt](http://i32.lt/) (i32.add (i32.extend_i16_s (extract (i32 0) 0 2)) (i32 925874590)) (i32 0)))))")
@krtab krtab self-assigned this Mar 12, 2024
@zapashcanon zapashcanon added the bug Something isn't working label Apr 24, 2024
@zapashcanon
Copy link
Member

@filipeom, is this expected ?

@filipeom filipeom self-assigned this Jul 23, 2024
@filipeom
Copy link
Collaborator

Yes, since we're not concretely simplifying extract. I will address this once I change the representation of bitvectors in smtml.

@zapashcanon zapashcanon changed the title Incomplete simplification in Encoding Incomplete simplification in smtml Aug 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working pending smtml
Projects
None yet
Development

No branches or pull requests

4 participants