schema_exp.smt2 47.9 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
241
(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 c () T@$Value)
(declare-fun $abort_flag@0 () Bool)
(declare-fun inline$$Not$0$dst@1 () T@$Value)
(declare-fun inline$$TestSchemaExp_bar_incorrect_$def_verify$0$$t3@1 () T@$Value)
(declare-fun $abort_code@1 () Int)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 13476) (let ((anon0$2_correct  (and (=> (= (ControlFlow 0 10554) (- 0 13686)) (=> (|b#$Boolean| ($Boolean  (and (|b#$Boolean| c) (|b#$Boolean| ($Boolean false))))) $abort_flag@0)) (=> (=> (|b#$Boolean| ($Boolean  (and (|b#$Boolean| c) (|b#$Boolean| ($Boolean false))))) $abort_flag@0) (=> (= (ControlFlow 0 10554) (- 0 13705)) (=> $abort_flag@0 (|b#$Boolean| ($Boolean  (and (|b#$Boolean| c) (|b#$Boolean| ($Boolean false)))))))))))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon6_correct  (=> (and (= $abort_flag@0 true) (= (ControlFlow 0 10532) 10554)) anon0$2_correct)))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 10528) 10532)) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon6_correct)))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 10540) 10532) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon6_correct)))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon8_Then_correct  (=> (|b#$Boolean| inline$$Not$0$dst@1) (=> (and (= inline$$TestSchemaExp_bar_incorrect_$def_verify$0$$t3@1 ($Integer 1)) (= $abort_code@1 (|i#$Integer| inline$$TestSchemaExp_bar_incorrect_$def_verify$0$$t3@1))) (and (=> (= (ControlFlow 0 10522) 10540) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 10522) 10528) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon9_Else_correct))))))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon8_Else_correct  (=> (not (|b#$Boolean| inline$$Not$0$dst@1)) (=> (and (= $abort_flag@0 false) (= (ControlFlow 0 10508) 10554)) anon0$2_correct))))
(let ((inline$$Not$0$anon0_correct  (=> (= inline$$Not$0$dst@1 ($Boolean  (not (|b#$Boolean| c)))) (and (=> (= (ControlFlow 0 10492) 10522) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 10492) 10508) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$Not$0$Entry_correct  (and (=> (= (ControlFlow 0 10482) (- 0 13616)) true) (=> (= (ControlFlow 0 10482) 10492) inline$$Not$0$anon0_correct))))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 10414) 10482)) inline$$Not$0$Entry_correct)))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 10548) 10482) inline$$Not$0$Entry_correct)))
(let ((inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 10408) 10548) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 10408) 10414) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon7_Else_correct)))))
242
(let ((anon0_correct  (=> (and ((_ is $Boolean) c) (= (ControlFlow 0 10260) 10408)) inline$$TestSchemaExp_bar_incorrect_$def_verify$0$anon0_correct)))
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
(let ((PreconditionGeneratedEntry_correct  (=> (= (ControlFlow 0 13476) 10260) anon0_correct)))
PreconditionGeneratedEntry_correct))))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(declare-fun $abort_flag@3 () Bool)
(declare-fun i@@10 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun $abort_flag@1 () Bool)
(declare-fun $abort_flag@0@@0 () Bool)
(declare-fun |inline$$TestSchemaExp_baz_$def_verify$0$tmp#$1@1| () T@$Value)
(declare-fun $abort_flag@2 () Bool)
(declare-fun inline$$AddU64$1$dst@2 () T@$Value)
(declare-fun inline$$AddU64$1$dst@0 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_$def_verify$0$$t5@1 () T@$Value)
(declare-fun inline$$AddU64$1$dst@1 () T@$Value)
(declare-fun inline$$Gt$0$dst@1 () T@$Value)
(declare-fun inline$$AddU64$0$dst@2 () T@$Value)
(declare-fun inline$$AddU64$0$dst@0 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_$def_verify$0$$t6@1 () T@$Value)
(declare-fun inline$$AddU64$0$dst@1 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_$def_verify$0$$t3@1 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 13737) (let ((anon0$2_correct@@0  (and (=> (= (ControlFlow 0 11588) (- 0 14352)) (=> (not $abort_flag@3) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean (> (|i#$Integer| i@@10) (|i#$Integer| ($Integer 10))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestSchemaExp_baz_$def_verify$0$$ret0@2 ($Integer (+ (|i#$Integer| i@@10) (|i#$Integer| ($Integer 2)))))))))))) (=> (=> (not $abort_flag@3) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean (> (|i#$Integer| i@@10) (|i#$Integer| ($Integer 10))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestSchemaExp_baz_$def_verify$0$$ret0@2 ($Integer (+ (|i#$Integer| i@@10) (|i#$Integer| ($Integer 2))))))))))) (=> (= (ControlFlow 0 11588) (- 0 14400)) (=> (not $abort_flag@3) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean  (not (|b#$Boolean| ($Boolean (> (|i#$Integer| i@@10) (|i#$Integer| ($Integer 10)))))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestSchemaExp_baz_$def_verify$0$$ret0@2 ($Integer (+ (|i#$Integer| i@@10) (|i#$Integer| ($Integer 1))))))))))))))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$Abort_correct  (=> (and (and (= inline$$TestSchemaExp_baz_$def_verify$0$$ret0@1 $Error) (= inline$$TestSchemaExp_baz_$def_verify$0$$ret0@2 inline$$TestSchemaExp_baz_$def_verify$0$$ret0@1)) (and (= $abort_flag@3 true) (= (ControlFlow 0 11325) 11588))) anon0$2_correct@@0)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon22_Else_correct  (=> (and (not true) (= (ControlFlow 0 11562) 11325)) inline$$TestSchemaExp_baz_$def_verify$0$Abort_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon22_Then_correct  (=> (= (ControlFlow 0 11572) 11325) inline$$TestSchemaExp_baz_$def_verify$0$Abort_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon21_Then_correct  (=> $abort_flag@1 (and (=> (= (ControlFlow 0 11556) 11572) inline$$TestSchemaExp_baz_$def_verify$0$anon22_Then_correct) (=> (= (ControlFlow 0 11556) 11562) inline$$TestSchemaExp_baz_$def_verify$0$anon22_Else_correct)))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon25_Else_correct  (=> (and (not true) (= (ControlFlow 0 11317) 11325)) inline$$TestSchemaExp_baz_$def_verify$0$Abort_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon25_Then_correct  (=> (= (ControlFlow 0 11333) 11325) inline$$TestSchemaExp_baz_$def_verify$0$Abort_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon24_Then_correct  (=> $abort_flag@0@@0 (and (=> (= (ControlFlow 0 11311) 11333) inline$$TestSchemaExp_baz_$def_verify$0$anon25_Then_correct) (=> (= (ControlFlow 0 11311) 11317) inline$$TestSchemaExp_baz_$def_verify$0$anon25_Else_correct)))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon18_correct  (=> (= inline$$TestSchemaExp_baz_$def_verify$0$$ret0@2 |inline$$TestSchemaExp_baz_$def_verify$0$tmp#$1@1|) (=> (and (= $abort_flag@3 $abort_flag@2) (= (ControlFlow 0 11291) 11588)) anon0$2_correct@@0))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon27_Else_correct  (=> (and (not true) (= (ControlFlow 0 11289) 11291)) inline$$TestSchemaExp_baz_$def_verify$0$anon18_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon27_Then_correct  (=> (= (ControlFlow 0 11299) 11291) inline$$TestSchemaExp_baz_$def_verify$0$anon18_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon10_correct  (=> (and (= |inline$$TestSchemaExp_baz_$def_verify$0$tmp#$1@1| inline$$AddU64$1$dst@2) (= $abort_flag@2 $abort_flag@1)) (and (=> (= (ControlFlow 0 11544) 11299) inline$$TestSchemaExp_baz_$def_verify$0$anon27_Then_correct) (=> (= (ControlFlow 0 11544) 11289) inline$$TestSchemaExp_baz_$def_verify$0$anon27_Else_correct)))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon23_Else_correct  (=> (and (not true) (= (ControlFlow 0 11542) 11544)) inline$$TestSchemaExp_baz_$def_verify$0$anon10_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon23_Then_correct  (=> (= (ControlFlow 0 11552) 11544) inline$$TestSchemaExp_baz_$def_verify$0$anon10_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon21_Else_correct  (=> (not $abort_flag@1) (and (=> (= (ControlFlow 0 11536) 11552) inline$$TestSchemaExp_baz_$def_verify$0$anon23_Then_correct) (=> (= (ControlFlow 0 11536) 11542) inline$$TestSchemaExp_baz_$def_verify$0$anon23_Else_correct)))))
(let ((inline$$AddU64$1$anon3_Then$1_correct  (=> (and (= $abort_flag@1 true) (= inline$$AddU64$1$dst@2 inline$$AddU64$1$dst@0)) (and (=> (= (ControlFlow 0 11522) 11556) inline$$TestSchemaExp_baz_$def_verify$0$anon21_Then_correct) (=> (= (ControlFlow 0 11522) 11536) inline$$TestSchemaExp_baz_$def_verify$0$anon21_Else_correct)))))
(let ((inline$$AddU64$1$anon3_Then_correct  (=> (and (> (+ (|i#$Integer| i@@10) (|i#$Integer| inline$$TestSchemaExp_baz_$def_verify$0$$t5@1)) $MAX_U64) (= (ControlFlow 0 11520) 11522)) inline$$AddU64$1$anon3_Then$1_correct)))
(let ((inline$$AddU64$1$anon3_Else_correct  (=> (and (and (>= $MAX_U64 (+ (|i#$Integer| i@@10) (|i#$Integer| inline$$TestSchemaExp_baz_$def_verify$0$$t5@1))) (= inline$$AddU64$1$dst@1 ($Integer (+ (|i#$Integer| i@@10) (|i#$Integer| inline$$TestSchemaExp_baz_$def_verify$0$$t5@1))))) (and (= $abort_flag@1 false) (= inline$$AddU64$1$dst@2 inline$$AddU64$1$dst@1))) (and (=> (= (ControlFlow 0 11464) 11556) inline$$TestSchemaExp_baz_$def_verify$0$anon21_Then_correct) (=> (= (ControlFlow 0 11464) 11536) inline$$TestSchemaExp_baz_$def_verify$0$anon21_Else_correct)))))
(let ((inline$$AddU64$1$Entry_correct  (and (=> (= (ControlFlow 0 11434) (- 0 14184)) true) (and (=> (= (ControlFlow 0 11434) 11520) inline$$AddU64$1$anon3_Then_correct) (=> (= (ControlFlow 0 11434) 11464) inline$$AddU64$1$anon3_Else_correct)))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon20_Then_correct  (=> (|b#$Boolean| inline$$Gt$0$dst@1) (=> (and (= inline$$TestSchemaExp_baz_$def_verify$0$$t5@1 ($Integer 2)) (= (ControlFlow 0 11528) 11434)) inline$$AddU64$1$Entry_correct))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon16_correct  (=> (and (= |inline$$TestSchemaExp_baz_$def_verify$0$tmp#$1@1| inline$$AddU64$0$dst@2) (= $abort_flag@2 $abort_flag@0@@0)) (and (=> (= (ControlFlow 0 11279) 11299) inline$$TestSchemaExp_baz_$def_verify$0$anon27_Then_correct) (=> (= (ControlFlow 0 11279) 11289) inline$$TestSchemaExp_baz_$def_verify$0$anon27_Else_correct)))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon26_Else_correct  (=> (and (not true) (= (ControlFlow 0 11277) 11279)) inline$$TestSchemaExp_baz_$def_verify$0$anon16_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon26_Then_correct  (=> (= (ControlFlow 0 11307) 11279) inline$$TestSchemaExp_baz_$def_verify$0$anon16_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon24_Else_correct  (=> (not $abort_flag@0@@0) (and (=> (= (ControlFlow 0 11271) 11307) inline$$TestSchemaExp_baz_$def_verify$0$anon26_Then_correct) (=> (= (ControlFlow 0 11271) 11277) inline$$TestSchemaExp_baz_$def_verify$0$anon26_Else_correct)))))
(let ((inline$$AddU64$0$anon3_Then$1_correct  (=> (and (= $abort_flag@0@@0 true) (= inline$$AddU64$0$dst@2 inline$$AddU64$0$dst@0)) (and (=> (= (ControlFlow 0 11257) 11311) inline$$TestSchemaExp_baz_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 11257) 11271) inline$$TestSchemaExp_baz_$def_verify$0$anon24_Else_correct)))))
(let ((inline$$AddU64$0$anon3_Then_correct  (=> (and (> (+ (|i#$Integer| i@@10) (|i#$Integer| inline$$TestSchemaExp_baz_$def_verify$0$$t6@1)) $MAX_U64) (= (ControlFlow 0 11255) 11257)) inline$$AddU64$0$anon3_Then$1_correct)))
(let ((inline$$AddU64$0$anon3_Else_correct  (=> (and (and (>= $MAX_U64 (+ (|i#$Integer| i@@10) (|i#$Integer| inline$$TestSchemaExp_baz_$def_verify$0$$t6@1))) (= inline$$AddU64$0$dst@1 ($Integer (+ (|i#$Integer| i@@10) (|i#$Integer| inline$$TestSchemaExp_baz_$def_verify$0$$t6@1))))) (and (= $abort_flag@0@@0 false) (= inline$$AddU64$0$dst@2 inline$$AddU64$0$dst@1))) (and (=> (= (ControlFlow 0 11199) 11311) inline$$TestSchemaExp_baz_$def_verify$0$anon24_Then_correct) (=> (= (ControlFlow 0 11199) 11271) inline$$TestSchemaExp_baz_$def_verify$0$anon24_Else_correct)))))
(let ((inline$$AddU64$0$Entry_correct  (and (=> (= (ControlFlow 0 11169) (- 0 14074)) true) (and (=> (= (ControlFlow 0 11169) 11255) inline$$AddU64$0$anon3_Then_correct) (=> (= (ControlFlow 0 11169) 11199) inline$$AddU64$0$anon3_Else_correct)))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon20_Else_correct  (=> (not (|b#$Boolean| inline$$Gt$0$dst@1)) (=> (and (= inline$$TestSchemaExp_baz_$def_verify$0$$t6@1 ($Integer 1)) (= (ControlFlow 0 11263) 11169)) inline$$AddU64$0$Entry_correct))))
(let ((inline$$Gt$0$anon0_correct  (=> (= inline$$Gt$0$dst@1 ($Boolean (> (|i#$Integer| i@@10) (|i#$Integer| inline$$TestSchemaExp_baz_$def_verify$0$$t3@1)))) (and (=> (= (ControlFlow 0 11058) 11528) inline$$TestSchemaExp_baz_$def_verify$0$anon20_Then_correct) (=> (= (ControlFlow 0 11058) 11263) inline$$TestSchemaExp_baz_$def_verify$0$anon20_Else_correct)))))
(let ((inline$$Gt$0$Entry_correct  (and (=> (= (ControlFlow 0 11044) (- 0 14019)) true) (=> (= (ControlFlow 0 11044) 11058) inline$$Gt$0$anon0_correct))))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon2$1_correct  (=> (and (= inline$$TestSchemaExp_baz_$def_verify$0$$t3@1 ($Integer 10)) (= (ControlFlow 0 11064) 11044)) inline$$Gt$0$Entry_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon19_Else_correct  (=> (and (not true) (= (ControlFlow 0 10962) 11064)) inline$$TestSchemaExp_baz_$def_verify$0$anon2$1_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon19_Then_correct  (=> (= (ControlFlow 0 11580) 11064) inline$$TestSchemaExp_baz_$def_verify$0$anon2$1_correct)))
(let ((inline$$TestSchemaExp_baz_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 10956) 11580) inline$$TestSchemaExp_baz_$def_verify$0$anon19_Then_correct) (=> (= (ControlFlow 0 10956) 10962) inline$$TestSchemaExp_baz_$def_verify$0$anon19_Else_correct)))))
304
(let ((anon0_correct@@0  (=> (and (and (and ((_ is $Integer) i@@10) (>= (|i#$Integer| i@@10) 0)) (<= (|i#$Integer| i@@10) $MAX_U64)) (= (ControlFlow 0 10633) 10956)) inline$$TestSchemaExp_baz_$def_verify$0$anon0_correct)))
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
(let ((PreconditionGeneratedEntry_correct@@0  (=> (= (ControlFlow 0 13737) 10633) anon0_correct@@0)))
PreconditionGeneratedEntry_correct@@0))))))))))))))))))))))))))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(declare-fun $abort_flag@1@@0 () Bool)
(declare-fun i@@11 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@2 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@1 () T@$Value)
(declare-fun $abort_flag@0@@1 () Bool)
(declare-fun inline$$AddU64$0$dst@2@@0 () T@$Value)
(declare-fun inline$$AddU64$0$dst@0@@0 () T@$Value)
(declare-fun inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$t2@1 () T@$Value)
(declare-fun inline$$AddU64$0$dst@1@@0 () T@$Value)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 14459) (let ((anon0$2_correct@@1  (and (=> (= (ControlFlow 0 12205) (- 0 14827)) (=> (not $abort_flag@1@@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean (> (|i#$Integer| i@@11) (|i#$Integer| ($Integer 10))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@2 ($Integer (+ (|i#$Integer| i@@11) (|i#$Integer| ($Integer 2)))))))))))) (=> (=> (not $abort_flag@1@@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean (> (|i#$Integer| i@@11) (|i#$Integer| ($Integer 10))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@2 ($Integer (+ (|i#$Integer| i@@11) (|i#$Integer| ($Integer 2))))))))))) (=> (= (ControlFlow 0 12205) (- 0 14875)) (=> (not $abort_flag@1@@0) (|b#$Boolean| ($Boolean  (=> (|b#$Boolean| ($Boolean (<= (|i#$Integer| i@@11) (|i#$Integer| ($Integer 10))))) (|b#$Boolean| ($Boolean ($IsEqual_stratified inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@2 ($Integer (+ (|i#$Integer| i@@11) (|i#$Integer| ($Integer 1))))))))))))))))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon5_correct  (=> (and (and (= inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@1 $Error) (= inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@2 inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@1)) (and (= $abort_flag@1@@0 true) (= (ControlFlow 0 12181) 12205))) anon0$2_correct@@1)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon11_Else_correct  (=> (and (not true) (= (ControlFlow 0 12175) 12181)) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon5_correct)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon11_Then_correct  (=> (= (ControlFlow 0 12189) 12181) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon5_correct)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon10_Then_correct  (=> $abort_flag@0@@1 (and (=> (= (ControlFlow 0 12169) 12189) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon11_Then_correct) (=> (= (ControlFlow 0 12169) 12175) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon11_Else_correct)))))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon8_correct  (=> (= inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$ret0@2 inline$$AddU64$0$dst@2@@0) (=> (and (= $abort_flag@1@@0 $abort_flag@0@@1) (= (ControlFlow 0 12157) 12205)) anon0$2_correct@@1))))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon12_Else_correct  (=> (and (not true) (= (ControlFlow 0 12155) 12157)) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon8_correct)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon12_Then_correct  (=> (= (ControlFlow 0 12165) 12157) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon8_correct)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon10_Else_correct  (=> (not $abort_flag@0@@1) (and (=> (= (ControlFlow 0 12149) 12165) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon12_Then_correct) (=> (= (ControlFlow 0 12149) 12155) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon12_Else_correct)))))
(let ((inline$$AddU64$0$anon3_Then$1_correct@@0  (=> (and (= $abort_flag@0@@1 true) (= inline$$AddU64$0$dst@2@@0 inline$$AddU64$0$dst@0@@0)) (and (=> (= (ControlFlow 0 12133) 12169) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon10_Then_correct) (=> (= (ControlFlow 0 12133) 12149) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon10_Else_correct)))))
(let ((inline$$AddU64$0$anon3_Then_correct@@0  (=> (and (> (+ (|i#$Integer| i@@11) (|i#$Integer| inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$t2@1)) $MAX_U64) (= (ControlFlow 0 12131) 12133)) inline$$AddU64$0$anon3_Then$1_correct@@0)))
(let ((inline$$AddU64$0$anon3_Else_correct@@0  (=> (and (and (>= $MAX_U64 (+ (|i#$Integer| i@@11) (|i#$Integer| inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$t2@1))) (= inline$$AddU64$0$dst@1@@0 ($Integer (+ (|i#$Integer| i@@11) (|i#$Integer| inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$t2@1))))) (and (= $abort_flag@0@@1 false) (= inline$$AddU64$0$dst@2@@0 inline$$AddU64$0$dst@1@@0))) (and (=> (= (ControlFlow 0 12075) 12169) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon10_Then_correct) (=> (= (ControlFlow 0 12075) 12149) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon10_Else_correct)))))
(let ((inline$$AddU64$0$Entry_correct@@0  (and (=> (= (ControlFlow 0 12045) (- 0 14688)) true) (and (=> (= (ControlFlow 0 12045) 12131) inline$$AddU64$0$anon3_Then_correct@@0) (=> (= (ControlFlow 0 12045) 12075) inline$$AddU64$0$anon3_Else_correct@@0)))))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon2$1_correct  (=> (and (= inline$$TestSchemaExp_baz_incorrect_$def_verify$0$$t2@1 ($Integer 1)) (= (ControlFlow 0 12139) 12045)) inline$$AddU64$0$Entry_correct@@0)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 11914) 12139)) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon2$1_correct)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 12197) 12139) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon2$1_correct)))
(let ((inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 11908) 12197) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 11908) 11914) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon9_Else_correct)))))
339
(let ((anon0_correct@@1  (=> (and (and (and ((_ is $Integer) i@@11) (>= (|i#$Integer| i@@11) 0)) (<= (|i#$Integer| i@@11) $MAX_U64)) (= (ControlFlow 0 11729) 11908)) inline$$TestSchemaExp_baz_incorrect_$def_verify$0$anon0_correct)))
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
(let ((PreconditionGeneratedEntry_correct@@1  (=> (= (ControlFlow 0 14459) 11729) anon0_correct@@1)))
PreconditionGeneratedEntry_correct@@1))))))))))))))))))))
))
(set-info :status unknown)
(check-sat)
(pop 1)
(declare-fun c@@0 () T@$Value)
(declare-fun $abort_flag@0@@2 () Bool)
(declare-fun inline$$Not$0$dst@1@@0 () T@$Value)
(declare-fun inline$$TestSchemaExp_foo_$def_verify$0$$t3@1 () T@$Value)
(declare-fun $abort_code@1@@0 () Int)
(push 1)
(assert (not
 (=> (= (ControlFlow 0 0) 14927) (let ((anon0$2_correct@@2  (and (=> (= (ControlFlow 0 12594) (- 0 15188)) (=> (|b#$Boolean| ($Boolean  (and (|b#$Boolean| c@@0) (|b#$Boolean| ($Boolean false))))) $abort_flag@0@@2)) (=> (=> (|b#$Boolean| ($Boolean  (and (|b#$Boolean| c@@0) (|b#$Boolean| ($Boolean false))))) $abort_flag@0@@2) (and (=> (= (ControlFlow 0 12594) (- 0 15207)) (=> (|b#$Boolean| ($Boolean  (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| c@@0)))) (|b#$Boolean| ($Boolean true))))) $abort_flag@0@@2)) (=> (=> (|b#$Boolean| ($Boolean  (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| c@@0)))) (|b#$Boolean| ($Boolean true))))) $abort_flag@0@@2) (=> (= (ControlFlow 0 12594) (- 0 15232)) (=> $abort_flag@0@@2 (or (|b#$Boolean| ($Boolean  (and (|b#$Boolean| c@@0) (|b#$Boolean| ($Boolean false))))) (|b#$Boolean| ($Boolean  (and (|b#$Boolean| ($Boolean  (not (|b#$Boolean| c@@0)))) (|b#$Boolean| ($Boolean true))))))))))))))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon6_correct  (=> (and (= $abort_flag@0@@2 true) (= (ControlFlow 0 12572) 12594)) anon0$2_correct@@2)))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon9_Else_correct  (=> (and (not true) (= (ControlFlow 0 12568) 12572)) inline$$TestSchemaExp_foo_$def_verify$0$anon6_correct)))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon9_Then_correct  (=> (= (ControlFlow 0 12580) 12572) inline$$TestSchemaExp_foo_$def_verify$0$anon6_correct)))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon8_Then_correct  (=> (|b#$Boolean| inline$$Not$0$dst@1@@0) (=> (and (= inline$$TestSchemaExp_foo_$def_verify$0$$t3@1 ($Integer 1)) (= $abort_code@1@@0 (|i#$Integer| inline$$TestSchemaExp_foo_$def_verify$0$$t3@1))) (and (=> (= (ControlFlow 0 12562) 12580) inline$$TestSchemaExp_foo_$def_verify$0$anon9_Then_correct) (=> (= (ControlFlow 0 12562) 12568) inline$$TestSchemaExp_foo_$def_verify$0$anon9_Else_correct))))))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon8_Else_correct  (=> (not (|b#$Boolean| inline$$Not$0$dst@1@@0)) (=> (and (= $abort_flag@0@@2 false) (= (ControlFlow 0 12548) 12594)) anon0$2_correct@@2))))
(let ((inline$$Not$0$anon0_correct@@0  (=> (= inline$$Not$0$dst@1@@0 ($Boolean  (not (|b#$Boolean| c@@0)))) (and (=> (= (ControlFlow 0 12532) 12562) inline$$TestSchemaExp_foo_$def_verify$0$anon8_Then_correct) (=> (= (ControlFlow 0 12532) 12548) inline$$TestSchemaExp_foo_$def_verify$0$anon8_Else_correct)))))
(let ((inline$$Not$0$Entry_correct@@0  (and (=> (= (ControlFlow 0 12522) (- 0 15118)) true) (=> (= (ControlFlow 0 12522) 12532) inline$$Not$0$anon0_correct@@0))))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon7_Else_correct  (=> (and (not true) (= (ControlFlow 0 12454) 12522)) inline$$Not$0$Entry_correct@@0)))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon7_Then_correct  (=> (= (ControlFlow 0 12588) 12522) inline$$Not$0$Entry_correct@@0)))
(let ((inline$$TestSchemaExp_foo_$def_verify$0$anon0_correct  (=> (not false) (and (=> (= (ControlFlow 0 12448) 12588) inline$$TestSchemaExp_foo_$def_verify$0$anon7_Then_correct) (=> (= (ControlFlow 0 12448) 12454) inline$$TestSchemaExp_foo_$def_verify$0$anon7_Else_correct)))))
364
(let ((anon0_correct@@2  (=> (and ((_ is $Boolean) c@@0) (= (ControlFlow 0 12300) 12448)) inline$$TestSchemaExp_foo_$def_verify$0$anon0_correct)))
365
366
367
368
369
370
371
(let ((PreconditionGeneratedEntry_correct@@2  (=> (= (ControlFlow 0 14927) 12300) anon0_correct@@2)))
PreconditionGeneratedEntry_correct@@2))))))))))))))
))
(set-info :status unsat)
(check-sat)
(pop 1)
(exit)