(set-logic QF_BV)
(declare-fun x () (_ BitVec 22))
(declare-fun y () (_ BitVec 53))
(assert 
  (let ((e8 ((_ repeat 1) x))) 
  (let ((e20 (bvadd y ((_ sign_extend 31) e8)))) 
  (let ((e62 (distinct y e20))) 
  (let ((e69 (bvsgt ((_ zero_extend 57) x) (_ bv0 79)))) 
  (let ((e125 (not e62))) 
  (let ((e128 e69)) 
  (let ((e130 (= e125 e128))) 
  (let ((e152 (not e130))) 
  (let ((e158 (and e152 e152))) 
  (let ((e159 (xor true e158))) 
  (let ((e160 e159)) 
  (let ((e161 e160)) 
  (let ((e162 e161)) e162))))))))))))))
(check-sat)

