Debug.smt2 256 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
(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 $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 $Option_Option_vec () Int)
(declare-fun $Option_Option_type_value (T@$TypeValue) T@$TypeValue)
(declare-fun $Option_Option () T@$TypeName)
(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 |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 (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))
116
(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))
117
)))
118
(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))
119
)))
120
(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))
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
)))
(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))
)))
178
(assert (forall ((v1@@2 T@$Value) (v2@@2 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@2) (let ((va (|v#$Vector| v1@@2)))
179
180
(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))
181
)))))) (and ((_ is $Vector) v2@@2) (let ((va@@0 (|v#$Vector| v2@@2)))
182
183
184
(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)))))
185
(assert (forall ((v1@@3 T@$Value) (v2@@3 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@3) (let ((va@@1 (|v#$Vector| v1@@3)))
186
187
(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))
188
)))))) (and ((_ is $Vector) v2@@3) (let ((va@@2 (|v#$Vector| v2@@3)))
189
190
191
(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))))
192
(assert (forall ((v1@@4 T@$Value) (v2@@4 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@4) (let ((va@@3 (|v#$Vector| v1@@4)))
193
194
(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))
195
)))))) (and ((_ is $Vector) v2@@4) (let ((va@@4 (|v#$Vector| v2@@4)))
196
197
198
(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)))))
199
(assert (forall ((v1@@5 T@$Value) (v2@@5 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@5) (let ((va@@5 (|v#$Vector| v1@@5)))
200
201
(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))
202
)))))) (and ((_ is $Vector) v2@@5) (let ((va@@6 (|v#$Vector| v2@@5)))
203
204
205
(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))))
206
207
(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))))
208
209
210
(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)))
211
 (and (and (and ((_ is $Vector) r) (let ((va@@7 (|v#$Vector| r)))
212
213
(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))
214
)))))) (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))
215
216
))) (> (|l#$ValueArray| (|v#$Vector| r)) 0)))))
(assert (forall ((v@@13 T@$Value) ) (let ((r@@0 ($BCS_serialize_core v@@13)))
217
 (=> ((_ is $Address) v@@13) (= (|l#$ValueArray| (|v#$Vector| r@@0)) $serialized_address_len)))))
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
(assert (= $Option_Option_vec 0))
(assert (forall (($tv0 T@$TypeValue) ) (! (= ($Option_Option_type_value $tv0) ($StructType $Option_Option ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $tv0) 1))) :pattern ( ($Option_Option_type_value $tv0))
)))
(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 $tv0@@0 () T@$TypeValue)
(declare-fun t () T@$Value)
(declare-fun $abort_flag@3 () Bool)
(declare-fun $abort_code@6 () Int)
(declare-fun inline$$Option_borrow_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun $abort_code@4 () Int)
(declare-fun inline$$Vector_borrow$0$dst@2 () T@$Value)
(declare-fun $abort_flag@2 () Bool)
(declare-fun inline$$Option_borrow_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun $abort_code@5 () Int)
(declare-fun $abort_code@1 () Int)
(declare-fun $abort_flag@0 () Bool)
(declare-fun $abort_code@2 () Int)
(declare-fun $abort_flag@1 () Bool)
(declare-fun inline$$Vector_borrow$0$dst@0 () T@$Value)
(declare-fun inline$$Vector_borrow$0$i_ind@1 () Int)
(declare-fun inline$$GetFieldFromValue$0$dst@1 () T@$Value)
(declare-fun inline$$Vector_borrow$0$dst@1 () T@$Value)
(declare-fun inline$$Option_borrow_$def_verify$0$$t8@1 () T@$Value)
(declare-fun call4formal@$ret0@0 () T@$Value)
(declare-fun $abort_code@3 () Int)
(declare-fun call3formal@$ret0@0 () T@$Value)
(declare-fun inline$$Option_borrow_$def_verify$0$$t5@1 () T@$Value)
(declare-fun |Select_[$TypeValueArray,$int]$Value| (|T@[$TypeValueArray,Int]$Value| T@$TypeValueArray Int) T@$Value)
(declare-fun $Option_Option_$memory () T@$Memory)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 47732) (let ((anon0$2_correct  (and (=> (= (ControlFlow 0 27643) (- 0 48557)) (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3)) (=> (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3) (and (=> (= (ControlFlow 0 27643) (- 0 48568)) (=> $abort_flag@3 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) ($Integer 0)))))) (=> (=> $abort_flag@3 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) ($Integer 0))))) (and (=> (= (ControlFlow 0 27643) (- 0 48579)) (=> $abort_flag@3 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6 (|i#$Integer| ($Integer 7)))))) (=> (=> $abort_flag@3 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6 (|i#$Integer| ($Integer 7))))) (=> (= (ControlFlow 0 27643) (- 0 48601)) (=> (not $abort_flag@3) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_borrow_$def_verify$0$$ret0@2 ($Vector_$borrow $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec) ($Integer 0)))))))))))))))
(let ((inline$$Option_borrow_$def_verify$0$anon20_correct  (=> (and (and (= $abort_code@6 $abort_code@4) (= inline$$Option_borrow_$def_verify$0$$ret0@2 inline$$Vector_borrow$0$dst@2)) (and (= $abort_flag@3 $abort_flag@2) (= (ControlFlow 0 27559) 27643))) anon0$2_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon30_Else_correct  (=> (and (not true) (= (ControlFlow 0 27557) 27559)) inline$$Option_borrow_$def_verify$0$anon20_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon30_Then_correct  (=> (= (ControlFlow 0 27567) 27559) inline$$Option_borrow_$def_verify$0$anon20_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon28_Else_correct  (=> (not $abort_flag@2) (and (=> (= (ControlFlow 0 27551) 27567) inline$$Option_borrow_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 27551) 27557) inline$$Option_borrow_$def_verify$0$anon30_Else_correct)))))
(let ((inline$$Option_borrow_$def_verify$0$Abort_correct  (=> (= inline$$Option_borrow_$def_verify$0$$ret0@1 $Error) (=> (and (and (= $abort_code@6 $abort_code@5) (= inline$$Option_borrow_$def_verify$0$$ret0@2 inline$$Option_borrow_$def_verify$0$$ret0@1)) (and (= $abort_flag@3 true) (= (ControlFlow 0 27261) 27643))) anon0$2_correct))))
(let ((inline$$Option_borrow_$def_verify$0$anon5_correct  (=> (and (= $abort_code@5 $abort_code@1) (= (ControlFlow 0 27619) 27261)) inline$$Option_borrow_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon23_Else_correct  (=> (and (not true) (= (ControlFlow 0 27617) 27619)) inline$$Option_borrow_$def_verify$0$anon5_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon23_Then_correct  (=> (= (ControlFlow 0 27627) 27619) inline$$Option_borrow_$def_verify$0$anon5_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon22_Then_correct  (=> $abort_flag@0 (and (=> (= (ControlFlow 0 27611) 27627) inline$$Option_borrow_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 27611) 27617) inline$$Option_borrow_$def_verify$0$anon23_Else_correct)))))
(let ((inline$$Option_borrow_$def_verify$0$anon9_correct  (=> (and (= $abort_code@5 $abort_code@2) (= (ControlFlow 0 27599) 27261)) inline$$Option_borrow_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon25_Else_correct  (=> (and (not true) (= (ControlFlow 0 27597) 27599)) inline$$Option_borrow_$def_verify$0$anon9_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon25_Then_correct  (=> (= (ControlFlow 0 27607) 27599) inline$$Option_borrow_$def_verify$0$anon9_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon24_Then_correct  (=> $abort_flag@1 (and (=> (= (ControlFlow 0 27591) 27607) inline$$Option_borrow_$def_verify$0$anon25_Then_correct) (=> (= (ControlFlow 0 27591) 27597) inline$$Option_borrow_$def_verify$0$anon25_Else_correct)))))
(let ((inline$$Option_borrow_$def_verify$0$anon17_correct  (=> (and (= $abort_code@5 $abort_code@4) (= (ControlFlow 0 27579) 27261)) inline$$Option_borrow_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon29_Else_correct  (=> (and (not true) (= (ControlFlow 0 27577) 27579)) inline$$Option_borrow_$def_verify$0$anon17_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon29_Then_correct  (=> (= (ControlFlow 0 27587) 27579) inline$$Option_borrow_$def_verify$0$anon17_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon28_Then_correct  (=> $abort_flag@2 (and (=> (= (ControlFlow 0 27571) 27587) inline$$Option_borrow_$def_verify$0$anon29_Then_correct) (=> (= (ControlFlow 0 27571) 27577) inline$$Option_borrow_$def_verify$0$anon29_Else_correct)))))
(let ((inline$$Vector_borrow$0$anon3_Then$1_correct  (=> (= $abort_flag@2 true) (=> (and (= $abort_code@4 $EXEC_FAILURE_CODE) (= inline$$Vector_borrow$0$dst@2 inline$$Vector_borrow$0$dst@0)) (and (=> (= (ControlFlow 0 27535) 27571) inline$$Option_borrow_$def_verify$0$anon28_Then_correct) (=> (= (ControlFlow 0 27535) 27551) inline$$Option_borrow_$def_verify$0$anon28_Else_correct))))))
(let ((inline$$Vector_borrow$0$anon3_Then_correct  (=> (and (or (< inline$$Vector_borrow$0$i_ind@1 0) (>= inline$$Vector_borrow$0$i_ind@1 (|l#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1)))) (= (ControlFlow 0 27533) 27535)) inline$$Vector_borrow$0$anon3_Then$1_correct)))
(let ((inline$$Vector_borrow$0$anon3_Else_correct  (=> (not (or (< inline$$Vector_borrow$0$i_ind@1 0) (>= inline$$Vector_borrow$0$i_ind@1 (|l#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1))))) (=> (and (and (= inline$$Vector_borrow$0$dst@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1)) inline$$Vector_borrow$0$i_ind@1)) (= $abort_flag@2 $abort_flag@1)) (and (= $abort_code@4 $abort_code@2) (= inline$$Vector_borrow$0$dst@2 inline$$Vector_borrow$0$dst@1))) (and (=> (= (ControlFlow 0 27475) 27571) inline$$Option_borrow_$def_verify$0$anon28_Then_correct) (=> (= (ControlFlow 0 27475) 27551) inline$$Option_borrow_$def_verify$0$anon28_Else_correct))))))
282
(let ((inline$$Vector_borrow$0$anon0_correct  (=> ((_ is $Vector) inline$$GetFieldFromValue$0$dst@1) (=> (and ((_ is $Integer) inline$$Option_borrow_$def_verify$0$$t8@1) (= inline$$Vector_borrow$0$i_ind@1 (|i#$Integer| inline$$Option_borrow_$def_verify$0$$t8@1))) (and (=> (= (ControlFlow 0 27449) 27533) inline$$Vector_borrow$0$anon3_Then_correct) (=> (= (ControlFlow 0 27449) 27475) inline$$Vector_borrow$0$anon3_Else_correct))))))
283
284
285
286
287
288
289
290
(let ((inline$$Option_borrow_$def_verify$0$anon26_Then$1_correct  (=> (and (= inline$$Option_borrow_$def_verify$0$$t8@1 ($Integer 0)) (= (ControlFlow 0 27541) 27449)) inline$$Vector_borrow$0$anon0_correct)))
(let ((inline$$GetFieldFromValue$0$anon0_correct  (=> (and (= inline$$GetFieldFromValue$0$dst@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) (= (ControlFlow 0 27315) 27541)) inline$$Option_borrow_$def_verify$0$anon26_Then$1_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon26_Then_correct  (=> (and (|b#$Boolean| call4formal@$ret0@0) (= (ControlFlow 0 27321) 27315)) inline$$GetFieldFromValue$0$anon0_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon14_correct  (=> (and (= $abort_code@5 $abort_code@3) (= (ControlFlow 0 27255) 27261)) inline$$Option_borrow_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon27_Else_correct  (=> (and (not true) (= (ControlFlow 0 27253) 27255)) inline$$Option_borrow_$def_verify$0$anon14_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon27_Then_correct  (=> (= (ControlFlow 0 27269) 27255) inline$$Option_borrow_$def_verify$0$anon14_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon26_Else_correct  (=> (and (not (|b#$Boolean| call4formal@$ret0@0)) (= $abort_code@3 (|i#$Integer| call3formal@$ret0@0))) (and (=> (= (ControlFlow 0 27247) 27269) inline$$Option_borrow_$def_verify$0$anon27_Then_correct) (=> (= (ControlFlow 0 27247) 27253) inline$$Option_borrow_$def_verify$0$anon27_Else_correct)))))
(let ((inline$$Option_borrow_$def_verify$0$anon24_Else_correct  (=> (not $abort_flag@1) (and (=> (= (ControlFlow 0 27235) 27321) inline$$Option_borrow_$def_verify$0$anon26_Then_correct) (=> (= (ControlFlow 0 27235) 27247) inline$$Option_borrow_$def_verify$0$anon26_Else_correct)))))
291
292
(let ((inline$$Option_borrow_$def_verify$0$anon22_Else_correct  (=> (not $abort_flag@0) (=> (and (and (and (= inline$$Option_borrow_$def_verify$0$$t5@1 ($Integer 1)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@1)) (and (=> $abort_flag@1 (|b#$Boolean| ($Boolean false))) (=> (not $abort_flag@1) (|b#$Boolean| ($Boolean ($IsEqual_stratified call3formal@$ret0@0 ($Integer 7))))))) (and (and ((_ is $Integer) call3formal@$ret0@0) (>= (|i#$Integer| call3formal@$ret0@0) 0)) (<= (|i#$Integer| call3formal@$ret0@0) $MAX_U64))) (and (=> (= (ControlFlow 0 27229) 27591) inline$$Option_borrow_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 27229) 27235) inline$$Option_borrow_$def_verify$0$anon24_Else_correct))))))
(let ((inline$$Option_borrow_$def_verify$0$anon2$1_correct  (=> (and (and (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0) (=> $abort_flag@0 (|b#$Boolean| ($Boolean false)))) (and (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified call4formal@$ret0@0 ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) ($Integer 0)))))))))) ((_ is $Boolean) call4formal@$ret0@0))) (and (=> (= (ControlFlow 0 27219) 27611) inline$$Option_borrow_$def_verify$0$anon22_Then_correct) (=> (= (ControlFlow 0 27219) 27229) inline$$Option_borrow_$def_verify$0$anon22_Else_correct)))))
293
294
295
(let ((inline$$Option_borrow_$def_verify$0$anon21_Else_correct  (=> (and (not true) (= (ControlFlow 0 27183) 27219)) inline$$Option_borrow_$def_verify$0$anon2$1_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon21_Then_correct  (=> (= (ControlFlow 0 27635) 27219) inline$$Option_borrow_$def_verify$0$anon2$1_correct)))
(let ((inline$$Option_borrow_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 27177) 27635) inline$$Option_borrow_$def_verify$0$anon21_Then_correct) (=> (= (ControlFlow 0 27177) 27183) inline$$Option_borrow_$def_verify$0$anon21_Else_correct)))))
296
(let ((anon0$1_correct  (=> (and (forall (($inv_addr Int) ($inv_tv0 T@$TypeValue) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0) 1) $inv_addr)) (let ((va@@8 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0) 1) $inv_addr))))
297
298
(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))
299
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0) 1) $inv_addr))) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0) 1) $inv_addr))) $Option_Option_vec)) (let ((va@@9 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0) 1) $inv_addr))) $Option_Option_vec))))
300
301
302
303
(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))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0) 1) $inv_addr))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0) 1) $inv_addr))
)) (= (ControlFlow 0 27641) 27177)) inline$$Option_borrow_$def_verify$0$anon0_correct)))
304
(let ((anon0_correct  (=> (and (and (and (and (and ((_ is $Vector) t) (let ((va@@10 (|v#$Vector| t)))
305
306
(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))
307
)))))) (= (|l#$ValueArray| (|v#$Vector| t)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec)) (let ((va@@11 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t)) $Option_Option_vec))))
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
359
360
361
362
363
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
(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| t)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 26774) 27641)) anon0$1_correct)))
(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 47732) 26774) anon0_correct)))
PreconditionGeneratedEntry_correct)))))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $tv0@@1 () T@$TypeValue)
(declare-fun t@@0 () T@$Value)
(declare-fun $abort_flag@3@@0 () Bool)
(declare-fun $abort_code@6@@0 () Int)
(declare-fun inline$$Option_borrow_mut_$def_verify$0$$ret0@1 () T@$Mutation)
(declare-fun inline$$Option_borrow_mut_$def_verify$0$$ret1@2 () T@$Value)
(declare-fun |inline$$Splice1$0$dst'@1| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@2| () T@$Value)
(declare-fun $abort_code@4@@0 () Int)
(declare-fun $abort_flag@2@@0 () Bool)
(declare-fun inline$$Option_borrow_mut_$def_verify$0$$trace_temp@1 () T@$Value)
(declare-fun |inline$$WritebackToReference$0$dst'@2| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1| () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1| () T@$Mutation)
(declare-fun inline$$Vector_borrow_mut$0$dst@2 () T@$Mutation)
(declare-fun inline$$BorrowField$0$dst@1 () T@$Mutation)
(declare-fun |inline$$Vector_borrow_mut$0$v'@1| () T@$Value)
(declare-fun inline$$Option_borrow_mut_$def_verify$0$$ret1@1 () T@$Value)
(declare-fun $DefaultMutation () T@$Mutation)
(declare-fun $abort_code@5@@0 () Int)
(declare-fun $abort_code@1@@0 () Int)
(declare-fun $abort_flag@0@@0 () Bool)
(declare-fun $abort_code@2@@0 () Int)
(declare-fun $abort_flag@1@@0 () Bool)
(declare-fun inline$$Vector_borrow_mut$0$dst@0 () T@$Mutation)
(declare-fun |inline$$Vector_borrow_mut$0$v'@0| () T@$Value)
(declare-fun inline$$Vector_borrow_mut$0$i_ind@1 () Int)
(declare-fun inline$$ReadRef$1$v@1 () T@$Value)
(declare-fun inline$$Vector_borrow_mut$0$dst@1 () T@$Mutation)
(declare-fun inline$$Option_borrow_mut_$def_verify$0$$t10@1 () T@$Value)
(declare-fun inline$$BorrowField$0$p@1 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1 () Int)
(declare-fun inline$$BorrowField$0$p@2 () T@$Path)
(declare-fun call4formal@$ret0@0@@0 () T@$Value)
(declare-fun $abort_code@3@@0 () Int)
(declare-fun call3formal@$ret0@0@@0 () T@$Value)
(declare-fun inline$$Option_borrow_mut_$def_verify$0$$t7@1 () T@$Value)
(declare-fun inline$$ReadRef$0$v@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 48634) (let ((anon0$2_correct@@0  (and (=> (= (ControlFlow 0 29504) (- 0 49966)) (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3@@0)) (=> (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3@@0) (and (=> (= (ControlFlow 0 29504) (- 0 49977)) (=> $abort_flag@3@@0 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec)) ($Integer 0)))))) (=> (=> $abort_flag@3@@0 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec)) ($Integer 0))))) (and (=> (= (ControlFlow 0 29504) (- 0 49988)) (=> $abort_flag@3@@0 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6@@0 (|i#$Integer| ($Integer 7)))))) (=> (=> $abort_flag@3@@0 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6@@0 (|i#$Integer| ($Integer 7))))) (=> (= (ControlFlow 0 29504) (- 0 50010)) (=> (not $abort_flag@3@@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified (|v#$Mutation| inline$$Option_borrow_mut_$def_verify$0$$ret0@1) ($Vector_$borrow $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_borrow_mut_$def_verify$0$$ret1@2)) $Option_Option_vec) ($Integer 0)))))))))))))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon22_correct  (=> (= inline$$Option_borrow_mut_$def_verify$0$$ret0@1 |inline$$Splice1$0$dst'@1|) (=> (and (and (= inline$$Option_borrow_mut_$def_verify$0$$ret1@2 |inline$$WritebackToValue$0$vdst'@2|) (= $abort_code@6@@0 $abort_code@4@@0)) (and (= $abort_flag@3@@0 $abort_flag@2@@0) (= (ControlFlow 0 29408) 29504))) anon0$2_correct@@0))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon33_Else_correct  (=> (and (not true) (= (ControlFlow 0 29406) 29408)) inline$$Option_borrow_mut_$def_verify$0$anon22_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon33_Then_correct  (=> (= (ControlFlow 0 29416) 29408) inline$$Option_borrow_mut_$def_verify$0$anon22_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon32_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 29396) 29416) inline$$Option_borrow_mut_$def_verify$0$anon33_Then_correct) (=> (= (ControlFlow 0 29396) 29406) inline$$Option_borrow_mut_$def_verify$0$anon33_Else_correct)))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon32_Then_correct  (=> (= inline$$Option_borrow_mut_$def_verify$0$$trace_temp@1 (|v#$Mutation| |inline$$Splice1$0$dst'@1|)) (and (=> (= (ControlFlow 0 29426) 29416) inline$$Option_borrow_mut_$def_verify$0$anon33_Then_correct) (=> (= (ControlFlow 0 29426) 29406) inline$$Option_borrow_mut_$def_verify$0$anon33_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Else_correct  (=> (and (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2|) ($Local 3))) (= |inline$$WritebackToValue$0$vdst'@2| t@@0)) (and (=> (= (ControlFlow 0 29354) 29426) inline$$Option_borrow_mut_$def_verify$0$anon32_Then_correct) (=> (= (ControlFlow 0 29354) 29396) inline$$Option_borrow_mut_$def_verify$0$anon32_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct  (=> (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2|) ($Local 3)) (=> (and (= |inline$$WritebackToValue$0$vdst'@1| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2|) 0 t@@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2|))) (= |inline$$WritebackToValue$0$vdst'@2| |inline$$WritebackToValue$0$vdst'@1|)) (and (=> (= (ControlFlow 0 29380) 29426) inline$$Option_borrow_mut_$def_verify$0$anon32_Then_correct) (=> (= (ControlFlow 0 29380) 29396) inline$$Option_borrow_mut_$def_verify$0$anon32_Else_correct))))))
(let ((inline$$WritebackToReference$0$anon3_Else_correct  (=> (and (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1) (|size#$Path| inline$$WritebackToReference$0$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1 inline$$WritebackToReference$0$srcPath@1))) (= |inline$$WritebackToReference$0$dst'@2| inline$$BorrowLoc$0$dst@1)) (and (=> (= (ControlFlow 0 29199) 29380) inline$$WritebackToValue$0$anon3_Then_correct) (=> (= (ControlFlow 0 29199) 29354) inline$$WritebackToValue$0$anon3_Else_correct)))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct  (=> (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1) (|l#$Mutation| |inline$$WriteRef$0$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1) (|size#$Path| inline$$WritebackToReference$0$srcPath@1))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1 inline$$WritebackToReference$0$srcPath@1)) (and (= |inline$$WritebackToReference$0$dst'@1| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1) inline$$WritebackToReference$0$dstPath@1 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1 (|size#$Path| inline$$WritebackToReference$0$dstPath@1) (|v#$Mutation| inline$$BorrowLoc$0$dst@1) (|v#$Mutation| |inline$$WriteRef$0$to'@1|)))) (= |inline$$WritebackToReference$0$dst'@2| |inline$$WritebackToReference$0$dst'@1|))) (and (=> (= (ControlFlow 0 29255) 29380) inline$$WritebackToValue$0$anon3_Then_correct) (=> (= (ControlFlow 0 29255) 29354) inline$$WritebackToValue$0$anon3_Else_correct)))))
(let ((inline$$WritebackToReference$0$anon0_correct  (=> (and (= inline$$WritebackToReference$0$srcPath@1 (|p#$Mutation| |inline$$WriteRef$0$to'@1|)) (= inline$$WritebackToReference$0$dstPath@1 (|p#$Mutation| inline$$BorrowLoc$0$dst@1))) (and (=> (= (ControlFlow 0 29163) 29255) inline$$WritebackToReference$0$anon3_Then_correct) (=> (= (ControlFlow 0 29163) 29199) inline$$WritebackToReference$0$anon3_Else_correct)))))
(let ((inline$$Splice1$0$anon0_correct  (=> (and (= |inline$$Splice1$0$dst'@1| ($Mutation (|l#$Mutation| |inline$$WriteRef$0$to'@1|) ($ConcatPath_stratified (|p#$Mutation| |inline$$WriteRef$0$to'@1|) (|p#$Mutation| inline$$Vector_borrow_mut$0$dst@2)) (|v#$Mutation| inline$$Vector_borrow_mut$0$dst@2))) (= (ControlFlow 0 29020) 29163)) inline$$WritebackToReference$0$anon0_correct)))
(let ((inline$$WriteRef$0$anon0_correct  (=> (and (= |inline$$WriteRef$0$to'@1| ($Mutation (|l#$Mutation| inline$$BorrowField$0$dst@1) (|p#$Mutation| inline$$BorrowField$0$dst@1) |inline$$Vector_borrow_mut$0$v'@1|)) (= (ControlFlow 0 28939) 29020)) inline$$Splice1$0$anon0_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon30_Else_correct  (=> (and (not $abort_flag@2@@0) (= (ControlFlow 0 28945) 28939)) inline$$WriteRef$0$anon0_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$Abort_correct  (=> (and (= inline$$Option_borrow_mut_$def_verify$0$$ret1@1 $Error) (= inline$$Option_borrow_mut_$def_verify$0$$ret0@1 $DefaultMutation)) (=> (and (and (= inline$$Option_borrow_mut_$def_verify$0$$ret1@2 inline$$Option_borrow_mut_$def_verify$0$$ret1@1) (= $abort_code@6@@0 $abort_code@5@@0)) (and (= $abort_flag@3@@0 true) (= (ControlFlow 0 28439) 29504))) anon0$2_correct@@0))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon5_correct  (=> (and (= $abort_code@5@@0 $abort_code@1@@0) (= (ControlFlow 0 29478) 28439)) inline$$Option_borrow_mut_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon25_Else_correct  (=> (and (not true) (= (ControlFlow 0 29476) 29478)) inline$$Option_borrow_mut_$def_verify$0$anon5_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon25_Then_correct  (=> (= (ControlFlow 0 29486) 29478) inline$$Option_borrow_mut_$def_verify$0$anon5_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon24_Then_correct  (=> $abort_flag@0@@0 (and (=> (= (ControlFlow 0 29470) 29486) inline$$Option_borrow_mut_$def_verify$0$anon25_Then_correct) (=> (= (ControlFlow 0 29470) 29476) inline$$Option_borrow_mut_$def_verify$0$anon25_Else_correct)))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon9_correct  (=> (and (= $abort_code@5@@0 $abort_code@2@@0) (= (ControlFlow 0 29458) 28439)) inline$$Option_borrow_mut_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon27_Else_correct  (=> (and (not true) (= (ControlFlow 0 29456) 29458)) inline$$Option_borrow_mut_$def_verify$0$anon9_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon27_Then_correct  (=> (= (ControlFlow 0 29466) 29458) inline$$Option_borrow_mut_$def_verify$0$anon9_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon26_Then_correct  (=> $abort_flag@1@@0 (and (=> (= (ControlFlow 0 29450) 29466) inline$$Option_borrow_mut_$def_verify$0$anon27_Then_correct) (=> (= (ControlFlow 0 29450) 29456) inline$$Option_borrow_mut_$def_verify$0$anon27_Else_correct)))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon17_correct  (=> (and (= $abort_code@5@@0 $abort_code@4@@0) (= (ControlFlow 0 29438) 28439)) inline$$Option_borrow_mut_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon31_Else_correct  (=> (and (not true) (= (ControlFlow 0 29436) 29438)) inline$$Option_borrow_mut_$def_verify$0$anon17_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon31_Then_correct  (=> (= (ControlFlow 0 29446) 29438) inline$$Option_borrow_mut_$def_verify$0$anon17_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon30_Then_correct  (=> $abort_flag@2@@0 (and (=> (= (ControlFlow 0 29430) 29446) inline$$Option_borrow_mut_$def_verify$0$anon31_Then_correct) (=> (= (ControlFlow 0 29430) 29436) inline$$Option_borrow_mut_$def_verify$0$anon31_Else_correct)))))
(let ((inline$$Vector_borrow_mut$0$anon3_Then$1_correct  (=> (and (and (= $abort_flag@2@@0 true) (= $abort_code@4@@0 $EXEC_FAILURE_CODE)) (and (= inline$$Vector_borrow_mut$0$dst@2 inline$$Vector_borrow_mut$0$dst@0) (= |inline$$Vector_borrow_mut$0$v'@1| |inline$$Vector_borrow_mut$0$v'@0|))) (and (=> (= (ControlFlow 0 28872) 29430) inline$$Option_borrow_mut_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 28872) 28945) inline$$Option_borrow_mut_$def_verify$0$anon30_Else_correct)))))
(let ((inline$$Vector_borrow_mut$0$anon3_Then_correct  (=> (and (or (< inline$$Vector_borrow_mut$0$i_ind@1 0) (>= inline$$Vector_borrow_mut$0$i_ind@1 (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1)))) (= (ControlFlow 0 28870) 28872)) inline$$Vector_borrow_mut$0$anon3_Then$1_correct)))
(let ((inline$$Vector_borrow_mut$0$anon3_Else_correct  (=> (and (not (or (< inline$$Vector_borrow_mut$0$i_ind@1 0) (>= inline$$Vector_borrow_mut$0$i_ind@1 (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1))))) (= inline$$Vector_borrow_mut$0$dst@1 ($Mutation ($Local 0) ($Path (|Store_[$int]$int| (|p#$Path| $EmptyPath) 0 inline$$Vector_borrow_mut$0$i_ind@1) 1) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1)) inline$$Vector_borrow_mut$0$i_ind@1)))) (=> (and (and (= $abort_flag@2@@0 $abort_flag@1@@0) (= $abort_code@4@@0 $abort_code@2@@0)) (and (= inline$$Vector_borrow_mut$0$dst@2 inline$$Vector_borrow_mut$0$dst@1) (= |inline$$Vector_borrow_mut$0$v'@1| inline$$ReadRef$1$v@1))) (and (=> (= (ControlFlow 0 28812) 29430) inline$$Option_borrow_mut_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 28812) 28945) inline$$Option_borrow_mut_$def_verify$0$anon30_Else_correct))))))
391
(let ((inline$$Vector_borrow_mut$0$anon0_correct  (=> (and (= inline$$Vector_borrow_mut$0$i_ind@1 (|i#$Integer| inline$$Option_borrow_mut_$def_verify$0$$t10@1)) ((_ is $Vector) inline$$ReadRef$1$v@1)) (and (=> (= (ControlFlow 0 28764) 28870) inline$$Vector_borrow_mut$0$anon3_Then_correct) (=> (= (ControlFlow 0 28764) 28812) inline$$Vector_borrow_mut$0$anon3_Else_correct)))))
392
393
394
395
396
397
398
399
400
401
(let ((inline$$Vector_borrow_mut$0$Entry_correct  (and (=> (= (ControlFlow 0 28754) (- 0 49459)) true) (=> (= (ControlFlow 0 28754) 28764) inline$$Vector_borrow_mut$0$anon0_correct))))
(let ((inline$$ReadRef$1$anon0_correct  (=> (and (= inline$$ReadRef$1$v@1 (|v#$Mutation| inline$$BorrowField$0$dst@1)) (= (ControlFlow 0 28611) 28754)) inline$$Vector_borrow_mut$0$Entry_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon28_Then$1_correct  (=> (and (= inline$$Option_borrow_mut_$def_verify$0$$t10@1 ($Integer 0)) (= (ControlFlow 0 28617) 28611)) inline$$ReadRef$1$anon0_correct)))
(let ((inline$$BorrowField$0$anon0_correct  (=> (= inline$$BorrowField$0$p@1 (|p#$Mutation| inline$$BorrowLoc$0$dst@1)) (=> (and (and (= inline$$BorrowField$0$size@1 (|size#$Path| inline$$BorrowField$0$p@1)) (= inline$$BorrowField$0$p@2 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1) inline$$BorrowField$0$size@1 $Option_Option_vec) (+ inline$$BorrowField$0$size@1 1)))) (and (= inline$$BorrowField$0$dst@1 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1) inline$$BorrowField$0$p@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1))) $Option_Option_vec))) (= (ControlFlow 0 28569) 28617))) inline$$Option_borrow_mut_$def_verify$0$anon28_Then$1_correct))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon28_Then_correct  (=> (and (|b#$Boolean| call4formal@$ret0@0@@0) (= (ControlFlow 0 28575) 28569)) inline$$BorrowField$0$anon0_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon14_correct  (=> (and (= $abort_code@5@@0 $abort_code@3@@0) (= (ControlFlow 0 28431) 28439)) inline$$Option_borrow_mut_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon29_Else_correct  (=> (and (not true) (= (ControlFlow 0 28429) 28431)) inline$$Option_borrow_mut_$def_verify$0$anon14_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon29_Then_correct  (=> (= (ControlFlow 0 28447) 28431) inline$$Option_borrow_mut_$def_verify$0$anon14_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon28_Else_correct  (=> (and (not (|b#$Boolean| call4formal@$ret0@0@@0)) (= $abort_code@3@@0 (|i#$Integer| call3formal@$ret0@0@@0))) (and (=> (= (ControlFlow 0 28423) 28447) inline$$Option_borrow_mut_$def_verify$0$anon29_Then_correct) (=> (= (ControlFlow 0 28423) 28429) inline$$Option_borrow_mut_$def_verify$0$anon29_Else_correct)))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon26_Else_correct  (=> (not $abort_flag@1@@0) (and (=> (= (ControlFlow 0 28411) 28575) inline$$Option_borrow_mut_$def_verify$0$anon28_Then_correct) (=> (= (ControlFlow 0 28411) 28423) inline$$Option_borrow_mut_$def_verify$0$anon28_Else_correct)))))
402
403
(let ((inline$$Option_borrow_mut_$def_verify$0$anon24_Else_correct  (=> (not $abort_flag@0@@0) (=> (and (and (and (= inline$$Option_borrow_mut_$def_verify$0$$t7@1 ($Integer 1)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@1@@0)) (and (=> $abort_flag@1@@0 (|b#$Boolean| ($Boolean false))) (=> (not $abort_flag@1@@0) (|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 28405) 29450) inline$$Option_borrow_mut_$def_verify$0$anon26_Then_correct) (=> (= (ControlFlow 0 28405) 28411) inline$$Option_borrow_mut_$def_verify$0$anon26_Else_correct))))))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon2$3_correct  (and (=> (= (ControlFlow 0 28395) (- 0 49196)) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$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$0$v@1)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (=> (and (and (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@0) (=> $abort_flag@0@@0 (|b#$Boolean| ($Boolean false)))) (and (=> (not $abort_flag@0@@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified call4formal@$ret0@0@@0 ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1)) $Option_Option_vec)) ($Integer 0)))))))))) ((_ is $Boolean) call4formal@$ret0@0@@0))) (and (=> (= (ControlFlow 0 28395) 29470) inline$$Option_borrow_mut_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 28395) 28405) inline$$Option_borrow_mut_$def_verify$0$anon24_Else_correct)))))))
404
405
406
407
408
(let ((inline$$ReadRef$0$anon0_correct  (=> (and (= inline$$ReadRef$0$v@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1)) (= (ControlFlow 0 28383) 28395)) inline$$Option_borrow_mut_$def_verify$0$anon2$3_correct)))
(let ((inline$$BorrowLoc$0$anon0_correct  (=> (and (= inline$$BorrowLoc$0$dst@1 ($Mutation ($Local 3) $EmptyPath t@@0)) (= (ControlFlow 0 28345) 28383)) inline$$ReadRef$0$anon0_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon23_Else_correct  (=> (and (not true) (= (ControlFlow 0 28261) 28345)) inline$$BorrowLoc$0$anon0_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon23_Then_correct  (=> (= (ControlFlow 0 29494) 28345) inline$$BorrowLoc$0$anon0_correct)))
(let ((inline$$Option_borrow_mut_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 28255) 29494) inline$$Option_borrow_mut_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 28255) 28261) inline$$Option_borrow_mut_$def_verify$0$anon23_Else_correct)))))
409
(let ((anon0$1_correct@@0  (=> (and (forall (($inv_addr@@0 Int) ($inv_tv0@@0 T@$TypeValue) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@0) 1) $inv_addr@@0)) (let ((va@@12 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@0) 1) $inv_addr@@0))))
410
411
(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))
412
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@0) 1) $inv_addr@@0))) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@0) 1) $inv_addr@@0))) $Option_Option_vec)) (let ((va@@13 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@0) 1) $inv_addr@@0))) $Option_Option_vec))))
413
414
415
416
(let ((l@@13 (|l#$ValueArray| va@@13)))
 (and (and (<= 0 l@@13) (<= l@@13 $MAX_U64)) (forall ((x@@13 Int) ) (!  (=> (or (< x@@13 0) (>= x@@13 l@@13)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@13) x@@13) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@13) x@@13))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@0) 1) $inv_addr@@0))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@0) 1) $inv_addr@@0))
)) (= (ControlFlow 0 29502) 28255)) inline$$Option_borrow_mut_$def_verify$0$anon0_correct)))
417
(let ((anon0_correct@@0  (=> (and (and (and (and (and ((_ is $Vector) t@@0) (let ((va@@14 (|v#$Vector| t@@0)))
418
419
(let ((l@@14 (|l#$ValueArray| va@@14)))
 (and (and (<= 0 l@@14) (<= l@@14 $MAX_U64)) (forall ((x@@14 Int) ) (!  (=> (or (< x@@14 0) (>= x@@14 l@@14)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@14) x@@14) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@14) x@@14))
420
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@0)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec)) (let ((va@@15 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec))))
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
(let ((l@@15 (|l#$ValueArray| va@@15)))
 (and (and (<= 0 l@@15) (<= l@@15 $MAX_U64)) (forall ((x@@15 Int) ) (!  (=> (or (< x@@15 0) (>= x@@15 l@@15)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@15) x@@15) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@15) x@@15))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 27775) 29502)) anon0$1_correct@@0)))
(let ((PreconditionGeneratedEntry_correct@@0  (=> (= (ControlFlow 0 48634) 27775) anon0_correct@@0)))
PreconditionGeneratedEntry_correct@@0))))))))))))))))))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $abort_flag@0@@1 () Bool)
(declare-fun inline$$Option_contains_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun $tv0@@2 () T@$TypeValue)
(declare-fun t@@1 () T@$Value)
(declare-fun e_ref () T@$Value)
(declare-fun inline$$Vector_contains$0$res@1 () T@$Value)
(declare-fun inline$$GetFieldFromValue$0$dst@1@@0 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 50036) (let ((anon0$2_correct@@1  (and (=> (= (ControlFlow 0 30322) (- 0 50386)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@1)) (=> (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@1) (and (=> (= (ControlFlow 0 30322) (- 0 50395)) (=> $abort_flag@0@@1 (|b#$Boolean| ($Boolean false)))) (=> (=> $abort_flag@0@@1 (|b#$Boolean| ($Boolean false))) (=> (= (ControlFlow 0 30322) (- 0 50404)) (=> (not $abort_flag@0@@1) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_contains_$def_verify$0$$ret0@2 ($Boolean  (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $Option_Option_vec)) ($Integer 0))))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$borrow $tv0@@2 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $Option_Option_vec) ($Integer 0)) e_ref))))))))))))))))
(let ((inline$$Option_contains_$def_verify$0$anon10_correct  (=> (= $abort_flag@0@@1 false) (=> (and (= inline$$Option_contains_$def_verify$0$$ret0@2 inline$$Vector_contains$0$res@1) (= (ControlFlow 0 30266) 30322)) anon0$2_correct@@1))))
(let ((inline$$Option_contains_$def_verify$0$anon15_Else_correct  (=> (and (not true) (= (ControlFlow 0 30264) 30266)) inline$$Option_contains_$def_verify$0$anon10_correct)))
(let ((inline$$Option_contains_$def_verify$0$anon15_Then_correct  (=> (= (ControlFlow 0 30274) 30266) inline$$Option_contains_$def_verify$0$anon10_correct)))
(let ((inline$$Option_contains_$def_verify$0$anon13_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 30258) 30274) inline$$Option_contains_$def_verify$0$anon15_Then_correct) (=> (= (ControlFlow 0 30258) 30264) inline$$Option_contains_$def_verify$0$anon15_Else_correct)))))
(let ((inline$$Option_contains_$def_verify$0$anon13_Then_correct true))
445
(let ((inline$$Vector_contains$0$anon0_correct  (=> (and ((_ is $Vector) inline$$GetFieldFromValue$0$dst@1@@0) (= inline$$Vector_contains$0$res@1 ($Boolean (exists ((i@@10 Int) )  (and (and (<= 0 i@@10) (< i@@10 (|l#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1@@0)))) ($IsEqual_stratified (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1@@0)) i@@10) e_ref)))))) (and (=> (= (ControlFlow 0 30242) 30278) inline$$Option_contains_$def_verify$0$anon13_Then_correct) (=> (= (ControlFlow 0 30242) 30258) inline$$Option_contains_$def_verify$0$anon13_Else_correct)))))
446
447
448
449
450
451
(let ((inline$$GetFieldFromValue$0$anon0_correct@@0  (=> (and (= inline$$GetFieldFromValue$0$dst@1@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $Option_Option_vec)) (= (ControlFlow 0 30175) 30242)) inline$$Vector_contains$0$anon0_correct)))
(let ((inline$$Option_contains_$def_verify$0$anon12_Else_correct  (=> (and (not true) (= (ControlFlow 0 30065) 30175)) inline$$GetFieldFromValue$0$anon0_correct@@0)))
(let ((inline$$Option_contains_$def_verify$0$anon12_Then_correct  (=> (= (ControlFlow 0 30306) 30175) inline$$GetFieldFromValue$0$anon0_correct@@0)))
(let ((inline$$Option_contains_$def_verify$0$anon11_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 30057) 30306) inline$$Option_contains_$def_verify$0$anon12_Then_correct) (=> (= (ControlFlow 0 30057) 30065) inline$$Option_contains_$def_verify$0$anon12_Else_correct)))))
(let ((inline$$Option_contains_$def_verify$0$anon11_Then_correct  (and (=> (= (ControlFlow 0 30314) 30306) inline$$Option_contains_$def_verify$0$anon12_Then_correct) (=> (= (ControlFlow 0 30314) 30065) inline$$Option_contains_$def_verify$0$anon12_Else_correct))))
(let ((inline$$Option_contains_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 30051) 30314) inline$$Option_contains_$def_verify$0$anon11_Then_correct) (=> (= (ControlFlow 0 30051) 30057) inline$$Option_contains_$def_verify$0$anon11_Else_correct)))))
452
(let ((anon0$1_correct@@1  (=> (and (forall (($inv_addr@@1 Int) ($inv_tv0@@1 T@$TypeValue) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@1) 1) $inv_addr@@1)) (let ((va@@16 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@1) 1) $inv_addr@@1))))
453
454
(let ((l@@16 (|l#$ValueArray| va@@16)))
 (and (and (<= 0 l@@16) (<= l@@16 $MAX_U64)) (forall ((x@@16 Int) ) (!  (=> (or (< x@@16 0) (>= x@@16 l@@16)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@16) x@@16) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@16) x@@16))
455
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@1) 1) $inv_addr@@1))) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@1) 1) $inv_addr@@1))) $Option_Option_vec)) (let ((va@@17 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@1) 1) $inv_addr@@1))) $Option_Option_vec))))
456
457
458
459
(let ((l@@17 (|l#$ValueArray| va@@17)))
 (and (and (<= 0 l@@17) (<= l@@17 $MAX_U64)) (forall ((x@@17 Int) ) (!  (=> (or (< x@@17 0) (>= x@@17 l@@17)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@17) x@@17) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@17) x@@17))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@1) 1) $inv_addr@@1))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@1) 1) $inv_addr@@1))
)) (= (ControlFlow 0 30320) 30051)) inline$$Option_contains_$def_verify$0$anon0_correct)))
460
(let ((anon0_correct@@1  (=> (and (and (and (and (and ((_ is $Vector) t@@1) (let ((va@@18 (|v#$Vector| t@@1)))
461
462
(let ((l@@18 (|l#$ValueArray| va@@18)))
 (and (and (<= 0 l@@18) (<= l@@18 $MAX_U64)) (forall ((x@@18 Int) ) (!  (=> (or (< x@@18 0) (>= x@@18 l@@18)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@18) x@@18) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@18) x@@18))
463
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@1)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $Option_Option_vec)) (let ((va@@19 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $Option_Option_vec))))
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
(let ((l@@19 (|l#$ValueArray| va@@19)))
 (and (and (<= 0 l@@19) (<= l@@19 $MAX_U64)) (forall ((x@@19 Int) ) (!  (=> (or (< x@@19 0) (>= x@@19 l@@19)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@19) x@@19) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@19) x@@19))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@1)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 29785) 30320)) anon0$1_correct@@1)))
(let ((PreconditionGeneratedEntry_correct@@1  (=> (= (ControlFlow 0 50036) 29785) anon0_correct@@1)))
PreconditionGeneratedEntry_correct@@1)))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $tv0@@3 () T@$TypeValue)
(declare-fun t@@2 () T@$Value)
(declare-fun $abort_flag@3@@1 () Bool)
(declare-fun $abort_code@6@@1 () Int)
(declare-fun inline$$Option_swap_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun inline$$Option_swap_$def_verify$0$$ret1@2 () T@$Value)
(declare-fun e () T@$Value)
(declare-fun inline$$Vector_pop_back$0$e@2 () T@$Value)
(declare-fun |inline$$WritebackToValue$0$vdst'@2@@0| () T@$Value)
(declare-fun $abort_code@4@@1 () Int)
(declare-fun $abort_flag@2@@1 () Bool)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@0| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@0| () T@$Value)
(declare-fun inline$$Option_Option_$pack_ref$1$$after@0 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@0 () T@$Mutation)
(declare-fun |inline$$WriteRef$1$to'@1| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@0 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@0 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@0| () T@$Mutation)
(declare-fun inline$$Option_swap_$def_verify$0$$trace_temp@2 () T@$Value)
(declare-fun |inline$$WriteRef$0$to'@1@@0| () T@$Mutation)
(declare-fun |inline$$Vector_push_back$0$v'@1| () T@$Value)
(declare-fun inline$$Option_swap_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun inline$$Option_swap_$def_verify$0$$ret1@1 () T@$Value)
(declare-fun $abort_code@5@@1 () Int)
(declare-fun $abort_code@1@@1 () Int)
(declare-fun $abort_flag@0@@2 () Bool)
(declare-fun $abort_code@2@@1 () Int)
(declare-fun $abort_flag@1@@1 () Bool)
(declare-fun inline$$ReadRef$2$v@1 () T@$Value)
(declare-fun inline$$Option_swap_$def_verify$0$$trace_temp@1 () T@$Value)
(declare-fun inline$$BorrowField$0$dst@1@@0 () T@$Mutation)
(declare-fun |inline$$Vector_pop_back$0$v'@2| () T@$Value)
(declare-fun inline$$Vector_pop_back$0$e@0 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@0| () T@$Value)
(declare-fun inline$$Vector_pop_back$0$len@1 () Int)
(declare-fun inline$$Vector_pop_back$0$e@1 () T@$Value)
(declare-fun inline$$ReadRef$1$v@1@@0 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@1| () T@$Value)
(declare-fun inline$$BorrowField$0$p@1@@0 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@0 () Int)
(declare-fun inline$$BorrowField$0$p@2@@0 () T@$Path)
(declare-fun call4formal@$ret0@0@@1 () T@$Value)
(declare-fun $abort_code@3@@1 () Int)
(declare-fun call3formal@$ret0@0@@1 () T@$Value)
(declare-fun inline$$Option_Option_$pack_ref$0$$after@0 () T@$Value)
(declare-fun inline$$Option_swap_$def_verify$0$$t11@1 () T@$Value)
(declare-fun inline$$ReadRef$0$v@1@@0 () T@$Value)
(declare-fun inline$$Option_Option_$unpack_ref$0$$before@0 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 50433) (let ((anon0$2_correct@@2  (and (=> (= (ControlFlow 0 32703) (- 0 52007)) (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3@@1)) (=> (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3@@1) (and (=> (= (ControlFlow 0 32703) (- 0 52018)) (=> $abort_flag@3@@1 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec)) ($Integer 0)))))) (=> (=> $abort_flag@3@@1 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec)) ($Integer 0))))) (and (=> (= (ControlFlow 0 32703) (- 0 52029)) (=> $abort_flag@3@@1 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6@@1 (|i#$Integer| ($Integer 7)))))) (=> (=> $abort_flag@3@@1 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6@@1 (|i#$Integer| ($Integer 7))))) (and (=> (= (ControlFlow 0 32703) (- 0 52051)) (=> (not $abort_flag@3@@1) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_swap_$def_verify$0$$ret0@2 ($Vector_$borrow $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec) ($Integer 0))))))) (=> (=> (not $abort_flag@3@@1) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_swap_$def_verify$0$$ret0@2 ($Vector_$borrow $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec) ($Integer 0)))))) (and (=> (= (ControlFlow 0 32703) (- 0 52069)) (=> (not $abort_flag@3@@1) (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_swap_$def_verify$0$$ret1@2)) $Option_Option_vec)) ($Integer 0))))))))) (=> (=> (not $abort_flag@3@@1) (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_swap_$def_verify$0$$ret1@2)) $Option_Option_vec)) ($Integer 0)))))))) (=> (= (ControlFlow 0 32703) (- 0 52081)) (=> (not $abort_flag@3@@1) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$borrow $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_swap_$def_verify$0$$ret1@2)) $Option_Option_vec) ($Integer 0)) e)))))))))))))))))
(let ((inline$$Option_swap_$def_verify$0$anon34_correct  (=> (= inline$$Option_swap_$def_verify$0$$ret0@2 inline$$Vector_pop_back$0$e@2) (=> (and (and (= inline$$Option_swap_$def_verify$0$$ret1@2 |inline$$WritebackToValue$0$vdst'@2@@0|) (= $abort_code@6@@1 $abort_code@4@@1)) (and (= $abort_flag@3@@1 $abort_flag@2@@1) (= (ControlFlow 0 32553) 32703))) anon0$2_correct@@2))))
(let ((inline$$Option_swap_$def_verify$0$anon51_Else_correct  (=> (and (not true) (= (ControlFlow 0 32551) 32553)) inline$$Option_swap_$def_verify$0$anon34_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon51_Then_correct  (=> (= (ControlFlow 0 32561) 32553) inline$$Option_swap_$def_verify$0$anon34_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon50_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 32541) 32561) inline$$Option_swap_$def_verify$0$anon51_Then_correct) (=> (= (ControlFlow 0 32541) 32551) inline$$Option_swap_$def_verify$0$anon51_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon50_Then_correct  (and (=> (= (ControlFlow 0 32569) 32561) inline$$Option_swap_$def_verify$0$anon51_Then_correct) (=> (= (ControlFlow 0 32569) 32551) inline$$Option_swap_$def_verify$0$anon51_Else_correct))))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@0  (=> (and (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|) ($Local 6))) (= |inline$$WritebackToValue$0$vdst'@2@@0| t@@2)) (and (=> (= (ControlFlow 0 32499) 32569) inline$$Option_swap_$def_verify$0$anon50_Then_correct) (=> (= (ControlFlow 0 32499) 32541) inline$$Option_swap_$def_verify$0$anon50_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@0  (=> (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|) ($Local 6)) (=> (and (= |inline$$WritebackToValue$0$vdst'@1@@0| ($UpdateValue_stratified (|p#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|) 0 t@@2 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|))) (= |inline$$WritebackToValue$0$vdst'@2@@0| |inline$$WritebackToValue$0$vdst'@1@@0|)) (and (=> (= (ControlFlow 0 32525) 32569) inline$$Option_swap_$def_verify$0$anon50_Then_correct) (=> (= (ControlFlow 0 32525) 32541) inline$$Option_swap_$def_verify$0$anon50_Else_correct))))))
(let ((inline$$Option_Option_$pack_ref$1$anon0_correct  (and (=> (= (ControlFlow 0 32402) (- 0 51783)) (|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))))) (and (=> (= (ControlFlow 0 32402) 32525) inline$$WritebackToValue$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 32402) 32499) inline$$WritebackToValue$0$anon3_Else_correct@@0))))))
(let ((inline$$Option_Option_$pack_ref$1$Entry_correct  (=> (and (= inline$$Option_Option_$pack_ref$1$$after@0 (|v#$Mutation| |inline$$WritebackToReference$0$dst'@2@@0|)) (= (ControlFlow 0 32378) 32402)) inline$$Option_Option_$pack_ref$1$anon0_correct)))
(let ((inline$$WritebackToReference$0$anon3_Else_correct@@0  (=> (not (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) (|l#$Mutation| |inline$$WriteRef$1$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@0) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@0))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@0 inline$$WritebackToReference$0$srcPath@1@@0))) (=> (and (= |inline$$WritebackToReference$0$dst'@2@@0| inline$$BorrowLoc$0$dst@1@@0) (= (ControlFlow 0 32270) 32378)) inline$$Option_Option_$pack_ref$1$Entry_correct))))
(let ((inline$$WritebackToReference$0$anon3_Then_correct@@0  (=> (and (and (and (and (= (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) (|l#$Mutation| |inline$$WriteRef$1$to'@1|)) (<= (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@0) (|size#$Path| inline$$WritebackToReference$0$srcPath@1@@0))) ($IsPathPrefix_stratified inline$$WritebackToReference$0$dstPath@1@@0 inline$$WritebackToReference$0$srcPath@1@@0)) (= |inline$$WritebackToReference$0$dst'@1@@0| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) inline$$WritebackToReference$0$dstPath@1@@0 ($UpdateValue_stratified inline$$WritebackToReference$0$srcPath@1@@0 (|size#$Path| inline$$WritebackToReference$0$dstPath@1@@0) (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0) (|v#$Mutation| |inline$$WriteRef$1$to'@1|))))) (and (= |inline$$WritebackToReference$0$dst'@2@@0| |inline$$WritebackToReference$0$dst'@1@@0|) (= (ControlFlow 0 32326) 32378))) inline$$Option_Option_$pack_ref$1$Entry_correct)))
(let ((inline$$WritebackToReference$0$anon0_correct@@0  (=> (and (= inline$$WritebackToReference$0$srcPath@1@@0 (|p#$Mutation| |inline$$WriteRef$1$to'@1|)) (= inline$$WritebackToReference$0$dstPath@1@@0 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@0))) (and (=> (= (ControlFlow 0 32234) 32326) inline$$WritebackToReference$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 32234) 32270) inline$$WritebackToReference$0$anon3_Else_correct@@0)))))
(let ((inline$$Option_swap_$def_verify$0$anon49_Else_correct  (=> (and (not true) (= (ControlFlow 0 32097) 32234)) inline$$WritebackToReference$0$anon0_correct@@0)))
(let ((inline$$Option_swap_$def_verify$0$anon49_Then_correct  (=> (and (= inline$$Option_swap_$def_verify$0$$trace_temp@2 (|v#$Mutation| |inline$$WriteRef$1$to'@1|)) (= (ControlFlow 0 32579) 32234)) inline$$WritebackToReference$0$anon0_correct@@0)))
(let ((inline$$WriteRef$1$anon0_correct  (=> (= |inline$$WriteRef$1$to'@1| ($Mutation (|l#$Mutation| |inline$$WriteRef$0$to'@1@@0|) (|p#$Mutation| |inline$$WriteRef$0$to'@1@@0|) |inline$$Vector_push_back$0$v'@1|)) (and (=> (= (ControlFlow 0 32083) 32579) inline$$Option_swap_$def_verify$0$anon49_Then_correct) (=> (= (ControlFlow 0 32083) 32097) inline$$Option_swap_$def_verify$0$anon49_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon47_Else_correct  (=> (and (not $abort_flag@2@@1) (= (ControlFlow 0 32089) 32083)) inline$$WriteRef$1$anon0_correct)))
(let ((inline$$Option_swap_$def_verify$0$Abort_correct  (=> (= inline$$Option_swap_$def_verify$0$$ret0@1 $Error) (=> (and (= inline$$Option_swap_$def_verify$0$$ret1@1 $Error) (= inline$$Option_swap_$def_verify$0$$ret0@2 inline$$Option_swap_$def_verify$0$$ret0@1)) (=> (and (and (= inline$$Option_swap_$def_verify$0$$ret1@2 inline$$Option_swap_$def_verify$0$$ret1@1) (= $abort_code@6@@1 $abort_code@5@@1)) (and (= $abort_flag@3@@1 true) (= (ControlFlow 0 31449) 32703))) anon0$2_correct@@2)))))
(let ((inline$$Option_swap_$def_verify$0$anon7_correct  (=> (and (= $abort_code@5@@1 $abort_code@1@@1) (= (ControlFlow 0 32669) 31449)) inline$$Option_swap_$def_verify$0$Abort_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon38_Else_correct  (=> (and (not true) (= (ControlFlow 0 32667) 32669)) inline$$Option_swap_$def_verify$0$anon7_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon38_Then_correct  (=> (= (ControlFlow 0 32677) 32669) inline$$Option_swap_$def_verify$0$anon7_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon37_Then_correct  (=> $abort_flag@0@@2 (and (=> (= (ControlFlow 0 32661) 32677) inline$$Option_swap_$def_verify$0$anon38_Then_correct) (=> (= (ControlFlow 0 32661) 32667) inline$$Option_swap_$def_verify$0$anon38_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon11_correct  (=> (and (= $abort_code@5@@1 $abort_code@2@@1) (= (ControlFlow 0 32649) 31449)) inline$$Option_swap_$def_verify$0$Abort_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon40_Else_correct  (=> (and (not true) (= (ControlFlow 0 32647) 32649)) inline$$Option_swap_$def_verify$0$anon11_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon40_Then_correct  (=> (= (ControlFlow 0 32657) 32649) inline$$Option_swap_$def_verify$0$anon11_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon39_Then_correct  (=> $abort_flag@1@@1 (and (=> (= (ControlFlow 0 32641) 32657) inline$$Option_swap_$def_verify$0$anon40_Then_correct) (=> (= (ControlFlow 0 32641) 32647) inline$$Option_swap_$def_verify$0$anon40_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon19_correct  (=> (and (= $abort_code@5@@1 $abort_code@4@@1) (= (ControlFlow 0 32629) 31449)) inline$$Option_swap_$def_verify$0$Abort_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon44_Else_correct  (=> (and (not true) (= (ControlFlow 0 32627) 32629)) inline$$Option_swap_$def_verify$0$anon19_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon44_Then_correct  (=> (= (ControlFlow 0 32637) 32629) inline$$Option_swap_$def_verify$0$anon19_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon43_Then_correct  (=> $abort_flag@2@@1 (and (=> (= (ControlFlow 0 32621) 32637) inline$$Option_swap_$def_verify$0$anon44_Then_correct) (=> (= (ControlFlow 0 32621) 32627) inline$$Option_swap_$def_verify$0$anon44_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon27_correct  (=> (and (= $abort_code@5@@1 $abort_code@4@@1) (= (ControlFlow 0 32591) 31449)) inline$$Option_swap_$def_verify$0$Abort_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon48_Else_correct  (=> (and (not true) (= (ControlFlow 0 32589) 32591)) inline$$Option_swap_$def_verify$0$anon27_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon48_Then_correct  (=> (= (ControlFlow 0 32599) 32591) inline$$Option_swap_$def_verify$0$anon27_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon47_Then_correct  (=> $abort_flag@2@@1 (and (=> (= (ControlFlow 0 32583) 32599) inline$$Option_swap_$def_verify$0$anon48_Then_correct) (=> (= (ControlFlow 0 32583) 32589) inline$$Option_swap_$def_verify$0$anon48_Else_correct)))))
558
(let ((inline$$Vector_push_back$0$anon0_correct  (=> (and ((_ is $Vector) inline$$ReadRef$2$v@1) (= |inline$$Vector_push_back$0$v'@1| ($Vector (let ((len@@0 (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$2$v@1))))
559
560
561
562
563
564
565
566
567
568
569
570
($ValueArray (|Store_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$2$v@1)) len@@0 e) (+ len@@0 1)))))) (and (=> (= (ControlFlow 0 32018) 32583) inline$$Option_swap_$def_verify$0$anon47_Then_correct) (=> (= (ControlFlow 0 32018) 32089) inline$$Option_swap_$def_verify$0$anon47_Else_correct)))))
(let ((inline$$ReadRef$2$anon0_correct  (=> (and (= inline$$ReadRef$2$v@1 (|v#$Mutation| |inline$$WriteRef$0$to'@1@@0|)) (= (ControlFlow 0 31955) 32018)) inline$$Vector_push_back$0$anon0_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon46_Else_correct  (=> (and (not true) (= (ControlFlow 0 31923) 31955)) inline$$ReadRef$2$anon0_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon46_Then_correct  (=> (= (ControlFlow 0 32607) 31955) inline$$ReadRef$2$anon0_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon45_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 31881) 32607) inline$$Option_swap_$def_verify$0$anon46_Then_correct) (=> (= (ControlFlow 0 31881) 31923) inline$$Option_swap_$def_verify$0$anon46_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon45_Then_correct  (=> (= inline$$Option_swap_$def_verify$0$$trace_temp@1 (|v#$Mutation| |inline$$WriteRef$0$to'@1@@0|)) (and (=> (= (ControlFlow 0 32617) 32607) inline$$Option_swap_$def_verify$0$anon46_Then_correct) (=> (= (ControlFlow 0 32617) 31923) inline$$Option_swap_$def_verify$0$anon46_Else_correct)))))
(let ((inline$$WriteRef$0$anon0_correct@@0  (=> (= |inline$$WriteRef$0$to'@1@@0| ($Mutation (|l#$Mutation| inline$$BorrowField$0$dst@1@@0) (|p#$Mutation| inline$$BorrowField$0$dst@1@@0) |inline$$Vector_pop_back$0$v'@2|)) (and (=> (= (ControlFlow 0 31867) 32617) inline$$Option_swap_$def_verify$0$anon45_Then_correct) (=> (= (ControlFlow 0 31867) 31881) inline$$Option_swap_$def_verify$0$anon45_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon43_Else_correct  (=> (and (not $abort_flag@2@@1) (= (ControlFlow 0 31873) 31867)) inline$$WriteRef$0$anon0_correct@@0)))
(let ((inline$$Vector_pop_back$0$anon3_Then$1_correct  (=> (and (and (= $abort_flag@2@@1 true) (= $abort_code@4@@1 $EXEC_FAILURE_CODE)) (and (= inline$$Vector_pop_back$0$e@2 inline$$Vector_pop_back$0$e@0) (= |inline$$Vector_pop_back$0$v'@2| |inline$$Vector_pop_back$0$v'@0|))) (and (=> (= (ControlFlow 0 31800) 32621) inline$$Option_swap_$def_verify$0$anon43_Then_correct) (=> (= (ControlFlow 0 31800) 31873) inline$$Option_swap_$def_verify$0$anon43_Else_correct)))))
(let ((inline$$Vector_pop_back$0$anon3_Then_correct  (=> (and (= inline$$Vector_pop_back$0$len@1 0) (= (ControlFlow 0 31798) 31800)) inline$$Vector_pop_back$0$anon3_Then$1_correct)))
(let ((inline$$Vector_pop_back$0$anon3_Else_correct  (=> (not (= inline$$Vector_pop_back$0$len@1 0)) (=> (and (= inline$$Vector_pop_back$0$e@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@0)) (- inline$$Vector_pop_back$0$len@1 1))) (= |inline$$Vector_pop_back$0$v'@1| ($Vector (let ((l@@20 (- (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@0)) 1)))
($ValueArray (|lambda#0| 0 l@@20 (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@0)) $Error) l@@20))))) (=> (and (and (= $abort_flag@2@@1 $abort_flag@1@@1) (= $abort_code@4@@1 $abort_code@2@@1)) (and (= inline$$Vector_pop_back$0$e@2 inline$$Vector_pop_back$0$e@1) (= |inline$$Vector_pop_back$0$v'@2| |inline$$Vector_pop_back$0$v'@1|))) (and (=> (= (ControlFlow 0 31750) 32621) inline$$Option_swap_$def_verify$0$anon43_Then_correct) (=> (= (ControlFlow 0 31750) 31873) inline$$Option_swap_$def_verify$0$anon43_Else_correct)))))))
571
(let ((inline$$Vector_pop_back$0$anon0_correct  (=> (and ((_ is $Vector) inline$$ReadRef$1$v@1@@0) (= inline$$Vector_pop_back$0$len@1 (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@0)))) (and (=> (= (ControlFlow 0 31728) 31798) inline$$Vector_pop_back$0$anon3_Then_correct) (=> (= (ControlFlow 0 31728) 31750) inline$$Vector_pop_back$0$anon3_Else_correct)))))
572
573
574
575
576
577
578
579
580
581
582
(let ((inline$$ReadRef$1$anon0_correct@@0  (=> (and (= inline$$ReadRef$1$v@1@@0 (|v#$Mutation| inline$$BorrowField$0$dst@1@@0)) (= (ControlFlow 0 31617) 31728)) inline$$Vector_pop_back$0$anon0_correct)))
(let ((inline$$BorrowField$0$anon0_correct@@0  (=> (= inline$$BorrowField$0$p@1@@0 (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@0)) (=> (and (and (= inline$$BorrowField$0$size@1@@0 (|size#$Path| inline$$BorrowField$0$p@1@@0)) (= inline$$BorrowField$0$p@2@@0 ($Path (|Store_[$int]$int| (|p#$Path| inline$$BorrowField$0$p@1@@0) inline$$BorrowField$0$size@1@@0 $Option_Option_vec) (+ inline$$BorrowField$0$size@1@@0 1)))) (and (= inline$$BorrowField$0$dst@1@@0 ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@0) inline$$BorrowField$0$p@2@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0))) $Option_Option_vec))) (= (ControlFlow 0 31579) 31617))) inline$$ReadRef$1$anon0_correct@@0))))
(let ((inline$$Option_swap_$def_verify$0$anon41_Then_correct  (=> (and (|b#$Boolean| call4formal@$ret0@0@@1) (= (ControlFlow 0 31585) 31579)) inline$$BorrowField$0$anon0_correct@@0)))
(let ((inline$$Option_swap_$def_verify$0$anon16_correct  (=> (and (= $abort_code@5@@1 $abort_code@3@@1) (= (ControlFlow 0 31441) 31449)) inline$$Option_swap_$def_verify$0$Abort_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon42_Else_correct  (=> (and (not true) (= (ControlFlow 0 31439) 31441)) inline$$Option_swap_$def_verify$0$anon16_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon42_Then_correct  (=> (= (ControlFlow 0 31457) 31441) inline$$Option_swap_$def_verify$0$anon16_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon41_Else$1_correct  (=> (= $abort_code@3@@1 (|i#$Integer| call3formal@$ret0@0@@1)) (and (=> (= (ControlFlow 0 31433) 31457) inline$$Option_swap_$def_verify$0$anon42_Then_correct) (=> (= (ControlFlow 0 31433) 31439) inline$$Option_swap_$def_verify$0$anon42_Else_correct)))))
(let ((inline$$Option_Option_$pack_ref$0$anon0_correct  (and (=> (= (ControlFlow 0 31423) (- 0 51261)) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_Option_$pack_ref$0$$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$0$$after@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (=> (= (ControlFlow 0 31423) 31433) inline$$Option_swap_$def_verify$0$anon41_Else$1_correct)))))
(let ((inline$$Option_Option_$pack_ref$0$Entry_correct  (=> (and (= inline$$Option_Option_$pack_ref$0$$after@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0)) (= (ControlFlow 0 31399) 31423)) inline$$Option_Option_$pack_ref$0$anon0_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon41_Else_correct  (=> (and (not (|b#$Boolean| call4formal@$ret0@0@@1)) (= (ControlFlow 0 31427) 31399)) inline$$Option_Option_$pack_ref$0$Entry_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon39_Else_correct  (=> (not $abort_flag@1@@1) (and (=> (= (ControlFlow 0 31347) 31585) inline$$Option_swap_$def_verify$0$anon41_Then_correct) (=> (= (ControlFlow 0 31347) 31427) inline$$Option_swap_$def_verify$0$anon41_Else_correct)))))
583
584
(let ((inline$$Option_swap_$def_verify$0$anon37_Else_correct  (=> (not $abort_flag@0@@2) (=> (and (and (and (= inline$$Option_swap_$def_verify$0$$t11@1 ($Integer 1)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@1@@1)) (and (=> $abort_flag@1@@1 (|b#$Boolean| ($Boolean false))) (=> (not $abort_flag@1@@1) (|b#$Boolean| ($Boolean ($IsEqual_stratified call3formal@$ret0@0@@1 ($Integer 7))))))) (and (and ((_ is $Integer) call3formal@$ret0@0@@1) (>= (|i#$Integer| call3formal@$ret0@0@@1) 0)) (<= (|i#$Integer| call3formal@$ret0@0@@1) $MAX_U64))) (and (=> (= (ControlFlow 0 31341) 32641) inline$$Option_swap_$def_verify$0$anon39_Then_correct) (=> (= (ControlFlow 0 31341) 31347) inline$$Option_swap_$def_verify$0$anon39_Else_correct))))))
(let ((inline$$Option_swap_$def_verify$0$anon4$5_correct  (and (=> (= (ControlFlow 0 31331) (- 0 51111)) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@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$$ReadRef$0$v@1@@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (=> (and (and (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@2) (=> $abort_flag@0@@2 (|b#$Boolean| ($Boolean false)))) (and (=> (not $abort_flag@0@@2) (|b#$Boolean| ($Boolean ($IsEqual_stratified call4formal@$ret0@0@@1 ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@3 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@0)) $Option_Option_vec)) ($Integer 0)))))))))) ((_ is $Boolean) call4formal@$ret0@0@@1))) (and (=> (= (ControlFlow 0 31331) 32661) inline$$Option_swap_$def_verify$0$anon37_Then_correct) (=> (= (ControlFlow 0 31331) 31341) inline$$Option_swap_$def_verify$0$anon37_Else_correct)))))))
585
586
587
588
589
590
591
592
593
(let ((inline$$ReadRef$0$anon0_correct@@0  (=> (and (= inline$$ReadRef$0$v@1@@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0)) (= (ControlFlow 0 31319) 31331)) inline$$Option_swap_$def_verify$0$anon4$5_correct)))
(let ((inline$$Option_Option_$unpack_ref$0$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$0$$before@0)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1))))) (= (ControlFlow 0 31283) 31319)) inline$$ReadRef$0$anon0_correct@@0)))
(let ((inline$$Option_Option_$unpack_ref$0$Entry_correct  (=> (and (= inline$$Option_Option_$unpack_ref$0$$before@0 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@0)) (= (ControlFlow 0 31277) 31283)) inline$$Option_Option_$unpack_ref$0$anon0_correct)))
(let ((inline$$BorrowLoc$0$anon0_correct@@0  (=> (and (= inline$$BorrowLoc$0$dst@1@@0 ($Mutation ($Local 6) $EmptyPath t@@2)) (= (ControlFlow 0 31243) 31277)) inline$$Option_Option_$unpack_ref$0$Entry_correct)))
(let ((inline$$Option_swap_$def_verify$0$anon36_Else_correct  (=> (and (not true) (= (ControlFlow 0 31125) 31243)) inline$$BorrowLoc$0$anon0_correct@@0)))
(let ((inline$$Option_swap_$def_verify$0$anon36_Then_correct  (=> (= (ControlFlow 0 32685) 31243) inline$$BorrowLoc$0$anon0_correct@@0)))
(let ((inline$$Option_swap_$def_verify$0$anon35_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 31117) 32685) inline$$Option_swap_$def_verify$0$anon36_Then_correct) (=> (= (ControlFlow 0 31117) 31125) inline$$Option_swap_$def_verify$0$anon36_Else_correct)))))
(let ((inline$$Option_swap_$def_verify$0$anon35_Then_correct  (and (=> (= (ControlFlow 0 32693) 32685) inline$$Option_swap_$def_verify$0$anon36_Then_correct) (=> (= (ControlFlow 0 32693) 31125) inline$$Option_swap_$def_verify$0$anon36_Else_correct))))
(let ((inline$$Option_swap_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 31111) 32693) inline$$Option_swap_$def_verify$0$anon35_Then_correct) (=> (= (ControlFlow 0 31111) 31117) inline$$Option_swap_$def_verify$0$anon35_Else_correct)))))
594
(let ((anon0$1_correct@@2  (=> (and (forall (($inv_addr@@2 Int) ($inv_tv0@@2 T@$TypeValue) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@2) 1) $inv_addr@@2)) (let ((va@@20 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@2) 1) $inv_addr@@2))))
595
596
(let ((l@@21 (|l#$ValueArray| va@@20)))
 (and (and (<= 0 l@@21) (<= l@@21 $MAX_U64)) (forall ((x@@20 Int) ) (!  (=> (or (< x@@20 0) (>= x@@20 l@@21)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@20) x@@20) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@20) x@@20))
597
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@2) 1) $inv_addr@@2))) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@2) 1) $inv_addr@@2))) $Option_Option_vec)) (let ((va@@21 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@2) 1) $inv_addr@@2))) $Option_Option_vec))))
598
599
600
601
(let ((l@@22 (|l#$ValueArray| va@@21)))
 (and (and (<= 0 l@@22) (<= l@@22 $MAX_U64)) (forall ((x@@21 Int) ) (!  (=> (or (< x@@21 0) (>= x@@21 l@@22)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@21) x@@21) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@21) x@@21))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@2) 1) $inv_addr@@2))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@2) 1) $inv_addr@@2))
)) (= (ControlFlow 0 32701) 31111)) inline$$Option_swap_$def_verify$0$anon0_correct)))
602
(let ((anon0_correct@@2  (=> (and (and (and (and (and ((_ is $Vector) t@@2) (let ((va@@22 (|v#$Vector| t@@2)))
603
604
(let ((l@@23 (|l#$ValueArray| va@@22)))
 (and (and (<= 0 l@@23) (<= l@@23 $MAX_U64)) (forall ((x@@22 Int) ) (!  (=> (or (< x@@22 0) (>= x@@22 l@@23)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@22) x@@22) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@22) x@@22))
605
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@2)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec)) (let ((va@@23 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec))))
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
(let ((l@@24 (|l#$ValueArray| va@@23)))
 (and (and (<= 0 l@@24) (<= l@@24 $MAX_U64)) (forall ((x@@23 Int) ) (!  (=> (or (< x@@23 0) (>= x@@23 l@@24)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@23) x@@23) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@23) x@@23))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@2)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 30456) 32701)) anon0$1_correct@@2)))
(let ((PreconditionGeneratedEntry_correct@@2  (=> (= (ControlFlow 0 50433) 30456) anon0_correct@@2)))
PreconditionGeneratedEntry_correct@@2))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $abort_flag@2@@2 () Bool)
(declare-fun inline$$Option_borrow_with_default_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun $tv0@@4 () T@$TypeValue)
(declare-fun t@@3 () T@$Value)
(declare-fun default_ref () T@$Value)
(declare-fun inline$$Option_borrow_with_default_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun $abort_flag@0@@3 () Bool)
(declare-fun $abort_flag@1@@2 () Bool)
(declare-fun |inline$$Option_borrow_with_default_$def_verify$0$tmp#$2@1| () T@$Value)
(declare-fun inline$$Vector_is_empty$0$b@1 () T@$Value)
(declare-fun inline$$Vector_borrow$0$dst@2@@0 () T@$Value)
(declare-fun inline$$Vector_borrow$0$dst@0@@0 () T@$Value)
(declare-fun inline$$Vector_borrow$0$i_ind@1@@0 () Int)
(declare-fun inline$$GetFieldFromValue$0$dst@1@@1 () T@$Value)
(declare-fun inline$$Vector_borrow$0$dst@1@@0 () T@$Value)
(declare-fun inline$$Option_borrow_with_default_$def_verify$0$$t7@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 52106) (let ((anon0$2_correct@@3  (and (=> (= (ControlFlow 0 34066) (- 0 52693)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@2@@2)) (=> (=> (|b#$Boolean| ($Boolean false)) $abort_flag@2@@2) (and (=> (= (ControlFlow 0 34066) (- 0 52702)) (=> $abort_flag@2@@2 (|b#$Boolean| ($Boolean false)))) (=> (=> $abort_flag@2@@2 (|b#$Boolean| ($Boolean false))) (=> (= (ControlFlow 0 34066) (- 0 52711)) (=> (not $abort_flag@2@@2) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_borrow_with_default_$def_verify$0$$ret0@2 (ite (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@4 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@3)) $Option_Option_vec)) ($Integer 0))))))) ($Vector_$borrow $tv0@@4 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@3)) $Option_Option_vec) ($Integer 0)) default_ref))))))))))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$Abort_correct  (=> (and (and (= inline$$Option_borrow_with_default_$def_verify$0$$ret0@1 $Error) (= $abort_flag@2@@2 true)) (and (= inline$$Option_borrow_with_default_$def_verify$0$$ret0@2 inline$$Option_borrow_with_default_$def_verify$0$$ret0@1) (= (ControlFlow 0 33950) 34066))) anon0$2_correct@@3)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon29_Else_correct  (=> (and (not true) (= (ControlFlow 0 33942) 33950)) inline$$Option_borrow_with_default_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon29_Then_correct  (=> (= (ControlFlow 0 33958) 33950) inline$$Option_borrow_with_default_$def_verify$0$Abort_correct)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon28_Then_correct  (=> $abort_flag@0@@3 (and (=> (= (ControlFlow 0 33936) 33958) inline$$Option_borrow_with_default_$def_verify$0$anon29_Then_correct) (=> (= (ControlFlow 0 33936) 33942) inline$$Option_borrow_with_default_$def_verify$0$anon29_Else_correct)))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon20_correct  (=> (= $abort_flag@2@@2 $abort_flag@1@@2) (=> (and (= inline$$Option_borrow_with_default_$def_verify$0$$ret0@2 |inline$$Option_borrow_with_default_$def_verify$0$tmp#$2@1|) (= (ControlFlow 0 33924) 34066)) anon0$2_correct@@3))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon30_Else_correct  (=> (and (not true) (= (ControlFlow 0 33922) 33924)) inline$$Option_borrow_with_default_$def_verify$0$anon20_correct)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon30_Then_correct  (=> (= (ControlFlow 0 33932) 33924) inline$$Option_borrow_with_default_$def_verify$0$anon20_correct)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon14_correct  (=> (and (= $abort_flag@1@@2 false) (= |inline$$Option_borrow_with_default_$def_verify$0$tmp#$2@1| default_ref)) (and (=> (= (ControlFlow 0 34006) 33932) inline$$Option_borrow_with_default_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 34006) 33922) inline$$Option_borrow_with_default_$def_verify$0$anon30_Else_correct)))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon27_Else_correct  (=> (and (not true) (= (ControlFlow 0 34004) 34006)) inline$$Option_borrow_with_default_$def_verify$0$anon14_correct)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon27_Then_correct  (=> (= (ControlFlow 0 34014) 34006) inline$$Option_borrow_with_default_$def_verify$0$anon14_correct)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon26_Then_correct  (=> (|b#$Boolean| inline$$Vector_is_empty$0$b@1) (and (=> (= (ControlFlow 0 33996) 34014) inline$$Option_borrow_with_default_$def_verify$0$anon27_Then_correct) (=> (= (ControlFlow 0 33996) 34004) inline$$Option_borrow_with_default_$def_verify$0$anon27_Else_correct)))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon28_Else_correct  (=> (not $abort_flag@0@@3) (=> (and (= $abort_flag@1@@2 $abort_flag@0@@3) (= |inline$$Option_borrow_with_default_$def_verify$0$tmp#$2@1| inline$$Vector_borrow$0$dst@2@@0)) (and (=> (= (ControlFlow 0 33912) 33932) inline$$Option_borrow_with_default_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 33912) 33922) inline$$Option_borrow_with_default_$def_verify$0$anon30_Else_correct))))))
(let ((inline$$Vector_borrow$0$anon3_Then$1_correct@@0  (=> (and (= $abort_flag@0@@3 true) (= inline$$Vector_borrow$0$dst@2@@0 inline$$Vector_borrow$0$dst@0@@0)) (and (=> (= (ControlFlow 0 33898) 33936) inline$$Option_borrow_with_default_$def_verify$0$anon28_Then_correct) (=> (= (ControlFlow 0 33898) 33912) inline$$Option_borrow_with_default_$def_verify$0$anon28_Else_correct)))))
(let ((inline$$Vector_borrow$0$anon3_Then_correct@@0  (=> (and (or (< inline$$Vector_borrow$0$i_ind@1@@0 0) (>= inline$$Vector_borrow$0$i_ind@1@@0 (|l#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1@@1)))) (= (ControlFlow 0 33896) 33898)) inline$$Vector_borrow$0$anon3_Then$1_correct@@0)))
(let ((inline$$Vector_borrow$0$anon3_Else_correct@@0  (=> (and (and (not (or (< inline$$Vector_borrow$0$i_ind@1@@0 0) (>= inline$$Vector_borrow$0$i_ind@1@@0 (|l#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1@@1))))) (= inline$$Vector_borrow$0$dst@1@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1@@1)) inline$$Vector_borrow$0$i_ind@1@@0))) (and (= $abort_flag@0@@3 false) (= inline$$Vector_borrow$0$dst@2@@0 inline$$Vector_borrow$0$dst@1@@0))) (and (=> (= (ControlFlow 0 33838) 33936) inline$$Option_borrow_with_default_$def_verify$0$anon28_Then_correct) (=> (= (ControlFlow 0 33838) 33912) inline$$Option_borrow_with_default_$def_verify$0$anon28_Else_correct)))))
649
(let ((inline$$Vector_borrow$0$anon0_correct@@0  (=> ((_ is $Vector) inline$$GetFieldFromValue$0$dst@1@@1) (=> (and ((_ is $Integer) inline$$Option_borrow_with_default_$def_verify$0$$t7@1) (= inline$$Vector_borrow$0$i_ind@1@@0 (|i#$Integer| inline$$Option_borrow_with_default_$def_verify$0$$t7@1))) (and (=> (= (ControlFlow 0 33812) 33896) inline$$Vector_borrow$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 33812) 33838) inline$$Vector_borrow$0$anon3_Else_correct@@0))))))
650
651
652
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon26_Else_correct  (=> (not (|b#$Boolean| inline$$Vector_is_empty$0$b@1)) (=> (and (= inline$$Option_borrow_with_default_$def_verify$0$$t7@1 ($Integer 0)) (= (ControlFlow 0 33904) 33812)) inline$$Vector_borrow$0$anon0_correct@@0))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon24_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 33678) 33996) inline$$Option_borrow_with_default_$def_verify$0$anon26_Then_correct) (=> (= (ControlFlow 0 33678) 33904) inline$$Option_borrow_with_default_$def_verify$0$anon26_Else_correct)))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon24_Then_correct true))
653
(let ((inline$$Vector_is_empty$0$anon0_correct  (=> (and ((_ is $Vector) inline$$GetFieldFromValue$0$dst@1@@1) (= inline$$Vector_is_empty$0$b@1 ($Boolean (= (|l#$ValueArray| (|v#$Vector| inline$$GetFieldFromValue$0$dst@1@@1)) 0)))) (and (=> (= (ControlFlow 0 33664) 34018) inline$$Option_borrow_with_default_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 33664) 33678) inline$$Option_borrow_with_default_$def_verify$0$anon24_Else_correct)))))
654
655
656
657
658
659
660
661
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon23_Else_correct  (=> (and (not true) (= (ControlFlow 0 33605) 33664)) inline$$Vector_is_empty$0$anon0_correct)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon23_Then_correct  (=> (= (ControlFlow 0 34042) 33664) inline$$Vector_is_empty$0$anon0_correct)))
(let ((inline$$GetFieldFromValue$0$anon0_correct@@1  (=> (= inline$$GetFieldFromValue$0$dst@1@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@3)) $Option_Option_vec)) (and (=> (= (ControlFlow 0 33591) 34042) inline$$Option_borrow_with_default_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 33591) 33605) inline$$Option_borrow_with_default_$def_verify$0$anon23_Else_correct)))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon22_Else_correct  (=> (and (not true) (= (ControlFlow 0 33481) 33591)) inline$$GetFieldFromValue$0$anon0_correct@@1)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon22_Then_correct  (=> (= (ControlFlow 0 34050) 33591) inline$$GetFieldFromValue$0$anon0_correct@@1)))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon21_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 33473) 34050) inline$$Option_borrow_with_default_$def_verify$0$anon22_Then_correct) (=> (= (ControlFlow 0 33473) 33481) inline$$Option_borrow_with_default_$def_verify$0$anon22_Else_correct)))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon21_Then_correct  (and (=> (= (ControlFlow 0 34058) 34050) inline$$Option_borrow_with_default_$def_verify$0$anon22_Then_correct) (=> (= (ControlFlow 0 34058) 33481) inline$$Option_borrow_with_default_$def_verify$0$anon22_Else_correct))))
(let ((inline$$Option_borrow_with_default_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 33467) 34058) inline$$Option_borrow_with_default_$def_verify$0$anon21_Then_correct) (=> (= (ControlFlow 0 33467) 33473) inline$$Option_borrow_with_default_$def_verify$0$anon21_Else_correct)))))
662
(let ((anon0$1_correct@@3  (=> (and (forall (($inv_addr@@3 Int) ($inv_tv0@@3 T@$TypeValue) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@3) 1) $inv_addr@@3)) (let ((va@@24 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@3) 1) $inv_addr@@3))))
663
664
(let ((l@@25 (|l#$ValueArray| va@@24)))
 (and (and (<= 0 l@@25) (<= l@@25 $MAX_U64)) (forall ((x@@24 Int) ) (!  (=> (or (< x@@24 0) (>= x@@24 l@@25)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@24) x@@24) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@24) x@@24))
665
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@3) 1) $inv_addr@@3))) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@3) 1) $inv_addr@@3))) $Option_Option_vec)) (let ((va@@25 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@3) 1) $inv_addr@@3))) $Option_Option_vec))))
666
667
668
669
(let ((l@@26 (|l#$ValueArray| va@@25)))
 (and (and (<= 0 l@@26) (<= l@@26 $MAX_U64)) (forall ((x@@25 Int) ) (!  (=> (or (< x@@25 0) (>= x@@25 l@@26)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@25) x@@25) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@25) x@@25))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@3) 1) $inv_addr@@3))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@3) 1) $inv_addr@@3))
)) (= (ControlFlow 0 34064) 33467)) inline$$Option_borrow_with_default_$def_verify$0$anon0_correct)))
670
(let ((anon0_correct@@3  (=> (and (and (and (and (and ((_ is $Vector) t@@3) (let ((va@@26 (|v#$Vector| t@@3)))
671
672
(let ((l@@27 (|l#$ValueArray| va@@26)))
 (and (and (<= 0 l@@27) (<= l@@27 $MAX_U64)) (forall ((x@@26 Int) ) (!  (=> (or (< x@@26 0) (>= x@@26 l@@27)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@26) x@@26) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@26) x@@26))
673
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@3)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@3)) $Option_Option_vec)) (let ((va@@27 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@3)) $Option_Option_vec))))
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
(let ((l@@28 (|l#$ValueArray| va@@27)))
 (and (and (<= 0 l@@28) (<= l@@28 $MAX_U64)) (forall ((x@@27 Int) ) (!  (=> (or (< x@@27 0) (>= x@@27 l@@28)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@27) x@@27) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@27) x@@27))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@3)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 33060) 34064)) anon0$1_correct@@3)))
(let ((PreconditionGeneratedEntry_correct@@3  (=> (= (ControlFlow 0 52106) 33060) anon0_correct@@3)))
PreconditionGeneratedEntry_correct@@3)))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $tv0@@5 () T@$TypeValue)
(declare-fun t@@4 () T@$Value)
(declare-fun $abort_flag@3@@2 () Bool)
(declare-fun $abort_code@6@@2 () Int)
(declare-fun $abort_flag@2@@3 () Bool)
(declare-fun $abort_code@4@@2 () Int)
(declare-fun $abort_code@5@@2 () Int)
(declare-fun $abort_code@1@@2 () Int)
(declare-fun $abort_flag@0@@4 () Bool)
(declare-fun $abort_code@2@@2 () Int)
(declare-fun $abort_flag@1@@3 () Bool)
(declare-fun inline$$Option_Option_unpack$0$vec@1 () T@$Value)
(declare-fun call4formal@$ret0@0@@2 () T@$Value)
(declare-fun $abort_code@3@@2 () Int)
(declare-fun call3formal@$ret0@0@@2 () T@$Value)
(declare-fun inline$$Option_destroy_none_$def_verify$0$$t6@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 52747) (let ((anon0$2_correct@@4  (and (=> (= (ControlFlow 0 35001) (- 0 53446)) (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@5 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec)) ($Integer 0))))))) $abort_flag@3@@2)) (=> (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@5 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec)) ($Integer 0))))))) $abort_flag@3@@2) (and (=> (= (ControlFlow 0 35001) (- 0 53457)) (=> $abort_flag@3@@2 (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@5 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec)) ($Integer 0))))))))) (=> (=> $abort_flag@3@@2 (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@5 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec)) ($Integer 0)))))))) (=> (= (ControlFlow 0 35001) (- 0 53468)) (=> $abort_flag@3@@2 (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@5 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec)) ($Integer 0))))))) (= $abort_code@6@@2 (|i#$Integer| ($Integer 7))))))))))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon29_Else_correct  (=> (and (and (not $abort_flag@2@@3) (= $abort_code@6@@2 $abort_code@4@@2)) (and (= $abort_flag@3@@2 $abort_flag@2@@3) (= (ControlFlow 0 34919) 35001))) anon0$2_correct@@4)))
(let ((inline$$Option_destroy_none_$def_verify$0$Abort_correct  (=> (= $abort_code@6@@2 $abort_code@5@@2) (=> (and (= $abort_flag@3@@2 true) (= (ControlFlow 0 34697) 35001)) anon0$2_correct@@4))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon5_correct  (=> (and (= $abort_code@5@@2 $abort_code@1@@2) (= (ControlFlow 0 34979) 34697)) inline$$Option_destroy_none_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon23_Else_correct  (=> (and (not true) (= (ControlFlow 0 34977) 34979)) inline$$Option_destroy_none_$def_verify$0$anon5_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon23_Then_correct  (=> (= (ControlFlow 0 34987) 34979) inline$$Option_destroy_none_$def_verify$0$anon5_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon22_Then_correct  (=> $abort_flag@0@@4 (and (=> (= (ControlFlow 0 34971) 34987) inline$$Option_destroy_none_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 34971) 34977) inline$$Option_destroy_none_$def_verify$0$anon23_Else_correct)))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon9_correct  (=> (and (= $abort_code@5@@2 $abort_code@2@@2) (= (ControlFlow 0 34959) 34697)) inline$$Option_destroy_none_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon25_Else_correct  (=> (and (not true) (= (ControlFlow 0 34957) 34959)) inline$$Option_destroy_none_$def_verify$0$anon9_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon25_Then_correct  (=> (= (ControlFlow 0 34967) 34959) inline$$Option_destroy_none_$def_verify$0$anon9_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon24_Then_correct  (=> $abort_flag@1@@3 (and (=> (= (ControlFlow 0 34951) 34967) inline$$Option_destroy_none_$def_verify$0$anon25_Then_correct) (=> (= (ControlFlow 0 34951) 34957) inline$$Option_destroy_none_$def_verify$0$anon25_Else_correct)))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon19_correct  (=> (and (= $abort_code@5@@2 $abort_code@4@@2) (= (ControlFlow 0 34931) 34697)) inline$$Option_destroy_none_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon30_Else_correct  (=> (and (not true) (= (ControlFlow 0 34929) 34931)) inline$$Option_destroy_none_$def_verify$0$anon19_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon30_Then_correct  (=> (= (ControlFlow 0 34939) 34931) inline$$Option_destroy_none_$def_verify$0$anon19_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon29_Then_correct  (=> $abort_flag@2@@3 (and (=> (= (ControlFlow 0 34923) 34939) inline$$Option_destroy_none_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 34923) 34929) inline$$Option_destroy_none_$def_verify$0$anon30_Else_correct)))))
(let ((inline$$Vector_destroy_empty$0$anon2_Then$1_correct  (=> (and (= $abort_flag@2@@3 true) (= $abort_code@4@@2 $EXEC_FAILURE_CODE)) (and (=> (= (ControlFlow 0 34907) 34923) inline$$Option_destroy_none_$def_verify$0$anon29_Then_correct) (=> (= (ControlFlow 0 34907) 34919) inline$$Option_destroy_none_$def_verify$0$anon29_Else_correct)))))
(let ((inline$$Vector_destroy_empty$0$anon2_Then_correct  (=> (and (not (= (|l#$ValueArray| (|v#$Vector| inline$$Option_Option_unpack$0$vec@1)) 0)) (= (ControlFlow 0 34905) 34907)) inline$$Vector_destroy_empty$0$anon2_Then$1_correct)))
(let ((inline$$Vector_destroy_empty$0$anon2_Else_correct  (=> (= (|l#$ValueArray| (|v#$Vector| inline$$Option_Option_unpack$0$vec@1)) 0) (=> (and (= $abort_flag@2@@3 $abort_flag@1@@3) (= $abort_code@4@@2 $abort_code@2@@2)) (and (=> (= (ControlFlow 0 34855) 34923) inline$$Option_destroy_none_$def_verify$0$anon29_Then_correct) (=> (= (ControlFlow 0 34855) 34919) inline$$Option_destroy_none_$def_verify$0$anon29_Else_correct))))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon28_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 34782) 34905) inline$$Vector_destroy_empty$0$anon2_Then_correct) (=> (= (ControlFlow 0 34782) 34855) inline$$Vector_destroy_empty$0$anon2_Else_correct)))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon28_Then_correct  (and (=> (= (ControlFlow 0 34947) 34905) inline$$Vector_destroy_empty$0$anon2_Then_correct) (=> (= (ControlFlow 0 34947) 34855) inline$$Vector_destroy_empty$0$anon2_Else_correct))))
721
(let ((inline$$Option_Option_unpack$0$anon0_correct  (=> (and (and ((_ is $Vector) t@@4) (= inline$$Option_Option_unpack$0$vec@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec))) (and ((_ is $Vector) inline$$Option_Option_unpack$0$vec@1) (let ((va@@28 (|v#$Vector| inline$$Option_Option_unpack$0$vec@1)))
722
723
724
725
726
727
728
729
730
(let ((l@@29 (|l#$ValueArray| va@@28)))
 (and (and (<= 0 l@@29) (<= l@@29 $MAX_U64)) (forall ((x@@28 Int) ) (!  (=> (or (< x@@28 0) (>= x@@28 l@@29)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@28) x@@28) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@28) x@@28))
))))))) (and (=> (= (ControlFlow 0 34768) 34947) inline$$Option_destroy_none_$def_verify$0$anon28_Then_correct) (=> (= (ControlFlow 0 34768) 34782) inline$$Option_destroy_none_$def_verify$0$anon28_Else_correct)))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon26_Then_correct  (=> (and (|b#$Boolean| call4formal@$ret0@0@@2) (= (ControlFlow 0 34774) 34768)) inline$$Option_Option_unpack$0$anon0_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon14_correct  (=> (and (= $abort_code@5@@2 $abort_code@3@@2) (= (ControlFlow 0 34693) 34697)) inline$$Option_destroy_none_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon27_Else_correct  (=> (and (not true) (= (ControlFlow 0 34691) 34693)) inline$$Option_destroy_none_$def_verify$0$anon14_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon27_Then_correct  (=> (= (ControlFlow 0 34705) 34693) inline$$Option_destroy_none_$def_verify$0$anon14_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon26_Else_correct  (=> (and (not (|b#$Boolean| call4formal@$ret0@0@@2)) (= $abort_code@3@@2 (|i#$Integer| call3formal@$ret0@0@@2))) (and (=> (= (ControlFlow 0 34685) 34705) inline$$Option_destroy_none_$def_verify$0$anon27_Then_correct) (=> (= (ControlFlow 0 34685) 34691) inline$$Option_destroy_none_$def_verify$0$anon27_Else_correct)))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon24_Else_correct  (=> (not $abort_flag@1@@3) (and (=> (= (ControlFlow 0 34673) 34774) inline$$Option_destroy_none_$def_verify$0$anon26_Then_correct) (=> (= (ControlFlow 0 34673) 34685) inline$$Option_destroy_none_$def_verify$0$anon26_Else_correct)))))
731
732
(let ((inline$$Option_destroy_none_$def_verify$0$anon22_Else_correct  (=> (not $abort_flag@0@@4) (=> (and (and (and (= inline$$Option_destroy_none_$def_verify$0$$t6@1 ($Integer 0)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@1@@3)) (and (=> $abort_flag@1@@3 (|b#$Boolean| ($Boolean false))) (=> (not $abort_flag@1@@3) (|b#$Boolean| ($Boolean ($IsEqual_stratified call3formal@$ret0@0@@2 ($Integer 7))))))) (and (and ((_ is $Integer) call3formal@$ret0@0@@2) (>= (|i#$Integer| call3formal@$ret0@0@@2) 0)) (<= (|i#$Integer| call3formal@$ret0@0@@2) $MAX_U64))) (and (=> (= (ControlFlow 0 34667) 34951) inline$$Option_destroy_none_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 34667) 34673) inline$$Option_destroy_none_$def_verify$0$anon24_Else_correct))))))
(let ((inline$$Option_destroy_none_$def_verify$0$anon2$1_correct  (=> (and (and (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@4) (=> $abort_flag@0@@4 (|b#$Boolean| ($Boolean false)))) (and (=> (not $abort_flag@0@@4) (|b#$Boolean| ($Boolean ($IsEqual_stratified call4formal@$ret0@0@@2 ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@5 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec)) ($Integer 0))))))) ((_ is $Boolean) call4formal@$ret0@0@@2))) (and (=> (= (ControlFlow 0 34657) 34971) inline$$Option_destroy_none_$def_verify$0$anon22_Then_correct) (=> (= (ControlFlow 0 34657) 34667) inline$$Option_destroy_none_$def_verify$0$anon22_Else_correct)))))
733
734
735
(let ((inline$$Option_destroy_none_$def_verify$0$anon21_Else_correct  (=> (and (not true) (= (ControlFlow 0 34621) 34657)) inline$$Option_destroy_none_$def_verify$0$anon2$1_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon21_Then_correct  (=> (= (ControlFlow 0 34995) 34657) inline$$Option_destroy_none_$def_verify$0$anon2$1_correct)))
(let ((inline$$Option_destroy_none_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 34615) 34995) inline$$Option_destroy_none_$def_verify$0$anon21_Then_correct) (=> (= (ControlFlow 0 34615) 34621) inline$$Option_destroy_none_$def_verify$0$anon21_Else_correct)))))
736
(let ((anon0$1_correct@@4  (=> (and (forall (($inv_addr@@4 Int) ($inv_tv0@@4 T@$TypeValue) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@4) 1) $inv_addr@@4)) (let ((va@@29 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@4) 1) $inv_addr@@4))))
737
738
(let ((l@@30 (|l#$ValueArray| va@@29)))
 (and (and (<= 0 l@@30) (<= l@@30 $MAX_U64)) (forall ((x@@29 Int) ) (!  (=> (or (< x@@29 0) (>= x@@29 l@@30)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@29) x@@29) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@29) x@@29))
739
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@4) 1) $inv_addr@@4))) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@4) 1) $inv_addr@@4))) $Option_Option_vec)) (let ((va@@30 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@4) 1) $inv_addr@@4))) $Option_Option_vec))))
740
741
742
743
(let ((l@@31 (|l#$ValueArray| va@@30)))
 (and (and (<= 0 l@@31) (<= l@@31 $MAX_U64)) (forall ((x@@30 Int) ) (!  (=> (or (< x@@30 0) (>= x@@30 l@@31)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@30) x@@30) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@30) x@@30))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@4) 1) $inv_addr@@4))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@4) 1) $inv_addr@@4))
)) (= (ControlFlow 0 34999) 34615)) inline$$Option_destroy_none_$def_verify$0$anon0_correct)))
744
(let ((anon0_correct@@4  (=> (and (and (and (and (and ((_ is $Vector) t@@4) (let ((va@@31 (|v#$Vector| t@@4)))
745
746
(let ((l@@32 (|l#$ValueArray| va@@31)))
 (and (and (<= 0 l@@32) (<= l@@32 $MAX_U64)) (forall ((x@@31 Int) ) (!  (=> (or (< x@@31 0) (>= x@@31 l@@32)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@31) x@@31) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@31) x@@31))
747
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@4)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec)) (let ((va@@32 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec))))
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
(let ((l@@33 (|l#$ValueArray| va@@32)))
 (and (and (<= 0 l@@33) (<= l@@33 $MAX_U64)) (forall ((x@@32 Int) ) (!  (=> (or (< x@@32 0) (>= x@@32 l@@33)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@32) x@@32) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@32) x@@32))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@4)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 34238) 34999)) anon0$1_correct@@4)))
(let ((PreconditionGeneratedEntry_correct@@4  (=> (= (ControlFlow 0 52747) 34238) anon0_correct@@4)))
PreconditionGeneratedEntry_correct@@4))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $tv0@@6 () T@$TypeValue)
(declare-fun t@@5 () T@$Value)
(declare-fun $abort_flag@4 () Bool)
(declare-fun $abort_code@7 () Int)
(declare-fun inline$$Option_destroy_some_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun inline$$Vector_pop_back$0$e@2@@0 () T@$Value)
(declare-fun $abort_flag@3@@3 () Bool)
(declare-fun $abort_code@5@@3 () Int)
(declare-fun inline$$Option_destroy_some_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun $abort_code@6@@3 () Int)
(declare-fun $abort_code@1@@3 () Int)
(declare-fun $abort_flag@0@@5 () Bool)
(declare-fun $abort_code@2@@3 () Int)
(declare-fun $abort_flag@1@@4 () Bool)
(declare-fun $abort_code@4@@3 () Int)
(declare-fun $abort_flag@2@@4 () Bool)
(declare-fun |inline$$WritebackToValue$0$vdst'@2@@1| () T@$Value)
(declare-fun |inline$$WriteRef$0$to'@1@@1| () T@$Mutation)
(declare-fun inline$$Option_Option_unpack$0$vec@1@@0 () T@$Value)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@1| () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@1 () T@$Mutation)
(declare-fun |inline$$Vector_pop_back$0$v'@2@@0| () T@$Value)
(declare-fun inline$$Vector_pop_back$0$e@0@@0 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@0@@0| () T@$Value)
(declare-fun inline$$Vector_pop_back$0$len@1@@0 () Int)
(declare-fun inline$$Vector_pop_back$0$e@1@@0 () T@$Value)
(declare-fun inline$$ReadRef$0$v@1@@1 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@1@@0| () T@$Value)
(declare-fun call4formal@$ret0@0@@3 () T@$Value)
(declare-fun $abort_code@3@@3 () Int)
(declare-fun call3formal@$ret0@0@@3 () T@$Value)
(declare-fun inline$$Option_destroy_some_$def_verify$0$$t7@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 53496) (let ((anon0$2_correct@@5  (and (=> (= (ControlFlow 0 36572) (- 0 54609)) (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@4)) (=> (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@4) (and (=> (= (ControlFlow 0 36572) (- 0 54620)) (=> $abort_flag@4 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) ($Integer 0)))))) (=> (=> $abort_flag@4 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) ($Integer 0))))) (and (=> (= (ControlFlow 0 36572) (- 0 54631)) (=> $abort_flag@4 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@7 (|i#$Integer| ($Integer 7)))))) (=> (=> $abort_flag@4 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@7 (|i#$Integer| ($Integer 7))))) (=> (= (ControlFlow 0 36572) (- 0 54653)) (=> (not $abort_flag@4) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_destroy_some_$def_verify$0$$ret0@2 ($Vector_$borrow $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec) ($Integer 0)))))))))))))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon28_correct  (=> (and (and (= inline$$Option_destroy_some_$def_verify$0$$ret0@2 inline$$Vector_pop_back$0$e@2@@0) (= $abort_flag@4 $abort_flag@3@@3)) (and (= $abort_code@7 $abort_code@5@@3) (= (ControlFlow 0 36452) 36572))) anon0$2_correct@@5)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon42_Else_correct  (=> (and (not true) (= (ControlFlow 0 36450) 36452)) inline$$Option_destroy_some_$def_verify$0$anon28_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon42_Then_correct  (=> (= (ControlFlow 0 36460) 36452) inline$$Option_destroy_some_$def_verify$0$anon28_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon40_Else_correct  (=> (not $abort_flag@3@@3) (and (=> (= (ControlFlow 0 36444) 36460) inline$$Option_destroy_some_$def_verify$0$anon42_Then_correct) (=> (= (ControlFlow 0 36444) 36450) inline$$Option_destroy_some_$def_verify$0$anon42_Else_correct)))))
(let ((inline$$Option_destroy_some_$def_verify$0$Abort_correct  (=> (= inline$$Option_destroy_some_$def_verify$0$$ret0@1 $Error) (=> (and (and (= inline$$Option_destroy_some_$def_verify$0$$ret0@2 inline$$Option_destroy_some_$def_verify$0$$ret0@1) (= $abort_flag@4 true)) (and (= $abort_code@7 $abort_code@6@@3) (= (ControlFlow 0 35709) 36572))) anon0$2_correct@@5))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon5_correct  (=> (and (= $abort_code@6@@3 $abort_code@1@@3) (= (ControlFlow 0 36548) 35709)) inline$$Option_destroy_some_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon31_Else_correct  (=> (and (not true) (= (ControlFlow 0 36546) 36548)) inline$$Option_destroy_some_$def_verify$0$anon5_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon31_Then_correct  (=> (= (ControlFlow 0 36556) 36548) inline$$Option_destroy_some_$def_verify$0$anon5_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon30_Then_correct  (=> $abort_flag@0@@5 (and (=> (= (ControlFlow 0 36540) 36556) inline$$Option_destroy_some_$def_verify$0$anon31_Then_correct) (=> (= (ControlFlow 0 36540) 36546) inline$$Option_destroy_some_$def_verify$0$anon31_Else_correct)))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon9_correct  (=> (and (= $abort_code@6@@3 $abort_code@2@@3) (= (ControlFlow 0 36528) 35709)) inline$$Option_destroy_some_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon33_Else_correct  (=> (and (not true) (= (ControlFlow 0 36526) 36528)) inline$$Option_destroy_some_$def_verify$0$anon9_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon33_Then_correct  (=> (= (ControlFlow 0 36536) 36528) inline$$Option_destroy_some_$def_verify$0$anon9_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon32_Then_correct  (=> $abort_flag@1@@4 (and (=> (= (ControlFlow 0 36520) 36536) inline$$Option_destroy_some_$def_verify$0$anon33_Then_correct) (=> (= (ControlFlow 0 36520) 36526) inline$$Option_destroy_some_$def_verify$0$anon33_Else_correct)))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon19_correct  (=> (and (= $abort_code@6@@3 $abort_code@4@@3) (= (ControlFlow 0 36500) 35709)) inline$$Option_destroy_some_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon38_Else_correct  (=> (and (not true) (= (ControlFlow 0 36498) 36500)) inline$$Option_destroy_some_$def_verify$0$anon19_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon38_Then_correct  (=> (= (ControlFlow 0 36508) 36500) inline$$Option_destroy_some_$def_verify$0$anon19_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon37_Then_correct  (=> $abort_flag@2@@4 (and (=> (= (ControlFlow 0 36492) 36508) inline$$Option_destroy_some_$def_verify$0$anon38_Then_correct) (=> (= (ControlFlow 0 36492) 36498) inline$$Option_destroy_some_$def_verify$0$anon38_Else_correct)))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon25_correct  (=> (and (= $abort_code@6@@3 $abort_code@5@@3) (= (ControlFlow 0 36472) 35709)) inline$$Option_destroy_some_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon41_Else_correct  (=> (and (not true) (= (ControlFlow 0 36470) 36472)) inline$$Option_destroy_some_$def_verify$0$anon25_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon41_Then_correct  (=> (= (ControlFlow 0 36480) 36472) inline$$Option_destroy_some_$def_verify$0$anon25_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon40_Then_correct  (=> $abort_flag@3@@3 (and (=> (= (ControlFlow 0 36464) 36480) inline$$Option_destroy_some_$def_verify$0$anon41_Then_correct) (=> (= (ControlFlow 0 36464) 36470) inline$$Option_destroy_some_$def_verify$0$anon41_Else_correct)))))
(let ((inline$$Vector_destroy_empty$0$anon2_Then$1_correct@@0  (=> (and (= $abort_code@5@@3 $EXEC_FAILURE_CODE) (= $abort_flag@3@@3 true)) (and (=> (= (ControlFlow 0 36430) 36464) inline$$Option_destroy_some_$def_verify$0$anon40_Then_correct) (=> (= (ControlFlow 0 36430) 36444) inline$$Option_destroy_some_$def_verify$0$anon40_Else_correct)))))
(let ((inline$$Vector_destroy_empty$0$anon2_Then_correct@@0  (=> (and (not (= (|l#$ValueArray| (|v#$Vector| |inline$$WritebackToValue$0$vdst'@2@@1|)) 0)) (= (ControlFlow 0 36428) 36430)) inline$$Vector_destroy_empty$0$anon2_Then$1_correct@@0)))
(let ((inline$$Vector_destroy_empty$0$anon2_Else_correct@@0  (=> (= (|l#$ValueArray| (|v#$Vector| |inline$$WritebackToValue$0$vdst'@2@@1|)) 0) (=> (and (= $abort_code@5@@3 $abort_code@4@@3) (= $abort_flag@3@@3 $abort_flag@2@@4)) (and (=> (= (ControlFlow 0 36378) 36464) inline$$Option_destroy_some_$def_verify$0$anon40_Then_correct) (=> (= (ControlFlow 0 36378) 36444) inline$$Option_destroy_some_$def_verify$0$anon40_Else_correct))))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon39_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 36305) 36428) inline$$Vector_destroy_empty$0$anon2_Then_correct@@0) (=> (= (ControlFlow 0 36305) 36378) inline$$Vector_destroy_empty$0$anon2_Else_correct@@0)))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon39_Then_correct  (and (=> (= (ControlFlow 0 36488) 36428) inline$$Vector_destroy_empty$0$anon2_Then_correct@@0) (=> (= (ControlFlow 0 36488) 36378) inline$$Vector_destroy_empty$0$anon2_Else_correct@@0))))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@1  (=> (and (not (= (|l#$Mutation| |inline$$WriteRef$0$to'@1@@1|) ($Local 4))) (= |inline$$WritebackToValue$0$vdst'@2@@1| inline$$Option_Option_unpack$0$vec@1@@0)) (and (=> (= (ControlFlow 0 36231) 36488) inline$$Option_destroy_some_$def_verify$0$anon39_Then_correct) (=> (= (ControlFlow 0 36231) 36305) inline$$Option_destroy_some_$def_verify$0$anon39_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@1  (=> (= (|l#$Mutation| |inline$$WriteRef$0$to'@1@@1|) ($Local 4)) (=> (and (= |inline$$WritebackToValue$0$vdst'@1@@1| ($UpdateValue_stratified (|p#$Mutation| |inline$$WriteRef$0$to'@1@@1|) 0 inline$$Option_Option_unpack$0$vec@1@@0 (|v#$Mutation| |inline$$WriteRef$0$to'@1@@1|))) (= |inline$$WritebackToValue$0$vdst'@2@@1| |inline$$WritebackToValue$0$vdst'@1@@1|)) (and (=> (= (ControlFlow 0 36257) 36488) inline$$Option_destroy_some_$def_verify$0$anon39_Then_correct) (=> (= (ControlFlow 0 36257) 36305) inline$$Option_destroy_some_$def_verify$0$anon39_Else_correct))))))
(let ((inline$$WriteRef$0$anon0_correct@@1  (=> (= |inline$$WriteRef$0$to'@1@@1| ($Mutation (|l#$Mutation| inline$$BorrowLoc$0$dst@1@@1) (|p#$Mutation| inline$$BorrowLoc$0$dst@1@@1) |inline$$Vector_pop_back$0$v'@2@@0|)) (and (=> (= (ControlFlow 0 36132) 36257) inline$$WritebackToValue$0$anon3_Then_correct@@1) (=> (= (ControlFlow 0 36132) 36231) inline$$WritebackToValue$0$anon3_Else_correct@@1)))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon37_Else_correct  (=> (and (not $abort_flag@2@@4) (= (ControlFlow 0 36138) 36132)) inline$$WriteRef$0$anon0_correct@@1)))
(let ((inline$$Vector_pop_back$0$anon3_Then$1_correct@@0  (=> (and (and (= $abort_flag@2@@4 true) (= $abort_code@4@@3 $EXEC_FAILURE_CODE)) (and (= inline$$Vector_pop_back$0$e@2@@0 inline$$Vector_pop_back$0$e@0@@0) (= |inline$$Vector_pop_back$0$v'@2@@0| |inline$$Vector_pop_back$0$v'@0@@0|))) (and (=> (= (ControlFlow 0 36065) 36492) inline$$Option_destroy_some_$def_verify$0$anon37_Then_correct) (=> (= (ControlFlow 0 36065) 36138) inline$$Option_destroy_some_$def_verify$0$anon37_Else_correct)))))
(let ((inline$$Vector_pop_back$0$anon3_Then_correct@@0  (=> (and (= inline$$Vector_pop_back$0$len@1@@0 0) (= (ControlFlow 0 36063) 36065)) inline$$Vector_pop_back$0$anon3_Then$1_correct@@0)))
(let ((inline$$Vector_pop_back$0$anon3_Else_correct@@0  (=> (not (= inline$$Vector_pop_back$0$len@1@@0 0)) (=> (and (= inline$$Vector_pop_back$0$e@1@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@1)) (- inline$$Vector_pop_back$0$len@1@@0 1))) (= |inline$$Vector_pop_back$0$v'@1@@0| ($Vector (let ((l@@34 (- (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@1)) 1)))
($ValueArray (|lambda#0| 0 l@@34 (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@1)) $Error) l@@34))))) (=> (and (and (= $abort_flag@2@@4 $abort_flag@1@@4) (= $abort_code@4@@3 $abort_code@2@@3)) (and (= inline$$Vector_pop_back$0$e@2@@0 inline$$Vector_pop_back$0$e@1@@0) (= |inline$$Vector_pop_back$0$v'@2@@0| |inline$$Vector_pop_back$0$v'@1@@0|))) (and (=> (= (ControlFlow 0 36015) 36492) inline$$Option_destroy_some_$def_verify$0$anon37_Then_correct) (=> (= (ControlFlow 0 36015) 36138) inline$$Option_destroy_some_$def_verify$0$anon37_Else_correct)))))))
826
(let ((inline$$Vector_pop_back$0$anon0_correct@@0  (=> (and ((_ is $Vector) inline$$ReadRef$0$v@1@@1) (= inline$$Vector_pop_back$0$len@1@@0 (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@1)))) (and (=> (= (ControlFlow 0 35993) 36063) inline$$Vector_pop_back$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 35993) 36015) inline$$Vector_pop_back$0$anon3_Else_correct@@0)))))
827
828
829
830
(let ((inline$$ReadRef$0$anon0_correct@@1  (=> (and (= inline$$ReadRef$0$v@1@@1 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@1)) (= (ControlFlow 0 35882) 35993)) inline$$Vector_pop_back$0$anon0_correct@@0)))
(let ((inline$$BorrowLoc$0$anon0_correct@@1  (=> (and (= inline$$BorrowLoc$0$dst@1@@1 ($Mutation ($Local 4) $EmptyPath inline$$Option_Option_unpack$0$vec@1@@0)) (= (ControlFlow 0 35844) 35882)) inline$$ReadRef$0$anon0_correct@@1)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon36_Else_correct  (=> (and (not true) (= (ControlFlow 0 35794) 35844)) inline$$BorrowLoc$0$anon0_correct@@1)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon36_Then_correct  (=> (= (ControlFlow 0 36516) 35844) inline$$BorrowLoc$0$anon0_correct@@1)))
831
(let ((inline$$Option_Option_unpack$0$anon0_correct@@0  (=> (and (and ((_ is $Vector) t@@5) (= inline$$Option_Option_unpack$0$vec@1@@0 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec))) (and ((_ is $Vector) inline$$Option_Option_unpack$0$vec@1@@0) (let ((va@@33 (|v#$Vector| inline$$Option_Option_unpack$0$vec@1@@0)))
832
833
834
835
836
837
838
839
840
(let ((l@@35 (|l#$ValueArray| va@@33)))
 (and (and (<= 0 l@@35) (<= l@@35 $MAX_U64)) (forall ((x@@33 Int) ) (!  (=> (or (< x@@33 0) (>= x@@33 l@@35)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@33) x@@33) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@33) x@@33))
))))))) (and (=> (= (ControlFlow 0 35780) 36516) inline$$Option_destroy_some_$def_verify$0$anon36_Then_correct) (=> (= (ControlFlow 0 35780) 35794) inline$$Option_destroy_some_$def_verify$0$anon36_Else_correct)))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon34_Then_correct  (=> (and (|b#$Boolean| call4formal@$ret0@0@@3) (= (ControlFlow 0 35786) 35780)) inline$$Option_Option_unpack$0$anon0_correct@@0)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon14_correct  (=> (and (= $abort_code@6@@3 $abort_code@3@@3) (= (ControlFlow 0 35703) 35709)) inline$$Option_destroy_some_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon35_Else_correct  (=> (and (not true) (= (ControlFlow 0 35701) 35703)) inline$$Option_destroy_some_$def_verify$0$anon14_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon35_Then_correct  (=> (= (ControlFlow 0 35717) 35703) inline$$Option_destroy_some_$def_verify$0$anon14_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon34_Else_correct  (=> (and (not (|b#$Boolean| call4formal@$ret0@0@@3)) (= $abort_code@3@@3 (|i#$Integer| call3formal@$ret0@0@@3))) (and (=> (= (ControlFlow 0 35695) 35717) inline$$Option_destroy_some_$def_verify$0$anon35_Then_correct) (=> (= (ControlFlow 0 35695) 35701) inline$$Option_destroy_some_$def_verify$0$anon35_Else_correct)))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon32_Else_correct  (=> (not $abort_flag@1@@4) (and (=> (= (ControlFlow 0 35683) 35786) inline$$Option_destroy_some_$def_verify$0$anon34_Then_correct) (=> (= (ControlFlow 0 35683) 35695) inline$$Option_destroy_some_$def_verify$0$anon34_Else_correct)))))
841
842
(let ((inline$$Option_destroy_some_$def_verify$0$anon30_Else_correct  (=> (not $abort_flag@0@@5) (=> (and (and (and (= inline$$Option_destroy_some_$def_verify$0$$t7@1 ($Integer 1)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@1@@4)) (and (=> $abort_flag@1@@4 (|b#$Boolean| ($Boolean false))) (=> (not $abort_flag@1@@4) (|b#$Boolean| ($Boolean ($IsEqual_stratified call3formal@$ret0@0@@3 ($Integer 7))))))) (and (and ((_ is $Integer) call3formal@$ret0@0@@3) (>= (|i#$Integer| call3formal@$ret0@0@@3) 0)) (<= (|i#$Integer| call3formal@$ret0@0@@3) $MAX_U64))) (and (=> (= (ControlFlow 0 35677) 36520) inline$$Option_destroy_some_$def_verify$0$anon32_Then_correct) (=> (= (ControlFlow 0 35677) 35683) inline$$Option_destroy_some_$def_verify$0$anon32_Else_correct))))))
(let ((inline$$Option_destroy_some_$def_verify$0$anon2$1_correct  (=> (and (and (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@5) (=> $abort_flag@0@@5 (|b#$Boolean| ($Boolean false)))) (and (=> (not $abort_flag@0@@5) (|b#$Boolean| ($Boolean ($IsEqual_stratified call4formal@$ret0@0@@3 ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@6 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) ($Integer 0)))))))))) ((_ is $Boolean) call4formal@$ret0@0@@3))) (and (=> (= (ControlFlow 0 35667) 36540) inline$$Option_destroy_some_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 35667) 35677) inline$$Option_destroy_some_$def_verify$0$anon30_Else_correct)))))
843
844
845
(let ((inline$$Option_destroy_some_$def_verify$0$anon29_Else_correct  (=> (and (not true) (= (ControlFlow 0 35631) 35667)) inline$$Option_destroy_some_$def_verify$0$anon2$1_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon29_Then_correct  (=> (= (ControlFlow 0 36564) 35667) inline$$Option_destroy_some_$def_verify$0$anon2$1_correct)))
(let ((inline$$Option_destroy_some_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 35625) 36564) inline$$Option_destroy_some_$def_verify$0$anon29_Then_correct) (=> (= (ControlFlow 0 35625) 35631) inline$$Option_destroy_some_$def_verify$0$anon29_Else_correct)))))
846
(let ((anon0$1_correct@@5  (=> (and (forall (($inv_addr@@5 Int) ($inv_tv0@@5 T@$TypeValue) ) (!  (and (and (and (and ((_ is $Vector) (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@5) 1) $inv_addr@@5)) (let ((va@@34 (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@5) 1) $inv_addr@@5))))
847
848
(let ((l@@36 (|l#$ValueArray| va@@34)))
 (and (and (<= 0 l@@36) (<= l@@36 $MAX_U64)) (forall ((x@@34 Int) ) (!  (=> (or (< x@@34 0) (>= x@@34 l@@36)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@34) x@@34) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@34) x@@34))
849
)))))) (= (|l#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@5) 1) $inv_addr@@5))) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@5) 1) $inv_addr@@5))) $Option_Option_vec)) (let ((va@@35 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@5) 1) $inv_addr@@5))) $Option_Option_vec))))
850
851
852
853
(let ((l@@37 (|l#$ValueArray| va@@35)))
 (and (and (<= 0 l@@37) (<= l@@37 $MAX_U64)) (forall ((x@@35 Int) ) (!  (=> (or (< x@@35 0) (>= x@@35 l@@37)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@35) x@@35) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@35) x@@35))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@5) 1) $inv_addr@@5))) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) :pattern ( (|Select_[$TypeValueArray,$int]$Value| (|contents#$Memory| $Option_Option_$memory) ($TypeValueArray (|Store_[$int]$TypeValue| ($MapConstTypeValue $ErrorType) 0 $inv_tv0@@5) 1) $inv_addr@@5))
)) (= (ControlFlow 0 36570) 35625)) inline$$Option_destroy_some_$def_verify$0$anon0_correct)))
854
(let ((anon0_correct@@5  (=> (and (and (and (and (and ((_ is $Vector) t@@5) (let ((va@@36 (|v#$Vector| t@@5)))
855
856
(let ((l@@38 (|l#$ValueArray| va@@36)))
 (and (and (<= 0 l@@38) (<= l@@38 $MAX_U64)) (forall ((x@@36 Int) ) (!  (=> (or (< x@@36 0) (>= x@@36 l@@38)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@36) x@@36) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@36) x@@36))
857
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@5)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec)) (let ((va@@37 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec))))
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
(let ((l@@39 (|l#$ValueArray| va@@37)))
 (and (and (<= 0 l@@39) (<= l@@39 $MAX_U64)) (forall ((x@@37 Int) ) (!  (=> (or (< x@@37 0) (>= x@@37 l@@39)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@37) x@@37) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@37) x@@37))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@5)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 35110) 36570)) anon0$1_correct@@5)))
(let ((PreconditionGeneratedEntry_correct@@5  (=> (= (ControlFlow 0 53496) 35110) anon0_correct@@5)))
PreconditionGeneratedEntry_correct@@5)))))))))))))))))))))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $abort_flag@2@@5 () Bool)
(declare-fun inline$$Option_destroy_with_default_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun $tv0@@7 () T@$TypeValue)
(declare-fun t@@6 () T@$Value)
(declare-fun q@default () T@$Value)
(declare-fun inline$$Option_destroy_with_default_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun $abort_flag@0@@6 () Bool)
(declare-fun $abort_flag@1@@5 () Bool)
(declare-fun |inline$$Option_destroy_with_default_$def_verify$0$tmp#$2@1| () T@$Value)
(declare-fun inline$$Vector_is_empty$0$b@1@@0 () T@$Value)
(declare-fun inline$$Vector_pop_back$0$e@2@@1 () T@$Value)
(declare-fun |inline$$WriteRef$0$to'@1@@2| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@2| () T@$Value)
(declare-fun inline$$Option_Option_unpack$0$vec@1@@1 () T@$Value)
(declare-fun inline$$BorrowLoc$1$dst@1 () T@$Mutation)
(declare-fun |inline$$Vector_pop_back$0$v'@2@@1| () T@$Value)
(declare-fun inline$$Vector_pop_back$0$e@0@@1 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@0@@1| () T@$Value)
(declare-fun inline$$Vector_pop_back$0$len@1@@1 () Int)
(declare-fun inline$$Vector_pop_back$0$e@1@@1 () T@$Value)
(declare-fun inline$$ReadRef$1$v@1@@1 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@1@@1| () T@$Value)
(declare-fun inline$$ReadRef$0$v@1@@2 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@2 () T@$Mutation)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 54678) (let ((anon0$2_correct@@6  (and (=> (= (ControlFlow 0 38195) (- 0 55457)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@2@@5)) (=> (=> (|b#$Boolean| ($Boolean false)) $abort_flag@2@@5) (and (=> (= (ControlFlow 0 38195) (- 0 55466)) (=> $abort_flag@2@@5 (|b#$Boolean| ($Boolean false)))) (=> (=> $abort_flag@2@@5 (|b#$Boolean| ($Boolean false))) (=> (= (ControlFlow 0 38195) (- 0 55475)) (=> (not $abort_flag@2@@5) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_destroy_with_default_$def_verify$0$$ret0@2 (ite (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@7 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@6)) $Option_Option_vec)) ($Integer 0))))))) ($Vector_$borrow $tv0@@7 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@6)) $Option_Option_vec) ($Integer 0)) q@default))))))))))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$Abort_correct  (=> (and (and (= inline$$Option_destroy_with_default_$def_verify$0$$ret0@1 $Error) (= $abort_flag@2@@5 true)) (and (= inline$$Option_destroy_with_default_$def_verify$0$$ret0@2 inline$$Option_destroy_with_default_$def_verify$0$$ret0@1) (= (ControlFlow 0 38079) 38195))) anon0$2_correct@@6)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon31_Else_correct  (=> (and (not true) (= (ControlFlow 0 38071) 38079)) inline$$Option_destroy_with_default_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon31_Then_correct  (=> (= (ControlFlow 0 38087) 38079) inline$$Option_destroy_with_default_$def_verify$0$Abort_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon30_Then_correct  (=> $abort_flag@0@@6 (and (=> (= (ControlFlow 0 38065) 38087) inline$$Option_destroy_with_default_$def_verify$0$anon31_Then_correct) (=> (= (ControlFlow 0 38065) 38071) inline$$Option_destroy_with_default_$def_verify$0$anon31_Else_correct)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon22_correct  (=> (= $abort_flag@2@@5 $abort_flag@1@@5) (=> (and (= inline$$Option_destroy_with_default_$def_verify$0$$ret0@2 |inline$$Option_destroy_with_default_$def_verify$0$tmp#$2@1|) (= (ControlFlow 0 38045) 38195)) anon0$2_correct@@6))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon33_Else_correct  (=> (and (not true) (= (ControlFlow 0 38043) 38045)) inline$$Option_destroy_with_default_$def_verify$0$anon22_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon33_Then_correct  (=> (= (ControlFlow 0 38053) 38045) inline$$Option_destroy_with_default_$def_verify$0$anon22_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon14_correct  (=> (and (= $abort_flag@1@@5 false) (= |inline$$Option_destroy_with_default_$def_verify$0$tmp#$2@1| q@default)) (and (=> (= (ControlFlow 0 38135) 38053) inline$$Option_destroy_with_default_$def_verify$0$anon33_Then_correct) (=> (= (ControlFlow 0 38135) 38043) inline$$Option_destroy_with_default_$def_verify$0$anon33_Else_correct)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon29_Else_correct  (=> (and (not true) (= (ControlFlow 0 38133) 38135)) inline$$Option_destroy_with_default_$def_verify$0$anon14_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon29_Then_correct  (=> (= (ControlFlow 0 38143) 38135) inline$$Option_destroy_with_default_$def_verify$0$anon14_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon28_Then_correct  (=> (|b#$Boolean| inline$$Vector_is_empty$0$b@1@@0) (and (=> (= (ControlFlow 0 38125) 38143) inline$$Option_destroy_with_default_$def_verify$0$anon29_Then_correct) (=> (= (ControlFlow 0 38125) 38133) inline$$Option_destroy_with_default_$def_verify$0$anon29_Else_correct)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon20_correct  (=> (and (= $abort_flag@1@@5 $abort_flag@0@@6) (= |inline$$Option_destroy_with_default_$def_verify$0$tmp#$2@1| inline$$Vector_pop_back$0$e@2@@1)) (and (=> (= (ControlFlow 0 38033) 38053) inline$$Option_destroy_with_default_$def_verify$0$anon33_Then_correct) (=> (= (ControlFlow 0 38033) 38043) inline$$Option_destroy_with_default_$def_verify$0$anon33_Else_correct)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon32_Else_correct  (=> (and (not true) (= (ControlFlow 0 38031) 38033)) inline$$Option_destroy_with_default_$def_verify$0$anon20_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon32_Then_correct  (=> (= (ControlFlow 0 38061) 38033) inline$$Option_destroy_with_default_$def_verify$0$anon20_correct)))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@2  (=> (not (= (|l#$Mutation| |inline$$WriteRef$0$to'@1@@2|) ($Local 3))) (and (=> (= (ControlFlow 0 37957) 38061) inline$$Option_destroy_with_default_$def_verify$0$anon32_Then_correct) (=> (= (ControlFlow 0 37957) 38031) inline$$Option_destroy_with_default_$def_verify$0$anon32_Else_correct)))))
(let ((inline$$WritebackToValue$0$anon3_Then_correct@@2  (=> (and (= (|l#$Mutation| |inline$$WriteRef$0$to'@1@@2|) ($Local 3)) (= |inline$$WritebackToValue$0$vdst'@1@@2| ($UpdateValue_stratified (|p#$Mutation| |inline$$WriteRef$0$to'@1@@2|) 0 inline$$Option_Option_unpack$0$vec@1@@1 (|v#$Mutation| |inline$$WriteRef$0$to'@1@@2|)))) (and (=> (= (ControlFlow 0 37983) 38061) inline$$Option_destroy_with_default_$def_verify$0$anon32_Then_correct) (=> (= (ControlFlow 0 37983) 38031) inline$$Option_destroy_with_default_$def_verify$0$anon32_Else_correct)))))
(let ((inline$$WriteRef$0$anon0_correct@@2  (=> (= |inline$$WriteRef$0$to'@1@@2| ($Mutation (|l#$Mutation| inline$$BorrowLoc$1$dst@1) (|p#$Mutation| inline$$BorrowLoc$1$dst@1) |inline$$Vector_pop_back$0$v'@2@@1|)) (and (=> (= (ControlFlow 0 37858) 37983) inline$$WritebackToValue$0$anon3_Then_correct@@2) (=> (= (ControlFlow 0 37858) 37957) inline$$WritebackToValue$0$anon3_Else_correct@@2)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon30_Else_correct  (=> (and (not $abort_flag@0@@6) (= (ControlFlow 0 37864) 37858)) inline$$WriteRef$0$anon0_correct@@2)))
(let ((inline$$Vector_pop_back$0$anon3_Then$1_correct@@1  (=> (= $abort_flag@0@@6 true) (=> (and (= inline$$Vector_pop_back$0$e@2@@1 inline$$Vector_pop_back$0$e@0@@1) (= |inline$$Vector_pop_back$0$v'@2@@1| |inline$$Vector_pop_back$0$v'@0@@1|)) (and (=> (= (ControlFlow 0 37791) 38065) inline$$Option_destroy_with_default_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 37791) 37864) inline$$Option_destroy_with_default_$def_verify$0$anon30_Else_correct))))))
(let ((inline$$Vector_pop_back$0$anon3_Then_correct@@1  (=> (and (= inline$$Vector_pop_back$0$len@1@@1 0) (= (ControlFlow 0 37789) 37791)) inline$$Vector_pop_back$0$anon3_Then$1_correct@@1)))
(let ((inline$$Vector_pop_back$0$anon3_Else_correct@@1  (=> (and (not (= inline$$Vector_pop_back$0$len@1@@1 0)) (= inline$$Vector_pop_back$0$e@1@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@1)) (- inline$$Vector_pop_back$0$len@1@@1 1)))) (=> (and (and (= |inline$$Vector_pop_back$0$v'@1@@1| ($Vector (let ((l@@40 (- (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@1)) 1)))
($ValueArray (|lambda#0| 0 l@@40 (|v#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@1)) $Error) l@@40)))) (= $abort_flag@0@@6 false)) (and (= inline$$Vector_pop_back$0$e@2@@1 inline$$Vector_pop_back$0$e@1@@1) (= |inline$$Vector_pop_back$0$v'@2@@1| |inline$$Vector_pop_back$0$v'@1@@1|))) (and (=> (= (ControlFlow 0 37741) 38065) inline$$Option_destroy_with_default_$def_verify$0$anon30_Then_correct) (=> (= (ControlFlow 0 37741) 37864) inline$$Option_destroy_with_default_$def_verify$0$anon30_Else_correct))))))
916
(let ((inline$$Vector_pop_back$0$anon0_correct@@1  (=> (and ((_ is $Vector) inline$$ReadRef$1$v@1@@1) (= inline$$Vector_pop_back$0$len@1@@1 (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$1$v@1@@1)))) (and (=> (= (ControlFlow 0 37719) 37789) inline$$Vector_pop_back$0$anon3_Then_correct@@1) (=> (= (ControlFlow 0 37719) 37741) inline$$Vector_pop_back$0$anon3_Else_correct@@1)))))
917
918
919
920
921
(let ((inline$$ReadRef$1$anon0_correct@@1  (=> (and (= inline$$ReadRef$1$v@1@@1 (|v#$Mutation| inline$$BorrowLoc$1$dst@1)) (= (ControlFlow 0 37608) 37719)) inline$$Vector_pop_back$0$anon0_correct@@1)))
(let ((inline$$BorrowLoc$1$anon0_correct  (=> (and (= inline$$BorrowLoc$1$dst@1 ($Mutation ($Local 3) $EmptyPath inline$$Option_Option_unpack$0$vec@1@@1)) (= (ControlFlow 0 37570) 37608)) inline$$ReadRef$1$anon0_correct@@1)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon28_Else_correct  (=> (and (not (|b#$Boolean| inline$$Vector_is_empty$0$b@1@@0)) (= (ControlFlow 0 37576) 37570)) inline$$BorrowLoc$1$anon0_correct)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon26_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 37514) 38125) inline$$Option_destroy_with_default_$def_verify$0$anon28_Then_correct) (=> (= (ControlFlow 0 37514) 37576) inline$$Option_destroy_with_default_$def_verify$0$anon28_Else_correct)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon26_Then_correct true))
922
(let ((inline$$Vector_is_empty$0$anon0_correct@@0  (=> (and ((_ is $Vector) inline$$ReadRef$0$v@1@@2) (= inline$$Vector_is_empty$0$b@1@@0 ($Boolean (= (|l#$ValueArray| (|v#$Vector| inline$$ReadRef$0$v@1@@2)) 0)))) (and (=> (= (ControlFlow 0 37500) 38147) inline$$Option_destroy_with_default_$def_verify$0$anon26_Then_correct) (=> (= (ControlFlow 0 37500) 37514) inline$$Option_destroy_with_default_$def_verify$0$anon26_Else_correct)))))
923
924
925
926
(let ((inline$$ReadRef$0$anon0_correct@@2  (=> (and (= inline$$ReadRef$0$v@1@@2 (|v#$Mutation| inline$$BorrowLoc$0$dst@1@@2)) (= (ControlFlow 0 37435) 37500)) inline$$Vector_is_empty$0$anon0_correct@@0)))
(let ((inline$$BorrowLoc$0$anon0_correct@@2  (=> (and (= inline$$BorrowLoc$0$dst@1@@2 ($Mutation ($Local 3) $EmptyPath inline$$Option_Option_unpack$0$vec@1@@1)) (= (ControlFlow 0 37397) 37435)) inline$$ReadRef$0$anon0_correct@@2)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon25_Else_correct  (=> (and (not true) (= (ControlFlow 0 37347) 37397)) inline$$BorrowLoc$0$anon0_correct@@2)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon25_Then_correct  (=> (= (ControlFlow 0 38171) 37397) inline$$BorrowLoc$0$anon0_correct@@2)))
927
(let ((inline$$Option_Option_unpack$0$anon0_correct@@1  (=> (and (and ((_ is $Vector) t@@6) (= inline$$Option_Option_unpack$0$vec@1@@1 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@6)) $Option_Option_vec))) (and ((_ is $Vector) inline$$Option_Option_unpack$0$vec@1@@1) (let ((va@@38 (|v#$Vector| inline$$Option_Option_unpack$0$vec@1@@1)))
928
929
930
931
932
933
934
935
(let ((l@@41 (|l#$ValueArray| va@@38)))
 (and (and (<= 0 l@@41) (<= l@@41 $MAX_U64)) (forall ((x@@38 Int) ) (!  (=> (or (< x@@38 0) (>= x@@38 l@@41)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@38) x@@38) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@38) x@@38))
))))))) (and (=> (= (ControlFlow 0 37333) 38171) inline$$Option_destroy_with_default_$def_verify$0$anon25_Then_correct) (=> (= (ControlFlow 0 37333) 37347) inline$$Option_destroy_with_default_$def_verify$0$anon25_Else_correct)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon24_Else_correct  (=> (and (not true) (= (ControlFlow 0 37206) 37333)) inline$$Option_Option_unpack$0$anon0_correct@@1)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon24_Then_correct  (=> (= (ControlFlow 0 38179) 37333) inline$$Option_Option_unpack$0$anon0_correct@@1)))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon23_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 37198) 38179) inline$$Option_destroy_with_default_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 37198) 37206) inline$$Option_destroy_with_default_$def_verify$0$anon24_Else_correct)))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon23_Then_correct  (and (=> (= (ControlFlow 0 38187) 38179) inline$$Option_destroy_with_default_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 38187) 37206) inline$$Option_destroy_with_default_$def_verify$0$anon24_Else_correct))))
(let ((inline$$Option_destroy_with_default_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 37192) 38187) inline$$Option_destroy_with_default_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 37192) 37198) inline$$Option_destroy_with_default_$def_verify$0$anon23_Else_correct)))))
936
(let ((anon0_correct@@6  (=> (and (and (and (and (and ((_ is $Vector) t@@6) (let ((va@@39 (|v#$Vector| t@@6)))
937
938
(let ((l@@42 (|l#$ValueArray| va@@39)))
 (and (and (<= 0 l@@42) (<= l@@42 $MAX_U64)) (forall ((x@@39 Int) ) (!  (=> (or (< x@@39 0) (>= x@@39 l@@42)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@39) x@@39) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@39) x@@39))
939
)))))) (= (|l#$ValueArray| (|v#$Vector| t@@6)) 1)) (and ((_ is $Vector) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@6)) $Option_Option_vec)) (let ((va@@40 (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@6)) $Option_Option_vec))))
940
941
942
943
944
945
946
947
948
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
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(let ((l@@43 (|l#$ValueArray| va@@40)))
 (and (and (<= 0 l@@43) (<= l@@43 $MAX_U64)) (forall ((x@@40 Int) ) (!  (=> (or (< x@@40 0) (>= x@@40 l@@43)) (= (|Select_[$int]$Value| (|v#$ValueArray| va@@40) x@@40) $Error)) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| va@@40) x@@40))
))))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@6)) $Option_Option_vec))))) (|i#$Integer| ($Integer 1)))))) (= (ControlFlow 0 36783) 37192)) inline$$Option_destroy_with_default_$def_verify$0$anon0_correct)))
(let ((PreconditionGeneratedEntry_correct@@6  (=> (= (ControlFlow 0 54678) 36783) anon0_correct@@6)))
PreconditionGeneratedEntry_correct@@6))))))))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $tv0@@8 () T@$TypeValue)
(declare-fun t@@7 () T@$Value)
(declare-fun $abort_flag@3@@4 () Bool)
(declare-fun $abort_code@6@@4 () Int)
(declare-fun inline$$Option_extract_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun inline$$Option_extract_$def_verify$0$$ret1@2 () T@$Value)
(declare-fun inline$$Vector_pop_back$0$e@2@@2 () T@$Value)
(declare-fun |inline$$WritebackToValue$0$vdst'@2@@2| () T@$Value)
(declare-fun $abort_code@4@@4 () Int)
(declare-fun $abort_flag@2@@6 () Bool)
(declare-fun |inline$$WritebackToReference$0$dst'@2@@1| () T@$Mutation)
(declare-fun |inline$$WritebackToValue$0$vdst'@1@@3| () T@$Value)
(declare-fun inline$$Option_Option_$pack_ref$1$$after@0@@0 () T@$Value)
(declare-fun inline$$BorrowLoc$0$dst@1@@3 () T@$Mutation)
(declare-fun |inline$$WriteRef$0$to'@1@@3| () T@$Mutation)
(declare-fun inline$$WritebackToReference$0$dstPath@1@@1 () T@$Path)
(declare-fun inline$$WritebackToReference$0$srcPath@1@@1 () T@$Path)
(declare-fun |inline$$WritebackToReference$0$dst'@1@@1| () T@$Mutation)
(declare-fun inline$$BorrowField$0$dst@1@@1 () T@$Mutation)
(declare-fun |inline$$Vector_pop_back$0$v'@2@@2| () T@$Value)
(declare-fun inline$$Option_extract_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun inline$$Option_extract_$def_verify$0$$ret1@1 () T@$Value)
(declare-fun $abort_code@5@@4 () Int)
(declare-fun $abort_code@1@@4 () Int)
(declare-fun $abort_flag@0@@7 () Bool)
(declare-fun $abort_code@2@@4 () Int)
(declare-fun $abort_flag@1@@6 () Bool)
(declare-fun inline$$Vector_pop_back$0$e@0@@2 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@0@@2| () T@$Value)
(declare-fun inline$$Vector_pop_back$0$len@1@@2 () Int)
(declare-fun inline$$Vector_pop_back$0$e@1@@2 () T@$Value)
(declare-fun inline$$ReadRef$1$v@1@@2 () T@$Value)
(declare-fun |inline$$Vector_pop_back$0$v'@1@@2| () T@$Value)
(declare-fun inline$$BorrowField$0$p@1@@1 () T@$Path)
(declare-fun inline$$BorrowField$0$size@1@@1 () Int)
(declare-fun inline$$BorrowField$0$p@2@@1 () T@$Path)
(declare-fun call4formal@$ret0@0@@4 () T@$Value)
(declare-fun $abort_code@3@@4 () Int)
(declare-fun call3formal@$ret0@0@@4 () T@$Value)
(declare-fun inline$$Option_Option_$pack_ref$0$$after@0@@0 () T@$Value)
(declare-fun inline$$Option_extract_$def_verify$0$$t7@1 () T@$Value)
(declare-fun inline$$ReadRef$0$v@1@@3 () T@$Value)
(declare-fun inline$$Option_Option_$unpack_ref$0$$before@0@@0 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 55513) (let ((anon0$2_correct@@7  (and (=> (= (ControlFlow 0 40201) (- 0 56854)) (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3@@4)) (=> (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec)) ($Integer 0)))) $abort_flag@3@@4) (and (=> (= (ControlFlow 0 40201) (- 0 56865)) (=> $abort_flag@3@@4 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec)) ($Integer 0)))))) (=> (=> $abort_flag@3@@4 (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec)) ($Integer 0))))) (and (=> (= (ControlFlow 0 40201) (- 0 56876)) (=> $abort_flag@3@@4 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6@@4 (|i#$Integer| ($Integer 7)))))) (=> (=> $abort_flag@3@@4 (and (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec)) ($Integer 0)))) (= $abort_code@6@@4 (|i#$Integer| ($Integer 7))))) (and (=> (= (ControlFlow 0 40201) (- 0 56898)) (=> (not $abort_flag@3@@4) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_extract_$def_verify$0$$ret0@2 ($Vector_$borrow $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec) ($Integer 0))))))) (=> (=> (not $abort_flag@3@@4) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$Option_extract_$def_verify$0$$ret0@2 ($Vector_$borrow $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| t@@7)) $Option_Option_vec) ($Integer 0)))))) (=> (= (ControlFlow 0 40201) (- 0 56916)) (=> (not $abort_flag@3@@4) (|b#$Boolean| ($Boolean ($IsEqual_stratified ($Vector_$length $tv0@@8 (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$Option_extract_$def_verify$0$$ret1@2)) $Option_Option_vec)) ($Integer 0))))))))))))))))
(let ((inline$$Option_extract_$def_verify$0$anon22_correct  (=> (= inline$$Option_extract_$def_verify$0$$ret0@2 inline$$Vector_pop_back$0$e@2@@2) (=> (and (and (= inline$$Option_extract_$def_verify$0$$ret1@2 |inline$$WritebackToValue$0$vdst'@2@@2|) (= $abort_code@6@@4 $abort_code@4@@4)) (and (= $abort_flag@3@@4 $abort_flag@2@@6) (= (ControlFlow 0 40107) 40201))) anon0$2_correct@@7))))
(let ((inline$$Option_extract_$def_verify$0$anon33_Else_correct  (=> (and (not true) (= (ControlFlow 0 40105) 40107)) inline$$Option_extract_$def_verify$0$anon22_correct)))
(let ((inline$$Option_extract_$def_verify$0$anon33_Then_correct  (=> (= (ControlFlow 0 40115) 40107) inline$$Option_extract_$def_verify$0$anon22_correct)))
(let ((inline$$Option_extract_$def_verify$0$anon32_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 40095) 40115) inline$$Option_extract_$def_verify$0$anon33_Then_correct) (=> (= (ControlFlow 0 40095) 40105) inline$$Option_extract_$def_verify$0$anon33_Else_correct)))))
(let ((inline$$Option_extract_$def_verify$0$anon32_Then_correct  (and (=> (= (ControlFlow 0 40123) 40115) inline$$Option_extract_$def_verify$0$anon33_Then_correct) (=> (= (ControlFlow 0 40123) 40105) inline$$Option_extract_$def_verify$0$anon33_Else_correct))))
(let ((inline$$WritebackToValue$0$anon3_Else_correct@@3  (=> (and (not (= (|l#$Mutation| |inline$$WritebackToReference$0$dst'@2@@1|) ($Local 3))) (= |inline$$WritebackToValue$0$vdst'@2@@2| t@@7)) (and (=> (= (ControlFlow 0 40053) 40123) inline$$Option_extract_$def_verify$0$anon32_Then_correct) (=> (= (ControlFlow 0 40053) 40095) inline$$Option_extract_$def_verify$0$anon32_Else_correct)))))
For faster browsing, not all history is shown. View entire blame