(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :status sat)
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 64))
(declare-fun z () (_ BitVec 64))
(assert (bvsle z ((_ sign_extend 32) (bvadd (_ bv1844674407 32) x))))
(assert (bvsle y z))
(assert (bvsle (bvadd (_ bv1844674407 32) x)(_ bv0 32)))
(check-sat)
(exit)