out1.smt2

(set-logic HORN)

(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(declare-datatypes ((|struct MultiSig.Tx| 0)) (((|struct MultiSig.Tx| (|struct MultiSig.Tx_accessor_id| Int) (|struct MultiSig.Tx_accessor_to| Int) (|struct MultiSig.Tx_accessor_amount| Int) (|struct MultiSig.Tx_accessor_approved| Int)))))
(declare-datatypes ((|struct MultiSig.Tx_array_tuple| 0)) (((|struct MultiSig.Tx_array_tuple| (|struct MultiSig.Tx_array_tuple_accessor_array| (Array Int |struct MultiSig.Tx|)) (|struct MultiSig.Tx_array_tuple_accessor_length| Int)))))
(declare-datatypes ((|mapping(address => bool)_tuple| 0)) (((|mapping(address => bool)_tuple| (|mapping(address => bool)_tuple_accessor_array| (Array Int Bool)) (|mapping(address => bool)_tuple_accessor_length| Int)))))
(declare-datatypes ((|mapping(uint256 => bool)_tuple| 0)) (((|mapping(uint256 => bool)_tuple| (|mapping(uint256 => bool)_tuple_accessor_array| (Array Int Bool)) (|mapping(uint256 => bool)_tuple_accessor_length| Int)))))
(declare-datatypes ((|mapping(address => mapping(uint256 => bool))_tuple| 0)) (((|mapping(address => mapping(uint256 => bool))_tuple| (|mapping(address => mapping(uint256 => bool))_tuple_accessor_array| (Array Int |mapping(uint256 => bool)_tuple|)) (|mapping(address => mapping(uint256 => bool))_tuple_accessor_length| Int)))))
(declare-datatypes ((|address_array_tuple| 0)) (((|address_array_tuple| (|address_array_tuple_accessor_array| (Array Int Int)) (|address_array_tuple_accessor_length| Int)))))
(declare-fun |interface_0_MultiSig_162_0| (Int |abi_type| |crypto_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| ) Bool)
(declare-fun |nondet_interface_1_MultiSig_162_0| (Int Int |abi_type| |crypto_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| ) Bool)
(declare-fun |summary_constructor_2_MultiSig_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| ) Bool)
(assert
(forall ( (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (nOwners_15_0 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|))
(=> (= error_0 0) (nondet_interface_1_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0))))


(declare-fun |summary_3_constructor_67_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| ) Bool)
(declare-fun |summary_4_function_add__94_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (nondet_interface_1_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1) true) (and (= error_0 0) (summary_4_function_add__94_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_0 _amt_71_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _to_69_1 _amt_71_1))) (nondet_interface_1_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2))))


(declare-fun |summary_5_function_approve__139_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (nondet_interface_1_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1) true) (and (= error_1 0) (summary_5_function_approve__139_162_0 error_2 this_0 abi_0 crypto_0 tx_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _id_96_1))) (nondet_interface_1_MultiSig_162_0 error_2 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2))))


(declare-fun |summary_6_function_inv__161_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (nondet_interface_1_MultiSig_162_0 error_2 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1) true) (and (= error_2 0) (summary_6_function_inv__161_162_0 error_3 this_0 abi_0 crypto_0 tx_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _id_141_1))) (nondet_interface_1_MultiSig_162_0 error_3 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2))))


(declare-fun |block_7_function_add__94_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int ) Bool)
(declare-fun |block_8_add_93_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(block_7_function_add__94_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1)))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_7_function_add__94_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and (and true (= txs_13_length_pair_1 txs_13_length_pair_0)) (= nOwners_15_1 nOwners_15_0)) (= owner_19_length_pair_1 owner_19_length_pair_0)) (= approved_25_length_pair_1 approved_25_length_pair_0))) (and (and true (= _to_69_1 _to_69_0)) (= _amt_71_1 _amt_71_0))) true)) true) (block_8_add_93_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1))))


