(define-type bv-type-32 (bitvector 32))
(define EIP_0_1_0::bv-type-32)
(define temp-var-0::bv-type-32 (mk-bv 32 7))
(define temp-var-22::bv-type-32 (mk-bv 32 0))
(define temp-var-1::bool (= EIP_0_1_0 temp-var-0))
(define ESP_0_1_0::bv-type-32)
(define ESP_0_0_0::bv-type-32)
(define temp-var-2::bv-type-32 (mk-bv 32 4294967292))
(define temp-var-3::bv-type-32 (bv-add ESP_0_0_0 temp-var-2))
(define temp-var-4::bool (= ESP_0_1_0 temp-var-3))
(define temp-var-5::bool (and temp-var-1 temp-var-4))
(define temp-var-54::bv-type-32 (bv-mul ESP_0_1_0 (mk-bv 32 473028019)))
(define temp-var-55::bv-type-32 (bv-mul temp-var-0 (mk-bv 32 956831788)))
(define temp-var-56::bv-type-32 (bv-sub temp-var-54 temp-var-55))
(define temp-var-57::bv-type-32 (bv-mul ESP_0_0_0 (mk-bv 32 473028019)))
(define temp-var-58::bv-type-32 (bv-sub temp-var-56 temp-var-57))
(define temp-var-59::bool (= temp-var-22 temp-var-58))
(define temp-var-65::bool (not temp-var-59))
(define temp-var-66::bool (and temp-var-5 temp-var-65))
(assert temp-var-66)
(check)