Skip to content

Instantly share code, notes, and snippets.

@leonardoalt

leonardoalt/segfault.smt2

Created September 17, 2020 17:04
Show Gist options
  • Save leonardoalt/9be6d535d0ee1aeecd8383d094283d8f to your computer and use it in GitHub Desktop.
Save leonardoalt/9be6d535d0ee1aeecd8383d094283d8f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
segfault.smt2
(declare-datatypes ((|uint[]_tuple| 0)) (((|uint[]_tuple| (|uint[]_tuple_accessor_array| (Array Int Int)) (|uint[]_tuple_accessor_length| Int)))))
(declare-datatypes ((|struct C.T| 0)) (((|struct C.T| (|struct C.T_accessor_y| Int) (|struct C.T_accessor_a| |uint[]_tuple|)))))
(declare-datatypes ((|struct C.T[]_tuple| 0)) (((|struct C.T[]_tuple| (|struct C.T[]_tuple_accessor_array| (Array Int |struct C.T|)) (|struct C.T[]_tuple_accessor_length| Int)))))
(declare-datatypes ((|struct C.S| 0)) (((|struct C.S| (|struct C.S_accessor_x| Int) (|struct C.S_accessor_t| |struct C.T|) (|struct C.S_accessor_a| |uint[]_tuple|) (|struct C.S_accessor_ts| |struct C.T[]_tuple|)))))
(declare-datatypes ((|struct C.S[]_tuple| 0)) (((|struct C.S[]_tuple| (|struct C.S[]_tuple_accessor_array| (Array Int |struct C.S|)) (|struct C.S[]_tuple_accessor_length| Int)))))
(declare-datatypes ((state_type 0)) (((state_type (balances (Array Int Int))))))
(declare-rel nondet_interface_C_154_0 (state_type state_type))
(declare-rel error_target_10_0 ())
(declare-rel error_target_9_0 ())
(declare-rel summary_constructor_C_154_0 (Int Int state_type))
(declare-rel block_1_function_f__153_154_0 (Int Int state_type |struct C.S| state_type |struct C.S|))
(declare-rel implicit_constructor_C_154_0 (Int state_type))
(declare-rel interface_C_154_0 (Int state_type))
(declare-rel block_2_f_152_154_0 (Int Int state_type |struct C.S| state_type |struct C.S| |struct C.S[]_tuple|))
(declare-rel summary_0_function_f__153_154_0 (Int Int state_type |struct C.S| state_type |struct C.S|))
(declare-rel error_target_6_0 ())
(declare-rel error_target_7_0 ())
(declare-rel error_target_8_0 ())
(declare-var A state_type)
(declare-var B Int)
(declare-var C |struct C.S|)
(declare-var D |struct C.S|)
(declare-var E Int)
(declare-var F |struct C.S[]_tuple|)
(declare-var G |struct C.S[]_tuple|)
(declare-var H |struct C.S[]_tuple|)
(declare-var I Bool)
(declare-var J |struct C.S|)
(declare-var K Int)
(declare-var L |struct C.S|)
(declare-var M Int)
(declare-var N |struct C.S[]_tuple|)
(declare-var O Int)
(declare-var P Int)
(declare-var Q Int)
(declare-var R Int)
(declare-var S |struct C.S|)
(declare-var T |struct C.S|)
(declare-var U |struct C.S|)
(declare-var V Int)
(declare-var W |struct C.S[]_tuple|)
(declare-var X |struct C.S[]_tuple|)
(declare-var Y |struct C.S[]_tuple|)
(declare-var Z |struct C.S[]_tuple|)
(declare-var A1 Int)
(declare-var B1 Int)
(declare-var C1 Int)
(declare-var D1 |struct C.T|)
(declare-var E1 |struct C.T|)
(declare-var F1 |struct C.T|)
(declare-var G1 |struct C.T|)
(declare-var H1 |struct C.T|)
(declare-var I1 Bool)
(declare-var J1 |struct C.S|)
(declare-var K1 |struct C.S|)
(declare-var L1 |struct C.S[]_tuple|)
(declare-var M1 Int)
(declare-var N1 Int)
(declare-var O1 Int)
(declare-var P1 Int)
(declare-var Q1 |struct C.S|)
(declare-var R1 |struct C.S|)
(declare-var S1 |struct C.S|)
(declare-var T1 Int)
(declare-var U1 |struct C.S[]_tuple|)
(declare-var V1 |struct C.S[]_tuple|)
(declare-var W1 |struct C.S[]_tuple|)
(declare-var X1 |struct C.S[]_tuple|)
(declare-var Y1 Int)
(declare-var Z1 Int)
(declare-var A2 Int)
(declare-var B2 Int)
(declare-var C2 |uint[]_tuple|)
(declare-var D2 |uint[]_tuple|)
(declare-var E2 |uint[]_tuple|)
(declare-var F2 |uint[]_tuple|)
(declare-var G2 Bool)
(declare-var H2 |struct C.S|)
(declare-var I2 Int)
(declare-var J2 |struct C.S|)
(declare-var K2 Int)
(declare-var L2 |struct C.S[]_tuple|)
(declare-var M2 Int)
(declare-var N2 Int)
(declare-var O2 Int)
(declare-var P2 Int)
(declare-var Q2 |struct C.S|)
(declare-var R2 |struct C.S|)
(declare-var S2 |struct C.S|)
(declare-var T2 Int)
(declare-var U2 |struct C.S[]_tuple|)
(declare-var V2 |struct C.S[]_tuple|)
(declare-var W2 |struct C.S[]_tuple|)
(declare-var X2 |struct C.S[]_tuple|)
(declare-var Y2 Int)
(declare-var Z2 Int)
(declare-var A3 Int)
(declare-var B3 Int)
(declare-var C3 Int)
(declare-var D3 |struct C.T[]_tuple|)
(declare-var E3 |struct C.T[]_tuple|)
(declare-var F3 |struct C.T|)
(declare-var G3 |struct C.T|)
(declare-var H3 |struct C.T|)
(declare-var I3 |struct C.S|)
(declare-var J3 |struct C.S|)
(declare-var K3 |struct C.S|)
(declare-var L3 |struct C.S[]_tuple|)
(declare-var M3 |struct C.S[]_tuple|)
(declare-var N3 |struct C.S[]_tuple|)
(declare-var O3 |struct C.S[]_tuple|)
(declare-var P3 Bool)
(declare-var Q3 |struct C.T|)
(declare-var R3 |struct C.T[]_tuple|)
(declare-var S3 |struct C.S|)
(declare-var T3 Int)
(declare-var U3 |struct C.T|)
(declare-var V3 Int)
(declare-var W3 |struct C.T[]_tuple|)
(declare-var X3 |struct C.S|)
(declare-var Y3 Int)
(declare-var Z3 |struct C.S[]_tuple|)
(declare-var A4 Int)
(declare-var B4 Int)
(declare-var C4 Int)
(declare-var D4 Int)
(declare-var E4 Int)
(declare-var F4 Int)
(declare-var G4 Int)
(declare-var H4 Int)
(declare-var I4 Int)
(declare-var J4 |uint[]_tuple|)
(declare-var K4 |uint[]_tuple|)
(declare-var L4 |struct C.S[]_tuple|)
(declare-var M4 |uint[]_tuple|)
(declare-var N4 |uint[]_tuple|)
(declare-var O4 |struct C.T|)
(declare-var P4 |struct C.T|)
(declare-var Q4 |struct C.T|)
(declare-var R4 |struct C.T[]_tuple|)
(declare-var S4 |struct C.T[]_tuple|)
(declare-var T4 |struct C.S|)
(declare-var U4 |struct C.S|)
(declare-var V4 |struct C.S|)
(declare-var W4 |struct C.S[]_tuple|)
(declare-var X4 |struct C.S[]_tuple|)
(declare-var Y4 |struct C.S[]_tuple|)
(declare-var Z4 Bool)
(declare-var A5 Int)
(declare-var B5 |struct C.T|)
(declare-var C5 Int)
(declare-var D5 |struct C.T[]_tuple|)
(declare-var E5 |struct C.S|)
(declare-var F5 Int)
(declare-var G5 |struct C.T|)
(declare-var H5 Int)
(declare-var I5 |struct C.T[]_tuple|)
(declare-var J5 |struct C.S|)
(declare-var K5 Int)
(declare-var L5 |struct C.S[]_tuple|)
(declare-var M5 Int)
(declare-var N5 Int)
(declare-var O5 Int)
(declare-var P5 Int)
(declare-var Q5 Int)
(declare-var R5 Int)
(declare-var S5 Int)
(declare-var T5 Int)
(declare-var U5 Int)
(declare-var V5 Int)
(rule (! (nondet_interface_C_154_0 A A) :named base_nondet))
(rule (! (=> (and (nondet_interface_C_154_0 A A)
(summary_0_function_f__153_154_0 E B A D A C))
(nondet_interface_C_154_0 A A)) :named nondet_interface_C_154_0_to_nondet_interface_C_154_0))
(rule (! (block_1_function_f__153_154_0 E B A D A C) :named block_1_function_f__153_154_0!))
(rule (! (=> (and (block_1_function_f__153_154_0 E B A D A C) (= E 0) (= D C))
(block_2_f_152_154_0 E B A D A C F)) :named block_1_function_f__153_154_0_to_block_2_f_152_154_0))
(rule (! (let ((a!1 (= F
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| X) V T)
(|struct C.S[]_tuple_accessor_length| X))))
(a!2 ((as const (Array Int |struct C.T|))
(|struct C.T| 0 (|uint[]_tuple| ((as const (Array Int Int)) 0) 0)))))
(let ((a!3 (|struct C.S| 0
(|struct C.T| 0
(|uint[]_tuple| ((as const
(Array Int Int))
0)
0))
(|uint[]_tuple| ((as const (Array Int Int)) 0) 0)
(|struct C.T[]_tuple| a!2 0))))
(let ((a!4 (and (block_2_f_152_154_0 C1 B A D A C H)
(= G Z)
(= Y G)
(= V 0)
(= U (select (|struct C.S[]_tuple_accessor_array| G) V))
(= R (|struct C.S_accessor_x| U))
(= P 2)
(= O P)
(= (|struct C.S_accessor_x| T) O)
(= (|struct C.S_accessor_t| T) (|struct C.S_accessor_t| U))
(= (|struct C.S_accessor_a| T) (|struct C.S_accessor_a| U))
(= (|struct C.S_accessor_ts| T) (|struct C.S_accessor_ts| U))
(= Q (|struct C.S_accessor_x| T))
(= X G)
(= S (select (|struct C.S[]_tuple_accessor_array| X) V))
a!1
(= W F)
(= N F)
(= M 0)
(= L (select (|struct C.S[]_tuple_accessor_array| F) M))
(= K (|struct C.S_accessor_x| L))
(= J C)
(= E (|struct C.S_accessor_x| J))
(= I (= K E))
(not (= I true))
(= H
(|struct C.S[]_tuple|
((as const (Array Int |struct C.S|)) a!3)
0))
(= B1 1)
(= A1 3))))
(=> a!4 (summary_0_function_f__153_154_0 B1 B A D A C))))) :named block_2_f_152_154_0_to_summary_0_function_f__153_154_0))
(rule (! (let ((a!1 (= G
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| V1) T1 R1)
(|struct C.S[]_tuple_accessor_length| V1))))
(a!2 (= F
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| Y) V T)
(|struct C.S[]_tuple_accessor_length| Y))))
(a!3 ((as const (Array Int |struct C.T|))
(|struct C.T| 0 (|uint[]_tuple| ((as const (Array Int Int)) 0) 0)))))
(let ((a!4 (|struct C.S| 0
(|struct C.T| 0
(|uint[]_tuple| ((as const
(Array Int Int))
0)
0))
(|uint[]_tuple| ((as const (Array Int Int)) 0) 0)
(|struct C.T[]_tuple| a!3 0))))
(let ((a!5 (and (block_2_f_152_154_0 B2 B A D A C N)
(= H X1)
(= W1 H)
(= T1 0)
(= S1 (select (|struct C.S[]_tuple_accessor_array| H) T1))
(= P1 (|struct C.S_accessor_x| S1))
(= N1 2)
(= M1 N1)
(= (|struct C.S_accessor_x| R1) M1)
(= (|struct C.S_accessor_t| R1) (|struct C.S_accessor_t| S1))
(= (|struct C.S_accessor_a| R1) (|struct C.S_accessor_a| S1))
(= (|struct C.S_accessor_ts| R1) (|struct C.S_accessor_ts| S1))
(= O1 (|struct C.S_accessor_x| R1))
(= V1 H)
(= Q1 (select (|struct C.S[]_tuple_accessor_array| V1) T1))
a!1
(= U1 G)
(= L1 G)
(= C1 0)
(= K1 (select (|struct C.S[]_tuple_accessor_array| G) C1))
(= B1 (|struct C.S_accessor_x| K1))
(= J1 C)
(= A1 (|struct C.S_accessor_x| J1))
(= I1 (= B1 A1))
(= A2 B2)
(= Z G)
(= V 1)
(= U (select (|struct C.S[]_tuple_accessor_array| G) V))
(= H1 (|struct C.S_accessor_t| U))
(= R (|struct C.T_accessor_y| H1))
(= P 3)
(= O P)
(= (|struct C.T_accessor_y| G1) O)
(= (|struct C.T_accessor_a| G1) (|struct C.T_accessor_a| H1))
(= Q (|struct C.T_accessor_y| G1))
(= (|struct C.S_accessor_x| T) (|struct C.S_accessor_x| U))
(= (|struct C.S_accessor_t| T) G1)
(= (|struct C.S_accessor_a| T) (|struct C.S_accessor_a| U))
(= (|struct C.S_accessor_ts| T) (|struct C.S_accessor_ts| U))
(= F1 (|struct C.S_accessor_t| T))
(= Y G)
(= S (select (|struct C.S[]_tuple_accessor_array| Y) V))
a!2
(= X F)
(= W F)
(= M 1)
(= L (select (|struct C.S[]_tuple_accessor_array| F) M))
(= E1 (|struct C.S_accessor_t| L))
(= K (|struct C.T_accessor_y| E1))
(= J C)
(= D1 (|struct C.S_accessor_t| J))
(= E (|struct C.T_accessor_y| D1))
(= I (= K E))
(not (= I true))
(= N
(|struct C.S[]_tuple|
((as const (Array Int |struct C.S|)) a!4)
0))
(= Z1 2)
(= Y1 3))))
(=> a!5 (summary_0_function_f__153_154_0 Z1 B A D A C))))) :named block_2_f_152_154_0_to_summary_0_function_f__153_154_0!))
(rule (! (let ((a!1 (= H
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| V2) T2 R2)
(|struct C.S[]_tuple_accessor_length| V2))))
(a!2 (= G
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| W1) A2 R1)
(|struct C.S[]_tuple_accessor_length| W1))))
(a!3 (= (|struct C.S_accessor_a| T)
(|uint[]_tuple| (store (|uint[]_tuple_accessor_array| F2) B1 Q)
(|uint[]_tuple_accessor_length| F2))))
(a!4 (= F
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| Z) C1 T)
(|struct C.S[]_tuple_accessor_length| Z))))
(a!5 ((as const (Array Int |struct C.T|))
(|struct C.T| 0 (|uint[]_tuple| ((as const (Array Int Int)) 0) 0)))))
(let ((a!6 (|struct C.S| 0
(|struct C.T| 0
(|uint[]_tuple| ((as const
(Array Int Int))
0)
0))
(|uint[]_tuple| ((as const (Array Int Int)) 0) 0)
(|struct C.T[]_tuple| a!5 0))))
(let ((a!7 (and (block_2_f_152_154_0 C3 B A D A C W)
(= N X2)
(= W2 N)
(= T2 0)
(= S2 (select (|struct C.S[]_tuple_accessor_array| N) T2))
(= P2 (|struct C.S_accessor_x| S2))
(= N2 2)
(= M2 N2)
(= (|struct C.S_accessor_x| R2) M2)
(= (|struct C.S_accessor_t| R2) (|struct C.S_accessor_t| S2))
(= (|struct C.S_accessor_a| R2) (|struct C.S_accessor_a| S2))
(= (|struct C.S_accessor_ts| R2) (|struct C.S_accessor_ts| S2))
(= O2 (|struct C.S_accessor_x| R2))
(= V2 N)
(= Q2 (select (|struct C.S[]_tuple_accessor_array| V2) T2))
a!1
(= U2 H)
(= L2 H)
(= K2 0)
(= J2 (select (|struct C.S[]_tuple_accessor_array| H) K2))
(= I2 (|struct C.S_accessor_x| J2))
(= H2 C)
(= B2 (|struct C.S_accessor_x| H2))
(= G2 (= I2 B2))
(= B3 C3)
(= X1 H)
(= A2 1)
(= S1 (select (|struct C.S[]_tuple_accessor_array| H) A2))
(= H1 (|struct C.S_accessor_t| S1))
(= Z1 (|struct C.T_accessor_y| H1))
(= T1 3)
(= P1 T1)
(= (|struct C.T_accessor_y| G1) P1)
(= (|struct C.T_accessor_a| G1) (|struct C.T_accessor_a| H1))
(= Y1 (|struct C.T_accessor_y| G1))
(= (|struct C.S_accessor_x| R1) (|struct C.S_accessor_x| S1))
(= (|struct C.S_accessor_t| R1) G1)
(= (|struct C.S_accessor_a| R1) (|struct C.S_accessor_a| S1))
(= (|struct C.S_accessor_ts| R1) (|struct C.S_accessor_ts| S1))
(= F1 (|struct C.S_accessor_t| R1))
(= W1 H)
(= Q1 (select (|struct C.S[]_tuple_accessor_array| W1) A2))
a!2
(= V1 G)
(= U1 G)
(= O1 1)
(= K1 (select (|struct C.S[]_tuple_accessor_array| G) O1))
(= E1 (|struct C.S_accessor_t| K1))
(= N1 (|struct C.T_accessor_y| E1))
(= J1 C)
(= D1 (|struct C.S_accessor_t| J1))
(= M1 (|struct C.T_accessor_y| D1))
(= I1 (= N1 M1))
(= A3 B3)
(= L1 G)
(= C1 2)
(= U (select (|struct C.S[]_tuple_accessor_array| G) C1))
(= F2 (|struct C.S_accessor_a| U))
(= B1 2)
(= A1 (select (|uint[]_tuple_accessor_array| F2) B1))
(>= A1 0)
(<= A1
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= R 4)
(= Q R)
(= V (select (|uint[]_tuple_accessor_array| F2) B1))
(= (|struct C.S_accessor_x| T) (|struct C.S_accessor_x| U))
(= (|struct C.S_accessor_t| T) (|struct C.S_accessor_t| U))
a!3
(= (|struct C.S_accessor_ts| T) (|struct C.S_accessor_ts| U))
(= E2 (|struct C.S_accessor_a| T))
(= Z G)
(= S (select (|struct C.S[]_tuple_accessor_array| Z) C1))
a!4
(= Y F)
(= X F)
(= P 2)
(= L (select (|struct C.S[]_tuple_accessor_array| F) P))
(= D2 (|struct C.S_accessor_a| L))
(= O 2)
(= M (select (|uint[]_tuple_accessor_array| D2) O))
(>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= J C)
(= C2 (|struct C.S_accessor_a| J))
(= K 2)
(= E (select (|uint[]_tuple_accessor_array| C2) K))
(>= E 0)
(<= E
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= I (= M E))
(not (= I true))
(= W
(|struct C.S[]_tuple|
((as const (Array Int |struct C.S|)) a!6)
0))
(= Z2 3)
(= Y2 3))))
(=> a!7 (summary_0_function_f__153_154_0 Z2 B A D A C))))) :named block_2_f_152_154_0_to_summary_0_function_f__153_154_0!!))
(rule (! (let ((a!1 (= N
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| M3) Z2 J3)
(|struct C.S[]_tuple_accessor_length| M3))))
(a!2 (= H
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| V2) I2 J2)
(|struct C.S[]_tuple_accessor_length| V2))))
(a!3 (= (|struct C.S_accessor_a| K1)
(|uint[]_tuple| (store (|uint[]_tuple_accessor_array| F2) M1 V)
(|uint[]_tuple_accessor_length| F2))))
(a!4 (= G
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| W1) N1 K1)
(|struct C.S[]_tuple_accessor_length| W1))))
(a!5 (= (|struct C.S_accessor_ts| L)
(|struct C.T[]_tuple|
(store (|struct C.T[]_tuple_accessor_array| E3) E E1)
(|struct C.T[]_tuple_accessor_length| E3))))
(a!6 (= F
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| Z) K L)
(|struct C.S[]_tuple_accessor_length| Z))))
(a!7 ((as const (Array Int |struct C.T|))
(|struct C.T| 0 (|uint[]_tuple| ((as const (Array Int Int)) 0) 0)))))
(let ((a!8 (|struct C.S| 0
(|struct C.T| 0
(|uint[]_tuple| ((as const
(Array Int Int))
0)
0))
(|uint[]_tuple| ((as const (Array Int Int)) 0) 0)
(|struct C.T[]_tuple| a!7 0))))
(let ((a!9 (and (block_2_f_152_154_0 I4 B A D A C X)
(= W O3)
(= N3 W)
(= Z2 0)
(= K3 (select (|struct C.S[]_tuple_accessor_array| W) Z2))
(= Y2 (|struct C.S_accessor_x| K3))
(= P2 2)
(= O2 P2)
(= (|struct C.S_accessor_x| J3) O2)
(= (|struct C.S_accessor_t| J3) (|struct C.S_accessor_t| K3))
(= (|struct C.S_accessor_a| J3) (|struct C.S_accessor_a| K3))
(= (|struct C.S_accessor_ts| J3) (|struct C.S_accessor_ts| K3))
(= T2 (|struct C.S_accessor_x| J3))
(= M3 W)
(= I3 (select (|struct C.S[]_tuple_accessor_array| M3) Z2))
a!1
(= L3 N)
(= X2 N)
(= N2 0)
(= S2 (select (|struct C.S[]_tuple_accessor_array| N) N2))
(= M2 (|struct C.S_accessor_x| S2))
(= R2 C)
(= K2 (|struct C.S_accessor_x| R2))
(= G2 (= M2 K2))
(= H4 I4)
(= W2 N)
(= I2 1)
(= Q2 (select (|struct C.S[]_tuple_accessor_array| N) I2))
(= H3 (|struct C.S_accessor_t| Q2))
(= B2 (|struct C.T_accessor_y| H3))
(= Z1 3)
(= Y1 Z1)
(= (|struct C.T_accessor_y| G3) Y1)
(= (|struct C.T_accessor_a| G3) (|struct C.T_accessor_a| H3))
(= A2 (|struct C.T_accessor_y| G3))
(= (|struct C.S_accessor_x| J2) (|struct C.S_accessor_x| Q2))
(= (|struct C.S_accessor_t| J2) G3)
(= (|struct C.S_accessor_a| J2) (|struct C.S_accessor_a| Q2))
(= (|struct C.S_accessor_ts| J2) (|struct C.S_accessor_ts| Q2))
(= F3 (|struct C.S_accessor_t| J2))
(= V2 N)
(= H2 (select (|struct C.S[]_tuple_accessor_array| V2) I2))
a!2
(= U2 H)
(= L2 H)
(= T1 1)
(= S1 (select (|struct C.S[]_tuple_accessor_array| H) T1))
(= H1 (|struct C.S_accessor_t| S1))
(= P1 (|struct C.T_accessor_y| H1))
(= R1 C)
(= G1 (|struct C.S_accessor_t| R1))
(= O1 (|struct C.T_accessor_y| G1))
(= I1 (= P1 O1))
(= G4 H4)
(= X1 H)
(= N1 2)
(= Q1 (select (|struct C.S[]_tuple_accessor_array| H) N1))
(= F2 (|struct C.S_accessor_a| Q1))
(= M1 2)
(= C1 (select (|uint[]_tuple_accessor_array| F2) M1))
(>= C1 0)
(<= C1
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= A1 4)
(= V A1)
(= B1 (select (|uint[]_tuple_accessor_array| F2) M1))
(= (|struct C.S_accessor_x| K1) (|struct C.S_accessor_x| Q1))
(= (|struct C.S_accessor_t| K1) (|struct C.S_accessor_t| Q1))
a!3
(= (|struct C.S_accessor_ts| K1) (|struct C.S_accessor_ts| Q1))
(= E2 (|struct C.S_accessor_a| K1))
(= W1 H)
(= J1 (select (|struct C.S[]_tuple_accessor_array| W1) N1))
a!4
(= V1 G)
(= U1 G)
(= R 2)
(= U (select (|struct C.S[]_tuple_accessor_array| G) R))
(= D2 (|struct C.S_accessor_a| U))
(= Q 2)
(= P (select (|uint[]_tuple_accessor_array| D2) Q))
(>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= T C)
(= C2 (|struct C.S_accessor_a| T))
(= O 2)
(= M (select (|uint[]_tuple_accessor_array| C2) O))
(>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= I (= P M))
(= F4 G4)
(= L1 G)
(= K 0)
(= S (select (|struct C.S[]_tuple_accessor_array| G) K))
(= E3 (|struct C.S_accessor_ts| S))
(= E 3)
(= F1 (select (|struct C.T[]_tuple_accessor_array| E3) E))
(= D4 (|struct C.T_accessor_y| F1))
(= B4 5)
(= A4 B4)
(= (|struct C.T_accessor_y| E1) A4)
(= (|struct C.T_accessor_a| E1) (|struct C.T_accessor_a| F1))
(= C4 (|struct C.T_accessor_y| E1))
(= D1 (select (|struct C.T[]_tuple_accessor_array| E3) E))
(= (|struct C.S_accessor_x| L) (|struct C.S_accessor_x| S))
(= (|struct C.S_accessor_t| L) (|struct C.S_accessor_t| S))
(= (|struct C.S_accessor_a| L) (|struct C.S_accessor_a| S))
a!5
(= D3 (|struct C.S_accessor_ts| L))
(= Z G)
(= J (select (|struct C.S[]_tuple_accessor_array| Z) K))
a!6
(= Y F)
(= Z3 F)
(= Y3 0)
(= X3 (select (|struct C.S[]_tuple_accessor_array| F) Y3))
(= W3 (|struct C.S_accessor_ts| X3))
(= V3 3)
(= U3 (select (|struct C.T[]_tuple_accessor_array| W3) V3))
(= T3 (|struct C.T_accessor_y| U3))
(= S3 C)
(= R3 (|struct C.S_accessor_ts| S3))
(= C3 3)
(= Q3 (select (|struct C.T[]_tuple_accessor_array| R3) C3))
(= B3 (|struct C.T_accessor_y| Q3))
(= P3 (= T3 B3))
(not (= P3 true))
(= X
(|struct C.S[]_tuple|
((as const (Array Int |struct C.S|)) a!8)
0))
(= E4 4)
(= A3 3))))
(=> a!9 (summary_0_function_f__153_154_0 E4 B A D A C))))) :named block_2_f_152_154_0_to_summary_0_function_f__153_154_0!!!))
(rule (! (let ((a!1 (= W
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| N3) Z2 J3)
(|struct C.S[]_tuple_accessor_length| N3))))
(a!2 (= N
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| W2) I2 J2)
(|struct C.S[]_tuple_accessor_length| W2))))
(a!3 (= (|struct C.S_accessor_a| K1)
(|uint[]_tuple| (store (|uint[]_tuple_accessor_array| F2) M1 V)
(|uint[]_tuple_accessor_length| F2))))
(a!4 (= H
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| X1) N1 K1)
(|struct C.S[]_tuple_accessor_length| X1))))
(a!5 (= (|struct C.S_accessor_ts| L)
(|struct C.T[]_tuple|
(store (|struct C.T[]_tuple_accessor_array| E3) E E1)
(|struct C.T[]_tuple_accessor_length| E3))))
(a!6 (= G
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| L1) K L)
(|struct C.S[]_tuple_accessor_length| L1))))
(a!7 (= (|struct C.T_accessor_a| P4)
(|uint[]_tuple| (store (|uint[]_tuple_accessor_array| N4) G4 C4)
(|uint[]_tuple_accessor_length| N4))))
(a!8 (= (|struct C.S_accessor_ts| U4)
(|struct C.T[]_tuple|
(store (|struct C.T[]_tuple_accessor_array| S4) H4 P4)
(|struct C.T[]_tuple_accessor_length| S4))))
(a!9 (= F
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| X4) I4 U4)
(|struct C.S[]_tuple_accessor_length| X4))))
(a!10 ((as const (Array Int |struct C.T|))
(|struct C.T| 0 (|uint[]_tuple| ((as const (Array Int Int)) 0) 0)))))
(let ((a!11 (|struct C.S| 0
(|struct C.T| 0
(|uint[]_tuple| ((as const
(Array Int Int))
0)
0))
(|uint[]_tuple| ((as const (Array Int Int)) 0) 0)
(|struct C.T[]_tuple| a!10 0))))
(let ((a!12 (and (block_2_f_152_154_0 V5 B A D A C Y)
(= X Z3)
(= O3 X)
(= Z2 0)
(= K3 (select (|struct C.S[]_tuple_accessor_array| X) Z2))
(= Y2 (|struct C.S_accessor_x| K3))
(= P2 2)
(= O2 P2)
(= (|struct C.S_accessor_x| J3) O2)
(= (|struct C.S_accessor_t| J3) (|struct C.S_accessor_t| K3))
(= (|struct C.S_accessor_a| J3) (|struct C.S_accessor_a| K3))
(= (|struct C.S_accessor_ts| J3) (|struct C.S_accessor_ts| K3))
(= T2 (|struct C.S_accessor_x| J3))
(= N3 X)
(= I3 (select (|struct C.S[]_tuple_accessor_array| N3) Z2))
a!1
(= M3 W)
(= L3 W)
(= N2 0)
(= S2 (select (|struct C.S[]_tuple_accessor_array| W) N2))
(= M2 (|struct C.S_accessor_x| S2))
(= R2 C)
(= K2 (|struct C.S_accessor_x| R2))
(= G2 (= M2 K2))
(= U5 V5)
(= X2 W)
(= I2 1)
(= Q2 (select (|struct C.S[]_tuple_accessor_array| W) I2))
(= H3 (|struct C.S_accessor_t| Q2))
(= B2 (|struct C.T_accessor_y| H3))
(= Z1 3)
(= Y1 Z1)
(= (|struct C.T_accessor_y| G3) Y1)
(= (|struct C.T_accessor_a| G3) (|struct C.T_accessor_a| H3))
(= A2 (|struct C.T_accessor_y| G3))
(= (|struct C.S_accessor_x| J2) (|struct C.S_accessor_x| Q2))
(= (|struct C.S_accessor_t| J2) G3)
(= (|struct C.S_accessor_a| J2) (|struct C.S_accessor_a| Q2))
(= (|struct C.S_accessor_ts| J2) (|struct C.S_accessor_ts| Q2))
(= F3 (|struct C.S_accessor_t| J2))
(= W2 W)
(= H2 (select (|struct C.S[]_tuple_accessor_array| W2) I2))
a!2
(= V2 N)
(= U2 N)
(= T1 1)
(= S1 (select (|struct C.S[]_tuple_accessor_array| N) T1))
(= H1 (|struct C.S_accessor_t| S1))
(= P1 (|struct C.T_accessor_y| H1))
(= R1 C)
(= G1 (|struct C.S_accessor_t| R1))
(= O1 (|struct C.T_accessor_y| G1))
(= I1 (= P1 O1))
(= T5 U5)
(= L2 N)
(= N1 2)
(= Q1 (select (|struct C.S[]_tuple_accessor_array| N) N1))
(= F2 (|struct C.S_accessor_a| Q1))
(= M1 2)
(= C1 (select (|uint[]_tuple_accessor_array| F2) M1))
(>= C1 0)
(<= C1
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= A1 4)
(= V A1)
(= B1 (select (|uint[]_tuple_accessor_array| F2) M1))
(= (|struct C.S_accessor_x| K1) (|struct C.S_accessor_x| Q1))
(= (|struct C.S_accessor_t| K1) (|struct C.S_accessor_t| Q1))
a!3
(= (|struct C.S_accessor_ts| K1) (|struct C.S_accessor_ts| Q1))
(= E2 (|struct C.S_accessor_a| K1))
(= X1 N)
(= J1 (select (|struct C.S[]_tuple_accessor_array| X1) N1))
a!4
(= W1 H)
(= V1 H)
(= R 2)
(= U (select (|struct C.S[]_tuple_accessor_array| H) R))
(= D2 (|struct C.S_accessor_a| U))
(= Q 2)
(= P (select (|uint[]_tuple_accessor_array| D2) Q))
(>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= T C)
(= C2 (|struct C.S_accessor_a| T))
(= O 2)
(= M (select (|uint[]_tuple_accessor_array| C2) O))
(>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= I (= P M))
(= S5 T5)
(= U1 H)
(= K 0)
(= S (select (|struct C.S[]_tuple_accessor_array| H) K))
(= E3 (|struct C.S_accessor_ts| S))
(= E 3)
(= F1 (select (|struct C.T[]_tuple_accessor_array| E3) E))
(= P5 (|struct C.T_accessor_y| F1))
(= N5 5)
(= M5 N5)
(= (|struct C.T_accessor_y| E1) M5)
(= (|struct C.T_accessor_a| E1) (|struct C.T_accessor_a| F1))
(= O5 (|struct C.T_accessor_y| E1))
(= D1 (select (|struct C.T[]_tuple_accessor_array| E3) E))
(= (|struct C.S_accessor_x| L) (|struct C.S_accessor_x| S))
(= (|struct C.S_accessor_t| L) (|struct C.S_accessor_t| S))
(= (|struct C.S_accessor_a| L) (|struct C.S_accessor_a| S))
a!5
(= D3 (|struct C.S_accessor_ts| L))
(= L1 H)
(= J (select (|struct C.S[]_tuple_accessor_array| L1) K))
a!6
(= Z G)
(= L5 G)
(= K5 0)
(= J5 (select (|struct C.S[]_tuple_accessor_array| G) K5))
(= I5 (|struct C.S_accessor_ts| J5))
(= H5 3)
(= G5 (select (|struct C.T[]_tuple_accessor_array| I5) H5))
(= F5 (|struct C.T_accessor_y| G5))
(= E5 C)
(= D5 (|struct C.S_accessor_ts| E5))
(= C5 3)
(= B5 (select (|struct C.T[]_tuple_accessor_array| D5) C5))
(= A5 (|struct C.T_accessor_y| B5))
(= Z4 (= F5 A5))
(= R5 S5)
(= Y4 G)
(= I4 1)
(= V4 (select (|struct C.S[]_tuple_accessor_array| G) I4))
(= S4 (|struct C.S_accessor_ts| V4))
(= H4 4)
(= Q4 (select (|struct C.T[]_tuple_accessor_array| S4) H4))
(= N4 (|struct C.T_accessor_a| Q4))
(= G4 5)
(= F4 (select (|uint[]_tuple_accessor_array| N4) G4))
(>= F4 0)
(<= F4
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= D4 6)
(= C4 D4)
(= E4 (select (|uint[]_tuple_accessor_array| N4) G4))
(= (|struct C.T_accessor_y| P4) (|struct C.T_accessor_y| Q4))
a!7
(= M4 (|struct C.T_accessor_a| P4))
(= O4 (select (|struct C.T[]_tuple_accessor_array| S4) H4))
(= (|struct C.S_accessor_x| U4) (|struct C.S_accessor_x| V4))
(= (|struct C.S_accessor_t| U4) (|struct C.S_accessor_t| V4))
(= (|struct C.S_accessor_a| U4) (|struct C.S_accessor_a| V4))
a!8
(= R4 (|struct C.S_accessor_ts| U4))
(= X4 G)
(= T4 (select (|struct C.S[]_tuple_accessor_array| X4) I4))
a!9
(= W4 F)
(= L4 F)
(= B4 1)
(= X3 (select (|struct C.S[]_tuple_accessor_array| F) B4))
(= W3 (|struct C.S_accessor_ts| X3))
(= A4 4)
(= U3 (select (|struct C.T[]_tuple_accessor_array| W3) A4))
(= K4 (|struct C.T_accessor_a| U3))
(= Y3 5)
(= V3 (select (|uint[]_tuple_accessor_array| K4) Y3))
(>= V3 0)
(<= V3
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= S3 C)
(= R3 (|struct C.S_accessor_ts| S3))
(= T3 4)
(= Q3 (select (|struct C.T[]_tuple_accessor_array| R3) T3))
(= J4 (|struct C.T_accessor_a| Q3))
(= C3 5)
(= B3 (select (|uint[]_tuple_accessor_array| J4) C3))
(>= B3 0)
(<= B3
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= P3 (= V3 B3))
(not (= P3 true))
(= Y
(|struct C.S[]_tuple|
((as const (Array Int |struct C.S|)) a!11)
0))
(= Q5 5)
(= A3 3))))
(=> a!12 (summary_0_function_f__153_154_0 Q5 B A D A C))))) :named block_2_f_152_154_0_to_summary_0_function_f__153_154_0!!!!))
(rule (! (let ((a!1 (= W
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| N3) Z2 J3)
(|struct C.S[]_tuple_accessor_length| N3))))
(a!2 (= N
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| W2) I2 J2)
(|struct C.S[]_tuple_accessor_length| W2))))
(a!3 (= (|struct C.S_accessor_a| K1)
(|uint[]_tuple| (store (|uint[]_tuple_accessor_array| F2) M1 V)
(|uint[]_tuple_accessor_length| F2))))
(a!4 (= H
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| X1) N1 K1)
(|struct C.S[]_tuple_accessor_length| X1))))
(a!5 (= (|struct C.S_accessor_ts| L)
(|struct C.T[]_tuple|
(store (|struct C.T[]_tuple_accessor_array| E3) E E1)
(|struct C.T[]_tuple_accessor_length| E3))))
(a!6 (= G
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| L1) K L)
(|struct C.S[]_tuple_accessor_length| L1))))
(a!7 (= (|struct C.T_accessor_a| P4)
(|uint[]_tuple| (store (|uint[]_tuple_accessor_array| N4) G4 C4)
(|uint[]_tuple_accessor_length| N4))))
(a!8 (= (|struct C.S_accessor_ts| U4)
(|struct C.T[]_tuple|
(store (|struct C.T[]_tuple_accessor_array| S4) H4 P4)
(|struct C.T[]_tuple_accessor_length| S4))))
(a!9 (= F
(|struct C.S[]_tuple|
(store (|struct C.S[]_tuple_accessor_array| X4) I4 U4)
(|struct C.S[]_tuple_accessor_length| X4))))
(a!10 ((as const (Array Int |struct C.T|))
(|struct C.T| 0 (|uint[]_tuple| ((as const (Array Int Int)) 0) 0)))))
(let ((a!11 (|struct C.S| 0
(|struct C.T| 0
(|uint[]_tuple| ((as const
(Array Int Int))
0)
0))
(|uint[]_tuple| ((as const (Array Int Int)) 0) 0)
(|struct C.T[]_tuple| a!10 0))))
(let ((a!12 (and (block_2_f_152_154_0 V5 B A D A C Y)
(= X Z3)
(= O3 X)
(= Z2 0)
(= K3 (select (|struct C.S[]_tuple_accessor_array| X) Z2))
(= Y2 (|struct C.S_accessor_x| K3))
(= P2 2)
(= O2 P2)
(= (|struct C.S_accessor_x| J3) O2)
(= (|struct C.S_accessor_t| J3) (|struct C.S_accessor_t| K3))
(= (|struct C.S_accessor_a| J3) (|struct C.S_accessor_a| K3))
(= (|struct C.S_accessor_ts| J3) (|struct C.S_accessor_ts| K3))
(= T2 (|struct C.S_accessor_x| J3))
(= N3 X)
(= I3 (select (|struct C.S[]_tuple_accessor_array| N3) Z2))
a!1
(= M3 W)
(= L3 W)
(= N2 0)
(= S2 (select (|struct C.S[]_tuple_accessor_array| W) N2))
(= M2 (|struct C.S_accessor_x| S2))
(= R2 C)
(= K2 (|struct C.S_accessor_x| R2))
(= G2 (= M2 K2))
(= U5 V5)
(= X2 W)
(= I2 1)
(= Q2 (select (|struct C.S[]_tuple_accessor_array| W) I2))
(= H3 (|struct C.S_accessor_t| Q2))
(= B2 (|struct C.T_accessor_y| H3))
(= Z1 3)
(= Y1 Z1)
(= (|struct C.T_accessor_y| G3) Y1)
(= (|struct C.T_accessor_a| G3) (|struct C.T_accessor_a| H3))
(= A2 (|struct C.T_accessor_y| G3))
(= (|struct C.S_accessor_x| J2) (|struct C.S_accessor_x| Q2))
(= (|struct C.S_accessor_t| J2) G3)
(= (|struct C.S_accessor_a| J2) (|struct C.S_accessor_a| Q2))
(= (|struct C.S_accessor_ts| J2) (|struct C.S_accessor_ts| Q2))
(= F3 (|struct C.S_accessor_t| J2))
(= W2 W)
(= H2 (select (|struct C.S[]_tuple_accessor_array| W2) I2))
a!2
(= V2 N)
(= U2 N)
(= T1 1)
(= S1 (select (|struct C.S[]_tuple_accessor_array| N) T1))
(= H1 (|struct C.S_accessor_t| S1))
(= P1 (|struct C.T_accessor_y| H1))
(= R1 C)
(= G1 (|struct C.S_accessor_t| R1))
(= O1 (|struct C.T_accessor_y| G1))
(= I1 (= P1 O1))
(= T5 U5)
(= L2 N)
(= N1 2)
(= Q1 (select (|struct C.S[]_tuple_accessor_array| N) N1))
(= F2 (|struct C.S_accessor_a| Q1))
(= M1 2)
(= C1 (select (|uint[]_tuple_accessor_array| F2) M1))
(>= C1 0)
(<= C1
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= A1 4)
(= V A1)
(= B1 (select (|uint[]_tuple_accessor_array| F2) M1))
(= (|struct C.S_accessor_x| K1) (|struct C.S_accessor_x| Q1))
(= (|struct C.S_accessor_t| K1) (|struct C.S_accessor_t| Q1))
a!3
(= (|struct C.S_accessor_ts| K1) (|struct C.S_accessor_ts| Q1))
(= E2 (|struct C.S_accessor_a| K1))
(= X1 N)
(= J1 (select (|struct C.S[]_tuple_accessor_array| X1) N1))
a!4
(= W1 H)
(= V1 H)
(= R 2)
(= U (select (|struct C.S[]_tuple_accessor_array| H) R))
(= D2 (|struct C.S_accessor_a| U))
(= Q 2)
(= P (select (|uint[]_tuple_accessor_array| D2) Q))
(>= P 0)
(<= P
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= T C)
(= C2 (|struct C.S_accessor_a| T))
(= O 2)
(= M (select (|uint[]_tuple_accessor_array| C2) O))
(>= M 0)
(<= M
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= I (= P M))
(= S5 T5)
(= U1 H)
(= K 0)
(= S (select (|struct C.S[]_tuple_accessor_array| H) K))
(= E3 (|struct C.S_accessor_ts| S))
(= E 3)
(= F1 (select (|struct C.T[]_tuple_accessor_array| E3) E))
(= P5 (|struct C.T_accessor_y| F1))
(= N5 5)
(= M5 N5)
(= (|struct C.T_accessor_y| E1) M5)
(= (|struct C.T_accessor_a| E1) (|struct C.T_accessor_a| F1))
(= O5 (|struct C.T_accessor_y| E1))
(= D1 (select (|struct C.T[]_tuple_accessor_array| E3) E))
(= (|struct C.S_accessor_x| L) (|struct C.S_accessor_x| S))
(= (|struct C.S_accessor_t| L) (|struct C.S_accessor_t| S))
(= (|struct C.S_accessor_a| L) (|struct C.S_accessor_a| S))
a!5
(= D3 (|struct C.S_accessor_ts| L))
(= L1 H)
(= J (select (|struct C.S[]_tuple_accessor_array| L1) K))
a!6
(= Z G)
(= L5 G)
(= K5 0)
(= J5 (select (|struct C.S[]_tuple_accessor_array| G) K5))
(= I5 (|struct C.S_accessor_ts| J5))
(= H5 3)
(= G5 (select (|struct C.T[]_tuple_accessor_array| I5) H5))
(= F5 (|struct C.T_accessor_y| G5))
(= E5 C)
(= D5 (|struct C.S_accessor_ts| E5))
(= C5 3)
(= B5 (select (|struct C.T[]_tuple_accessor_array| D5) C5))
(= A5 (|struct C.T_accessor_y| B5))
(= Z4 (= F5 A5))
(= R5 S5)
(= Y4 G)
(= I4 1)
(= V4 (select (|struct C.S[]_tuple_accessor_array| G) I4))
(= S4 (|struct C.S_accessor_ts| V4))
(= H4 4)
(= Q4 (select (|struct C.T[]_tuple_accessor_array| S4) H4))
(= N4 (|struct C.T_accessor_a| Q4))
(= G4 5)
(= F4 (select (|uint[]_tuple_accessor_array| N4) G4))
(>= F4 0)
(<= F4
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= D4 6)
(= C4 D4)
(= E4 (select (|uint[]_tuple_accessor_array| N4) G4))
(= (|struct C.T_accessor_y| P4) (|struct C.T_accessor_y| Q4))
a!7
(= M4 (|struct C.T_accessor_a| P4))
(= O4 (select (|struct C.T[]_tuple_accessor_array| S4) H4))
(= (|struct C.S_accessor_x| U4) (|struct C.S_accessor_x| V4))
(= (|struct C.S_accessor_t| U4) (|struct C.S_accessor_t| V4))
(= (|struct C.S_accessor_a| U4) (|struct C.S_accessor_a| V4))
a!8
(= R4 (|struct C.S_accessor_ts| U4))
(= X4 G)
(= T4 (select (|struct C.S[]_tuple_accessor_array| X4) I4))
a!9
(= W4 F)
(= L4 F)
(= B4 1)
(= X3 (select (|struct C.S[]_tuple_accessor_array| F) B4))
(= W3 (|struct C.S_accessor_ts| X3))
(= A4 4)
(= U3 (select (|struct C.T[]_tuple_accessor_array| W3) A4))
(= K4 (|struct C.T_accessor_a| U3))
(= Y3 5)
(= V3 (select (|uint[]_tuple_accessor_array| K4) Y3))
(>= V3 0)
(<= V3
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= S3 C)
(= R3 (|struct C.S_accessor_ts| S3))
(= T3 4)
(= Q3 (select (|struct C.T[]_tuple_accessor_array| R3) T3))
(= J4 (|struct C.T_accessor_a| Q3))
(= C3 5)
(= B3 (select (|uint[]_tuple_accessor_array| J4) C3))
(>= B3 0)
(<= B3
115792089237316195423570985008687907853269984665640564039457584007913129639935)
(= P3 (= V3 B3))
(= Q5 R5)
(= Y
(|struct C.S[]_tuple|
((as const (Array Int |struct C.S|)) a!11)
0))
(= A3 3))))
(=> a!12 (summary_0_function_f__153_154_0 Q5 B A D A C))))) :named block_2_f_152_154_0_to_summary_0_function_f__153_154_0!!!!!))
(rule (! (=> (and (summary_0_function_f__153_154_0 E B A D A C)
(interface_C_154_0 B A)
(= E 0))
(interface_C_154_0 B A)) :named interface_C_154_0_to_interface_C_154_0))
(rule (! (implicit_constructor_C_154_0 B A) :named implicit_constructor_C_154_0!))
(rule (! (=> (and (implicit_constructor_C_154_0 B A) (= E 0))
(summary_constructor_C_154_0 E B A)) :named implicit_constructor_C_154_0_to_summary_constructor_C_154_0))
(rule (! (=> (and (summary_constructor_C_154_0 E B A) (= E 0)) (interface_C_154_0 B A)) :named summary_constructor_C_154_0_to_interface_C_154_0))
(rule (! (=> (and (summary_0_function_f__153_154_0 E B A D A C)
(interface_C_154_0 B A)
(= E 1))
error_target_6_0) :named interface_C_154_0_to_error_target_6_0))
(rule (! (=> (and (summary_0_function_f__153_154_0 E B A D A C)
(interface_C_154_0 B A)
(= E 2))
error_target_7_0) :named interface_C_154_0_to_error_target_7_0))
(rule (! (=> (and (summary_0_function_f__153_154_0 E B A D A C)
(interface_C_154_0 B A)
(= E 3))
error_target_8_0) :named interface_C_154_0_to_error_target_8_0))
(rule (! (=> (and (summary_0_function_f__153_154_0 E B A D A C)
(interface_C_154_0 B A)
(= E 4))
error_target_9_0) :named interface_C_154_0_to_error_target_9_0))
(rule (! (=> (and (summary_0_function_f__153_154_0 E B A D A C)
(interface_C_154_0 B A)
(= E 5))
error_target_10_0) :named interface_C_154_0_to_error_target_10_0))
(query error_target_10_0 :print-certificate true)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment