out1.smt2

(declare-datatypes ((ecrecover_input_type 0)) (((ecrecover_input_type (hash Int) (v Int) (r Int) (s Int)))))
(declare-datatypes ((storage_State_42_type 0)) (((storage_State_42_type (x_20_State_42 Int) (o_23_State_42 Int) (c_26_State_42 Int)))))
(declare-datatypes ((storage_Other_18_type 0)) (((storage_Other_18_type (c_4_Other_18 Int)))))
(declare-datatypes ((storage_C_103_type 0)) (((storage_C_103_type (owner_44_C_103 Int) (y_46_C_103 Int) (s_49_C_103 Int)))))
(declare-datatypes ((storage_type 0)) (((storage_type (storage_C_103 (Array Int storage_C_103_type)) (storage_Other_18 (Array Int storage_Other_18_type)) (storage_State_42 (Array Int storage_State_42_type))))))
(declare-datatypes ((abi_type 0)) (((abi_type))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int)) (isActive (Array Int Bool)) (storage storage_type)))))
(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 ((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-rel block_43_function_f__94_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int Int))
(declare-rel implicit_constructor_entry_22_Other_18_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int))
(declare-rel contract_initializer_19_Other_18_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int))
(declare-rel contract_initializer_entry_31_State_42_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int Int Int Int Int))
(declare-rel nondet_call_41_0 (Int Int abi_type crypto_type state_type Int Int Int state_type Int Int Int))
(declare-rel summary_7_function_f__41_42_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel nondet_call_27_0 (Int Int abi_type crypto_type state_type Int Int Int state_type Int Int Int))
(declare-rel block_40_return_function_f__94_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int Int))
(declare-rel block_47_return_ghost_g_100_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel error_target_4_0 ())
(declare-rel block_26_return_function_f__41_42_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel block_35_function_setOwner__68_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int Int state_type Int Int Int Int))
(declare-rel contract_initializer_51_C_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel block_38_function_f__94_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int Int))
(declare-rel block_48_constructor_58_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel nondet_call_18_0 (Int Int abi_type crypto_type state_type Int state_type Int))
(declare-rel summary_13_function_f__94_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel interface_4_State_42_0 (Int abi_type crypto_type state_type Int Int Int))
(declare-rel block_24_function_f__41_42_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel block_42_function_f__94_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int Int))
(declare-rel nondet_interface_1_Other_18_0 (Int Int abi_type crypto_type state_type Int state_type Int))
(declare-rel block_15_function_h__17_18_0 (Int Int abi_type crypto_type tx_type state_type Int state_type Int))
(declare-rel implicit_constructor_entry_33_State_42_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int Int Int Int Int))
(declare-rel block_49__57_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel summary_12_function_setOwner__68_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int Int state_type Int Int Int Int))
(declare-rel summary_3_function_h__17_18_0 (Int Int abi_type crypto_type tx_type state_type Int state_type Int))
(declare-rel block_50_return_constructor_58_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel nondet_interface_9_C_103_0 (Int Int abi_type crypto_type state_type Int Int Int state_type Int Int Int))
(declare-rel contract_initializer_after_init_32_State_42_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int Int Int Int Int))
(declare-rel summary_constructor_10_C_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel nondet_interface_5_State_42_0 (Int Int abi_type crypto_type state_type Int Int Int state_type Int Int Int))
(declare-rel implicit_constructor_entry_54_C_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel interface_8_C_103_0 (Int abi_type crypto_type state_type Int Int Int))
(declare-rel implicit_constructor_entry_after_address_55_C_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel block_44_function_g__102_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel error_target_3_0 ())
(declare-rel contract_initializer_30_State_42_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int Int Int Int Int))
(declare-rel summary_14_function_g__102_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel summary_constructor_6_State_42_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int Int Int Int Int))
(declare-rel block_37_return_function_setOwner__68_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int Int state_type Int Int Int Int))
(declare-rel summary_constructor_2_Other_18_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int))
(declare-rel block_36_setOwner_67_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int Int state_type Int Int Int Int))
(declare-rel contract_initializer_entry_20_Other_18_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int))
(declare-rel block_46_return_function_g__102_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel contract_initializer_entry_52_C_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel summary_11_constructor_58_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel contract_initializer_after_init_21_Other_18_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int))
(declare-rel block_16_h_16_18_0 (Int Int abi_type crypto_type tx_type state_type Int state_type Int))
(declare-rel implicit_constructor_entry_after_address_23_Other_18_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int))
(declare-rel interface_0_Other_18_0 (Int abi_type crypto_type state_type Int))
(declare-rel contract_initializer_after_init_53_C_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int))
(declare-rel block_25_f_40_42_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel block_45_g_101_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-rel block_39_f_93_103_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int Int))
(declare-rel block_17_return_function_h__17_18_0 (Int Int abi_type crypto_type tx_type state_type Int state_type Int))
(declare-rel implicit_constructor_entry_after_address_34_State_42_0 (Int Int abi_type crypto_type tx_type state_type state_type Int Int Int Int Int Int))
(declare-rel nondet_call_28_0 (Int Int abi_type crypto_type state_type Int Int Int state_type Int Int Int))
(declare-rel block_29_return_ghost_f_39_42_0 (Int Int abi_type crypto_type tx_type state_type Int Int Int state_type Int Int Int Int))
(declare-var A Int)
(declare-var B state_type)
(declare-var C Int)
(declare-var D crypto_type)
(declare-var E Int)
(declare-var F abi_type)
(declare-var G tx_type)
(declare-var H state_type)
(declare-var I state_type)
(declare-var J Int)
(declare-var K Int)
(declare-var L Int)
(declare-var M Int)
(declare-var N Int)
(declare-var O Int)
(declare-var P Int)
(declare-var Q Int)
(declare-var R Int)
(declare-var S Int)
(declare-var T Int)
(declare-var U state_type)
(declare-var V Int)
(declare-var W Int)
(declare-var X Int)
(declare-var Y Int)
(declare-var Z Int)
(declare-var A1 Bool)
(declare-var B1 Int)
(declare-var C1 Int)
(declare-var D1 Int)
(declare-var E1 Int)
(declare-var F1 Bool)
(declare-var G1 Int)
(declare-var H1 Int)
(declare-var I1 Int)
(rule (! (=> (= C 0) (nondet_interface_1_Other_18_0 C A F D B E B E)) :named base_nondet))
(rule (! (=> (and (summary_3_function_h__17_18_0 C A F D G H K B J)
         (nondet_interface_1_Other_18_0 E A F D I L H K)
         (= E 0))
    (nondet_interface_1_Other_18_0 C A F D I L B J)) :named nondet_interface_1_Other_18_0_to_nondet_interface_1_Other_18_0))
(rule (! (=> (= J 0) (nondet_interface_5_State_42_0 J C F D B A E K B A E K)) :named base_nondet!))
(rule (! (=> (and (summary_7_function_f__41_42_0 N J F D G H C L Q B A K P S)
         (nondet_interface_5_State_42_0 O J F D I E M R H C L Q)
         (= O 0))
    (nondet_interface_5_State_42_0 N J F D I E M R B A K P)) :named nondet_interface_5_State_42_0_to_nondet_interface_5_State_42_0))
(rule (! (=> (= K 0) (nondet_interface_9_C_103_0 K C F D B J A E B J A E)) :named base_nondet!!))
(rule (! (=> (and (summary_12_function_setOwner__68_103_0 Q J F D G H O C L T B N A K S)
         (nondet_interface_9_C_103_0 R J F D I P E M H O C L)
         (= R 0))
    (nondet_interface_9_C_103_0 Q J F D I P E M B N A K)) :named nondet_interface_9_C_103_0_to_nondet_interface_9_C_103_0))
(rule (! (=> (and (summary_13_function_f__94_103_0 Q J F D G H O C L B N A K)
         (nondet_interface_9_C_103_0 R J F D I P E M H O C L)
         (= R 0))
    (nondet_interface_9_C_103_0 Q J F D I P E M B N A K)) :named nondet_interface_9_C_103_0_to_nondet_interface_9_C_103_0!))
(rule (! (=> (and (summary_14_function_g__102_103_0 Q J F D G H O C L B N A K S)
         (nondet_interface_9_C_103_0 R J F D I P E M H O C L)
         (= R 0))
    (nondet_interface_9_C_103_0 Q J F D I P E M B N A K)) :named nondet_interface_9_C_103_0_to_nondet_interface_9_C_103_0!!))
(rule (! (block_15_function_h__17_18_0 C A F D G H J B E) :named block_15_function_h__17_18_0!))
(rule (! (=> (and (block_15_function_h__17_18_0 C A F D G H J B E)
         (= C 0)
         (= E J)
         (= B H))
    (block_16_h_16_18_0 C A F D G H J B E)) :named block_15_function_h__17_18_0_to_block_16_h_16_18_0))
(rule (! (=> (nondet_interface_1_Other_18_0 C A F D H J B E)
    (nondet_call_18_0 C A F D H J B E)) :named nondet_call_18_0!))
(rule (! (let ((a!1 (and (block_16_h_16_18_0 L A F D G I O H N)
                (nondet_call_18_0 K A F D H N B M)
                (= J 0)
                (=> true true)
                (= E J)
                (=> true
                    (and (>= E 0)
                         (<= E
                             1461501637330902918203684832716283019655932542975)))
                (= C N)
                (> K 0)
                (=> true true))))
  (=> a!1 (summary_3_function_h__17_18_0 K A F D G I O B M))) :named block_16_h_16_18_0_to_summary_3_function_h__17_18_0))
(rule (! (let ((a!1 (and (block_16_h_16_18_0 L A F D G I O H N)
                (nondet_call_18_0 K A F D H N B M)
                (= J 0)
                (=> true true)
                (= E J)
                (=> true
                    (and (>= E 0)
                         (<= E
                             1461501637330902918203684832716283019655932542975)))
                (= K 0)
                (= C N)
                (=> true true))))
  (=> a!1 (block_17_return_function_h__17_18_0 K A F D G I O B M))) :named block_16_h_16_18_0_to_block_17_return_function_h__17_18_0))
(rule (! (=> (block_17_return_function_h__17_18_0 C A F D G H J B E)
    (summary_3_function_h__17_18_0 C A F D G H J B E)) :named block_17_return_function_h__17_18_0_to_summary_3_function_h__17_18_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data G)) 0) 184))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data G)) 1) 201))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data G)) 2) 211))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data G)) 3) 101)))
