soundness_sat.smt2

(set-logic HORN)

(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 ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
(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 ((|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_95_0| (Int |abi_type| |crypto_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int ) Bool)
(declare-fun |nondet_interface_1_MultiSig_95_0| (Int Int |abi_type| |crypto_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int ) Bool)
(declare-fun |summary_constructor_2_MultiSig_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| ) Bool)
(assert
(forall ( (a_10_0 Int) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|))
(=> (= error_0 0) (nondet_interface_1_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0))))


(declare-fun |summary_3_constructor_59_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| ) Bool)
(declare-fun |summary_4_function_inv__94_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (nondet_interface_1_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1) true) (and (= error_0 0) (summary_4_function_inv__94_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2))) (nondet_interface_1_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2))))


(declare-fun |block_5_function_inv__94_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int ) Bool)
(declare-fun |block_6_inv_93_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(block_5_function_inv__94_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1)))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_5_function_inv__94_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and true (= owner_4_length_pair_1 owner_4_length_pair_0)) (= approved_8_length_pair_1 approved_8_length_pair_0)) (= a_10_1 a_10_0))) true) true)) true) (block_6_inv_93_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1))))


(declare-fun |block_7_return_function_inv__94_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int ) Bool)
(declare-fun |block_8_function_inv__94_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_6_inv_93_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1) (and (= expr_90_1 (<= expr_88_0 expr_89_0)) (and (=> true true) (and (= expr_89_0 1) (and (=> true (and (>= expr_88_0 0) (<= expr_88_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_88_0 a_10_2) (and (= a_10_2 (+ expr_84_0 1)) (and (=> true (and (>= expr_85_1 0) (<= expr_85_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_85_1 (+ expr_84_0 1)) (and (=> true (and (>= expr_84_0 0) (<= expr_84_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_84_0 a_10_1) (and (= expr_77_length_pair_2 approved_8_length_pair_2) (and (= approved_8_length_pair_2 (|mapping(address => bool)_tuple| (store (|mapping(address => bool)_tuple_accessor_array| expr_77_length_pair_1) expr_79_1 expr_82_1) (|mapping(address => bool)_tuple_accessor_length| expr_77_length_pair_1))) (and (= expr_80_2 (select (|mapping(address => bool)_tuple_accessor_array| expr_77_length_pair_1) expr_79_1)) (and (= expr_77_length_pair_1 approved_8_length_pair_1) (and (= expr_82_1 expr_81_0) (and true (and (= expr_80_1 (select (|mapping(address => bool)_tuple_accessor_array| approved_8_length_pair_1) expr_79_1)) (and (=> true (and (>= expr_79_1 0) (<= expr_79_1 1461501637330902918203684832716283019655932542975))) (and (= expr_79_1 (|msg.sender| tx_0)) (and (= expr_77_length_pair_0 approved_8_length_pair_1) (and (= expr_81_0 true) (and (=> true expr_74_1) (and (= expr_74_1 (not expr_73_1)) (and true (and (= expr_73_1 (select (|mapping(address => bool)_tuple_accessor_array| approved_8_length_pair_1) expr_72_1)) (and (=> true (and (>= expr_72_1 0) (<= expr_72_1 1461501637330902918203684832716283019655932542975))) (and (= expr_72_1 (|msg.sender| tx_0)) (and (= expr_70_length_pair_0 approved_8_length_pair_1) (and (=> true expr_66_1) (and true (and (= expr_66_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_4_length_pair_1) expr_65_1)) (and (=> true (and (>= expr_65_1 0) (<= expr_65_1 1461501637330902918203684832716283019655932542975))) (and (= expr_65_1 (|msg.sender| tx_0)) (and (= expr_63_length_pair_0 owner_4_length_pair_1) true))))))))))))))))))))))))))))))))))) (and (not expr_90_1) (= error_1 1))) (block_8_function_inv__94_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_2 a_10_2))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (block_8_function_inv__94_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_2 a_10_2) (summary_4_function_inv__94_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_2 a_10_2))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_6_inv_93_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1) (and (= error_1 error_0) (and (= expr_90_1 (<= expr_88_0 expr_89_0)) (and (=> true true) (and (= expr_89_0 1) (and (=> true (and (>= expr_88_0 0) (<= expr_88_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_88_0 a_10_2) (and (= a_10_2 (+ expr_84_0 1)) (and (=> true (and (>= expr_85_1 0) (<= expr_85_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_85_1 (+ expr_84_0 1)) (and (=> true (and (>= expr_84_0 0) (<= expr_84_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_84_0 a_10_1) (and (= expr_77_length_pair_2 approved_8_length_pair_2) (and (= approved_8_length_pair_2 (|mapping(address => bool)_tuple| (store (|mapping(address => bool)_tuple_accessor_array| expr_77_length_pair_1) expr_79_1 expr_82_1) (|mapping(address => bool)_tuple_accessor_length| expr_77_length_pair_1))) (and (= expr_80_2 (select (|mapping(address => bool)_tuple_accessor_array| expr_77_length_pair_1) expr_79_1)) (and (= expr_77_length_pair_1 approved_8_length_pair_1) (and (= expr_82_1 expr_81_0) (and true (and (= expr_80_1 (select (|mapping(address => bool)_tuple_accessor_array| approved_8_length_pair_1) expr_79_1)) (and (=> true (and (>= expr_79_1 0) (<= expr_79_1 1461501637330902918203684832716283019655932542975))) (and (= expr_79_1 (|msg.sender| tx_0)) (and (= expr_77_length_pair_0 approved_8_length_pair_1) (and (= expr_81_0 true) (and (=> true expr_74_1) (and (= expr_74_1 (not expr_73_1)) (and true (and (= expr_73_1 (select (|mapping(address => bool)_tuple_accessor_array| approved_8_length_pair_1) expr_72_1)) (and (=> true (and (>= expr_72_1 0) (<= expr_72_1 1461501637330902918203684832716283019655932542975))) (and (= expr_72_1 (|msg.sender| tx_0)) (and (= expr_70_length_pair_0 approved_8_length_pair_1) (and (=> true expr_66_1) (and true (and (= expr_66_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_4_length_pair_1) expr_65_1)) (and (=> true (and (>= expr_65_1 0) (<= expr_65_1 1461501637330902918203684832716283019655932542975))) (and (= expr_65_1 (|msg.sender| tx_0)) (and (= expr_63_length_pair_0 owner_4_length_pair_1) true)))))))))))))))))))))))))))))))))))) true) (block_7_return_function_inv__94_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_2 a_10_2))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_7_return_function_inv__94_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1) true) true) (summary_4_function_inv__94_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (interface_0_MultiSig_95_0 this_0 abi_0 crypto_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_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) 53283169)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 3)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 45)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 9)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 97)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_4_function_inv__94_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1)) (= error_0 0))) (interface_0_MultiSig_95_0 this_0 abi_0 crypto_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1))))