(declare-fun |block_9_return_function_add__94_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_8_add_93_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1) (and (= txs_13_length_pair_2 expr_81_length_pair_1) (and (= (|struct MultiSig.Tx_array_tuple_accessor_length| expr_81_length_pair_1) (+ (|struct MultiSig.Tx_array_tuple_accessor_length| expr_81_length_pair_0) 1)) (and (= (|struct MultiSig.Tx_array_tuple_accessor_array| expr_81_length_pair_1) (store (|struct MultiSig.Tx_array_tuple_accessor_array| expr_81_length_pair_0) (|struct MultiSig.Tx_array_tuple_accessor_length| expr_81_length_pair_0) expr_90_1)) (and (< (+ (|struct MultiSig.Tx_array_tuple_accessor_length| expr_81_length_pair_0) 1) (- 115792089237316195423570985008687907853269984665640564039457584007913129639935 1)) (and (>= (|struct MultiSig.Tx_array_tuple_accessor_length| expr_81_length_pair_0) 0) (and (= expr_89_0 (|struct MultiSig.Tx_accessor_approved| expr_90_1)) (and (= expr_88_0 (|struct MultiSig.Tx_accessor_amount| expr_90_1)) (and (= expr_87_0 (|struct MultiSig.Tx_accessor_to| expr_90_1)) (and (= expr_86_1 (|struct MultiSig.Tx_accessor_id| expr_90_1)) (and (=> true true) (and (= expr_89_0 0) (and (=> true (and (>= expr_88_0 0) (<= expr_88_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_88_0 _amt_71_1) (and (=> true (and (>= expr_87_0 0) (<= expr_87_0 1461501637330902918203684832716283019655932542975))) (and (= expr_87_0 _to_69_1) (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 (|struct MultiSig.Tx_array_tuple_accessor_length| expr_85_length_pair_0)) (and (= expr_85_length_pair_0 txs_13_length_pair_1) (and (= expr_81_length_pair_0 txs_13_length_pair_1) (and (=> true expr_78_1) (and true (and (= expr_78_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_19_length_pair_1) expr_77_1)) (and (=> true (and (>= expr_77_1 0) (<= expr_77_1 1461501637330902918203684832716283019655932542975))) (and (= expr_77_1 (|msg.sender| tx_0)) (and (= expr_75_length_pair_0 owner_19_length_pair_1) (and (and (>= _amt_71_1 0) (<= _amt_71_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= _to_69_1 0) (<= _to_69_1 1461501637330902918203684832716283019655932542975)) true))))))))))))))))))))))))))))) true) (block_9_return_function_add__94_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_2 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_9_return_function_add__94_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1) true) true) (summary_4_function_add__94_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 4124584811)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 245)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 216)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 43)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 107)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_4_function_add__94_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _to_69_0 _amt_71_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _to_69_1 _amt_71_1)) (= error_0 0))) (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1))))


(declare-fun |block_10_function_approve__139_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(declare-fun |block_11_approve_138_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(block_10_function_approve__139_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_1)))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_10_function_approve__139_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and (and true (= txs_13_length_pair_1 txs_13_length_pair_0)) (= nOwners_15_1 nOwners_15_0)) (= owner_19_length_pair_1 owner_19_length_pair_0)) (= approved_25_length_pair_1 approved_25_length_pair_0))) (and true (= _id_96_1 _id_96_0))) true)) true) (block_11_approve_138_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_1))))


