serialize_model.smt2 38.4 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
(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 |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))
109
(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))
110
)))
111
(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))
112
)))
113
(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))
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
)))
(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))
)))
171
(assert (forall ((v1@@2 T@$Value) (v2@@2 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@2) (let ((va (|v#$Vector| v1@@2)))
172
173
(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))
174
)))))) (and ((_ is $Vector) v2@@2) (let ((va@@0 (|v#$Vector| v2@@2)))
175
176
177
(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)))))
178
(assert (forall ((v1@@3 T@$Value) (v2@@3 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@3) (let ((va@@1 (|v#$Vector| v1@@3)))
179
180
(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))
181
)))))) (and ((_ is $Vector) v2@@3) (let ((va@@2 (|v#$Vector| v2@@3)))
182
183
184
(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))))
185
(assert (forall ((v1@@4 T@$Value) (v2@@4 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@4) (let ((va@@3 (|v#$Vector| v1@@4)))
186
187
(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))
188
)))))) (and ((_ is $Vector) v2@@4) (let ((va@@4 (|v#$Vector| v2@@4)))
189
190
191
(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)))))
192
(assert (forall ((v1@@5 T@$Value) (v2@@5 T@$Value) )  (=> (and (and (and ((_ is $Vector) v1@@5) (let ((va@@5 (|v#$Vector| v1@@5)))
193
194
(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))
195
)))))) (and ((_ is $Vector) v2@@5) (let ((va@@6 (|v#$Vector| v2@@5)))
196
197
198
(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))))
199
200
(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))))
201
202
203
(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)))
204
 (and (and (and ((_ is $Vector) r) (let ((va@@7 (|v#$Vector| r)))
205
206
(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))
207
)))))) (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))
208
209
))) (> (|l#$ValueArray| (|v#$Vector| r)) 0)))))
(assert (forall ((v@@13 T@$Value) ) (let ((r@@0 ($BCS_serialize_core v@@13)))
210
 (=> ((_ is $Address) v@@13) (= (|l#$ValueArray| (|v#$Vector| r@@0)) $serialized_address_len)))))
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
(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 $abort_flag@0 () Bool)
(declare-fun inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun inline$$TestBCS_bcs_test1_$def_verify$0$$ret1@2 () T@$Value)
(declare-fun v1@@7 () T@$Value)
(declare-fun v2@@7 () T@$Value)
(declare-fun call2formal@res@0 () T@$Value)
(declare-fun call2formal@res@0@@0 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 11865) (let ((anon0$2_correct  (and (=> (= (ControlFlow 0 10341) (- 0 12357)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0)) (=> (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0) (and (=> (= (ControlFlow 0 10341) (- 0 12366)) (=> $abort_flag@0 (|b#$Boolean| ($Boolean false)))) (=> (=> $abort_flag@0 (|b#$Boolean| ($Boolean false))) (and (=> (= (ControlFlow 0 10341) (- 0 12375)) (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2 inline$$TestBCS_bcs_test1_$def_verify$0$$ret1@2))) (|b#$Boolean| ($Boolean ($IsEqual_stratified v1@@7 v2@@7)))))))) (=> (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2 inline$$TestBCS_bcs_test1_$def_verify$0$$ret1@2))) (|b#$Boolean| ($Boolean ($IsEqual_stratified v1@@7 v2@@7))))))) (and (=> (= (ControlFlow 0 10341) (- 0 12404)) (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified v1@@7 v2@@7))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2 inline$$TestBCS_bcs_test1_$def_verify$0$$ret1@2)))))))) (=> (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean ($IsEqual_stratified v1@@7 v2@@7))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2 inline$$TestBCS_bcs_test1_$def_verify$0$$ret1@2))))))) (=> (= (ControlFlow 0 10341) (- 0 12433)) (=> (not $abort_flag@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean (> (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2)))) (|i#$Integer| ($Integer 0))))) (|b#$Boolean| ($Boolean (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2)) (|i#$Integer| ($Integer 0)))) (|i#$Integer| ($Integer $MAX_U8))))))))))))))))))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon16_correct  (=> (and (and (= $abort_flag@0 false) (= inline$$TestBCS_bcs_test1_$def_verify$0$$ret0@2 call2formal@res@0)) (and (= inline$$TestBCS_bcs_test1_$def_verify$0$$ret1@2 call2formal@res@0@@0) (= (ControlFlow 0 10251) 10341))) anon0$2_correct)))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon24_Else_correct  (=> (and (not true) (= (ControlFlow 0 10249) 10251)) inline$$TestBCS_bcs_test1_$def_verify$0$anon16_correct)))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon24_Then_correct  (=> (= (ControlFlow 0 10259) 10251) inline$$TestBCS_bcs_test1_$def_verify$0$anon16_correct)))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon23_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 10239) 10259) inline$$TestBCS_bcs_test1_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 10239) 10249) inline$$TestBCS_bcs_test1_$def_verify$0$anon24_Else_correct)))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon23_Then_correct  (and (=> (= (ControlFlow 0 10267) 10259) inline$$TestBCS_bcs_test1_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 10267) 10249) inline$$TestBCS_bcs_test1_$def_verify$0$anon24_Else_correct))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon21_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 10233) 10267) inline$$TestBCS_bcs_test1_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 10233) 10239) inline$$TestBCS_bcs_test1_$def_verify$0$anon23_Else_correct)))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon21_Then_correct true))
241
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon19_Else_correct  (=> (and (not false) (= call2formal@res@0@@0 ($BCS_serialize_core v2@@7))) (=> (and (and ((_ is $Vector) call2formal@res@0@@0) (let ((va@@8 (|v#$Vector| call2formal@res@0@@0)))
242
243
(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))
244
)))))) (forall ((i@@10 Int) ) (!  (=> (and (<= 0 i@@10) (< i@@10 (|l#$ValueArray| (|v#$Vector| call2formal@res@0@@0)))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@0)) i@@10)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@0)) i@@10)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@0)) i@@10)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@0)) i@@10))
245
246
))) (and (=> (= (ControlFlow 0 10225) 10271) inline$$TestBCS_bcs_test1_$def_verify$0$anon21_Then_correct) (=> (= (ControlFlow 0 10225) 10233) inline$$TestBCS_bcs_test1_$def_verify$0$anon21_Else_correct))))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon19_Then_correct true))
247
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon4$2_correct  (=> (= call2formal@res@0 ($BCS_serialize_core v1@@7)) (=> (and (and ((_ is $Vector) call2formal@res@0) (let ((va@@9 (|v#$Vector| call2formal@res@0)))
248
249
(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))
250
)))))) (forall ((i@@11 Int) ) (!  (=> (and (<= 0 i@@11) (< i@@11 (|l#$ValueArray| (|v#$Vector| call2formal@res@0)))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0)) i@@11)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0)) i@@11)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0)) i@@11)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0)) i@@11))
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
))) (and (=> (= (ControlFlow 0 10219) 10299) inline$$TestBCS_bcs_test1_$def_verify$0$anon19_Then_correct) (=> (= (ControlFlow 0 10219) 10225) inline$$TestBCS_bcs_test1_$def_verify$0$anon19_Else_correct))))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon18_Else_correct  (=> (and (not true) (= (ControlFlow 0 10149) 10219)) inline$$TestBCS_bcs_test1_$def_verify$0$anon4$2_correct)))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon18_Then_correct  (=> (= (ControlFlow 0 10323) 10219) inline$$TestBCS_bcs_test1_$def_verify$0$anon4$2_correct)))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon17_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 10141) 10323) inline$$TestBCS_bcs_test1_$def_verify$0$anon18_Then_correct) (=> (= (ControlFlow 0 10141) 10149) inline$$TestBCS_bcs_test1_$def_verify$0$anon18_Else_correct)))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon17_Then_correct  (and (=> (= (ControlFlow 0 10331) 10323) inline$$TestBCS_bcs_test1_$def_verify$0$anon18_Then_correct) (=> (= (ControlFlow 0 10331) 10149) inline$$TestBCS_bcs_test1_$def_verify$0$anon18_Else_correct))))
(let ((inline$$TestBCS_bcs_test1_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 10135) 10331) inline$$TestBCS_bcs_test1_$def_verify$0$anon17_Then_correct) (=> (= (ControlFlow 0 10135) 10141) inline$$TestBCS_bcs_test1_$def_verify$0$anon17_Else_correct)))))
(let ((anon0_correct  (=> (= (ControlFlow 0 11865) 10135) inline$$TestBCS_bcs_test1_$def_verify$0$anon0_correct)))
anon0_correct))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $abort_flag@0@@0 () Bool)
(declare-fun inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret1@2 () T@$Value)
(declare-fun call2formal@res@0@@1 () T@$Value)
(declare-fun call2formal@res@0@@2 () T@$Value)
(declare-fun v2@@8 () T@$Value)
(declare-fun v1@@8 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 12500) (let ((anon0$2_correct@@0  (and (=> (= (ControlFlow 0 10949) (- 0 12922)) (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@0)) (=> (=> (|b#$Boolean| ($Boolean false)) $abort_flag@0@@0) (and (=> (= (ControlFlow 0 10949) (- 0 12931)) (=> $abort_flag@0@@0 (|b#$Boolean| ($Boolean false)))) (=> (=> $abort_flag@0@@0 (|b#$Boolean| ($Boolean false))) (and (=> (= (ControlFlow 0 10949) (- 0 12940)) (=> (not $abort_flag@0@@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret0@2 inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret1@2))))) (=> (=> (not $abort_flag@0@@0) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret0@2 inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret1@2)))) (=> (= (ControlFlow 0 10949) (- 0 12953)) (=> (not $abort_flag@0@@0) (|b#$Boolean| ($Boolean (> (|i#$Integer| ($Integer (|l#$ValueArray| (|v#$Vector| inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret0@2)))) (|i#$Integer| ($Integer 0)))))))))))))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon16_correct  (=> (and (and (= $abort_flag@0@@0 false) (= inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret0@2 call2formal@res@0@@1)) (and (= inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$$ret1@2 call2formal@res@0@@2) (= (ControlFlow 0 10859) 10949))) anon0$2_correct@@0)))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon24_Else_correct  (=> (and (not true) (= (ControlFlow 0 10857) 10859)) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon16_correct)))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon24_Then_correct  (=> (= (ControlFlow 0 10867) 10859) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon16_correct)))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon23_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 10847) 10867) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 10847) 10857) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon24_Else_correct)))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon23_Then_correct  (and (=> (= (ControlFlow 0 10875) 10867) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 10875) 10857) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon24_Else_correct))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon21_Else_correct  (=> (not false) (and (=> (= (ControlFlow 0 10841) 10875) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 10841) 10847) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon23_Else_correct)))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon21_Then_correct true))
280
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon19_Else_correct  (=> (and (not false) (= call2formal@res@0@@2 ($BCS_serialize_core v2@@8))) (=> (and (and ((_ is $Vector) call2formal@res@0@@2) (let ((va@@10 (|v#$Vector| call2formal@res@0@@2)))
281
282
(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))
283
)))))) (forall ((i@@12 Int) ) (!  (=> (and (<= 0 i@@12) (< i@@12 (|l#$ValueArray| (|v#$Vector| call2formal@res@0@@2)))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@2)) i@@12)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@2)) i@@12)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@2)) i@@12)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@2)) i@@12))
284
285
))) (and (=> (= (ControlFlow 0 10833) 10879) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon21_Then_correct) (=> (= (ControlFlow 0 10833) 10841) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon21_Else_correct))))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon19_Then_correct true))
286
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon4$2_correct  (=> (= call2formal@res@0@@1 ($BCS_serialize_core v1@@8)) (=> (and (and ((_ is $Vector) call2formal@res@0@@1) (let ((va@@11 (|v#$Vector| call2formal@res@0@@1)))
287
288
(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))
289
)))))) (forall ((i@@13 Int) ) (!  (=> (and (<= 0 i@@13) (< i@@13 (|l#$ValueArray| (|v#$Vector| call2formal@res@0@@1)))) (and (and ((_ is $Integer) (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@1)) i@@13)) (>= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@1)) i@@13)) 0)) (<= (|i#$Integer| (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@1)) i@@13)) $MAX_U8))) :pattern ( (|Select_[$int]$Value| (|v#$ValueArray| (|v#$Vector| call2formal@res@0@@1)) i@@13))
290
291
292
293
294
295
296
297
298
299
300
301
302
))) (and (=> (= (ControlFlow 0 10827) 10907) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon19_Then_correct) (=> (= (ControlFlow 0 10827) 10833) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon19_Else_correct))))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon18_Else_correct  (=> (and (not true) (= (ControlFlow 0 10757) 10827)) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon4$2_correct)))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon18_Then_correct  (=> (= (ControlFlow 0 10931) 10827) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon4$2_correct)))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon17_Else_correct  (=> (not true) (and (=> (= (ControlFlow 0 10749) 10931) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon18_Then_correct) (=> (= (ControlFlow 0 10749) 10757) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon18_Else_correct)))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon17_Then_correct  (and (=> (= (ControlFlow 0 10939) 10931) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon18_Then_correct) (=> (= (ControlFlow 0 10939) 10757) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon18_Else_correct))))
(let ((inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 10743) 10939) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon17_Then_correct) (=> (= (ControlFlow 0 10743) 10749) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon17_Else_correct)))))
(let ((anon0_correct@@0  (=> (= (ControlFlow 0 12500) 10743) inline$$TestBCS_bcs_test1_incorrect_$def_verify$0$anon0_correct)))
anon0_correct@@0))))))))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(exit)