We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
How do you get z3 to simplify (ite (= (extract i i x) 0) 0 1) into (zeroext (extract...))?
(ite (= (extract i i x) 0) 0 1)
(zeroext (extract...))
The text was updated successfully, but these errors were encountered:
42e2145
z3 2479.smt2 rewriter.bv_ite2id=true
where 2479.smt2 is:
(declare-const x (_ BitVec 64)) (simplify (ite (= (_ bv1 1) ((_ extract 21 21) x)) (_ bv1 64) (_ bv0 64))) (simplify (ite (= (_ bv0 1) ((_ extract 21 21) x)) (_ bv1 64) (_ bv0 64))) (simplify (ite (= (_ bv1 1) ((_ extract 21 21) x)) (_ bv0 64) (_ bv1 64))) (simplify (ite (= (_ bv0 1) ((_ extract 21 21) x)) (_ bv0 64) (_ bv1 64)))
Sorry, something went wrong.
No branches or pull requests
How do you get z3 to simplify
(ite (= (extract i i x) 0) 0 1)
into(zeroext (extract...))
?The text was updated successfully, but these errors were encountered: