In [15]: print(rip_ast)
((_ extract 63 0) ((_ zero_extend 0) (ite (= (bvor (bvxor ((_ extract 0 0) ((_ extract 31 31) (bvsub ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8))))) ((_ extract 0 0) ((_ extract 31 31) (bvand (bvxor ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8))) (bvxor ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ extract 31 0) (bvsub ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8))))))))) ((_ extract 0 0) (ite (= ((_ extract 31 0) (bvsub ((_ extract 31 0) ((_ zero_extend 32) SymVar_0)) ((_ sign_extend 24) (_ bv4 8)))) (_ bv0 32)) (_ bv1 1) (_ bv0 1)))) (_ bv1 1)) (_ bv20 64) (_ bv5 64))))

In [16]: state.ctx.simplify(rip_ast,True)
---------------------------------------------------------------------------
TypeError                                 Traceback (most recent call last)
<ipython-input-16-743ad7e3a694> in <module>()
----> 1 state.ctx.simplify(rip_ast,True)

TypeError: Z3ToTritonAst::visit(): 'iff' AST node not supported yet