(declare-fun |block_9_constructor_59_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| Int ) Bool)
(declare-fun |block_10__58_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| Int ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(block_9_constructor_59_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1)))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_9_constructor_59_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and true (= owner_4_length_pair_1 owner_4_length_pair_0)) (= approved_8_length_pair_1 approved_8_length_pair_0)) (= a_10_1 a_10_0))) (and true (= aa_14_length_pair_1 aa_14_length_pair_0))) true)) true) (block_10__58_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1))))


(declare-fun |block_11_return_constructor_59_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| Int ) Bool)
(declare-fun |block_12_for_header__57_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| Int ) Bool)
(declare-fun |block_13_for_body__56_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| Int ) Bool)
(declare-fun |block_14__58_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| Int ) Bool)
(declare-fun |block_15_for_post__38_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| Int ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_10__58_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) (and (= i_29_2 expr_30_0) (and (=> true true) (and (= expr_30_0 0) (and (=> true expr_25_1) (and (= expr_25_1 (= expr_23_1 expr_24_0)) (and (=> true true) (and (= expr_24_0 1) (and (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_23_1 0) (<= expr_23_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_23_1 (|address_array_tuple_accessor_length| expr_22_length_pair_0)) (and (= expr_22_length_pair_0 aa_14_length_pair_1) (and (= a_10_2 expr_19_1) (and (=> true (and (>= expr_19_1 0) (<= expr_19_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_19_1 expr_18_0) (and (=> true (and (>= expr_17_0 0) (<= expr_17_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_17_0 a_10_1) (and (=> true true) (and (= expr_18_0 0) (and (=> true true) (and (= expr_12_0 1) (and (>= (|address_array_tuple_accessor_length| aa_14_length_pair_1) 0) (and (= i_29_1 0) true))))))))))))))))))))))) true) (block_12_for_header__57_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_2 aa_14_length_pair_1 i_29_2))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_12_for_header__57_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) (and (= expr_35_1 (< expr_32_0 expr_34_1)) (and (and (>= expr_34_1 0) (<= expr_34_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_34_1 0) (<= expr_34_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_34_1 (|address_array_tuple_accessor_length| expr_33_length_pair_0)) (and (= expr_33_length_pair_0 aa_14_length_pair_1) (and (=> true (and (>= expr_32_0 0) (<= expr_32_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_32_0 i_29_1) true)))))))) expr_35_1) (block_13_for_body__56_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_12_for_header__57_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) (and (= expr_35_1 (< expr_32_0 expr_34_1)) (and (and (>= expr_34_1 0) (<= expr_34_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (=> true (and (>= expr_34_1 0) (<= expr_34_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_34_1 (|address_array_tuple_accessor_length| expr_33_length_pair_0)) (and (= expr_33_length_pair_0 aa_14_length_pair_1) (and (=> true (and (>= expr_32_0 0) (<= expr_32_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_32_0 i_29_1) true)))))))) (not expr_35_1)) (block_14__58_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_13_for_body__56_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) (and (= expr_48_length_pair_2 owner_4_length_pair_2) (and (= owner_4_length_pair_2 (|mapping(address => bool)_tuple| (store (|mapping(address => bool)_tuple_accessor_array| expr_48_length_pair_1) expr_51_1 expr_54_1) (|mapping(address => bool)_tuple_accessor_length| expr_48_length_pair_1))) (and (= expr_52_2 (select (|mapping(address => bool)_tuple_accessor_array| expr_48_length_pair_1) expr_51_1)) (and (= expr_48_length_pair_1 owner_4_length_pair_1) (and (= expr_54_1 expr_53_0) (and true (and (= expr_52_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_4_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| aa_14_length_pair_1) expr_50_0)) (and (=> true (and (>= expr_50_0 0) (<= expr_50_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_50_0 i_29_1) (and (= expr_49_length_pair_0 aa_14_length_pair_1) (and (= expr_48_length_pair_0 owner_4_length_pair_1) (and (= expr_53_0 true) (and (=> true expr_45_1) (and (= expr_45_1 (not expr_44_1)) (and true (and (= expr_44_1 (select (|mapping(address => bool)_tuple_accessor_array| owner_4_length_pair_1) expr_43_1)) (and (and (>= expr_43_1 0) (<= expr_43_1 1461501637330902918203684832716283019655932542975)) (and (=> true (and (>= expr_43_1 0) (<= expr_43_1 1461501637330902918203684832716283019655932542975))) (and (= expr_43_1 (select (|address_array_tuple_accessor_array| aa_14_length_pair_1) expr_42_0)) (and (=> true (and (>= expr_42_0 0) (<= expr_42_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_42_0 i_29_1) (and (= expr_41_length_pair_0 aa_14_length_pair_1) (and (= expr_40_length_pair_0 owner_4_length_pair_1) true))))))))))))))))))))))))))) true) (block_15_for_post__38_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_2 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_15_for_post__38_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) (and (= i_29_2 (+ expr_36_0 1)) (and (=> true (and (>= expr_37_1 0) (<= expr_37_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_37_1 (+ expr_36_0 1)) (and (=> true (and (>= expr_36_0 0) (<= expr_36_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_36_0 i_29_1) true)))))) true) (block_12_for_header__57_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_2))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_14__58_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) true) true) (block_11_return_constructor_59_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (block_11_return_constructor_59_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 i_29_1) true) true) (summary_3_constructor_59_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1))))


