script_provider.smt2 152 KB
Newer Older
1
(set-info :smt-lib-version 2.6)
2
(set-logic UFDTNIA)
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
(set-info :source |

From the test suite for the Move Prover, a verifier for smart contracts in the
Move programming language.  A paper about the tool is here:
https://doi.org/10.1007/978-3-030-53288-8_7

The Move Prover code and tests are available at:
https://github.com/diem/diem/tree/main/language/move-prover

The benchmarks were generated using the master branch and standard test suite
as of Dec 17, 2020.  Submitted by Clark Barrett <barrett@cs.stanford.edu>.

|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")

(declare-sort T@$TypeName 0)
(declare-sort |T@[Int]$TypeValue| 0)
(declare-datatypes ((T@$TypeValue 0)(T@$TypeValueArray 0)) ((($BooleanType ) ($IntegerType ) ($AddressType ) ($StrType ) ($VectorType (|t#$VectorType| T@$TypeValue) ) ($StructType (|name#$StructType| T@$TypeName) (|ts#$StructType| T@$TypeValueArray) ) ($TypeType ) ($ErrorType ) ) (($TypeValueArray (|v#$TypeValueArray| |T@[Int]$TypeValue|) (|l#$TypeValueArray| Int) ) ) ))
(declare-sort |T@[Int]$Value| 0)
(declare-datatypes ((T@$Value 0)(T@$ValueArray 0)) ((($Boolean (|b#$Boolean| Bool) ) ($Integer (|i#$Integer| Int) ) ($Address (|a#$Address| Int) ) ($Vector (|v#$Vector| T@$ValueArray) ) ($Range (|lb#$Range| T@$Value) (|ub#$Range| T@$Value) ) ($Type (|t#$Type| T@$TypeValue) ) ($Error ) ) (($ValueArray (|v#$ValueArray| |T@[Int]$Value|) (|l#$ValueArray| Int) ) ) ))
(declare-sort |T@[$TypeValueArray,Int]Bool| 0)
(declare-sort |T@[$TypeValueArray,Int]$Value| 0)
(declare-datatypes ((T@$Memory 0)) ((($Memory (|domain#$Memory| |T@[$TypeValueArray,Int]Bool|) (|contents#$Memory| |T@[$TypeValueArray,Int]$Value|) ) ) ))
(declare-datatypes ((T@$Location 0)) ((($Global (|ts#$Global| T@$TypeValueArray) (|a#$Global| Int) ) ($Local (|i#$Local| Int) ) ($Param (|i#$Param| Int) ) ) ))
(declare-sort |T@[Int]Int| 0)
(declare-datatypes ((T@$Path 0)) ((($Path (|p#$Path| |T@[Int]Int|) (|size#$Path| Int) ) ) ))
(declare-datatypes ((T@$Mutation 0)) ((($Mutation (|l#$Mutation| T@$Location) (|p#$Mutation| T@$Path) (|v#$Mutation| T@$Value) ) ) ))
(declare-fun $TestGlobalVars_S () T@$TypeName)
(declare-fun $TestGlobalVars_T () T@$TypeName)
(declare-fun $DebugTrackLocal (Int Int Int T@$Value) Bool)
(declare-fun $DebugTrackAbort (Int Int Int) Bool)
(declare-fun $DebugTrackExp (Int Int T@$Value) T@$Value)
(declare-fun $EmptyPath () T@$Path)
(declare-fun $EmptyTypeValueArray () T@$TypeValueArray)
(declare-fun $MapConstTypeValue (T@$TypeValue) |T@[Int]$TypeValue|)
(declare-fun $MAX_U8 () Int)
(declare-fun $MAX_U64 () Int)
(declare-fun $MAX_U128 () Int)
(declare-fun $EmptyValueArray () T@$ValueArray)
(declare-fun $MapConstValue (T@$Value) |T@[Int]$Value|)
(declare-fun $StratificationDepth () Int)
(declare-fun $IsEqual_stratified (T@$Value T@$Value) Bool)
(declare-fun $IsEqual_level1 (T@$Value T@$Value) Bool)
(declare-fun |Select_[$int]$Value| (|T@[Int]$Value| Int) T@$Value)
(declare-fun $IsEqual_level2 (T@$Value T@$Value) Bool)
(declare-fun $ReadValue_stratified (T@$Path T@$Value) T@$Value)
(declare-fun $ReadValue_level1 (T@$Path T@$Value) T@$Value)
(declare-fun |Select_[$int]$int| (|T@[Int]Int| Int) Int)
(declare-fun $ReadValue_level2 (T@$Path T@$Value) T@$Value)
(declare-fun $UpdateValue_stratified (T@$Path Int T@$Value T@$Value) T@$Value)
(declare-fun |Store_[$int]$Value| (|T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
(assert (forall ( ( ?x0 |T@[Int]$Value|) ( ?x1 Int) ( ?x2 T@$Value)) (= (|Select_[$int]$Value| (|Store_[$int]$Value| ?x0 ?x1 ?x2) ?x1)  ?x2)))
(assert (forall ( ( ?x0 |T@[Int]$Value|) ( ?x1 Int) ( ?y1 Int) ( ?x2 T@$Value)) (=>  (not (= ?x1 ?y1)) (= (|Select_[$int]$Value| (|Store_[$int]$Value| ?x0 ?x1 ?x2) ?y1) (|Select_[$int]$Value| ?x0 ?y1)))))
(declare-fun $UpdateValue_level1 (T@$Path Int T@$Value T@$Value) T@$Value)
(declare-fun $UpdateValue_level2 (T@$Path Int T@$Value T@$Value) T@$Value)
(declare-fun $IsPathPrefix_stratified (T@$Path T@$Path) Bool)
(declare-fun $IsPathPrefix_level1 (T@$Path T@$Path) Bool)
(declare-fun $IsPathPrefix_level2 (T@$Path T@$Path) Bool)
(declare-fun $ConcatPath_stratified (T@$Path T@$Path) T@$Path)
(declare-fun $ConcatPath_level1 (T@$Path T@$Path) T@$Path)
(declare-fun |Store_[$int]$int| (|T@[Int]Int| Int Int) |T@[Int]Int|)
(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?x2 Int)) (= (|Select_[$int]$int| (|Store_[$int]$int| ?x0 ?x1 ?x2) ?x1)  ?x2)))
(assert (forall ( ( ?x0 |T@[Int]Int|) ( ?x1 Int) ( ?y1 Int) ( ?x2 Int)) (=>  (not (= ?x1 ?y1)) (= (|Select_[$int]$int| (|Store_[$int]$int| ?x0 ?x1 ?x2) ?y1) (|Select_[$int]$int| ?x0 ?y1)))))
(declare-fun $ConcatPath_level2 (T@$Path T@$Path) T@$Path)
(declare-fun $ConstMemoryDomain (Bool) |T@[$TypeValueArray,Int]Bool|)
(declare-fun |lambda#5| (Bool) |T@[$TypeValueArray,Int]Bool|)
(declare-fun $EmptyMemory () T@$Memory)
(declare-fun $ConstMemoryContent (T@$Value) |T@[$TypeValueArray,Int]$Value|)
(declare-fun $EXEC_FAILURE_CODE () Int)
(declare-fun $power_of_2 (T@$Value) Int)
(declare-fun $shl (T@$Value T@$Value) T@$Value)
(declare-fun $shr (T@$Value T@$Value) T@$Value)
(declare-fun $Vector_$empty (T@$TypeValue) T@$Value)
(declare-fun $Vector_$push_back (T@$TypeValue T@$Value T@$Value) T@$Value)
(declare-fun $Vector_$pop_back (T@$TypeValue T@$Value) T@$Value)
(declare-fun $Vector_$length (T@$TypeValue T@$Value) T@$Value)
(declare-fun $Vector_$borrow (T@$TypeValue T@$Value T@$Value) T@$Value)
(declare-fun $Vector_$borrow_mut (T@$TypeValue T@$Value T@$Value) T@$Value)
(declare-fun $Vector_$swap (T@$TypeValue T@$Value T@$Value T@$Value) T@$Value)
(declare-fun $Hash_sha2_core (T@$Value) T@$Value)
(declare-fun $Hash_sha3_core (T@$Value) T@$Value)
(declare-fun $Signature_$ed25519_validate_pubkey (T@$Value) T@$Value)
(declare-fun $Signature_$ed25519_verify (T@$Value T@$Value T@$Value) T@$Value)
(declare-fun $BCS_serialize_core (T@$Value) T@$Value)
(declare-fun $BCS_serialize_core_inv (T@$Value) T@$Value)
(declare-fun $serialized_address_len () Int)
(declare-fun $TestGlobalVars_S_x () Int)
(declare-fun $TestGlobalVars_S_type_value () T@$TypeValue)
(declare-fun $TestGlobalVars_T_i () Int)
(declare-fun $TestGlobalVars_T_type_value () T@$TypeValue)
(declare-fun |lambda#0| (Int Int |T@[Int]$Value| T@$Value) |T@[Int]$Value|)
(declare-fun |lambda#1| (Int Int Int |T@[Int]$Value| |T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
(declare-fun |lambda#2| (Int Int Int |T@[Int]$Value| |T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
(declare-fun |lambda#3| (Int Int |T@[Int]$Value| Int Int T@$Value) |T@[Int]$Value|)
(declare-fun |lambda#4| (Int Int |T@[Int]$Value| Int T@$Value) |T@[Int]$Value|)
(declare-fun |Select_[$TypeValueArray,$int]$bool| (|T@[$TypeValueArray,Int]Bool| T@$TypeValueArray Int) Bool)
(assert (distinct $TestGlobalVars_S $TestGlobalVars_T)
)
(assert (forall ((file_id Int) (byte_index Int) (var_idx Int) ($Value T@$Value) ) (! (= ($DebugTrackLocal file_id byte_index var_idx $Value) true) :pattern ( ($DebugTrackLocal file_id byte_index var_idx $Value))
)))
(assert (forall ((file_id@@0 Int) (byte_index@@0 Int) (code Int) ) (! (= ($DebugTrackAbort file_id@@0 byte_index@@0 code) true) :pattern ( ($DebugTrackAbort file_id@@0 byte_index@@0 code))
)))
(assert (forall ((module_id Int) (node_id Int) ($Value@@0 T@$Value) ) (! (= ($DebugTrackExp module_id node_id $Value@@0) $Value@@0) :pattern ( ($DebugTrackExp module_id node_id $Value@@0))
)))
(assert (= (|size#$Path| $EmptyPath) 0))
(assert (= (|l#$TypeValueArray| $EmptyTypeValueArray) 0))
(assert (= (|v#$TypeValueArray| $EmptyTypeValueArray) ($MapConstTypeValue $ErrorType)))
(assert (= $MAX_U8 255))
(assert (= $MAX_U64 18446744073709551615))
(assert (= $MAX_U128 340282366920938463463374607431768211455))
(assert (= (|l#$ValueArray| $EmptyValueArray) 0))
(assert (= (|v#$ValueArray| $EmptyValueArray) ($MapConstValue $Error)))
(assert (= $StratificationDepth 4))
117
(assert (forall ((v1 T@$Value) (v2 T@$Value) ) (! (= ($IsEqual_stratified v1 v2)  (or (= v1 v2) (and (and (and ((_ is $Vector) v1) ((_ is $Vector) v2)) (= (|l#$ValueArray| (|v#$Vector| v1)) (|l#$ValueArray| (|v#$Vector| v2)))) (forall ((i Int) )  (=> (and (<= 0 i) (< i (|l#$ValueArray| (|v#$Vector| v1)))) ($IsEqual_level1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1)) i) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2)) i))))))) :pattern ( ($IsEqual_stratified v1 v2))
118
)))
119
(assert (forall ((v1@@0 T@$Value) (v2@@0 T@$Value) ) (! (= ($IsEqual_level1 v1@@0 v2@@0)  (or (= v1@@0 v2@@0) (and (and (and ((_ is $Vector) v1@@0) ((_ is $Vector) v2@@0)) (= (|l#$ValueArray| (|v#$Vector| v1@@0)) (|l#$ValueArray| (|v#$Vector| v2@@0)))) (forall ((i@@0 Int) )  (=> (and (<= 0 i@@0) (< i@@0 (|l#$ValueArray| (|v#$Vector| v1@@0)))) ($IsEqual_level2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1@@0)) i@@0) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2@@0)) i@@0))))))) :pattern ( ($IsEqual_level1 v1@@0 v2@@0))
120
)))
121
(assert (forall ((v1@@1 T@$Value) (v2@@1 T@$Value) ) (! (= ($IsEqual_level2 v1@@1 v2@@1)  (or (= v1@@1 v2@@1) (and (and (and ((_ is $Vector) v1@@1) ((_ is $Vector) v2@@1)) (= (|l#$ValueArray| (|v#$Vector| v1@@1)) (|l#$ValueArray| (|v#$Vector| v2@@1)))) (forall ((i@@1 Int) )  (=> (and (<= 0 i@@1) (< i@@1 (|l#$ValueArray| (|v#$Vector| v1@@1)))) (= (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v1@@1)) i@@1) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v2@@1)) i@@1))))))) :pattern ( ($IsEqual_level2 v1@@1 v2@@1))
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
)))
(assert (forall ((p T@$Path) (v T@$Value) ) (! (= ($ReadValue_stratified p v) (ite (= 0 (|size#$Path| p)) v ($ReadValue_level1 p (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v)) (|Select_[$int]$int| (|p#$Path| p) 0))))) :pattern ( ($ReadValue_stratified p v))
)))
(assert (forall ((p@@0 T@$Path) (v@@0 T@$Value) ) (! (= ($ReadValue_level1 p@@0 v@@0) (ite (= 1 (|size#$Path| p@@0)) v@@0 ($ReadValue_level2 p@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@0)) (|Select_[$int]$int| (|p#$Path| p@@0) 1))))) :pattern ( ($ReadValue_level1 p@@0 v@@0))
)))
(assert (forall ((p@@1 T@$Path) (v@@1 T@$Value) ) (! (= ($ReadValue_level2 p@@1 v@@1) (ite (= 2 (|size#$Path| p@@1)) v@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@1)) (|Select_[$int]$int| (|p#$Path| p@@1) 2)))) :pattern ( ($ReadValue_level2 p@@1 v@@1))
)))
(assert (forall ((p@@2 T@$Path) (offset Int) (v@@2 T@$Value) (new_v T@$Value) ) (! (= ($UpdateValue_stratified p@@2 offset v@@2 new_v) (let ((poffset (+ offset 0)))
(ite (= poffset (|size#$Path| p@@2)) new_v ($Vector ($ValueArray (|Store_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@2)) (|Select_[$int]$int| (|p#$Path| p@@2) poffset) ($UpdateValue_level1 p@@2 offset (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@2)) (|Select_[$int]$int| (|p#$Path| p@@2) poffset)) new_v)) (|l#$ValueArray| (|v#$Vector| v@@2))))))) :pattern ( ($UpdateValue_stratified p@@2 offset v@@2 new_v))
)))
(assert (forall ((p@@3 T@$Path) (offset@@0 Int) (v@@3 T@$Value) (new_v@@0 T@$Value) ) (! (= ($UpdateValue_level1 p@@3 offset@@0 v@@3 new_v@@0) (let ((poffset@@0 (+ offset@@0 1)))
(ite (= poffset@@0 (|size#$Path| p@@3)) new_v@@0 ($Vector ($ValueArray (|Store_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@3)) (|Select_[$int]$int| (|p#$Path| p@@3) poffset@@0) ($UpdateValue_level2 p@@3 offset@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@3)) (|Select_[$int]$int| (|p#$Path| p@@3) poffset@@0)) new_v@@0)) (|l#$ValueArray| (|v#$Vector| v@@3))))))) :pattern ( ($UpdateValue_level1 p@@3 offset@@0 v@@3 new_v@@0))
)))
(assert (forall ((p@@4 T@$Path) (offset@@1 Int) (v@@4 T@$Value) (new_v@@1 T@$Value) ) (! (= ($UpdateValue_level2 p@@4 offset@@1 v@@4 new_v@@1) (let ((poffset@@1 (+ offset@@1 2)))
(ite (= poffset@@1 (|size#$Path| p@@4)) new_v@@1 ($Vector ($ValueArray (|Store_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@4)) (|Select_[$int]$int| (|p#$Path| p@@4) poffset@@1) new_v@@1) (|l#$ValueArray| (|v#$Vector| v@@4))))))) :pattern ( ($UpdateValue_level2 p@@4 offset@@1 v@@4 new_v@@1))
)))
(assert (forall ((p1 T@$Path) (p2 T@$Path) ) (! (= ($IsPathPrefix_stratified p1 p2) (ite (= 0 (|size#$Path| p1)) true (ite (= (|Select_[$int]$int| (|p#$Path| p1) 0) (|Select_[$int]$int| (|p#$Path| p2) 0)) ($IsPathPrefix_level1 p1 p2) false))) :pattern ( ($IsPathPrefix_stratified p1 p2))
)))
(assert (forall ((p1@@0 T@$Path) (p2@@0 T@$Path) ) (! (= ($IsPathPrefix_level1 p1@@0 p2@@0) (ite (= 1 (|size#$Path| p1@@0)) true (ite (= (|Select_[$int]$int| (|p#$Path| p1@@0) 1) (|Select_[$int]$int| (|p#$Path| p2@@0) 1)) ($IsPathPrefix_level2 p1@@0 p2@@0) false))) :pattern ( ($IsPathPrefix_level1 p1@@0 p2@@0))
)))
(assert (forall ((p1@@1 T@$Path) (p2@@1 T@$Path) ) (! (= ($IsPathPrefix_level2 p1@@1 p2@@1) (ite (= 2 (|size#$Path| p1@@1)) true (ite (= (|Select_[$int]$int| (|p#$Path| p1@@1) 2) (|Select_[$int]$int| (|p#$Path| p2@@1) 2)) true false))) :pattern ( ($IsPathPrefix_level2 p1@@1 p2@@1))
)))
(assert (forall ((p1@@2 T@$Path) (p2@@2 T@$Path) ) (! (= ($ConcatPath_stratified p1@@2 p2@@2) (ite (= 0 (|size#$Path| p2@@2)) p1@@2 ($ConcatPath_level1 ($Path (|Store_[$int]$int| (|p#$Path| p1@@2) (|size#$Path| p1@@2) (|Select_[$int]$int| (|p#$Path| p2@@2) 0)) (+ (|size#$Path| p1@@2) 1)) p2@@2))) :pattern ( ($ConcatPath_stratified p1@@2 p2@@2))
)))
(assert (forall ((p1@@3 T@$Path) (p2@@3 T@$Path) ) (! (= ($ConcatPath_level1 p1@@3 p2@@3) (ite (= 1 (|size#$Path| p2@@3)) p1@@3 ($ConcatPath_level2 ($Path (|Store_[$int]$int| (|p#$Path| p1@@3) (|size#$Path| p1@@3) (|Select_[$int]$int| (|p#$Path| p2@@3) 1)) (+ (|size#$Path| p1@@3) 1)) p2@@3))) :pattern ( ($ConcatPath_level1 p1@@3 p2@@3))
)))
(assert (forall ((p1@@4 T@$Path) (p2@@4 T@$Path) ) (! (= ($ConcatPath_level2 p1@@4 p2@@4) (ite (= 2 (|size#$Path| p2@@4)) p1@@4 ($Path (|Store_[$int]$int| (|p#$Path| p1@@4) (|size#$Path| p1@@4) (|Select_[$int]$int| (|p#$Path| p2@@4) 2)) (+ (|size#$Path| p1@@4) 1)))) :pattern ( ($ConcatPath_level2 p1@@4 p2@@4))
)))
(assert (= ($ConstMemoryDomain false) (|lambda#5| false)))
(assert (= ($ConstMemoryDomain true) (|lambda#5| true)))
(assert (= (|domain#$Memory| $EmptyMemory) ($ConstMemoryDomain false)))
(assert (= (|contents#$Memory| $EmptyMemory) ($ConstMemoryContent $Error)))
(assert (= $EXEC_FAILURE_CODE (- 0 1)))
(assert (forall ((power T@$Value) ) (! (= ($power_of_2 power) (let ((p@@5 (|i#$Integer| power)))
(ite (= p@@5 8) 256 (ite (= p@@5 16) 65536 (ite (= p@@5 32) 4294967296 (ite (= p@@5 64) 18446744073709551616 (- 0 1))))))) :pattern ( ($power_of_2 power))
)))
(assert (forall ((src1 T@$Value) (src2 T@$Value) ) (! (= ($shl src1 src2) (let ((po2 ($power_of_2 src2)))
($Integer (* (|i#$Integer| src1) po2)))) :pattern ( ($shl src1 src2))
)))
(assert (forall ((src1@@0 T@$Value) (src2@@0 T@$Value) ) (! (= ($shr src1@@0 src2@@0) (let ((po2@@0 ($power_of_2 src2@@0)))
($Integer (div (|i#$Integer| src1@@0) po2@@0)))) :pattern ( ($shr src1@@0 src2@@0))
)))
(assert (forall ((ta T@$TypeValue) ) (! (= ($Vector_$empty ta) ($Vector $EmptyValueArray)) :pattern ( ($Vector_$empty ta))
)))
(assert (forall ((ta@@0 T@$TypeValue) (v@@5 T@$Value) (val T@$Value) ) (! (= ($Vector_$push_back ta@@0 v@@5 val) ($Vector (let ((len (|l#$ValueArray| (|v#$Vector| v@@5))))
($ValueArray (|Store_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@5)) len val) (+ len 1))))) :pattern ( ($Vector_$push_back ta@@0 v@@5 val))
)))
(assert (forall ((ta@@1 T@$TypeValue) (v@@6 T@$Value) ) (! (= ($Vector_$pop_back ta@@1 v@@6) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@6)) (- (|l#$ValueArray| (|v#$Vector| v@@6)) 1))) :pattern ( ($Vector_$pop_back ta@@1 v@@6))
)))
(assert (forall ((ta@@2 T@$TypeValue) (v@@7 T@$Value) ) (! (= ($Vector_$length ta@@2 v@@7) ($Integer (|l#$ValueArray| (|v#$Vector| v@@7)))) :pattern ( ($Vector_$length ta@@2 v@@7))
)))
(assert (forall ((ta@@3 T@$TypeValue) (v@@8 T@$Value) (i@@2 T@$Value) ) (! (= ($Vector_$borrow ta@@3 v@@8 i@@2) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@8)) (|i#$Integer| i@@2))) :pattern ( ($Vector_$borrow ta@@3 v@@8 i@@2))
)))
(assert (forall ((ta@@4 T@$TypeValue) (v@@9 T@$Value) (i@@3 T@$Value) ) (! (= ($Vector_$borrow_mut ta@@4 v@@9 i@@3) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@9)) (|i#$Integer| i@@3))) :pattern ( ($Vector_$borrow_mut ta@@4 v@@9 i@@3))
)))
(assert (forall ((ta@@5 T@$TypeValue) (v@@10 T@$Value) (i@@4 T@$Value) (j T@$Value) ) (! (= ($Vector_$swap ta@@5 v@@10 i@@4 j) ($Vector ($ValueArray (|Store_[$int]$Value| (|Store_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@10)) (|i#$Integer| i@@4) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@10)) (|i#$Integer| j))) (|i#$Integer| j) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| v@@10)) (|i#$Integer| i@@4))) (|l#$ValueArray| (|v#$Vector| v@@10))))) :pattern ( ($Vector_$swap ta@@5 v@@10 i@@4 j))
)))
179
(assert (forall ((v1@@2 T@$Value) (v2@@2 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@2) (let ((va (|v#$Vector| v1@@2)))
180
181
(let ((l (|l#$ValueArray| va)))
 (and (and (<= 0 l) (<= l $MAX_U64)) (forall ((x Int) ) (!  (=> (or (< x 0) (>= x l)) (= (|Select_[$int]$Value| (|v#$ValueArray| va) x) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va) x))
182
)))))) (and ((_ is $Vector) v2@@2) (let ((va@@0 (|v#$Vector| v2@@2)))
183
184
185
(let ((l@@0 (|l#$ValueArray| va@@0)))
 (and (and (<= 0 l@@0) (<= l@@0 $MAX_U64)) (forall ((x@@0 Int) ) (!  (=> (or (< x@@0 0) (>= x@@0 l@@0)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@0) x@@0) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@0) x@@0))
))))))) ($IsEqual_stratified v1@@2 v2@@2)) ($IsEqual_stratified ($Hash_sha2_core v1@@2) ($Hash_sha2_core v2@@2)))))
186
(assert (forall ((v1@@3 T@$Value) (v2@@3 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@3) (let ((va@@1 (|v#$Vector| v1@@3)))
187
188
(let ((l@@1 (|l#$ValueArray| va@@1)))
 (and (and (<= 0 l@@1) (<= l@@1 $MAX_U64)) (forall ((x@@1 Int) ) (!  (=> (or (< x@@1 0) (>= x@@1 l@@1)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@1) x@@1) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@1) x@@1))
189
)))))) (and ((_ is $Vector) v2@@3) (let ((va@@2 (|v#$Vector| v2@@3)))
190
191
192
(let ((l@@2 (|l#$ValueArray| va@@2)))
 (and (and (<= 0 l@@2) (<= l@@2 $MAX_U64)) (forall ((x@@2 Int) ) (!  (=> (or (< x@@2 0) (>= x@@2 l@@2)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@2) x@@2) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@2) x@@2))
))))))) ($IsEqual_stratified ($Hash_sha2_core v1@@3) ($Hash_sha2_core v2@@3))) ($IsEqual_stratified v1@@3 v2@@3))))
193
(assert (forall ((v1@@4 T@$Value) (v2@@4 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@4) (let ((va@@3 (|v#$Vector| v1@@4)))
194
195
(let ((l@@3 (|l#$ValueArray| va@@3)))
 (and (and (<= 0 l@@3) (<= l@@3 $MAX_U64)) (forall ((x@@3 Int) ) (!  (=> (or (< x@@3 0) (>= x@@3 l@@3)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@3) x@@3) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@3) x@@3))
196
)))))) (and ((_ is $Vector) v2@@4) (let ((va@@4 (|v#$Vector| v2@@4)))
197
198
199
(let ((l@@4 (|l#$ValueArray| va@@4)))
 (and (and (<= 0 l@@4) (<= l@@4 $MAX_U64)) (forall ((x@@4 Int) ) (!  (=> (or (< x@@4 0) (>= x@@4 l@@4)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@4) x@@4) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@4) x@@4))
))))))) ($IsEqual_stratified v1@@4 v2@@4)) ($IsEqual_stratified ($Hash_sha3_core v1@@4) ($Hash_sha3_core v2@@4)))))
200
(assert (forall ((v1@@5 T@$Value) (v2@@5 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@5) (let ((va@@5 (|v#$Vector| v1@@5)))
201
202
(let ((l@@5 (|l#$ValueArray| va@@5)))
 (and (and (<= 0 l@@5) (<= l@@5 $MAX_U64)) (forall ((x@@5 Int) ) (!  (=> (or (< x@@5 0) (>= x@@5 l@@5)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@5) x@@5) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@5) x@@5))
203
)))))) (and ((_ is $Vector) v2@@5) (let ((va@@6 (|v#$Vector| v2@@5)))
204
205
206
(let ((l@@6 (|l#$ValueArray| va@@6)))
 (and (and (<= 0 l@@6) (<= l@@6 $MAX_U64)) (forall ((x@@6 Int) ) (!  (=> (or (< x@@6 0) (>= x@@6 l@@6)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@6) x@@6) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@6) x@@6))
))))))) ($IsEqual_stratified ($Hash_sha3_core v1@@5) ($Hash_sha3_core v2@@5))) ($IsEqual_stratified v1@@5 v2@@5))))
207
208
(assert (forall ((public_key T@$Value) ) ((_ is $Boolean) ($Signature_$ed25519_validate_pubkey public_key))))
(assert (forall ((signature T@$Value) (public_key@@0 T@$Value) (message T@$Value) ) ((_ is $Boolean) ($Signature_$ed25519_verify signature public_key@@0 message))))
209
210
211
(assert (forall ((v1@@6 T@$Value) (v2@@6 T@$Value) )  (=> ($IsEqual_stratified v1@@6 v2@@6) (= ($BCS_serialize_core v1@@6) ($BCS_serialize_core v2@@6)))))
(assert (forall ((v@@11 T@$Value) ) (= ($BCS_serialize_core_inv ($BCS_serialize_core v@@11)) v@@11)))
(assert (forall ((v@@12 T@$Value) ) (let ((r ($BCS_serialize_core v@@12)))
212
 (and (and (and ((_ is $Vector) r) (let ((va@@7 (|v#$Vector| r)))
213
214
(let ((l@@7 (|l#$ValueArray| va@@7)))
 (and (and (<= 0 l@@7) (<= l@@7 $MAX_U64)) (forall ((x@@7 Int) ) (!  (=> (or (< x@@7 0) (>= x@@7 l@@7)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@7) x@@7) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@7) x@@7))
215
)))))) (forall ((i@@5 Int) ) (!  (=> (and (<= 0 i@@5) (< i@@5 (|l#$ValueArray| (|v#$Vector| r)))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| r)) i@@5))
216
217
))) (> (|l#$ValueArray| (|v#$Vector| r)) 0)))))
(assert (forall ((v@@13 T@$Value) ) (let ((r@@0 ($BCS_serialize_core v@@13)))
218
 (=> ((_ is $Address) v@@13) (= (|l#$ValueArray| (|v#$Vector| r@@0)) $serialized_address_len)))))
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
(assert (= $TestGlobalVars_S_x 0))
(assert (= $TestGlobalVars_S_type_value ($StructType $TestGlobalVars_S $EmptyTypeValueArray)))
(assert (= $TestGlobalVars_T_i 0))
(assert (= $TestGlobalVars_T_type_value ($StructType $TestGlobalVars_T $EmptyTypeValueArray)))
(assert (forall ((i@@6 Int) (|l#0| Int) (|l#1| Int) (|l#2| |T@[Int]$Value|) (|l#3| T@$Value) ) (! (= (|Select_[$int]$Value| (|lambda#0| |l#0| |l#1| |l#2| |l#3|) i@@6) (ite  (and (>= i@@6 |l#0|) (< i@@6 |l#1|)) (|Select_[$int]$Value| |l#2| i@@6) |l#3|)) :pattern ( (|Select_[$int]$Value| (|lambda#0| |l#0| |l#1| |l#2| |l#3|) i@@6))
)))
(assert (forall ((j@@0 Int) (|l#0@@0| Int) (|l#1@@0| Int) (|l#2@@0| Int) (|l#3@@0| |T@[Int]$Value|) (|l#4| |T@[Int]$Value|) (|l#5| Int) (|l#6| T@$Value) ) (! (= (|Select_[$int]$Value| (|lambda#1| |l#0@@0| |l#1@@0| |l#2@@0| |l#3@@0| |l#4| |l#5| |l#6|) j@@0) (ite  (and (>= j@@0 |l#0@@0|) (< j@@0 |l#1@@0|)) (ite (< j@@0 |l#2@@0|) (|Select_[$int]$Value| |l#3@@0| j@@0) (|Select_[$int]$Value| |l#4| (+ j@@0 |l#5|))) |l#6|)) :pattern ( (|Select_[$int]$Value| (|lambda#1| |l#0@@0| |l#1@@0| |l#2@@0| |l#3@@0| |l#4| |l#5| |l#6|) j@@0))
)))
(assert (forall ((i@@7 Int) (|l#0@@1| Int) (|l#1@@1| Int) (|l#2@@1| Int) (|l#3@@1| |T@[Int]$Value|) (|l#4@@0| |T@[Int]$Value|) (|l#5@@0| Int) (|l#6@@0| T@$Value) ) (! (= (|Select_[$int]$Value| (|lambda#2| |l#0@@1| |l#1@@1| |l#2@@1| |l#3@@1| |l#4@@0| |l#5@@0| |l#6@@0|) i@@7) (ite  (and (>= i@@7 |l#0@@1|) (< i@@7 |l#1@@1|)) (ite (< i@@7 |l#2@@1|) (|Select_[$int]$Value| |l#3@@1| i@@7) (|Select_[$int]$Value| |l#4@@0| (- i@@7 |l#5@@0|))) |l#6@@0|)) :pattern ( (|Select_[$int]$Value| (|lambda#2| |l#0@@1| |l#1@@1| |l#2@@1| |l#3@@1| |l#4@@0| |l#5@@0| |l#6@@0|) i@@7))
)))
(assert (forall ((i@@8 Int) (|l#0@@2| Int) (|l#1@@2| Int) (|l#2@@2| |T@[Int]$Value|) (|l#3@@2| Int) (|l#4@@1| Int) (|l#5@@1| T@$Value) ) (! (= (|Select_[$int]$Value| (|lambda#3| |l#0@@2| |l#1@@2| |l#2@@2| |l#3@@2| |l#4@@1| |l#5@@1|) i@@8) (ite  (and (<= |l#0@@2| i@@8) (< i@@8 |l#1@@2|)) (|Select_[$int]$Value| |l#2@@2| (- (- |l#3@@2| i@@8) |l#4@@1|)) |l#5@@1|)) :pattern ( (|Select_[$int]$Value| (|lambda#3| |l#0@@2| |l#1@@2| |l#2@@2| |l#3@@2| |l#4@@1| |l#5@@1|) i@@8))
)))
(assert (forall ((k Int) (|l#0@@3| Int) (|l#1@@3| Int) (|l#2@@3| |T@[Int]$Value|) (|l#3@@3| Int) (|l#4@@2| T@$Value) ) (! (= (|Select_[$int]$Value| (|lambda#4| |l#0@@3| |l#1@@3| |l#2@@3| |l#3@@3| |l#4@@2|) k) (ite  (and (<= |l#0@@3| k) (< k |l#1@@3|)) (|Select_[$int]$Value| |l#2@@3| (+ |l#3@@3| k)) |l#4@@2|)) :pattern ( (|Select_[$int]$Value| (|lambda#4| |l#0@@3| |l#1@@3| |l#2@@3| |l#3@@3| |l#4@@2|) k))
)))
(assert (forall ((ta@@6 T@$TypeValueArray) (i@@9 Int) (|l#0@@4| Bool) ) (! (= (|Select_[$TypeValueArray,$int]$bool| (|lambda#5| |l#0@@4|) ta@@6 i@@9) |l#0@@4|) :pattern ( (|Select_[$TypeValueArray,$int]$bool| (|lambda#5| |l#0@@4|) ta@@6 i@@9))
)))
(declare-fun ControlFlow (Int Int) Int)
(declare-fun $TestGlobalVars_sum_of_T@4 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$1$$struct@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_unpack$0$i@1 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@3 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@2 () T@$Value)
(declare-fun inline$$TestGlobalVars_combi_correct_$def_verify$0$$t6@1 () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1| () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$0$$struct@1 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$pack_ref$0$$after@0 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1| () T@$Mutation)
(declare-fun inline$$TestGlobalVars_combi_correct_$def_verify$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1 () T@$Mutation)
(declare-fun inline$$TestGlobalVars_combi_correct_$def_verify$0$$t4@1 () T@$Value)
(declare-fun inline$$BorrowField$0$p@1 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1 () Int)
(declare-fun inline$$BorrowField$0$p@2 () T@$Path)
(declare-fun $TestGlobalVars_sum_of_T@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$unpack_ref$0$$before@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_combi_correct_$def_verify$0$$t3@1 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_S () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 29259) (let ((anon0$2_correct  (=> (= (ControlFlow 0 15080) (- 0 30167)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@4 ($Integer (- (|i#$Integer| ($Integer (+ (|i#$Integer| ($Integer (- (|i#$Integer| ($Integer (+ (|i#$Integer| ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| ($Integer 2))))) (|i#$Integer| ($Integer 3))))) (|i#$Integer| ($Integer 3))))) (|i#$Integer| ($Integer 4))))) (|i#$Integer| ($Integer 2)))))))))))
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 15044) 15080)) anon0$2_correct)))
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 15054) 15080) anon0$2_correct)))
268
(let ((inline$$TestGlobalVars_T_unpack$0$anon0_correct  (=> (and ((_ is $Vector) inline$$TestGlobalVars_T_pack$1$$struct@1) (= inline$$TestGlobalVars_T_unpack$0$i@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$1$$struct@1)) $TestGlobalVars_T_i))) (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_T_unpack$0$i@1) (>= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1) $MAX_U64)) (= $TestGlobalVars_sum_of_T@4 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T@3) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$1$$struct@1)) $TestGlobalVars_T_i)))))) (and (=> (= (ControlFlow 0 15028) 15054) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 15028) 15044) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon9_Else_correct))))))
269
270
271
272
273
(let ((inline$$TestGlobalVars_T_pack$1$anon3_correct  (=> (and (= $TestGlobalVars_sum_of_T@3 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T@2) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$1$$struct@1)) $TestGlobalVars_T_i))))) (= (ControlFlow 0 14909) 15028)) inline$$TestGlobalVars_T_unpack$0$anon0_correct)))
(let ((inline$$TestGlobalVars_T_pack$1$anon5_Else_correct  (=> (and (not true) (= (ControlFlow 0 14923) 14909)) inline$$TestGlobalVars_T_pack$1$anon3_correct)))
(let ((inline$$TestGlobalVars_T_pack$1$anon5_Then_correct  (=> (= (ControlFlow 0 14929) 14909) inline$$TestGlobalVars_T_pack$1$anon3_correct)))
(let ((inline$$TestGlobalVars_T_pack$1$anon4_Then_correct  (=> (> 0 0) (and (=> (= (ControlFlow 0 14917) 14929) inline$$TestGlobalVars_T_pack$1$anon5_Then_correct) (=> (= (ControlFlow 0 14917) 14923) inline$$TestGlobalVars_T_pack$1$anon5_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$1$anon4_Else_correct  (=> (and (>= 0 0) (= (ControlFlow 0 14891) 14909)) inline$$TestGlobalVars_T_pack$1$anon3_correct)))
274
(let ((inline$$TestGlobalVars_T_pack$1$anon0_correct  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_combi_correct_$def_verify$0$$t6@1) (>= (|i#$Integer| inline$$TestGlobalVars_combi_correct_$def_verify$0$$t6@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_combi_correct_$def_verify$0$$t6@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$1$$struct@1 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_combi_correct_$def_verify$0$$t6@1) 1)))) (and (=> (= (ControlFlow 0 14883) 14917) inline$$TestGlobalVars_T_pack$1$anon4_Then_correct) (=> (= (ControlFlow 0 14883) 14891) inline$$TestGlobalVars_T_pack$1$anon4_Else_correct)))))
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon4$3_correct  (=> (and (= inline$$TestGlobalVars_combi_correct_$def_verify$0$$t6@1 ($Integer 2)) (= (ControlFlow 0 14935) 14883)) inline$$TestGlobalVars_T_pack$1$anon0_correct)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct  (=> (and (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2|) ($Local 0))) (= (ControlFlow 0 14694) 14935)) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon4$3_correct)))
(let ((inline$$WritebackToValue$0$anon3_Then_correct  (=> (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2|) ($Local 0)) (=> (and (= |inline$$WritebackToValue$0$vdst'@1| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2|) 0 inline$$TestGlobalVars_T_pack$0$$struct@1 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2|))) (= (ControlFlow 0 14720) 14935)) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon4$3_correct))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct  (=> (= $TestGlobalVars_sum_of_T@2 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T@1) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$pack_ref$0$$after@0)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 14597) 14720) inline$$WritebackToValue$0$anon3_Then_correct) (=> (= (ControlFlow 0 14597) 14694) inline$$WritebackToValue$0$anon3_Else_correct)))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct  (=> (and (= inline$$TestGlobalVars_T_$pack_ref$0$$after@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2|)) (= (ControlFlow 0 14579) 14597)) inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct)))
(let ((inline$$WritebackToReference$0$anon3_Else_correct  (=> (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1) (|size#$Path| inline$$WritebackToReference$0$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1 inline$$WritebackToReference$0$srcPath@1))) (=> (and (= |inline$$WritebackToReference$0$dst'@2| inline$$BorrowLoc$0$dst@1) (= (ControlFlow 0 14475) 14579)) inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct  (=> (and (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1) (|size#$Path| inline$$WritebackToReference$0$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1 inline$$WritebackToReference$0$srcPath@1)) (= |inline$$WritebackToReference$0$dst'@1| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1) inline$$WritebackToReference$0$dstPath@1 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1 (|size#$Path| inline$$WritebackToReference$0$dstPath@1) (|v#$Mutation| inline$$BorrowLoc$0$dst@1) (|v#$Mutation| |inline$$WriteRef$0$to'@1|))))) (and (= |inline$$WritebackToReference$0$dst'@2| |inline$$WritebackToReference$0$dst'@1|) (= (ControlFlow 0 14531) 14579))) inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct)))
(let ((inline$$WritebackToReference$0$anon0_correct  (=> (and (= inline$$WritebackToReference$0$srcPath@1 (|p#$Mutation| |inline$$WriteRef$0$to'@1|)) (= inline$$WritebackToReference$0$dstPath@1 (|p#$Mutation| inline$$BorrowLoc$0$dst@1))) (and (=> (= (ControlFlow 0 14439) 14531) inline$$WritebackToReference$0$anon3_Then_correct) (=> (= (ControlFlow 0 14439) 14475) inline$$WritebackToReference$0$anon3_Else_correct)))))
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon8_Else_correct  (=> (and (not true) (= (ControlFlow 0 14302) 14439)) inline$$WritebackToReference$0$anon0_correct)))
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon8_Then_correct  (=> (and (= inline$$TestGlobalVars_combi_correct_$def_verify$0$$trace_temp@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1)) (= (ControlFlow 0 15064) 14439)) inline$$WritebackToReference$0$anon0_correct)))
(let ((inline$$WriteRef$0$anon0_correct  (=> (= |inline$$WriteRef$0$to'@1| ($Mutation (|l#$Mutation| inline$$BorrowField$0$dst@1) (|p#$Mutation| inline$$BorrowField$0$dst@1) inline$$TestGlobalVars_combi_correct_$def_verify$0$$t4@1)) (and (=> (= (ControlFlow 0 14288) 15064) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 14288) 14302) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$BorrowField$0$anon0_correct  (=> (= inline$$BorrowField$0$p@1 (|p#$Mutation| inline$$BorrowLoc$0$dst@1)) (=> (and (and (= inline$$BorrowField$0$size@1 (|size#$Path| inline$$BorrowField$0$p@1)) (= inline$$BorrowField$0$p@2 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1) inline$$BorrowField$0$size@1 $TestGlobalVars_T_i) (+ inline$$BorrowField$0$size@1 1)))) (and (= inline$$BorrowField$0$dst@1 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1) inline$$BorrowField$0$p@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1))) $TestGlobalVars_T_i))) (= (ControlFlow 0 14229) 14288))) inline$$WriteRef$0$anon0_correct))))
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon2$2_correct  (=> (and (= inline$$TestGlobalVars_combi_correct_$def_verify$0$$t4@1 ($Integer 4)) (= (ControlFlow 0 14235) 14229)) inline$$BorrowField$0$anon0_correct)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct  (=> (and (= $TestGlobalVars_sum_of_T@1 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$unpack_ref$0$$before@0)) $TestGlobalVars_T_i))))) (= (ControlFlow 0 14103) 14235)) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon2$2_correct)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct  (=> (and (= inline$$TestGlobalVars_T_$unpack_ref$0$$before@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1)) (= (ControlFlow 0 14081) 14103)) inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct)))
(let ((inline$$BorrowLoc$0$anon0_correct  (=> (and (= inline$$BorrowLoc$0$dst@1 ($Mutation ($Local 0) $EmptyPath inline$$TestGlobalVars_T_pack$0$$struct@1)) (= (ControlFlow 0 14029) 14081)) inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct)))
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 13979) 14029)) inline$$BorrowLoc$0$anon0_correct)))
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 15072) 14029) inline$$BorrowLoc$0$anon0_correct)))
(let ((inline$$TestGlobalVars_T_pack$0$anon3_correct  (=> (= $TestGlobalVars_sum_of_T@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$0$$struct@1)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 13945) 15072) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 13945) 13979) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon7_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Else_correct  (=> (and (not true) (= (ControlFlow 0 13959) 13945)) inline$$TestGlobalVars_T_pack$0$anon3_correct)))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Then_correct  (=> (= (ControlFlow 0 13965) 13945) inline$$TestGlobalVars_T_pack$0$anon3_correct)))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Then_correct  (=> (> 2184 0) (and (=> (= (ControlFlow 0 13953) 13965) inline$$TestGlobalVars_T_pack$0$anon5_Then_correct) (=> (= (ControlFlow 0 13953) 13959) inline$$TestGlobalVars_T_pack$0$anon5_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Else_correct  (=> (and (>= 0 2184) (= (ControlFlow 0 13927) 13945)) inline$$TestGlobalVars_T_pack$0$anon3_correct)))
298
(let ((inline$$TestGlobalVars_T_pack$0$anon0_correct  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_combi_correct_$def_verify$0$$t3@1) (>= (|i#$Integer| inline$$TestGlobalVars_combi_correct_$def_verify$0$$t3@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_combi_correct_$def_verify$0$$t3@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$0$$struct@1 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_combi_correct_$def_verify$0$$t3@1) 1)))) (and (=> (= (ControlFlow 0 13919) 13953) inline$$TestGlobalVars_T_pack$0$anon4_Then_correct) (=> (= (ControlFlow 0 13919) 13927) inline$$TestGlobalVars_T_pack$0$anon4_Else_correct)))))
299
(let ((inline$$TestGlobalVars_combi_correct_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_combi_correct_$def_verify$0$$t3@1 ($Integer 3)) (= (ControlFlow 0 13971) 13919)) inline$$TestGlobalVars_T_pack$0$anon0_correct))))
300
(let ((anon0_correct  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 29259) 13971)) inline$$TestGlobalVars_combi_correct_$def_verify$0$anon0_correct))))
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
anon0_correct)))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $TestGlobalVars_sum_of_T@4@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$1$$struct@1@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_unpack$0$i@1@@0 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@3@@0 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@2@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t6@1 () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@0| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@0| () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$0$$struct@1@@0 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@1@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@0 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@0 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1@@0| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@0 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@0 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@0| () T@$Mutation)
(declare-fun inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1@@0 () T@$Mutation)
(declare-fun inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t4@1 () T@$Value)
(declare-fun inline$$BorrowField$0$p@1@@0 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@0 () Int)
(declare-fun inline$$BorrowField$0$p@2@@0 () T@$Path)
(declare-fun $TestGlobalVars_sum_of_T@0@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t3@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 30254) (let ((anon0$2_correct@@0  (=> (= (ControlFlow 0 16865) (- 0 31114)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@4@@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| ($Integer 2)))))))))))
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 16829) 16865)) anon0$2_correct@@0)))
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 16839) 16865) anon0$2_correct@@0)))
336
(let ((inline$$TestGlobalVars_T_unpack$0$anon0_correct@@0  (=> (and ((_ is $Vector) inline$$TestGlobalVars_T_pack$1$$struct@1@@0) (= inline$$TestGlobalVars_T_unpack$0$i@1@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$1$$struct@1@@0)) $TestGlobalVars_T_i))) (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_T_unpack$0$i@1@@0) (>= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1@@0) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1@@0) $MAX_U64)) (= $TestGlobalVars_sum_of_T@4@@0 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T@3@@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$1$$struct@1@@0)) $TestGlobalVars_T_i)))))) (and (=> (= (ControlFlow 0 16813) 16839) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 16813) 16829) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon9_Else_correct))))))
337
338
339
340
341
(let ((inline$$TestGlobalVars_T_pack$1$anon3_correct@@0  (=> (and (= $TestGlobalVars_sum_of_T@3@@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T@2@@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$1$$struct@1@@0)) $TestGlobalVars_T_i))))) (= (ControlFlow 0 16694) 16813)) inline$$TestGlobalVars_T_unpack$0$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_T_pack$1$anon5_Else_correct@@0  (=> (and (not true) (= (ControlFlow 0 16708) 16694)) inline$$TestGlobalVars_T_pack$1$anon3_correct@@0)))
(let ((inline$$TestGlobalVars_T_pack$1$anon5_Then_correct@@0  (=> (= (ControlFlow 0 16714) 16694) inline$$TestGlobalVars_T_pack$1$anon3_correct@@0)))
(let ((inline$$TestGlobalVars_T_pack$1$anon4_Then_correct@@0  (=> (> 0 0) (and (=> (= (ControlFlow 0 16702) 16714) inline$$TestGlobalVars_T_pack$1$anon5_Then_correct@@0) (=> (= (ControlFlow 0 16702) 16708) inline$$TestGlobalVars_T_pack$1$anon5_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_T_pack$1$anon4_Else_correct@@0  (=> (and (>= 0 0) (= (ControlFlow 0 16676) 16694)) inline$$TestGlobalVars_T_pack$1$anon3_correct@@0)))
342
(let ((inline$$TestGlobalVars_T_pack$1$anon0_correct@@0  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t6@1) (>= (|i#$Integer| inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t6@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t6@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$1$$struct@1@@0 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t6@1) 1)))) (and (=> (= (ControlFlow 0 16668) 16702) inline$$TestGlobalVars_T_pack$1$anon4_Then_correct@@0) (=> (= (ControlFlow 0 16668) 16676) inline$$TestGlobalVars_T_pack$1$anon4_Else_correct@@0)))))
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon4$3_correct  (=> (and (= inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t6@1 ($Integer 2)) (= (ControlFlow 0 16720) 16668)) inline$$TestGlobalVars_T_pack$1$anon0_correct@@0)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@0  (=> (and (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|) ($Local 0))) (= (ControlFlow 0 16479) 16720)) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon4$3_correct)))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@0  (=> (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|) ($Local 0)) (=> (and (= |inline$$WritebackToValue$0$vdst'@1@@0| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|) 0 inline$$TestGlobalVars_T_pack$0$$struct@1@@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|))) (= (ControlFlow 0 16505) 16720)) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon4$3_correct))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct@@0  (=> (= $TestGlobalVars_sum_of_T@2@@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T@1@@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@0)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 16382) 16505) inline$$WritebackToValue$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 16382) 16479) inline$$WritebackToValue$0$anon3_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct@@0  (=> (and (= inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|)) (= (ControlFlow 0 16364) 16382)) inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct@@0)))
(let ((inline$$WritebackToReference$0$anon3_Else_correct@@0  (=> (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@0|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@0) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@0))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@0 inline$$WritebackToReference$0$srcPath@1@@0))) (=> (and (= |inline$$WritebackToReference$0$dst'@2@@0| inline$$BorrowLoc$0$dst@1@@0) (= (ControlFlow 0 16260) 16364)) inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct@@0))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct@@0  (=> (and (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@0|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@0) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@0))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@0 inline$$WritebackToReference$0$srcPath@1@@0)) (= |inline$$WritebackToReference$0$dst'@1@@0| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) inline$$WritebackToReference$0$dstPath@1@@0 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1@@0 (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@0) (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0) (|v#$Mutation| |inline$$WriteRef$0$to'@1@@0|))))) (and (= |inline$$WritebackToReference$0$dst'@2@@0| |inline$$WritebackToReference$0$dst'@1@@0|) (= (ControlFlow 0 16316) 16364))) inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct@@0)))
(let ((inline$$WritebackToReference$0$anon0_correct@@0  (=> (and (= inline$$WritebackToReference$0$srcPath@1@@0 (|p#$Mutation| |inline$$WriteRef$0$to'@1@@0|)) (= inline$$WritebackToReference$0$dstPath@1@@0 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@0))) (and (=> (= (ControlFlow 0 16224) 16316) inline$$WritebackToReference$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 16224) 16260) inline$$WritebackToReference$0$anon3_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon8_Else_correct  (=> (and (not true) (= (ControlFlow 0 16087) 16224)) inline$$WritebackToReference$0$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon8_Then_correct  (=> (and (= inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$trace_temp@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0)) (= (ControlFlow 0 16849) 16224)) inline$$WritebackToReference$0$anon0_correct@@0)))
(let ((inline$$WriteRef$0$anon0_correct@@0  (=> (= |inline$$WriteRef$0$to'@1@@0| ($Mutation (|l#$Mutation| inline$$BorrowField$0$dst@1@@0) (|p#$Mutation| inline$$BorrowField$0$dst@1@@0) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t4@1)) (and (=> (= (ControlFlow 0 16073) 16849) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 16073) 16087) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$BorrowField$0$anon0_correct@@0  (=> (= inline$$BorrowField$0$p@1@@0 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@0)) (=> (and (and (= inline$$BorrowField$0$size@1@@0 (|size#$Path| inline$$BorrowField$0$p@1@@0)) (= inline$$BorrowField$0$p@2@@0 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1@@0) inline$$BorrowField$0$size@1@@0 $TestGlobalVars_T_i) (+ inline$$BorrowField$0$size@1@@0 1)))) (and (= inline$$BorrowField$0$dst@1@@0 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) inline$$BorrowField$0$p@2@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0))) $TestGlobalVars_T_i))) (= (ControlFlow 0 16014) 16073))) inline$$WriteRef$0$anon0_correct@@0))))
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon2$2_correct  (=> (and (= inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t4@1 ($Integer 4)) (= (ControlFlow 0 16020) 16014)) inline$$BorrowField$0$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct@@0  (=> (and (= $TestGlobalVars_sum_of_T@1@@0 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T@0@@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@0)) $TestGlobalVars_T_i))))) (= (ControlFlow 0 15888) 16020)) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon2$2_correct)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct@@0  (=> (and (= inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0)) (= (ControlFlow 0 15866) 15888)) inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct@@0)))
(let ((inline$$BorrowLoc$0$anon0_correct@@0  (=> (and (= inline$$BorrowLoc$0$dst@1@@0 ($Mutation ($Local 0) $EmptyPath inline$$TestGlobalVars_T_pack$0$$struct@1@@0)) (= (ControlFlow 0 15814) 15866)) inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct@@0)))
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 15764) 15814)) inline$$BorrowLoc$0$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 16857) 15814) inline$$BorrowLoc$0$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_T_pack$0$anon3_correct@@0  (=> (= $TestGlobalVars_sum_of_T@0@@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$0$$struct@1@@0)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 15730) 16857) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 15730) 15764) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon7_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@0  (=> (and (not true) (= (ControlFlow 0 15744) 15730)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@0)))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@0  (=> (= (ControlFlow 0 15750) 15730) inline$$TestGlobalVars_T_pack$0$anon3_correct@@0)))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@0  (=> (> 2445 0) (and (=> (= (ControlFlow 0 15738) 15750) inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@0) (=> (= (ControlFlow 0 15738) 15744) inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@0  (=> (and (>= 0 2445) (= (ControlFlow 0 15712) 15730)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@0)))
366
(let ((inline$$TestGlobalVars_T_pack$0$anon0_correct@@0  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t3@1) (>= (|i#$Integer| inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t3@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t3@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$0$$struct@1@@0 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t3@1) 1)))) (and (=> (= (ControlFlow 0 15704) 15738) inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@0) (=> (= (ControlFlow 0 15704) 15712) inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@0)))))
367
(let ((inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_combi_incorrect_$def_verify$0$$t3@1 ($Integer 3)) (= (ControlFlow 0 15756) 15704)) inline$$TestGlobalVars_T_pack$0$anon0_correct@@0))))
368
(let ((anon0_correct@@0  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 30254) 15756)) inline$$TestGlobalVars_combi_incorrect_$def_verify$0$anon0_correct))))
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
anon0_correct@@0)))))))))))))))))))))))))))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(declare-fun $TestGlobalVars_sum_of_T@0@@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$0$$struct@1@@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_pack_correct_$def_verify$0$$t0@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 31145) (let ((anon0$2_correct@@1  (=> (= (ControlFlow 0 17448) (- 0 31358)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@0@@1 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| ($Integer 2)))))))))))
(let ((inline$$TestGlobalVars_pack_correct_$def_verify$0$anon3_Else_correct  (=> (and (not true) (= (ControlFlow 0 17430) 17448)) anon0$2_correct@@1)))
(let ((inline$$TestGlobalVars_pack_correct_$def_verify$0$anon3_Then_correct  (=> (= (ControlFlow 0 17440) 17448) anon0$2_correct@@1)))
(let ((inline$$TestGlobalVars_T_pack$0$anon3_correct@@1  (=> (= $TestGlobalVars_sum_of_T@0@@1 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$0$$struct@1@@1)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 17394) 17440) inline$$TestGlobalVars_pack_correct_$def_verify$0$anon3_Then_correct) (=> (= (ControlFlow 0 17394) 17430) inline$$TestGlobalVars_pack_correct_$def_verify$0$anon3_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@1  (=> (and (not true) (= (ControlFlow 0 17408) 17394)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@1)))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@1  (=> (= (ControlFlow 0 17414) 17394) inline$$TestGlobalVars_T_pack$0$anon3_correct@@1)))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@1  (=> (> 0 0) (and (=> (= (ControlFlow 0 17402) 17414) inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@1) (=> (= (ControlFlow 0 17402) 17408) inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@1)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@1  (=> (and (>= 0 0) (= (ControlFlow 0 17376) 17394)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@1)))
387
(let ((inline$$TestGlobalVars_T_pack$0$anon0_correct@@1  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_pack_correct_$def_verify$0$$t0@1) (>= (|i#$Integer| inline$$TestGlobalVars_pack_correct_$def_verify$0$$t0@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_pack_correct_$def_verify$0$$t0@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$0$$struct@1@@1 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_pack_correct_$def_verify$0$$t0@1) 1)))) (and (=> (= (ControlFlow 0 17368) 17402) inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@1) (=> (= (ControlFlow 0 17368) 17376) inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@1)))))
388
(let ((inline$$TestGlobalVars_pack_correct_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_pack_correct_$def_verify$0$$t0@1 ($Integer 2)) (= (ControlFlow 0 17420) 17368)) inline$$TestGlobalVars_T_pack$0$anon0_correct@@1))))
389
(let ((anon0_correct@@1  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 31145) 17420)) inline$$TestGlobalVars_pack_correct_$def_verify$0$anon0_correct))))
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
anon0_correct@@1))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $TestGlobalVars_sum_of_T@0@@2 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$0$$struct@1@@2 () T@$Value)
(declare-fun inline$$TestGlobalVars_pack_incorrect_$def_verify$0$$t0@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 31389) (let ((anon0$2_correct@@2  (and (=> (= (ControlFlow 0 17849) (- 0 31624)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@0@@2 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| ($Integer 1))))))))) (=> (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@0@@2 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| ($Integer 1)))))))) (=> (= (ControlFlow 0 17849) (- 0 31649)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$0$$struct@1@@2)) $TestGlobalVars_T_i) ($Integer 2))))))))))
(let ((inline$$TestGlobalVars_pack_incorrect_$def_verify$0$anon3_Else_correct  (=> (and (not true) (= (ControlFlow 0 17831) 17849)) anon0$2_correct@@2)))
(let ((inline$$TestGlobalVars_pack_incorrect_$def_verify$0$anon3_Then_correct  (=> (= (ControlFlow 0 17841) 17849) anon0$2_correct@@2)))
(let ((inline$$TestGlobalVars_T_pack$0$anon3_correct@@2  (=> (= $TestGlobalVars_sum_of_T@0@@2 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$0$$struct@1@@2)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 17795) 17841) inline$$TestGlobalVars_pack_incorrect_$def_verify$0$anon3_Then_correct) (=> (= (ControlFlow 0 17795) 17831) inline$$TestGlobalVars_pack_incorrect_$def_verify$0$anon3_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@2  (=> (and (not true) (= (ControlFlow 0 17809) 17795)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@2)))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@2  (=> (= (ControlFlow 0 17815) 17795) inline$$TestGlobalVars_T_pack$0$anon3_correct@@2)))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@2  (=> (> 0 0) (and (=> (= (ControlFlow 0 17803) 17815) inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@2) (=> (= (ControlFlow 0 17803) 17809) inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@2)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@2  (=> (and (>= 0 0) (= (ControlFlow 0 17777) 17795)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@2)))
408
(let ((inline$$TestGlobalVars_T_pack$0$anon0_correct@@2  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_pack_incorrect_$def_verify$0$$t0@1) (>= (|i#$Integer| inline$$TestGlobalVars_pack_incorrect_$def_verify$0$$t0@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_pack_incorrect_$def_verify$0$$t0@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$0$$struct@1@@2 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_pack_incorrect_$def_verify$0$$t0@1) 1)))) (and (=> (= (ControlFlow 0 17769) 17803) inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@2) (=> (= (ControlFlow 0 17769) 17777) inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@2)))))
409
(let ((inline$$TestGlobalVars_pack_incorrect_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_pack_incorrect_$def_verify$0$$t0@1 ($Integer 2)) (= (ControlFlow 0 17821) 17769)) inline$$TestGlobalVars_T_pack$0$anon0_correct@@2))))
410
(let ((anon0_correct@@2  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 31389) 17821)) inline$$TestGlobalVars_pack_incorrect_$def_verify$0$anon0_correct))))
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
anon0_correct@@2))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(declare-fun $TestGlobalVars_sum_of_T@0@@3 () T@$Value)
(declare-fun t () T@$Value)
(declare-fun inline$$TestGlobalVars_T_unpack$0$i@1@@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 31676) (let ((anon0$2_correct@@3  (and (=> (= (ControlFlow 0 18259) (- 0 31908)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@0@@3 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i))))))))) (=> (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@0@@3 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i)))))))) (=> (= (ControlFlow 0 18259) (- 0 31935)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestGlobalVars_T_unpack$0$i@1@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i))))))))))
(let ((inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 18225) 18259)) anon0$2_correct@@3)))
(let ((inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 18235) 18259) anon0$2_correct@@3)))
(let ((inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon8_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 18215) 18235) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 18215) 18225) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon8_Then_correct  (and (=> (= (ControlFlow 0 18243) 18235) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 18243) 18225) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon9_Else_correct))))
426
(let ((inline$$TestGlobalVars_T_unpack$0$anon0_correct@@1  (=> (and ((_ is $Vector) t) (= inline$$TestGlobalVars_T_unpack$0$i@1@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i))) (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_T_unpack$0$i@1@@1) (>= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1@@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1@@1) $MAX_U64)) (= $TestGlobalVars_sum_of_T@0@@3 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i)))))) (and (=> (= (ControlFlow 0 18201) 18243) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 18201) 18215) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon8_Else_correct))))))
427
428
429
(let ((inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 18074) 18201)) inline$$TestGlobalVars_T_unpack$0$anon0_correct@@1)))
(let ((inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 18251) 18201) inline$$TestGlobalVars_T_unpack$0$anon0_correct@@1)))
(let ((inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 18068) 18251) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 18068) 18074) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon7_Else_correct)))))
430
(let ((anon0_correct@@3  (=> (and (and (and (and (and ((_ is $Vector) t) (let ((va@@8 (|v#$Vector| t)))
431
432
(let ((l@@8 (|l#$ValueArray| va@@8)))
 (and (and (<= 0 l@@8) (<= l@@8 $MAX_U64)) (forall ((x@@8 Int) ) (!  (=> (or (< x@@8 0) (>= x@@8 l@@8)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@8) x@@8) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@8) x@@8))
433
434
)))))) (= (|l#$ValueArray| (|v#$Vector| t)) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $TestGlobalVars_T_i)) $MAX_U64))) true) (= (ControlFlow 0 17928) 18068)) inline$$TestGlobalVars_unpack_correct_$def_verify$0$anon0_correct)))
(let ((PreconditionGeneratedEntry_correct  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 31676) 17928)) anon0_correct@@3))))
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
PreconditionGeneratedEntry_correct))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $TestGlobalVars_sum_of_T@0@@4 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_unpack$0$i@1@@2 () T@$Value)
(declare-fun t@@0 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 31960) (let ((anon0$2_correct@@4  (and (=> (= (ControlFlow 0 18689) (- 0 32178)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@0@@4 $TestGlobalVars_sum_of_T))))) (=> (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@0@@4 $TestGlobalVars_sum_of_T)))) (=> (= (ControlFlow 0 18689) (- 0 32191)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestGlobalVars_T_unpack$0$i@1@@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $TestGlobalVars_T_i))))))))))
(let ((inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 18655) 18689)) anon0$2_correct@@4)))
(let ((inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 18665) 18689) anon0$2_correct@@4)))
(let ((inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon8_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 18645) 18665) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 18645) 18655) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon8_Then_correct  (and (=> (= (ControlFlow 0 18673) 18665) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 18673) 18655) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon9_Else_correct))))
450
(let ((inline$$TestGlobalVars_T_unpack$0$anon0_correct@@2  (=> (and ((_ is $Vector) t@@0) (= inline$$TestGlobalVars_T_unpack$0$i@1@@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $TestGlobalVars_T_i))) (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_T_unpack$0$i@1@@2) (>= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1@@2) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_T_unpack$0$i@1@@2) $MAX_U64)) (= $TestGlobalVars_sum_of_T@0@@4 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $TestGlobalVars_T_i)))))) (and (=> (= (ControlFlow 0 18631) 18673) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 18631) 18645) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon8_Else_correct))))))
451
452
453
(let ((inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 18504) 18631)) inline$$TestGlobalVars_T_unpack$0$anon0_correct@@2)))
(let ((inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 18681) 18631) inline$$TestGlobalVars_T_unpack$0$anon0_correct@@2)))
(let ((inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 18498) 18681) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 18498) 18504) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon7_Else_correct)))))
454
(let ((anon0_correct@@4  (=> (and (and (and (and (and ((_ is $Vector) t@@0) (let ((va@@9 (|v#$Vector| t@@0)))
455
456
(let ((l@@9 (|l#$ValueArray| va@@9)))
 (and (and (<= 0 l@@9) (<= l@@9 $MAX_U64)) (forall ((x@@9 Int) ) (!  (=> (or (< x@@9 0) (>= x@@9 l@@9)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@9) x@@9) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@9) x@@9))
457
458
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@0)) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $TestGlobalVars_T_i)) $MAX_U64))) true) (= (ControlFlow 0 18358) 18498)) inline$$TestGlobalVars_unpack_incorrect_$def_verify$0$anon0_correct)))
(let ((PreconditionGeneratedEntry_correct@@0  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 31960) 18358)) anon0_correct@@4))))
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
PreconditionGeneratedEntry_correct@@0))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(declare-fun $TestGlobalVars_sum_of_S@2 () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@1| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@1| () T@$Value)
(declare-fun inline$$TestGlobalVars_S_pack$0$$struct@1 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_S@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_S_$pack_ref$0$$after@0 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@1 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1@@1| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@1 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@1 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@1| () T@$Mutation)
(declare-fun inline$$TestGlobalVars_update_S_correct_$def_verify$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1@@1 () T@$Mutation)
(declare-fun inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t3@1 () T@$Value)
(declare-fun inline$$BorrowField$0$p@1@@1 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@1 () Int)
(declare-fun inline$$BorrowField$0$p@2@@1 () T@$Path)
(declare-fun $TestGlobalVars_sum_of_S@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_S_$unpack_ref$0$$before@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t2@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 32215) (let ((anon0$2_correct@@5  (=> (= (ControlFlow 0 19979) (- 0 32901)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_S@2 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_S) (|i#$Integer| ($Integer 2)))))))))))
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 19943) 19979)) anon0$2_correct@@5)))
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 19953) 19979) anon0$2_correct@@5)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@1  (=> (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@1|) ($Local 1))) (and (=> (= (ControlFlow 0 19901) 19953) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 19901) 19943) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@1  (=> (and (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@1|) ($Local 1)) (= |inline$$WritebackToValue$0$vdst'@1@@1| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2@@1|) 0 inline$$TestGlobalVars_S_pack$0$$struct@1 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@1|)))) (and (=> (= (ControlFlow 0 19927) 19953) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 19927) 19943) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$TestGlobalVars_S_$pack_ref$0$anon0_correct  (=> (= $TestGlobalVars_sum_of_S@2 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_S@1) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_S_$pack_ref$0$$after@0)) $TestGlobalVars_S_x))))) (and (=> (= (ControlFlow 0 19804) 19927) inline$$WritebackToValue$0$anon3_Then_correct@@1) (=> (= (ControlFlow 0 19804) 19901) inline$$WritebackToValue$0$anon3_Else_correct@@1)))))
(let ((inline$$TestGlobalVars_S_$pack_ref$0$Entry_correct  (=> (and (= inline$$TestGlobalVars_S_$pack_ref$0$$after@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@1|)) (= (ControlFlow 0 19786) 19804)) inline$$TestGlobalVars_S_$pack_ref$0$anon0_correct)))
(let ((inline$$WritebackToReference$0$anon3_Else_correct@@1  (=> (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@1) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@1 inline$$WritebackToReference$0$srcPath@1@@1))) (=> (and (= |inline$$WritebackToReference$0$dst'@2@@1| inline$$BorrowLoc$0$dst@1@@1) (= (ControlFlow 0 19682) 19786)) inline$$TestGlobalVars_S_$pack_ref$0$Entry_correct))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct@@1  (=> (and (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@1) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@1 inline$$WritebackToReference$0$srcPath@1@@1)) (= |inline$$WritebackToReference$0$dst'@1@@1| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@1) inline$$WritebackToReference$0$dstPath@1@@1 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1@@1 (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@1) (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@1) (|v#$Mutation| |inline$$WriteRef$0$to'@1@@1|))))) (and (= |inline$$WritebackToReference$0$dst'@2@@1| |inline$$WritebackToReference$0$dst'@1@@1|) (= (ControlFlow 0 19738) 19786))) inline$$TestGlobalVars_S_$pack_ref$0$Entry_correct)))
(let ((inline$$WritebackToReference$0$anon0_correct@@1  (=> (and (= inline$$WritebackToReference$0$srcPath@1@@1 (|p#$Mutation| |inline$$WriteRef$0$to'@1@@1|)) (= inline$$WritebackToReference$0$dstPath@1@@1 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@1))) (and (=> (= (ControlFlow 0 19646) 19738) inline$$WritebackToReference$0$anon3_Then_correct@@1) (=> (= (ControlFlow 0 19646) 19682) inline$$WritebackToReference$0$anon3_Else_correct@@1)))))
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon8_Else_correct  (=> (and (not true) (= (ControlFlow 0 19509) 19646)) inline$$WritebackToReference$0$anon0_correct@@1)))
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon8_Then_correct  (=> (and (= inline$$TestGlobalVars_update_S_correct_$def_verify$0$$trace_temp@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@1)) (= (ControlFlow 0 19963) 19646)) inline$$WritebackToReference$0$anon0_correct@@1)))
(let ((inline$$WriteRef$0$anon0_correct@@1  (=> (= |inline$$WriteRef$0$to'@1@@1| ($Mutation (|l#$Mutation| inline$$BorrowField$0$dst@1@@1) (|p#$Mutation| inline$$BorrowField$0$dst@1@@1) inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t3@1)) (and (=> (= (ControlFlow 0 19495) 19963) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 19495) 19509) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$BorrowField$0$anon0_correct@@1  (=> (= inline$$BorrowField$0$p@1@@1 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@1)) (=> (and (and (= inline$$BorrowField$0$size@1@@1 (|size#$Path| inline$$BorrowField$0$p@1@@1)) (= inline$$BorrowField$0$p@2@@1 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1@@1) inline$$BorrowField$0$size@1@@1 $TestGlobalVars_S_x) (+ inline$$BorrowField$0$size@1@@1 1)))) (and (= inline$$BorrowField$0$dst@1@@1 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@1) inline$$BorrowField$0$p@2@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@1))) $TestGlobalVars_S_x))) (= (ControlFlow 0 19436) 19495))) inline$$WriteRef$0$anon0_correct@@1))))
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon2$2_correct  (=> (and (= inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t3@1 ($Integer 2)) (= (ControlFlow 0 19442) 19436)) inline$$BorrowField$0$anon0_correct@@1)))
(let ((inline$$TestGlobalVars_S_$unpack_ref$0$anon0_correct  (=> (and (= $TestGlobalVars_sum_of_S@1 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_S@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_S_$unpack_ref$0$$before@0)) $TestGlobalVars_S_x))))) (= (ControlFlow 0 19310) 19442)) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon2$2_correct)))
(let ((inline$$TestGlobalVars_S_$unpack_ref$0$Entry_correct  (=> (and (= inline$$TestGlobalVars_S_$unpack_ref$0$$before@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@1)) (= (ControlFlow 0 19288) 19310)) inline$$TestGlobalVars_S_$unpack_ref$0$anon0_correct)))
(let ((inline$$BorrowLoc$0$anon0_correct@@1  (=> (and (= inline$$BorrowLoc$0$dst@1@@1 ($Mutation ($Local 1) $EmptyPath inline$$TestGlobalVars_S_pack$0$$struct@1)) (= (ControlFlow 0 19236) 19288)) inline$$TestGlobalVars_S_$unpack_ref$0$Entry_correct)))
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 19186) 19236)) inline$$BorrowLoc$0$anon0_correct@@1)))
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 19971) 19236) inline$$BorrowLoc$0$anon0_correct@@1)))
(let ((inline$$TestGlobalVars_S_pack$0$anon3_correct  (=> (= $TestGlobalVars_sum_of_S@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_S) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_S_pack$0$$struct@1)) $TestGlobalVars_S_x))))) (and (=> (= (ControlFlow 0 19152) 19971) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 19152) 19186) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon7_Else_correct)))))
(let ((inline$$TestGlobalVars_S_pack$0$anon5_Else_correct  (=> (and (not true) (= (ControlFlow 0 19166) 19152)) inline$$TestGlobalVars_S_pack$0$anon3_correct)))
(let ((inline$$TestGlobalVars_S_pack$0$anon5_Then_correct  (=> (= (ControlFlow 0 19172) 19152) inline$$TestGlobalVars_S_pack$0$anon3_correct)))
(let ((inline$$TestGlobalVars_S_pack$0$anon4_Then_correct  (=> (> 3118 0) (and (=> (= (ControlFlow 0 19160) 19172) inline$$TestGlobalVars_S_pack$0$anon5_Then_correct) (=> (= (ControlFlow 0 19160) 19166) inline$$TestGlobalVars_S_pack$0$anon5_Else_correct)))))
(let ((inline$$TestGlobalVars_S_pack$0$anon4_Else_correct  (=> (and (>= 0 3118) (= (ControlFlow 0 19134) 19152)) inline$$TestGlobalVars_S_pack$0$anon3_correct)))
511
(let ((inline$$TestGlobalVars_S_pack$0$anon0_correct  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t2@1) (>= (|i#$Integer| inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t2@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t2@1) $MAX_U64)) (= inline$$TestGlobalVars_S_pack$0$$struct@1 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t2@1) 1)))) (and (=> (= (ControlFlow 0 19126) 19160) inline$$TestGlobalVars_S_pack$0$anon4_Then_correct) (=> (= (ControlFlow 0 19126) 19134) inline$$TestGlobalVars_S_pack$0$anon4_Else_correct)))))
512
(let ((inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_update_S_correct_$def_verify$0$$t2@1 ($Integer 0)) (= (ControlFlow 0 19178) 19126)) inline$$TestGlobalVars_S_pack$0$anon0_correct))))
513
(let ((anon0_correct@@5  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 32215) 19178)) inline$$TestGlobalVars_update_S_correct_$def_verify$0$anon0_correct))))
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
anon0_correct@@5)))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $TestGlobalVars_sum_of_S@2@@0 () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@2| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@2| () T@$Value)
(declare-fun inline$$TestGlobalVars_S_pack$0$$struct@1@@0 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_S@1@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_S_$pack_ref$0$$after@0@@0 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@2 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1@@2| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@2 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@2 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@2| () T@$Mutation)
(declare-fun inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1@@2 () T@$Mutation)
(declare-fun inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t3@1 () T@$Value)
(declare-fun inline$$BorrowField$0$p@1@@2 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@2 () Int)
(declare-fun inline$$BorrowField$0$p@2@@2 () T@$Path)
(declare-fun $TestGlobalVars_sum_of_S@0@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_S_$unpack_ref$0$$before@0@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t2@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 32932) (let ((anon0$2_correct@@6  (=> (= (ControlFlow 0 21387) (- 0 33618)) (=> (not false) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_S@2@@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_S) (|i#$Integer| ($Integer 1)))))))))))
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 21351) 21387)) anon0$2_correct@@6)))
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 21361) 21387) anon0$2_correct@@6)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@2  (=> (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@2|) ($Local 1))) (and (=> (= (ControlFlow 0 21309) 21361) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 21309) 21351) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@2  (=> (and (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@2|) ($Local 1)) (= |inline$$WritebackToValue$0$vdst'@1@@2| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2@@2|) 0 inline$$TestGlobalVars_S_pack$0$$struct@1@@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@2|)))) (and (=> (= (ControlFlow 0 21335) 21361) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 21335) 21351) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$TestGlobalVars_S_$pack_ref$0$anon0_correct@@0  (=> (= $TestGlobalVars_sum_of_S@2@@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_S@1@@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_S_$pack_ref$0$$after@0@@0)) $TestGlobalVars_S_x))))) (and (=> (= (ControlFlow 0 21212) 21335) inline$$WritebackToValue$0$anon3_Then_correct@@2) (=> (= (ControlFlow 0 21212) 21309) inline$$WritebackToValue$0$anon3_Else_correct@@2)))))
(let ((inline$$TestGlobalVars_S_$pack_ref$0$Entry_correct@@0  (=> (and (= inline$$TestGlobalVars_S_$pack_ref$0$$after@0@@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@2|)) (= (ControlFlow 0 21194) 21212)) inline$$TestGlobalVars_S_$pack_ref$0$anon0_correct@@0)))
(let ((inline$$WritebackToReference$0$anon3_Else_correct@@2  (=> (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@2) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@2|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@2) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@2))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@2 inline$$WritebackToReference$0$srcPath@1@@2))) (=> (and (= |inline$$WritebackToReference$0$dst'@2@@2| inline$$BorrowLoc$0$dst@1@@2) (= (ControlFlow 0 21090) 21194)) inline$$TestGlobalVars_S_$pack_ref$0$Entry_correct@@0))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct@@2  (=> (and (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@2) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@2|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@2) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@2))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@2 inline$$WritebackToReference$0$srcPath@1@@2)) (= |inline$$WritebackToReference$0$dst'@1@@2| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@2) inline$$WritebackToReference$0$dstPath@1@@2 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1@@2 (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@2) (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@2) (|v#$Mutation| |inline$$WriteRef$0$to'@1@@2|))))) (and (= |inline$$WritebackToReference$0$dst'@2@@2| |inline$$WritebackToReference$0$dst'@1@@2|) (= (ControlFlow 0 21146) 21194))) inline$$TestGlobalVars_S_$pack_ref$0$Entry_correct@@0)))
(let ((inline$$WritebackToReference$0$anon0_correct@@2  (=> (and (= inline$$WritebackToReference$0$srcPath@1@@2 (|p#$Mutation| |inline$$WriteRef$0$to'@1@@2|)) (= inline$$WritebackToReference$0$dstPath@1@@2 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@2))) (and (=> (= (ControlFlow 0 21054) 21146) inline$$WritebackToReference$0$anon3_Then_correct@@2) (=> (= (ControlFlow 0 21054) 21090) inline$$WritebackToReference$0$anon3_Else_correct@@2)))))
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon8_Else_correct  (=> (and (not true) (= (ControlFlow 0 20917) 21054)) inline$$WritebackToReference$0$anon0_correct@@2)))
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon8_Then_correct  (=> (and (= inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$trace_temp@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@2)) (= (ControlFlow 0 21371) 21054)) inline$$WritebackToReference$0$anon0_correct@@2)))
(let ((inline$$WriteRef$0$anon0_correct@@2  (=> (= |inline$$WriteRef$0$to'@1@@2| ($Mutation (|l#$Mutation| inline$$BorrowField$0$dst@1@@2) (|p#$Mutation| inline$$BorrowField$0$dst@1@@2) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t3@1)) (and (=> (= (ControlFlow 0 20903) 21371) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 20903) 20917) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$BorrowField$0$anon0_correct@@2  (=> (= inline$$BorrowField$0$p@1@@2 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@2)) (=> (and (and (= inline$$BorrowField$0$size@1@@2 (|size#$Path| inline$$BorrowField$0$p@1@@2)) (= inline$$BorrowField$0$p@2@@2 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1@@2) inline$$BorrowField$0$size@1@@2 $TestGlobalVars_S_x) (+ inline$$BorrowField$0$size@1@@2 1)))) (and (= inline$$BorrowField$0$dst@1@@2 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@2) inline$$BorrowField$0$p@2@@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@2))) $TestGlobalVars_S_x))) (= (ControlFlow 0 20844) 20903))) inline$$WriteRef$0$anon0_correct@@2))))
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon2$2_correct  (=> (and (= inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t3@1 ($Integer 2)) (= (ControlFlow 0 20850) 20844)) inline$$BorrowField$0$anon0_correct@@2)))
(let ((inline$$TestGlobalVars_S_$unpack_ref$0$anon0_correct@@0  (=> (and (= $TestGlobalVars_sum_of_S@1@@0 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_S@0@@0) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_S_$unpack_ref$0$$before@0@@0)) $TestGlobalVars_S_x))))) (= (ControlFlow 0 20718) 20850)) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon2$2_correct)))
(let ((inline$$TestGlobalVars_S_$unpack_ref$0$Entry_correct@@0  (=> (and (= inline$$TestGlobalVars_S_$unpack_ref$0$$before@0@@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@2)) (= (ControlFlow 0 20696) 20718)) inline$$TestGlobalVars_S_$unpack_ref$0$anon0_correct@@0)))
(let ((inline$$BorrowLoc$0$anon0_correct@@2  (=> (and (= inline$$BorrowLoc$0$dst@1@@2 ($Mutation ($Local 1) $EmptyPath inline$$TestGlobalVars_S_pack$0$$struct@1@@0)) (= (ControlFlow 0 20644) 20696)) inline$$TestGlobalVars_S_$unpack_ref$0$Entry_correct@@0)))
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 20594) 20644)) inline$$BorrowLoc$0$anon0_correct@@2)))
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 21379) 20644) inline$$BorrowLoc$0$anon0_correct@@2)))
(let ((inline$$TestGlobalVars_S_pack$0$anon3_correct@@0  (=> (= $TestGlobalVars_sum_of_S@0@@0 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_S) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_S_pack$0$$struct@1@@0)) $TestGlobalVars_S_x))))) (and (=> (= (ControlFlow 0 20560) 21379) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 20560) 20594) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon7_Else_correct)))))
(let ((inline$$TestGlobalVars_S_pack$0$anon5_Else_correct@@0  (=> (and (not true) (= (ControlFlow 0 20574) 20560)) inline$$TestGlobalVars_S_pack$0$anon3_correct@@0)))
(let ((inline$$TestGlobalVars_S_pack$0$anon5_Then_correct@@0  (=> (= (ControlFlow 0 20580) 20560) inline$$TestGlobalVars_S_pack$0$anon3_correct@@0)))
(let ((inline$$TestGlobalVars_S_pack$0$anon4_Then_correct@@0  (=> (> 3321 0) (and (=> (= (ControlFlow 0 20568) 20580) inline$$TestGlobalVars_S_pack$0$anon5_Then_correct@@0) (=> (= (ControlFlow 0 20568) 20574) inline$$TestGlobalVars_S_pack$0$anon5_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_S_pack$0$anon4_Else_correct@@0  (=> (and (>= 0 3321) (= (ControlFlow 0 20542) 20560)) inline$$TestGlobalVars_S_pack$0$anon3_correct@@0)))
566
(let ((inline$$TestGlobalVars_S_pack$0$anon0_correct@@0  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t2@1) (>= (|i#$Integer| inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t2@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t2@1) $MAX_U64)) (= inline$$TestGlobalVars_S_pack$0$$struct@1@@0 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t2@1) 1)))) (and (=> (= (ControlFlow 0 20534) 20568) inline$$TestGlobalVars_S_pack$0$anon4_Then_correct@@0) (=> (= (ControlFlow 0 20534) 20542) inline$$TestGlobalVars_S_pack$0$anon4_Else_correct@@0)))))
567
(let ((inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$$t2@1 ($Integer 0)) (= (ControlFlow 0 20586) 20534)) inline$$TestGlobalVars_S_pack$0$anon0_correct@@0))))
568
(let ((anon0_correct@@6  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 32932) 20586)) inline$$TestGlobalVars_update_S_incorrect_$def_verify$0$anon0_correct))))
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
anon0_correct@@6)))))))))))))))))))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(declare-fun $abort_flag@2 () Bool)
(declare-fun $TestGlobalVars_sum_of_T@3@@1 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@2@@1 () T@$Value)
(declare-fun $abort_flag@1 () Bool)
(declare-fun |inline$$WriteRef$1$to'@1| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$1$vdst'@1| () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$0$$struct@1@@3 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@1@@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@1 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@3 () T@$Mutation)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_correct_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@1 () T@$Value)
(declare-fun $abort_flag@0 () Bool)
(declare-fun |inline$$WritebackToValue$0$vdst'@2| () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@3| () T@$Mutation)
(declare-fun inline$$ReadRef$0$v@1 () T@$Value)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@3| () T@$Value)
(declare-fun inline$$BorrowLoc$1$dst@1 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1@@3| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@3 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@3 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@3| () T@$Mutation)
(declare-fun inline$$BorrowField$1$dst@1 () T@$Mutation)
(declare-fun inline$$AddU64$0$dst@2 () T@$Value)
(declare-fun inline$$BorrowField$1$p@1 () T@$Path)
(declare-fun inline$$BorrowField$1$size@1 () Int)
(declare-fun inline$$BorrowField$1$p@2 () T@$Path)
(declare-fun inline$$AddU64$0$dst@0 () T@$Value)
(declare-fun inline$$ReadRef$1$v@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1 () T@$Value)
(declare-fun inline$$AddU64$0$dst@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1@@3 () T@$Mutation)
(declare-fun inline$$BorrowField$0$p@1@@3 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@3 () Int)
(declare-fun inline$$BorrowField$0$p@2@@3 () T@$Path)
(declare-fun $TestGlobalVars_sum_of_T@0@@5 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_correct_$def_verify$0$$t1@1 () T@$Value)
(declare-fun |Select_[$TypeValueArray,$int]$Value| (|T@[$TypeValueArray,Int]$Value| T@$TypeValueArray Int) T@$Value)
(declare-fun $TestGlobalVars_T_$memory () T@$Memory)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 33649) (let ((anon0$2_correct@@7  (=> (= (ControlFlow 0 23856) (- 0 34930)) (=> (not $abort_flag@2) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@3@@1 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| ($Integer 3)))))))))))
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon6_correct  (=> (= $TestGlobalVars_sum_of_T@3@@1 $TestGlobalVars_sum_of_T@2@@1) (=> (and (= $abort_flag@2 $abort_flag@1) (= (ControlFlow 0 23824) 23856)) anon0$2_correct@@7))))
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 23822) 23824)) inline$$TestGlobalVars_update_correct_$def_verify$0$anon6_correct)))
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 23832) 23824) inline$$TestGlobalVars_update_correct_$def_verify$0$anon6_correct)))
(let ((inline$$WritebackToValue$1$anon3_Else_correct  (=> (not (= (|l#$Mutation| |inline$$WriteRef$1$to'@1|) ($Local 0))) (and (=> (= (ControlFlow 0 23780) 23832) inline$$TestGlobalVars_update_correct_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 23780) 23822) inline$$TestGlobalVars_update_correct_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$WritebackToValue$1$anon3_Then_correct  (=> (and (= (|l#$Mutation| |inline$$WriteRef$1$to'@1|) ($Local 0)) (= |inline$$WritebackToValue$1$vdst'@1| ($UpdateValue_stratified (|p#$Mutation| |inline$$WriteRef$1$to'@1|) 0 inline$$TestGlobalVars_T_pack$0$$struct@1@@3 (|v#$Mutation| |inline$$WriteRef$1$to'@1|)))) (and (=> (= (ControlFlow 0 23806) 23832) inline$$TestGlobalVars_update_correct_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 23806) 23822) inline$$TestGlobalVars_update_correct_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct@@1  (=> (= $TestGlobalVars_sum_of_T@2@@1 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T@1@@1) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@1)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 23683) 23806) inline$$WritebackToValue$1$anon3_Then_correct) (=> (= (ControlFlow 0 23683) 23780) inline$$WritebackToValue$1$anon3_Else_correct)))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct@@1  (=> (and (= inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@1 (|v#$Mutation| |inline$$WriteRef$1$to'@1|)) (= (ControlFlow 0 23665) 23683)) inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct@@1)))
(let ((inline$$WriteRef$1$anon0_correct  (=> (and (= |inline$$WriteRef$1$to'@1| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@3) (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@3) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2)) (= (ControlFlow 0 23617) 23665)) inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct@@1)))
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon8_Else_correct  (=> (and (not $abort_flag@1) (= (ControlFlow 0 23623) 23617)) inline$$WriteRef$1$anon0_correct)))
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon8_Then_correct  (=> $abort_flag@1 (=> (and (and (= inline$$TestGlobalVars_update_correct_$def_verify$0$$ret0@1 $Error) (= $TestGlobalVars_sum_of_T@3@@1 $TestGlobalVars_sum_of_T@1@@1)) (and (= $abort_flag@2 true) (= (ControlFlow 0 23840) 23856))) anon0$2_correct@@7))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon5_correct  (=> (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@1 $Error) (=> (and (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2 inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@1) (= $abort_flag@1 true)) (and (=> (= (ControlFlow 0 23528) 23840) inline$$TestGlobalVars_update_correct_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 23528) 23623) inline$$TestGlobalVars_update_correct_$def_verify$0$anon8_Else_correct))))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Else_correct  (=> (and (not true) (= (ControlFlow 0 23522) 23528)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon5_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Then_correct  (=> (= (ControlFlow 0 23536) 23528) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon5_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Then_correct  (=> $abort_flag@0 (and (=> (= (ControlFlow 0 23516) 23536) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Then_correct) (=> (= (ControlFlow 0 23516) 23522) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Else_correct)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon8_correct  (=> (and (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2 |inline$$WritebackToValue$0$vdst'@2|) (= $abort_flag@1 $abort_flag@0)) (and (=> (= (ControlFlow 0 23504) 23840) inline$$TestGlobalVars_update_correct_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 23504) 23623) inline$$TestGlobalVars_update_correct_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Else_correct  (=> (and (not true) (= (ControlFlow 0 23502) 23504)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon8_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Then_correct  (=> (= (ControlFlow 0 23512) 23504) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon8_correct)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@3  (=> (and (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@3|) ($Local 1))) (= |inline$$WritebackToValue$0$vdst'@2| inline$$ReadRef$0$v@1)) (and (=> (= (ControlFlow 0 23460) 23512) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Then_correct) (=> (= (ControlFlow 0 23460) 23502) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@3  (=> (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@3|) ($Local 1)) (=> (and (= |inline$$WritebackToValue$0$vdst'@1@@3| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2@@3|) 0 inline$$ReadRef$0$v@1 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@3|))) (= |inline$$WritebackToValue$0$vdst'@2| |inline$$WritebackToValue$0$vdst'@1@@3|)) (and (=> (= (ControlFlow 0 23486) 23512) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Then_correct) (=> (= (ControlFlow 0 23486) 23502) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Else_correct))))))
(let ((inline$$WritebackToReference$0$anon3_Else_correct@@3  (=> (and (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$1$dst@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@3|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@3) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@3))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@3 inline$$WritebackToReference$0$srcPath@1@@3))) (= |inline$$WritebackToReference$0$dst'@2@@3| inline$$BorrowLoc$1$dst@1)) (and (=> (= (ControlFlow 0 23305) 23486) inline$$WritebackToValue$0$anon3_Then_correct@@3) (=> (= (ControlFlow 0 23305) 23460) inline$$WritebackToValue$0$anon3_Else_correct@@3)))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct@@3  (=> (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$1$dst@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@3|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@3) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@3))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@3 inline$$WritebackToReference$0$srcPath@1@@3)) (and (= |inline$$WritebackToReference$0$dst'@1@@3| ($Mutation (|l#$Mutation| inline$$BorrowLoc$1$dst@1) inline$$WritebackToReference$0$dstPath@1@@3 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1@@3 (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@3) (|v#$Mutation| inline$$BorrowLoc$1$dst@1) (|v#$Mutation| |inline$$WriteRef$0$to'@1@@3|)))) (= |inline$$WritebackToReference$0$dst'@2@@3| |inline$$WritebackToReference$0$dst'@1@@3|))) (and (=> (= (ControlFlow 0 23361) 23486) inline$$WritebackToValue$0$anon3_Then_correct@@3) (=> (= (ControlFlow 0 23361) 23460) inline$$WritebackToValue$0$anon3_Else_correct@@3)))))
(let ((inline$$WritebackToReference$0$anon0_correct@@3  (=> (and (= inline$$WritebackToReference$0$srcPath@1@@3 (|p#$Mutation| |inline$$WriteRef$0$to'@1@@3|)) (= inline$$WritebackToReference$0$dstPath@1@@3 (|p#$Mutation| inline$$BorrowLoc$1$dst@1))) (and (=> (= (ControlFlow 0 23269) 23361) inline$$WritebackToReference$0$anon3_Then_correct@@3) (=> (= (ControlFlow 0 23269) 23305) inline$$WritebackToReference$0$anon3_Else_correct@@3)))))
(let ((inline$$WriteRef$0$anon0_correct@@3  (=> (and (= |inline$$WriteRef$0$to'@1@@3| ($Mutation (|l#$Mutation| inline$$BorrowField$1$dst@1) (|p#$Mutation| inline$$BorrowField$1$dst@1) inline$$AddU64$0$dst@2)) (= (ControlFlow 0 23126) 23269)) inline$$WritebackToReference$0$anon0_correct@@3)))
(let ((inline$$BorrowField$1$anon0_correct  (=> (= inline$$BorrowField$1$p@1 (|p#$Mutation| inline$$BorrowLoc$1$dst@1)) (=> (and (and (= inline$$BorrowField$1$size@1 (|size#$Path| inline$$BorrowField$1$p@1)) (= inline$$BorrowField$1$p@2 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$1$p@1) inline$$BorrowField$1$size@1 $TestGlobalVars_T_i) (+ inline$$BorrowField$1$size@1 1)))) (and (= inline$$BorrowField$1$dst@1 ($Mutation (|l#$Mutation| inline$$BorrowLoc$1$dst@1) inline$$BorrowField$1$p@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$1$dst@1))) $TestGlobalVars_T_i))) (= (ControlFlow 0 23067) 23126))) inline$$WriteRef$0$anon0_correct@@3))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Else_correct  (=> (and (not $abort_flag@0) (= (ControlFlow 0 23073) 23067)) inline$$BorrowField$1$anon0_correct)))
(let ((inline$$AddU64$0$anon3_Then$1_correct  (=> (and (= $abort_flag@0 true) (= inline$$AddU64$0$dst@2 inline$$AddU64$0$dst@0)) (and (=> (= (ControlFlow 0 22937) 23516) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Then_correct) (=> (= (ControlFlow 0 22937) 23073) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Else_correct)))))
(let ((inline$$AddU64$0$anon3_Then_correct  (=> (and (> (+ (|i#$Integer| inline$$ReadRef$1$v@1) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1)) $MAX_U64) (= (ControlFlow 0 22935) 22937)) inline$$AddU64$0$anon3_Then$1_correct)))
(let ((inline$$AddU64$0$anon3_Else_correct  (=> (and (and (>= $MAX_U64 (+ (|i#$Integer| inline$$ReadRef$1$v@1) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1))) (= inline$$AddU64$0$dst@1 ($Integer (+ (|i#$Integer| inline$$ReadRef$1$v@1) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1))))) (and (= $abort_flag@0 false) (= inline$$AddU64$0$dst@2 inline$$AddU64$0$dst@1))) (and (=> (= (ControlFlow 0 22879) 23516) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Then_correct) (=> (= (ControlFlow 0 22879) 23073) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Else_correct)))))
(let ((inline$$AddU64$0$Entry_correct  (and (=> (= (ControlFlow 0 22849) (- 0 34367)) true) (and (=> (= (ControlFlow 0 22849) 22935) inline$$AddU64$0$anon3_Then_correct) (=> (= (ControlFlow 0 22849) 22879) inline$$AddU64$0$anon3_Else_correct)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon2$3_correct  (=> (and (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1 ($Integer 3)) (= (ControlFlow 0 22943) 22849)) inline$$AddU64$0$Entry_correct)))
(let ((inline$$ReadRef$1$anon0_correct  (=> (and (= inline$$ReadRef$1$v@1 (|v#$Mutation| inline$$BorrowField$0$dst@1@@3)) (= (ControlFlow 0 22738) 22943)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon2$3_correct)))
(let ((inline$$BorrowField$0$anon0_correct@@3  (=> (= inline$$BorrowField$0$p@1@@3 (|p#$Mutation| inline$$BorrowLoc$1$dst@1)) (=> (and (and (= inline$$BorrowField$0$size@1@@3 (|size#$Path| inline$$BorrowField$0$p@1@@3)) (= inline$$BorrowField$0$p@2@@3 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1@@3) inline$$BorrowField$0$size@1@@3 $TestGlobalVars_T_i) (+ inline$$BorrowField$0$size@1@@3 1)))) (and (= inline$$BorrowField$0$dst@1@@3 ($Mutation (|l#$Mutation| inline$$BorrowLoc$1$dst@1) inline$$BorrowField$0$p@2@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$1$dst@1))) $TestGlobalVars_T_i))) (= (ControlFlow 0 22700) 22738))) inline$$ReadRef$1$anon0_correct))))
(let ((inline$$BorrowLoc$1$anon0_correct  (=> (and (= inline$$BorrowLoc$1$dst@1 ($Mutation ($Local 1) $EmptyPath inline$$ReadRef$0$v@1)) (= (ControlFlow 0 22540) 22700)) inline$$BorrowField$0$anon0_correct@@3)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 22456) 22540)) inline$$BorrowLoc$1$anon0_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Then_correct  (=> (= (ControlFlow 0 23544) 22540) inline$$BorrowLoc$1$anon0_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 22450) 23544) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Then_correct) (=> (= (ControlFlow 0 22450) 22456) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Else_correct)))))
654
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$direct_intra$0$anon0_correct  (=> (and (and (and (and ((_ is $Vector) inline$$ReadRef$0$v@1) (let ((va@@10 (|v#$Vector| inline$$ReadRef$0$v@1)))
655
656
(let ((l@@10 (|l#$ValueArray| va@@10)))
 (and (and (<= 0 l@@10) (<= l@@10 $MAX_U64)) (forall ((x@@10 Int) ) (!  (=> (or (< x@@10 0) (>= x@@10 l@@10)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@10) x@@10) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@10) x@@10))
657
)))))) (= (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1)) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1)) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1)) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1)) $TestGlobalVars_T_i)) $MAX_U64))) (= (ControlFlow 0 23550) 22450)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon0_correct)))
658
659
660
661
662
663
664
665
666
667
668
669
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon2$3_correct  (and (=> (= (ControlFlow 0 23558) (- 0 34158)) true) (=> (= (ControlFlow 0 23558) 23550) inline$$TestGlobalVars_update_valid_still_mutating_$direct_intra$0$anon0_correct))))
(let ((inline$$ReadRef$0$anon0_correct  (=> (and (= inline$$ReadRef$0$v@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@3)) (= (ControlFlow 0 22184) 23558)) inline$$TestGlobalVars_update_correct_$def_verify$0$anon2$3_correct)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct@@1  (=> (and (= $TestGlobalVars_sum_of_T@1@@1 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T@0@@5) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@1)) $TestGlobalVars_T_i))))) (= (ControlFlow 0 22148) 22184)) inline$$ReadRef$0$anon0_correct)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct@@1  (=> (and (= inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@3)) (= (ControlFlow 0 22126) 22148)) inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct@@1)))
(let ((inline$$BorrowLoc$0$anon0_correct@@3  (=> (and (= inline$$BorrowLoc$0$dst@1@@3 ($Mutation ($Local 0) $EmptyPath inline$$TestGlobalVars_T_pack$0$$struct@1@@3)) (= (ControlFlow 0 22074) 22126)) inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct@@1)))
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 22024) 22074)) inline$$BorrowLoc$0$anon0_correct@@3)))
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 23848) 22074) inline$$BorrowLoc$0$anon0_correct@@3)))
(let ((inline$$TestGlobalVars_T_pack$0$anon3_correct@@3  (=> (= $TestGlobalVars_sum_of_T@0@@5 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$0$$struct@1@@3)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 21990) 23848) inline$$TestGlobalVars_update_correct_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 21990) 22024) inline$$TestGlobalVars_update_correct_$def_verify$0$anon7_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@3  (=> (and (not true) (= (ControlFlow 0 22004) 21990)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@3)))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@3  (=> (= (ControlFlow 0 22010) 21990) inline$$TestGlobalVars_T_pack$0$anon3_correct@@3)))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@3  (=> (> 1468 0) (and (=> (= (ControlFlow 0 21998) 22010) inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@3) (=> (= (ControlFlow 0 21998) 22004) inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@3)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@3  (=> (and (>= 0 1468) (= (ControlFlow 0 21972) 21990)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@3)))
670
(let ((inline$$TestGlobalVars_T_pack$0$anon0_correct@@3  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_update_correct_$def_verify$0$$t1@1) (>= (|i#$Integer| inline$$TestGlobalVars_update_correct_$def_verify$0$$t1@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_update_correct_$def_verify$0$$t1@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$0$$struct@1@@3 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_update_correct_$def_verify$0$$t1@1) 1)))) (and (=> (= (ControlFlow 0 21964) 21998) inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@3) (=> (= (ControlFlow 0 21964) 21972) inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@3)))))
671
(let ((inline$$TestGlobalVars_update_correct_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_update_correct_$def_verify$0$$t1@1 ($Integer 0)) (= (ControlFlow 0 22016) 21964)) inline$$TestGlobalVars_T_pack$0$anon0_correct@@3))))
672
(let ((anon0$1_correct  (=> (and (forall (($inv_addr Int) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr)) (let ((va@@11 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr))))
673
674
(let ((l@@11 (|l#$ValueArray| va@@11)))
 (and (and (<= 0 l@@11) (<= l@@11 $MAX_U64)) (forall ((x@@11 Int) ) (!  (=> (or (< x@@11 0) (>= x@@11 l@@11)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@11) x@@11) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@11) x@@11))
675
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr))) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr))) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr))) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr))) $TestGlobalVars_T_i)) $MAX_U64))) true) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr))
676
)) (= (ControlFlow 0 23854) 22016)) inline$$TestGlobalVars_update_correct_$def_verify$0$anon0_correct)))
677
(let ((anon0_correct@@7  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 33649) 23854)) anon0$1_correct))))
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
anon0_correct@@7)))))))))))))))))))))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $abort_flag@2@@0 () Bool)
(declare-fun $TestGlobalVars_sum_of_T@3@@2 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@2@@2 () T@$Value)
(declare-fun $abort_flag@1@@0 () Bool)
(declare-fun |inline$$WriteRef$1$to'@1@@0| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$1$vdst'@1@@0| () T@$Value)
(declare-fun inline$$TestGlobalVars_T_pack$0$$struct@1@@4 () T@$Value)
(declare-fun $TestGlobalVars_sum_of_T@1@@2 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@2 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@4 () T@$Mutation)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_incorrect_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@1@@0 () T@$Value)
(declare-fun $abort_flag@0@@0 () Bool)
(declare-fun |inline$$WritebackToValue$0$vdst'@2@@0| () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@4| () T@$Mutation)
(declare-fun inline$$ReadRef$0$v@1@@0 () T@$Value)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@4| () T@$Value)
(declare-fun inline$$BorrowLoc$1$dst@1@@0 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1@@4| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@4 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@4 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@4| () T@$Mutation)
(declare-fun inline$$BorrowField$1$dst@1@@0 () T@$Mutation)
(declare-fun inline$$AddU64$0$dst@2@@0 () T@$Value)
(declare-fun inline$$BorrowField$1$p@1@@0 () T@$Path)
(declare-fun inline$$BorrowField$1$size@1@@0 () Int)
(declare-fun inline$$BorrowField$1$p@2@@0 () T@$Path)
(declare-fun inline$$AddU64$0$dst@0@@0 () T@$Value)
(declare-fun inline$$ReadRef$1$v@1@@0 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1@@0 () T@$Value)
(declare-fun inline$$AddU64$0$dst@1@@0 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1@@4 () T@$Mutation)
(declare-fun inline$$BorrowField$0$p@1@@4 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@4 () Int)
(declare-fun inline$$BorrowField$0$p@2@@4 () T@$Path)
(declare-fun $TestGlobalVars_sum_of_T@0@@6 () T@$Value)
(declare-fun inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@2 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_incorrect_$def_verify$0$$t1@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 34961) (let ((anon0$2_correct@@8  (=> (= (ControlFlow 0 26485) (- 0 36230)) (=> (not $abort_flag@2@@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T@3@@2 $TestGlobalVars_sum_of_T)))))))
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon6_correct  (=> (= $TestGlobalVars_sum_of_T@3@@2 $TestGlobalVars_sum_of_T@2@@2) (=> (and (= $abort_flag@2@@0 $abort_flag@1@@0) (= (ControlFlow 0 26453) 26485)) anon0$2_correct@@8))))
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 26451) 26453)) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon6_correct)))
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 26461) 26453) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon6_correct)))
(let ((inline$$WritebackToValue$1$anon3_Else_correct@@0  (=> (not (= (|l#$Mutation| |inline$$WriteRef$1$to'@1@@0|) ($Local 0))) (and (=> (= (ControlFlow 0 26409) 26461) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 26409) 26451) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$WritebackToValue$1$anon3_Then_correct@@0  (=> (and (= (|l#$Mutation| |inline$$WriteRef$1$to'@1@@0|) ($Local 0)) (= |inline$$WritebackToValue$1$vdst'@1@@0| ($UpdateValue_stratified (|p#$Mutation| |inline$$WriteRef$1$to'@1@@0|) 0 inline$$TestGlobalVars_T_pack$0$$struct@1@@4 (|v#$Mutation| |inline$$WriteRef$1$to'@1@@0|)))) (and (=> (= (ControlFlow 0 26435) 26461) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 26435) 26451) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon9_Else_correct)))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct@@2  (=> (= $TestGlobalVars_sum_of_T@2@@2 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T@1@@2) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@2)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 26312) 26435) inline$$WritebackToValue$1$anon3_Then_correct@@0) (=> (= (ControlFlow 0 26312) 26409) inline$$WritebackToValue$1$anon3_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct@@2  (=> (and (= inline$$TestGlobalVars_T_$pack_ref$0$$after@0@@2 (|v#$Mutation| |inline$$WriteRef$1$to'@1@@0|)) (= (ControlFlow 0 26294) 26312)) inline$$TestGlobalVars_T_$pack_ref$0$anon0_correct@@2)))
(let ((inline$$WriteRef$1$anon0_correct@@0  (=> (and (= |inline$$WriteRef$1$to'@1@@0| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@4) (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@4) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2@@0)) (= (ControlFlow 0 26246) 26294)) inline$$TestGlobalVars_T_$pack_ref$0$Entry_correct@@2)))
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon8_Else_correct  (=> (and (not $abort_flag@1@@0) (= (ControlFlow 0 26252) 26246)) inline$$WriteRef$1$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon8_Then_correct  (=> $abort_flag@1@@0 (=> (and (and (= inline$$TestGlobalVars_update_incorrect_$def_verify$0$$ret0@1 $Error) (= $TestGlobalVars_sum_of_T@3@@2 $TestGlobalVars_sum_of_T@1@@2)) (and (= $abort_flag@2@@0 true) (= (ControlFlow 0 26469) 26485))) anon0$2_correct@@8))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon5_correct@@0  (=> (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@1@@0 $Error) (=> (and (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2@@0 inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@1@@0) (= $abort_flag@1@@0 true)) (and (=> (= (ControlFlow 0 26157) 26469) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 26157) 26252) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon8_Else_correct))))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Else_correct@@0  (=> (and (not true) (= (ControlFlow 0 26151) 26157)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon5_correct@@0)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Then_correct@@0  (=> (= (ControlFlow 0 26165) 26157) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon5_correct@@0)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Then_correct@@0  (=> $abort_flag@0@@0 (and (=> (= (ControlFlow 0 26145) 26165) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Then_correct@@0) (=> (= (ControlFlow 0 26145) 26151) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon11_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon8_correct@@0  (=> (and (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$ret0@2@@0 |inline$$WritebackToValue$0$vdst'@2@@0|) (= $abort_flag@1@@0 $abort_flag@0@@0)) (and (=> (= (ControlFlow 0 26133) 26469) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 26133) 26252) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Else_correct@@0  (=> (and (not true) (= (ControlFlow 0 26131) 26133)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon8_correct@@0)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Then_correct@@0  (=> (= (ControlFlow 0 26141) 26133) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon8_correct@@0)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@4  (=> (and (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@4|) ($Local 1))) (= |inline$$WritebackToValue$0$vdst'@2@@0| inline$$ReadRef$0$v@1@@0)) (and (=> (= (ControlFlow 0 26089) 26141) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Then_correct@@0) (=> (= (ControlFlow 0 26089) 26131) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Else_correct@@0)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@4  (=> (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@4|) ($Local 1)) (=> (and (= |inline$$WritebackToValue$0$vdst'@1@@4| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2@@4|) 0 inline$$ReadRef$0$v@1@@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@4|))) (= |inline$$WritebackToValue$0$vdst'@2@@0| |inline$$WritebackToValue$0$vdst'@1@@4|)) (and (=> (= (ControlFlow 0 26115) 26141) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Then_correct@@0) (=> (= (ControlFlow 0 26115) 26131) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon12_Else_correct@@0))))))
(let ((inline$$WritebackToReference$0$anon3_Else_correct@@4  (=> (and (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$1$dst@1@@0) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@4|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@4) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@4))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@4 inline$$WritebackToReference$0$srcPath@1@@4))) (= |inline$$WritebackToReference$0$dst'@2@@4| inline$$BorrowLoc$1$dst@1@@0)) (and (=> (= (ControlFlow 0 25934) 26115) inline$$WritebackToValue$0$anon3_Then_correct@@4) (=> (= (ControlFlow 0 25934) 26089) inline$$WritebackToValue$0$anon3_Else_correct@@4)))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct@@4  (=> (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$1$dst@1@@0) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@4|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@4) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@4))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@4 inline$$WritebackToReference$0$srcPath@1@@4)) (and (= |inline$$WritebackToReference$0$dst'@1@@4| ($Mutation (|l#$Mutation| inline$$BorrowLoc$1$dst@1@@0) inline$$WritebackToReference$0$dstPath@1@@4 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1@@4 (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@4) (|v#$Mutation| inline$$BorrowLoc$1$dst@1@@0) (|v#$Mutation| |inline$$WriteRef$0$to'@1@@4|)))) (= |inline$$WritebackToReference$0$dst'@2@@4| |inline$$WritebackToReference$0$dst'@1@@4|))) (and (=> (= (ControlFlow 0 25990) 26115) inline$$WritebackToValue$0$anon3_Then_correct@@4) (=> (= (ControlFlow 0 25990) 26089) inline$$WritebackToValue$0$anon3_Else_correct@@4)))))
(let ((inline$$WritebackToReference$0$anon0_correct@@4  (=> (and (= inline$$WritebackToReference$0$srcPath@1@@4 (|p#$Mutation| |inline$$WriteRef$0$to'@1@@4|)) (= inline$$WritebackToReference$0$dstPath@1@@4 (|p#$Mutation| inline$$BorrowLoc$1$dst@1@@0))) (and (=> (= (ControlFlow 0 25898) 25990) inline$$WritebackToReference$0$anon3_Then_correct@@4) (=> (= (ControlFlow 0 25898) 25934) inline$$WritebackToReference$0$anon3_Else_correct@@4)))))
(let ((inline$$WriteRef$0$anon0_correct@@4  (=> (and (= |inline$$WriteRef$0$to'@1@@4| ($Mutation (|l#$Mutation| inline$$BorrowField$1$dst@1@@0) (|p#$Mutation| inline$$BorrowField$1$dst@1@@0) inline$$AddU64$0$dst@2@@0)) (= (ControlFlow 0 25755) 25898)) inline$$WritebackToReference$0$anon0_correct@@4)))
(let ((inline$$BorrowField$1$anon0_correct@@0  (=> (= inline$$BorrowField$1$p@1@@0 (|p#$Mutation| inline$$BorrowLoc$1$dst@1@@0)) (=> (and (and (= inline$$BorrowField$1$size@1@@0 (|size#$Path| inline$$BorrowField$1$p@1@@0)) (= inline$$BorrowField$1$p@2@@0 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$1$p@1@@0) inline$$BorrowField$1$size@1@@0 $TestGlobalVars_T_i) (+ inline$$BorrowField$1$size@1@@0 1)))) (and (= inline$$BorrowField$1$dst@1@@0 ($Mutation (|l#$Mutation| inline$$BorrowLoc$1$dst@1@@0) inline$$BorrowField$1$p@2@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$1$dst@1@@0))) $TestGlobalVars_T_i))) (= (ControlFlow 0 25696) 25755))) inline$$WriteRef$0$anon0_correct@@4))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Else_correct@@0  (=> (and (not $abort_flag@0@@0) (= (ControlFlow 0 25702) 25696)) inline$$BorrowField$1$anon0_correct@@0)))
(let ((inline$$AddU64$0$anon3_Then$1_correct@@0  (=> (and (= $abort_flag@0@@0 true) (= inline$$AddU64$0$dst@2@@0 inline$$AddU64$0$dst@0@@0)) (and (=> (= (ControlFlow 0 25566) 26145) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Then_correct@@0) (=> (= (ControlFlow 0 25566) 25702) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Else_correct@@0)))))
(let ((inline$$AddU64$0$anon3_Then_correct@@0  (=> (and (> (+ (|i#$Integer| inline$$ReadRef$1$v@1@@0) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1@@0)) $MAX_U64) (= (ControlFlow 0 25564) 25566)) inline$$AddU64$0$anon3_Then$1_correct@@0)))
(let ((inline$$AddU64$0$anon3_Else_correct@@0  (=> (and (and (>= $MAX_U64 (+ (|i#$Integer| inline$$ReadRef$1$v@1@@0) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1@@0))) (= inline$$AddU64$0$dst@1@@0 ($Integer (+ (|i#$Integer| inline$$ReadRef$1$v@1@@0) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1@@0))))) (and (= $abort_flag@0@@0 false) (= inline$$AddU64$0$dst@2@@0 inline$$AddU64$0$dst@1@@0))) (and (=> (= (ControlFlow 0 25508) 26145) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Then_correct@@0) (=> (= (ControlFlow 0 25508) 25702) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon10_Else_correct@@0)))))
(let ((inline$$AddU64$0$Entry_correct@@0  (and (=> (= (ControlFlow 0 25478) (- 0 35667)) true) (and (=> (= (ControlFlow 0 25478) 25564) inline$$AddU64$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 25478) 25508) inline$$AddU64$0$anon3_Else_correct@@0)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon2$3_correct@@0  (=> (and (= inline$$TestGlobalVars_update_valid_still_mutating_$def$0$$t4@1@@0 ($Integer 3)) (= (ControlFlow 0 25572) 25478)) inline$$AddU64$0$Entry_correct@@0)))
(let ((inline$$ReadRef$1$anon0_correct@@0  (=> (and (= inline$$ReadRef$1$v@1@@0 (|v#$Mutation| inline$$BorrowField$0$dst@1@@4)) (= (ControlFlow 0 25367) 25572)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon2$3_correct@@0)))
(let ((inline$$BorrowField$0$anon0_correct@@4  (=> (= inline$$BorrowField$0$p@1@@4 (|p#$Mutation| inline$$BorrowLoc$1$dst@1@@0)) (=> (and (and (= inline$$BorrowField$0$size@1@@4 (|size#$Path| inline$$BorrowField$0$p@1@@4)) (= inline$$BorrowField$0$p@2@@4 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1@@4) inline$$BorrowField$0$size@1@@4 $TestGlobalVars_T_i) (+ inline$$BorrowField$0$size@1@@4 1)))) (and (= inline$$BorrowField$0$dst@1@@4 ($Mutation (|l#$Mutation| inline$$BorrowLoc$1$dst@1@@0) inline$$BorrowField$0$p@2@@4 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$1$dst@1@@0))) $TestGlobalVars_T_i))) (= (ControlFlow 0 25329) 25367))) inline$$ReadRef$1$anon0_correct@@0))))
(let ((inline$$BorrowLoc$1$anon0_correct@@0  (=> (and (= inline$$BorrowLoc$1$dst@1@@0 ($Mutation ($Local 1) $EmptyPath inline$$ReadRef$0$v@1@@0)) (= (ControlFlow 0 25169) 25329)) inline$$BorrowField$0$anon0_correct@@4)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Else_correct@@0  (=> (and (not true) (= (ControlFlow 0 25085) 25169)) inline$$BorrowLoc$1$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Then_correct@@0  (=> (= (ControlFlow 0 26173) 25169) inline$$BorrowLoc$1$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon0_correct@@0  (=> (not false) (and (=> (= (ControlFlow 0 25079) 26173) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Then_correct@@0) (=> (= (ControlFlow 0 25079) 25085) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon9_Else_correct@@0)))))
761
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$direct_intra$0$anon0_correct@@0  (=> (and (and (and (and ((_ is $Vector) inline$$ReadRef$0$v@1@@0) (let ((va@@12 (|v#$Vector| inline$$ReadRef$0$v@1@@0)))
762
763
(let ((l@@12 (|l#$ValueArray| va@@12)))
 (and (and (<= 0 l@@12) (<= l@@12 $MAX_U64)) (forall ((x@@12 Int) ) (!  (=> (or (< x@@12 0) (>= x@@12 l@@12)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@12) x@@12) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@12) x@@12))
764
)))))) (= (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@0)) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@0)) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@0)) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@0)) $TestGlobalVars_T_i)) $MAX_U64))) (= (ControlFlow 0 26179) 25079)) inline$$TestGlobalVars_update_valid_still_mutating_$def$0$anon0_correct@@0)))
765
766
767
768
769
770
771
772
773
774
775
776
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon2$3_correct  (and (=> (= (ControlFlow 0 26187) (- 0 35458)) true) (=> (= (ControlFlow 0 26187) 26179) inline$$TestGlobalVars_update_valid_still_mutating_$direct_intra$0$anon0_correct@@0))))
(let ((inline$$ReadRef$0$anon0_correct@@0  (=> (and (= inline$$ReadRef$0$v@1@@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@4)) (= (ControlFlow 0 24813) 26187)) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon2$3_correct)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct@@2  (=> (and (= $TestGlobalVars_sum_of_T@1@@2 ($Integer (- (|i#$Integer| $TestGlobalVars_sum_of_T@0@@6) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@2)) $TestGlobalVars_T_i))))) (= (ControlFlow 0 24777) 24813)) inline$$ReadRef$0$anon0_correct@@0)))
(let ((inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct@@2  (=> (and (= inline$$TestGlobalVars_T_$unpack_ref$0$$before@0@@2 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@4)) (= (ControlFlow 0 24755) 24777)) inline$$TestGlobalVars_T_$unpack_ref$0$anon0_correct@@2)))
(let ((inline$$BorrowLoc$0$anon0_correct@@4  (=> (and (= inline$$BorrowLoc$0$dst@1@@4 ($Mutation ($Local 0) $EmptyPath inline$$TestGlobalVars_T_pack$0$$struct@1@@4)) (= (ControlFlow 0 24703) 24755)) inline$$TestGlobalVars_T_$unpack_ref$0$Entry_correct@@2)))
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 24653) 24703)) inline$$BorrowLoc$0$anon0_correct@@4)))
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 26477) 24703) inline$$BorrowLoc$0$anon0_correct@@4)))
(let ((inline$$TestGlobalVars_T_pack$0$anon3_correct@@4  (=> (= $TestGlobalVars_sum_of_T@0@@6 ($Integer (+ (|i#$Integer| $TestGlobalVars_sum_of_T) (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestGlobalVars_T_pack$0$$struct@1@@4)) $TestGlobalVars_T_i))))) (and (=> (= (ControlFlow 0 24619) 26477) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 24619) 24653) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon7_Else_correct)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@4  (=> (and (not true) (= (ControlFlow 0 24633) 24619)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@4)))
(let ((inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@4  (=> (= (ControlFlow 0 24639) 24619) inline$$TestGlobalVars_T_pack$0$anon3_correct@@4)))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@4  (=> (> 1733 0) (and (=> (= (ControlFlow 0 24627) 24639) inline$$TestGlobalVars_T_pack$0$anon5_Then_correct@@4) (=> (= (ControlFlow 0 24627) 24633) inline$$TestGlobalVars_T_pack$0$anon5_Else_correct@@4)))))
(let ((inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@4  (=> (and (>= 0 1733) (= (ControlFlow 0 24601) 24619)) inline$$TestGlobalVars_T_pack$0$anon3_correct@@4)))
777
(let ((inline$$TestGlobalVars_T_pack$0$anon0_correct@@4  (=> (and (and (and ((_ is $Integer) inline$$TestGlobalVars_update_incorrect_$def_verify$0$$t1@1) (>= (|i#$Integer| inline$$TestGlobalVars_update_incorrect_$def_verify$0$$t1@1) 0)) (<= (|i#$Integer| inline$$TestGlobalVars_update_incorrect_$def_verify$0$$t1@1) $MAX_U64)) (= inline$$TestGlobalVars_T_pack$0$$struct@1@@4 ($Vector ($ValueArray (|Store_[$int]$Value| ($MapConstValue $Error) 0 inline$$TestGlobalVars_update_incorrect_$def_verify$0$$t1@1) 1)))) (and (=> (= (ControlFlow 0 24593) 24627) inline$$TestGlobalVars_T_pack$0$anon4_Then_correct@@4) (=> (= (ControlFlow 0 24593) 24601) inline$$TestGlobalVars_T_pack$0$anon4_Else_correct@@4)))))
778
(let ((inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon0_correct  (=> (not false) (=> (and (= inline$$TestGlobalVars_update_incorrect_$def_verify$0$$t1@1 ($Integer 0)) (= (ControlFlow 0 24645) 24593)) inline$$TestGlobalVars_T_pack$0$anon0_correct@@4))))
779
(let ((anon0$1_correct@@0  (=> (and (forall (($inv_addr@@0 Int) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@0)) (let ((va@@13 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@0))))
780
781
(let ((l@@13 (|l#$ValueArray| va@@13)))
 (and (and (<= 0 l@@13) (<= l@@13 $MAX_U64)) (forall ((x@@13 Int) ) (!  (=> (or (< x@@13 0) (>= x@@13 l@@13)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@13) x@@13) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@13) x@@13))
782
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@0))) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@0))) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@0))) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@0))) $TestGlobalVars_T_i)) $MAX_U64))) true) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@0))
783
)) (= (ControlFlow 0 26483) 24645)) inline$$TestGlobalVars_update_incorrect_$def_verify$0$anon0_correct)))
784
(let ((anon0_correct@@8  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 34961) 26483)) anon0$1_correct@@0))))
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
anon0_correct@@8)))))))))))))))))))))))))))))))))))))))))))))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(declare-fun $abort_flag@1@@1 () Bool)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun $abort_flag@0@@1 () Bool)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@5| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@5| () T@$Value)
(declare-fun t@@1 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@5 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1@@5| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@5 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@5 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@5| () T@$Mutation)
(declare-fun inline$$BorrowField$1$dst@1@@1 () T@$Mutation)
(declare-fun inline$$AddU64$0$dst@2@@1 () T@$Value)
(declare-fun inline$$BorrowField$1$p@1@@1 () T@$Path)
(declare-fun inline$$BorrowField$1$size@1@@1 () Int)
(declare-fun inline$$BorrowField$1$p@2@@1 () T@$Path)
(declare-fun inline$$AddU64$0$dst@0@@1 () T@$Value)
(declare-fun inline$$ReadRef$0$v@1@@1 () T@$Value)
(declare-fun inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$$t4@1 () T@$Value)
(declare-fun inline$$AddU64$0$dst@1@@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1@@5 () T@$Mutation)
(declare-fun inline$$BorrowField$0$p@1@@5 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@5 () Int)
(declare-fun inline$$BorrowField$0$p@2@@5 () T@$Path)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 36250) (let ((anon0$2_correct@@9  (=> (= (ControlFlow 0 28201) (- 0 37043)) (=> (not $abort_flag@1@@1) (|b#$Boolean| ($Boolean ($IsEqual_stratified $TestGlobalVars_sum_of_T $TestGlobalVars_sum_of_T)))))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon5_correct  (=> (= inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$$ret0@1 $Error) (=> (and (= $abort_flag@1@@1 true) (= (ControlFlow 0 28177) 28201)) anon0$2_correct@@9))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon11_Else_correct  (=> (and (not true) (= (ControlFlow 0 28171) 28177)) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon5_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon11_Then_correct  (=> (= (ControlFlow 0 28185) 28177) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon5_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon10_Then_correct  (=> $abort_flag@0@@1 (and (=> (= (ControlFlow 0 28165) 28185) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon11_Then_correct) (=> (= (ControlFlow 0 28165) 28171) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon11_Else_correct)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon8_correct  (=> (and (= $abort_flag@1@@1 $abort_flag@0@@1) (= (ControlFlow 0 28153) 28201)) anon0$2_correct@@9)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon12_Else_correct  (=> (and (not true) (= (ControlFlow 0 28151) 28153)) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon8_correct)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon12_Then_correct  (=> (= (ControlFlow 0 28161) 28153) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon8_correct)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@5  (=> (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@5|) ($Local 1))) (and (=> (= (ControlFlow 0 28109) 28161) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon12_Then_correct) (=> (= (ControlFlow 0 28109) 28151) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon12_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@5  (=> (and (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@5|) ($Local 1)) (= |inline$$WritebackToValue$0$vdst'@1@@5| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2@@5|) 0 t@@1 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@5|)))) (and (=> (= (ControlFlow 0 28135) 28161) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon12_Then_correct) (=> (= (ControlFlow 0 28135) 28151) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon12_Else_correct)))))
(let ((inline$$WritebackToReference$0$anon3_Else_correct@@5  (=> (and (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@5) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@5|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@5) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@5))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@5 inline$$WritebackToReference$0$srcPath@1@@5))) (= |inline$$WritebackToReference$0$dst'@2@@5| inline$$BorrowLoc$0$dst@1@@5)) (and (=> (= (ControlFlow 0 27954) 28135) inline$$WritebackToValue$0$anon3_Then_correct@@5) (=> (= (ControlFlow 0 27954) 28109) inline$$WritebackToValue$0$anon3_Else_correct@@5)))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct@@5  (=> (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@5) (|l#$Mutation| |inline$$WriteRef$0$to'@1@@5|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@5) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@5))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@5 inline$$WritebackToReference$0$srcPath@1@@5)) (and (= |inline$$WritebackToReference$0$dst'@1@@5| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@5) inline$$WritebackToReference$0$dstPath@1@@5 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1@@5 (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@5) (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@5) (|v#$Mutation| |inline$$WriteRef$0$to'@1@@5|)))) (= |inline$$WritebackToReference$0$dst'@2@@5| |inline$$WritebackToReference$0$dst'@1@@5|))) (and (=> (= (ControlFlow 0 28010) 28135) inline$$WritebackToValue$0$anon3_Then_correct@@5) (=> (= (ControlFlow 0 28010) 28109) inline$$WritebackToValue$0$anon3_Else_correct@@5)))))
(let ((inline$$WritebackToReference$0$anon0_correct@@5  (=> (and (= inline$$WritebackToReference$0$srcPath@1@@5 (|p#$Mutation| |inline$$WriteRef$0$to'@1@@5|)) (= inline$$WritebackToReference$0$dstPath@1@@5 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@5))) (and (=> (= (ControlFlow 0 27918) 28010) inline$$WritebackToReference$0$anon3_Then_correct@@5) (=> (= (ControlFlow 0 27918) 27954) inline$$WritebackToReference$0$anon3_Else_correct@@5)))))
(let ((inline$$WriteRef$0$anon0_correct@@5  (=> (and (= |inline$$WriteRef$0$to'@1@@5| ($Mutation (|l#$Mutation| inline$$BorrowField$1$dst@1@@1) (|p#$Mutation| inline$$BorrowField$1$dst@1@@1) inline$$AddU64$0$dst@2@@1)) (= (ControlFlow 0 27775) 27918)) inline$$WritebackToReference$0$anon0_correct@@5)))
(let ((inline$$BorrowField$1$anon0_correct@@1  (=> (= inline$$BorrowField$1$p@1@@1 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@5)) (=> (and (and (= inline$$BorrowField$1$size@1@@1 (|size#$Path| inline$$BorrowField$1$p@1@@1)) (= inline$$BorrowField$1$p@2@@1 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$1$p@1@@1) inline$$BorrowField$1$size@1@@1 $TestGlobalVars_T_i) (+ inline$$BorrowField$1$size@1@@1 1)))) (and (= inline$$BorrowField$1$dst@1@@1 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@5) inline$$BorrowField$1$p@2@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@5))) $TestGlobalVars_T_i))) (= (ControlFlow 0 27716) 27775))) inline$$WriteRef$0$anon0_correct@@5))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon10_Else_correct  (=> (and (not $abort_flag@0@@1) (= (ControlFlow 0 27722) 27716)) inline$$BorrowField$1$anon0_correct@@1)))
(let ((inline$$AddU64$0$anon3_Then$1_correct@@1  (=> (and (= $abort_flag@0@@1 true) (= inline$$AddU64$0$dst@2@@1 inline$$AddU64$0$dst@0@@1)) (and (=> (= (ControlFlow 0 27586) 28165) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon10_Then_correct) (=> (= (ControlFlow 0 27586) 27722) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon10_Else_correct)))))
(let ((inline$$AddU64$0$anon3_Then_correct@@1  (=> (and (> (+ (|i#$Integer| inline$$ReadRef$0$v@1@@1) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$$t4@1)) $MAX_U64) (= (ControlFlow 0 27584) 27586)) inline$$AddU64$0$anon3_Then$1_correct@@1)))
(let ((inline$$AddU64$0$anon3_Else_correct@@1  (=> (and (and (>= $MAX_U64 (+ (|i#$Integer| inline$$ReadRef$0$v@1@@1) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$$t4@1))) (= inline$$AddU64$0$dst@1@@1 ($Integer (+ (|i#$Integer| inline$$ReadRef$0$v@1@@1) (|i#$Integer| inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$$t4@1))))) (and (= $abort_flag@0@@1 false) (= inline$$AddU64$0$dst@2@@1 inline$$AddU64$0$dst@1@@1))) (and (=> (= (ControlFlow 0 27528) 28165) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon10_Then_correct) (=> (= (ControlFlow 0 27528) 27722) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon10_Else_correct)))))
(let ((inline$$AddU64$0$Entry_correct@@1  (and (=> (= (ControlFlow 0 27498) (- 0 36650)) true) (and (=> (= (ControlFlow 0 27498) 27584) inline$$AddU64$0$anon3_Then_correct@@1) (=> (= (ControlFlow 0 27498) 27528) inline$$AddU64$0$anon3_Else_correct@@1)))))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon2$3_correct  (=> (and (= inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$$t4@1 ($Integer 3)) (= (ControlFlow 0 27592) 27498)) inline$$AddU64$0$Entry_correct@@1)))
(let ((inline$$ReadRef$0$anon0_correct@@1  (=> (and (= inline$$ReadRef$0$v@1@@1 (|v#$Mutation| inline$$BorrowField$0$dst@1@@5)) (= (ControlFlow 0 27387) 27592)) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon2$3_correct)))
(let ((inline$$BorrowField$0$anon0_correct@@5  (=> (= inline$$BorrowField$0$p@1@@5 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@5)) (=> (and (and (= inline$$BorrowField$0$size@1@@5 (|size#$Path| inline$$BorrowField$0$p@1@@5)) (= inline$$BorrowField$0$p@2@@5 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1@@5) inline$$BorrowField$0$size@1@@5 $TestGlobalVars_T_i) (+ inline$$BorrowField$0$size@1@@5 1)))) (and (= inline$$BorrowField$0$dst@1@@5 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@5) inline$$BorrowField$0$p@2@@5 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@5))) $TestGlobalVars_T_i))) (= (ControlFlow 0 27349) 27387))) inline$$ReadRef$0$anon0_correct@@1))))
(let ((inline$$BorrowLoc$0$anon0_correct@@5  (=> (and (= inline$$BorrowLoc$0$dst@1@@5 ($Mutation ($Local 1) $EmptyPath t@@1)) (= (ControlFlow 0 27189) 27349)) inline$$BorrowField$0$anon0_correct@@5)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 27105) 27189)) inline$$BorrowLoc$0$anon0_correct@@5)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 28193) 27189) inline$$BorrowLoc$0$anon0_correct@@5)))
(let ((inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 27099) 28193) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 27099) 27105) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon9_Else_correct)))))
843
(let ((anon0$1_correct@@1  (=> (and (forall (($inv_addr@@1 Int) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@1)) (let ((va@@14 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@1))))
844
845
(let ((l@@14 (|l#$ValueArray| va@@14)))
 (and (and (<= 0 l@@14) (<= l@@14 $MAX_U64)) (forall ((x@@14 Int) ) (!  (=> (or (< x@@14 0) (>= x@@14 l@@14)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@14) x@@14) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@14) x@@14))
846
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@1))) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@1))) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@1))) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@1))) $TestGlobalVars_T_i)) $MAX_U64))) true) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $TestGlobalVars_T_$memory) $EmptyTypeValueArray $inv_addr@@1))
847
)) (= (ControlFlow 0 28199) 27099)) inline$$TestGlobalVars_update_valid_still_mutating_$def_verify$0$anon0_correct)))
848
(let ((anon0_correct@@9  (=> (and (and (and (and ((_ is $Vector) t@@1) (let ((va@@15 (|v#$Vector| t@@1)))
849
850
(let ((l@@15 (|l#$ValueArray| va@@15)))
 (and (and (<= 0 l@@15) (<= l@@15 $MAX_U64)) (forall ((x@@15 Int) ) (!  (=> (or (< x@@15 0) (>= x@@15 l@@15)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@15) x@@15) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@15) x@@15))
851
852
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@1)) 1)) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $TestGlobalVars_T_i)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $TestGlobalVars_T_i)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $TestGlobalVars_T_i)) $MAX_U64))) (= (ControlFlow 0 26862) 28199)) anon0$1_correct@@1)))
(let ((PreconditionGeneratedEntry_correct@@1  (=> (and (and ((_ is $Integer) $TestGlobalVars_sum_of_T) (>= (|i#$Integer| $TestGlobalVars_sum_of_T) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_T) $MAX_U64)) (=> (and (and (and ((_ is $Integer) $TestGlobalVars_sum_of_S) (>= (|i#$Integer| $TestGlobalVars_sum_of_S) 0)) (<= (|i#$Integer| $TestGlobalVars_sum_of_S) $MAX_U64)) (= (ControlFlow 0 36250) 26862)) anon0_correct@@9))))
853
854
855
856
857
858
PreconditionGeneratedEntry_correct@@1)))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)