(declare-fun |block_12_return_function_approve__139_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_11_approve_138_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_1) (and (= expr_132_length_pair_2 txs_13_length_pair_2) (and (= txs_13_length_pair_2 (|struct MultiSig.Tx_array_tuple| (store (|struct MultiSig.Tx_array_tuple_accessor_array| expr_132_length_pair_1) expr_133_0 expr_134_2) (|struct MultiSig.Tx_array_tuple_accessor_length| expr_132_length_pair_1))) (and (= expr_134_3 (select (|struct MultiSig.Tx_array_tuple_accessor_array| expr_132_length_pair_1) expr_133_0)) (and (= expr_132_length_pair_1 txs_13_length_pair_1) (and (=> true (and (>= expr_135_2 0) (<= expr_135_2 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_135_2 (|struct MultiSig.Tx_accessor_approved| expr_134_2)) (and (= (|struct MultiSig.Tx_accessor_approved| expr_134_2) (+ expr_135_1 1)) (and (= (|struct MultiSig.Tx_accessor_amount| expr_134_2) (|struct MultiSig.Tx_accessor_amount| expr_134_1)) (and (= (|struct MultiSig.Tx_accessor_to| expr_134_2) (|struct MultiSig.Tx_accessor_to| expr_134_1)) (and (= (|struct MultiSig.Tx_accessor_id| expr_134_2) (|struct MultiSig.Tx_accessor_id| expr_134_1)) (and (=> true (and (>= expr_136_1 0) (<= expr_136_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_136_1 (+ expr_135_1 1)) (and (=> true (and (>= expr_135_1 0) (<= expr_135_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_135_1 (|struct MultiSig.Tx_accessor_approved| expr_134_1)) (and true (and (= expr_134_1 (select (|struct MultiSig.Tx_array_tuple_accessor_array| txs_13_length_pair_1) expr_133_0)) (and (=> true (and (>= expr_133_0 0) (<= expr_133_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_133_0 _id_96_1) (and (= expr_132_length_pair_0 txs_13_length_pair_1) (and (= expr_123_length_pair_2 approved_25_length_pair_2) (and (= approved_25_length_pair_2 (|mapping(address => mapping(uint256 => bool))_tuple| (store (|mapping(address => mapping(uint256 => bool))_tuple_accessor_array| expr_123_length_pair_1) expr_125_1 (|mapping(uint256 => bool)_tuple| (store (|mapping(uint256 => bool)_tuple_accessor_array| expr_127_length_pair_1) expr_126_0 expr_130_1) (|mapping(uint256 => bool)_tuple_accessor_length| expr_127_length_pair_1))) (|mapping(address => mapping(uint256 => bool))_tuple_accessor_length| expr_123_length_pair_1))) (and (= expr_127_length_pair_2 (select (|mapping(address => mapping(uint256 => bool))_tuple_accessor_array| expr_123_length_pair_1) expr_125_1)) (and (= expr_123_length_pair_1 approved_25_length_pair_1) (and (= expr_128_2 (select (|mapping(uint256 => bool)_tuple_accessor_array| expr_127_length_pair_1) expr_126_0)) (and (= expr_130_1 expr_129_0) (and true (and (= expr_128_1 (select (|mapping(uint256 => bool)_tuple_accessor_array| expr_127_length_pair_1) expr_126_0)) (and (=> true (and (>= expr_126_0 0) (<= expr_126_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_126_0 _id_96_1) (and (>= (|mapping(uint256 => bool)_tuple_accessor_length| expr_127_length_pair_1) 0) (and (= expr_127_length_pair_1 (select (|mapping(address => mapping(uint256 => bool))_tuple_accessor_array| approved_25_length_pair_1) expr_125_1)) (and (=> true (and (>= expr_125_1 0) (<= expr_125_1 1461501637330902918203684832716283019655932542975))) (and (= expr_125_1 (|msg.sender| tx_0)) (and (= expr_123_length_pair_0 approved_25_length_pair_1) (and (= expr_129_0 true) (and (=> true expr_120_1) (and (= expr_120_1 (< expr_117_0 expr_119_1)) (and (and (>= expr_119_1 0) (<= expr_119_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_119_1 0) (<= expr_119_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_119_1 (|struct MultiSig.Tx_array_tuple_accessor_length| expr_118_length_pair_0)) (and (= expr_118_length_pair_0 txs_13_length_pair_1) (and (=> true (and (>= expr_117_0 0) (<= expr_117_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_117_0 _id_96_1) (and (=> true expr_113_1) (and (= expr_113_1 (not expr_112_1)) (and true (and (= expr_112_1 (select (|mapping(uint256 => bool)_tuple_accessor_array| expr_110_length_pair_1) expr_111_0)) (and (=> true (and (>= expr_111_0 0) (<= expr_111_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_111_0 _id_96_1) (and (>= (|mapping(uint256 => bool)_tuple_accessor_length| expr_110_length_pair_1) 0) (and (= expr_110_length_pair_1 (select (|mapping(address => mapping(uint256 => bool))_tuple_accessor_array| approved_25_length_pair_1) expr_109_1)) (and (=> true (and (>= expr_109_1 0) (<= expr_109_1 1461501637330902918203684832716283019655932542975))) (and (= expr_109_1 (|msg.sender| tx_0)) (and (= expr_107_length_pair_0 approved_25_length_pair_1) (and (=> true expr_103_1) (and true (and (= expr_103_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_19_length_pair_1) expr_102_1)) (and (=> true (and (>= expr_102_1 0) (<= expr_102_1 1461501637330902918203684832716283019655932542975))) (and (= expr_102_1 (|msg.sender| tx_0)) (and (= expr_100_length_pair_0 owner_19_length_pair_1) (and (and (>= _id_96_1 0) (<= _id_96_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) true) (block_12_return_function_approve__139_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_2 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_2 _id_96_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_12_return_function_approve__139_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_1) true) true) (summary_5_function_approve__139_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3076127060)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 183)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 89)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 249)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 84)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_5_function_approve__139_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_96_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_96_1)) (= error_0 0))) (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1))))


(declare-fun |block_13_function_inv__161_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(declare-fun |block_14_inv_160_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(block_13_function_inv__161_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1)))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_13_function_inv__161_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and (and true (= txs_13_length_pair_1 txs_13_length_pair_0)) (= nOwners_15_1 nOwners_15_0)) (= owner_19_length_pair_1 owner_19_length_pair_0)) (= approved_25_length_pair_1 approved_25_length_pair_0))) (and true (= _id_141_1 _id_141_0))) true)) true) (block_14_inv_160_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1))))


(declare-fun |block_15_return_function_inv__161_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(declare-fun |block_16_function_inv__161_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_14_inv_160_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1) (and (= expr_157_1 (<= expr_155_1 expr_156_0)) (and (=> true (and (>= expr_156_0 0) (<= expr_156_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_156_0 nOwners_15_1) (and (=> true (and (>= expr_155_1 0) (<= expr_155_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_155_1 (|struct MultiSig.Tx_accessor_approved| expr_154_1)) (and true (and (= expr_154_1 (select (|struct MultiSig.Tx_array_tuple_accessor_array| txs_13_length_pair_1) expr_153_0)) (and (=> true (and (>= expr_153_0 0) (<= expr_153_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_153_0 _id_141_1) (and (= expr_152_length_pair_0 txs_13_length_pair_1) (and (=> true expr_148_1) (and (= expr_148_1 (< expr_145_0 expr_147_1)) (and (and (>= expr_147_1 0) (<= expr_147_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_147_1 0) (<= expr_147_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_147_1 (|struct MultiSig.Tx_array_tuple_accessor_length| expr_146_length_pair_0)) (and (= expr_146_length_pair_0 txs_13_length_pair_1) (and (=> true (and (>= expr_145_0 0) (<= expr_145_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_145_0 _id_141_1) (and (and (>= _id_141_1 0) (<= _id_141_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true)))))))))))))))))))) (and (not expr_157_1) (= error_1 1))) (block_16_function_inv__161_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (block_16_function_inv__161_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1) (summary_6_function_inv__161_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_14_inv_160_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1) (and (= error_1 error_0) (and (= expr_157_1 (<= expr_155_1 expr_156_0)) (and (=> true (and (>= expr_156_0 0) (<= expr_156_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_156_0 nOwners_15_1) (and (=> true (and (>= expr_155_1 0) (<= expr_155_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_155_1 (|struct MultiSig.Tx_accessor_approved| expr_154_1)) (and true (and (= expr_154_1 (select (|struct MultiSig.Tx_array_tuple_accessor_array| txs_13_length_pair_1) expr_153_0)) (and (=> true (and (>= expr_153_0 0) (<= expr_153_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_153_0 _id_141_1) (and (= expr_152_length_pair_0 txs_13_length_pair_1) (and (=> true expr_148_1) (and (= expr_148_1 (< expr_145_0 expr_147_1)) (and (and (>= expr_147_1 0) (<= expr_147_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_147_1 0) (<= expr_147_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_147_1 (|struct MultiSig.Tx_array_tuple_accessor_length| expr_146_length_pair_0)) (and (= expr_146_length_pair_0 txs_13_length_pair_1) (and (=> true (and (>= expr_145_0 0) (<= expr_145_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_145_0 _id_141_1) (and (and (>= _id_141_1 0) (<= _id_141_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))))))))))))))))) true) (block_15_return_function_inv__161_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_15_return_function_inv__161_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1) true) true) (summary_6_function_inv__161_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2048143150)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 122)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 20)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 47)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_6_function_inv__161_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1)) (= error_0 0))) (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1))))


(declare-fun |block_17_constructor_67_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| Int ) Bool)
(declare-fun |block_18__66_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(block_17_constructor_67_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1)))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_17_constructor_67_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and (and true (= txs_13_length_pair_1 txs_13_length_pair_0)) (= nOwners_15_1 nOwners_15_0)) (= owner_19_length_pair_1 owner_19_length_pair_0)) (= approved_25_length_pair_1 approved_25_length_pair_0))) (and true (= _owners_28_length_pair_1 _owners_28_length_pair_0))) true)) true) (block_18__66_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1))))


(declare-fun |block_19_return_constructor_67_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| Int ) Bool)
(declare-fun |block_20_for_header__65_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| Int ) Bool)
(declare-fun |block_21_for_body__64_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| Int ) Bool)
(declare-fun |block_22__66_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| Int ) Bool)
(declare-fun |block_23_for_post__46_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| Int ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_18__66_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) (and (= i_37_2 expr_38_0) (and (=> true true) (and (= expr_38_0 0) (and (= nOwners_15_2 expr_34_1) (and (=> true (and (>= expr_34_1 0) (<= expr_34_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_34_1 expr_33_1) (and (=> true (and (>= expr_31_0 0) (<= expr_31_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_31_0 nOwners_15_1) (and (and (>= expr_33_1 0) (<= expr_33_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_33_1 0) (<= expr_33_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_33_1 (|address_array_tuple_accessor_length| expr_32_length_pair_0)) (and (= expr_32_length_pair_0 _owners_28_length_pair_1) (and (>= (|address_array_tuple_accessor_length| _owners_28_length_pair_1) 0) (and (= i_37_1 0) true))))))))))))))) true) (block_20_for_header__65_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_2 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_2))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_20_for_header__65_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) (and (= expr_43_1 (< expr_40_0 expr_42_1)) (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 (|address_array_tuple_accessor_length| expr_41_length_pair_0)) (and (= expr_41_length_pair_0 _owners_28_length_pair_1) (and (=> true (and (>= expr_40_0 0) (<= expr_40_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_40_0 i_37_1) true)))))))) expr_43_1) (block_21_for_body__64_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_20_for_header__65_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) (and (= expr_43_1 (< expr_40_0 expr_42_1)) (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 (|address_array_tuple_accessor_length| expr_41_length_pair_0)) (and (= expr_41_length_pair_0 _owners_28_length_pair_1) (and (=> true (and (>= expr_40_0 0) (<= expr_40_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_40_0 i_37_1) true)))))))) (not expr_43_1)) (block_22__66_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_21_for_body__64_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) (and (= expr_56_length_pair_2 owner_19_length_pair_2) (and (= owner_19_length_pair_2 (|mapping(address => bool)_tuple| (store (|mapping(address => bool)_tuple_accessor_array| expr_56_length_pair_1) expr_59_1 expr_62_1) (|mapping(address => bool)_tuple_accessor_length| expr_56_length_pair_1))) (and (= expr_60_2 (select (|mapping(address => bool)_tuple_accessor_array| expr_56_length_pair_1) expr_59_1)) (and (= expr_56_length_pair_1 owner_19_length_pair_1) (and (= expr_62_1 expr_61_0) (and true (and (= expr_60_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_19_length_pair_1) expr_59_1)) (and (and (>= expr_59_1 0) (<= expr_59_1 1461501637330902918203684832716283019655932542975)) (and (=> true (and (>= expr_59_1 0) (<= expr_59_1 1461501637330902918203684832716283019655932542975))) (and (= expr_59_1 (select (|address_array_tuple_accessor_array| _owners_28_length_pair_1) expr_58_0)) (and (=> true (and (>= expr_58_0 0) (<= expr_58_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_58_0 i_37_1) (and (= expr_57_length_pair_0 _owners_28_length_pair_1) (and (= expr_56_length_pair_0 owner_19_length_pair_1) (and (= expr_61_0 true) (and (=> true expr_53_1) (and (= expr_53_1 (not expr_52_1)) (and true (and (= expr_52_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_19_length_pair_1) expr_51_1)) (and (and (>= expr_51_1 0) (<= expr_51_1 1461501637330902918203684832716283019655932542975)) (and (=> true (and (>= expr_51_1 0) (<= expr_51_1 1461501637330902918203684832716283019655932542975))) (and (= expr_51_1 (select (|address_array_tuple_accessor_array| _owners_28_length_pair_1) expr_50_0)) (and (=> true (and (>= expr_50_0 0) (<= expr_50_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_50_0 i_37_1) (and (= expr_49_length_pair_0 _owners_28_length_pair_1) (and (= expr_48_length_pair_0 owner_19_length_pair_1) true))))))))))))))))))))))))))) true) (block_23_for_post__46_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_2 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_23_for_post__46_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) (and (= i_37_2 (+ expr_44_0 1)) (and (=> true (and (>= expr_45_1 0) (<= expr_45_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_45_1 (+ expr_44_0 1)) (and (=> true (and (>= expr_44_0 0) (<= expr_44_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_44_0 i_37_1) true)))))) true) (block_20_for_header__65_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_2))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_22__66_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) true) true) (block_19_return_constructor_67_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (block_19_return_constructor_67_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 i_37_1) true) true) (summary_3_constructor_67_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1))))


(declare-fun |contract_initializer_24_MultiSig_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| ) Bool)
(declare-fun |contract_initializer_entry_25_MultiSig_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and (and true (= txs_13_length_pair_1 txs_13_length_pair_0)) (= nOwners_15_1 nOwners_15_0)) (= owner_19_length_pair_1 owner_19_length_pair_0)) (= approved_25_length_pair_1 approved_25_length_pair_0))) (and true (= _owners_28_length_pair_1 _owners_28_length_pair_0))) (contract_initializer_entry_25_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1))))


(declare-fun |contract_initializer_after_init_26_MultiSig_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (contract_initializer_entry_25_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1) true) true) (contract_initializer_after_init_26_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (contract_initializer_after_init_26_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1) (and (summary_3_constructor_67_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_2) true)) (> error_1 0)) (contract_initializer_24_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_2))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (contract_initializer_after_init_26_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1) (and (= error_1 0) (and (summary_3_constructor_67_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_1 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_2) true))) true) (contract_initializer_24_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_2))))


(declare-fun |implicit_constructor_entry_27_MultiSig_162_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| |state_type| |struct MultiSig.Tx_array_tuple| Int |mapping(address => bool)_tuple| |mapping(address => mapping(uint256 => bool))_tuple| |address_array_tuple| ) Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (and (and (= state_2 state_0) (= error_1 0)) (and (and (and (and true (= txs_13_length_pair_2 txs_13_length_pair_0)) (= nOwners_15_2 nOwners_15_0)) (= owner_19_length_pair_2 owner_19_length_pair_0)) (= approved_25_length_pair_2 approved_25_length_pair_0))) (and true (= _owners_28_length_pair_2 _owners_28_length_pair_0))) (and (and (and (and true (= txs_13_length_pair_2 (|struct MultiSig.Tx_array_tuple| ((as const (Array Int |struct MultiSig.Tx|)) (|struct MultiSig.Tx| 0 0 0 0)) 0))) (= nOwners_15_2 0)) (= owner_19_length_pair_2 (|mapping(address => bool)_tuple| ((as const (Array Int Bool)) false) 0))) (= approved_25_length_pair_2 (|mapping(address => mapping(uint256 => bool))_tuple| ((as const (Array Int |mapping(uint256 => bool)_tuple|)) (|mapping(uint256 => bool)_tuple| ((as const (Array Int Bool)) false) 0)) 0)))) (implicit_constructor_entry_27_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_2))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_owners_28_length_pair_3 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (implicit_constructor_entry_27_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_2) (and (contract_initializer_24_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_2 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_3) true)) (> error_1 0)) (summary_constructor_2_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_3))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_owners_28_length_pair_3 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (implicit_constructor_entry_27_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_2) (and (= error_1 0) (and (contract_initializer_24_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_2 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_3) true))) true) (summary_constructor_2_MultiSig_162_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_2 txs_13_length_pair_2 nOwners_15_2 owner_19_length_pair_2 approved_25_length_pair_2 _owners_28_length_pair_3))))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_96_0 Int) (_id_96_1 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_owners_28_length_pair_3 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (summary_constructor_2_MultiSig_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _owners_28_length_pair_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _owners_28_length_pair_3) true) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1))))


