Skip to content

Instantly share code, notes, and snippets.

@leonardoalt

leonardoalt/a.smt2

Created June 23, 2021 17:18
Show Gist options
  • Save leonardoalt/2f44341789b6353ce300003ef7928902 to your computer and use it in GitHub Desktop.
Save leonardoalt/2f44341789b6353ce300003ef7928902 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
a.smt2
(declare-datatypes ((ecrecover_input_type 0)) (((ecrecover_input_type (hash Int) (v Int) (r Int) (s Int)))))
(declare-datatypes ((abi_type 0)) (((abi_type))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int))))))
(declare-datatypes ((bytes_tuple 0)) (((bytes_tuple (bytes_tuple_accessor_array (Array Int Int)) (bytes_tuple_accessor_length Int)))))
(declare-datatypes ((tx_type 0)) (((tx_type (block.chainid Int) (block.coinbase Int) (block.difficulty Int) (block.gaslimit Int) (block.number Int) (block.timestamp Int) (blockhash (Array Int Int)) (msg.data bytes_tuple) (msg.sender Int) (msg.sig Int) (msg.value Int) (tx.gasprice Int) (tx.origin Int)))))
(declare-datatypes ((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_7_exp_38_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel contract_initializer_entry_39_C_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel summary_23_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_17_if_true_exp_36_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel summary_3_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel implicit_constructor_entry_after_address_42_C_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel block_12_return_ghost_exp_13_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel interface_0_C_104_0 (Int abi_type crypto_type state_type))
(declare-rel summary_constructor_2_C_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel error_target_13_0 ())
(declare-rel block_10_if_true_exp_13_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel summary_34_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_13_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_15_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel summary_30_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_29_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel block_11_exp_38_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel summary_5_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel block_20_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_18_exp_38_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_22_return_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_33_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel block_19_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_21_g_53_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel summary_28_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel summary_32_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_8_return_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_37_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel nondet_interface_1_C_104_0 (Int Int abi_type crypto_type state_type state_type))
(declare-rel block_26_f_102_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel block_27_return_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel contract_initializer_after_init_40_C_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel error_target_11_0 ())
(declare-rel block_16_if_header_exp_37_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel summary_36_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel error_target_12_0 ())
(declare-rel block_24_return_ghost_g_52_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_6_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_35_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel summary_14_function_exp__39_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_25_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel error_target_10_0 ())
(declare-rel error_target_14_0 ())
(declare-rel implicit_constructor_entry_41_C_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel block_31_function_f__103_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel contract_initializer_38_C_104_0 (Int Int abi_type crypto_type tx_type state_type state_type))
(declare-rel summary_4_function_g__54_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-rel block_9_if_header_exp_14_104_0 (Int Int abi_type crypto_type tx_type state_type Int Int state_type Int Int Int))
(declare-var A Int)
(declare-var B state_type)
(declare-var C Int)
(declare-var D crypto_type)
(declare-var E abi_type)
(declare-var F tx_type)
(declare-var G state_type)
(declare-var H state_type)
(declare-var I Int)
(declare-var J Int)
(declare-var K Int)
(declare-var L Int)
(declare-var M Int)
(declare-var N Bool)
(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 Int)
(declare-var V Int)
(declare-var W Int)
(declare-var X Int)
(declare-var Y Int)
(declare-var Z Int)
(declare-var A1 Int)
(declare-var B1 Int)
(declare-var C1 Int)
(declare-var D1 Int)
(declare-var E1 Int)
(declare-var F1 Int)
(declare-var G1 Int)
(declare-var H1 Int)
(declare-var I1 Bool)
(declare-var J1 Bool)
(declare-var K1 Int)
(declare-var L1 Int)
(declare-var M1 Int)
(declare-var N1 Int)
(declare-var O1 Int)
(declare-var P1 Int)
(declare-var Q1 Int)
(declare-var R1 Int)
(declare-var S1 Bool)
(declare-var T1 Int)
(declare-var U1 Int)
(declare-var V1 Int)
(declare-var W1 Int)
(declare-var X1 Int)
(declare-var Y1 Int)
(declare-var Z1 Int)
(declare-var A2 Int)
(declare-var B2 Int)
(declare-var C2 Bool)
(declare-var D2 Int)
(declare-var E2 Int)
(declare-var F2 Int)
(declare-var G2 Bool)
(declare-var H2 Int)
(declare-var I2 Int)
(declare-var J2 Int)
(declare-var K2 Bool)
(declare-var L2 Int)
(declare-var M2 Int)
(declare-var N2 Int)
(declare-var O2 Int)
(declare-var P2 Int)
(declare-var Q2 Int)
(declare-var R2 Int)
(declare-var S2 Int)
(declare-var T2 Int)
(declare-var U2 Int)
(declare-var V2 Int)
(declare-var W2 Int)
(declare-var X2 Int)
(declare-var Y2 Int)
(declare-var Z2 Int)
(declare-var A3 Int)
(declare-var B3 Int)
(declare-var C3 Int)
(declare-var D3 Int)
(declare-var E3 Int)
(declare-var F3 Int)
(declare-var G3 Int)
(declare-var H3 Int)
(declare-var I3 Int)
(declare-var J3 Int)
(declare-var K3 Int)
(declare-var L3 Int)
(declare-var M3 Int)
(declare-var N3 Int)
(declare-var O3 Int)
(declare-var P3 Int)
(declare-var Q3 Int)
(declare-var R3 Int)
(declare-var S3 Int)
(declare-var T3 Int)
(declare-var U3 Int)
(declare-var V3 Int)
(declare-var W3 Int)
(declare-var X3 Int)
(declare-var Y3 Int)
(declare-var Z3 Int)
(declare-var A4 Int)
(declare-var B4 Int)
(declare-var C4 Int)
(declare-var D4 Int)
(rule (! (=> (= C 0) (nondet_interface_1_C_104_0 C A E D B B)) :named base_nondet))
(rule (! (=> (and (summary_5_function_f__103_104_0 C A E D F G B)
(nondet_interface_1_C_104_0 I A E D H G)
(= I 0))
(nondet_interface_1_C_104_0 C A E D H B)) :named nondet_interface_1_C_104_0_to_nondet_interface_1_C_104_0))
(rule (! (block_6_function_exp__39_104_0 K A E D F G M J B L I C) :named block_6_function_exp__39_104_0!))
(rule (! (=> (and (block_6_function_exp__39_104_0 K A E D F G M J B L I C)
(= L M)
(= K 0)
(= I J)
(= B G))
(block_7_exp_38_104_0 K A E D F G M J B L I C)) :named block_6_function_exp__39_104_0_to_block_7_exp_38_104_0))
(rule (! (=> (and (block_7_exp_38_104_0 K A E D F G M J B L I C)
(>= L 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= C 0)
(<= L
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= I 0))
(block_9_if_header_exp_14_104_0 K A E D F G M J B L I C)) :named block_7_exp_38_104_0_to_block_9_if_header_exp_14_104_0))
(rule (! (let ((a!1 (and (block_9_if_header_exp_14_104_0 M A E D F G P L B O K C)
(= J 0)
(=> true true)
(= N (= I J))
(= I K)
(= N true)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935))))))
(=> a!1 (block_10_if_true_exp_13_104_0 M A E D F G P L B O K C))) :named block_9_if_header_exp_14_104_0_to_block_10_if_true_exp_13_104_0))
(rule (! (let ((a!1 (and (block_9_if_header_exp_14_104_0 M A E D F G P L B O K C)
(= J 0)
(=> true true)
(= N (= I J))
(= I K)
(not (= N true))
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935))))))
(=> a!1 (block_11_exp_38_104_0 M A E D F G P L B O K C))) :named block_9_if_header_exp_14_104_0_to_block_11_exp_38_104_0))
(rule (! (=> (and (block_10_if_true_exp_13_104_0 M A E D F G P L B O K I)
(= C J)
(= J 1)
(=> true true))
(block_8_return_function_exp__39_104_0 M A E D F G P L B O K C)) :named block_10_if_true_exp_13_104_0_to_block_8_return_function_exp__39_104_0))
(rule (! (=> (and (block_12_return_ghost_exp_13_104_0 L A E D F G O K B M J C)
(= C I)
(= I 1)
(=> true true))
(block_11_exp_38_104_0 L A E D F G O K B M J C)) :named block_12_return_ghost_exp_13_104_0_to_block_11_exp_38_104_0))
(rule (! (let ((a!1 (and (block_11_exp_38_104_0 P A E D F G R M B Q L C)
(= J L)
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= I 2)
(=> true true)
(= I 0)
(= K Q)
(= O 1)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935))))))
(=> a!1 (block_13_function_exp__39_104_0 O A E D F G R M B Q L C))) :named block_11_exp_38_104_0_to_block_13_function_exp__39_104_0))
(rule (! (=> (block_13_function_exp__39_104_0 K A E D F G M J B L I C)
(summary_3_function_exp__39_104_0 K A E D F G M J B L I C)) :named block_13_function_exp__39_104_0!))
(rule (! (=> (summary_3_function_exp__39_104_0 K A E D F G M J B L I C)
(summary_14_function_exp__39_104_0 K A E D F G M J B L I C)) :named summary_14_function_exp__39_104_0!))
(rule (! (let ((a!1 (and (block_11_exp_38_104_0 U A E D F G Y R B X Q J)
(summary_14_function_exp__39_104_0 S A E D F B O K B W P I)
(=> true
(and (>= O 0)
(<= O
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= M Q)
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= L 2)
(=> true true)
(= T U)
(= (+ (* V L) C) M)
(or (= L 0) (< C L))
(= K (ite (= L 0) 0 V))
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= O X)
(> S 0)
(<= 0 C))))
(=> a!1 (summary_3_function_exp__39_104_0 S A E D F G Y R B W P I))) :named block_11_exp_38_104_0_to_summary_3_function_exp__39_104_0))
(rule (! (let ((a!1 (and (block_11_exp_38_104_0 B1 A E D F G F1 X B E1 W K)
(summary_14_function_exp__39_104_0 Z A E D F B T Q B D1 V J)
(=> true
(and (>= T 0)
(<= T
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= S W)
(=> true
(and (>= S 0)
(<= S
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= R 2)
(=> true true)
(= A1 B1)
(= (+ (* C1 R) C) S)
(or (= R 0) (< C R))
(= Q (ite (= R 0) 0 C1))
(=> true
(and (>= Q 0)
(<= Q
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Z 0)
(= P J)
(=> true
(and (>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= U J)
(=> true
(and (>= U 0)
(<= U
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= O P)
(=> true
(and (>= O 0)
(<= O
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= I O)
(= L I)
(=> true
(and (>= L 0)
(<= L
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= M I)
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(> (* I L)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= T E1)
(= Y 3)
(<= 0 C))))
(=> a!1 (block_15_function_exp__39_104_0 Y A E D F G F1 X B D1 V I))) :named block_11_exp_38_104_0_to_block_15_function_exp__39_104_0))
(rule (! (=> (block_15_function_exp__39_104_0 K A E D F G M J B L I C)
(summary_3_function_exp__39_104_0 K A E D F G M J B L I C)) :named block_15_function_exp__39_104_0!))
(rule (! (let ((a!1 (and (block_11_exp_38_104_0 D1 A E D F G H1 Z B G1 Y L)
(summary_14_function_exp__39_104_0 B1 A E D F B V S B F1 X K)
(=> true
(and (>= V 0)
(<= V
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= U Y)
(=> true
(and (>= U 0)
(<= U
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= T 2)
(=> true true)
(= C1 D1)
(= (+ (* E1 T) C) U)
(or (= T 0) (< C T))
(= S (ite (= T 0) 0 E1))
(=> true
(and (>= S 0)
(<= S
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= B1 0)
(= R K)
(=> true
(and (>= R 0)
(<= R
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= W K)
(=> true
(and (>= W 0)
(<= W
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Q R)
(=> true
(and (>= Q 0)
(<= Q
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= J Q)
(= O J)
(=> true
(and (>= O 0)
(<= O
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= P J)
(=> true
(and (>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= A1 B1)
(= M (* J O))
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= I M)
(= V G1)
(<= 0 C))))
(=> a!1 (block_16_if_header_exp_37_104_0 A1 A E D F G H1 Z B F1 X I))) :named block_11_exp_38_104_0_to_block_16_if_header_exp_37_104_0))
(rule (! (let ((a!1 (= J (bv2int (bvand ((_ int2bv 256) L) ((_ int2bv 256) K))))))
(let ((a!2 (and (block_16_if_header_exp_37_104_0 P A E D F G R O B Q M C)
(= K 1)
(=> true true)
a!1
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= I 1)
(=> true true)
(= N (= J I))
(= L M)
(= N true)
(=> true
(and (>= L 0)
(<= L
115792089237316195423570985008687907853269984665640564039457584007913129639935))))))
(=> a!2 (block_17_if_true_exp_36_104_0 P A E D F G R O B Q M C)))) :named block_16_if_header_exp_37_104_0_to_block_17_if_true_exp_36_104_0))
(rule (! (let ((a!1 (= J (bv2int (bvand ((_ int2bv 256) L) ((_ int2bv 256) K))))))
(let ((a!2 (and (block_16_if_header_exp_37_104_0 P A E D F G R O B Q M C)
(= K 1)
(=> true true)
a!1
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= I 1)
(=> true true)
(= N (= J I))
(= L M)
(not (= N true))
(=> true
(and (>= L 0)
(<= L
115792089237316195423570985008687907853269984665640564039457584007913129639935))))))
(=> a!2 (block_18_exp_38_104_0 P A E D F G R O B Q M C)))) :named block_16_if_header_exp_37_104_0_to_block_18_exp_38_104_0))
(rule (! (let ((a!1 (and (block_17_if_true_exp_36_104_0 O A E D F G Q L B P K C)
(= J C)
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(> (* C I)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= I P)
(= M 4)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935))))))
(=> a!1 (block_19_function_exp__39_104_0 M A E D F G Q L B P K C))) :named block_17_if_true_exp_36_104_0_to_block_19_function_exp__39_104_0))
(rule (! (=> (block_19_function_exp__39_104_0 K A E D F G M J B L I C)
(summary_3_function_exp__39_104_0 K A E D F G M J B L I C)) :named block_19_function_exp__39_104_0!))
(rule (! (let ((a!1 (and (block_17_if_true_exp_36_104_0 Q A E D F G S O B R M I)
(= L I)
(=> true
(and (>= L 0)
(<= L
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= P Q)
(= J (* I K))
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= C J)
(= K R)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935))))))
(=> a!1 (block_18_exp_38_104_0 P A E D F G S O B R M C))) :named block_17_if_true_exp_36_104_0_to_block_18_exp_38_104_0))
(rule (! (=> (block_18_exp_38_104_0 K A E D F G M J B L I C)
(block_8_return_function_exp__39_104_0 K A E D F G M J B L I C)) :named block_18_exp_38_104_0_to_block_8_return_function_exp__39_104_0))
(rule (! (=> (block_8_return_function_exp__39_104_0 K A E D F G M J B L I C)
(summary_3_function_exp__39_104_0 K A E D F G M J B L I C)) :named block_8_return_function_exp__39_104_0_to_summary_3_function_exp__39_104_0))
(rule (! (block_20_function_g__54_104_0 J A E D F G L I B K C M) :named block_20_function_g__54_104_0!))
(rule (! (=> (and (block_20_function_g__54_104_0 J A E D F G L I B K C M)
(= K L)
(= J 0)
(= C I)
(= B G))
(block_21_g_53_104_0 J A E D F G L I B K C M)) :named block_20_function_g__54_104_0_to_block_21_g_53_104_0))
(rule (! (=> (summary_3_function_exp__39_104_0 K A E D F G M J B L I C)
(summary_23_function_exp__39_104_0 K A E D F G M J B L I C)) :named summary_23_function_exp__39_104_0!))
(rule (! (let ((a!1 (and (block_21_g_53_104_0 P A E D F G R M B Q L T)
(summary_23_function_exp__39_104_0 O A E D F B J I B S K C)
(>= Q 0)
(<= L
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= T 0)
(= J Q)
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= I L)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(<= Q
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(> O 0)
(>= L 0))))
(=> a!1 (summary_4_function_g__54_104_0 O A E D F G R M B Q L T))) :named block_21_g_53_104_0_to_summary_4_function_g__54_104_0))
(rule (! (let ((a!1 (and (block_21_g_53_104_0 Q A E D F G S O B R M V)
(summary_23_function_exp__39_104_0 P A E D F B K J B T L C)
(>= R 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= V 0)
(= K R)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= J M)
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= P 0)
(= I C)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= U I)
(<= R
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= M 0))))
(=> a!1 (block_22_return_function_g__54_104_0 P A E D F G S O B R M U))) :named block_21_g_53_104_0_to_block_22_return_function_g__54_104_0))
(rule (! (let ((a!1 (and (block_24_return_ghost_g_52_104_0 P A E D F G R O B Q M T)
(summary_23_function_exp__39_104_0 P A E D F B K J B S L C)
(>= Q 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= U 0)
(= K Q)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= J M)
(=> true
(and (>= J 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= P 0)
(= I C)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= T I)
(<= Q
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= M 0))))
(=> a!1 (block_22_return_function_g__54_104_0 P A E D F G R O B Q M T))) :named block_24_return_ghost_g_52_104_0_to_block_22_return_function_g__54_104_0))
(rule (! (=> (block_22_return_function_g__54_104_0 J A E D F G L I B K C M)
(summary_4_function_g__54_104_0 J A E D F G L I B K C M)) :named block_22_return_function_g__54_104_0_to_summary_4_function_g__54_104_0))
(rule (! (block_25_function_f__103_104_0 C A E D F G B) :named block_25_function_f__103_104_0!))
(rule (! (=> (and (block_25_function_f__103_104_0 C A E D F G B) (= C 0) (= B G))
(block_26_f_102_104_0 C A E D F G B)) :named block_25_function_f__103_104_0_to_block_26_f_102_104_0))
(rule (! (=> (summary_4_function_g__54_104_0 J A E D F G L I B K C M)
(summary_28_function_g__54_104_0 J A E D F G L I B K C M)) :named summary_28_function_g__54_104_0!))
(rule (! (=> (and (block_26_f_102_104_0 L A E D F G B)
(summary_28_function_g__54_104_0 K A E D F B I C B M J O)
(= C 0)
(=> true true)
(= I 0)
(> K 0)
(=> true true))
(summary_5_function_f__103_104_0 K A E D F G B)) :named block_26_f_102_104_0_to_summary_5_function_f__103_104_0))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 P A E D F G B)
(summary_28_function_g__54_104_0 O A E D F B K J B Q L R)
(= J 0)
(=> true true)
(= O 0)
(= I R)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= C 1)
(=> true true)
(= N (= I C))
(not (= N true))
(= K 0)
(= M 5)
(=> true true))))
(=> a!1 (block_29_function_f__103_104_0 M A E D F G B))) :named block_26_f_102_104_0_to_block_29_function_f__103_104_0))
(rule (! (=> (block_29_function_f__103_104_0 C A E D F G B)
(summary_5_function_f__103_104_0 C A E D F G B)) :named block_29_function_f__103_104_0!))
(rule (! (=> (summary_4_function_g__54_104_0 J A E D F G L I B K C M)
(summary_30_function_g__54_104_0 J A E D F G L I B K C M)) :named summary_30_function_g__54_104_0!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 T A E D F G B)
(summary_30_function_g__54_104_0 Q A E D F B I C B U O W)
(summary_28_function_g__54_104_0 S A E D F B M L B V P X)
(= L 0)
(=> true true)
(= S 0)
(= K X)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= J 1)
(=> true true)
(= N (= K J))
(= R S)
(= I 0)
(=> true true)
(= C 1)
(=> true true)
(= M 0)
(> Q 0)
(=> true true))))
(=> a!1 (summary_5_function_f__103_104_0 Q A E D F G B))) :named block_26_f_102_104_0_to_summary_5_function_f__103_104_0!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 W A E D F G B)
(summary_30_function_g__54_104_0 T A E D F B K J B X Q Z)
(summary_28_function_g__54_104_0 V A E D F B P O B Y R A1)
(= O 0)
(=> true true)
(= V 0)
(= M A1)
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= L 1)
(=> true true)
(= I1 (= M L))
(= U V)
(= K 0)
(=> true true)
(= J 1)
(=> true true)
(= T 0)
(= I Z)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= C 0)
(=> true true)
(= N (= I C))
(not (= N true))
(= P 0)
(= S 6)
(=> true true))))
(=> a!1 (block_31_function_f__103_104_0 S A E D F G B))) :named block_26_f_102_104_0_to_block_31_function_f__103_104_0))
(rule (! (=> (block_31_function_f__103_104_0 C A E D F G B)
(summary_5_function_f__103_104_0 C A E D F G B)) :named block_31_function_f__103_104_0!))
(rule (! (=> (summary_4_function_g__54_104_0 J A E D F G L I B K C M)
(summary_32_function_g__54_104_0 J A E D F G L I B K C M)) :named summary_32_function_g__54_104_0!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 A1 A E D F G B)
(summary_32_function_g__54_104_0 V A E D F B I C B B1 S E1)
(summary_30_function_g__54_104_0 X A E D F B M L B C1 T F1)
(summary_28_function_g__54_104_0 Z A E D F B R Q B D1 U G1)
(= Q 0)
(=> true true)
(= Z 0)
(= P G1)
(=> true
(and (>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= O 1)
(=> true true)
(= I1 (= P O))
(= Y Z)
(= M 0)
(=> true true)
(= L 1)
(=> true true)
(= X 0)
(= K F1)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= J 0)
(=> true true)
(= N (= K J))
(= W X)
(= I 1)
(=> true true)
(= C 0)
(=> true true)
(= R 0)
(> V 0)
(=> true true))))
(=> a!1 (summary_5_function_f__103_104_0 V A E D F G B))) :named block_26_f_102_104_0_to_summary_5_function_f__103_104_0!!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 D1 A E D F G B)
(summary_32_function_g__54_104_0 Y A E D F B K J B E1 U H1)
(summary_30_function_g__54_104_0 A1 A E D F B P O B F1 V K1)
(summary_28_function_g__54_104_0 C1 A E D F B T S B G1 W L1)
(= S 0)
(=> true true)
(= C1 0)
(= R L1)
(=> true
(and (>= R 0)
(<= R
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Q 1)
(=> true true)
(= J1 (= R Q))
(= B1 C1)
(= P 0)
(=> true true)
(= O 1)
(=> true true)
(= A1 0)
(= M K1)
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= L 0)
(=> true true)
(= I1 (= M L))
(= Z A1)
(= K 1)
(=> true true)
(= J 0)
(=> true true)
(= Y 0)
(= I H1)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= C 1)
(=> true true)
(= N (= I C))
(not (= N true))
(= T 0)
(= X 7)
(=> true true))))
(=> a!1 (block_33_function_f__103_104_0 X A E D F G B))) :named block_26_f_102_104_0_to_block_33_function_f__103_104_0))
(rule (! (=> (block_33_function_f__103_104_0 C A E D F G B)
(summary_5_function_f__103_104_0 C A E D F G B)) :named block_33_function_f__103_104_0!))
(rule (! (=> (summary_4_function_g__54_104_0 J A E D F G L I B K C M)
(summary_34_function_g__54_104_0 J A E D F G L I B K C M)) :named summary_34_function_g__54_104_0!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 H1 A E D F G B)
(summary_34_function_g__54_104_0 A1 A E D F B I C B K1 W O1)
(summary_32_function_g__54_104_0 C1 A E D F B M L B L1 X P1)
(summary_30_function_g__54_104_0 E1 A E D F B R Q B M1 Y Q1)
(summary_28_function_g__54_104_0 G1 A E D F B V U B N1 Z R1)
(= U 0)
(=> true true)
(= G1 0)
(= T R1)
(=> true
(and (>= T 0)
(<= T
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= S 1)
(=> true true)
(= J1 (= T S))
(= F1 G1)
(= R 0)
(=> true true)
(= Q 1)
(=> true true)
(= E1 0)
(= P Q1)
(=> true
(and (>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= O 0)
(=> true true)
(= I1 (= P O))
(= D1 E1)
(= M 1)
(=> true true)
(= L 0)
(=> true true)
(= C1 0)
(= K P1)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= J 1)
(=> true true)
(= N (= K J))
(= B1 C1)
(= I 2)
(=> true true)
(= C 3)
(=> true true)
(= V 0)
(> A1 0)
(=> true true))))
(=> a!1 (summary_5_function_f__103_104_0 A1 A E D F G B))) :named block_26_f_102_104_0_to_summary_5_function_f__103_104_0!!!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 M1 A E D F G B)
(summary_34_function_g__54_104_0 D1 A E D F B K J B N1 Y R1)
(summary_32_function_g__54_104_0 F1 A E D F B P O B O1 Z T1)
(summary_30_function_g__54_104_0 H1 A E D F B T S B P1 A1 U1)
(summary_28_function_g__54_104_0 L1 A E D F B X W B Q1 B1 V1)
(= W 0)
(=> true true)
(= L1 0)
(= V V1)
(=> true
(and (>= V 0)
(<= V
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= U 1)
(=> true true)
(= S1 (= V U))
(= K1 L1)
(= T 0)
(=> true true)
(= S 1)
(=> true true)
(= H1 0)
(= R U1)
(=> true
(and (>= R 0)
(<= R
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Q 0)
(=> true true)
(= J1 (= R Q))
(= G1 H1)
(= P 1)
(=> true true)
(= O 0)
(=> true true)
(= F1 0)
(= M T1)
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= L 1)
(=> true true)
(= I1 (= M L))
(= E1 F1)
(= K 2)
(=> true true)
(= J 3)
(=> true true)
(= D1 0)
(= I R1)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= C 8)
(=> true true)
(= N (= I C))
(not (= N true))
(= X 0)
(= C1 8)
(=> true true))))
(=> a!1 (block_35_function_f__103_104_0 C1 A E D F G B))) :named block_26_f_102_104_0_to_block_35_function_f__103_104_0))
(rule (! (=> (block_35_function_f__103_104_0 C A E D F G B)
(summary_5_function_f__103_104_0 C A E D F G B)) :named block_35_function_f__103_104_0!))
(rule (! (=> (summary_4_function_g__54_104_0 J A E D F G L I B K C M)
(summary_36_function_g__54_104_0 J A E D F G L I B K C M)) :named summary_36_function_g__54_104_0!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 Q1 A E D F G B)
(summary_36_function_g__54_104_0 F1 A E D F B I C B R1 A1 X1)
(summary_34_function_g__54_104_0 H1 A E D F B M L B T1 B1 Y1)
(summary_32_function_g__54_104_0 L1 A E D F B R Q B U1 C1 Z1)
(summary_30_function_g__54_104_0 N1 A E D F B V U B V1 D1 A2)
(summary_28_function_g__54_104_0 P1 A E D F B Z Y B W1 E1 B2)
(= Y 0)
(=> true true)
(= P1 0)
(= X B2)
(=> true
(and (>= X 0)
(<= X
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= W 1)
(=> true true)
(= S1 (= X W))
(= O1 P1)
(= V 0)
(=> true true)
(= U 1)
(=> true true)
(= N1 0)
(= T A2)
(=> true
(and (>= T 0)
(<= T
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= S 0)
(=> true true)
(= J1 (= T S))
(= M1 N1)
(= R 1)
(=> true true)
(= Q 0)
(=> true true)
(= L1 0)
(= P Z1)
(=> true
(and (>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= O 1)
(=> true true)
(= I1 (= P O))
(= K1 L1)
(= M 2)
(=> true true)
(= L 3)
(=> true true)
(= H1 0)
(= K Y1)
(=> true
(and (>= K 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= J 8)
(=> true true)
(= N (= K J))
(= G1 H1)
(= I 3)
(=> true true)
(= C 10)
(=> true true)
(= Z 0)
(> F1 0)
(=> true true))))
(=> a!1 (summary_5_function_f__103_104_0 F1 A E D F G B))) :named block_26_f_102_104_0_to_summary_5_function_f__103_104_0!!!!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 U1 A E D F G B)
(summary_36_function_g__54_104_0 H1 A E D F B K J B V1 C1 A2)
(summary_34_function_g__54_104_0 L1 A E D F B P O B W1 D1 B2)
(summary_32_function_g__54_104_0 N1 A E D F B T S B X1 E1 D2)
(summary_30_function_g__54_104_0 P1 A E D F B X W B Y1 F1 E2)
(summary_28_function_g__54_104_0 T1 A E D F B B1 A1 B Z1 G1 F2)
(= A1 0)
(=> true true)
(= T1 0)
(= Z F2)
(=> true
(and (>= Z 0)
(<= Z
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Y 1)
(=> true true)
(= C2 (= Z Y))
(= Q1 T1)
(= X 0)
(=> true true)
(= W 1)
(=> true true)
(= P1 0)
(= V E2)
(=> true
(and (>= V 0)
(<= V
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= U 0)
(=> true true)
(= S1 (= V U))
(= O1 P1)
(= T 1)
(=> true true)
(= S 0)
(=> true true)
(= N1 0)
(= R D2)
(=> true
(and (>= R 0)
(<= R
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Q 1)
(=> true true)
(= J1 (= R Q))
(= M1 N1)
(= P 2)
(=> true true)
(= O 3)
(=> true true)
(= L1 0)
(= M B2)
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= L 8)
(=> true true)
(= I1 (= M L))
(= K1 L1)
(= K 3)
(=> true true)
(= J 10)
(=> true true)
(= H1 0)
(= I A2)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= C 59049)
(=> true true)
(= N (= I C))
(not (= N true))
(= B1 0)
(= R1 9)
(=> true true))))
(=> a!1 (block_37_function_f__103_104_0 R1 A E D F G B))) :named block_26_f_102_104_0_to_block_37_function_f__103_104_0))
(rule (! (=> (block_37_function_f__103_104_0 C A E D F G B)
(summary_5_function_f__103_104_0 C A E D F G B)) :named block_37_function_f__103_104_0!))
(rule (! (let ((a!1 (and (block_26_f_102_104_0 U1 A E D F G B)
(summary_36_function_g__54_104_0 H1 A E D F B K J B V1 C1 A2)
(summary_34_function_g__54_104_0 L1 A E D F B P O B W1 D1 B2)
(summary_32_function_g__54_104_0 N1 A E D F B T S B X1 E1 D2)
(summary_30_function_g__54_104_0 P1 A E D F B X W B Y1 F1 E2)
(summary_28_function_g__54_104_0 T1 A E D F B B1 A1 B Z1 G1 F2)
(= A1 0)
(=> true true)
(= T1 0)
(= Z F2)
(=> true
(and (>= Z 0)
(<= Z
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Y 1)
(=> true true)
(= C2 (= Z Y))
(= Q1 T1)
(= X 0)
(=> true true)
(= W 1)
(=> true true)
(= P1 0)
(= V E2)
(=> true
(and (>= V 0)
(<= V
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= U 0)
(=> true true)
(= S1 (= V U))
(= O1 P1)
(= T 1)
(=> true true)
(= S 0)
(=> true true)
(= N1 0)
(= R D2)
(=> true
(and (>= R 0)
(<= R
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= Q 1)
(=> true true)
(= J1 (= R Q))
(= M1 N1)
(= P 2)
(=> true true)
(= O 3)
(=> true true)
(= L1 0)
(= M B2)
(=> true
(and (>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= L 8)
(=> true true)
(= I1 (= M L))
(= K1 L1)
(= K 3)
(=> true true)
(= J 10)
(=> true true)
(= H1 0)
(= I A2)
(=> true
(and (>= I 0)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)))
(= C 59049)
(=> true true)
(= N (= I C))
(= R1 H1)
(= B1 0)
(=> true true))))
(=> a!1 (block_27_return_function_f__103_104_0 R1 A E D F G B))) :named block_26_f_102_104_0_to_block_27_return_function_f__103_104_0))
(rule (! (=> (block_27_return_function_f__103_104_0 C A E D F G B)
(summary_5_function_f__103_104_0 C A E D F G B)) :named block_27_return_function_f__103_104_0_to_summary_5_function_f__103_104_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data F)) 0) 38))
(a!2 (= (select (bytes_tuple_accessor_array (msg.data F)) 1) 18))
(a!3 (= (select (bytes_tuple_accessor_array (msg.data F)) 2) 31))
(a!4 (= (select (bytes_tuple_accessor_array (msg.data F)) 3) 240)))
(let ((a!5 (and (interface_0_C_104_0 A E D G)
(summary_5_function_f__103_104_0 C A E D F G B)
(>= (block.coinbase F) 0)
(<= (block.chainid F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.difficulty F) 0)
(<= (block.coinbase F)
1461501637330902918203684832716283019655932542975)
(>= (block.gaslimit F) 0)
(<= (block.difficulty F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.number F) 0)
(<= (block.gaslimit F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value F) 0)
(>= (block.timestamp F) 0)
(<= (block.number F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.sig F) 638722032)
(>= (msg.sender F) 0)
(<= (block.timestamp F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!1
(>= (msg.value F) 0)
(<= (msg.sender F)
1461501637330902918203684832716283019655932542975)
a!2
(>= (tx.origin F) 0)
(<= (msg.value F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!3
(>= (tx.gasprice F) 0)
(<= (tx.origin F)
1461501637330902918203684832716283019655932542975)
a!4
(<= (tx.gasprice F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (bytes_tuple_accessor_length (msg.data F)) 4)
(= C 0)
(>= (block.chainid F) 0))))
(=> a!5 (interface_0_C_104_0 A E D B)))) :named interface_0_C_104_0_to_interface_0_C_104_0))
(rule (! (=> (and (= B G) (= C 0)) (contract_initializer_entry_39_C_104_0 C A E D F G B)) :named contract_initializer_entry_39_C_104_0!))
(rule (! (=> (contract_initializer_entry_39_C_104_0 C A E D F G B)
(contract_initializer_after_init_40_C_104_0 C A E D F G B)) :named contract_initializer_entry_39_C_104_0_to_contract_initializer_after_init_40_C_104_0))
(rule (! (=> (contract_initializer_after_init_40_C_104_0 C A E D F G B)
(contract_initializer_38_C_104_0 C A E D F G B)) :named contract_initializer_after_init_40_C_104_0_to_contract_initializer_38_C_104_0))
(rule (! (=> (and (= B G) (= C 0)) (implicit_constructor_entry_41_C_104_0 C A E D F G B)) :named implicit_constructor_entry_41_C_104_0!))
(rule (! (=> (implicit_constructor_entry_41_C_104_0 C A E D F G B)
(implicit_constructor_entry_after_address_42_C_104_0 C A E D F G B)) :named implicit_constructor_entry_41_C_104_0_to_implicit_constructor_entry_after_address_42_C_104_0))
(rule (! (=> (and (implicit_constructor_entry_after_address_42_C_104_0 I A E D F H G)
(contract_initializer_38_C_104_0 C A E D F G B)
(> C 0))
(summary_constructor_2_C_104_0 C A E D F H B)) :named implicit_constructor_entry_after_address_42_C_104_0_to_summary_constructor_2_C_104_0))
(rule (! (=> (and (contract_initializer_38_C_104_0 C A E D F G B)
(implicit_constructor_entry_after_address_42_C_104_0 I A E D F H G)
(= C 0))
(summary_constructor_2_C_104_0 C A E D F H B)) :named implicit_constructor_entry_after_address_42_C_104_0_to_summary_constructor_2_C_104_0!))
(rule (! (=> (and (summary_constructor_2_C_104_0 C A E D F G B)
(>= (block.coinbase F) 0)
(<= (block.chainid F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.difficulty F) 0)
(<= (block.coinbase F)
1461501637330902918203684832716283019655932542975)
(>= (block.gaslimit F) 0)
(<= (block.difficulty F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.number F) 0)
(<= (block.gaslimit F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.timestamp F) 0)
(<= (block.number F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (msg.sender F) 0)
(<= (block.timestamp F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (msg.value F) 0)
(<= (msg.sender F) 1461501637330902918203684832716283019655932542975)
(>= (tx.origin F) 0)
(<= (msg.value F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (tx.gasprice F) 0)
(<= (tx.origin F) 1461501637330902918203684832716283019655932542975)
(<= (tx.gasprice F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value F) 0)
(= C 0)
(>= (block.chainid F) 0))
(interface_0_C_104_0 A E D B)) :named summary_constructor_2_C_104_0_to_interface_0_C_104_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data F)) 0) 38))
(a!2 (= (select (bytes_tuple_accessor_array (msg.data F)) 1) 18))
(a!3 (= (select (bytes_tuple_accessor_array (msg.data F)) 2) 31))
(a!4 (= (select (bytes_tuple_accessor_array (msg.data F)) 3) 240)))
(let ((a!5 (and (interface_0_C_104_0 A E D G)
(summary_5_function_f__103_104_0 C A E D F G B)
(>= (block.coinbase F) 0)
(<= (block.chainid F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.difficulty F) 0)
(<= (block.coinbase F)
1461501637330902918203684832716283019655932542975)
(>= (block.gaslimit F) 0)
(<= (block.difficulty F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.number F) 0)
(<= (block.gaslimit F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value F) 0)
(>= (block.timestamp F) 0)
(<= (block.number F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.sig F) 638722032)
(>= (msg.sender F) 0)
(<= (block.timestamp F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!1
(>= (msg.value F) 0)
(<= (msg.sender F)
1461501637330902918203684832716283019655932542975)
a!2
(>= (tx.origin F) 0)
(<= (msg.value F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!3
(>= (tx.gasprice F) 0)
(<= (tx.origin F)
1461501637330902918203684832716283019655932542975)
a!4
(<= (tx.gasprice F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (bytes_tuple_accessor_length (msg.data F)) 4)
(= C 1)
(>= (block.chainid F) 0))))
(=> a!5 error_target_10_0))) :named interface_0_C_104_0_to_error_target_10_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data F)) 0) 38))
(a!2 (= (select (bytes_tuple_accessor_array (msg.data F)) 1) 18))
(a!3 (= (select (bytes_tuple_accessor_array (msg.data F)) 2) 31))
(a!4 (= (select (bytes_tuple_accessor_array (msg.data F)) 3) 240)))
(let ((a!5 (and (interface_0_C_104_0 A E D G)
(summary_5_function_f__103_104_0 C A E D F G B)
(>= (block.coinbase F) 0)
(<= (block.chainid F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.difficulty F) 0)
(<= (block.coinbase F)
1461501637330902918203684832716283019655932542975)
(>= (block.gaslimit F) 0)
(<= (block.difficulty F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.number F) 0)
(<= (block.gaslimit F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value F) 0)
(>= (block.timestamp F) 0)
(<= (block.number F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.sig F) 638722032)
(>= (msg.sender F) 0)
(<= (block.timestamp F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!1
(>= (msg.value F) 0)
(<= (msg.sender F)
1461501637330902918203684832716283019655932542975)
a!2
(>= (tx.origin F) 0)
(<= (msg.value F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!3
(>= (tx.gasprice F) 0)
(<= (tx.origin F)
1461501637330902918203684832716283019655932542975)
a!4
(<= (tx.gasprice F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (bytes_tuple_accessor_length (msg.data F)) 4)
(= C 3)
(>= (block.chainid F) 0))))
(=> a!5 error_target_11_0))) :named interface_0_C_104_0_to_error_target_11_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data F)) 0) 38))
(a!2 (= (select (bytes_tuple_accessor_array (msg.data F)) 1) 18))
(a!3 (= (select (bytes_tuple_accessor_array (msg.data F)) 2) 31))
(a!4 (= (select (bytes_tuple_accessor_array (msg.data F)) 3) 240)))
(let ((a!5 (and (interface_0_C_104_0 A E D G)
(summary_5_function_f__103_104_0 C A E D F G B)
(>= (block.coinbase F) 0)
(<= (block.chainid F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.difficulty F) 0)
(<= (block.coinbase F)
1461501637330902918203684832716283019655932542975)
(>= (block.gaslimit F) 0)
(<= (block.difficulty F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.number F) 0)
(<= (block.gaslimit F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value F) 0)
(>= (block.timestamp F) 0)
(<= (block.number F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.sig F) 638722032)
(>= (msg.sender F) 0)
(<= (block.timestamp F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!1
(>= (msg.value F) 0)
(<= (msg.sender F)
1461501637330902918203684832716283019655932542975)
a!2
(>= (tx.origin F) 0)
(<= (msg.value F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!3
(>= (tx.gasprice F) 0)
(<= (tx.origin F)
1461501637330902918203684832716283019655932542975)
a!4
(<= (tx.gasprice F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (bytes_tuple_accessor_length (msg.data F)) 4)
(= C 4)
(>= (block.chainid F) 0))))
(=> a!5 error_target_12_0))) :named interface_0_C_104_0_to_error_target_12_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data F)) 0) 38))
(a!2 (= (select (bytes_tuple_accessor_array (msg.data F)) 1) 18))
(a!3 (= (select (bytes_tuple_accessor_array (msg.data F)) 2) 31))
(a!4 (= (select (bytes_tuple_accessor_array (msg.data F)) 3) 240)))
(let ((a!5 (and (interface_0_C_104_0 A E D G)
(summary_5_function_f__103_104_0 C A E D F G B)
(>= (block.coinbase F) 0)
(<= (block.chainid F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.difficulty F) 0)
(<= (block.coinbase F)
1461501637330902918203684832716283019655932542975)
(>= (block.gaslimit F) 0)
(<= (block.difficulty F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.number F) 0)
(<= (block.gaslimit F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value F) 0)
(>= (block.timestamp F) 0)
(<= (block.number F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.sig F) 638722032)
(>= (msg.sender F) 0)
(<= (block.timestamp F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!1
(>= (msg.value F) 0)
(<= (msg.sender F)
1461501637330902918203684832716283019655932542975)
a!2
(>= (tx.origin F) 0)
(<= (msg.value F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!3
(>= (tx.gasprice F) 0)
(<= (tx.origin F)
1461501637330902918203684832716283019655932542975)
a!4
(<= (tx.gasprice F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (bytes_tuple_accessor_length (msg.data F)) 4)
(= C 5)
(>= (block.chainid F) 0))))
(=> a!5 error_target_13_0))) :named interface_0_C_104_0_to_error_target_13_0))
(rule (! (let ((a!1 (= (select (bytes_tuple_accessor_array (msg.data F)) 0) 38))
(a!2 (= (select (bytes_tuple_accessor_array (msg.data F)) 1) 18))
(a!3 (= (select (bytes_tuple_accessor_array (msg.data F)) 2) 31))
(a!4 (= (select (bytes_tuple_accessor_array (msg.data F)) 3) 240)))
(let ((a!5 (and (interface_0_C_104_0 A E D H)
true
(>= (block.chainid F) 0)
(<= (block.chainid F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.coinbase F) 0)
(<= (block.coinbase F)
1461501637330902918203684832716283019655932542975)
(>= (block.difficulty F) 0)
(<= (block.difficulty F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.gaslimit F) 0)
(<= (block.gaslimit F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.number F) 0)
(<= (block.number F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (block.timestamp F) 0)
(<= (block.timestamp F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (msg.sender F) 0)
(<= (msg.sender F)
1461501637330902918203684832716283019655932542975)
(>= (msg.value F) 0)
(<= (msg.value F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= (tx.origin F) 0)
(<= (tx.origin F)
1461501637330902918203684832716283019655932542975)
(>= (tx.gasprice F) 0)
(<= (tx.gasprice F)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value F) 0)
(= (msg.sig F) 638722032)
a!1
a!2
a!3
a!4
(>= (bytes_tuple_accessor_length (msg.data F)) 4)
(summary_5_function_f__103_104_0 I3 A E D F H G)
(= I3 6))))
(=> a!5 error_target_14_0))) :named interface_0_C_104_0_to_error_target_14_0))
(query error_target_14_0 :print-certificate true)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment