(set-info :status unsat)
(declare-const x Bool)
(assert (and (exists ((y (_ BitVec 32))) true) (forall ((y (_ BitVec 32))) (and x (exists ((y2 (_ BitVec 32))) (forall ((? (_ BitVec 32))) (bvsle (_ bv0 32) (bvadd ? y2 y))))))))
(check-sat)