(declare-fun |error_target_2_0| () Bool)
(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_amt_71_2 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_141_2 Int) (_id_96_0 Int) (_id_96_1 Int) (_id_96_2 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_owners_28_length_pair_3 |address_array_tuple|) (_owners_28_length_pair_4 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (_to_69_2 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> (and (and (interface_0_MultiSig_162_0 this_0 abi_0 crypto_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2048143150)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 122)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 20)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 47)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_6_function_inv__161_162_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 txs_13_length_pair_0 nOwners_15_0 owner_19_length_pair_0 approved_25_length_pair_0 _id_141_0 state_1 txs_13_length_pair_1 nOwners_15_1 owner_19_length_pair_1 approved_25_length_pair_1 _id_141_1)) (= error_0 1))) error_target_2_0)))


(assert
(forall ( (_amt_71_0 Int) (_amt_71_1 Int) (_amt_71_2 Int) (_id_141_0 Int) (_id_141_1 Int) (_id_141_2 Int) (_id_96_0 Int) (_id_96_1 Int) (_id_96_2 Int) (_owners_28_length_pair_0 |address_array_tuple|) (_owners_28_length_pair_1 |address_array_tuple|) (_owners_28_length_pair_2 |address_array_tuple|) (_owners_28_length_pair_3 |address_array_tuple|) (_owners_28_length_pair_4 |address_array_tuple|) (_to_69_0 Int) (_to_69_1 Int) (_to_69_2 Int) (abi_0 |abi_type|) (approved_25_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (approved_25_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (error_2 Int) (error_3 Int) (expr_100_length_pair_0 |mapping(address => bool)_tuple|) (expr_102_1 Int) (expr_103_1 Bool) (expr_107_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_109_1 Int) (expr_110_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_110_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_111_0 Int) (expr_112_1 Bool) (expr_113_1 Bool) (expr_117_0 Int) (expr_118_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_119_1 Int) (expr_120_1 Bool) (expr_123_length_pair_0 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_1 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_123_length_pair_2 |mapping(address => mapping(uint256 => bool))_tuple|) (expr_125_1 Int) (expr_126_0 Int) (expr_127_length_pair_0 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_1 |mapping(uint256 => bool)_tuple|) (expr_127_length_pair_2 |mapping(uint256 => bool)_tuple|) (expr_128_1 Bool) (expr_128_2 Bool) (expr_129_0 Bool) (expr_130_1 Bool) (expr_132_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_132_length_pair_2 |struct MultiSig.Tx_array_tuple|) (expr_133_0 Int) (expr_134_1 |struct MultiSig.Tx|) (expr_134_2 |struct MultiSig.Tx|) (expr_134_3 |struct MultiSig.Tx|) (expr_135_1 Int) (expr_135_2 Int) (expr_136_1 Int) (expr_145_0 Int) (expr_146_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_147_1 Int) (expr_148_1 Bool) (expr_152_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_153_0 Int) (expr_154_1 |struct MultiSig.Tx|) (expr_155_1 Int) (expr_156_0 Int) (expr_157_1 Bool) (expr_31_0 Int) (expr_32_length_pair_0 |address_array_tuple|) (expr_33_1 Int) (expr_34_1 Int) (expr_38_0 Int) (expr_40_0 Int) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_1 Int) (expr_43_1 Bool) (expr_44_0 Int) (expr_45_1 Int) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_49_length_pair_0 |address_array_tuple|) (expr_50_0 Int) (expr_51_1 Int) (expr_52_1 Bool) (expr_53_1 Bool) (expr_56_length_pair_0 |mapping(address => bool)_tuple|) (expr_56_length_pair_1 |mapping(address => bool)_tuple|) (expr_56_length_pair_2 |mapping(address => bool)_tuple|) (expr_57_length_pair_0 |address_array_tuple|) (expr_58_0 Int) (expr_59_1 Int) (expr_60_1 Bool) (expr_60_2 Bool) (expr_61_0 Bool) (expr_62_1 Bool) (expr_75_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_1 Int) (expr_78_1 Bool) (expr_81_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_81_length_pair_1 |struct MultiSig.Tx_array_tuple|) (expr_85_length_pair_0 |struct MultiSig.Tx_array_tuple|) (expr_86_1 Int) (expr_87_0 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 |struct MultiSig.Tx|) (i_37_0 Int) (i_37_1 Int) (i_37_2 Int) (nOwners_15_0 Int) (nOwners_15_1 Int) (nOwners_15_2 Int) (owner_19_length_pair_0 |mapping(address => bool)_tuple|) (owner_19_length_pair_1 |mapping(address => bool)_tuple|) (owner_19_length_pair_2 |mapping(address => bool)_tuple|) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (txs_13_length_pair_0 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_1 |struct MultiSig.Tx_array_tuple|) (txs_13_length_pair_2 |struct MultiSig.Tx_array_tuple|))
(=> error_target_2_0 false)))
(check-sat)