Simplifying ite and extract

[ychen306]

How do you get z3 to simplify (ite (= (extract i i x) 0) 0 1) into (zeroext (extract...))?

[NikolajBjorner]

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)))