Created
November 30, 2022 18:41
-
-
Save leonardoalt/25c938e2963dd435138653312421496d 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.basefee| Int) (|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 ((|abi_type| 0)) (((|abi_type| (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| (Array |uint_array_tuple| |bytes_tuple|)) (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_t_bytes_memory_ptr| (Array |uint_array_tuple| |bytes_tuple|)))))) | |
| (declare-datatypes ((|array_length_pair| 0)) (((|array_length_pair| (|array| (Array Int Int)) (|length| Int))))) | |
| (declare-fun |interface_0_C_94_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) | |
| (declare-fun |nondet_interface_1_C_94_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) | |
| (declare-fun |summary_constructor_2_C_94_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_94_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) | |
| (declare-fun |summary_3_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| ) Bool) | |
| (declare-fun |summary_4_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| ) Bool) | |
| (assert | |
| (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|)) | |
| (=> (and (and (nondet_interface_1_C_94_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_abiEncodeSlice__93_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 data_3_length_pair_0 state_2 data_3_length_pair_1))) (nondet_interface_1_C_94_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) | |
| (declare-fun |block_5_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (declare-fun |block_6_abiEncodeSlice_92_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (block_5_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1))) | |
| (assert | |
| (forall ( (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (and (and (block_5_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= data_3_length_pair_1 data_3_length_pair_0))) true)) true) (block_6_abiEncodeSlice_92_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1)))) | |
| (declare-fun |block_7_return_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (declare-fun |array_slice_uint_array_tuple_0| ((Array Int Int) (Array Int Int) Int Int ) Bool) | |
| (declare-fun |array_slice_header_uint_array_tuple_0| ((Array Int Int) (Array Int Int) Int Int Int ) Bool) | |
| (declare-fun |array_slice_loop_uint_array_tuple_0| ((Array Int Int) (Array Int Int) Int Int Int ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (> end_uint_array_tuple_0 start_uint_array_tuple_0) (array_slice_header_uint_array_tuple_0 (|array| a_uint_array_tuple_array_length_pair_0) (|array| b_uint_array_tuple_array_length_pair_0) start_uint_array_tuple_0 end_uint_array_tuple_0 0)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (and (array_slice_header_uint_array_tuple_0 (|array| a_uint_array_tuple_array_length_pair_0) (|array| b_uint_array_tuple_array_length_pair_0) start_uint_array_tuple_0 end_uint_array_tuple_0 i_uint_array_tuple_0) (>= i_uint_array_tuple_0 (- end_uint_array_tuple_0 start_uint_array_tuple_0))) (array_slice_uint_array_tuple_0 (|array| a_uint_array_tuple_array_length_pair_0) (|array| b_uint_array_tuple_array_length_pair_0) start_uint_array_tuple_0 end_uint_array_tuple_0)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (and (and (array_slice_header_uint_array_tuple_0 (|array| a_uint_array_tuple_array_length_pair_0) (|array| b_uint_array_tuple_array_length_pair_0) start_uint_array_tuple_0 end_uint_array_tuple_0 i_uint_array_tuple_0) (>= i_uint_array_tuple_0 0)) (< i_uint_array_tuple_0 (- end_uint_array_tuple_0 start_uint_array_tuple_0))) (array_slice_loop_uint_array_tuple_0 (|array| a_uint_array_tuple_array_length_pair_0) (|array| b_uint_array_tuple_array_length_pair_0) start_uint_array_tuple_0 end_uint_array_tuple_0 i_uint_array_tuple_0)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (and (array_slice_loop_uint_array_tuple_0 (|array| a_uint_array_tuple_array_length_pair_0) (|array| b_uint_array_tuple_array_length_pair_0) start_uint_array_tuple_0 end_uint_array_tuple_0 i_uint_array_tuple_0) (= (select (|array| b_uint_array_tuple_array_length_pair_0) i_uint_array_tuple_0) (select (|array| a_uint_array_tuple_array_length_pair_0) (+ start_uint_array_tuple_0 i_uint_array_tuple_0)))) (array_slice_header_uint_array_tuple_0 (|array| a_uint_array_tuple_array_length_pair_0) (|array| b_uint_array_tuple_array_length_pair_0) start_uint_array_tuple_0 end_uint_array_tuple_0 (+ i_uint_array_tuple_0 1))))) | |
| (declare-fun |block_8_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (and (and (block_6_abiEncodeSlice_92_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (and (= expr_27_1 (= expr_24_1 expr_26_1)) (and (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (|bytes_tuple_accessor_length| expr_25_length_pair_0)) (and (= expr_25_length_pair_0 b2_14_length_pair_2) (and (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_24_1 (|bytes_tuple_accessor_length| expr_23_length_pair_0)) (and (= expr_23_length_pair_0 b1_7_length_pair_2) (and (= b2_14_length_pair_2 expr_20_length_pair_1) (and (= expr_20_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_19_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_19_length_pair_0) (- (|uint_array_tuple_accessor_length| expr_17_length_pair_0) expr_18_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_17_length_pair_0) (|uint_array_tuple_accessor_array| expr_19_length_pair_0) expr_18_0 (|uint_array_tuple_accessor_length| expr_17_length_pair_0)) (and (=> true true) (and (= expr_18_0 0) (and (= expr_17_length_pair_0 data_3_length_pair_1) (and (= b1_7_length_pair_2 expr_11_length_pair_1) (and (= expr_11_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_t_bytes_memory_ptr| abi_0) expr_10_length_pair_0)) (and (= expr_10_length_pair_0 data_3_length_pair_1) (and (>= (|uint_array_tuple_accessor_length| data_3_length_pair_1) 0) (and (= b5_75_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= y_71_1 0) (and (= x_67_1 0) (and (= b4_49_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b3_31_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b2_14_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b1_7_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) true)))))))))))))))))))))))))))) (and (not expr_27_1) (= error_1 1))) (block_8_function_abiEncodeSlice__93_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (block_8_function_abiEncodeSlice__93_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (summary_3_function_abiEncodeSlice__93_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1)))) | |
| (declare-fun |block_9_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (and (and (block_6_abiEncodeSlice_92_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (and (= expr_45_1 (= expr_42_1 expr_44_1)) (and (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_44_1 (|bytes_tuple_accessor_length| expr_43_length_pair_0)) (and (= expr_43_length_pair_0 b3_31_length_pair_2) (and (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_42_1 (|bytes_tuple_accessor_length| expr_41_length_pair_0)) (and (= expr_41_length_pair_0 b1_7_length_pair_2) (and (= b3_31_length_pair_2 expr_38_length_pair_1) (and (= expr_38_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_37_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_37_length_pair_0) (- expr_36_1 0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_34_length_pair_0) (|uint_array_tuple_accessor_array| expr_37_length_pair_0) 0 expr_36_1) (and (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_1 (|uint_array_tuple_accessor_length| expr_35_length_pair_0)) (and (= expr_35_length_pair_0 data_3_length_pair_1) (and (= expr_34_length_pair_0 data_3_length_pair_1) (and (= error_1 error_0) (and (= expr_27_1 (= expr_24_1 expr_26_1)) (and (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (|bytes_tuple_accessor_length| expr_25_length_pair_0)) (and (= expr_25_length_pair_0 b2_14_length_pair_2) (and (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_24_1 (|bytes_tuple_accessor_length| expr_23_length_pair_0)) (and (= expr_23_length_pair_0 b1_7_length_pair_2) (and (= b2_14_length_pair_2 expr_20_length_pair_1) (and (= expr_20_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_19_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_19_length_pair_0) (- (|uint_array_tuple_accessor_length| expr_17_length_pair_0) expr_18_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_17_length_pair_0) (|uint_array_tuple_accessor_array| expr_19_length_pair_0) expr_18_0 (|uint_array_tuple_accessor_length| expr_17_length_pair_0)) (and (=> true true) (and (= expr_18_0 0) (and (= expr_17_length_pair_0 data_3_length_pair_1) (and (= b1_7_length_pair_2 expr_11_length_pair_1) (and (= expr_11_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_t_bytes_memory_ptr| abi_0) expr_10_length_pair_0)) (and (= expr_10_length_pair_0 data_3_length_pair_1) (and (>= (|uint_array_tuple_accessor_length| data_3_length_pair_1) 0) (and (= b5_75_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= y_71_1 0) (and (= x_67_1 0) (and (= b4_49_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b3_31_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b2_14_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b1_7_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) true))))))))))))))))))))))))))))))))))))))))))))))) (and (not expr_45_1) (= error_2 2))) (block_9_function_abiEncodeSlice__93_94_0 error_2 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_2 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (block_9_function_abiEncodeSlice__93_94_0 error_2 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_2 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (summary_3_function_abiEncodeSlice__93_94_0 error_2 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1)))) | |
| (declare-fun |block_10_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (and (and (block_6_abiEncodeSlice_92_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (and (= expr_63_1 (= expr_60_1 expr_62_1)) (and (and (>= expr_62_1 0) (<= expr_62_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_62_1 0) (<= expr_62_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_62_1 (|bytes_tuple_accessor_length| expr_61_length_pair_0)) (and (= expr_61_length_pair_0 b4_49_length_pair_2) (and (and (>= expr_60_1 0) (<= expr_60_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_60_1 0) (<= expr_60_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_60_1 (|bytes_tuple_accessor_length| expr_59_length_pair_0)) (and (= expr_59_length_pair_0 b1_7_length_pair_2) (and (= b4_49_length_pair_2 expr_56_length_pair_1) (and (= expr_56_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_55_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_55_length_pair_0) (- expr_54_0 expr_53_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_52_length_pair_0) (|uint_array_tuple_accessor_array| expr_55_length_pair_0) expr_53_0 expr_54_0) (and (=> true true) (and (= expr_54_0 10) (and (=> true true) (and (= expr_53_0 5) (and (= expr_52_length_pair_0 data_3_length_pair_1) (and (= error_2 error_1) (and (= expr_45_1 (= expr_42_1 expr_44_1)) (and (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_44_1 (|bytes_tuple_accessor_length| expr_43_length_pair_0)) (and (= expr_43_length_pair_0 b3_31_length_pair_2) (and (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_42_1 (|bytes_tuple_accessor_length| expr_41_length_pair_0)) (and (= expr_41_length_pair_0 b1_7_length_pair_2) (and (= b3_31_length_pair_2 expr_38_length_pair_1) (and (= expr_38_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_37_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_37_length_pair_0) (- expr_36_1 0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_34_length_pair_0) (|uint_array_tuple_accessor_array| expr_37_length_pair_0) 0 expr_36_1) (and (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_1 (|uint_array_tuple_accessor_length| expr_35_length_pair_0)) (and (= expr_35_length_pair_0 data_3_length_pair_1) (and (= expr_34_length_pair_0 data_3_length_pair_1) (and (= error_1 error_0) (and (= expr_27_1 (= expr_24_1 expr_26_1)) (and (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (|bytes_tuple_accessor_length| expr_25_length_pair_0)) (and (= expr_25_length_pair_0 b2_14_length_pair_2) (and (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_24_1 (|bytes_tuple_accessor_length| expr_23_length_pair_0)) (and (= expr_23_length_pair_0 b1_7_length_pair_2) (and (= b2_14_length_pair_2 expr_20_length_pair_1) (and (= expr_20_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_19_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_19_length_pair_0) (- (|uint_array_tuple_accessor_length| expr_17_length_pair_0) expr_18_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_17_length_pair_0) (|uint_array_tuple_accessor_array| expr_19_length_pair_0) expr_18_0 (|uint_array_tuple_accessor_length| expr_17_length_pair_0)) (and (=> true true) (and (= expr_18_0 0) (and (= expr_17_length_pair_0 data_3_length_pair_1) (and (= b1_7_length_pair_2 expr_11_length_pair_1) (and (= expr_11_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_t_bytes_memory_ptr| abi_0) expr_10_length_pair_0)) (and (= expr_10_length_pair_0 data_3_length_pair_1) (and (>= (|uint_array_tuple_accessor_length| data_3_length_pair_1) 0) (and (= b5_75_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= y_71_1 0) (and (= x_67_1 0) (and (= b4_49_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b3_31_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b2_14_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b1_7_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (and (not expr_63_1) (= error_3 3))) (block_10_function_abiEncodeSlice__93_94_0 error_3 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_2 b4_49_length_pair_2 x_67_1 y_71_1 b5_75_length_pair_1)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (y_71_0 Int) (y_71_1 Int)) | |
| (=> (block_10_function_abiEncodeSlice__93_94_0 error_3 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_2 b4_49_length_pair_2 x_67_1 y_71_1 b5_75_length_pair_1) (summary_3_function_abiEncodeSlice__93_94_0 error_3 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1)))) | |
| (declare-fun |block_11_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (block_6_abiEncodeSlice_92_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (and (= expr_89_1 (= expr_86_1 expr_88_1)) (and (and (>= expr_88_1 0) (<= expr_88_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_88_1 0) (<= expr_88_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_88_1 (|bytes_tuple_accessor_length| expr_87_length_pair_0)) (and (= expr_87_length_pair_0 b5_75_length_pair_2) (and (and (>= expr_86_1 0) (<= expr_86_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_86_1 0) (<= expr_86_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_86_1 (|bytes_tuple_accessor_length| expr_85_length_pair_0)) (and (= expr_85_length_pair_0 b1_7_length_pair_2) (and (= b5_75_length_pair_2 expr_82_length_pair_1) (and (= expr_82_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_81_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_81_length_pair_0) (- expr_80_0 expr_79_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_78_length_pair_0) (|uint_array_tuple_accessor_array| expr_81_length_pair_0) expr_79_0 expr_80_0) (and (=> true (and (>= expr_80_0 0) (<= expr_80_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_80_0 y_71_2) (and (=> true (and (>= expr_79_0 0) (<= expr_79_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_79_0 x_67_2) (and (= expr_78_length_pair_0 data_3_length_pair_1) (and (= y_71_2 expr_72_0) (and (=> true true) (and (= expr_72_0 10) (and (= x_67_2 expr_68_0) (and (=> true true) (and (= expr_68_0 5) (and (= error_3 error_2) (and (= expr_63_1 (= expr_60_1 expr_62_1)) (and (and (>= expr_62_1 0) (<= expr_62_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_62_1 0) (<= expr_62_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_62_1 (|bytes_tuple_accessor_length| expr_61_length_pair_0)) (and (= expr_61_length_pair_0 b4_49_length_pair_2) (and (and (>= expr_60_1 0) (<= expr_60_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_60_1 0) (<= expr_60_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_60_1 (|bytes_tuple_accessor_length| expr_59_length_pair_0)) (and (= expr_59_length_pair_0 b1_7_length_pair_2) (and (= b4_49_length_pair_2 expr_56_length_pair_1) (and (= expr_56_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_55_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_55_length_pair_0) (- expr_54_0 expr_53_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_52_length_pair_0) (|uint_array_tuple_accessor_array| expr_55_length_pair_0) expr_53_0 expr_54_0) (and (=> true true) (and (= expr_54_0 10) (and (=> true true) (and (= expr_53_0 5) (and (= expr_52_length_pair_0 data_3_length_pair_1) (and (= error_2 error_1) (and (= expr_45_1 (= expr_42_1 expr_44_1)) (and (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_44_1 (|bytes_tuple_accessor_length| expr_43_length_pair_0)) (and (= expr_43_length_pair_0 b3_31_length_pair_2) (and (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_42_1 (|bytes_tuple_accessor_length| expr_41_length_pair_0)) (and (= expr_41_length_pair_0 b1_7_length_pair_2) (and (= b3_31_length_pair_2 expr_38_length_pair_1) (and (= expr_38_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_37_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_37_length_pair_0) (- expr_36_1 0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_34_length_pair_0) (|uint_array_tuple_accessor_array| expr_37_length_pair_0) 0 expr_36_1) (and (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_1 (|uint_array_tuple_accessor_length| expr_35_length_pair_0)) (and (= expr_35_length_pair_0 data_3_length_pair_1) (and (= expr_34_length_pair_0 data_3_length_pair_1) (and (= error_1 error_0) (and (= expr_27_1 (= expr_24_1 expr_26_1)) (and (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (|bytes_tuple_accessor_length| expr_25_length_pair_0)) (and (= expr_25_length_pair_0 b2_14_length_pair_2) (and (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_24_1 (|bytes_tuple_accessor_length| expr_23_length_pair_0)) (and (= expr_23_length_pair_0 b1_7_length_pair_2) (and (= b2_14_length_pair_2 expr_20_length_pair_1) (and (= expr_20_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_19_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_19_length_pair_0) (- (|uint_array_tuple_accessor_length| expr_17_length_pair_0) expr_18_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_17_length_pair_0) (|uint_array_tuple_accessor_array| expr_19_length_pair_0) expr_18_0 (|uint_array_tuple_accessor_length| expr_17_length_pair_0)) (and (=> true true) (and (= expr_18_0 0) (and (= expr_17_length_pair_0 data_3_length_pair_1) (and (= b1_7_length_pair_2 expr_11_length_pair_1) (and (= expr_11_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_t_bytes_memory_ptr| abi_0) expr_10_length_pair_0)) (and (= expr_10_length_pair_0 data_3_length_pair_1) (and (>= (|uint_array_tuple_accessor_length| data_3_length_pair_1) 0) (and (= b5_75_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= y_71_1 0) (and (= x_67_1 0) (and (= b4_49_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b3_31_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b2_14_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b1_7_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) true))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (and (not expr_89_1) (= error_4 4))) (block_11_function_abiEncodeSlice__93_94_0 error_4 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_2 b4_49_length_pair_2 x_67_2 y_71_2 b5_75_length_pair_2)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (block_11_function_abiEncodeSlice__93_94_0 error_4 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_2 b4_49_length_pair_2 x_67_2 y_71_2 b5_75_length_pair_2) (summary_3_function_abiEncodeSlice__93_94_0 error_4 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (block_6_abiEncodeSlice_92_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (and (= error_4 error_3) (and (= expr_89_1 (= expr_86_1 expr_88_1)) (and (and (>= expr_88_1 0) (<= expr_88_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_88_1 0) (<= expr_88_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_88_1 (|bytes_tuple_accessor_length| expr_87_length_pair_0)) (and (= expr_87_length_pair_0 b5_75_length_pair_2) (and (and (>= expr_86_1 0) (<= expr_86_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_86_1 0) (<= expr_86_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_86_1 (|bytes_tuple_accessor_length| expr_85_length_pair_0)) (and (= expr_85_length_pair_0 b1_7_length_pair_2) (and (= b5_75_length_pair_2 expr_82_length_pair_1) (and (= expr_82_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_81_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_81_length_pair_0) (- expr_80_0 expr_79_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_78_length_pair_0) (|uint_array_tuple_accessor_array| expr_81_length_pair_0) expr_79_0 expr_80_0) (and (=> true (and (>= expr_80_0 0) (<= expr_80_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_80_0 y_71_2) (and (=> true (and (>= expr_79_0 0) (<= expr_79_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_79_0 x_67_2) (and (= expr_78_length_pair_0 data_3_length_pair_1) (and (= y_71_2 expr_72_0) (and (=> true true) (and (= expr_72_0 10) (and (= x_67_2 expr_68_0) (and (=> true true) (and (= expr_68_0 5) (and (= error_3 error_2) (and (= expr_63_1 (= expr_60_1 expr_62_1)) (and (and (>= expr_62_1 0) (<= expr_62_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_62_1 0) (<= expr_62_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_62_1 (|bytes_tuple_accessor_length| expr_61_length_pair_0)) (and (= expr_61_length_pair_0 b4_49_length_pair_2) (and (and (>= expr_60_1 0) (<= expr_60_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_60_1 0) (<= expr_60_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_60_1 (|bytes_tuple_accessor_length| expr_59_length_pair_0)) (and (= expr_59_length_pair_0 b1_7_length_pair_2) (and (= b4_49_length_pair_2 expr_56_length_pair_1) (and (= expr_56_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_55_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_55_length_pair_0) (- expr_54_0 expr_53_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_52_length_pair_0) (|uint_array_tuple_accessor_array| expr_55_length_pair_0) expr_53_0 expr_54_0) (and (=> true true) (and (= expr_54_0 10) (and (=> true true) (and (= expr_53_0 5) (and (= expr_52_length_pair_0 data_3_length_pair_1) (and (= error_2 error_1) (and (= expr_45_1 (= expr_42_1 expr_44_1)) (and (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_44_1 0) (<= expr_44_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_44_1 (|bytes_tuple_accessor_length| expr_43_length_pair_0)) (and (= expr_43_length_pair_0 b3_31_length_pair_2) (and (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_42_1 0) (<= expr_42_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_42_1 (|bytes_tuple_accessor_length| expr_41_length_pair_0)) (and (= expr_41_length_pair_0 b1_7_length_pair_2) (and (= b3_31_length_pair_2 expr_38_length_pair_1) (and (= expr_38_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_37_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_37_length_pair_0) (- expr_36_1 0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_34_length_pair_0) (|uint_array_tuple_accessor_array| expr_37_length_pair_0) 0 expr_36_1) (and (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_36_1 0) (<= expr_36_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_1 (|uint_array_tuple_accessor_length| expr_35_length_pair_0)) (and (= expr_35_length_pair_0 data_3_length_pair_1) (and (= expr_34_length_pair_0 data_3_length_pair_1) (and (= error_1 error_0) (and (= expr_27_1 (= expr_24_1 expr_26_1)) (and (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_26_1 0) (<= expr_26_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_26_1 (|bytes_tuple_accessor_length| expr_25_length_pair_0)) (and (= expr_25_length_pair_0 b2_14_length_pair_2) (and (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_24_1 0) (<= expr_24_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_24_1 (|bytes_tuple_accessor_length| expr_23_length_pair_0)) (and (= expr_23_length_pair_0 b1_7_length_pair_2) (and (= b2_14_length_pair_2 expr_20_length_pair_1) (and (= expr_20_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_slice_t_bytes_memory_ptr| abi_0) expr_19_length_pair_0)) (and (= (|uint_array_tuple_accessor_length| expr_19_length_pair_0) (- (|uint_array_tuple_accessor_length| expr_17_length_pair_0) expr_18_0)) (and (array_slice_uint_array_tuple_0 (|uint_array_tuple_accessor_array| expr_17_length_pair_0) (|uint_array_tuple_accessor_array| expr_19_length_pair_0) expr_18_0 (|uint_array_tuple_accessor_length| expr_17_length_pair_0)) (and (=> true true) (and (= expr_18_0 0) (and (= expr_17_length_pair_0 data_3_length_pair_1) (and (= b1_7_length_pair_2 expr_11_length_pair_1) (and (= expr_11_length_pair_1 (select (|t_function_abiencode_pure()returns(t_bytes_memory_ptr)_t_array(t_uint256)dyn_calldata_ptr_t_bytes_memory_ptr| abi_0) expr_10_length_pair_0)) (and (= expr_10_length_pair_0 data_3_length_pair_1) (and (>= (|uint_array_tuple_accessor_length| data_3_length_pair_1) 0) (and (= b5_75_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= y_71_1 0) (and (= x_67_1 0) (and (= b4_49_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b3_31_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b2_14_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) (and (= b1_7_length_pair_1 (|bytes_tuple| ((as const (Array Int Int)) 0) 0)) true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) true) (block_7_return_function_abiEncodeSlice__93_94_0 error_4 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_2 b2_14_length_pair_2 b3_31_length_pair_2 b4_49_length_pair_2 x_67_2 y_71_2 b5_75_length_pair_2)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (block_7_return_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) true) true) (summary_3_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1)))) | |
| (declare-fun |block_12_function_abiEncodeSlice__93_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |uint_array_tuple| |state_type| |uint_array_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| |bytes_tuple| Int Int |bytes_tuple| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (block_12_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (block_12_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1 b1_7_length_pair_1 b2_14_length_pair_1 b3_31_length_pair_1 b4_49_length_pair_1 x_67_1 y_71_1 b5_75_length_pair_1) (and (summary_3_function_abiEncodeSlice__93_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 data_3_length_pair_1 state_3 data_3_length_pair_2) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_5_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_5_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_5_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_5_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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) 3461905247)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 206)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 123)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 95)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= data_3_length_pair_1 data_3_length_pair_0))) true))))))) true) (summary_4_function_abiEncodeSlice__93_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_3 data_3_length_pair_2)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (interface_0_C_94_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1) (= error_0 0))) (interface_0_C_94_0 this_0 abi_0 crypto_0 state_1)))) | |
| (declare-fun |contract_initializer_13_C_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (declare-fun |contract_initializer_entry_14_C_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_14_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (declare-fun |contract_initializer_after_init_15_C_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (contract_initializer_entry_14_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_15_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (contract_initializer_after_init_15_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_13_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (declare-fun |implicit_constructor_entry_16_C_94_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_16_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (implicit_constructor_entry_16_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_13_C_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (implicit_constructor_entry_16_C_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_13_C_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_94_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (summary_constructor_2_C_94_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 (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (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_94_0 this_0 abi_0 crypto_0 state_1)))) | |
| (declare-fun |error_target_6_0| () Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (interface_0_C_94_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1) (= error_0 1))) error_target_6_0))) | |
| (declare-fun |error_target_7_0| () Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (interface_0_C_94_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1) (= error_0 2))) error_target_7_0))) | |
| (declare-fun |error_target_8_0| () Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (interface_0_C_94_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1) (= error_0 3))) error_target_8_0))) | |
| (declare-fun |error_target_9_0| () Bool) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> (and (and (interface_0_C_94_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_abiEncodeSlice__93_94_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 data_3_length_pair_0 state_1 data_3_length_pair_1) (= error_0 4))) error_target_9_0))) | |
| (assert | |
| (forall ( (a_uint_array_tuple_array_length_pair_0 |array_length_pair|) (abi_0 |abi_type|) (b1_7_length_pair_0 |bytes_tuple|) (b1_7_length_pair_1 |bytes_tuple|) (b1_7_length_pair_2 |bytes_tuple|) (b2_14_length_pair_0 |bytes_tuple|) (b2_14_length_pair_1 |bytes_tuple|) (b2_14_length_pair_2 |bytes_tuple|) (b3_31_length_pair_0 |bytes_tuple|) (b3_31_length_pair_1 |bytes_tuple|) (b3_31_length_pair_2 |bytes_tuple|) (b4_49_length_pair_0 |bytes_tuple|) (b4_49_length_pair_1 |bytes_tuple|) (b4_49_length_pair_2 |bytes_tuple|) (b5_75_length_pair_0 |bytes_tuple|) (b5_75_length_pair_1 |bytes_tuple|) (b5_75_length_pair_2 |bytes_tuple|) (b_uint_array_tuple_array_length_pair_0 |array_length_pair|) (crypto_0 |crypto_type|) (data_3_length_pair_0 |uint_array_tuple|) (data_3_length_pair_1 |uint_array_tuple|) (data_3_length_pair_2 |uint_array_tuple|) (end_uint_array_tuple_0 Int) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (error_4 Int) (expr_10_length_pair_0 |uint_array_tuple|) (expr_11_length_pair_0 |bytes_tuple|) (expr_11_length_pair_1 |bytes_tuple|) (expr_17_length_pair_0 |uint_array_tuple|) (expr_18_0 Int) (expr_19_length_pair_0 |uint_array_tuple|) (expr_20_length_pair_0 |bytes_tuple|) (expr_20_length_pair_1 |bytes_tuple|) (expr_23_length_pair_0 |bytes_tuple|) (expr_24_1 Int) (expr_25_length_pair_0 |bytes_tuple|) (expr_26_1 Int) (expr_27_1 Bool) (expr_34_length_pair_0 |uint_array_tuple|) (expr_35_length_pair_0 |uint_array_tuple|) (expr_36_1 Int) (expr_37_length_pair_0 |uint_array_tuple|) (expr_38_length_pair_0 |bytes_tuple|) (expr_38_length_pair_1 |bytes_tuple|) (expr_41_length_pair_0 |bytes_tuple|) (expr_42_1 Int) (expr_43_length_pair_0 |bytes_tuple|) (expr_44_1 Int) (expr_45_1 Bool) (expr_52_length_pair_0 |uint_array_tuple|) (expr_53_0 Int) (expr_54_0 Int) (expr_55_length_pair_0 |uint_array_tuple|) (expr_56_length_pair_0 |bytes_tuple|) (expr_56_length_pair_1 |bytes_tuple|) (expr_59_length_pair_0 |bytes_tuple|) (expr_60_1 Int) (expr_61_length_pair_0 |bytes_tuple|) (expr_62_1 Int) (expr_63_1 Bool) (expr_68_0 Int) (expr_72_0 Int) (expr_78_length_pair_0 |uint_array_tuple|) (expr_79_0 Int) (expr_80_0 Int) (expr_81_length_pair_0 |uint_array_tuple|) (expr_82_length_pair_0 |bytes_tuple|) (expr_82_length_pair_1 |bytes_tuple|) (expr_85_length_pair_0 |bytes_tuple|) (expr_86_1 Int) (expr_87_length_pair_0 |bytes_tuple|) (expr_88_1 Int) (expr_89_1 Bool) (funds_5_0 Int) (i_uint_array_tuple_0 Int) (start_uint_array_tuple_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_67_0 Int) (x_67_1 Int) (x_67_2 Int) (y_71_0 Int) (y_71_1 Int) (y_71_2 Int)) | |
| (=> error_target_9_0 false))) | |
| (check-sat) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment