rotate_authentication_key.smt2 212 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
117
118
119
120
121
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
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
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
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
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
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
(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 $DiemTimestamp_CurrentTimeMicroseconds () T@$TypeName)
(declare-fun $Roles_RoleId () T@$TypeName)
(declare-fun $Event_EventHandle () T@$TypeName)
(declare-fun $Event_EventHandleGenerator () T@$TypeName)
(declare-fun $AccountFreezing_FreezeAccountEvent () T@$TypeName)
(declare-fun $AccountFreezing_FreezeEventsHolder () T@$TypeName)
(declare-fun $AccountFreezing_FreezingBit () T@$TypeName)
(declare-fun $AccountFreezing_UnfreezeAccountEvent () T@$TypeName)
(declare-fun $AccountLimits_AccountLimitMutationCapability () T@$TypeName)
(declare-fun $AccountLimits_LimitsDefinition () T@$TypeName)
(declare-fun $AccountLimits_Window () T@$TypeName)
(declare-fun $ChainId_ChainId () T@$TypeName)
(declare-fun $FixedPoint32_FixedPoint32 () T@$TypeName)
(declare-fun $DiemConfig_DiemConfig () T@$TypeName)
(declare-fun $DiemConfig_Configuration () T@$TypeName)
(declare-fun $DiemConfig_DisableReconfiguration () T@$TypeName)
(declare-fun $DiemConfig_ModifyConfigCapability () T@$TypeName)
(declare-fun $DiemConfig_NewEpochEvent () T@$TypeName)
(declare-fun $RegisteredCurrencies_RegisteredCurrencies () T@$TypeName)
(declare-fun $Diem_Diem () T@$TypeName)
(declare-fun $Diem_BurnCapability () T@$TypeName)
(declare-fun $Diem_BurnEvent () T@$TypeName)
(declare-fun $Diem_CancelBurnEvent () T@$TypeName)
(declare-fun $Diem_CurrencyInfo () T@$TypeName)
(declare-fun $Diem_MintCapability () T@$TypeName)
(declare-fun $Diem_MintEvent () T@$TypeName)
(declare-fun $Diem_Preburn () T@$TypeName)
(declare-fun $Diem_PreburnEvent () T@$TypeName)
(declare-fun $Diem_ToXDXExchangeRateUpdateEvent () T@$TypeName)
(declare-fun $XUS_XUS () T@$TypeName)
(declare-fun $DesignatedDealer_Dealer () T@$TypeName)
(declare-fun $DesignatedDealer_ReceivedMintEvent () T@$TypeName)
(declare-fun $DesignatedDealer_TierInfo () T@$TypeName)
(declare-fun $XDX_XDX () T@$TypeName)
(declare-fun $XDX_Reserve () T@$TypeName)
(declare-fun $ValidatorOperatorConfig_ValidatorOperatorConfig () T@$TypeName)
(declare-fun $Option_Option () T@$TypeName)
(declare-fun $ValidatorConfig_Config () T@$TypeName)
(declare-fun $ValidatorConfig_ValidatorConfig () T@$TypeName)
(declare-fun $VASP_ChildVASP () T@$TypeName)
(declare-fun $VASP_ParentVASP () T@$TypeName)
(declare-fun $TransactionFee_TransactionFee () T@$TypeName)
(declare-fun $SlidingNonce_SlidingNonce () T@$TypeName)
(declare-fun $DualAttestation_BaseUrlRotationEvent () T@$TypeName)
(declare-fun $DualAttestation_ComplianceKeyRotationEvent () T@$TypeName)
(declare-fun $DualAttestation_Credential () T@$TypeName)
(declare-fun $DualAttestation_Limit () T@$TypeName)
(declare-fun $DiemTransactionPublishingOption_DiemTransactionPublishingOption () T@$TypeName)
(declare-fun $DiemAccount_DiemAccount () T@$TypeName)
(declare-fun $DiemAccount_AccountOperationsCapability () T@$TypeName)
(declare-fun $DiemAccount_AdminTransactionEvent () T@$TypeName)
(declare-fun $DiemAccount_Balance () T@$TypeName)
(declare-fun $DiemAccount_CreateAccountEvent () T@$TypeName)
(declare-fun $DiemAccount_DiemWriteSetManager () T@$TypeName)
(declare-fun $DiemAccount_KeyRotationCapability () T@$TypeName)
(declare-fun $DiemAccount_ReceivedPaymentEvent () T@$TypeName)
(declare-fun $DiemAccount_SentPaymentEvent () T@$TypeName)
(declare-fun $DiemAccount_WithdrawCapability () 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 $DiemTimestamp_CurrentTimeMicroseconds_microseconds () Int)
(declare-fun $DiemTimestamp_CurrentTimeMicroseconds_type_value () T@$TypeValue)
(declare-fun $Roles_RoleId_role_id () Int)
(declare-fun $Roles_RoleId_type_value () T@$TypeValue)
(declare-fun $Event_EventHandle_counter () Int)
(declare-fun $Event_EventHandle_guid () Int)
(declare-fun $Event_EventHandle_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun |Store_[$int]$TypeValue| (|T@[Int]$TypeValue| Int T@$TypeValue) |T@[Int]$TypeValue|)
(declare-fun |Select_[$int]$TypeValue| (|T@[Int]$TypeValue| Int) T@$TypeValue)
(assert (forall ( ( ?x0 |T@[Int]$TypeValue|) ( ?x1 Int) ( ?x2 T@$TypeValue)) (= (|Select_[$int]$TypeValue| (|Store_[$int]$TypeValue| ?x0 ?x1 ?x2) ?x1)  ?x2)))
(assert (forall ( ( ?x0 |T@[Int]$TypeValue|) ( ?x1 Int) ( ?y1 Int) ( ?x2 T@$TypeValue)) (=>  (not (= ?x1 ?y1)) (= (|Select_[$int]$TypeValue| (|Store_[$int]$TypeValue| ?x0 ?x1 ?x2) ?y1) (|Select_[$int]$TypeValue| ?x0 ?y1)))))
(declare-fun $Event_EventHandleGenerator_counter () Int)
(declare-fun $Event_EventHandleGenerator_addr () Int)
(declare-fun $Event_EventHandleGenerator_type_value () T@$TypeValue)
(declare-fun $AccountFreezing_FreezeAccountEvent_initiator_address () Int)
(declare-fun $AccountFreezing_FreezeAccountEvent_frozen_address () Int)
(declare-fun $AccountFreezing_FreezeAccountEvent_type_value () T@$TypeValue)
(declare-fun $AccountFreezing_FreezeEventsHolder_freeze_event_handle () Int)
(declare-fun $AccountFreezing_FreezeEventsHolder_unfreeze_event_handle () Int)
(declare-fun $AccountFreezing_FreezeEventsHolder_type_value () T@$TypeValue)
(declare-fun $AccountFreezing_FreezingBit_is_frozen () Int)
(declare-fun $AccountFreezing_FreezingBit_type_value () T@$TypeValue)
(declare-fun $AccountFreezing_UnfreezeAccountEvent_initiator_address () Int)
(declare-fun $AccountFreezing_UnfreezeAccountEvent_unfrozen_address () Int)
(declare-fun $AccountFreezing_UnfreezeAccountEvent_type_value () T@$TypeValue)
(declare-fun $AccountLimits_AccountLimitMutationCapability_dummy_field () Int)
(declare-fun $AccountLimits_AccountLimitMutationCapability_type_value () T@$TypeValue)
(declare-fun $AccountLimits_LimitsDefinition_max_inflow () Int)
(declare-fun $AccountLimits_LimitsDefinition_max_outflow () Int)
(declare-fun $AccountLimits_LimitsDefinition_time_period () Int)
(declare-fun $AccountLimits_LimitsDefinition_max_holding () Int)
(declare-fun $AccountLimits_LimitsDefinition_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $AccountLimits_Window_window_start () Int)
(declare-fun $AccountLimits_Window_window_inflow () Int)
(declare-fun $AccountLimits_Window_window_outflow () Int)
(declare-fun $AccountLimits_Window_tracked_balance () Int)
(declare-fun $AccountLimits_Window_limit_address () Int)
(declare-fun $AccountLimits_Window_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $ChainId_ChainId_id () Int)
(declare-fun $ChainId_ChainId_type_value () T@$TypeValue)
(declare-fun $FixedPoint32_FixedPoint32_value () Int)
(declare-fun $FixedPoint32_FixedPoint32_type_value () T@$TypeValue)
(declare-fun $DiemConfig_DiemConfig_payload () Int)
(declare-fun $DiemConfig_DiemConfig_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $DiemConfig_Configuration_epoch () Int)
(declare-fun $DiemConfig_Configuration_last_reconfiguration_time () Int)
(declare-fun $DiemConfig_Configuration_events () Int)
(declare-fun $DiemConfig_Configuration_type_value () T@$TypeValue)
(declare-fun $DiemConfig_DisableReconfiguration_dummy_field () Int)
(declare-fun $DiemConfig_DisableReconfiguration_type_value () T@$TypeValue)
(declare-fun $DiemConfig_ModifyConfigCapability_dummy_field () Int)
(declare-fun $DiemConfig_ModifyConfigCapability_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $DiemConfig_NewEpochEvent_epoch () Int)
(declare-fun $DiemConfig_NewEpochEvent_type_value () T@$TypeValue)
(declare-fun $RegisteredCurrencies_RegisteredCurrencies_currency_codes () Int)
(declare-fun $RegisteredCurrencies_RegisteredCurrencies_type_value () T@$TypeValue)
(declare-fun $Diem_Diem_value () Int)
(declare-fun $Diem_Diem_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $Diem_BurnCapability_dummy_field () Int)
(declare-fun $Diem_BurnCapability_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $Diem_BurnEvent_amount () Int)
(declare-fun $Diem_BurnEvent_currency_code () Int)
(declare-fun $Diem_BurnEvent_preburn_address () Int)
(declare-fun $Diem_BurnEvent_type_value () T@$TypeValue)
(declare-fun $Diem_CancelBurnEvent_amount () Int)
(declare-fun $Diem_CancelBurnEvent_currency_code () Int)
(declare-fun $Diem_CancelBurnEvent_preburn_address () Int)
(declare-fun $Diem_CancelBurnEvent_type_value () T@$TypeValue)
(declare-fun $Diem_CurrencyInfo_total_value () Int)
(declare-fun $Diem_CurrencyInfo_preburn_value () Int)
(declare-fun $Diem_CurrencyInfo_to_xdx_exchange_rate () Int)
(declare-fun $Diem_CurrencyInfo_is_synthetic () Int)
(declare-fun $Diem_CurrencyInfo_scaling_factor () Int)
(declare-fun $Diem_CurrencyInfo_fractional_part () Int)
(declare-fun $Diem_CurrencyInfo_currency_code () Int)
(declare-fun $Diem_CurrencyInfo_can_mint () Int)
(declare-fun $Diem_CurrencyInfo_mint_events () Int)
(declare-fun $Diem_CurrencyInfo_burn_events () Int)
(declare-fun $Diem_CurrencyInfo_preburn_events () Int)
(declare-fun $Diem_CurrencyInfo_cancel_burn_events () Int)
(declare-fun $Diem_CurrencyInfo_exchange_rate_update_events () Int)
(declare-fun $Diem_CurrencyInfo_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $Diem_MintCapability_dummy_field () Int)
(declare-fun $Diem_MintCapability_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $Diem_MintEvent_amount () Int)
(declare-fun $Diem_MintEvent_currency_code () Int)
(declare-fun $Diem_MintEvent_type_value () T@$TypeValue)
(declare-fun $Diem_Preburn_to_burn () Int)
(declare-fun $Diem_Preburn_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $Diem_PreburnEvent_amount () Int)
(declare-fun $Diem_PreburnEvent_currency_code () Int)
(declare-fun $Diem_PreburnEvent_preburn_address () Int)
(declare-fun $Diem_PreburnEvent_type_value () T@$TypeValue)
(declare-fun $Diem_ToXDXExchangeRateUpdateEvent_currency_code () Int)
(declare-fun $Diem_ToXDXExchangeRateUpdateEvent_new_to_xdx_exchange_rate () Int)
(declare-fun $Diem_ToXDXExchangeRateUpdateEvent_type_value () T@$TypeValue)
(declare-fun $XUS_XUS_dummy_field () Int)
(declare-fun $XUS_XUS_type_value () T@$TypeValue)
(declare-fun $DesignatedDealer_Dealer_mint_event_handle () Int)
(declare-fun $DesignatedDealer_Dealer_type_value () T@$TypeValue)
(declare-fun $DesignatedDealer_ReceivedMintEvent_currency_code () Int)
(declare-fun $DesignatedDealer_ReceivedMintEvent_destination_address () Int)
(declare-fun $DesignatedDealer_ReceivedMintEvent_amount () Int)
(declare-fun $DesignatedDealer_ReceivedMintEvent_type_value () T@$TypeValue)
(declare-fun $DesignatedDealer_TierInfo_window_start () Int)
(declare-fun $DesignatedDealer_TierInfo_window_inflow () Int)
(declare-fun $DesignatedDealer_TierInfo_tiers () Int)
(declare-fun $DesignatedDealer_TierInfo_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $XDX_XDX_dummy_field () Int)
(declare-fun $XDX_XDX_type_value () T@$TypeValue)
(declare-fun $XDX_Reserve_mint_cap () Int)
(declare-fun $XDX_Reserve_burn_cap () Int)
(declare-fun $XDX_Reserve_preburn_cap () Int)
(declare-fun $XDX_Reserve_type_value () T@$TypeValue)
(declare-fun $ValidatorOperatorConfig_ValidatorOperatorConfig_human_name () Int)
(declare-fun $ValidatorOperatorConfig_ValidatorOperatorConfig_type_value () T@$TypeValue)
(declare-fun $Option_Option_vec () Int)
(declare-fun $Option_Option_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $ValidatorConfig_Config_consensus_pubkey () Int)
(declare-fun $ValidatorConfig_Config_validator_network_addresses () Int)
(declare-fun $ValidatorConfig_Config_fullnode_network_addresses () Int)
(declare-fun $ValidatorConfig_Config_type_value () T@$TypeValue)
(declare-fun $ValidatorConfig_ValidatorConfig_config () Int)
(declare-fun $ValidatorConfig_ValidatorConfig_operator_account () Int)
(declare-fun $ValidatorConfig_ValidatorConfig_human_name () Int)
(declare-fun $ValidatorConfig_ValidatorConfig_type_value () T@$TypeValue)
(declare-fun $VASP_ChildVASP_parent_vasp_addr () Int)
(declare-fun $VASP_ChildVASP_type_value () T@$TypeValue)
(declare-fun $VASP_ParentVASP_num_children () Int)
(declare-fun $VASP_ParentVASP_type_value () T@$TypeValue)
(declare-fun $TransactionFee_TransactionFee_balance () Int)
(declare-fun $TransactionFee_TransactionFee_preburn () Int)
(declare-fun $TransactionFee_TransactionFee_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $SlidingNonce_spec_try_record_nonce (T@$Value T@$Value) T@$Value)
(declare-fun $SlidingNonce_SlidingNonce_min_nonce () Int)
(declare-fun $SlidingNonce_SlidingNonce_nonce_mask () Int)
(declare-fun $SlidingNonce_SlidingNonce_type_value () T@$TypeValue)
(declare-fun $DualAttestation_spec_dual_attestation_message (T@$Value T@$Value T@$Value) T@$Value)
(declare-fun $DualAttestation_BaseUrlRotationEvent_new_base_url () Int)
(declare-fun $DualAttestation_BaseUrlRotationEvent_time_rotated_seconds () Int)
(declare-fun $DualAttestation_BaseUrlRotationEvent_type_value () T@$TypeValue)
(declare-fun $DualAttestation_ComplianceKeyRotationEvent_new_compliance_public_key () Int)
(declare-fun $DualAttestation_ComplianceKeyRotationEvent_time_rotated_seconds () Int)
(declare-fun $DualAttestation_ComplianceKeyRotationEvent_type_value () T@$TypeValue)
(declare-fun $DualAttestation_Credential_human_name () Int)
(declare-fun $DualAttestation_Credential_base_url () Int)
(declare-fun $DualAttestation_Credential_compliance_public_key () Int)
(declare-fun $DualAttestation_Credential_expiration_date () Int)
(declare-fun $DualAttestation_Credential_compliance_key_rotation_events () Int)
(declare-fun $DualAttestation_Credential_base_url_rotation_events () Int)
(declare-fun $DualAttestation_Credential_type_value () T@$TypeValue)
(declare-fun $DualAttestation_Limit_micro_xdx_limit () Int)
(declare-fun $DualAttestation_Limit_type_value () T@$TypeValue)
(declare-fun $DiemTransactionPublishingOption_DiemTransactionPublishingOption_script_allow_list () Int)
(declare-fun $DiemTransactionPublishingOption_DiemTransactionPublishingOption_module_publishing_allowed () Int)
(declare-fun $DiemTransactionPublishingOption_DiemTransactionPublishingOption_type_value () T@$TypeValue)
(declare-fun $DiemAccount_spec_abstract_create_authentication_key (T@$Value) T@$Value)
(declare-fun $DiemAccount_DiemAccount_authentication_key () Int)
(declare-fun $DiemAccount_DiemAccount_withdraw_capability () Int)
(declare-fun $DiemAccount_DiemAccount_key_rotation_capability () Int)
(declare-fun $DiemAccount_DiemAccount_received_events () Int)
(declare-fun $DiemAccount_DiemAccount_sent_events () Int)
(declare-fun $DiemAccount_DiemAccount_sequence_number () Int)
(declare-fun $DiemAccount_DiemAccount_type_value () T@$TypeValue)
(declare-fun $DiemAccount_AccountOperationsCapability_limits_cap () Int)
(declare-fun $DiemAccount_AccountOperationsCapability_creation_events () Int)
(declare-fun $DiemAccount_AccountOperationsCapability_type_value () T@$TypeValue)
(declare-fun $DiemAccount_AdminTransactionEvent_committed_timestamp_secs () Int)
(declare-fun $DiemAccount_AdminTransactionEvent_type_value () T@$TypeValue)
(declare-fun $DiemAccount_Balance_coin () Int)
(declare-fun $DiemAccount_Balance_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $DiemAccount_CreateAccountEvent_created () Int)
(declare-fun $DiemAccount_CreateAccountEvent_role_id () Int)
(declare-fun $DiemAccount_CreateAccountEvent_type_value () T@$TypeValue)
(declare-fun $DiemAccount_DiemWriteSetManager_upgrade_events () Int)
(declare-fun $DiemAccount_DiemWriteSetManager_type_value () T@$TypeValue)
(declare-fun $DiemAccount_KeyRotationCapability_account_address () Int)
(declare-fun $DiemAccount_KeyRotationCapability_type_value () T@$TypeValue)
(declare-fun $DiemAccount_ReceivedPaymentEvent_amount () Int)
(declare-fun $DiemAccount_ReceivedPaymentEvent_currency_code () Int)
(declare-fun $DiemAccount_ReceivedPaymentEvent_payer () Int)
(declare-fun $DiemAccount_ReceivedPaymentEvent_metadata () Int)
(declare-fun $DiemAccount_ReceivedPaymentEvent_type_value () T@$TypeValue)
(declare-fun $DiemAccount_SentPaymentEvent_amount () Int)
(declare-fun $DiemAccount_SentPaymentEvent_currency_code () Int)
(declare-fun $DiemAccount_SentPaymentEvent_payee () Int)
(declare-fun $DiemAccount_SentPaymentEvent_metadata () Int)
(declare-fun $DiemAccount_SentPaymentEvent_type_value () T@$TypeValue)
(declare-fun $DiemAccount_WithdrawCapability_account_address () Int)
(declare-fun $DiemAccount_WithdrawCapability_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 $DiemTimestamp_CurrentTimeMicroseconds $Roles_RoleId $Event_EventHandle $Event_EventHandleGenerator $AccountFreezing_FreezeAccountEvent $AccountFreezing_FreezeEventsHolder $AccountFreezing_FreezingBit $AccountFreezing_UnfreezeAccountEvent $AccountLimits_AccountLimitMutationCapability $AccountLimits_LimitsDefinition $AccountLimits_Window $ChainId_ChainId $FixedPoint32_FixedPoint32 $DiemConfig_DiemConfig $DiemConfig_Configuration $DiemConfig_DisableReconfiguration $DiemConfig_ModifyConfigCapability $DiemConfig_NewEpochEvent $RegisteredCurrencies_RegisteredCurrencies $Diem_Diem $Diem_BurnCapability $Diem_BurnEvent $Diem_CancelBurnEvent $Diem_CurrencyInfo $Diem_MintCapability $Diem_MintEvent $Diem_Preburn $Diem_PreburnEvent $Diem_ToXDXExchangeRateUpdateEvent $XUS_XUS $DesignatedDealer_Dealer $DesignatedDealer_ReceivedMintEvent $DesignatedDealer_TierInfo $XDX_XDX $XDX_Reserve $ValidatorOperatorConfig_ValidatorOperatorConfig $Option_Option $ValidatorConfig_Config $ValidatorConfig_ValidatorConfig $VASP_ChildVASP $VASP_ParentVASP $TransactionFee_TransactionFee $SlidingNonce_SlidingNonce $DualAttestation_BaseUrlRotationEvent $DualAttestation_ComplianceKeyRotationEvent $DualAttestation_Credential $DualAttestation_Limit $DiemTransactionPublishingOption_DiemTransactionPublishingOption $DiemAccount_DiemAccount $DiemAccount_AccountOperationsCapability $DiemAccount_AdminTransactionEvent $DiemAccount_Balance $DiemAccount_CreateAccountEvent $DiemAccount_DiemWriteSetManager $DiemAccount_KeyRotationCapability $DiemAccount_ReceivedPaymentEvent $DiemAccount_SentPaymentEvent $DiemAccount_WithdrawCapability)
)
(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))
359
(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))
360
)))
361
(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))
362
)))
363
(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))
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
)))
(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))
)))
421
(assert (forall ((v1@@2 T@$Value) (v2@@2 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@2) (let ((va (|v#$Vector| v1@@2)))
422
423
(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))
424
)))))) (and ((_ is $Vector) v2@@2) (let ((va@@0 (|v#$Vector| v2@@2)))
425
426
427
(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)))))
428
(assert (forall ((v1@@3 T@$Value) (v2@@3 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@3) (let ((va@@1 (|v#$Vector| v1@@3)))
429
430
(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))
431
)))))) (and ((_ is $Vector) v2@@3) (let ((va@@2 (|v#$Vector| v2@@3)))
432
433
434
(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))))
435
(assert (forall ((v1@@4 T@$Value) (v2@@4 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@4) (let ((va@@3 (|v#$Vector| v1@@4)))
436
437
(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))
438
)))))) (and ((_ is $Vector) v2@@4) (let ((va@@4 (|v#$Vector| v2@@4)))
439
440
441
(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)))))
442
(assert (forall ((v1@@5 T@$Value) (v2@@5 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@5) (let ((va@@5 (|v#$Vector| v1@@5)))
443
444
(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))
445
)))))) (and ((_ is $Vector) v2@@5) (let ((va@@6 (|v#$Vector| v2@@5)))
446
447
448
(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))))
449
450
(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))))
451
452
453
(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)))
454
 (and (and (and ((_ is $Vector) r) (let ((va@@7 (|v#$Vector| r)))
455
456
(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))
457
)))))) (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))
458
459
))) (> (|l#$ValueArray| (|v#$Vector| r)) 0)))))
(assert (forall ((v@@13 T@$Value) ) (let ((r@@0 ($BCS_serialize_core v@@13)))
460
 (=> ((_ is $Address) v@@13) (= (|l#$ValueArray| (|v#$Vector| r@@0)) $serialized_address_len)))))
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
511
512
513
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
566
567
568
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
(assert (= $DiemTimestamp_CurrentTimeMicroseconds_microseconds 0))
(assert (= $DiemTimestamp_CurrentTimeMicroseconds_type_value ($StructType $DiemTimestamp_CurrentTimeMicroseconds $EmptyTypeValueArray)))
(assert (= $Roles_RoleId_role_id 0))
(assert (= $Roles_RoleId_type_value ($StructType $Roles_RoleId $EmptyTypeValueArray)))
(assert (= $Event_EventHandle_counter 0))
(assert (= $Event_EventHandle_guid 1))
(assert (forall (($tv0 T@$TypeValue) ) (! (= ($Event_EventHandle_type_value $tv0) ($StructType $Event_EventHandle ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0) 1))) :pattern ( ($Event_EventHandle_type_value $tv0))
)))
(assert (= $Event_EventHandleGenerator_counter 0))
(assert (= $Event_EventHandleGenerator_addr 1))
(assert (= $Event_EventHandleGenerator_type_value ($StructType $Event_EventHandleGenerator $EmptyTypeValueArray)))
(assert (= $AccountFreezing_FreezeAccountEvent_initiator_address 0))
(assert (= $AccountFreezing_FreezeAccountEvent_frozen_address 1))
(assert (= $AccountFreezing_FreezeAccountEvent_type_value ($StructType $AccountFreezing_FreezeAccountEvent $EmptyTypeValueArray)))
(assert (= $AccountFreezing_FreezeEventsHolder_freeze_event_handle 0))
(assert (= $AccountFreezing_FreezeEventsHolder_unfreeze_event_handle 1))
(assert (= $AccountFreezing_FreezeEventsHolder_type_value ($StructType $AccountFreezing_FreezeEventsHolder $EmptyTypeValueArray)))
(assert (= $AccountFreezing_FreezingBit_is_frozen 0))
(assert (= $AccountFreezing_FreezingBit_type_value ($StructType $AccountFreezing_FreezingBit $EmptyTypeValueArray)))
(assert (= $AccountFreezing_UnfreezeAccountEvent_initiator_address 0))
(assert (= $AccountFreezing_UnfreezeAccountEvent_unfrozen_address 1))
(assert (= $AccountFreezing_UnfreezeAccountEvent_type_value ($StructType $AccountFreezing_UnfreezeAccountEvent $EmptyTypeValueArray)))
(assert (= $AccountLimits_AccountLimitMutationCapability_dummy_field 0))
(assert (= $AccountLimits_AccountLimitMutationCapability_type_value ($StructType $AccountLimits_AccountLimitMutationCapability $EmptyTypeValueArray)))
(assert (= $AccountLimits_LimitsDefinition_max_inflow 0))
(assert (= $AccountLimits_LimitsDefinition_max_outflow 1))
(assert (= $AccountLimits_LimitsDefinition_time_period 2))
(assert (= $AccountLimits_LimitsDefinition_max_holding 3))
(assert (forall (($tv0@@0 T@$TypeValue) ) (! (= ($AccountLimits_LimitsDefinition_type_value $tv0@@0) ($StructType $AccountLimits_LimitsDefinition ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@0) 1))) :pattern ( ($AccountLimits_LimitsDefinition_type_value $tv0@@0))
)))
(assert (= $AccountLimits_Window_window_start 0))
(assert (= $AccountLimits_Window_window_inflow 1))
(assert (= $AccountLimits_Window_window_outflow 2))
(assert (= $AccountLimits_Window_tracked_balance 3))
(assert (= $AccountLimits_Window_limit_address 4))
(assert (forall (($tv0@@1 T@$TypeValue) ) (! (= ($AccountLimits_Window_type_value $tv0@@1) ($StructType $AccountLimits_Window ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@1) 1))) :pattern ( ($AccountLimits_Window_type_value $tv0@@1))
)))
(assert (= $ChainId_ChainId_id 0))
(assert (= $ChainId_ChainId_type_value ($StructType $ChainId_ChainId $EmptyTypeValueArray)))
(assert (= $FixedPoint32_FixedPoint32_value 0))
(assert (= $FixedPoint32_FixedPoint32_type_value ($StructType $FixedPoint32_FixedPoint32 $EmptyTypeValueArray)))
(assert (= $DiemConfig_DiemConfig_payload 0))
(assert (forall (($tv0@@2 T@$TypeValue) ) (! (= ($DiemConfig_DiemConfig_type_value $tv0@@2) ($StructType $DiemConfig_DiemConfig ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@2) 1))) :pattern ( ($DiemConfig_DiemConfig_type_value $tv0@@2))
)))
(assert (= $DiemConfig_Configuration_epoch 0))
(assert (= $DiemConfig_Configuration_last_reconfiguration_time 1))
(assert (= $DiemConfig_Configuration_events 2))
(assert (= $DiemConfig_Configuration_type_value ($StructType $DiemConfig_Configuration $EmptyTypeValueArray)))
(assert (= $DiemConfig_DisableReconfiguration_dummy_field 0))
(assert (= $DiemConfig_DisableReconfiguration_type_value ($StructType $DiemConfig_DisableReconfiguration $EmptyTypeValueArray)))
(assert (= $DiemConfig_ModifyConfigCapability_dummy_field 0))
(assert (forall (($tv0@@3 T@$TypeValue) ) (! (= ($DiemConfig_ModifyConfigCapability_type_value $tv0@@3) ($StructType $DiemConfig_ModifyConfigCapability ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@3) 1))) :pattern ( ($DiemConfig_ModifyConfigCapability_type_value $tv0@@3))
)))
(assert (= $DiemConfig_NewEpochEvent_epoch 0))
(assert (= $DiemConfig_NewEpochEvent_type_value ($StructType $DiemConfig_NewEpochEvent $EmptyTypeValueArray)))
(assert (= $RegisteredCurrencies_RegisteredCurrencies_currency_codes 0))
(assert (= $RegisteredCurrencies_RegisteredCurrencies_type_value ($StructType $RegisteredCurrencies_RegisteredCurrencies $EmptyTypeValueArray)))
(assert (= $Diem_Diem_value 0))
(assert (forall (($tv0@@4 T@$TypeValue) ) (! (= ($Diem_Diem_type_value $tv0@@4) ($StructType $Diem_Diem ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@4) 1))) :pattern ( ($Diem_Diem_type_value $tv0@@4))
)))
(assert (= $Diem_BurnCapability_dummy_field 0))
(assert (forall (($tv0@@5 T@$TypeValue) ) (! (= ($Diem_BurnCapability_type_value $tv0@@5) ($StructType $Diem_BurnCapability ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@5) 1))) :pattern ( ($Diem_BurnCapability_type_value $tv0@@5))
)))
(assert (= $Diem_BurnEvent_amount 0))
(assert (= $Diem_BurnEvent_currency_code 1))
(assert (= $Diem_BurnEvent_preburn_address 2))
(assert (= $Diem_BurnEvent_type_value ($StructType $Diem_BurnEvent $EmptyTypeValueArray)))
(assert (= $Diem_CancelBurnEvent_amount 0))
(assert (= $Diem_CancelBurnEvent_currency_code 1))
(assert (= $Diem_CancelBurnEvent_preburn_address 2))
(assert (= $Diem_CancelBurnEvent_type_value ($StructType $Diem_CancelBurnEvent $EmptyTypeValueArray)))
(assert (= $Diem_CurrencyInfo_total_value 0))
(assert (= $Diem_CurrencyInfo_preburn_value 1))
(assert (= $Diem_CurrencyInfo_to_xdx_exchange_rate 2))
(assert (= $Diem_CurrencyInfo_is_synthetic 3))
(assert (= $Diem_CurrencyInfo_scaling_factor 4))
(assert (= $Diem_CurrencyInfo_fractional_part 5))
(assert (= $Diem_CurrencyInfo_currency_code 6))
(assert (= $Diem_CurrencyInfo_can_mint 7))
(assert (= $Diem_CurrencyInfo_mint_events 8))
(assert (= $Diem_CurrencyInfo_burn_events 9))
(assert (= $Diem_CurrencyInfo_preburn_events 10))
(assert (= $Diem_CurrencyInfo_cancel_burn_events 11))
(assert (= $Diem_CurrencyInfo_exchange_rate_update_events 12))
(assert (forall (($tv0@@6 T@$TypeValue) ) (! (= ($Diem_CurrencyInfo_type_value $tv0@@6) ($StructType $Diem_CurrencyInfo ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@6) 1))) :pattern ( ($Diem_CurrencyInfo_type_value $tv0@@6))
)))
(assert (= $Diem_MintCapability_dummy_field 0))
(assert (forall (($tv0@@7 T@$TypeValue) ) (! (= ($Diem_MintCapability_type_value $tv0@@7) ($StructType $Diem_MintCapability ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@7) 1))) :pattern ( ($Diem_MintCapability_type_value $tv0@@7))
)))
(assert (= $Diem_MintEvent_amount 0))
(assert (= $Diem_MintEvent_currency_code 1))
(assert (= $Diem_MintEvent_type_value ($StructType $Diem_MintEvent $EmptyTypeValueArray)))
(assert (= $Diem_Preburn_to_burn 0))
(assert (forall (($tv0@@8 T@$TypeValue) ) (! (= ($Diem_Preburn_type_value $tv0@@8) ($StructType $Diem_Preburn ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@8) 1))) :pattern ( ($Diem_Preburn_type_value $tv0@@8))
)))
(assert (= $Diem_PreburnEvent_amount 0))
(assert (= $Diem_PreburnEvent_currency_code 1))
(assert (= $Diem_PreburnEvent_preburn_address 2))
(assert (= $Diem_PreburnEvent_type_value ($StructType $Diem_PreburnEvent $EmptyTypeValueArray)))
(assert (= $Diem_ToXDXExchangeRateUpdateEvent_currency_code 0))
(assert (= $Diem_ToXDXExchangeRateUpdateEvent_new_to_xdx_exchange_rate 1))
(assert (= $Diem_ToXDXExchangeRateUpdateEvent_type_value ($StructType $Diem_ToXDXExchangeRateUpdateEvent $EmptyTypeValueArray)))
(assert (= $XUS_XUS_dummy_field 0))
(assert (= $XUS_XUS_type_value ($StructType $XUS_XUS $EmptyTypeValueArray)))
(assert (= $DesignatedDealer_Dealer_mint_event_handle 0))
(assert (= $DesignatedDealer_Dealer_type_value ($StructType $DesignatedDealer_Dealer $EmptyTypeValueArray)))
(assert (= $DesignatedDealer_ReceivedMintEvent_currency_code 0))
(assert (= $DesignatedDealer_ReceivedMintEvent_destination_address 1))
(assert (= $DesignatedDealer_ReceivedMintEvent_amount 2))
(assert (= $DesignatedDealer_ReceivedMintEvent_type_value ($StructType $DesignatedDealer_ReceivedMintEvent $EmptyTypeValueArray)))
(assert (= $DesignatedDealer_TierInfo_window_start 0))
(assert (= $DesignatedDealer_TierInfo_window_inflow 1))
(assert (= $DesignatedDealer_TierInfo_tiers 2))
(assert (forall (($tv0@@9 T@$TypeValue) ) (! (= ($DesignatedDealer_TierInfo_type_value $tv0@@9) ($StructType $DesignatedDealer_TierInfo ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@9) 1))) :pattern ( ($DesignatedDealer_TierInfo_type_value $tv0@@9))
)))
(assert (= $XDX_XDX_dummy_field 0))
(assert (= $XDX_XDX_type_value ($StructType $XDX_XDX $EmptyTypeValueArray)))
(assert (= $XDX_Reserve_mint_cap 0))
(assert (= $XDX_Reserve_burn_cap 1))
(assert (= $XDX_Reserve_preburn_cap 2))
(assert (= $XDX_Reserve_type_value ($StructType $XDX_Reserve $EmptyTypeValueArray)))
(assert (= $ValidatorOperatorConfig_ValidatorOperatorConfig_human_name 0))
(assert (= $ValidatorOperatorConfig_ValidatorOperatorConfig_type_value ($StructType $ValidatorOperatorConfig_ValidatorOperatorConfig $EmptyTypeValueArray)))
(assert (= $Option_Option_vec 0))
(assert (forall (($tv0@@10 T@$TypeValue) ) (! (= ($Option_Option_type_value $tv0@@10) ($StructType $Option_Option ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@10) 1))) :pattern ( ($Option_Option_type_value $tv0@@10))
)))
(assert (= $ValidatorConfig_Config_consensus_pubkey 0))
(assert (= $ValidatorConfig_Config_validator_network_addresses 1))
(assert (= $ValidatorConfig_Config_fullnode_network_addresses 2))
(assert (= $ValidatorConfig_Config_type_value ($StructType $ValidatorConfig_Config $EmptyTypeValueArray)))
(assert (= $ValidatorConfig_ValidatorConfig_config 0))
(assert (= $ValidatorConfig_ValidatorConfig_operator_account 1))
(assert (= $ValidatorConfig_ValidatorConfig_human_name 2))
(assert (= $ValidatorConfig_ValidatorConfig_type_value ($StructType $ValidatorConfig_ValidatorConfig $EmptyTypeValueArray)))
(assert (= $VASP_ChildVASP_parent_vasp_addr 0))
(assert (= $VASP_ChildVASP_type_value ($StructType $VASP_ChildVASP $EmptyTypeValueArray)))
(assert (= $VASP_ParentVASP_num_children 0))
(assert (= $VASP_ParentVASP_type_value ($StructType $VASP_ParentVASP $EmptyTypeValueArray)))
(assert (= $TransactionFee_TransactionFee_balance 0))
(assert (= $TransactionFee_TransactionFee_preburn 1))
(assert (forall (($tv0@@11 T@$TypeValue) ) (! (= ($TransactionFee_TransactionFee_type_value $tv0@@11) ($StructType $TransactionFee_TransactionFee ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@11) 1))) :pattern ( ($TransactionFee_TransactionFee_type_value $tv0@@11))
)))
603
(assert (forall ((account T@$Value) (seq_nonce T@$Value) )  (and (and ((_ is $Integer) ($SlidingNonce_spec_try_record_nonce account seq_nonce)) (>= (|i#$Integer| ($SlidingNonce_spec_try_record_nonce account seq_nonce)) 0)) (<= (|i#$Integer| ($SlidingNonce_spec_try_record_nonce account seq_nonce)) $MAX_U64))))
604
605
606
(assert (= $SlidingNonce_SlidingNonce_min_nonce 0))
(assert (= $SlidingNonce_SlidingNonce_nonce_mask 1))
(assert (= $SlidingNonce_SlidingNonce_type_value ($StructType $SlidingNonce_SlidingNonce $EmptyTypeValueArray)))
607
(assert (forall ((payer T@$Value) (metadata T@$Value) (deposit_value T@$Value) )  (and (and ((_ is $Vector) ($DualAttestation_spec_dual_attestation_message payer metadata deposit_value)) (let ((va@@8 (|v#$Vector| ($DualAttestation_spec_dual_attestation_message payer metadata deposit_value))))
608
609
(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))
610
)))))) (forall (($$0 Int) ) (!  (=> (and (>= $$0 0) (< $$0 (|l#$ValueArray| (|v#$Vector| ($DualAttestation_spec_dual_attestation_message payer metadata deposit_value))))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DualAttestation_spec_dual_attestation_message payer metadata deposit_value))) $$0)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DualAttestation_spec_dual_attestation_message payer metadata deposit_value))) $$0)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DualAttestation_spec_dual_attestation_message payer metadata deposit_value))) $$0)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DualAttestation_spec_dual_attestation_message payer metadata deposit_value))) $$0))
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
)))))
(assert (= $DualAttestation_BaseUrlRotationEvent_new_base_url 0))
(assert (= $DualAttestation_BaseUrlRotationEvent_time_rotated_seconds 1))
(assert (= $DualAttestation_BaseUrlRotationEvent_type_value ($StructType $DualAttestation_BaseUrlRotationEvent $EmptyTypeValueArray)))
(assert (= $DualAttestation_ComplianceKeyRotationEvent_new_compliance_public_key 0))
(assert (= $DualAttestation_ComplianceKeyRotationEvent_time_rotated_seconds 1))
(assert (= $DualAttestation_ComplianceKeyRotationEvent_type_value ($StructType $DualAttestation_ComplianceKeyRotationEvent $EmptyTypeValueArray)))
(assert (= $DualAttestation_Credential_human_name 0))
(assert (= $DualAttestation_Credential_base_url 1))
(assert (= $DualAttestation_Credential_compliance_public_key 2))
(assert (= $DualAttestation_Credential_expiration_date 3))
(assert (= $DualAttestation_Credential_compliance_key_rotation_events 4))
(assert (= $DualAttestation_Credential_base_url_rotation_events 5))
(assert (= $DualAttestation_Credential_type_value ($StructType $DualAttestation_Credential $EmptyTypeValueArray)))
(assert (= $DualAttestation_Limit_micro_xdx_limit 0))
(assert (= $DualAttestation_Limit_type_value ($StructType $DualAttestation_Limit $EmptyTypeValueArray)))
(assert (= $DiemTransactionPublishingOption_DiemTransactionPublishingOption_script_allow_list 0))
(assert (= $DiemTransactionPublishingOption_DiemTransactionPublishingOption_module_publishing_allowed 1))
(assert (= $DiemTransactionPublishingOption_DiemTransactionPublishingOption_type_value ($StructType $DiemTransactionPublishingOption_DiemTransactionPublishingOption $EmptyTypeValueArray)))
630
(assert (forall ((auth_key_prefix T@$Value) )  (and (and ((_ is $Vector) ($DiemAccount_spec_abstract_create_authentication_key auth_key_prefix)) (let ((va@@9 (|v#$Vector| ($DiemAccount_spec_abstract_create_authentication_key auth_key_prefix))))
631
632
(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))
633
)))))) (forall (($$0@@0 Int) ) (!  (=> (and (>= $$0@@0 0) (< $$0@@0 (|l#$ValueArray| (|v#$Vector| ($DiemAccount_spec_abstract_create_authentication_key auth_key_prefix))))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DiemAccount_spec_abstract_create_authentication_key auth_key_prefix))) $$0@@0)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DiemAccount_spec_abstract_create_authentication_key auth_key_prefix))) $$0@@0)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DiemAccount_spec_abstract_create_authentication_key auth_key_prefix))) $$0@@0)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($DiemAccount_spec_abstract_create_authentication_key auth_key_prefix))) $$0@@0))
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
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
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
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
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
)))))
(assert (= $DiemAccount_DiemAccount_authentication_key 0))
(assert (= $DiemAccount_DiemAccount_withdraw_capability 1))
(assert (= $DiemAccount_DiemAccount_key_rotation_capability 2))
(assert (= $DiemAccount_DiemAccount_received_events 3))
(assert (= $DiemAccount_DiemAccount_sent_events 4))
(assert (= $DiemAccount_DiemAccount_sequence_number 5))
(assert (= $DiemAccount_DiemAccount_type_value ($StructType $DiemAccount_DiemAccount $EmptyTypeValueArray)))
(assert (= $DiemAccount_AccountOperationsCapability_limits_cap 0))
(assert (= $DiemAccount_AccountOperationsCapability_creation_events 1))
(assert (= $DiemAccount_AccountOperationsCapability_type_value ($StructType $DiemAccount_AccountOperationsCapability $EmptyTypeValueArray)))
(assert (= $DiemAccount_AdminTransactionEvent_committed_timestamp_secs 0))
(assert (= $DiemAccount_AdminTransactionEvent_type_value ($StructType $DiemAccount_AdminTransactionEvent $EmptyTypeValueArray)))
(assert (= $DiemAccount_Balance_coin 0))
(assert (forall (($tv0@@12 T@$TypeValue) ) (! (= ($DiemAccount_Balance_type_value $tv0@@12) ($StructType $DiemAccount_Balance ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0@@12) 1))) :pattern ( ($DiemAccount_Balance_type_value $tv0@@12))
)))
(assert (= $DiemAccount_CreateAccountEvent_created 0))
(assert (= $DiemAccount_CreateAccountEvent_role_id 1))
(assert (= $DiemAccount_CreateAccountEvent_type_value ($StructType $DiemAccount_CreateAccountEvent $EmptyTypeValueArray)))
(assert (= $DiemAccount_DiemWriteSetManager_upgrade_events 0))
(assert (= $DiemAccount_DiemWriteSetManager_type_value ($StructType $DiemAccount_DiemWriteSetManager $EmptyTypeValueArray)))
(assert (= $DiemAccount_KeyRotationCapability_account_address 0))
(assert (= $DiemAccount_KeyRotationCapability_type_value ($StructType $DiemAccount_KeyRotationCapability $EmptyTypeValueArray)))
(assert (= $DiemAccount_ReceivedPaymentEvent_amount 0))
(assert (= $DiemAccount_ReceivedPaymentEvent_currency_code 1))
(assert (= $DiemAccount_ReceivedPaymentEvent_payer 2))
(assert (= $DiemAccount_ReceivedPaymentEvent_metadata 3))
(assert (= $DiemAccount_ReceivedPaymentEvent_type_value ($StructType $DiemAccount_ReceivedPaymentEvent $EmptyTypeValueArray)))
(assert (= $DiemAccount_SentPaymentEvent_amount 0))
(assert (= $DiemAccount_SentPaymentEvent_currency_code 1))
(assert (= $DiemAccount_SentPaymentEvent_payee 2))
(assert (= $DiemAccount_SentPaymentEvent_metadata 3))
(assert (= $DiemAccount_SentPaymentEvent_type_value ($StructType $DiemAccount_SentPaymentEvent $EmptyTypeValueArray)))
(assert (= $DiemAccount_WithdrawCapability_account_address 0))
(assert (= $DiemAccount_WithdrawCapability_type_value ($StructType $DiemAccount_WithdrawCapability $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 $DiemAccount_DiemAccount_$memory () T@$Memory)
(declare-fun account@@0 () T@$Value)
(declare-fun $abort_flag@18 () Bool)
(declare-fun |Select_[$TypeValueArray,$int]$Value| (|T@[$TypeValueArray,Int]$Value| T@$TypeValueArray Int) T@$Value)
(declare-fun new_key () T@$Value)
(declare-fun $abort_code@30 () Int)
(declare-fun $DiemAccount_DiemAccount_$memory@4 () T@$Memory)
(declare-fun $DiemAccount_DiemAccount_$memory@3 () T@$Memory)
(declare-fun $abort_code@29 () Int)
(declare-fun $abort_flag@17 () Bool)
(declare-fun $abort_code@28 () Int)
(declare-fun $DiemAccount_DiemAccount_$memory@2 () T@$Memory)
(declare-fun $abort_flag@13 () Bool)
(declare-fun $abort_code@22 () Int)
(declare-fun $DiemAccount_DiemAccount_$memory@1 () T@$Memory)
(declare-fun $abort_flag@9 () Bool)
(declare-fun $abort_code@15 () Int)
(declare-fun $DiemAccount_DiemAccount_$memory@0 () T@$Memory)
(declare-fun $abort_flag@16 () Bool)
(declare-fun |inline$$WritebackToGlobal$2$m'@2| () T@$Memory)
(declare-fun $abort_code@26 () Int)
(declare-fun inline$$WritebackToGlobal$2$l@1 () T@$Location)
(declare-fun inline$$WritebackToGlobal$2$ta@1 () T@$TypeValueArray)
(declare-fun inline$$WritebackToGlobal$2$a@1 () Int)
(declare-fun inline$$WritebackToGlobal$2$v@1 () T@$Value)
(declare-fun |inline$$WritebackToReference$2$dst'@2| () T@$Mutation)
(declare-fun |inline$$WritebackToGlobal$2$m'@1| () T@$Memory)
(declare-fun |Store_[$TypeValueArray,$int]$Value| (|T@[$TypeValueArray,Int]$Value| T@$TypeValueArray Int T@$Value) |T@[$TypeValueArray,Int]$Value|)
(assert (forall ( ( ?x0 |T@[$TypeValueArray,Int]$Value|) ( ?x1 T@$TypeValueArray) ( ?x2 Int) ( ?x3 T@$Value)) (= (|Select_[$TypeValueArray,$int]$Value| (|Store_[$TypeValueArray,$int]$Value| ?x0 ?x1 ?x2 ?x3) ?x1 ?x2)  ?x3)))
(assert (forall ( ( ?x0 |T@[$TypeValueArray,Int]$Value|) ( ?x1 T@$TypeValueArray) ( ?y1 T@$TypeValueArray) ( ?x2 Int) ( ?y2 Int) ( ?x3 T@$Value)) (=> (or  (not (= ?x1 ?y1)) (not (= ?x2 ?y2))) (= (|Select_[$TypeValueArray,$int]$Value| (|Store_[$TypeValueArray,$int]$Value| ?x0 ?x1 ?x2 ?x3) ?y1 ?y2) (|Select_[$TypeValueArray,$int]$Value| ?x0 ?y1 ?y2)))))
(declare-fun inline$$DiemAccount_DiemAccount_$pack_ref$3$$after@0 () T@$Value)
(declare-fun inline$$BorrowGlobal$2$dst@2 () T@$Mutation)
(declare-fun |inline$$WriteRef$2$to'@1| () T@$Mutation)
(declare-fun inline$$WritebackToReference$2$dstPath@1 () T@$Path)
(declare-fun inline$$WritebackToReference$2$srcPath@1 () T@$Path)
(declare-fun |inline$$WritebackToReference$2$dst'@1| () T@$Mutation)
(declare-fun inline$$Option_Option_$pack_ref$1$$after@0 () T@$Value)
(declare-fun inline$$Option_Option_$pack_ref$1$$tv0@0 () T@$TypeValue)
(declare-fun inline$$DiemAccount_restore_key_rotation_capability_$def$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$2$dst@1 () T@$Mutation)
(declare-fun call5formal@$ret0@0 () T@$Value)
(declare-fun $abort_code@27 () Int)
(declare-fun $abort_code@23 () Int)
(declare-fun $abort_flag@14 () Bool)
(declare-fun $abort_code@25 () Int)
(declare-fun $abort_flag@15 () Bool)
(declare-fun inline$$ReadRef$1$v@1 () T@$Value)
(declare-fun call0formal@$tv0@0 () T@$TypeValue)
(declare-fun inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2 () T@$Value)
(declare-fun inline$$Option_Option_$unpack_ref$1$$before@0 () T@$Value)
(declare-fun inline$$Option_Option_$unpack_ref$1$$tv0@0 () T@$TypeValue)
(declare-fun inline$$BorrowField$2$p@1 () T@$Path)
(declare-fun inline$$BorrowField$2$size@1 () Int)
(declare-fun inline$$BorrowField$2$p@2 () T@$Path)
(declare-fun inline$$DiemAccount_DiemAccount_$unpack_ref$2$$before@0 () T@$Value)
(declare-fun inline$$BorrowGlobal$2$dst@0 () T@$Mutation)
(declare-fun inline$$BorrowGlobal$2$a@1 () Int)
(declare-fun inline$$BorrowGlobal$2$dst@1 () T@$Mutation)
(declare-fun inline$$GetFieldFromValue$4$dst@1 () T@$Value)
(declare-fun inline$$DiemAccount_exists_at_$def$3$$t2@1 () T@$Value)
(declare-fun $abort_code@24 () Int)
(declare-fun call3formal@$ret0@0 () T@$Value)
(declare-fun inline$$DiemAccount_restore_key_rotation_capability_$def$0$$t7@1 () T@$Value)
(declare-fun inline$$GetFieldFromValue$3$dst@1 () T@$Value)
(declare-fun $abort_flag@12 () Bool)
(declare-fun |inline$$WritebackToGlobal$1$m'@2| () T@$Memory)
(declare-fun $abort_code@19 () Int)
(declare-fun inline$$WritebackToGlobal$1$l@1 () T@$Location)
(declare-fun inline$$WritebackToGlobal$1$ta@1 () T@$TypeValueArray)
(declare-fun inline$$WritebackToGlobal$1$a@1 () Int)
(declare-fun inline$$WritebackToGlobal$1$v@1 () T@$Value)
(declare-fun |inline$$WritebackToReference$1$dst'@2| () T@$Mutation)
(declare-fun |inline$$WritebackToGlobal$1$m'@1| () T@$Memory)
(declare-fun inline$$DiemAccount_DiemAccount_$pack_ref$2$$after@0 () T@$Value)
(declare-fun inline$$BorrowGlobal$1$dst@2 () T@$Mutation)
(declare-fun |inline$$WriteRef$1$to'@1| () T@$Mutation)
(declare-fun inline$$WritebackToReference$1$dstPath@1 () T@$Path)
(declare-fun inline$$WritebackToReference$1$srcPath@1 () T@$Path)
(declare-fun |inline$$WritebackToReference$1$dst'@1| () T@$Mutation)
(declare-fun inline$$DiemAccount_rotate_authentication_key_$def$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$1$dst@1 () T@$Mutation)
(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$$DiemAccount_rotate_authentication_key_$def$0$$t16@1 () T@$Value)
(declare-fun $abort_code@21 () Int)
(declare-fun $abort_code@16 () Int)
(declare-fun $abort_flag@10 () Bool)
(declare-fun $abort_code@18 () Int)
(declare-fun $abort_flag@11 () Bool)
(declare-fun $abort_code@20 () Int)
(declare-fun call3formal@$ret0@0@@0 () T@$Value)
(declare-fun inline$$DiemAccount_DiemAccount_$pack_ref$1$$after@0 () T@$Value)
(declare-fun inline$$DiemAccount_rotate_authentication_key_$def$0$$t15@1 () T@$Value)
(declare-fun inline$$Vector_length$0$l@1 () T@$Value)
(declare-fun inline$$DiemAccount_rotate_authentication_key_$def$0$$t17@1 () T@$Value)
(declare-fun inline$$Vector_length$0$ta@0 () T@$TypeValue)
(declare-fun inline$$DiemAccount_DiemAccount_$unpack_ref$1$$before@0 () T@$Value)
(declare-fun inline$$BorrowGlobal$1$dst@0 () T@$Mutation)
(declare-fun inline$$BorrowGlobal$1$a@1 () Int)
(declare-fun inline$$BorrowGlobal$1$dst@1 () T@$Mutation)
(declare-fun inline$$GetFieldFromValue$2$dst@1 () T@$Value)
(declare-fun inline$$DiemAccount_exists_at_$def$2$$t2@1 () T@$Value)
(declare-fun $abort_code@17 () Int)
(declare-fun call3formal@$ret0@0@@1 () T@$Value)
(declare-fun inline$$DiemAccount_rotate_authentication_key_$def$0$$t11@1 () T@$Value)
(declare-fun inline$$GetFieldFromValue$1$dst@1 () T@$Value)
(declare-fun call4formal@$ret0@0 () T@$Value)
(declare-fun $abort_flag@8 () Bool)
(declare-fun $abort_code@13 () Int)
(declare-fun |inline$$WritebackToGlobal$0$m'@2| () T@$Memory)
(declare-fun inline$$WritebackToGlobal$0$l@1 () T@$Location)
(declare-fun inline$$WritebackToGlobal$0$ta@1 () T@$TypeValueArray)
(declare-fun inline$$WritebackToGlobal$0$a@1 () Int)
(declare-fun inline$$WritebackToGlobal$0$v@1 () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2| () T@$Mutation)
(declare-fun |inline$$WritebackToGlobal$0$m'@1| () T@$Memory)
(declare-fun inline$$DiemAccount_DiemAccount_$pack_ref$0$$after@0 () T@$Value)
(declare-fun inline$$BorrowGlobal$0$dst@2 () 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$$Option_Option_$pack_ref$0$$after@0 () T@$Value)
(declare-fun inline$$Option_Option_$pack_ref$0$$tv0@0 () T@$TypeValue)
(declare-fun inline$$DiemAccount_extract_key_rotation_capability_$def$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1 () T@$Mutation)
(declare-fun call5formal@$ret1@0 () T@$Value)
(declare-fun inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@1 () T@$Value)
(declare-fun $abort_code@14 () Int)
(declare-fun $abort_code@1 () Int)
(declare-fun $abort_flag@0 () Bool)
(declare-fun $abort_code@8 () Int)
(declare-fun $abort_flag@5 () Bool)
(declare-fun $abort_code@10 () Int)
(declare-fun $abort_flag@6 () Bool)
(declare-fun $abort_code@12 () Int)
(declare-fun $abort_flag@7 () Bool)
(declare-fun inline$$ReadRef$0$v@1 () T@$Value)
(declare-fun call0formal@$tv0@0@@0 () T@$TypeValue)
(declare-fun inline$$Option_Option_$unpack_ref$0$$before@0 () T@$Value)
(declare-fun inline$$Option_Option_$unpack_ref$0$$tv0@0 () T@$TypeValue)
(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 inline$$DiemAccount_DiemAccount_$unpack_ref$0$$before@0 () T@$Value)
(declare-fun inline$$BorrowGlobal$0$dst@0 () T@$Mutation)
(declare-fun inline$$BorrowGlobal$0$a@1 () Int)
(declare-fun inline$$BorrowGlobal$0$dst@1 () T@$Mutation)
(declare-fun call3formal@$ret0@0@@2 () T@$Value)
(declare-fun inline$$DiemAccount_exists_at_$def$1$$t2@1 () T@$Value)
(declare-fun $abort_code@11 () Int)
(declare-fun call3formal@$ret0@0@@3 () T@$Value)
(declare-fun inline$$DiemAccount_extract_key_rotation_capability_$def$0$$t13@1 () T@$Value)
(declare-fun inline$$Not$0$dst@1 () T@$Value)
(declare-fun $abort_code@9 () Int)
(declare-fun call3formal@$ret0@0@@4 () T@$Value)
(declare-fun inline$$DiemAccount_extract_key_rotation_capability_$def$0$$t10@1 () T@$Value)
(declare-fun inline$$DiemAccount_delegated_key_rotation_capability_$def$0$$ret0@2 () T@$Value)
(declare-fun $abort_flag@4 () Bool)
(declare-fun $abort_code@7 () Int)
(declare-fun $abort_code@5 () Int)
(declare-fun call4formal@$ret0@0@@0 () T@$Value)
(declare-fun $abort_flag@3 () Bool)
(declare-fun inline$$DiemAccount_delegated_key_rotation_capability_$def$0$$ret0@1 () T@$Value)
(declare-fun $abort_code@6 () Int)
(declare-fun $abort_code@2 () Int)
(declare-fun $abort_flag@1 () Bool)
(declare-fun $abort_code@4 () Int)
(declare-fun $abort_flag@2 () Bool)
(declare-fun call0formal@$tv0@0@@1 () T@$TypeValue)
(declare-fun inline$$GetFieldFromValue$0$dst@1 () T@$Value)
(declare-fun inline$$GetGlobal$0$dst@2 () T@$Value)
(declare-fun inline$$GetGlobal$0$dst@0 () T@$Value)
(declare-fun inline$$GetGlobal$0$a@1 () Int)
(declare-fun inline$$GetGlobal$0$dst@1 () T@$Value)
(declare-fun inline$$DiemAccount_exists_at_$def$0$$t2@1 () T@$Value)
(declare-fun $abort_code@3 () Int)
(declare-fun call3formal@$ret0@0@@5 () T@$Value)
(declare-fun inline$$DiemAccount_delegated_key_rotation_capability_$def$0$$t5@1 () T@$Value)
(declare-fun $Option_Option_$memory () T@$Memory)
(declare-fun $DiemAccount_KeyRotationCapability_$memory () T@$Memory)
(declare-fun $Roles_RoleId_$memory () T@$Memory)
(declare-fun $AccountFreezing_FreezingBit_$memory () T@$Memory)
(declare-fun $DiemTimestamp_CurrentTimeMicroseconds_$memory () T@$Memory)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 310690) (let ((anon0$2_correct  (and (=> (= (ControlFlow 0 308727) (- 0 316980)) (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0))))))) $abort_flag@18)) (=> (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0))))))) $abort_flag@18) (and (=> (= (ControlFlow 0 308727) (- 0 316998)) (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) $abort_flag@18)) (=> (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) $abort_flag@18) (and (=> (= (ControlFlow 0 308727) (- 0 317010)) (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($Vector_$borrow $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec) ($Integer 0)))) $DiemAccount_KeyRotationCapability_account_address)))))))) $abort_flag@18)) (=> (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($Vector_$borrow $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec) ($Integer 0)))) $DiemAccount_KeyRotationCapability_account_address)))))))) $abort_flag@18) (and (=> (= (ControlFlow 0 308727) (- 0 317033)) (=> (|b#$Boolean| ($Boolean  (not ($IsEqual_stratified ($Integer (|l#$ValueArray| (|v#$Vector| new_key))) ($Integer 32))))) $abort_flag@18)) (=> (=> (|b#$Boolean| ($Boolean  (not ($IsEqual_stratified ($Integer (|l#$ValueArray| (|v#$Vector| new_key))) ($Integer 32))))) $abort_flag@18) (and (=> (= (ControlFlow 0 308727) (- 0 317052)) (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) $abort_flag@18)) (=> (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) $abort_flag@18) (and (=> (= (ControlFlow 0 308727) (- 0 317064)) (=> $abort_flag@18 (or (or (or (or (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0))))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0))))) (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($Vector_$borrow $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec) ($Integer 0)))) $DiemAccount_KeyRotationCapability_account_address))))))))) (|b#$Boolean| ($Boolean  (not ($IsEqual_stratified ($Integer (|l#$ValueArray| (|v#$Vector| new_key))) ($Integer 32)))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0))))))) (=> (=> $abort_flag@18 (or (or (or (or (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0))))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0))))) (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($Vector_$borrow $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec) ($Integer 0)))) $DiemAccount_KeyRotationCapability_account_address))))))))) (|b#$Boolean| ($Boolean  (not ($IsEqual_stratified ($Integer (|l#$ValueArray| (|v#$Vector| new_key))) ($Integer 32)))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))))) (and (=> (= (ControlFlow 0 308727) (- 0 317144)) (=> $abort_flag@18 (or (or (or (or (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0))))))) (= $abort_code@30 (|i#$Integer| ($Integer 5)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@30 (|i#$Integer| ($Integer 1))))) (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($Vector_$borrow $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec) ($Integer 0)))) $DiemAccount_KeyRotationCapability_account_address)))))))) (= $abort_code@30 (|i#$Integer| ($Integer 5))))) (and (|b#$Boolean| ($Boolean  (not ($IsEqual_stratified ($Integer (|l#$ValueArray| (|v#$Vector| new_key))) ($Integer 32))))) (= $abort_code@30 (|i#$Integer| ($Integer 7))))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@30 (|i#$Integer| ($Integer 1))))))) (=> (=> $abort_flag@18 (or (or (or (or (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0))))))) (= $abort_code@30 (|i#$Integer| ($Integer 5)))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@30 (|i#$Integer| ($Integer 1))))) (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| ($Vector_$borrow $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec) ($Integer 0)))) $DiemAccount_KeyRotationCapability_account_address)))))))) (= $abort_code@30 (|i#$Integer| ($Integer 5))))) (and (|b#$Boolean| ($Boolean  (not ($IsEqual_stratified ($Integer (|l#$ValueArray| (|v#$Vector| new_key))) ($Integer 32))))) (= $abort_code@30 (|i#$Integer| ($Integer 7))))) (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $DiemAccount_KeyRotationCapability_type_value (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@30 (|i#$Integer| ($Integer 1)))))) (and (=> (= (ControlFlow 0 308727) (- 0 317279)) (=> $abort_flag@18 (or (= $abort_code@30 (|i#$Integer| ($Integer 1))) (= $abort_code@30 (|i#$Integer| ($Integer 7)))))) (=> (=> $abort_flag@18 (or (= $abort_code@30 (|i#$Integer| ($Integer 1))) (= $abort_code@30 (|i#$Integer| ($Integer 7))))) (=> (= (ControlFlow 0 308727) (- 0 317302)) (=> (not $abort_flag@18) (|b#$Boolean| ($Boolean ($IsEqual_stratified (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory@4) $EmptyTypeValueArray (|a#$Address| account@@0)))) $DiemAccount_DiemAccount_authentication_key) new_key)))))))))))))))))))))))
(let ((inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$Abort_correct  (=> (and (and (= $abort_flag@18 true) (= $DiemAccount_DiemAccount_$memory@4 $DiemAccount_DiemAccount_$memory@3)) (and (= $abort_code@30 $abort_code@29) (= (ControlFlow 0 308697) 308727))) anon0$2_correct)))
(let ((inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon15_Then_correct  (=> (and (and $abort_flag@17 (= $abort_code@29 $abort_code@28)) (and (= $DiemAccount_DiemAccount_$memory@3 $DiemAccount_DiemAccount_$memory@2) (= (ControlFlow 0 308693) 308697))) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$Abort_correct)))
(let ((inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon14_Then_correct  (=> (and (and $abort_flag@13 (= $abort_code@29 $abort_code@22)) (and (= $DiemAccount_DiemAccount_$memory@3 $DiemAccount_DiemAccount_$memory@1) (= (ControlFlow 0 308701) 308697))) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$Abort_correct)))
(let ((inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon13_Then_correct  (=> (and (and $abort_flag@9 (= $abort_code@29 $abort_code@15)) (and (= $DiemAccount_DiemAccount_$memory@3 $DiemAccount_DiemAccount_$memory@0) (= (ControlFlow 0 308705) 308697))) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$Abort_correct)))
(let ((inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon15_Else_correct  (=> (not $abort_flag@17) (=> (and (and (= $abort_flag@18 $abort_flag@17) (= $DiemAccount_DiemAccount_$memory@4 $DiemAccount_DiemAccount_$memory@2)) (and (= $abort_code@30 $abort_code@28) (= (ControlFlow 0 308689) 308727))) anon0$2_correct))))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon22$4_correct  (=> (= $abort_flag@17 $abort_flag@16) (=> (and (= $DiemAccount_DiemAccount_$memory@2 |inline$$WritebackToGlobal$2$m'@2|) (= $abort_code@28 $abort_code@26)) (and (=> (= (ControlFlow 0 308589) 308693) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon15_Then_correct) (=> (= (ControlFlow 0 308589) 308689) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon15_Else_correct))))))
876
877
(let ((inline$$WritebackToGlobal$2$anon3_Else_correct  (=> (not ((_ is $Global) inline$$WritebackToGlobal$2$l@1)) (=> (and (= |inline$$WritebackToGlobal$2$m'@2| $DiemAccount_DiemAccount_$memory@1) (= (ControlFlow 0 308527) 308589)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon22$4_correct))))
(let ((inline$$WritebackToGlobal$2$anon3_Then_correct  (=> ((_ is $Global) inline$$WritebackToGlobal$2$l@1) (=> (and (= inline$$WritebackToGlobal$2$ta@1 (|ts#$Global| inline$$WritebackToGlobal$2$l@1)) (= inline$$WritebackToGlobal$2$a@1 (|a#$Global| inline$$WritebackToGlobal$2$l@1))) (=> (and (and (= inline$$WritebackToGlobal$2$v@1 ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$2$dst'@2|) 0 (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory@1) inline$$WritebackToGlobal$2$ta@1 inline$$WritebackToGlobal$2$a@1) (|v#$Mutation| |inline$$WritebackToReference$2$dst'@2|))) (= |inline$$WritebackToGlobal$2$m'@1| ($Memory (|domain#$Memory| $DiemAccount_DiemAccount_$memory@1) (|Store_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory@1) inline$$WritebackToGlobal$2$ta@1 inline$$WritebackToGlobal$2$a@1 inline$$WritebackToGlobal$2$v@1)))) (and (= |inline$$WritebackToGlobal$2$m'@2| |inline$$WritebackToGlobal$2$m'@1|) (= (ControlFlow 0 308581) 308589))) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon22$4_correct)))))
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
(let ((inline$$WritebackToGlobal$2$anon0_correct  (=> (= inline$$WritebackToGlobal$2$l@1 (|l#$Mutation| |inline$$WritebackToReference$2$dst'@2|)) (and (=> (= (ControlFlow 0 308517) 308581) inline$$WritebackToGlobal$2$anon3_Then_correct) (=> (= (ControlFlow 0 308517) 308527) inline$$WritebackToGlobal$2$anon3_Else_correct)))))
(let ((inline$$DiemAccount_DiemAccount_$pack_ref$3$Entry_correct  (=> (and (= inline$$DiemAccount_DiemAccount_$pack_ref$3$$after@0 (|v#$Mutation| |inline$$WritebackToReference$2$dst'@2|)) (= (ControlFlow 0 308395) 308517)) inline$$WritebackToGlobal$2$anon0_correct)))
(let ((inline$$WritebackToReference$2$anon3_Else_correct  (=> (not (and (and (= (|l#$Mutation| inline$$BorrowGlobal$2$dst@2) (|l#$Mutation| |inline$$WriteRef$2$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$2$dstPath@1) (|size#$Path| inline$$WritebackToReference$2$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$2$dstPath@1 inline$$WritebackToReference$2$srcPath@1))) (=> (and (= |inline$$WritebackToReference$2$dst'@2| inline$$BorrowGlobal$2$dst@2) (= (ControlFlow 0 308316) 308395)) inline$$DiemAccount_DiemAccount_$pack_ref$3$Entry_correct))))
(let ((inline$$WritebackToReference$2$anon3_Then_correct  (=> (and (and (and (and (= (|l#$Mutation| inline$$BorrowGlobal$2$dst@2) (|l#$Mutation| |inline$$WriteRef$2$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$2$dstPath@1) (|size#$Path| inline$$WritebackToReference$2$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$2$dstPath@1 inline$$WritebackToReference$2$srcPath@1)) (= |inline$$WritebackToReference$2$dst'@1| ($Mutation (|l#$Mutation| inline$$BorrowGlobal$2$dst@2) inline$$WritebackToReference$2$dstPath@1 ($UpdateValue_stratified inline$$WritebackToReference$2$srcPath@1 (|size#$Path| inline$$WritebackToReference$2$dstPath@1) (|v#$Mutation| inline$$BorrowGlobal$2$dst@2) (|v#$Mutation| |inline$$WriteRef$2$to'@1|))))) (and (= |inline$$WritebackToReference$2$dst'@2| |inline$$WritebackToReference$2$dst'@1|) (= (ControlFlow 0 308372) 308395))) inline$$DiemAccount_DiemAccount_$pack_ref$3$Entry_correct)))
(let ((inline$$WritebackToReference$2$anon0_correct  (=> (and (= inline$$WritebackToReference$2$srcPath@1 (|p#$Mutation| |inline$$WriteRef$2$to'@1|)) (= inline$$WritebackToReference$2$dstPath@1 (|p#$Mutation| inline$$BorrowGlobal$2$dst@2))) (and (=> (= (ControlFlow 0 308280) 308372) inline$$WritebackToReference$2$anon3_Then_correct) (=> (= (ControlFlow 0 308280) 308316) inline$$WritebackToReference$2$anon3_Else_correct)))))
(let ((inline$$Option_Option_$pack_ref$1$anon0_correct  (and (=> (= (ControlFlow 0 308139) (- 0 316584)) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_Option_$pack_ref$1$$after@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (=> (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_Option_$pack_ref$1$$after@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (=> (= (ControlFlow 0 308139) 308280) inline$$WritebackToReference$2$anon0_correct)))))
(let ((inline$$Option_Option_$pack_ref$1$Entry_correct  (=> (= inline$$Option_Option_$pack_ref$1$$tv0@0 $DiemAccount_KeyRotationCapability_type_value) (=> (and (= inline$$Option_Option_$pack_ref$1$$after@0 (|v#$Mutation| |inline$$WriteRef$2$to'@1|)) (= (ControlFlow 0 308115) 308139)) inline$$Option_Option_$pack_ref$1$anon0_correct))))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon33_Else_correct  (=> (and (not true) (= (ControlFlow 0 308069) 308115)) inline$$Option_Option_$pack_ref$1$Entry_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon33_Then_correct  (=> (and (= inline$$DiemAccount_restore_key_rotation_capability_$def$0$$trace_temp@1 (|v#$Mutation| inline$$BorrowGlobal$2$dst@2)) (= (ControlFlow 0 308599) 308115)) inline$$Option_Option_$pack_ref$1$Entry_correct)))
(let ((inline$$WriteRef$2$anon0_correct  (=> (= |inline$$WriteRef$2$to'@1| ($Mutation (|l#$Mutation| inline$$BorrowField$2$dst@1) (|p#$Mutation| inline$$BorrowField$2$dst@1) call5formal@$ret0@0)) (and (=> (= (ControlFlow 0 308055) 308599) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon33_Then_correct) (=> (= (ControlFlow 0 308055) 308069) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon33_Else_correct)))))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon31_Else_correct  (=> (and (not $abort_flag@16) (= (ControlFlow 0 308061) 308055)) inline$$WriteRef$2$anon0_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$Abort_correct  (=> (= $abort_flag@17 true) (=> (and (= $DiemAccount_DiemAccount_$memory@2 $DiemAccount_DiemAccount_$memory@1) (= $abort_code@28 $abort_code@27)) (and (=> (= (ControlFlow 0 307498) 308693) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon15_Then_correct) (=> (= (ControlFlow 0 307498) 308689) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon15_Else_correct))))))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon7_correct  (=> (and (= $abort_code@27 $abort_code@23) (= (ControlFlow 0 308651) 307498)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon26_Else_correct  (=> (and (not true) (= (ControlFlow 0 308649) 308651)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon7_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon26_Then_correct  (=> (= (ControlFlow 0 308659) 308651) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon7_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon25_Then_correct  (=> $abort_flag@14 (and (=> (= (ControlFlow 0 308643) 308659) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon26_Then_correct) (=> (= (ControlFlow 0 308643) 308649) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon26_Else_correct)))))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon15_correct  (=> (and (= $abort_code@27 $abort_code@25) (= (ControlFlow 0 308631) 307498)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon30_Else_correct  (=> (and (not true) (= (ControlFlow 0 308629) 308631)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon15_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon30_Then_correct  (=> (= (ControlFlow 0 308639) 308631) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon15_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Then_correct  (=> $abort_flag@15 (and (=> (= (ControlFlow 0 308623) 308639) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon30_Then_correct) (=> (= (ControlFlow 0 308623) 308629) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon30_Else_correct)))))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon19_correct  (=> (and (= $abort_code@27 $abort_code@26) (= (ControlFlow 0 308611) 307498)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon32_Else_correct  (=> (and (not true) (= (ControlFlow 0 308609) 308611)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon19_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon32_Then_correct  (=> (= (ControlFlow 0 308619) 308611) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon19_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon31_Then_correct  (=> $abort_flag@16 (and (=> (= (ControlFlow 0 308603) 308619) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon32_Then_correct) (=> (= (ControlFlow 0 308603) 308609) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon32_Else_correct)))))
902
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Else$4_correct  (and (=> (= (ControlFlow 0 307998) (- 0 316423)) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (=> (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (=> (and (= call0formal@$tv0@0 $DiemAccount_KeyRotationCapability_type_value) (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length call0formal@$tv0@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1)) $Option_Option_vec)) ($Integer 0))))))) $abort_flag@16)) (=> (and (and (=> $abort_flag@16 (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length call0formal@$tv0@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1)) $Option_Option_vec)) ($Integer 0)))))))) (=> $abort_flag@16 (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length call0formal@$tv0@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1)) $Option_Option_vec)) ($Integer 0))))))) (= $abort_code@26 (|i#$Integer| ($Integer 7)))))) (and (=> (not $abort_flag@16) (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length call0formal@$tv0@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call5formal@$ret0@0)) $Option_Option_vec)) ($Integer 0)))))))) (=> (not $abort_flag@16) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$borrow call0formal@$tv0@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call5formal@$ret0@0)) $Option_Option_vec) ($Integer 0)) inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2)))))) (=> (and (and (and (and ((_ is $Vector) call5formal@$ret0@0) (let ((va@@10 (|v#$Vector| call5formal@$ret0@0)))
903
904
(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))
905
)))))) (= (|l#$ValueArray| (|v#$Vector| call5formal@$ret0@0)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call5formal@$ret0@0)) $Option_Option_vec)) (let ((va@@11 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call5formal@$ret0@0)) $Option_Option_vec))))
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
(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))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call5formal@$ret0@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (and (=> (= (ControlFlow 0 307998) 308603) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon31_Then_correct) (=> (= (ControlFlow 0 307998) 308061) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon31_Else_correct)))))))))
(let ((inline$$ReadRef$1$anon0_correct  (=> (and (= inline$$ReadRef$1$v@1 (|v#$Mutation| inline$$BorrowField$2$dst@1)) (= (ControlFlow 0 307986) 307998)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Else$4_correct)))
(let ((inline$$Option_Option_$unpack_ref$1$anon0_correct  (=> (and (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_Option_$unpack_ref$1$$before@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (= (ControlFlow 0 307950) 307986)) inline$$ReadRef$1$anon0_correct)))
(let ((inline$$Option_Option_$unpack_ref$1$Entry_correct  (=> (= inline$$Option_Option_$unpack_ref$1$$tv0@0 $DiemAccount_KeyRotationCapability_type_value) (=> (and (= inline$$Option_Option_$unpack_ref$1$$before@0 (|v#$Mutation| inline$$BorrowField$2$dst@1)) (= (ControlFlow 0 307944) 307950)) inline$$Option_Option_$unpack_ref$1$anon0_correct))))
(let ((inline$$BorrowField$2$anon0_correct  (=> (= inline$$BorrowField$2$p@1 (|p#$Mutation| inline$$BorrowGlobal$2$dst@2)) (=> (and (and (= inline$$BorrowField$2$size@1 (|size#$Path| inline$$BorrowField$2$p@1)) (= inline$$BorrowField$2$p@2 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$2$p@1) inline$$BorrowField$2$size@1 $DiemAccount_DiemAccount_key_rotation_capability) (+ inline$$BorrowField$2$size@1 1)))) (and (= inline$$BorrowField$2$dst@1 ($Mutation (|l#$Mutation| inline$$BorrowGlobal$2$dst@2) inline$$BorrowField$2$p@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowGlobal$2$dst@2))) $DiemAccount_DiemAccount_key_rotation_capability))) (= (ControlFlow 0 307910) 307944))) inline$$Option_Option_$unpack_ref$1$Entry_correct))))
(let ((inline$$DiemAccount_DiemAccount_$unpack_ref$2$anon0_correct  (=> (and (and (and (and (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_DiemAccount_$unpack_ref$2$$before@0)) $DiemAccount_DiemAccount_withdraw_capability))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_DiemAccount_$unpack_ref$2$$before@0)) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) true) true) (= (ControlFlow 0 307788) 307910)) inline$$BorrowField$2$anon0_correct)))
(let ((inline$$DiemAccount_DiemAccount_$unpack_ref$2$Entry_correct  (=> (and (= inline$$DiemAccount_DiemAccount_$unpack_ref$2$$before@0 (|v#$Mutation| inline$$BorrowGlobal$2$dst@2)) (= (ControlFlow 0 307782) 307788)) inline$$DiemAccount_DiemAccount_$unpack_ref$2$anon0_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Else_correct  (=> (and (not $abort_flag@15) (= (ControlFlow 0 307792) 307782)) inline$$DiemAccount_DiemAccount_$unpack_ref$2$Entry_correct)))
(let ((inline$$BorrowGlobal$2$anon3_Then$1_correct  (=> (= $abort_code@25 $EXEC_FAILURE_CODE) (=> (and (= $abort_flag@15 true) (= inline$$BorrowGlobal$2$dst@2 inline$$BorrowGlobal$2$dst@0)) (and (=> (= (ControlFlow 0 307749) 308623) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Then_correct) (=> (= (ControlFlow 0 307749) 307792) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Else_correct))))))
(let ((inline$$BorrowGlobal$2$anon3_Then_correct  (=> (and (not (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory@1) $EmptyTypeValueArray inline$$BorrowGlobal$2$a@1)) (= (ControlFlow 0 307747) 307749)) inline$$BorrowGlobal$2$anon3_Then$1_correct)))
(let ((inline$$BorrowGlobal$2$anon3_Else_correct  (=> (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory@1) $EmptyTypeValueArray inline$$BorrowGlobal$2$a@1) (=> (and (and (= inline$$BorrowGlobal$2$dst@1 ($Mutation ($Global $EmptyTypeValueArray inline$$BorrowGlobal$2$a@1) $EmptyPath (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory@1) $EmptyTypeValueArray inline$$BorrowGlobal$2$a@1))) (= $abort_code@25 $abort_code@23)) (and (= $abort_flag@15 $abort_flag@14) (= inline$$BorrowGlobal$2$dst@2 inline$$BorrowGlobal$2$dst@1))) (and (=> (= (ControlFlow 0 307695) 308623) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Then_correct) (=> (= (ControlFlow 0 307695) 307792) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon29_Else_correct))))))
(let ((inline$$BorrowGlobal$2$anon0_correct  (=> (= inline$$BorrowGlobal$2$a@1 (|a#$Address| inline$$GetFieldFromValue$4$dst@1)) (and (=> (= (ControlFlow 0 307665) 307747) inline$$BorrowGlobal$2$anon3_Then_correct) (=> (= (ControlFlow 0 307665) 307695) inline$$BorrowGlobal$2$anon3_Else_correct)))))
(let ((inline$$BorrowGlobal$2$Entry_correct  (and (=> (= (ControlFlow 0 307659) (- 0 316206)) true) (=> (= (ControlFlow 0 307659) 307665) inline$$BorrowGlobal$2$anon0_correct))))
(let ((inline$$GetFieldFromValue$4$anon0_correct  (=> (and (= inline$$GetFieldFromValue$4$dst@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2)) $DiemAccount_KeyRotationCapability_account_address)) (= (ControlFlow 0 307552) 307659)) inline$$BorrowGlobal$2$Entry_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon27_Then_correct  (=> (and (|b#$Boolean| inline$$DiemAccount_exists_at_$def$3$$t2@1) (= (ControlFlow 0 307558) 307552)) inline$$GetFieldFromValue$4$anon0_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon12_correct  (=> (and (= $abort_code@27 $abort_code@24) (= (ControlFlow 0 307494) 307498)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon28_Else_correct  (=> (and (not true) (= (ControlFlow 0 307492) 307494)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon12_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon28_Then_correct  (=> (= (ControlFlow 0 307506) 307494) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon12_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon27_Else_correct  (=> (and (not (|b#$Boolean| inline$$DiemAccount_exists_at_$def$3$$t2@1)) (= $abort_code@24 (|i#$Integer| call3formal@$ret0@0))) (and (=> (= (ControlFlow 0 307486) 307506) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon28_Then_correct) (=> (= (ControlFlow 0 307486) 307492) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon28_Else_correct)))))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon25_Else_correct  (=> (not $abort_flag@14) (and (=> (= (ControlFlow 0 307474) 307558) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon27_Then_correct) (=> (= (ControlFlow 0 307474) 307486) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon27_Else_correct)))))
928
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon24_Else_correct  (=> (not $abort_flag@13) (=> (and (and (and (= inline$$DiemAccount_restore_key_rotation_capability_$def$0$$t7@1 ($Integer 0)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@14)) (and (=> $abort_flag@14 (|b#$Boolean| ($Boolean false))) (=> (not $abort_flag@14) (|b#$Boolean| ($Boolean ($IsEqual_stratified call3formal@$ret0@0 ($Integer 5))))))) (and (and ((_ is $Integer) call3formal@$ret0@0) (>= (|i#$Integer| call3formal@$ret0@0) 0)) (<= (|i#$Integer| call3formal@$ret0@0) $MAX_U64))) (and (=> (= (ControlFlow 0 307468) 308643) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon25_Then_correct) (=> (= (ControlFlow 0 307468) 307474) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon25_Else_correct))))))
929
930
931
932
933
934
935
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon24_Then_correct  (=> $abort_flag@13 (=> (and (= $abort_code@27 $abort_code@22) (= (ControlFlow 0 308663) 307498)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$Abort_correct))))
(let ((inline$$DiemAccount_exists_at_$def$3$anon6_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 307424) 308663) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon24_Then_correct) (=> (= (ControlFlow 0 307424) 307468) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon24_Else_correct)))))
(let ((inline$$DiemAccount_exists_at_$def$3$anon6_Then_correct  (and (=> (= (ControlFlow 0 307434) 308663) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon24_Then_correct) (=> (= (ControlFlow 0 307434) 307468) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon24_Else_correct))))
(let ((inline$$DiemAccount_exists_at_$def$3$anon2$1_correct  (=> (= inline$$DiemAccount_exists_at_$def$3$$t2@1 ($Boolean (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory@1) $EmptyTypeValueArray (|a#$Address| inline$$GetFieldFromValue$3$dst@1)))) (and (=> (= (ControlFlow 0 307418) 307434) inline$$DiemAccount_exists_at_$def$3$anon6_Then_correct) (=> (= (ControlFlow 0 307418) 307424) inline$$DiemAccount_exists_at_$def$3$anon6_Else_correct)))))
(let ((inline$$DiemAccount_exists_at_$def$3$anon5_Else_correct  (=> (and (not true) (= (ControlFlow 0 307372) 307418)) inline$$DiemAccount_exists_at_$def$3$anon2$1_correct)))
(let ((inline$$DiemAccount_exists_at_$def$3$anon5_Then_correct  (=> (= (ControlFlow 0 307442) 307418) inline$$DiemAccount_exists_at_$def$3$anon2$1_correct)))
(let ((inline$$DiemAccount_exists_at_$def$3$anon0_correct  (=> (not $abort_flag@13) (and (=> (= (ControlFlow 0 307366) 307442) inline$$DiemAccount_exists_at_$def$3$anon5_Then_correct) (=> (= (ControlFlow 0 307366) 307372) inline$$DiemAccount_exists_at_$def$3$anon5_Else_correct)))))
936
(let ((inline$$DiemAccount_exists_at$3$anon0_correct  (=> (and ((_ is $Address) inline$$GetFieldFromValue$3$dst@1) (= (ControlFlow 0 307448) 307366)) inline$$DiemAccount_exists_at_$def$3$anon0_correct)))
937
938
939
940
(let ((inline$$GetFieldFromValue$3$anon0_correct  (=> (and (= inline$$GetFieldFromValue$3$dst@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2)) $DiemAccount_KeyRotationCapability_account_address)) (= (ControlFlow 0 307208) 307448)) inline$$DiemAccount_exists_at$3$anon0_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon23_Else_correct  (=> (and (not true) (= (ControlFlow 0 307132) 307208)) inline$$GetFieldFromValue$3$anon0_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon23_Then_correct  (=> (= (ControlFlow 0 308671) 307208) inline$$GetFieldFromValue$3$anon0_correct)))
(let ((inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon0_correct  (=> (not $abort_flag@13) (and (=> (= (ControlFlow 0 307126) 308671) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon23_Then_correct) (=> (= (ControlFlow 0 307126) 307132) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon23_Else_correct)))))
941
(let ((inline$$DiemAccount_restore_key_rotation_capability_$direct_inter$0$anon0_correct  (=> (and (and (and (and (and ((_ is $Vector) inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2) (let ((va@@12 (|v#$Vector| inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2)))
942
943
(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))
944
)))))) (= (|l#$ValueArray| (|v#$Vector| inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2)) 1)) ((_ is $Address) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2)) $DiemAccount_KeyRotationCapability_account_address))) true) (= (ControlFlow 0 308675) 307126)) inline$$DiemAccount_restore_key_rotation_capability_$def$0$anon0_correct)))
945
946
(let ((inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon14_Else_correct  (=> (and (not $abort_flag@13) (= (ControlFlow 0 308681) 308675)) inline$$DiemAccount_restore_key_rotation_capability_$direct_inter$0$anon0_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon32$3_correct  (=> (= $abort_flag@13 $abort_flag@12) (=> (and (= $DiemAccount_DiemAccount_$memory@1 |inline$$WritebackToGlobal$1$m'@2|) (= $abort_code@22 $abort_code@19)) (and (=> (= (ControlFlow 0 306544) 308701) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon14_Then_correct) (=> (= (ControlFlow 0 306544) 308681) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon14_Else_correct))))))
947
948
(let ((inline$$WritebackToGlobal$1$anon3_Else_correct  (=> (not ((_ is $Global) inline$$WritebackToGlobal$1$l@1)) (=> (and (= |inline$$WritebackToGlobal$1$m'@2| $DiemAccount_DiemAccount_$memory@0) (= (ControlFlow 0 306482) 306544)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon32$3_correct))))
(let ((inline$$WritebackToGlobal$1$anon3_Then_correct  (=> ((_ is $Global) inline$$WritebackToGlobal$1$l@1) (=> (and (= inline$$WritebackToGlobal$1$ta@1 (|ts#$Global| inline$$WritebackToGlobal$1$l@1)) (= inline$$WritebackToGlobal$1$a@1 (|a#$Global| inline$$WritebackToGlobal$1$l@1))) (=> (and (and (= inline$$WritebackToGlobal$1$v@1 ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$1$dst'@2|) 0 (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory@0) inline$$WritebackToGlobal$1$ta@1 inline$$WritebackToGlobal$1$a@1) (|v#$Mutation| |inline$$WritebackToReference$1$dst'@2|))) (= |inline$$WritebackToGlobal$1$m'@1| ($Memory (|domain#$Memory| $DiemAccount_DiemAccount_$memory@0) (|Store_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory@0) inline$$WritebackToGlobal$1$ta@1 inline$$WritebackToGlobal$1$a@1 inline$$WritebackToGlobal$1$v@1)))) (and (= |inline$$WritebackToGlobal$1$m'@2| |inline$$WritebackToGlobal$1$m'@1|) (= (ControlFlow 0 306536) 306544))) inline$$DiemAccount_rotate_authentication_key_$def$0$anon32$3_correct)))))
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
(let ((inline$$WritebackToGlobal$1$anon0_correct  (=> (= inline$$WritebackToGlobal$1$l@1 (|l#$Mutation| |inline$$WritebackToReference$1$dst'@2|)) (and (=> (= (ControlFlow 0 306472) 306536) inline$$WritebackToGlobal$1$anon3_Then_correct) (=> (= (ControlFlow 0 306472) 306482) inline$$WritebackToGlobal$1$anon3_Else_correct)))))
(let ((inline$$DiemAccount_DiemAccount_$pack_ref$2$Entry_correct  (=> (and (= inline$$DiemAccount_DiemAccount_$pack_ref$2$$after@0 (|v#$Mutation| |inline$$WritebackToReference$1$dst'@2|)) (= (ControlFlow 0 306350) 306472)) inline$$WritebackToGlobal$1$anon0_correct)))
(let ((inline$$WritebackToReference$1$anon3_Else_correct  (=> (not (and (and (= (|l#$Mutation| inline$$BorrowGlobal$1$dst@2) (|l#$Mutation| |inline$$WriteRef$1$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$1$dstPath@1) (|size#$Path| inline$$WritebackToReference$1$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$1$dstPath@1 inline$$WritebackToReference$1$srcPath@1))) (=> (and (= |inline$$WritebackToReference$1$dst'@2| inline$$BorrowGlobal$1$dst@2) (= (ControlFlow 0 306271) 306350)) inline$$DiemAccount_DiemAccount_$pack_ref$2$Entry_correct))))
(let ((inline$$WritebackToReference$1$anon3_Then_correct  (=> (and (and (and (and (= (|l#$Mutation| inline$$BorrowGlobal$1$dst@2) (|l#$Mutation| |inline$$WriteRef$1$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$1$dstPath@1) (|size#$Path| inline$$WritebackToReference$1$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$1$dstPath@1 inline$$WritebackToReference$1$srcPath@1)) (= |inline$$WritebackToReference$1$dst'@1| ($Mutation (|l#$Mutation| inline$$BorrowGlobal$1$dst@2) inline$$WritebackToReference$1$dstPath@1 ($UpdateValue_stratified inline$$WritebackToReference$1$srcPath@1 (|size#$Path| inline$$WritebackToReference$1$dstPath@1) (|v#$Mutation| inline$$BorrowGlobal$1$dst@2) (|v#$Mutation| |inline$$WriteRef$1$to'@1|))))) (and (= |inline$$WritebackToReference$1$dst'@2| |inline$$WritebackToReference$1$dst'@1|) (= (ControlFlow 0 306327) 306350))) inline$$DiemAccount_DiemAccount_$pack_ref$2$Entry_correct)))
(let ((inline$$WritebackToReference$1$anon0_correct  (=> (and (= inline$$WritebackToReference$1$srcPath@1 (|p#$Mutation| |inline$$WriteRef$1$to'@1|)) (= inline$$WritebackToReference$1$dstPath@1 (|p#$Mutation| inline$$BorrowGlobal$1$dst@2))) (and (=> (= (ControlFlow 0 306235) 306327) inline$$WritebackToReference$1$anon3_Then_correct) (=> (= (ControlFlow 0 306235) 306271) inline$$WritebackToReference$1$anon3_Else_correct)))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon48_Else_correct  (=> (and (not true) (= (ControlFlow 0 306098) 306235)) inline$$WritebackToReference$1$anon0_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon48_Then_correct  (=> (and (= inline$$DiemAccount_rotate_authentication_key_$def$0$$trace_temp@1 (|v#$Mutation| inline$$BorrowGlobal$1$dst@2)) (= (ControlFlow 0 306554) 306235)) inline$$WritebackToReference$1$anon0_correct)))
(let ((inline$$WriteRef$1$anon0_correct  (=> (= |inline$$WriteRef$1$to'@1| ($Mutation (|l#$Mutation| inline$$BorrowField$1$dst@1) (|p#$Mutation| inline$$BorrowField$1$dst@1) new_key)) (and (=> (= (ControlFlow 0 306084) 306554) inline$$DiemAccount_rotate_authentication_key_$def$0$anon48_Then_correct) (=> (= (ControlFlow 0 306084) 306098) inline$$DiemAccount_rotate_authentication_key_$def$0$anon48_Else_correct)))))
(let ((inline$$BorrowField$1$anon0_correct  (=> (= inline$$BorrowField$1$p@1 (|p#$Mutation| inline$$BorrowGlobal$1$dst@2)) (=> (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 $DiemAccount_DiemAccount_authentication_key) (+ inline$$BorrowField$1$size@1 1)))) (and (= inline$$BorrowField$1$dst@1 ($Mutation (|l#$Mutation| inline$$BorrowGlobal$1$dst@2) inline$$BorrowField$1$p@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowGlobal$1$dst@2))) $DiemAccount_DiemAccount_authentication_key))) (= (ControlFlow 0 306025) 306084))) inline$$WriteRef$1$anon0_correct))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon46_Then_correct  (=> (and (|b#$Boolean| inline$$DiemAccount_rotate_authentication_key_$def$0$$t16@1) (= (ControlFlow 0 306031) 306025)) inline$$BorrowField$1$anon0_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$Abort_correct  (=> (= $abort_flag@13 true) (=> (and (= $DiemAccount_DiemAccount_$memory@1 $DiemAccount_DiemAccount_$memory@0) (= $abort_code@22 $abort_code@21)) (and (=> (= (ControlFlow 0 305471) 308701) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon14_Then_correct) (=> (= (ControlFlow 0 305471) 308681) inline$$rotate_authentication_key_rotate_authentication_key_$def_verify$0$anon14_Else_correct))))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon9_correct  (=> (and (= $abort_code@21 $abort_code@16) (= (ControlFlow 0 306626) 305471)) inline$$DiemAccount_rotate_authentication_key_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon37_Else_correct  (=> (and (not true) (= (ControlFlow 0 306624) 306626)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon9_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon37_Then_correct  (=> (= (ControlFlow 0 306634) 306626) inline$$DiemAccount_rotate_authentication_key_$def$0$anon9_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon36_Then_correct  (=> $abort_flag@10 (and (=> (= (ControlFlow 0 306618) 306634) inline$$DiemAccount_rotate_authentication_key_$def$0$anon37_Then_correct) (=> (= (ControlFlow 0 306618) 306624) inline$$DiemAccount_rotate_authentication_key_$def$0$anon37_Else_correct)))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon17_correct  (=> (and (= $abort_code@21 $abort_code@18) (= (ControlFlow 0 306606) 305471)) inline$$DiemAccount_rotate_authentication_key_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon41_Else_correct  (=> (and (not true) (= (ControlFlow 0 306604) 306606)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon17_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon41_Then_correct  (=> (= (ControlFlow 0 306614) 306606) inline$$DiemAccount_rotate_authentication_key_$def$0$anon17_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon40_Then_correct  (=> $abort_flag@11 (and (=> (= (ControlFlow 0 306598) 306614) inline$$DiemAccount_rotate_authentication_key_$def$0$anon41_Then_correct) (=> (= (ControlFlow 0 306598) 306604) inline$$DiemAccount_rotate_authentication_key_$def$0$anon41_Else_correct)))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon21_correct  (=> (and (= $abort_code@21 $abort_code@18) (= (ControlFlow 0 306586) 305471)) inline$$DiemAccount_rotate_authentication_key_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon43_Else_correct  (=> (and (not true) (= (ControlFlow 0 306584) 306586)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon21_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon43_Then_correct  (=> (= (ControlFlow 0 306594) 306586) inline$$DiemAccount_rotate_authentication_key_$def$0$anon21_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon42_Then_correct  (=> $abort_flag@11 (and (=> (= (ControlFlow 0 306578) 306594) inline$$DiemAccount_rotate_authentication_key_$def$0$anon43_Then_correct) (=> (= (ControlFlow 0 306578) 306584) inline$$DiemAccount_rotate_authentication_key_$def$0$anon43_Else_correct)))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon25_correct  (=> (and (= $abort_code@21 $abort_code@19) (= (ControlFlow 0 306566) 305471)) inline$$DiemAccount_rotate_authentication_key_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon45_Else_correct  (=> (and (not true) (= (ControlFlow 0 306564) 306566)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon25_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon45_Then_correct  (=> (= (ControlFlow 0 306574) 306566) inline$$DiemAccount_rotate_authentication_key_$def$0$anon25_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon44_Then_correct  (=> $abort_flag@12 (and (=> (= (ControlFlow 0 306558) 306574) inline$$DiemAccount_rotate_authentication_key_$def$0$anon45_Then_correct) (=> (= (ControlFlow 0 306558) 306564) inline$$DiemAccount_rotate_authentication_key_$def$0$anon45_Else_correct)))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon30_correct  (=> (and (= $abort_code@21 $abort_code@20) (= (ControlFlow 0 305895) 305471)) inline$$DiemAccount_rotate_authentication_key_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon47_Else_correct  (=> (and (not true) (= (ControlFlow 0 305893) 305895)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon30_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon47_Then_correct  (=> (= (ControlFlow 0 305903) 305895) inline$$DiemAccount_rotate_authentication_key_$def$0$anon30_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon46_Else$1_correct  (=> (= $abort_code@20 (|i#$Integer| call3formal@$ret0@0@@0)) (and (=> (= (ControlFlow 0 305887) 305903) inline$$DiemAccount_rotate_authentication_key_$def$0$anon47_Then_correct) (=> (= (ControlFlow 0 305887) 305893) inline$$DiemAccount_rotate_authentication_key_$def$0$anon47_Else_correct)))))
(let ((inline$$DiemAccount_DiemAccount_$pack_ref$1$Entry_correct  (=> (and (= inline$$DiemAccount_DiemAccount_$pack_ref$1$$after@0 (|v#$Mutation| inline$$BorrowGlobal$1$dst@2)) (= (ControlFlow 0 305875) 305887)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon46_Else$1_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon46_Else_correct  (=> (and (not (|b#$Boolean| inline$$DiemAccount_rotate_authentication_key_$def$0$$t16@1)) (= (ControlFlow 0 305881) 305875)) inline$$DiemAccount_DiemAccount_$pack_ref$1$Entry_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon44_Else_correct  (=> (not $abort_flag@12) (and (=> (= (ControlFlow 0 305852) 306031) inline$$DiemAccount_rotate_authentication_key_$def$0$anon46_Then_correct) (=> (= (ControlFlow 0 305852) 305881) inline$$DiemAccount_rotate_authentication_key_$def$0$anon46_Else_correct)))))
983
984
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon42_Else_correct  (=> (not $abort_flag@11) (=> (and (= inline$$DiemAccount_rotate_authentication_key_$def$0$$t15@1 ($Integer 32)) (= inline$$DiemAccount_rotate_authentication_key_$def$0$$t16@1 ($Boolean ($IsEqual_stratified inline$$Vector_length$0$l@1 inline$$DiemAccount_rotate_authentication_key_$def$0$$t15@1)))) (=> (and (and (and (= inline$$DiemAccount_rotate_authentication_key_$def$0$$t17@1 ($Integer 8)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@12)) (and (=> $abort_flag@12 (|b#$Boolean| ($Boolean false))) (=> (not $abort_flag@12) (|b#$Boolean| ($Boolean ($IsEqual_stratified call3formal@$ret0@0@@0 ($Integer 7))))))) (and (and ((_ is $Integer) call3formal@$ret0@0@@0) (>= (|i#$Integer| call3formal@$ret0@0@@0) 0)) (<= (|i#$Integer| call3formal@$ret0@0@@0) $MAX_U64))) (and (=> (= (ControlFlow 0 305846) 306558) inline$$DiemAccount_rotate_authentication_key_$def$0$anon44_Then_correct) (=> (= (ControlFlow 0 305846) 305852) inline$$DiemAccount_rotate_authentication_key_$def$0$anon44_Else_correct)))))))
(let ((inline$$Vector_length$0$anon0_correct  (=> (and ((_ is $Vector) new_key) (= inline$$Vector_length$0$l@1 ($Integer (|l#$ValueArray| (|v#$Vector| new_key))))) (and (=> (= (ControlFlow 0 305816) 306578) inline$$DiemAccount_rotate_authentication_key_$def$0$anon42_Then_correct) (=> (= (ControlFlow 0 305816) 305846) inline$$DiemAccount_rotate_authentication_key_$def$0$anon42_Else_correct)))))
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(let ((inline$$Vector_length$0$Entry_correct  (=> (and (= inline$$Vector_length$0$ta@0 $IntegerType) (= (ControlFlow 0 305804) 305816)) inline$$Vector_length$0$anon0_correct)))
(let ((inline$$DiemAccount_DiemAccount_$unpack_ref$1$anon0_correct  (=> (and (and (and (and (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_DiemAccount_$unpack_ref$1$$before@0)) $DiemAccount_DiemAccount_withdraw_capability))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_DiemAccount_$unpack_ref$1$$before@0)) $DiemAccount_DiemAccount_key_rotation_capability))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) true) true) (= (ControlFlow 0 305761) 305804)) inline$$Vector_length$0$Entry_correct)))
(let ((inline$$DiemAccount_DiemAccount_$unpack_ref$1$Entry_correct  (=> (and (= inline$$DiemAccount_DiemAccount_$unpack_ref$1$$before@0 (|v#$Mutation| inline$$BorrowGlobal$1$dst@2)) (= (ControlFlow 0 305755) 305761)) inline$$DiemAccount_DiemAccount_$unpack_ref$1$anon0_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon40_Else_correct  (=> (and (not $abort_flag@11) (= (ControlFlow 0 305765) 305755)) inline$$DiemAccount_DiemAccount_$unpack_ref$1$Entry_correct)))
(let ((inline$$BorrowGlobal$1$anon3_Then$1_correct  (=> (= $abort_code@18 $EXEC_FAILURE_CODE) (=> (and (= $abort_flag@11 true) (= inline$$BorrowGlobal$1$dst@2 inline$$BorrowGlobal$1$dst@0)) (and (=> (= (ControlFlow 0 305722) 306598) inline$$DiemAccount_rotate_authentication_key_$def$0$anon40_Then_correct) (=> (= (ControlFlow 0 305722) 305765) inline$$DiemAccount_rotate_authentication_key_$def$0$anon40_Else_correct))))))
(let ((inline$$BorrowGlobal$1$anon3_Then_correct  (=> (and (not (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory@0) $EmptyTypeValueArray inline$$BorrowGlobal$1$a@1)) (= (ControlFlow 0 305720) 305722)) inline$$BorrowGlobal$1$anon3_Then$1_correct)))
(let ((inline$$BorrowGlobal$1$anon3_Else_correct  (=> (|Select_[$TypeValueArray,$int]$bool| (|domain#$Memory| $DiemAccount_DiemAccount_$memory@0) $EmptyTypeValueArray inline$$BorrowGlobal$1$a@1) (=> (and (and (= inline$$BorrowGlobal$1$dst@1 ($Mutation ($Global $EmptyTypeValueArray inline$$BorrowGlobal$1$a@1) $EmptyPath (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $DiemAccount_DiemAccount_$memory@0) $EmptyTypeValueArray inline$$BorrowGlobal$1$a@1))) (= $abort_code@18 $abort_code@16)) (and (= $abort_flag@11 $abort_flag@10) (= inline$$BorrowGlobal$1$dst@2 inline$$BorrowGlobal$1$dst@1))) (and (=> (= (ControlFlow 0 305668) 306598) inline$$DiemAccount_rotate_authentication_key_$def$0$anon40_Then_correct) (=> (= (ControlFlow 0 305668) 305765) inline$$DiemAccount_rotate_authentication_key_$def$0$anon40_Else_correct))))))
(let ((inline$$BorrowGlobal$1$anon0_correct  (=> (= inline$$BorrowGlobal$1$a@1 (|a#$Address| inline$$GetFieldFromValue$2$dst@1)) (and (=> (= (ControlFlow 0 305638) 305720) inline$$BorrowGlobal$1$anon3_Then_correct) (=> (= (ControlFlow 0 305638) 305668) inline$$BorrowGlobal$1$anon3_Else_correct)))))
(let ((inline$$BorrowGlobal$1$Entry_correct  (and (=> (= (ControlFlow 0 305632) (- 0 315185)) true) (=> (= (ControlFlow 0 305632) 305638) inline$$BorrowGlobal$1$anon0_correct))))
(let ((inline$$GetFieldFromValue$2$anon0_correct  (=> (and (= inline$$GetFieldFromValue$2$dst@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$DiemAccount_extract_key_rotation_capability_$def$0$$ret0@2)) $DiemAccount_KeyRotationCapability_account_address)) (= (ControlFlow 0 305525) 305632)) inline$$BorrowGlobal$1$Entry_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon38_Then_correct  (=> (and (|b#$Boolean| inline$$DiemAccount_exists_at_$def$2$$t2@1) (= (ControlFlow 0 305531) 305525)) inline$$GetFieldFromValue$2$anon0_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon14_correct  (=> (and (= $abort_code@21 $abort_code@17) (= (ControlFlow 0 305467) 305471)) inline$$DiemAccount_rotate_authentication_key_$def$0$Abort_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon39_Else_correct  (=> (and (not true) (= (ControlFlow 0 305465) 305467)) inline$$DiemAccount_rotate_authentication_key_$def$0$anon14_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon39_Then_correct  (=> (= (ControlFlow 0 305479) 305467) inline$$DiemAccount_rotate_authentication_key_$def$0$anon14_correct)))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon38_Else_correct  (=> (and (not (|b#$Boolean| inline$$DiemAccount_exists_at_$def$2$$t2@1)) (= $abort_code@17 (|i#$Integer| call3formal@$ret0@0@@1))) (and (=> (= (ControlFlow 0 305459) 305479) inline$$DiemAccount_rotate_authentication_key_$def$0$anon39_Then_correct) (=> (= (ControlFlow 0 305459) 305465) inline$$DiemAccount_rotate_authentication_key_$def$0$anon39_Else_correct)))))
(let ((inline$$DiemAccount_rotate_authentication_key_$def$0$anon36_Else_correct  (=> (not $abort_flag@10) (and (=> (= (ControlFlow 0 305447) 305531) inline$$DiemAccount_rotate_authentication_key_$def$0$anon38_Then_correct) (=> (= (ControlFlow 0 305447) 305459) inline$$DiemAccount_rotate_authentication_key_$def$0$anon38_Else_correct)))))
For faster browsing, not all history is shown. View entire blame