Skip to content

Instantly share code, notes, and snippets.

@leonardoalt

leonardoalt/cex.smt2

Created June 23, 2021 17:21
Show Gist options
  • Save leonardoalt/d623f11aef4bd2ab09e662cdfc96c88c to your computer and use it in GitHub Desktop.
Save leonardoalt/d623f11aef4bd2ab09e662cdfc96c88c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
cex.smt2
sat
(let ((a!1 (forall ((A Int)
(B abi_type)
(C crypto_type)
(D tx_type)
(E state_type))
(! (=> (and (>= (tx.origin D) 0)
(>= (tx.gasprice D) 0)
(>= (msg.value D) 0)
(>= (msg.sender D) 0)
(>= (block.timestamp D) 0)
(>= (block.number D) 0)
(>= (block.gaslimit D) 0)
(>= (block.difficulty D) 0)
(>= (block.coinbase D) 0)
(>= (block.chainid D) 0)
(<= (tx.origin D)
1461501637330902918203684832716283019655932542975)
(<= (tx.gasprice D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (msg.value D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (msg.sender D)
1461501637330902918203684832716283019655932542975)
(<= (block.timestamp D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.number D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.gaslimit D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.difficulty D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.coinbase D)
1461501637330902918203684832716283019655932542975)
(<= (block.chainid D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= (msg.value D) 0))
(interface_0_C_104_0 A B C E))
:weight 0)))
(a!3 (forall ((A Int)
(B abi_type)
(C crypto_type)
(D tx_type)
(E state_type)
(F Int)
(G Int)
(H Int)
(I Int)
(J Int)
(K Int))
(! (=> (and (summary_4_function_g__54_104_0
0
A
B
C
D
E
0
1
E
I
J
K)
(summary_4_function_g__54_104_0
0
A
B
C
D
E
0
0
E
F
G
H)
(>= K 0)
(>= H 0)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= H
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(not (= K 0)))
(summary_5_function_f__103_104_0 6 A B C D E E))
:weight 0)))
(a!4 (forall ((A Int)
(B abi_type)
(C crypto_type)
(D tx_type)
(E state_type)
(F Int)
(G Int)
(H Int)
(I Int)
(J Int))
(! (=> (and (summary_3_function_exp__39_104_0
0
A
B
C
D
E
F
G
E
H
I
J)
(>= F 0)
(>= G 0)
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= F
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= G
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= J 0))
(summary_4_function_g__54_104_0 0 A B C D E F G E F G J))
:weight 0)))
(a!5 (asserted (forall ((A Int)
(B abi_type)
(C crypto_type)
(D tx_type)
(E state_type)
(F Int)
(G Int)
(H Int)
(I Int)
(J Int)
(K Int)
(L Int))
(! (let ((a!1 (>= (bv2int ((_ extract 0 0)
((_ int2bv 256) I)))
0))
(a!2 (<= (bv2int ((_ extract 0 0)
((_ int2bv 256) I)))
115792089237316195423570985008687907853269984665640564039457584007913129639935))
(a!3 (not (<= 2 (+ (* (- 2) G) K))))
(a!4 (= (bv2int ((_ extract 0 0)
((_ int2bv 256) I)))
1)))
(let ((a!5 (and (summary_3_function_exp__39_104_0
0
A
B
C
D
E
F
G
E
H
I
J)
(not (= K 0))
(= L (* J J))
a!1
(>= J 0)
(>= K 0)
(>= L 0)
(>= F 0)
(>= G 0)
(>= I 0)
a!2
a!3
(<= 0 (+ (* (- 2) G) K))
(<= J
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= K
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= L
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= F
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= G
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= I
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(not a!4))))
(=> a!5
(summary_3_function_exp__39_104_0
0
A
B
C
D
E
F
K
E
H
I
L))))
:weight 0))))
(a!6 (forall ((A Int)
(B abi_type)
(C crypto_type)
(D tx_type)
(E state_type)
(F Int))
(! (=> (and (<= F
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(>= F 0))
(summary_3_function_exp__39_104_0 0 A B C D E F 0 E F 0 1))
:weight 0)))
(a!7 (store (store (store ((as const (Array Int Int)) 31) 12 13) 0 38)
25
26))
(a!11 (store (store (store ((as const (Array Int Int)) 31) 1 18) 0 38)
25
26))
(a!18 (store (store (store ((as const (Array Int Int)) 31) 1 18) 0 38)
12
13)))
(let ((a!2 ((_ hyper-res 0 0)
(asserted a!1)
(interface_0_C_104_0
8
abi_type
(crypto_type ((as const (Array ecrecover_input_type Int))
638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032))
(state_type ((as const (Array Int Int)) 638722032)))))
(a!8 (bytes_tuple (store (store (store a!7 1 18) 19 20) 3 240) 4))
(a!12 (bytes_tuple (store (store (store a!11 12 13) 19 20) 3 240) 4))
(a!19 (bytes_tuple (store (store (store a!18 25 26) 19 20) 3 240) 4)))
(let ((a!9 (tx_type 26285
8945
15921
20537
281
1142
(store (store ((as const (Array Int Int)) 16) 9 10) 25 27)
a!8
28100
638722032
0
5853
30612))
(a!13 (tx_type 26285
8945
15921
20537
281
1142
(store (store ((as const (Array Int Int)) 16) 9 10) 25 27)
a!12
28100
638722032
0
5853
30612))
(a!20 (tx_type 26285
8945
15921
20537
281
1142
(store (store ((as const (Array Int Int)) 16) 25 27) 9 10)
a!19
28100
638722032
0
5853
30612)))
(let ((a!10 ((_ hyper-res 0 0)
(asserted a!6)
(summary_3_function_exp__39_104_0
0
8
abi_type
(crypto_type ((as const (Array ecrecover_input_type Int))
638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032))
a!9
(state_type ((as const (Array Int Int)) 638722032))
0
0
(state_type ((as const (Array Int Int)) 638722032))
0
0
1)))
(a!16 ((_ hyper-res 0 0)
(asserted a!6)
(summary_3_function_exp__39_104_0
0
8
abi_type
(crypto_type ((as const (Array ecrecover_input_type Int))
638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032))
a!13
(state_type ((as const (Array Int Int)) 638722032))
0
0
(state_type ((as const (Array Int Int)) 638722032))
0
0
1))))
(let ((a!14 ((_ hyper-res 0 0 0 1)
a!5
a!10
(summary_3_function_exp__39_104_0
0
8
abi_type
(crypto_type ((as const (Array ecrecover_input_type Int))
638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032))
a!13
(state_type ((as const (Array Int Int)) 638722032))
0
1
(state_type ((as const (Array Int Int)) 638722032))
0
0
1)))
(a!17 ((_ hyper-res 0 0 0 1)
(asserted a!4)
a!16
(summary_4_function_g__54_104_0
0
8
abi_type
(crypto_type ((as const (Array ecrecover_input_type Int))
638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032))
a!9
(state_type ((as const (Array Int Int)) 638722032))
0
0
(state_type ((as const (Array Int Int)) 638722032))
0
0
1))))
(let ((a!15 ((_ hyper-res 0 0 0 1)
(asserted a!4)
a!14
(summary_4_function_g__54_104_0
0
8
abi_type
(crypto_type ((as const (Array ecrecover_input_type Int))
638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032))
a!9
(state_type ((as const (Array Int Int)) 638722032))
0
1
(state_type ((as const (Array Int Int)) 638722032))
0
1
1))))
(let ((a!21 ((_ hyper-res 0 0 0 1 0 2)
(asserted a!3)
a!15
a!17
(summary_5_function_f__103_104_0
6
8
abi_type
(crypto_type ((as const (Array ecrecover_input_type Int))
638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032)
((as const (Array bytes_tuple Int)) 638722032))
a!20
(state_type ((as const (Array Int Int)) 638722032))
(state_type ((as const (Array Int Int)) 638722032))))))
(let ((a!22 ((_ hyper-res 0 0 0 1 0 2)
(asserted (forall ((A Int)
(B abi_type)
(C crypto_type)
(D tx_type)
(E state_type)
(F state_type))
(! (let ((a!1 (= (select (bytes_tuple_accessor_array
(msg.data D))
2)
31))
(a!2 (= (select (bytes_tuple_accessor_array
(msg.data D))
1)
18))
(a!3 (= (select (bytes_tuple_accessor_array
(msg.data D))
0)
38))
(a!4 (= (select (bytes_tuple_accessor_array
(msg.data D))
3)
240)))
(let ((a!5 (and (interface_0_C_104_0 A B C E)
(summary_5_function_f__103_104_0
6
A
B
C
D
E
F)
a!1
a!2
a!3
(= (msg.value D) 0)
(= (msg.sig D) 638722032)
(>= (tx.origin D) 0)
(>= (tx.gasprice D) 0)
(>= (msg.value D) 0)
(>= (msg.sender D) 0)
(>= (block.timestamp D) 0)
(>= (block.number D) 0)
(>= (block.gaslimit D) 0)
(>= (block.difficulty D) 0)
(>= (block.coinbase D) 0)
(>= (block.chainid D) 0)
(>= (bytes_tuple_accessor_length
(msg.data D))
4)
(<= (tx.origin D)
1461501637330902918203684832716283019655932542975)
(<= (tx.gasprice D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (msg.value D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (msg.sender D)
1461501637330902918203684832716283019655932542975)
(<= (block.timestamp D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.number D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.gaslimit D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.difficulty D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(<= (block.coinbase D)
1461501637330902918203684832716283019655932542975)
(<= (block.chainid D)
115792089237316195423570985008687907853269984665640564039457584007913129639935)
a!4)))
(=> a!5 query!0)))
:weight 0)))
a!2
a!21
query!0)))
(mp a!22 (asserted (=> query!0 false)) false)))))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment