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

Question on simplify() #5929

Closed
qingkaishi opened this issue Mar 28, 2022 · 1 comment
Closed

Question on simplify() #5929

qingkaishi opened this issue Mar 28, 2022 · 1 comment

Comments

@qingkaishi
Copy link

Z3's simplify() function simplifies -4 + len <= 2 to extract(-4 + len, 63, 2) = 0 && extract(len, 1, 0) ≤ #b10.

Here, len is a 64bit bitvector, <= is unsigned. extract(v, high, low) just means extracting the bits from high to low.

I am wondering which simplification procedure does this simplification. I want to close it. I tried to use simplify(params const & p) but fail to find the correct options I need to pass into this API. Could you help?
@NikolajBjorner
Copy link
Contributor

To disable this requires a new parameter.

qingkaishi pushed a commit to qingkaishi/z3 that referenced this issue Mar 28, 2022
@NikolajBjorner @qingkaishi
fix Z3Prover#5929 - add parameter bv_le2extract to allow disabling th…
7ed5da1 
…e disassembly to extract
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @qingkaishi