(declare-fun |contract_initializer_16_MultiSig_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| ) Bool)
(declare-fun |contract_initializer_entry_17_MultiSig_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (and (= state_1 state_0) (= error_0 0)) (and (and (and true (= owner_4_length_pair_1 owner_4_length_pair_0)) (= approved_8_length_pair_1 approved_8_length_pair_0)) (= a_10_1 a_10_0))) (and true (= aa_14_length_pair_1 aa_14_length_pair_0))) (contract_initializer_entry_17_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1))))


(declare-fun |contract_initializer_after_init_18_MultiSig_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (contract_initializer_entry_17_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1) true) true) (contract_initializer_after_init_18_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (contract_initializer_after_init_18_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1) (and (summary_3_constructor_59_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_2) true)) (> error_1 0)) (contract_initializer_16_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_2))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (contract_initializer_after_init_18_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1) (and (= error_1 0) (and (summary_3_constructor_59_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_1 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_2) true))) true) (contract_initializer_16_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_2))))


(declare-fun |implicit_constructor_entry_19_MultiSig_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (and (and (and (= state_2 state_0) (= error_1 0)) (and (and (and true (= owner_4_length_pair_2 owner_4_length_pair_0)) (= approved_8_length_pair_2 approved_8_length_pair_0)) (= a_10_2 a_10_0))) (and true (= aa_14_length_pair_2 aa_14_length_pair_0))) (and (and (and true (= owner_4_length_pair_2 (|mapping(address => bool)_tuple| ((as const (Array Int Bool)) false) 0))) (= approved_8_length_pair_2 (|mapping(address => bool)_tuple| ((as const (Array Int Bool)) false) 0))) (= a_10_2 0))) true) (implicit_constructor_entry_19_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_2))))


