-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathExample.smt
More file actions
516 lines (516 loc) · 39.7 KB
/
Example.smt
File metadata and controls
516 lines (516 loc) · 39.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
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
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
; Proof attempt for Example.s(int)
(set-option :produce-models true)
(set-logic ALL)
(set-option :AUTO_CONFIG false)
(set-option :smt.MBQI false)
(declare-sort REF 0)
(declare-fun NULL () REF)
(declare-fun NULLSTRING () (Array Int Int))
(declare-fun stringConcat (REF REF ) REF)
(declare-fun stringLength ((Array Int Int) ) Int)
(declare-fun __JMLlength () (Array REF Int))
(assert (forall ((o REF) ) (>= (select __JMLlength o) 0)))
(declare-fun asIntArray (REF ) (Array Int Int))
(declare-fun asREFArray (REF ) (Array Int REF))
(declare-fun intValue (REF ) Int)
(declare-fun booleanValue (REF ) Bool)
(define-fun |#is_byte#| ((x Int)) Bool (and (<= (- 128) x) (<= x 127)))
(define-fun |#is_short#| ((x Int)) Bool (and (<= (- 32768) x) (<= x 32767)))
(define-fun |#is_char#| ((x Int)) Bool (and (<= 0 x) (<= x 65535)))
(define-fun |#is_int#| ((x Int)) Bool (and (<= (- 2147483648) x) (<= x 2147483647)))
(define-fun |#is_long#| ((x Int)) Bool (and (<= (- 9223372036854775808) x) (<= x 9223372036854775807)))
(define-fun |#big8#| () Int 256)
(define-fun |#big16#| () Int 65536)
(define-fun |#big32#| () Int 4294967296)
(define-fun |#big64#| () Int (* 4294967296 4294967296))
(define-fun |#max8#| () Int 127)
(define-fun |#min8#| () Int (- 128))
(define-fun |#max16#| () Int 32767)
(define-fun |#min16#| () Int (- 32768))
(define-fun |#max32#| () Int 2147483647)
(define-fun |#min32#| () Int (- 2147483648))
(define-fun |#max64#| () Int (- (* 2147483648 4294967296) 1))
(define-fun |#min64#| () Int (- (* 2147483648 4294967296)))
(define-fun |#isMul32ok#| ((x Int)(y Int)) Bool (let ((prod (* x y)) ) (and (<= |#min32#| prod) (<= prod |#max32#|))))
(define-fun |#isMul64ok#| ((x Int)(y Int)) Bool (let ((prod (* x y)) ) (and (<= |#min64#| prod) (<= prod |#max64#|))))
(define-fun |#trunc32s#| ((x Int)) Int (let ((m (mod x |#big32#|)) ) (ite (<= m |#max32#|) m (- m |#big32#|))))
(define-fun |#trunc16s#| ((x Int)) Int (let ((m (mod x |#big16#|)) ) (ite (<= m |#max16#|) m (- m |#big16#|))))
(define-fun |#trunc8s#| ((x Int)) Int (let ((m (mod x |#big8#|)) ) (ite (<= m |#max8#|) m (- m |#big8#|))))
(define-fun |#cdiv#| ((a Int)(b Int)) Int (ite (>= a 0) (div a b) (div (- a) (- b))))
(define-fun |#cmod#| ((a Int)(b Int)) Int (ite (>= a 0) (mod a b) (mod (- a) (- b))))
(define-fun |#inRange32#| ((a Int)) Bool (and (<= |#min32#| a) (<= a |#max32#|)))
(define-fun |#add32ok#| ((a Int)(b Int)) Bool (|#inRange32#| (+ a b)))
(define-fun |#add32#| ((a Int)(b Int)) Int (let ((p (+ a b)) ) (ite (|#inRange32#| p) p (ite (< |#max32#| p) (- p |#big32#|) (+ p |#big32#|)))))
(define-fun |#mul32ok#| ((a Int)(b Int)) Bool (|#inRange32#| (* a b)))
(define-fun |#mul32#| ((a Int)(b Int)) Int (let ((p (* a b)) ) (ite (|#inRange32#| p) p (+ (mod (- p |#min32#|) |#big32#|) |#min32#|))))
(define-fun |#inRange64#| ((a Int)) Bool (and (<= |#min64#| a) (<= a |#max64#|)))
(define-fun |#add64ok#| ((a Int)(b Int)) Bool (|#inRange64#| (+ a b)))
(define-fun |#add64#| ((a Int)(b Int)) Int (let ((p (+ a b)) ) (ite (|#inRange64#| p) p (ite (< |#max64#| p) (- p |#big64#|) (+ p |#big64#|)))))
(define-fun |#mul64ok#| ((a Int)(b Int)) Bool (|#inRange64#| (* a b)))
(define-fun |#mul64#| ((a Int)(b Int)) Int (let ((p (* a b)) ) (ite (|#inRange64#| p) p (+ (mod (- p |#min64#|) |#big64#|) |#min64#|))))
(declare-sort |RANGE| 0)
(declare-fun |range:cons| (Int Int ) |RANGE|)
(declare-fun |range:lo| (|RANGE| ) Int)
(declare-fun |range:hi| (|RANGE| ) Int)
(assert (forall ((i Int) (j Int) ) (= i (|range:lo| (|range:cons| i j)))))
(assert (forall ((i Int) (j Int) ) (= j (|range:hi| (|range:cons| i j)))))
(declare-sort JMLTypeSort 0)
(declare-fun javaTypeOf (REF ) REF)
(declare-fun jmlTypeOf (REF ) JMLTypeSort)
(declare-fun typearg1_1 (JMLTypeSort ) JMLTypeSort)
(declare-fun typearg2_1 (JMLTypeSort ) JMLTypeSort)
(declare-fun typearg2_2 (JMLTypeSort ) JMLTypeSort)
(declare-fun typearg3_1 (JMLTypeSort ) JMLTypeSort)
(declare-fun typearg3_2 (JMLTypeSort ) JMLTypeSort)
(declare-fun typearg3_3 (JMLTypeSort ) JMLTypeSort)
(declare-fun javaSubType (REF REF ) Bool)
(declare-fun jmlSubType (JMLTypeSort JMLTypeSort ) Bool)
(declare-fun erasure (JMLTypeSort ) REF)
(declare-fun erasure_java (REF ) REF)
(declare-fun _JMLT_0 (REF ) JMLTypeSort)
(declare-fun _JMLT_1 (REF JMLTypeSort ) JMLTypeSort)
(declare-fun _JMLT_2 (REF JMLTypeSort JMLTypeSort ) JMLTypeSort)
(declare-fun _JMLT_3 (REF JMLTypeSort JMLTypeSort JMLTypeSort ) JMLTypeSort)
(assert (forall ((o REF) ) (= (erasure (jmlTypeOf o)) (javaTypeOf o))))
(assert (forall ((o REF) ) (= (erasure_java (javaTypeOf o)) (javaTypeOf o))))
(declare-fun _makeArrayType (REF ) REF)
(declare-fun _isArrayType (REF ) Bool)
(declare-fun _makeJMLArrayType (JMLTypeSort ) JMLTypeSort)
(declare-fun _isJMLArrayType (JMLTypeSort ) Bool)
(declare-fun __arrayElemType (JMLTypeSort ) JMLTypeSort)
(assert (forall ((T JMLTypeSort) ) (= (erasure (_makeJMLArrayType T)) (_makeArrayType (erasure T)))))
(assert (forall ((T1 JMLTypeSort) (T2 JMLTypeSort) ) (=> (jmlSubType T1 T2) (javaSubType (erasure T1) (erasure T2)))))
(assert (forall ((T1 REF) (T2 REF) (T3 JMLTypeSort) ) (= (javaSubType T1 T2) (jmlSubType (_JMLT_1 T1 T3) (_JMLT_1 T2 T3)))))
(assert (forall ((T1 REF) (T2 REF) (T3 JMLTypeSort) (T4 JMLTypeSort) ) (=> (and (javaSubType T1 T2) (not (= T3 T4))) (not (jmlSubType (_JMLT_1 T1 T3) (_JMLT_1 T2 T4))))))
(assert (forall ((T1 REF) (T2 REF) (T3 JMLTypeSort) (T4 JMLTypeSort) ) (=> (jmlSubType (_JMLT_1 T1 T3) (_JMLT_1 T2 T4)) (and (javaSubType T1 T2) (= T3 T4)))))
(assert (forall ((T1 REF) (T2 REF) (T3 JMLTypeSort) (T4 JMLTypeSort) ) (=> (= (_JMLT_1 T1 T3) (_JMLT_1 T2 T4)) (and (= T1 T2) (= T3 T4)))))
(declare-fun nonnullelements (REF (Array REF (Array Int REF)) ) Bool)
(assert (forall ((a REF) (arrays (Array REF (Array Int REF))) ) (= (nonnullelements a arrays) (forall ((i Int) ) (=> (and (<= 0 i) (< i (select __JMLlength a))) (distinct NULL (select (select arrays a) i)))))))
(declare-fun T_java_lang_RuntimeException () REF)
(declare-fun JMLT_java_lang_RuntimeException () JMLTypeSort)
(declare-fun T_java_lang_Object () REF)
(declare-fun JMLT_java_lang_Object () JMLTypeSort)
(declare-fun T_int () REF)
(declare-fun JMLT_int () JMLTypeSort)
(declare-fun T_java_lang_Integer () REF)
(declare-fun JMLT_java_lang_Integer () JMLTypeSort)
(declare-fun T_java_lang_Exception () REF)
(declare-fun JMLT_java_lang_Exception () JMLTypeSort)
(declare-fun T_java_lang_Class () REF)
(assert (not (_isArrayType T_java_lang_RuntimeException)))
(assert (not (_isJMLArrayType JMLT_java_lang_RuntimeException)))
(assert (= (_JMLT_0 T_java_lang_RuntimeException) JMLT_java_lang_RuntimeException))
(assert (= (erasure JMLT_java_lang_RuntimeException) T_java_lang_RuntimeException))
(assert (not (_isArrayType T_java_lang_Object)))
(assert (not (_isJMLArrayType JMLT_java_lang_Object)))
(assert (= (_JMLT_0 T_java_lang_Object) JMLT_java_lang_Object))
(assert (= (erasure JMLT_java_lang_Object) T_java_lang_Object))
(assert (not (_isArrayType T_int)))
(assert (not (_isJMLArrayType JMLT_int)))
(assert (= (_JMLT_0 T_int) JMLT_int))
(assert (= (erasure JMLT_int) T_int))
(assert (not (_isArrayType T_java_lang_Integer)))
(assert (forall ((t REF) ) (=> (javaSubType t T_java_lang_Integer) (= t T_java_lang_Integer))))
(assert (not (_isJMLArrayType JMLT_java_lang_Integer)))
(assert (= (_JMLT_0 T_java_lang_Integer) JMLT_java_lang_Integer))
(assert (= (erasure JMLT_java_lang_Integer) T_java_lang_Integer))
(assert (forall ((t JMLTypeSort) ) (=> (jmlSubType t JMLT_java_lang_Integer) (= t JMLT_java_lang_Integer))))
(assert (not (_isArrayType T_java_lang_Exception)))
(assert (not (_isJMLArrayType JMLT_java_lang_Exception)))
(assert (= (_JMLT_0 T_java_lang_Exception) JMLT_java_lang_Exception))
(assert (= (erasure JMLT_java_lang_Exception) T_java_lang_Exception))
(assert (not (_isArrayType T_java_lang_Class)))
(assert (forall ((t REF) ) (=> (javaSubType t T_java_lang_Class) (= t T_java_lang_Class))))
(assert (not (_isJMLArrayType (_JMLT_1 T_java_lang_Class JMLT_java_lang_Integer))))
(assert (= (erasure (_JMLT_1 T_java_lang_Class JMLT_java_lang_Integer)) T_java_lang_Class))
(assert (forall ((t JMLTypeSort) ) (=> (jmlSubType t (_JMLT_1 T_java_lang_Class JMLT_java_lang_Integer)) (= t (_JMLT_1 T_java_lang_Class JMLT_java_lang_Integer)))))
(assert (distinct T_java_lang_RuntimeException T_java_lang_Object T_int T_java_lang_Integer T_java_lang_Exception T_java_lang_Class))
(assert (distinct JMLT_java_lang_RuntimeException JMLT_java_lang_Object JMLT_int JMLT_java_lang_Integer JMLT_java_lang_Exception))
(assert (javaSubType T_java_lang_RuntimeException T_java_lang_RuntimeException))
(assert (javaSubType (_makeArrayType T_java_lang_RuntimeException) (_makeArrayType T_java_lang_RuntimeException)))
(assert (jmlSubType JMLT_java_lang_RuntimeException JMLT_java_lang_RuntimeException))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_RuntimeException) (_makeJMLArrayType JMLT_java_lang_RuntimeException)))
(assert (javaSubType T_java_lang_RuntimeException T_java_lang_Object))
(assert (javaSubType (_makeArrayType T_java_lang_RuntimeException) (_makeArrayType T_java_lang_Object)))
(assert (jmlSubType JMLT_java_lang_RuntimeException JMLT_java_lang_Object))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_RuntimeException) (_makeJMLArrayType JMLT_java_lang_Object)))
(assert (forall ((e REF) ) (=> (javaSubType (javaTypeOf e) T_java_lang_RuntimeException) (javaSubType (javaTypeOf e) T_java_lang_Object))))
(assert (not (javaSubType T_java_lang_RuntimeException T_int)))
(assert (not (javaSubType (_makeArrayType T_java_lang_RuntimeException) (_makeArrayType T_int))))
(assert (not (jmlSubType JMLT_java_lang_RuntimeException JMLT_int)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_RuntimeException) (_makeJMLArrayType JMLT_int))))
(assert (forall ((e REF) ) (or (not (javaSubType (javaTypeOf e) T_java_lang_RuntimeException)) (not (javaSubType (javaTypeOf e) T_int)))))
(assert (not (javaSubType T_java_lang_RuntimeException T_java_lang_Integer)))
(assert (not (javaSubType (_makeArrayType T_java_lang_RuntimeException) (_makeArrayType T_java_lang_Integer))))
(assert (not (jmlSubType JMLT_java_lang_RuntimeException JMLT_java_lang_Integer)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_RuntimeException) (_makeJMLArrayType JMLT_java_lang_Integer))))
(assert (forall ((e REF) ) (or (not (javaSubType (javaTypeOf e) T_java_lang_RuntimeException)) (not (javaSubType (javaTypeOf e) T_java_lang_Integer)))))
(assert (javaSubType T_java_lang_RuntimeException T_java_lang_Exception))
(assert (javaSubType (_makeArrayType T_java_lang_RuntimeException) (_makeArrayType T_java_lang_Exception)))
(assert (jmlSubType JMLT_java_lang_RuntimeException JMLT_java_lang_Exception))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_RuntimeException) (_makeJMLArrayType JMLT_java_lang_Exception)))
(assert (forall ((e REF) ) (=> (javaSubType (javaTypeOf e) T_java_lang_RuntimeException) (javaSubType (javaTypeOf e) T_java_lang_Exception))))
(assert (not (javaSubType T_java_lang_RuntimeException T_java_lang_Class)))
(assert (not (javaSubType (_makeArrayType T_java_lang_RuntimeException) (_makeArrayType T_java_lang_Class))))
(assert (not (javaSubType T_java_lang_Object T_java_lang_RuntimeException)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Object) (_makeArrayType T_java_lang_RuntimeException))))
(assert (not (jmlSubType JMLT_java_lang_Object JMLT_java_lang_RuntimeException)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Object) (_makeJMLArrayType JMLT_java_lang_RuntimeException))))
(assert (javaSubType T_java_lang_Object T_java_lang_Object))
(assert (javaSubType (_makeArrayType T_java_lang_Object) (_makeArrayType T_java_lang_Object)))
(assert (jmlSubType JMLT_java_lang_Object JMLT_java_lang_Object))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_Object) (_makeJMLArrayType JMLT_java_lang_Object)))
(assert (not (javaSubType T_java_lang_Object T_int)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Object) (_makeArrayType T_int))))
(assert (not (jmlSubType JMLT_java_lang_Object JMLT_int)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Object) (_makeJMLArrayType JMLT_int))))
(assert (forall ((e REF) ) (or (not (javaSubType (javaTypeOf e) T_java_lang_Object)) (not (javaSubType (javaTypeOf e) T_int)))))
(assert (not (javaSubType T_java_lang_Object T_java_lang_Integer)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Object) (_makeArrayType T_java_lang_Integer))))
(assert (not (jmlSubType JMLT_java_lang_Object JMLT_java_lang_Integer)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Object) (_makeJMLArrayType JMLT_java_lang_Integer))))
(assert (forall ((e REF) ) (=> (javaSubType (javaTypeOf e) T_java_lang_Integer) (javaSubType (javaTypeOf e) T_java_lang_Object))))
(assert (not (javaSubType T_java_lang_Object T_java_lang_Exception)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Object) (_makeArrayType T_java_lang_Exception))))
(assert (not (jmlSubType JMLT_java_lang_Object JMLT_java_lang_Exception)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Object) (_makeJMLArrayType JMLT_java_lang_Exception))))
(assert (forall ((e REF) ) (=> (javaSubType (javaTypeOf e) T_java_lang_Exception) (javaSubType (javaTypeOf e) T_java_lang_Object))))
(assert (not (javaSubType T_java_lang_Object T_java_lang_Class)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Object) (_makeArrayType T_java_lang_Class))))
(assert (not (javaSubType T_int T_java_lang_RuntimeException)))
(assert (not (javaSubType (_makeArrayType T_int) (_makeArrayType T_java_lang_RuntimeException))))
(assert (not (jmlSubType JMLT_int JMLT_java_lang_RuntimeException)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_int) (_makeJMLArrayType JMLT_java_lang_RuntimeException))))
(assert (not (javaSubType T_int T_java_lang_Object)))
(assert (not (javaSubType (_makeArrayType T_int) (_makeArrayType T_java_lang_Object))))
(assert (not (jmlSubType JMLT_int JMLT_java_lang_Object)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_int) (_makeJMLArrayType JMLT_java_lang_Object))))
(assert (javaSubType T_int T_int))
(assert (javaSubType (_makeArrayType T_int) (_makeArrayType T_int)))
(assert (jmlSubType JMLT_int JMLT_int))
(assert (jmlSubType (_makeJMLArrayType JMLT_int) (_makeJMLArrayType JMLT_int)))
(assert (not (javaSubType T_int T_java_lang_Integer)))
(assert (not (javaSubType (_makeArrayType T_int) (_makeArrayType T_java_lang_Integer))))
(assert (not (jmlSubType JMLT_int JMLT_java_lang_Integer)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_int) (_makeJMLArrayType JMLT_java_lang_Integer))))
(assert (forall ((e REF) ) (or (not (javaSubType (javaTypeOf e) T_int)) (not (javaSubType (javaTypeOf e) T_java_lang_Integer)))))
(assert (not (javaSubType T_int T_java_lang_Exception)))
(assert (not (javaSubType (_makeArrayType T_int) (_makeArrayType T_java_lang_Exception))))
(assert (not (jmlSubType JMLT_int JMLT_java_lang_Exception)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_int) (_makeJMLArrayType JMLT_java_lang_Exception))))
(assert (forall ((e REF) ) (or (not (javaSubType (javaTypeOf e) T_int)) (not (javaSubType (javaTypeOf e) T_java_lang_Exception)))))
(assert (not (javaSubType T_int T_java_lang_Class)))
(assert (not (javaSubType (_makeArrayType T_int) (_makeArrayType T_java_lang_Class))))
(assert (not (javaSubType T_java_lang_Integer T_java_lang_RuntimeException)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Integer) (_makeArrayType T_java_lang_RuntimeException))))
(assert (not (jmlSubType JMLT_java_lang_Integer JMLT_java_lang_RuntimeException)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Integer) (_makeJMLArrayType JMLT_java_lang_RuntimeException))))
(assert (javaSubType T_java_lang_Integer T_java_lang_Object))
(assert (javaSubType (_makeArrayType T_java_lang_Integer) (_makeArrayType T_java_lang_Object)))
(assert (jmlSubType JMLT_java_lang_Integer JMLT_java_lang_Object))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_Integer) (_makeJMLArrayType JMLT_java_lang_Object)))
(assert (not (javaSubType T_java_lang_Integer T_int)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Integer) (_makeArrayType T_int))))
(assert (not (jmlSubType JMLT_java_lang_Integer JMLT_int)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Integer) (_makeJMLArrayType JMLT_int))))
(assert (javaSubType T_java_lang_Integer T_java_lang_Integer))
(assert (javaSubType (_makeArrayType T_java_lang_Integer) (_makeArrayType T_java_lang_Integer)))
(assert (jmlSubType JMLT_java_lang_Integer JMLT_java_lang_Integer))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_Integer) (_makeJMLArrayType JMLT_java_lang_Integer)))
(assert (not (javaSubType T_java_lang_Integer T_java_lang_Exception)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Integer) (_makeArrayType T_java_lang_Exception))))
(assert (not (jmlSubType JMLT_java_lang_Integer JMLT_java_lang_Exception)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Integer) (_makeJMLArrayType JMLT_java_lang_Exception))))
(assert (forall ((e REF) ) (or (not (javaSubType (javaTypeOf e) T_java_lang_Integer)) (not (javaSubType (javaTypeOf e) T_java_lang_Exception)))))
(assert (not (javaSubType T_java_lang_Integer T_java_lang_Class)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Integer) (_makeArrayType T_java_lang_Class))))
(assert (not (javaSubType T_java_lang_Exception T_java_lang_RuntimeException)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Exception) (_makeArrayType T_java_lang_RuntimeException))))
(assert (not (jmlSubType JMLT_java_lang_Exception JMLT_java_lang_RuntimeException)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Exception) (_makeJMLArrayType JMLT_java_lang_RuntimeException))))
(assert (javaSubType T_java_lang_Exception T_java_lang_Object))
(assert (javaSubType (_makeArrayType T_java_lang_Exception) (_makeArrayType T_java_lang_Object)))
(assert (jmlSubType JMLT_java_lang_Exception JMLT_java_lang_Object))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_Exception) (_makeJMLArrayType JMLT_java_lang_Object)))
(assert (not (javaSubType T_java_lang_Exception T_int)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Exception) (_makeArrayType T_int))))
(assert (not (jmlSubType JMLT_java_lang_Exception JMLT_int)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Exception) (_makeJMLArrayType JMLT_int))))
(assert (not (javaSubType T_java_lang_Exception T_java_lang_Integer)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Exception) (_makeArrayType T_java_lang_Integer))))
(assert (not (jmlSubType JMLT_java_lang_Exception JMLT_java_lang_Integer)))
(assert (not (jmlSubType (_makeJMLArrayType JMLT_java_lang_Exception) (_makeJMLArrayType JMLT_java_lang_Integer))))
(assert (javaSubType T_java_lang_Exception T_java_lang_Exception))
(assert (javaSubType (_makeArrayType T_java_lang_Exception) (_makeArrayType T_java_lang_Exception)))
(assert (jmlSubType JMLT_java_lang_Exception JMLT_java_lang_Exception))
(assert (jmlSubType (_makeJMLArrayType JMLT_java_lang_Exception) (_makeJMLArrayType JMLT_java_lang_Exception)))
(assert (not (javaSubType T_java_lang_Exception T_java_lang_Class)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Exception) (_makeArrayType T_java_lang_Class))))
(assert (not (javaSubType T_java_lang_Class T_java_lang_RuntimeException)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Class) (_makeArrayType T_java_lang_RuntimeException))))
(assert (javaSubType T_java_lang_Class T_java_lang_Object))
(assert (javaSubType (_makeArrayType T_java_lang_Class) (_makeArrayType T_java_lang_Object)))
(assert (not (javaSubType T_java_lang_Class T_int)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Class) (_makeArrayType T_int))))
(assert (not (javaSubType T_java_lang_Class T_java_lang_Integer)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Class) (_makeArrayType T_java_lang_Integer))))
(assert (not (javaSubType T_java_lang_Class T_java_lang_Exception)))
(assert (not (javaSubType (_makeArrayType T_java_lang_Class) (_makeArrayType T_java_lang_Exception))))
(assert (javaSubType T_java_lang_Class T_java_lang_Class))
(assert (javaSubType (_makeArrayType T_java_lang_Class) (_makeArrayType T_java_lang_Class)))
(assert (forall ((t1 REF) (t2 REF) (t3 REF) ) (=> (and (javaSubType t1 t2) (javaSubType t2 t3)) (javaSubType t1 t3))))
(assert (forall ((t1 JMLTypeSort) (t2 JMLTypeSort) (t3 JMLTypeSort) ) (=> (and (jmlSubType t1 t2) (jmlSubType t2 t3)) (jmlSubType t1 t3))))
(assert (distinct T_java_lang_RuntimeException T_java_lang_Object T_int T_java_lang_Integer T_java_lang_Exception T_java_lang_Class))
(assert (distinct (_JMLT_0 T_java_lang_Integer) (_JMLT_0 T_java_lang_Exception) (_JMLT_0 T_java_lang_Object) (_JMLT_0 T_java_lang_RuntimeException) (_JMLT_1 T_java_lang_Class JMLT_java_lang_Integer) (_JMLT_0 T_int)))
(declare-fun |java.lang.Integer_MAX_VALUE| () Int)
(declare-fun |java.lang.Integer_BYTES| () Int)
(declare-fun |java.lang.Integer_SIZE| () Int)
(declare-fun |java.lang.Integer_MIN_VALUE| () Int)
(declare-fun |java.lang.Integer_MAX_UNSIGNED_INT| () Int)
(declare-fun |java.lang.Integer_TYPE| () REF)
(declare-fun |n_0_0___2| () Int)
(declare-fun |`exception_253_253___3| () REF)
(declare-fun |`terminationPosition_253_253___4| () Int)
(declare-fun |n_259_259___5| () Int)
(declare-fun |`result_253_253___6| () Int)
(declare-fun |j_409_409___7| () Int)
(declare-fun |total_270_270___8| () Int)
(declare-fun |BL_0_afterIf_3_source| () Int)
(declare-fun |Pre_1_169_154___9| () Bool)
(declare-fun |ASSERT_16| () Bool)
(declare-fun |BL_0_afterIf_6_source| () Int)
(declare-fun |total_270_270___10| () Int)
(declare-fun |j_409_409___11| () Int)
(declare-fun |index_400_5_400_400___12| () Int)
(declare-fun |ASSERT_18| () Bool)
(declare-fun |ASSERT_20| () Bool)
(declare-fun |index_400_5_400_428___13| () Int)
(declare-fun |j_409_423___14| () Int)
(declare-fun |total_270_533___15| () Int)
(declare-fun |index_400_5_400_428___16| () Int)
(declare-fun |ASSERT_28| () Bool)
(declare-fun |ASSERT_30| () Bool)
(declare-fun |ASSERT_33| () Bool)
(declare-fun |ASSERT_34| () Bool)
(declare-fun |total_270_533___17| () Int)
(declare-fun |ASSERT_36| () Bool)
(declare-fun |ASSERT_37| () Bool)
(declare-fun |j_409_423___18| () Int)
(declare-fun |index_400_5_400_400___19| () Int)
(declare-fun |ASSERT_38| () Bool)
(declare-fun |ASSERT_39| () Bool)
(declare-fun |ASSERT_40| () Bool)
(declare-fun |BL_400_LoopAfter_21_source| () Int)
(declare-fun |`result_253_552___20| () Int)
(declare-fun |`terminationPosition_253_552___21| () Int)
(declare-fun |`exception_253_552___22| () REF)
(declare-fun |BL_253_finally_12_source| () Int)
(declare-fun |__JMLsavedException_253_253_253___23| () REF)
(declare-fun |__JMLsavedTermination_253_253_253___24| () Int)
(declare-fun |ASSERT_41| () Bool)
(declare-fun |ASSERT_42| () Bool)
(declare-fun |BL_0_afterIf_31_source| () Int)
(declare-fun |ASSERT_43| () Bool)
(declare-fun |BL_0_afterIf_28_source| () Int)
(declare-fun |`exception_253_253___25| () REF)
(declare-fun |`terminationPosition_253_253___26| () Int)
(declare-fun |BL_253_AfterTry_10_source| () Int)
(declare-fun BL_253Start_1 () Bool)
(declare-fun BL_262bodyBegin_2 () Bool)
(declare-fun BL_0_then_4 () Bool)
(declare-fun BL_0_else_5 () Bool)
(declare-fun BL_0_afterIf_3 () Bool)
(declare-fun BL_0_then_7 () Bool)
(declare-fun BL_0_else_8 () Bool)
(declare-fun BL_0_afterIf_6 () Bool)
(declare-fun BL_253_AfterLabel_9 () Bool)
(declare-fun BL_428_AfterLabel_17 () Bool)
(declare-fun BL_400_LoopBody_18 () Bool)
(declare-fun BL_428_AfterLabel_22 () Bool)
(declare-fun BL_0_then_24 () Bool)
(declare-fun BL_0_else_25 () Bool)
(declare-fun BL_0_afterIf_23 () Bool)
(declare-fun BL_428_AfterLabel_26 () Bool)
(declare-fun BL_400_LoopContinue_19 () Bool)
(declare-fun BL_400_LoopEnd_20 () Bool)
(declare-fun BL_400_LoopAfter_21 () Bool)
(declare-fun BL_552_return_27 () Bool)
(declare-fun BL_253tryTarget_11 () Bool)
(declare-fun BL_253noException_13 () Bool)
(declare-fun BL_253nocatch_14 () Bool)
(declare-fun BL_253_finally_12 () Bool)
(declare-fun BL_0_then_29 () Bool)
(declare-fun BL_0_then_32 () Bool)
(declare-fun BL_0_else_33 () Bool)
(declare-fun BL_0_afterIf_31 () Bool)
(declare-fun BL_0_else_30 () Bool)
(declare-fun BL_0_afterIf_28 () Bool)
(declare-fun BL_253finallyNormal_15 () Bool)
(declare-fun BL_253finallyExit_16 () Bool)
(declare-fun BL_253_AfterTry_10 () Bool)
(assert (= BL_253Start_1 BL_262bodyBegin_2))
(declare-fun |__JML_AssumeCheck_| () Int)
(define-fun |_JML__tmp0| () REF |java.lang.Integer_TYPE|)
(define-fun |_JML__tmp1| () Bool (= |java.lang.Integer_TYPE| T_int))
(declare-fun |_JML__tmp2| () Bool)
(declare-fun |_JML__tmp3| () Bool)
(define-fun BL_262bodyBegin_2__A1 () Bool (= |`exception_253_253___3| NULL))
(define-fun BL_262bodyBegin_2__A2 () Bool (= |`terminationPosition_253_253___4| 0))
(define-fun BL_262bodyBegin_2__A3 () Bool (= |java.lang.Integer_MIN_VALUE| (- 2147483648)))
(define-fun BL_262bodyBegin_2__A4 () Bool (= |java.lang.Integer_MAX_VALUE| 2147483647))
(define-fun BL_262bodyBegin_2__A5 () Bool (= |java.lang.Integer_MAX_UNSIGNED_INT| 4294967295))
(define-fun BL_262bodyBegin_2__A6 () Bool (= |java.lang.Integer_SIZE| 32))
(define-fun BL_262bodyBegin_2__A7 () Bool (= |java.lang.Integer_BYTES| 4))
(define-fun BL_262bodyBegin_2__A8 () Bool (and (<= (- 2147483648) |j_409_409___7|) (<= |j_409_409___7| 2147483647)))
(define-fun BL_262bodyBegin_2__A9 () Bool (and (<= (- 2147483648) |total_270_270___8|) (<= |total_270_270___8| 2147483647)))
(define-fun BL_262bodyBegin_2__A10 () Bool |_JML__tmp1|)
(define-fun BL_262bodyBegin_2__A11 () Bool (and (<= (- 2147483648) |n_259_259___5|) (<= |n_259_259___5| 2147483647)))
(define-fun BL_262bodyBegin_2__A12 () Bool (= |_JML__tmp2| true))
(assert (= BL_262bodyBegin_2 (=> BL_262bodyBegin_2__A1 (=> BL_262bodyBegin_2__A2 (=> BL_262bodyBegin_2__A3 (=> BL_262bodyBegin_2__A4 (=> BL_262bodyBegin_2__A5 (=> BL_262bodyBegin_2__A6 (=> BL_262bodyBegin_2__A7 (=> BL_262bodyBegin_2__A8 (=> BL_262bodyBegin_2__A9 (=> BL_262bodyBegin_2__A10 (=> BL_262bodyBegin_2__A11 (=> BL_262bodyBegin_2__A12 (and BL_0_then_4 BL_0_else_5)))))))))))))))
(define-fun |_JML__tmp4| () Bool (and (< 0 |n_259_259___5|) (< |n_259_259___5| 100)))
(define-fun BL_0_then_4__A1 () Bool |_JML__tmp2|)
(define-fun BL_0_then_4__A2 () Bool (= |_JML__tmp3| |_JML__tmp4|))
(define-fun BL_0_then_4__A3 () Bool (= |BL_0_afterIf_3_source| 4))
(assert (= BL_0_then_4 (=> BL_0_then_4__A1 (=> BL_0_then_4__A2 (=> BL_0_then_4__A3 BL_0_afterIf_3)))))
(define-fun BL_0_else_5__A1 () Bool (not |_JML__tmp2|))
(define-fun BL_0_else_5__A2 () Bool (= |_JML__tmp3| false))
(define-fun BL_0_else_5__A3 () Bool (= |BL_0_afterIf_3_source| 5))
(assert (= BL_0_else_5 (=> BL_0_else_5__A1 (=> BL_0_else_5__A2 (=> BL_0_else_5__A3 BL_0_afterIf_3)))))
(define-fun BL_0_afterIf_3__A1 () Bool (= |Pre_1_169_154___9| |_JML__tmp3|))
(define-fun BL_0_afterIf_3__A2 () Bool |Pre_1_169_154___9|)
(define-fun BL_0_afterIf_3__A3 () Bool (= |ASSERT_16| (distinct |__JML_AssumeCheck_| 1)))
(assert (= BL_0_afterIf_3 (=> BL_0_afterIf_3__A1 (=> BL_0_afterIf_3__A2 (=> BL_0_afterIf_3__A3 (and |ASSERT_16| (=> |ASSERT_16| (and BL_0_then_7 BL_0_else_8))))))))
(define-fun BL_0_then_7__A1 () Bool |Pre_1_169_154___9|)
(define-fun BL_0_then_7__A2 () Bool (= |BL_0_afterIf_6_source| 7))
(assert (= BL_0_then_7 (=> BL_0_then_7__A1 (=> BL_0_then_7__A2 BL_0_afterIf_6))))
(define-fun BL_0_else_8__A1 () Bool (not |Pre_1_169_154___9|))
(define-fun BL_0_else_8__A2 () Bool (= |BL_0_afterIf_6_source| 8))
(assert (= BL_0_else_8 (=> BL_0_else_8__A1 (=> BL_0_else_8__A2 BL_0_afterIf_6))))
(assert (= BL_0_afterIf_6 BL_253_AfterLabel_9))
(define-fun BL_253_AfterLabel_9__A1 () Bool (= |total_270_270___10| 0))
(define-fun BL_253_AfterLabel_9__A2 () Bool (= |j_409_409___11| 0))
(define-fun BL_253_AfterLabel_9__A3 () Bool (= |index_400_5_400_400___12| 0))
(assert (= BL_253_AfterLabel_9 (=> BL_253_AfterLabel_9__A1 (=> BL_253_AfterLabel_9__A2 (=> BL_253_AfterLabel_9__A3 BL_428_AfterLabel_17)))))
(define-fun |_JML__tmp6| () Bool (and (<= 0 |j_409_409___11|) (<= |j_409_409___11| |n_259_259___5|)))
(define-fun-rec sum_0 ((lo Int)(|i| Int)) Int (ite (< |i| lo) 0 (+ (sum_0 lo (- |i| 1)) (ite (and (<= 0 |i|) (< |i| |j_409_409___11|)) |i| 0))))
(declare-fun |_JML__tmp8| () Int)
(assert (= |_JML__tmp8| (sum_0 0 1000)))
(define-fun |_JML__tmp9| () Bool (= |total_270_270___10| |_JML__tmp8|))
(define-fun BL_428_AfterLabel_17__A1 () Bool (= |ASSERT_18| |_JML__tmp6|))
(define-fun BL_428_AfterLabel_17__A2 () Bool (= |ASSERT_20| |_JML__tmp9|))
(assert (= BL_428_AfterLabel_17 (=> BL_428_AfterLabel_17__A1 (and |ASSERT_18| (=> |ASSERT_18| (=> BL_428_AfterLabel_17__A2 (and |ASSERT_20| (=> |ASSERT_20| (and BL_400_LoopBody_18 BL_400_LoopEnd_20)))))))))
(define-fun BL_400_LoopBody_18__A1 () Bool true)
(define-fun BL_400_LoopBody_18__A2 () Bool (and (<= (- 2147483648) |index_400_5_400_428___16|) (<= |index_400_5_400_428___16| 2147483647)))
(define-fun BL_400_LoopBody_18__A3 () Bool (and (<= (- 2147483648) |j_409_423___14|) (<= |j_409_423___14| 2147483647)))
(define-fun BL_400_LoopBody_18__A4 () Bool (and (<= (- 2147483648) |total_270_533___15|) (<= |total_270_533___15| 2147483647)))
(define-fun BL_400_LoopBody_18__A5 () Bool (and (<= (- 2147483648) |index_400_5_400_428___16|) (<= |index_400_5_400_428___16| 2147483647)))
(assert (= BL_400_LoopBody_18 (=> BL_400_LoopBody_18__A1 (=> BL_400_LoopBody_18__A2 (=> BL_400_LoopBody_18__A3 (=> BL_400_LoopBody_18__A4 (=> BL_400_LoopBody_18__A5 BL_428_AfterLabel_22)))))))
(define-fun |_JML__tmp10| () Bool (and (<= 0 |j_409_423___14|) (<= |j_409_423___14| |n_259_259___5|)))
(define-fun-rec sum_1 ((lo Int)(|i| Int)) Int (ite (< |i| lo) 0 (+ (sum_1 lo (- |i| 1)) (ite (and (<= 0 |i|) (< |i| |j_409_423___14|)) |i| 0))))
(declare-fun |_JML__tmp12| () Int)
(assert (= |_JML__tmp12| (sum_1 0 1000)))
(define-fun |_JML__tmp13| () Bool (= |total_270_533___15| |_JML__tmp12|))
(define-fun |_JML__tmp14| () Int (- |n_259_259___5| |j_409_423___14|))
(define-fun |_JML__tmp15| () Int |_JML__tmp14|)
(define-fun |_JML__tmp16| () Bool (< |j_409_423___14| |n_259_259___5|))
(define-fun BL_428_AfterLabel_22__A1 () Bool (<= 0 |index_400_5_400_428___16|))
(define-fun BL_428_AfterLabel_22__A2 () Bool |_JML__tmp10|)
(define-fun BL_428_AfterLabel_22__A3 () Bool |_JML__tmp13|)
(assert (= BL_428_AfterLabel_22 (=> BL_428_AfterLabel_22__A1 (=> BL_428_AfterLabel_22__A2 (=> BL_428_AfterLabel_22__A3 (and BL_0_then_24 BL_0_else_25))))))
(define-fun BL_0_then_24__A1 () Bool (not |_JML__tmp16|))
(define-fun BL_0_then_24__A2 () Bool (= |BL_400_LoopAfter_21_source| 24))
(assert (= BL_0_then_24 (=> BL_0_then_24__A1 (=> BL_0_then_24__A2 BL_400_LoopAfter_21))))
(define-fun BL_0_else_25__A1 () Bool (not (not |_JML__tmp16|)))
(assert (= BL_0_else_25 (=> BL_0_else_25__A1 BL_0_afterIf_23)))
(define-fun |_JML__tmp18| () Int (+ |total_270_533___15| |j_409_423___14|))
(define-fun |_JML__tmp19| () Bool (and (<= |java.lang.Integer_MIN_VALUE| |_JML__tmp18|) (<= |_JML__tmp18| |java.lang.Integer_MAX_VALUE|)))
(define-fun |_JML__tmp20| () Bool (or (not (and (< 0 |total_270_533___15|) (< 0 |j_409_423___14|))) (<= |total_270_533___15| (- 2147483647 |j_409_423___14|))))
(define-fun |_JML__tmp21| () Bool (or (not (and (< |total_270_533___15| 0) (< |j_409_423___14| 0))) (<= (- (- 2147483648) |j_409_423___14|) |total_270_533___15|)))
(define-fun |_JML__tmp22| () Int (ite (< 2147483647 (+ |total_270_533___15| |j_409_423___14|)) (+ (+ (+ |total_270_533___15| |j_409_423___14|) (- 2147483648)) (- 2147483648)) (ite (< (+ |total_270_533___15| |j_409_423___14|) (- 2147483648)) (- (- (+ |total_270_533___15| |j_409_423___14|) (- 2147483648)) (- 2147483648)) (+ |total_270_533___15| |j_409_423___14|))))
(define-fun BL_0_afterIf_23__A1 () Bool (= |ASSERT_28| (<= 0 |_JML__tmp15|)))
(define-fun BL_0_afterIf_23__A2 () Bool |_JML__tmp19|)
(define-fun BL_0_afterIf_23__A3 () Bool (= |ASSERT_30| (distinct |__JML_AssumeCheck_| 2)))
(define-fun BL_0_afterIf_23__A4 () Bool (and (<= (- 2147483648) |total_270_533___15|) (<= |total_270_533___15| 2147483647)))
(define-fun BL_0_afterIf_23__A5 () Bool (and (<= (- 2147483648) |j_409_423___14|) (<= |j_409_423___14| 2147483647)))
(define-fun BL_0_afterIf_23__A6 () Bool (= |ASSERT_33| (or (not (and (< 0 |total_270_533___15|) (< 0 |j_409_423___14|))) (<= |total_270_533___15| (- 2147483647 |j_409_423___14|)))))
(define-fun BL_0_afterIf_23__A7 () Bool (= |ASSERT_34| (or (not (and (< |total_270_533___15| 0) (< |j_409_423___14| 0))) (<= (- (- 2147483648) |j_409_423___14|) |total_270_533___15|))))
(define-fun BL_0_afterIf_23__A8 () Bool (= |total_270_533___17| |_JML__tmp22|))
(assert (= BL_0_afterIf_23 (=> BL_0_afterIf_23__A1 (and |ASSERT_28| (=> |ASSERT_28| (=> BL_0_afterIf_23__A2 (=> BL_0_afterIf_23__A3 (and |ASSERT_30| (=> |ASSERT_30| (=> BL_0_afterIf_23__A4 (=> BL_0_afterIf_23__A5 (=> BL_0_afterIf_23__A6 (and |ASSERT_33| (=> |ASSERT_33| (=> BL_0_afterIf_23__A7 (and |ASSERT_34| (=> |ASSERT_34| (=> BL_0_afterIf_23__A8 BL_428_AfterLabel_26))))))))))))))))))
(define-fun |_JML__tmp23| () Int |j_409_423___14|)
(define-fun |_JML__tmp24| () Bool (or (not (and (< 0 |j_409_423___14|) (< 0 1))) (<= |j_409_423___14| (- 2147483647 1))))
(define-fun |_JML__tmp25| () Bool (or (not (and (< |j_409_423___14| 0) (< 1 0))) (<= (- (- 2147483648) 1) |j_409_423___14|)))
(define-fun |_JML__tmp26| () Int (ite (< 2147483647 (+ |j_409_423___14| 1)) (+ (+ (+ |j_409_423___14| 1) (- 2147483648)) (- 2147483648)) (ite (< (+ |j_409_423___14| 1) (- 2147483648)) (- (- (+ |j_409_423___14| 1) (- 2147483648)) (- 2147483648)) (+ |j_409_423___14| 1))))
(define-fun |_JML__tmp27| () Int |j_409_423___18|)
(define-fun |_JML__tmp28| () Bool (and (<= 0 |j_409_423___18|) (<= |j_409_423___18| |n_259_259___5|)))
(define-fun-rec sum_2 ((lo Int)(|i| Int)) Int (ite (< |i| lo) 0 (+ (sum_2 lo (- |i| 1)) (ite (and (<= 0 |i|) (< |i| |j_409_423___18|)) |i| 0))))
(declare-fun |_JML__tmp30| () Int)
(assert (= |_JML__tmp30| (sum_2 0 1000)))
(define-fun |_JML__tmp31| () Bool (= |total_270_533___17| |_JML__tmp30|))
(define-fun |_JML__tmp32| () Int (- |n_259_259___5| |j_409_423___18|))
(define-fun |_JML__tmp33| () Int |_JML__tmp32|)
(define-fun BL_428_AfterLabel_26__A1 () Bool (and (<= (- 2147483648) |j_409_423___14|) (<= |j_409_423___14| 2147483647)))
(define-fun BL_428_AfterLabel_26__A2 () Bool (= |ASSERT_36| (or (not (and (< 0 |j_409_423___14|) (< 0 1))) (<= |j_409_423___14| (- 2147483647 1)))))
(define-fun BL_428_AfterLabel_26__A3 () Bool (= |ASSERT_37| (or (not (and (< |j_409_423___14| 0) (< 1 0))) (<= (- (- 2147483648) 1) |j_409_423___14|))))
(define-fun BL_428_AfterLabel_26__A4 () Bool (= |j_409_423___18| |_JML__tmp26|))
(define-fun BL_428_AfterLabel_26__A5 () Bool (= |index_400_5_400_400___19| (+ |index_400_5_400_428___16| 1)))
(define-fun BL_428_AfterLabel_26__A6 () Bool (= |ASSERT_38| |_JML__tmp28|))
(define-fun BL_428_AfterLabel_26__A7 () Bool (= |ASSERT_39| |_JML__tmp31|))
(define-fun BL_428_AfterLabel_26__A8 () Bool (= |ASSERT_40| (< |_JML__tmp33| |_JML__tmp15|)))
(assert (= BL_428_AfterLabel_26 (=> BL_428_AfterLabel_26__A1 (=> BL_428_AfterLabel_26__A2 (and |ASSERT_36| (=> |ASSERT_36| (=> BL_428_AfterLabel_26__A3 (and |ASSERT_37| (=> |ASSERT_37| (=> BL_428_AfterLabel_26__A4 (=> BL_428_AfterLabel_26__A5 (=> BL_428_AfterLabel_26__A6 (and |ASSERT_38| (=> |ASSERT_38| (=> BL_428_AfterLabel_26__A7 (and |ASSERT_39| (=> |ASSERT_39| (=> BL_428_AfterLabel_26__A8 (and |ASSERT_40| (=> |ASSERT_40| BL_400_LoopContinue_19))))))))))))))))))))
(assert (= BL_400_LoopContinue_19 true))
(define-fun BL_400_LoopEnd_20__A1 () Bool (not true))
(define-fun BL_400_LoopEnd_20__A2 () Bool (= |total_270_533___15| |total_270_270___10|))
(define-fun BL_400_LoopEnd_20__A3 () Bool (= |j_409_423___14| |j_409_409___11|))
(define-fun BL_400_LoopEnd_20__A4 () Bool (= |index_400_5_400_428___16| |index_400_5_400_400___12|))
(define-fun BL_400_LoopEnd_20__A5 () Bool (= |BL_400_LoopAfter_21_source| 20))
(assert (= BL_400_LoopEnd_20 (=> BL_400_LoopEnd_20__A1 (=> BL_400_LoopEnd_20__A2 (=> BL_400_LoopEnd_20__A3 (=> BL_400_LoopEnd_20__A4 (=> BL_400_LoopEnd_20__A5 BL_400_LoopAfter_21)))))))
(define-fun BL_400_LoopAfter_21__A1 () Bool (= |`result_253_552___20| |total_270_533___15|))
(define-fun BL_400_LoopAfter_21__A2 () Bool (= |`terminationPosition_253_552___21| 552))
(define-fun BL_400_LoopAfter_21__A3 () Bool (= |`exception_253_552___22| NULL))
(assert (= BL_400_LoopAfter_21 (=> BL_400_LoopAfter_21__A1 (=> BL_400_LoopAfter_21__A2 (=> BL_400_LoopAfter_21__A3 BL_552_return_27)))))
(assert (= BL_552_return_27 BL_253tryTarget_11))
(assert (= BL_253tryTarget_11 (and BL_253noException_13 BL_253nocatch_14)))
(define-fun BL_253noException_13__A1 () Bool (= |`exception_253_552___22| NULL))
(define-fun BL_253noException_13__A2 () Bool (= |BL_253_finally_12_source| 13))
(assert (= BL_253noException_13 (=> BL_253noException_13__A1 (=> BL_253noException_13__A2 BL_253_finally_12))))
(define-fun BL_253nocatch_14__A1 () Bool (distinct |`exception_253_552___22| NULL))
(define-fun BL_253nocatch_14__A2 () Bool (= |BL_253_finally_12_source| 14))
(assert (= BL_253nocatch_14 (=> BL_253nocatch_14__A1 (=> BL_253nocatch_14__A2 BL_253_finally_12))))
(define-fun BL_253_finally_12__A1 () Bool (= |__JMLsavedException_253_253_253___23| |`exception_253_552___22|))
(define-fun BL_253_finally_12__A2 () Bool (= |__JMLsavedTermination_253_253_253___24| |`terminationPosition_253_552___21|))
(define-fun BL_253_finally_12__A3 () Bool (= |ASSERT_41| (distinct |__JML_AssumeCheck_| 3)))
(assert (= BL_253_finally_12 (=> BL_253_finally_12__A1 (=> BL_253_finally_12__A2 (=> BL_253_finally_12__A3 (and |ASSERT_41| (=> |ASSERT_41| (and BL_0_then_29 BL_0_else_30))))))))
(define-fun BL_0_then_29__A1 () Bool (= |`exception_253_552___22| NULL))
(assert (= BL_0_then_29 (=> BL_0_then_29__A1 (and BL_0_then_32 BL_0_else_33))))
(define-fun-rec sum_3 ((lo Int)(|i| Int)) Int (ite (< |i| lo) 0 (+ (sum_3 lo (- |i| 1)) (ite (and (<= 0 |i|) (< |i| |n_259_259___5|)) |i| 0))))
(declare-fun |_JML__tmp35| () Int)
(assert (= |_JML__tmp35| (sum_3 0 1000)))
(define-fun |_JML__tmp36| () Bool (= |`result_253_552___20| |_JML__tmp35|))
(define-fun BL_0_then_32__A1 () Bool |Pre_1_169_154___9|)
(define-fun BL_0_then_32__A2 () Bool (= |ASSERT_42| |_JML__tmp36|))
(define-fun BL_0_then_32__A3 () Bool (= |BL_0_afterIf_31_source| 32))
(assert (= BL_0_then_32 (=> BL_0_then_32__A1 (=> BL_0_then_32__A2 (and |ASSERT_42| (=> |ASSERT_42| (=> BL_0_then_32__A3 BL_0_afterIf_31)))))))
(define-fun BL_0_else_33__A1 () Bool (not |Pre_1_169_154___9|))
(define-fun BL_0_else_33__A2 () Bool (= |BL_0_afterIf_31_source| 33))
(assert (= BL_0_else_33 (=> BL_0_else_33__A1 (=> BL_0_else_33__A2 BL_0_afterIf_31))))
(define-fun BL_0_afterIf_31__A1 () Bool (= |BL_0_afterIf_28_source| 31))
(assert (= BL_0_afterIf_31 (=> BL_0_afterIf_31__A1 BL_0_afterIf_28)))
(define-fun BL_0_else_30__A1 () Bool (not (= |`exception_253_552___22| NULL)))
(define-fun BL_0_else_30__A2 () Bool (= |ASSERT_43| (or (not (and (distinct |`exception_253_552___22| NULL) (javaSubType (javaTypeOf |`exception_253_552___22|) T_java_lang_Exception))) (or (not |Pre_1_169_154___9|) (or false (and (distinct |`exception_253_552___22| NULL) (javaSubType (javaTypeOf |`exception_253_552___22|) T_java_lang_RuntimeException)))))))
(define-fun BL_0_else_30__A3 () Bool (= |BL_0_afterIf_28_source| 30))
(assert (= BL_0_else_30 (=> BL_0_else_30__A1 (=> BL_0_else_30__A2 (and |ASSERT_43| (=> |ASSERT_43| (=> BL_0_else_30__A3 BL_0_afterIf_28)))))))
(define-fun BL_0_afterIf_28__A1 () Bool (= |`exception_253_253___25| |__JMLsavedException_253_253_253___23|))
(define-fun BL_0_afterIf_28__A2 () Bool (= |`terminationPosition_253_253___26| |__JMLsavedTermination_253_253_253___24|))
(assert (= BL_0_afterIf_28 (=> BL_0_afterIf_28__A1 (=> BL_0_afterIf_28__A2 (and BL_253finallyNormal_15 BL_253finallyExit_16)))))
(define-fun BL_253finallyNormal_15__A1 () Bool (= |`terminationPosition_253_253___26| 0))
(define-fun BL_253finallyNormal_15__A2 () Bool (= |BL_253_AfterTry_10_source| 15))
(assert (= BL_253finallyNormal_15 (=> BL_253finallyNormal_15__A1 (=> BL_253finallyNormal_15__A2 BL_253_AfterTry_10))))
(define-fun BL_253finallyExit_16__A1 () Bool (distinct |`terminationPosition_253_253___26| 0))
(define-fun BL_253finallyExit_16__A2 () Bool (= |BL_253_AfterTry_10_source| 16))
(assert (= BL_253finallyExit_16 (=> BL_253finallyExit_16__A1 (=> BL_253finallyExit_16__A2 BL_253_AfterTry_10))))
(assert (= BL_253_AfterTry_10 true))
(assert (not BL_253Start_1))
(push 1)
(assert (= __JML_AssumeCheck_ 0))
(push 1)
(check-sat)