(declare-fun SVALUE_3 () (_ BitVec 256))
(declare-fun SVALUE_1 () (_ BitVec 256))
(declare-fun BV () (_ BitVec 256))
(declare-fun a_414 () (_ BitVec 256))(assert (= a_414 #x0000000000000000000000000000000000000000000000008ac7230489e80000))
(declare-fun a_415 () (_ BitVec 256))(assert (= a_415 (bvneg SVALUE_1)))
(declare-fun a_416 () (_ BitVec 256))(assert (= a_416 (bvadd a_414 a_415)))
(declare-fun a_417 () Bool)(assert (= a_417 (bvuge a_416 SVALUE_3)))
(declare-fun a_418 () (_ BitVec 256))(assert (= a_418 (bvadd SVALUE_1 SVALUE_3)))
(declare-fun a_419 () (_ BitVec 256))(assert (= a_419 #x0000000000000000000000000000000000000000000000000000000000000000))
(declare-fun a_420 () Bool)(assert (= a_420 (bvugt a_418 a_419)))
(declare-fun a_421 () Bool)(assert (= a_421 (not a_420)))
(declare-fun a_422 () (_ BitVec 256))(assert (= a_422 #x000000000000000000000000000000000000000000000000000000000000015a))
(declare-fun a_423 () (_ BitVec 256))(assert (= a_423 #x00000000000000000000000000000000000000000000000000000000000000bf))
(declare-fun a_424 () (_ BitVec 256))(assert (= a_424 (ite a_421 a_422 a_423)))
(declare-fun a_425 () (_ BitVec 256))(assert (= a_425 #x00000000000000000000000000000000000000000000000000000000000003e8))
(declare-fun a_426 () (_ BitVec 256))(assert (= a_426 (bvadd SVALUE_1 SVALUE_3)))
(declare-fun a_427 () (_ BitVec 256))(assert (= a_427 #x00000000000000000000000000000000000000000000000000000000000003e8))
(declare-fun a_428 () (_ BitVec 256))(assert (= a_428 #x0000000000000000000000000000000000000000000000008ac7230489e80000))
(declare-fun a_429 () Bool)(assert (= a_429 (bvule SVALUE_1 a_428)))
(assert (= a_429 true))
(assert (bvult a_426 a_427))
(assert (bvult SVALUE_1 a_425))
(assert (= BV a_424))
(assert (= a_417 true))
(check-sat)
(get-info :version)