(declare-fun |implicit_constructor_entry_after_address_20_MultiSig_95_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| |state_type| |mapping(address => bool)_tuple| |mapping(address => bool)_tuple| Int |address_array_tuple| ) Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (implicit_constructor_entry_19_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_2) true) true) (implicit_constructor_entry_after_address_20_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_2))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (aa_14_length_pair_3 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (implicit_constructor_entry_after_address_20_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_2) (and (contract_initializer_16_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_2 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_3) true)) (> error_1 0)) (summary_constructor_2_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_3))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (aa_14_length_pair_3 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (implicit_constructor_entry_after_address_20_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_2) (and (= error_1 0) (and (contract_initializer_16_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_length_pair_2 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_3) true))) true) (summary_constructor_2_MultiSig_95_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_2 owner_4_length_pair_2 approved_8_length_pair_2 a_10_2 aa_14_length_pair_3))))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (aa_14_length_pair_3 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (summary_constructor_2_MultiSig_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 aa_14_length_pair_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1 aa_14_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_95_0 this_0 abi_0 crypto_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1))))


(declare-fun |error_target_2_0| () Bool)
(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (aa_14_length_pair_3 |address_array_tuple|) (aa_14_length_pair_4 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> (and (and (interface_0_MultiSig_95_0 this_0 abi_0 crypto_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_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) 53283169)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 3)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 45)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 9)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 97)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (summary_4_function_inv__94_95_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 owner_4_length_pair_0 approved_8_length_pair_0 a_10_0 state_1 owner_4_length_pair_1 approved_8_length_pair_1 a_10_1)) (= error_0 1))) error_target_2_0)))


(assert
(forall ( (a_10_0 Int) (a_10_1 Int) (a_10_2 Int) (aa_14_length_pair_0 |address_array_tuple|) (aa_14_length_pair_1 |address_array_tuple|) (aa_14_length_pair_2 |address_array_tuple|) (aa_14_length_pair_3 |address_array_tuple|) (aa_14_length_pair_4 |address_array_tuple|) (abi_0 |abi_type|) (approved_8_length_pair_0 |mapping(address => bool)_tuple|) (approved_8_length_pair_1 |mapping(address => bool)_tuple|) (approved_8_length_pair_2 |mapping(address => bool)_tuple|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_12_0 Int) (expr_17_0 Int) (expr_18_0 Int) (expr_19_1 Int) (expr_22_length_pair_0 |address_array_tuple|) (expr_23_1 Int) (expr_24_0 Int) (expr_25_1 Bool) (expr_30_0 Int) (expr_32_0 Int) (expr_33_length_pair_0 |address_array_tuple|) (expr_34_1 Int) (expr_35_1 Bool) (expr_36_0 Int) (expr_37_1 Int) (expr_40_length_pair_0 |mapping(address => bool)_tuple|) (expr_41_length_pair_0 |address_array_tuple|) (expr_42_0 Int) (expr_43_1 Int) (expr_44_1 Bool) (expr_45_1 Bool) (expr_48_length_pair_0 |mapping(address => bool)_tuple|) (expr_48_length_pair_1 |mapping(address => bool)_tuple|) (expr_48_length_pair_2 |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_52_2 Bool) (expr_53_0 Bool) (expr_54_1 Bool) (expr_63_length_pair_0 |mapping(address => bool)_tuple|) (expr_65_1 Int) (expr_66_1 Bool) (expr_70_length_pair_0 |mapping(address => bool)_tuple|) (expr_72_1 Int) (expr_73_1 Bool) (expr_74_1 Bool) (expr_77_length_pair_0 |mapping(address => bool)_tuple|) (expr_77_length_pair_1 |mapping(address => bool)_tuple|) (expr_77_length_pair_2 |mapping(address => bool)_tuple|) (expr_79_1 Int) (expr_80_1 Bool) (expr_80_2 Bool) (expr_81_0 Bool) (expr_82_1 Bool) (expr_84_0 Int) (expr_85_1 Int) (expr_88_0 Int) (expr_89_0 Int) (expr_90_1 Bool) (i_29_0 Int) (i_29_1 Int) (i_29_2 Int) (owner_4_length_pair_0 |mapping(address => bool)_tuple|) (owner_4_length_pair_1 |mapping(address => bool)_tuple|) (owner_4_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|))
(=> error_target_2_0 false)))
(check-sat)