(let ((a!5 (and (interface_0_Other_18_0 A F D H J)
                (summary_3_function_h__17_18_0 C A F D G H J B E)
                (>= (block.coinbase G) 0)
                (<= (block.chainid G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.difficulty G) 0)
                (<= (block.coinbase G)
                    1461501637330902918203684832716283019655932542975)
                (>= (block.gaslimit G) 0)
                (<= (block.difficulty G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.number G) 0)
                (<= (block.gaslimit G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.value G) 0)
                (>= (block.timestamp G) 0)
                (<= (block.number G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.sig G) 3100234597)
                (>= (msg.sender G) 0)
                (<= (block.timestamp G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (>= (msg.value G) 0)
                (<= (msg.sender G)
                    1461501637330902918203684832716283019655932542975)
                a!2
                (>= (tx.origin G) 0)
                (<= (msg.value G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!3
                (>= (tx.gasprice G) 0)
                (<= (tx.origin G)
                    1461501637330902918203684832716283019655932542975)
                a!4
                (<= (tx.gasprice G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (bytes_tuple_accessor_length (msg.data G)) 4)
                (= C 0)
                (>= (block.chainid G) 0))))
  (=> a!5 (interface_0_Other_18_0 A F D B E)))) :named interface_0_Other_18_0_to_interface_0_Other_18_0))
(rule (! (=> (and (= B H) (= C 0) (= E J))
    (contract_initializer_entry_20_Other_18_0 C A F D G H B J E)) :named contract_initializer_entry_20_Other_18_0!))
(rule (! (=> (contract_initializer_entry_20_Other_18_0 C A F D G H B J E)
    (contract_initializer_after_init_21_Other_18_0 C A F D G H B J E)) :named contract_initializer_entry_20_Other_18_0_to_contract_initializer_after_init_21_Other_18_0))
(rule (! (=> (contract_initializer_after_init_21_Other_18_0 C A F D G H B J E)
    (contract_initializer_19_Other_18_0 C A F D G H B J E)) :named contract_initializer_after_init_21_Other_18_0_to_contract_initializer_19_Other_18_0))
(rule (! (let ((a!1 (and (= B H)
                (= C 0)
                (= E J)
                (= E 0)
                (= (select (isActive B) A) false))))
  (=> a!1 (implicit_constructor_entry_22_Other_18_0 C A F D G H B J E))) :named implicit_constructor_entry_22_Other_18_0!))
(rule (! (let ((a!1 (= B
              (state_type (balances H) (store (isActive H) A true) (storage H)))))
  (=> (and (implicit_constructor_entry_22_Other_18_0 C A F D G I H J E) a!1)
      (implicit_constructor_entry_after_address_23_Other_18_0 C A F D G I B J E))) :named implicit_constructor_entry_22_Other_18_0_to_implicit_constructor_entry_after_address_23_Other_18_0))
(rule (! (=> (and (implicit_constructor_entry_after_address_23_Other_18_0
           E
           A
           F
           D
           G
           I
           H
           L
           K)
         (contract_initializer_19_Other_18_0 C A F D G H B K J)
         (> C 0))
    (summary_constructor_2_Other_18_0 C A F D G I B L J)) :named implicit_constructor_entry_after_address_23_Other_18_0_to_summary_constructor_2_Other_18_0))
(rule (! (let ((a!1 (storage_type (storage_C_103 (storage H))
                         (store (storage_Other_18 (storage H))
                                A
                                (storage_Other_18_type J))
                         (storage_State_42 (storage H)))))
(let ((a!2 (and (contract_initializer_19_Other_18_0 C A F D G I H K J)
                (implicit_constructor_entry_after_address_23_Other_18_0
                  E
                  A
                  F
                  D
                  G
                  U
                  I
                  L
                  K)
                (= B (state_type (balances H) (isActive H) a!1))
                (= C 0))))
  (=> a!2 (summary_constructor_2_Other_18_0 C A F D G U B L J)))) :named implicit_constructor_entry_after_address_23_Other_18_0_to_summary_constructor_2_Other_18_0!))
(rule (! (=> (and (summary_constructor_2_Other_18_0 C A F D G H B J E)
         (>= (block.coinbase G) 0)
         (<= (block.chainid G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.difficulty G) 0)
         (<= (block.coinbase G)
             1461501637330902918203684832716283019655932542975)
         (>= (block.gaslimit G) 0)
         (<= (block.difficulty G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.number G) 0)
         (<= (block.gaslimit G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.timestamp G) 0)
         (<= (block.number G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (msg.sender G) 0)
         (<= (block.timestamp G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (msg.value G) 0)
         (<= (msg.sender G) 1461501637330902918203684832716283019655932542975)
         (>= (tx.origin G) 0)
         (<= (msg.value G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (tx.gasprice G) 0)
         (<= (tx.origin G) 1461501637330902918203684832716283019655932542975)
         (<= (tx.gasprice G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (= (msg.value G) 0)
         (= C 0)
         (>= (block.chainid G) 0))
    (interface_0_Other_18_0 A F D B E)) :named summary_constructor_2_Other_18_0_to_interface_0_Other_18_0))
(rule (! (block_24_function_f__41_42_0 L E F D G H C K N B A J M O) :named block_24_function_f__41_42_0!))
(rule (! (=> (and (block_24_function_f__41_42_0 L E F D G H C K N B A J M O)
         (= B H)
         (= J K)
         (= L 0)
         (= M N)
         (= A C))
    (block_25_f_40_42_0 L E F D G H C K N B A J M O)) :named block_24_function_f__41_42_0_to_block_25_f_40_42_0))
(rule (! (=> (nondet_interface_5_State_42_0 L E F D H C K N B A J M)
    (nondet_call_27_0 L E F D H C K N B A J M)) :named nondet_call_27_0!))
(rule (! (=> (and (block_25_f_40_42_0 P J F D G I E M S H C L R T)
         (nondet_call_27_0 O J F D H C L R B A K Q)
         (=> true true)
         (= T 0)
         (> O 0)
         (= N L))
    (summary_7_function_f__41_42_0 O J F D G I E M S B A K Q T)) :named block_25_f_40_42_0_to_summary_7_function_f__41_42_0))
(rule (! (=> (nondet_interface_5_State_42_0 J C F D B A E K B A E K)
    (nondet_call_28_0 J C F D B A E K B A E K)) :named nondet_call_28_0!))
(rule (! (=> (and (block_25_f_40_42_0 R J F D G I E M V H C L T W)
         (nondet_call_28_0 P J F D B A K S B A K S)
         (nondet_call_27_0 Q J F D H C L T B A K S)
         (=> true true)
         (= Q 0)
         (= N S)
         (=> true true)
         (= W 0)
         (> P 0)
         (= O L))
    (summary_7_function_f__41_42_0 P J F D G I E M V B A K S W)) :named block_25_f_40_42_0_to_summary_7_function_f__41_42_0!))
(rule (! (let ((a!1 (and (block_25_f_40_42_0 S J F D G I E M W H C L V Z)
                (nondet_call_28_0 Q J F D B A K T B A K T)
                (nondet_call_27_0 R J F D H C L V B A K T)
                (=> true true)
                (= R 0)
                (= O T)
                (=> true true)
                (= Q 0)
                (= N X)
                (=> true
                    (and (>= N 0)
                         (<= N
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= Y N)
                (= Z 0)
                (= P L))))
  (=> a!1 (block_26_return_function_f__41_42_0 Q J F D G I E M W B A K T Y))) :named block_25_f_40_42_0_to_block_26_return_function_f__41_42_0))
(rule (! (let ((a!1 (and (block_29_return_ghost_f_39_42_0 Q J F D G I E M V B A K S X)
                (nondet_call_28_0 Q J F D B A K S B A K S)
                (nondet_call_27_0 R J F D H C L T B A K S)
                (=> true true)
                (= R 0)
                (= O S)
                (=> true true)
                (= Q 0)
                (= N W)
                (=> true
                    (and (>= N 0)
                         (<= N
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= X N)
                (= Y 0)
                (= P L))))
  (=> a!1 (block_26_return_function_f__41_42_0 Q J F D G I E M V B A K S X))) :named block_29_return_ghost_f_39_42_0_to_block_26_return_function_f__41_42_0))
(rule (! (=> (block_26_return_function_f__41_42_0 L E F D G H C K N B A J M O)
    (summary_7_function_f__41_42_0 L E F D G H C K N B A J M O)) :named block_26_return_function_f__41_42_0_to_summary_7_function_f__41_42_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data G)) 0) 38))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data G)) 1) 18))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data G)) 2) 31))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data G)) 3) 240)))
(let ((a!5 (and (interface_4_State_42_0 E F D H C K N)
                (summary_7_function_f__41_42_0 L E F D G H C K N B A J M O)
                (>= (block.coinbase G) 0)
                (<= (block.chainid G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.difficulty G) 0)
                (<= (block.coinbase G)
                    1461501637330902918203684832716283019655932542975)
                (>= (block.gaslimit G) 0)
                (<= (block.difficulty G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.number G) 0)
                (<= (block.gaslimit G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.value G) 0)
                (>= (block.timestamp G) 0)
                (<= (block.number G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.sig G) 638722032)
                (>= (msg.sender G) 0)
                (<= (block.timestamp G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (>= (msg.value G) 0)
                (<= (msg.sender G)
                    1461501637330902918203684832716283019655932542975)
                a!2
                (>= (tx.origin G) 0)
                (<= (msg.value G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!3
                (>= (tx.gasprice G) 0)
                (<= (tx.origin G)
                    1461501637330902918203684832716283019655932542975)
                a!4
                (<= (tx.gasprice G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (bytes_tuple_accessor_length (msg.data G)) 4)
                (= L 0)
                (>= (block.chainid G) 0))))
  (=> a!5 (interface_4_State_42_0 E F D B A J M)))) :named interface_4_State_42_0_to_interface_4_State_42_0))
(rule (! (=> (and (= A C) (= B H) (= J K) (= L 0) (= M N))
    (contract_initializer_entry_31_State_42_0 L E F D G H B C K N A J M)) :named contract_initializer_entry_31_State_42_0!))
(rule (! (=> (contract_initializer_entry_31_State_42_0 L E F D G H B C K N A J M)
    (contract_initializer_after_init_32_State_42_0 L E F D G H B C K N A J M)) :named contract_initializer_entry_31_State_42_0_to_contract_initializer_after_init_32_State_42_0))
(rule (! (=> (contract_initializer_after_init_32_State_42_0 L E F D G H B C K N A J M)
    (contract_initializer_30_State_42_0 L E F D G H B C K N A J M)) :named contract_initializer_after_init_32_State_42_0_to_contract_initializer_30_State_42_0))
(rule (! (let ((a!1 (and (= A C)
                (= B H)
                (= A 0)
                (= J K)
                (= L 0)
                (= J 0)
                (= M N)
                (= M 0)
                (= (select (isActive B) E) false))))
  (=> a!1 (implicit_constructor_entry_33_State_42_0 L E F D G H B C K N A J M))) :named implicit_constructor_entry_33_State_42_0!))
(rule (! (let ((a!1 (= B
              (state_type (balances H) (store (isActive H) E true) (storage H)))))
  (=> (and (implicit_constructor_entry_33_State_42_0 L E F D G I H C K N A J M)
           a!1)
      (implicit_constructor_entry_after_address_34_State_42_0
        L
        E
        F
        D
        G
        I
        B
        C
        K
        N
        A
        J
        M))) :named implicit_constructor_entry_33_State_42_0_to_implicit_constructor_entry_after_address_34_State_42_0))
(rule (! (=> (and (implicit_constructor_entry_after_address_34_State_42_0
           O
           J
           F
           D
           G
           I
           H
           E
           M
           R
           C
           L
           Q)
         (contract_initializer_30_State_42_0 N J F D G H B C L Q A K P)
         (> N 0))
    (summary_constructor_6_State_42_0 N J F D G I B E M R A K P)) :named implicit_constructor_entry_after_address_34_State_42_0_to_summary_constructor_6_State_42_0))
(rule (! (let ((a!1 (storage_type (storage_C_103 (storage H))
                         (storage_Other_18 (storage H))
                         (store (storage_State_42 (storage H))
                                J
                                (storage_State_42_type A K P)))))
(let ((a!2 (and (contract_initializer_30_State_42_0 N J F D G I H C L Q A K P)
                (implicit_constructor_entry_after_address_34_State_42_0
                  O
                  J
                  F
                  D
                  G
                  U
                  I
                  E
                  M
                  R
                  C
                  L
                  Q)
                (= B (state_type (balances H) (isActive H) a!1))
                (= N 0))))
  (=> a!2 (summary_constructor_6_State_42_0 N J F D G U B E M R A K P)))) :named implicit_constructor_entry_after_address_34_State_42_0_to_summary_constructor_6_State_42_0!))
(rule (! (=> (and (summary_constructor_6_State_42_0 L E F D G H B C K N A J M)
         (>= (block.coinbase G) 0)
         (<= (block.chainid G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.difficulty G) 0)
         (<= (block.coinbase G)
             1461501637330902918203684832716283019655932542975)
         (>= (block.gaslimit G) 0)
         (<= (block.difficulty G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.number G) 0)
         (<= (block.gaslimit G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.timestamp G) 0)
         (<= (block.number G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (msg.sender G) 0)
         (<= (block.timestamp G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (msg.value G) 0)
         (<= (msg.sender G) 1461501637330902918203684832716283019655932542975)
         (>= (tx.origin G) 0)
         (<= (msg.value G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (tx.gasprice G) 0)
         (<= (tx.origin G) 1461501637330902918203684832716283019655932542975)
         (<= (tx.gasprice G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (= (msg.value G) 0)
         (= L 0)
         (>= (block.chainid G) 0))
    (interface_4_State_42_0 E F D B A J M)) :named summary_constructor_6_State_42_0_to_interface_4_State_42_0))
(rule (! (block_35_function_setOwner__68_103_0 N E F D G H M C K P B L A J O) :named block_35_function_setOwner__68_103_0!))
(rule (! (=> (and (block_35_function_setOwner__68_103_0 N E F D G H M C K P B L A J O)
         (= L M)
         (= N 0)
         (= A C)
         (= J K)
         (= O P)
         (= B H))
    (block_36_setOwner_67_103_0 N E F D G H M C K P B L A J O)) :named block_35_function_setOwner__68_103_0_to_block_36_setOwner_67_103_0))
(rule (! (let ((a!1 (and (block_36_setOwner_67_103_0 R E F D G H N C K T B M A J S)
                (= P S)
                (=> true
                    (and (>= P 0)
                         (<= P
                             1461501637330902918203684832716283019655932542975)))
                (= Q M)
                (=> true
                    (and (>= Q 0)
                         (<= Q
                             1461501637330902918203684832716283019655932542975)))
                (= O P)
                (=> true
                    (and (>= O 0)
                         (<= O
                             1461501637330902918203684832716283019655932542975)))
                (= L O)
                (<= S 1461501637330902918203684832716283019655932542975)
                (>= S 0))))
  (=> a!1
      (block_37_return_function_setOwner__68_103_0
        R
        E
        F
        D
        G
        H
        N
        C
        K
        T
        B
        L
        A
        J
        S))) :named block_36_setOwner_67_103_0_to_block_37_return_function_setOwner__68_103_0))
(rule (! (=> (block_37_return_function_setOwner__68_103_0 N E F D G H M C K P B L A J O)
    (summary_12_function_setOwner__68_103_0 N E F D G H M C K P B L A J O)) :named block_37_return_function_setOwner__68_103_0_to_summary_12_function_setOwner__68_103_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data G)) 0) 19))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data G)) 1) 175))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data G)) 2) 64))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data G)) 3) 53)))
(let ((a!5 (and (interface_8_C_103_0 E F D H M C K)
                (summary_12_function_setOwner__68_103_0
                  N
                  E
                  F
                  D
                  G
                  H
                  M
                  C
                  K
                  P
                  B
                  L
                  A
                  J
                  O)
                (>= (block.coinbase G) 0)
                (<= (block.chainid G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.difficulty G) 0)
                (<= (block.coinbase G)
                    1461501637330902918203684832716283019655932542975)
                (>= (block.gaslimit G) 0)
                (<= (block.difficulty G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.number G) 0)
                (<= (block.gaslimit G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.value G) 0)
                (>= (block.timestamp G) 0)
                (<= (block.number G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.sig G) 330252341)
                (>= (msg.sender G) 0)
                (<= (block.timestamp G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (>= (msg.value G) 0)
                (<= (msg.sender G)
                    1461501637330902918203684832716283019655932542975)
                a!2
                (>= (tx.origin G) 0)
                (<= (msg.value G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!3
                (>= (tx.gasprice G) 0)
                (<= (tx.origin G)
                    1461501637330902918203684832716283019655932542975)
                a!4
                (<= (tx.gasprice G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (bytes_tuple_accessor_length (msg.data G)) 4)
                (= N 0)
                (>= (block.chainid G) 0))))
  (=> a!5 (interface_8_C_103_0 E F D B L A J)))) :named interface_8_C_103_0_to_interface_8_C_103_0))
(rule (! (block_38_function_f__94_103_0 P J F D G H O E L B N C K M A) :named block_38_function_f__94_103_0!))
(rule (! (=> (and (block_38_function_f__94_103_0 P J F D G H O E L B N C K M A)
         (= B H)
         (= C E)
         (= P 0)
         (= K L)
         (= N O))
    (block_39_f_93_103_0 P J F D G H O E L B N C K M A)) :named block_38_function_f__94_103_0_to_block_39_f_93_103_0))
(rule (! (=> (nondet_interface_9_C_103_0 N E F D H M C K B L A J)
    (nondet_call_41_0 N E F D H M C K B L A J)) :named nondet_call_41_0!))
(rule (! (let ((a!1 (and (block_39_f_93_103_0 X K F D G I S J N H R E M P A)
                (nondet_call_41_0 W K F D H R E M B Q C L)
                (= V R)
                (=> true
                    (and (>= V 0)
                         (<= V
                             1461501637330902918203684832716283019655932542975)))
                (= O V)
                (= T M)
                (=> true true)
                (= P 0)
                (> W 0)
                (= A 0))))
  (=> a!1 (summary_13_function_f__94_103_0 W K F D G I S J N B Q C L))) :named block_39_f_93_103_0_to_summary_13_function_f__94_103_0))
(rule (! (let ((a!1 (and (block_39_f_93_103_0 D1 L F D G I T K O H S J N Q C)
                (nondet_call_41_0 C1 L F D H S J N B R E M)
                (= Z S)
                (=> true
                    (and (>= Z 0)
                         (<= Z
                             1461501637330902918203684832716283019655932542975)))
                (= P Z)
                (= Y N)
                (=> true true)
                (= C1 0)
                (= X E1)
                (=> true
                    (and (>= X 0)
                         (<= X
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= A X)
                (= W A)
                (=> true
                    (and (>= W 0)
                         (<= W
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= V E)
                (=> true
                    (and (>= V 0)
                         (<= V
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= A1 (= W V))
                (not (= A1 true))
                (= Q 0)
                (= B1 1)
                (= C 0))))
  (=> a!1 (block_42_function_f__94_103_0 B1 L F D G I T K O B R E M P A))) :named block_39_f_93_103_0_to_block_42_function_f__94_103_0))
(rule (! (=> (block_42_function_f__94_103_0 P J F D G H O E L B N C K M A)
    (summary_13_function_f__94_103_0 P J F D G H O E L B N C K)) :named block_42_function_f__94_103_0!))
(rule (! (let ((a!1 (and (block_39_f_93_103_0 H1 L F D G I T K O H S J N Q C)
                (nondet_call_41_0 G1 L F D H S J N B R E M)
                (= C1 S)
                (=> true
                    (and (>= C1 0)
                         (<= C1
                             1461501637330902918203684832716283019655932542975)))
                (= P C1)
                (= B1 N)
                (=> true true)
                (= G1 0)
                (= Z I1)
                (=> true
                    (and (>= Z 0)
                         (<= Z
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= A Z)
                (= Y A)
                (=> true
                    (and (>= Y 0)
                         (<= Y
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= X E)
                (=> true
                    (and (>= X 0)
                         (<= X
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= F1 (= Y X))
                (= E1 G1)
                (= W P)
                (=> true
                    (and (>= W 0)
                         (<= W
                             1461501637330902918203684832716283019655932542975)))
                (= V R)
                (=> true
                    (and (>= V 0)
                         (<= V
                             1461501637330902918203684832716283019655932542975)))
                (= A1 (= W V))
                (not (= A1 true))
                (= Q 0)
                (= D1 2)
                (= C 0))))
  (=> a!1 (block_43_function_f__94_103_0 D1 L F D G I T K O B R E M P A))) :named block_39_f_93_103_0_to_block_43_function_f__94_103_0))
(rule (! (=> (block_43_function_f__94_103_0 P J F D G H O E L B N C K M A)
    (summary_13_function_f__94_103_0 P J F D G H O E L B N C K)) :named block_43_function_f__94_103_0!))
(rule (! (let ((a!1 (and (block_39_f_93_103_0 H1 L F D G I T K O H S J N Q C)
                (nondet_call_41_0 G1 L F D H S J N B R E M)
                (= C1 S)
                (=> true
                    (and (>= C1 0)
                         (<= C1
                             1461501637330902918203684832716283019655932542975)))
                (= P C1)
                (= B1 N)
                (=> true true)
                (= G1 0)
                (= Z I1)
                (=> true
                    (and (>= Z 0)
                         (<= Z
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= A Z)
                (= Y A)
                (=> true
                    (and (>= Y 0)
                         (<= Y
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= X E)
                (=> true
                    (and (>= X 0)
                         (<= X
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= F1 (= Y X))
                (= E1 G1)
                (= W P)
                (=> true
                    (and (>= W 0)
                         (<= W
                             1461501637330902918203684832716283019655932542975)))
                (= V R)
                (=> true
                    (and (>= V 0)
                         (<= V
                             1461501637330902918203684832716283019655932542975)))
                (= A1 (= W V))
                (= D1 E1)
                (= Q 0)
                (= C 0))))
  (=> a!1 (block_40_return_function_f__94_103_0 D1 L F D G I T K O B R E M P A))) :named block_39_f_93_103_0_to_block_40_return_function_f__94_103_0))
(rule (! (=> (block_40_return_function_f__94_103_0 P J F D G H O E L B N C K M A)
    (summary_13_function_f__94_103_0 P J F D G H O E L B N C K)) :named block_40_return_function_f__94_103_0_to_summary_13_function_f__94_103_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data G)) 0) 38))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data G)) 1) 18))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data G)) 2) 31))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data G)) 3) 240)))
(let ((a!5 (and (interface_8_C_103_0 E F D H M C K)
                (summary_13_function_f__94_103_0 N E F D G H M C K B L A J)
                (>= (block.coinbase G) 0)
                (<= (block.chainid G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.difficulty G) 0)
                (<= (block.coinbase G)
                    1461501637330902918203684832716283019655932542975)
                (>= (block.gaslimit G) 0)
                (<= (block.difficulty G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.number G) 0)
                (<= (block.gaslimit G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.value G) 0)
                (>= (block.timestamp G) 0)
                (<= (block.number G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.sig G) 638722032)
                (>= (msg.sender G) 0)
                (<= (block.timestamp G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (>= (msg.value G) 0)
                (<= (msg.sender G)
                    1461501637330902918203684832716283019655932542975)
                a!2
                (>= (tx.origin G) 0)
                (<= (msg.value G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!3
                (>= (tx.gasprice G) 0)
                (<= (tx.origin G)
                    1461501637330902918203684832716283019655932542975)
                a!4
                (<= (tx.gasprice G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (bytes_tuple_accessor_length (msg.data G)) 4)
                (= N 0)
                (>= (block.chainid G) 0))))
  (=> a!5 (interface_8_C_103_0 E F D B L A J)))) :named interface_8_C_103_0_to_interface_8_C_103_0!))
(rule (! (block_44_function_g__102_103_0 N E F D G H M C K B L A J O) :named block_44_function_g__102_103_0!))
(rule (! (=> (and (block_44_function_g__102_103_0 N E F D G H M C K B L A J O)
         (= B H)
         (= A C)
         (= N 0)
         (= J K)
         (= L M))
    (block_45_g_101_103_0 N E F D G H M C K B L A J O)) :named block_44_function_g__102_103_0_to_block_45_g_101_103_0))
(rule (! (let ((a!1 (and (block_45_g_101_103_0 O E F D G H M C K B L A J Q)
                (=> true
                    (and (>= N 0)
                         (<= N
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= P N)
                (= Q 0)
                (= N A))))
  (=> a!1 (block_46_return_function_g__102_103_0 O E F D G H M C K B L A J P))) :named block_45_g_101_103_0_to_block_46_return_function_g__102_103_0))
(rule (! (let ((a!1 (and (block_47_return_ghost_g_100_103_0 O E F D G H M C K B L A J P)
                (=> true
                    (and (>= N 0)
                         (<= N
                             115792089237316195423570985008687907853269984665640564039457584007913129639935)))
                (= P N)
                (= Q 0)
                (= N A))))
  (=> a!1 (block_46_return_function_g__102_103_0 O E F D G H M C K B L A J P))) :named block_47_return_ghost_g_100_103_0_to_block_46_return_function_g__102_103_0))
(rule (! (=> (block_46_return_function_g__102_103_0 N E F D G H M C K B L A J O)
    (summary_14_function_g__102_103_0 N E F D G H M C K B L A J O)) :named block_46_return_function_g__102_103_0_to_summary_14_function_g__102_103_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data G)) 0) 226))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data G)) 1) 23))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data G)) 2) 155))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data G)) 3) 142)))
(let ((a!5 (and (interface_8_C_103_0 E F D H M C K)
                (summary_14_function_g__102_103_0 N E F D G H M C K B L A J O)
                (>= (block.coinbase G) 0)
                (<= (block.chainid G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.difficulty G) 0)
                (<= (block.coinbase G)
                    1461501637330902918203684832716283019655932542975)
                (>= (block.gaslimit G) 0)
                (<= (block.difficulty G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.number G) 0)
                (<= (block.gaslimit G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.value G) 0)
                (>= (block.timestamp G) 0)
                (<= (block.number G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.sig G) 3793197966)
                (>= (msg.sender G) 0)
                (<= (block.timestamp G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (>= (msg.value G) 0)
                (<= (msg.sender G)
                    1461501637330902918203684832716283019655932542975)
                a!2
                (>= (tx.origin G) 0)
                (<= (msg.value G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!3
                (>= (tx.gasprice G) 0)
                (<= (tx.origin G)
                    1461501637330902918203684832716283019655932542975)
                a!4
                (<= (tx.gasprice G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (bytes_tuple_accessor_length (msg.data G)) 4)
                (= N 0)
                (>= (block.chainid G) 0))))
  (=> a!5 (interface_8_C_103_0 E F D B L A J)))) :named interface_8_C_103_0_to_interface_8_C_103_0!!))
(rule (! (block_48_constructor_58_103_0 N E F D G H M C K B L A J) :named block_48_constructor_58_103_0!))
(rule (! (=> (and (block_48_constructor_58_103_0 N E F D G H M C K B L A J)
         (= B H)
         (= A C)
         (= N 0)
         (= J K)
         (= L M))
    (block_49__57_103_0 N E F D G H M C K B L A J)) :named block_48_constructor_58_103_0_to_block_49__57_103_0))
(rule (! (let ((a!1 (and (block_49__57_103_0 R E F D G H N C K B M A J)
                (= Q M)
                (=> true
                    (and (>= Q 0)
                         (<= Q
                             1461501637330902918203684832716283019655932542975)))
                (= O P)
                (=> true
                    (and (>= O 0)
                         (<= O
                             1461501637330902918203684832716283019655932542975)))
                (= L O)
                (= P (msg.sender G))
                (=> true
                    (and (>= P 0)
                         (<= P
                             1461501637330902918203684832716283019655932542975))))))
  (=> a!1 (block_50_return_constructor_58_103_0 R E F D G H N C K B L A J))) :named block_49__57_103_0_to_block_50_return_constructor_58_103_0))
(rule (! (=> (block_50_return_constructor_58_103_0 N E F D G H M C K B L A J)
    (summary_11_constructor_58_103_0 N E F D G H M C K B L A J)) :named block_50_return_constructor_58_103_0_to_summary_11_constructor_58_103_0))
(rule (! (=> (and (= L M) (= B H) (= A C) (= N 0) (= J K))
    (contract_initializer_entry_52_C_103_0 N E F D G H M C K B L A J)) :named contract_initializer_entry_52_C_103_0!))
(rule (! (=> (contract_initializer_entry_52_C_103_0 N E F D G H M C K B L A J)
    (contract_initializer_after_init_53_C_103_0 N E F D G H M C K B L A J)) :named contract_initializer_entry_52_C_103_0_to_contract_initializer_after_init_53_C_103_0))
(rule (! (=> (and (contract_initializer_after_init_53_C_103_0 R J F D G I P E M H O C L)
         (summary_11_constructor_58_103_0 Q J F D G H O C L B N A K)
         (> Q 0))
    (contract_initializer_51_C_103_0 Q J F D G I P E M B N A K)) :named contract_initializer_after_init_53_C_103_0_to_contract_initializer_51_C_103_0))
(rule (! (=> (and (summary_11_constructor_58_103_0 Q J F D G H O C L B N A K)
         (contract_initializer_after_init_53_C_103_0 R J F D G I P E M H O C L)
         (= Q 0))
    (contract_initializer_51_C_103_0 Q J F D G I P E M B N A K)) :named contract_initializer_after_init_53_C_103_0_to_contract_initializer_51_C_103_0!))
(rule (! (let ((a!1 (and (= L M)
                (= B H)
                (= L 0)
                (= A C)
                (= N 0)
                (= A 0)
                (= J K)
                (= J 0)
                (= (select (isActive B) E) false))))
  (=> a!1 (implicit_constructor_entry_54_C_103_0 N E F D G H M C K B L A J))) :named implicit_constructor_entry_54_C_103_0!))
(rule (! (let ((a!1 (= B
              (state_type (balances H) (store (isActive H) E true) (storage H)))))
  (=> (and (implicit_constructor_entry_54_C_103_0 N E F D G I M C K H L A J)
           a!1)
      (implicit_constructor_entry_after_address_55_C_103_0
        N
        E
        F
        D
        G
        I
        M
        C
        K
        B
        L
        A
        J))) :named implicit_constructor_entry_54_C_103_0_to_implicit_constructor_entry_after_address_55_C_103_0))
(rule (! (=> (and (implicit_constructor_entry_after_address_55_C_103_0
           R
           J
           F
           D
           G
           I
           P
           E
           M
           H
           O
           C
           L)
         (contract_initializer_51_C_103_0 Q J F D G H O C L B N A K)
         (> Q 0))
    (summary_constructor_10_C_103_0 Q J F D G I P E M B N A K)) :named implicit_constructor_entry_after_address_55_C_103_0_to_summary_constructor_10_C_103_0))
(rule (! (let ((a!1 (storage_type (store (storage_C_103 (storage H))
                                J
                                (storage_C_103_type N A K))
                         (storage_Other_18 (storage H))
                         (storage_State_42 (storage H)))))
(let ((a!2 (and (contract_initializer_51_C_103_0 Q J F D G I O C L H N A K)
                (implicit_constructor_entry_after_address_55_C_103_0
                  R
                  J
                  F
                  D
                  G
                  U
                  P
                  E
                  M
                  I
                  O
                  C
                  L)
                (= B (state_type (balances H) (isActive H) a!1))
                (= Q 0))))
  (=> a!2 (summary_constructor_10_C_103_0 Q J F D G U P E M B N A K)))) :named implicit_constructor_entry_after_address_55_C_103_0_to_summary_constructor_10_C_103_0!))
(rule (! (=> (and (summary_constructor_10_C_103_0 N E F D G H M C K B L A J)
         (>= (block.coinbase G) 0)
         (<= (block.chainid G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.difficulty G) 0)
         (<= (block.coinbase G)
             1461501637330902918203684832716283019655932542975)
         (>= (block.gaslimit G) 0)
         (<= (block.difficulty G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.number G) 0)
         (<= (block.gaslimit G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (block.timestamp G) 0)
         (<= (block.number G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (msg.sender G) 0)
         (<= (block.timestamp G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (msg.value G) 0)
         (<= (msg.sender G) 1461501637330902918203684832716283019655932542975)
         (>= (tx.origin G) 0)
         (<= (msg.value G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (>= (tx.gasprice G) 0)
         (<= (tx.origin G) 1461501637330902918203684832716283019655932542975)
         (<= (tx.gasprice G)
             115792089237316195423570985008687907853269984665640564039457584007913129639935)
         (= (msg.value G) 0)
         (= N 0)
         (>= (block.chainid G) 0))
    (interface_8_C_103_0 E F D B L A J)) :named summary_constructor_10_C_103_0_to_interface_8_C_103_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data G)) 0) 38))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data G)) 1) 18))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data G)) 2) 31))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data G)) 3) 240)))
(let ((a!5 (and (interface_8_C_103_0 E F D H M C K)
                (summary_13_function_f__94_103_0 N E F D G H M C K B L A J)
                (>= (block.coinbase G) 0)
                (<= (block.chainid G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.difficulty G) 0)
                (<= (block.coinbase G)
                    1461501637330902918203684832716283019655932542975)
                (>= (block.gaslimit G) 0)
                (<= (block.difficulty G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.number G) 0)
                (<= (block.gaslimit G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.value G) 0)
                (>= (block.timestamp G) 0)
                (<= (block.number G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.sig G) 638722032)
                (>= (msg.sender G) 0)
                (<= (block.timestamp G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (>= (msg.value G) 0)
                (<= (msg.sender G)
                    1461501637330902918203684832716283019655932542975)
                a!2
                (>= (tx.origin G) 0)
                (<= (msg.value G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!3
                (>= (tx.gasprice G) 0)
                (<= (tx.origin G)
                    1461501637330902918203684832716283019655932542975)
                a!4
                (<= (tx.gasprice G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (bytes_tuple_accessor_length (msg.data G)) 4)
                (= N 1)
                (>= (block.chainid G) 0))))
  (=> a!5 error_target_3_0))) :named interface_8_C_103_0_to_error_target_3_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data G)) 0) 38))
      (a!2 (= (select (bytes_tuple_accessor_array (msg.data G)) 1) 18))
      (a!3 (= (select (bytes_tuple_accessor_array (msg.data G)) 2) 31))
      (a!4 (= (select (bytes_tuple_accessor_array (msg.data G)) 3) 240)))
