Created
April 23, 2021 08:54
-
-
Save leonardoalt/6f08f54654ed8ebe4620e1b06eed9edc to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-logic HORN) | |
| (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) | |
| (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-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) | |
| (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) | |
| (declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int))))) | |
| (declare-datatypes ((|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| 0)) (((|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input_0| Int) (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input_1| Int) (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input_2| |uint_array_tuple|))))) | |
| (declare-datatypes ((|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| 0)) (((|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input_0| |bytes_tuple|) (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input_1| Int) (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input_2| |uint_array_tuple|))))) | |
| (declare-datatypes ((|abi_type| 0)) (((|abi_type| (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr| (Array |t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| |bytes_tuple|)) (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr| (Array |t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| |bytes_tuple|)))))) | |
| (declare-fun |interface_0_C_47_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) | |
| (declare-fun |nondet_interface_1_C_47_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) | |
| (declare-fun |summary_constructor_2_C_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (assert | |
| (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) | |
| (=> (= error_0 0) (nondet_interface_1_C_47_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) | |
| (declare-fun |summary_3_function_f__46_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |bytes_tuple| Int |uint_array_tuple| |state_type| |bytes_tuple| Int |uint_array_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (nondet_interface_1_C_47_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_3_function_f__46_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_2 sig_3_length_pair_1 x_5_1 a_8_length_pair_1))) (nondet_interface_1_C_47_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) | |
| (declare-fun |block_4_function_f__46_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |bytes_tuple| Int |uint_array_tuple| |state_type| |bytes_tuple| Int |uint_array_tuple| |bytes_tuple| |bytes_tuple| ) Bool) | |
| (declare-fun |block_5_f_45_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |bytes_tuple| Int |uint_array_tuple| |state_type| |bytes_tuple| Int |uint_array_tuple| |bytes_tuple| |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (block_4_function_f__46_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_1 b2_21_length_pair_1))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (block_4_function_f__46_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_1 b2_21_length_pair_1) (and (and (and (and (and (= state_1 state_0) (= error_0 0)) (= sig_3_length_pair_0 sig_3_length_pair_1)) (= x_5_0 x_5_1)) (= a_8_length_pair_0 a_8_length_pair_1)) true)) true) (block_5_f_45_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_1 b2_21_length_pair_1)))) | |
| (declare-fun |block_6_return_function_f__46_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |bytes_tuple| Int |uint_array_tuple| |state_type| |bytes_tuple| Int |uint_array_tuple| |bytes_tuple| |bytes_tuple| ) Bool) | |
| (declare-fun |block_7_function_f__46_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |bytes_tuple| Int |uint_array_tuple| |state_type| |bytes_tuple| Int |uint_array_tuple| |bytes_tuple| |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (block_5_f_45_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_1 b2_21_length_pair_1) (and (= expr_42_1 (= expr_39_1 expr_41_1)) (and (and (>= expr_41_1 0) (<= expr_41_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_41_1 0) (<= expr_41_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_41_1 (|bytes_tuple_accessor_length| expr_40_length_pair_0)) (and (= expr_40_length_pair_0 b2_21_length_pair_2) (and (and (>= expr_39_1 0) (<= expr_39_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_39_1 0) (<= expr_39_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_39_1 (|bytes_tuple_accessor_length| expr_38_length_pair_0)) (and (= expr_38_length_pair_0 b1_12_length_pair_2) (and (= b2_21_length_pair_2 expr_35_length_pair_1) (and (= expr_35_length_pair_1 (select (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr| abi_0) (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| expr_32_2 expr_33_0 expr_34_length_pair_0))) (and (= expr_34_length_pair_0 a_8_length_pair_1) (and (=> true (and (>= expr_33_0 0) (<= expr_33_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_33_0 x_5_1) (and (=> true (and (>= expr_32_2 0) (<= expr_32_2 4294967295))) (and (= expr_32_2 (bv2nat (bvlshr (ite (>= expr_31_1 0) ((_ int2bv 256) expr_31_1) (bvneg ((_ int2bv 256) (- expr_31_1)))) (ite (>= 224 0) ((_ int2bv 256) 224) (bvneg ((_ int2bv 256) (- 224))))))) (and (=> true (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (select (|keccak256| crypto_0) expr_30_length_pair_1)) (and (= expr_30_length_pair_1 expr_29_length_pair_0) (and (= expr_29_length_pair_0 sig_3_length_pair_1) (and true (and (= b1_12_length_pair_2 expr_18_length_pair_1) (and (= expr_18_length_pair_1 (select (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr| abi_0) (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| expr_15_length_pair_0 expr_16_0 expr_17_length_pair_0))) (and (= expr_17_length_pair_0 a_8_length_pair_1) (and (=> true (and (>= expr_16_0 0) (<= expr_16_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_16_0 x_5_1) (and (= expr_15_length_pair_0 sig_3_length_pair_1) (and (>= (|uint_array_tuple_accessor_length| a_8_length_pair_1) 0) (and (and (>= x_5_1 0) (<= x_5_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|bytes_tuple_accessor_length| sig_3_length_pair_1) 0) (and (= b2_21_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b1_12_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) true))))))))))))))))))))))))))))))))) (and (not expr_42_1) (= error_1 1))) (block_7_function_f__46_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_2 b2_21_length_pair_2)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (block_7_function_f__46_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_2 b2_21_length_pair_2) (summary_3_function_f__46_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (block_5_f_45_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_1 b2_21_length_pair_1) (and (= error_1 error_0) (and (= expr_42_1 (= expr_39_1 expr_41_1)) (and (and (>= expr_41_1 0) (<= expr_41_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_41_1 0) (<= expr_41_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_41_1 (|bytes_tuple_accessor_length| expr_40_length_pair_0)) (and (= expr_40_length_pair_0 b2_21_length_pair_2) (and (and (>= expr_39_1 0) (<= expr_39_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_39_1 0) (<= expr_39_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_39_1 (|bytes_tuple_accessor_length| expr_38_length_pair_0)) (and (= expr_38_length_pair_0 b1_12_length_pair_2) (and (= b2_21_length_pair_2 expr_35_length_pair_1) (and (= expr_35_length_pair_1 (select (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr| abi_0) (|t_function_abiencodewithselector_pure(t_bytes4)returns(t_bytes_memory_ptr)_t_bytes4_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| expr_32_2 expr_33_0 expr_34_length_pair_0))) (and (= expr_34_length_pair_0 a_8_length_pair_1) (and (=> true (and (>= expr_33_0 0) (<= expr_33_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_33_0 x_5_1) (and (=> true (and (>= expr_32_2 0) (<= expr_32_2 4294967295))) (and (= expr_32_2 (bv2nat (bvlshr (ite (>= expr_31_1 0) ((_ int2bv 256) expr_31_1) (bvneg ((_ int2bv 256) (- expr_31_1)))) (ite (>= 224 0) ((_ int2bv 256) 224) (bvneg ((_ int2bv 256) (- 224))))))) (and (=> true (and (>= expr_31_1 0) (<= expr_31_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_1 (select (|keccak256| crypto_0) expr_30_length_pair_1)) (and (= expr_30_length_pair_1 expr_29_length_pair_0) (and (= expr_29_length_pair_0 sig_3_length_pair_1) (and true (and (= b1_12_length_pair_2 expr_18_length_pair_1) (and (= expr_18_length_pair_1 (select (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr| abi_0) (|t_function_abiencodewithsignature_pure(t_string_memory_ptr)returns(t_bytes_memory_ptr)_t_string_memory_ptr_t_uint256_t_array(t_uint256)dyn_memory_ptr_t_bytes_memory_ptr_input| expr_15_length_pair_0 expr_16_0 expr_17_length_pair_0))) (and (= expr_17_length_pair_0 a_8_length_pair_1) (and (=> true (and (>= expr_16_0 0) (<= expr_16_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_16_0 x_5_1) (and (= expr_15_length_pair_0 sig_3_length_pair_1) (and (>= (|uint_array_tuple_accessor_length| a_8_length_pair_1) 0) (and (and (>= x_5_1 0) (<= x_5_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|bytes_tuple_accessor_length| sig_3_length_pair_1) 0) (and (= b2_21_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b1_12_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) true)))))))))))))))))))))))))))))))))) true) (block_6_return_function_f__46_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_2 b2_21_length_pair_2)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (block_6_return_function_f__46_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1 b1_12_length_pair_1 b2_21_length_pair_1) true) true) (summary_3_function_f__46_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (interface_0_C_47_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2654428275)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 158)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 55)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 92)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 115)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_3_function_f__46_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1)) (= error_0 0))) (interface_0_C_47_0 this_0 abi_0 crypto_0 state_1)))) | |
| (declare-fun |contract_initializer_8_C_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (declare-fun |contract_initializer_entry_9_C_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (= state_1 state_0) (= error_0 0)) (contract_initializer_entry_9_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (declare-fun |contract_initializer_after_init_10_C_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (contract_initializer_entry_9_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_10_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (contract_initializer_after_init_10_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_8_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (declare-fun |implicit_constructor_entry_11_C_47_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (= state_1 state_0) (= error_0 0)) true) (implicit_constructor_entry_11_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (implicit_constructor_entry_11_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_8_C_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (implicit_constructor_entry_11_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_8_C_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_47_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int)) | |
| (=> (and (and (summary_constructor_2_C_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_47_0 this_0 abi_0 crypto_0 state_1)))) | |
| (declare-fun |error_target_2_0| () Bool) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (a_8_length_pair_2 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (sig_3_length_pair_2 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) | |
| (=> (and (and (interface_0_C_47_0 this_0 abi_0 crypto_0 state_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2654428275)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 158)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 55)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 92)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 115)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_3_function_f__46_47_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 sig_3_length_pair_0 x_5_0 a_8_length_pair_0 state_1 sig_3_length_pair_1 x_5_1 a_8_length_pair_1)) (= error_0 1))) error_target_2_0))) | |
| (assert | |
| (forall ( (a_8_length_pair_0 |uint_array_tuple|) (a_8_length_pair_1 |uint_array_tuple|) (a_8_length_pair_2 |uint_array_tuple|) (abi_0 |abi_type|) (b1_12_length_pair_0 |bytes_tuple|) (b1_12_length_pair_1 |bytes_tuple|) (b1_12_length_pair_2 |bytes_tuple|) (b2_21_length_pair_0 |bytes_tuple|) (b2_21_length_pair_1 |bytes_tuple|) (b2_21_length_pair_2 |bytes_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_15_length_pair_0 |bytes_tuple|) (expr_16_0 Int) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_length_pair_0 |bytes_tuple|) (expr_18_length_pair_1 |bytes_tuple|) (expr_29_length_pair_0 |bytes_tuple|) (expr_30_length_pair_0 |bytes_tuple|) (expr_30_length_pair_1 |bytes_tuple|) (expr_31_1 Int) (expr_32_1 Int) (expr_32_2 Int) (expr_33_0 Int) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |bytes_tuple|) (expr_35_length_pair_1 |bytes_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_39_1 Int) (expr_40_length_pair_0 |bytes_tuple|) (expr_41_1 Int) (expr_42_1 Bool) (sig_3_length_pair_0 |bytes_tuple|) (sig_3_length_pair_1 |bytes_tuple|) (sig_3_length_pair_2 |bytes_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (t_function_keccak256_pure$_t_bytes_memory_ptr_$returns$_t_bytes32_$_abstract_0 Int) (this_0 Int) (tx_0 |tx_type|) (x_5_0 Int) (x_5_1 Int) (x_5_2 Int)) | |
| (=> error_target_2_0 false))) | |
| (check-sat) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment