timeout.smt2

(declare-datatypes ((bytes_tuple 0)) (((bytes_tuple (bytes_tuple_accessor_array (Array Int Int)) (bytes_tuple_accessor_length Int)))))
(declare-datatypes ((tx_type 0)) (((tx_type (block.chainid Int) (block.coinbase Int) (block.difficulty Int) (block.gaslimit Int) (block.number Int) (block.timestamp Int) (blockhash (Array Int Int)) (msg.data bytes_tuple) (msg.sender Int) (msg.sig Int) (msg.value Int) (tx.gasprice Int) (tx.origin Int)))))
(declare-fun expr_45_1 () Bool)
(declare-fun tx_0 () tx_type)
(declare-fun r_33_0 () Int)
(declare-fun x_3_0 () Int)
(declare-fun y_5_0 () Int)
(declare-fun k_7_0 () Int)
(declare-fun expr_11_0 () Int)
(declare-fun expr_12_0 () Int)
(declare-fun expr_13_1 () Bool)
(declare-fun expr_17_0 () Int)
(declare-fun expr_18_0 () Int)
(declare-fun r_div_mod_0_0 () Int)
(declare-fun d_div_mod_0_0 () Int)
(declare-fun expr_19_1 () Int)
(declare-fun expr_20_0 () Int)
(declare-fun expr_21_1 () Bool)
(declare-fun expr_25_0 () Int)
(declare-fun expr_26_0 () Int)
(declare-fun r_div_mod_1_0 () Int)
(declare-fun d_div_mod_1_0 () Int)
(declare-fun expr_27_1 () Int)
(declare-fun expr_28_0 () Int)
(declare-fun expr_29_1 () Bool)
(declare-fun expr_35_0 () Int)
(declare-fun expr_36_0 () Int)
(declare-fun expr_37_0 () Int)
(declare-fun r_div_mod_2_0 () Int)
(declare-fun d_div_mod_2_0 () Int)
(declare-fun expr_38_1 () Int)
(declare-fun r_33_1 () Int)
(declare-fun expr_41_0 () Int)
(declare-fun expr_42_0 () Int)
(declare-fun r_div_mod_3_0 () Int)
(declare-fun d_div_mod_3_0 () Int)
(declare-fun expr_43_1 () Int)
(declare-fun expr_44_0 () Int)
(assert (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 0) 191))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 1) 6))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 2) 219))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data tx_0)) 3) 241)))
  (and (and true true)
       (= expr_45_1 (= expr_43_1 expr_44_0))
       (=> (and true true) true)
       (= expr_44_0 0)
       (=> (and true true)
           (and (>= expr_43_1 0)
                (<= expr_43_1
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_43_1 (ite (= expr_42_0 0) 0 r_div_mod_3_0))
       (<= 0 r_div_mod_3_0)
       (or (= expr_42_0 0) (< r_div_mod_3_0 expr_42_0))
       (= (+ (* d_div_mod_3_0 expr_42_0) r_div_mod_3_0) expr_41_0)
       (=> (and true true)
           (and (>= expr_42_0 0)
                (<= expr_42_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_42_0 k_7_0)
       (=> (and true true)
           (and (>= expr_41_0 0)
                (<= expr_41_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_41_0 r_33_1)
       (ite (and true true) (= r_33_1 expr_38_1) (= r_33_1 r_33_0))
       (=> (and true true)
           (and (>= expr_38_1 0)
                (<= expr_38_1
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_38_1 (ite (= expr_37_0 0) 0 r_div_mod_2_0))
       (<= 0 r_div_mod_2_0)
       (or (= expr_37_0 0) (< r_div_mod_2_0 expr_37_0))
       (= (+ (* d_div_mod_2_0 expr_37_0) r_div_mod_2_0) (* expr_35_0 expr_36_0))
       (=> (and true true)
           (and (>= expr_37_0 0)
                (<= expr_37_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_37_0 k_7_0)
       (=> (and true true)
           (and (>= expr_36_0 0)
                (<= expr_36_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_36_0 y_5_0)
       (=> (and true true)
           (and (>= expr_35_0 0)
                (<= expr_35_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_35_0 x_3_0)
       true
       (=> (and true true) expr_29_1)
       (= expr_29_1 (= expr_27_1 expr_28_0))
       (=> (and true true) true)
       (= expr_28_0 0)
       (=> (and true true)
           (and (>= expr_27_1 0)
                (<= expr_27_1
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_27_1 (ite (= expr_26_0 0) 0 r_div_mod_1_0))
       (<= 0 r_div_mod_1_0)
       (or (= expr_26_0 0) (< r_div_mod_1_0 expr_26_0))
       (= (+ (* d_div_mod_1_0 expr_26_0) r_div_mod_1_0) expr_25_0)
       (=> (and true true)
           (and (>= expr_26_0 0)
                (<= expr_26_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_26_0 k_7_0)
       (=> (and true true)
           (and (>= expr_25_0 0)
                (<= expr_25_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_25_0 y_5_0)
       (=> (and true true) expr_21_1)
       (= expr_21_1 (= expr_19_1 expr_20_0))
       (=> (and true true) true)
       (= expr_20_0 0)
       (=> (and true true)
           (and (>= expr_19_1 0)
                (<= expr_19_1
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_19_1 (ite (= expr_18_0 0) 0 r_div_mod_0_0))
       (<= 0 r_div_mod_0_0)
       (or (= expr_18_0 0) (< r_div_mod_0_0 expr_18_0))
       (= (+ (* d_div_mod_0_0 expr_18_0) r_div_mod_0_0) expr_17_0)
       (=> (and true true)
           (and (>= expr_18_0 0)
                (<= expr_18_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_18_0 k_7_0)
       (=> (and true true)
           (and (>= expr_17_0 0)
                (<= expr_17_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_17_0 x_3_0)
       (=> (and true true) expr_13_1)
       (= expr_13_1 (> expr_11_0 expr_12_0))
       (=> (and true true) true)
       (= expr_12_0 0)
       (=> (and true true)
           (and (>= expr_11_0 0)
                (<= expr_11_0
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)))
       (= expr_11_0 k_7_0)
       (>= k_7_0 0)
       (<= k_7_0
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= y_5_0 0)
       (<= y_5_0
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= x_3_0 0)
       (<= x_3_0
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (= r_33_0 0)
       (>= (block.chainid tx_0) 0)
       (<= (block.chainid tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.coinbase tx_0) 0)
       (<= (block.coinbase tx_0)
           1461501637330902918203684832716283019655932542975)
       (>= (block.difficulty tx_0) 0)
       (<= (block.difficulty tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.gaslimit tx_0) 0)
       (<= (block.gaslimit tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.number tx_0) 0)
       (<= (block.number tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (block.timestamp tx_0) 0)
       (<= (block.timestamp tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (msg.sender tx_0) 0)
       (<= (msg.sender tx_0) 1461501637330902918203684832716283019655932542975)
       (>= (msg.value tx_0) 0)
       (<= (msg.value tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (>= (tx.origin tx_0) 0)
       (<= (tx.origin tx_0) 1461501637330902918203684832716283019655932542975)
       (>= (tx.gasprice tx_0) 0)
       (<= (tx.gasprice tx_0)
           115792089237316195423570985008687907853269984665640564039457584007913129639935)
       (= (msg.value tx_0) 0)
       (= (msg.sig tx_0) 3204897777)
       a!1
       a!2
       a!3
       a!4
       (>= (bytes_tuple_accessor_length (msg.data tx_0)) 4)
       true
       (not expr_45_1))))

(check-sat)