(let ((a!5 (and (interface_8_C_103_0 E F D H M C K)
                (summary_13_function_f__94_103_0 N E F D G H M C K B L A J)
                (>= (block.coinbase G) 0)
                (<= (block.chainid G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.difficulty G) 0)
                (<= (block.coinbase G)
                    1461501637330902918203684832716283019655932542975)
                (>= (block.gaslimit G) 0)
                (<= (block.difficulty G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (block.number G) 0)
                (<= (block.gaslimit G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.value G) 0)
                (>= (block.timestamp G) 0)
                (<= (block.number G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (= (msg.sig G) 638722032)
                (>= (msg.sender G) 0)
                (<= (block.timestamp G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!1
                (>= (msg.value G) 0)
                (<= (msg.sender G)
                    1461501637330902918203684832716283019655932542975)
                a!2
                (>= (tx.origin G) 0)
                (<= (msg.value G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                a!3
                (>= (tx.gasprice G) 0)
                (<= (tx.origin G)
                    1461501637330902918203684832716283019655932542975)
                a!4
                (<= (tx.gasprice G)
                    115792089237316195423570985008687907853269984665640564039457584007913129639935)
                (>= (bytes_tuple_accessor_length (msg.data G)) 4)
                (= N 2)
                (>= (block.chainid G) 0))))
  (=> a!5 error_target_4_0))) :named interface_8_C_103_0_to_error_target_4_0))

(query error_target_4_0 :print-certificate true)