src/HOL/SMT_Examples/Boogie_Max.b2i
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 52722 2c81f7baf8c4
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
boehmes@52722
     1
vc max 1
boehmes@52722
     2
    implies
boehmes@52722
     3
    label pos 10 7
boehmes@52722
     4
    true
boehmes@52722
     5
    implies
boehmes@52722
     6
    <
boehmes@52722
     7
    int-num 0
boehmes@52722
     8
    var length
boehmes@52722
     9
      int
boehmes@52722
    10
    implies
boehmes@52722
    11
    true
boehmes@52722
    12
    implies
boehmes@52722
    13
    =
boehmes@52722
    14
    var max@0
boehmes@52722
    15
      int
boehmes@52722
    16
    select 2
boehmes@52722
    17
    var array
boehmes@52722
    18
      array 2
boehmes@52722
    19
        int
boehmes@52722
    20
        int
boehmes@52722
    21
    int-num 0
boehmes@52722
    22
    implies
boehmes@52722
    23
    and 4
boehmes@52722
    24
    <=
boehmes@52722
    25
    int-num 0
boehmes@52722
    26
    int-num 0
boehmes@52722
    27
    <=
boehmes@52722
    28
    int-num 0
boehmes@52722
    29
    int-num 0
boehmes@52722
    30
    <=
boehmes@52722
    31
    int-num 1
boehmes@52722
    32
    int-num 1
boehmes@52722
    33
    <=
boehmes@52722
    34
    int-num 1
boehmes@52722
    35
    int-num 1
boehmes@52722
    36
    and 2
boehmes@52722
    37
    label neg 14 5
boehmes@52722
    38
    forall 1 0 3
boehmes@52722
    39
      var i
boehmes@52722
    40
        int
boehmes@52722
    41
      attribute qid 1
boehmes@52722
    42
        string-attr BoogieMa.14:23
boehmes@52722
    43
      attribute uniqueId 1
boehmes@52722
    44
        string-attr 2
boehmes@52722
    45
      attribute bvZ3Native 1
boehmes@52722
    46
        string-attr False
boehmes@52722
    47
    implies
boehmes@52722
    48
    and 2
boehmes@52722
    49
    <=
boehmes@52722
    50
    int-num 0
boehmes@52722
    51
    var i
boehmes@52722
    52
      int
boehmes@52722
    53
    <
boehmes@52722
    54
    var i
boehmes@52722
    55
      int
boehmes@52722
    56
    int-num 1
boehmes@52722
    57
    <=
boehmes@52722
    58
    select 2
boehmes@52722
    59
    var array
boehmes@52722
    60
      array 2
boehmes@52722
    61
        int
boehmes@52722
    62
        int
boehmes@52722
    63
    var i
boehmes@52722
    64
      int
boehmes@52722
    65
    var max@0
boehmes@52722
    66
      int
boehmes@52722
    67
    implies
boehmes@52722
    68
    forall 1 0 3
boehmes@52722
    69
      var i
boehmes@52722
    70
        int
boehmes@52722
    71
      attribute qid 1
boehmes@52722
    72
        string-attr BoogieMa.14:23
boehmes@52722
    73
      attribute uniqueId 1
boehmes@52722
    74
        string-attr 2
boehmes@52722
    75
      attribute bvZ3Native 1
boehmes@52722
    76
        string-attr False
boehmes@52722
    77
    implies
boehmes@52722
    78
    and 2
boehmes@52722
    79
    <=
boehmes@52722
    80
    int-num 0
boehmes@52722
    81
    var i
boehmes@52722
    82
      int
boehmes@52722
    83
    <
boehmes@52722
    84
    var i
boehmes@52722
    85
      int
boehmes@52722
    86
    int-num 1
boehmes@52722
    87
    <=
boehmes@52722
    88
    select 2
boehmes@52722
    89
    var array
boehmes@52722
    90
      array 2
boehmes@52722
    91
        int
boehmes@52722
    92
        int
boehmes@52722
    93
    var i
boehmes@52722
    94
      int
boehmes@52722
    95
    var max@0
boehmes@52722
    96
      int
boehmes@52722
    97
    and 2
boehmes@52722
    98
    label neg 15 5
boehmes@52722
    99
    =
boehmes@52722
   100
    select 2
boehmes@52722
   101
    var array
boehmes@52722
   102
      array 2
boehmes@52722
   103
        int
boehmes@52722
   104
        int
boehmes@52722
   105
    int-num 0
boehmes@52722
   106
    var max@0
boehmes@52722
   107
      int
boehmes@52722
   108
    implies
boehmes@52722
   109
    =
boehmes@52722
   110
    select 2
boehmes@52722
   111
    var array
boehmes@52722
   112
      array 2
boehmes@52722
   113
        int
boehmes@52722
   114
        int
boehmes@52722
   115
    int-num 0
boehmes@52722
   116
    var max@0
boehmes@52722
   117
      int
boehmes@52722
   118
    implies
boehmes@52722
   119
    label pos 13 3
boehmes@52722
   120
    true
boehmes@52722
   121
    implies
boehmes@52722
   122
    and 2
boehmes@52722
   123
    <=
boehmes@52722
   124
    int-num 0
boehmes@52722
   125
    var k@0
boehmes@52722
   126
      int
boehmes@52722
   127
    <=
boehmes@52722
   128
    int-num 1
boehmes@52722
   129
    var p@0
boehmes@52722
   130
      int
boehmes@52722
   131
    implies
boehmes@52722
   132
    forall 1 0 3
boehmes@52722
   133
      var i
boehmes@52722
   134
        int
boehmes@52722
   135
      attribute qid 1
boehmes@52722
   136
        string-attr BoogieMa.14:23
boehmes@52722
   137
      attribute uniqueId 1
boehmes@52722
   138
        string-attr 2
boehmes@52722
   139
      attribute bvZ3Native 1
boehmes@52722
   140
        string-attr False
boehmes@52722
   141
    implies
boehmes@52722
   142
    and 2
boehmes@52722
   143
    <=
boehmes@52722
   144
    int-num 0
boehmes@52722
   145
    var i
boehmes@52722
   146
      int
boehmes@52722
   147
    <
boehmes@52722
   148
    var i
boehmes@52722
   149
      int
boehmes@52722
   150
    var p@0
boehmes@52722
   151
      int
boehmes@52722
   152
    <=
boehmes@52722
   153
    select 2
boehmes@52722
   154
    var array
boehmes@52722
   155
      array 2
boehmes@52722
   156
        int
boehmes@52722
   157
        int
boehmes@52722
   158
    var i
boehmes@52722
   159
      int
boehmes@52722
   160
    var max@1
boehmes@52722
   161
      int
boehmes@52722
   162
    implies
boehmes@52722
   163
    =
boehmes@52722
   164
    select 2
boehmes@52722
   165
    var array
boehmes@52722
   166
      array 2
boehmes@52722
   167
        int
boehmes@52722
   168
        int
boehmes@52722
   169
    var k@0
boehmes@52722
   170
      int
boehmes@52722
   171
    var max@1
boehmes@52722
   172
      int
boehmes@52722
   173
    implies
boehmes@52722
   174
    and 2
boehmes@52722
   175
    <=
boehmes@52722
   176
    int-num 0
boehmes@52722
   177
    var k@0
boehmes@52722
   178
      int
boehmes@52722
   179
    <=
boehmes@52722
   180
    int-num 1
boehmes@52722
   181
    var p@0
boehmes@52722
   182
      int
boehmes@52722
   183
    and 2
boehmes@52722
   184
    implies
boehmes@52722
   185
    label pos 13 3
boehmes@52722
   186
    true
boehmes@52722
   187
    implies
boehmes@52722
   188
    and 2
boehmes@52722
   189
    <=
boehmes@52722
   190
    int-num 0
boehmes@52722
   191
    var k@0
boehmes@52722
   192
      int
boehmes@52722
   193
    <=
boehmes@52722
   194
    int-num 1
boehmes@52722
   195
    var p@0
boehmes@52722
   196
      int
boehmes@52722
   197
    implies
boehmes@52722
   198
    >=
boehmes@52722
   199
    var p@0
boehmes@52722
   200
      int
boehmes@52722
   201
    var length
boehmes@52722
   202
      int
boehmes@52722
   203
    implies
boehmes@52722
   204
    and 2
boehmes@52722
   205
    <=
boehmes@52722
   206
    int-num 0
boehmes@52722
   207
    var k@0
boehmes@52722
   208
      int
boehmes@52722
   209
    <=
boehmes@52722
   210
    int-num 1
boehmes@52722
   211
    var p@0
boehmes@52722
   212
      int
boehmes@52722
   213
    implies
boehmes@52722
   214
    label pos 0 0
boehmes@52722
   215
    true
boehmes@52722
   216
    implies
boehmes@52722
   217
    =
boehmes@52722
   218
    var k@2
boehmes@52722
   219
      int
boehmes@52722
   220
    var k@0
boehmes@52722
   221
      int
boehmes@52722
   222
    implies
boehmes@52722
   223
    =
boehmes@52722
   224
    var max@4
boehmes@52722
   225
      int
boehmes@52722
   226
    var max@1
boehmes@52722
   227
      int
boehmes@52722
   228
    implies
boehmes@52722
   229
    =
boehmes@52722
   230
    var p@2
boehmes@52722
   231
      int
boehmes@52722
   232
    var p@0
boehmes@52722
   233
      int
boehmes@52722
   234
    implies
boehmes@52722
   235
    label pos 0 0
boehmes@52722
   236
    true
boehmes@52722
   237
    and 2
boehmes@52722
   238
    label neg 5 3
boehmes@52722
   239
    exists 1 0 3
boehmes@52722
   240
      var i
boehmes@52722
   241
        int
boehmes@52722
   242
      attribute qid 1
boehmes@52722
   243
        string-attr BoogieMa.5:19
boehmes@52722
   244
      attribute uniqueId 1
boehmes@52722
   245
        string-attr 1
boehmes@52722
   246
      attribute bvZ3Native 1
boehmes@52722
   247
        string-attr False
boehmes@52722
   248
    implies
boehmes@52722
   249
    and 2
boehmes@52722
   250
    <=
boehmes@52722
   251
    int-num 0
boehmes@52722
   252
    var i
boehmes@52722
   253
      int
boehmes@52722
   254
    <
boehmes@52722
   255
    var i
boehmes@52722
   256
      int
boehmes@52722
   257
    var length
boehmes@52722
   258
      int
boehmes@52722
   259
    =
boehmes@52722
   260
    select 2
boehmes@52722
   261
    var array
boehmes@52722
   262
      array 2
boehmes@52722
   263
        int
boehmes@52722
   264
        int
boehmes@52722
   265
    var i
boehmes@52722
   266
      int
boehmes@52722
   267
    var max@4
boehmes@52722
   268
      int
boehmes@52722
   269
    implies
boehmes@52722
   270
    exists 1 0 3
boehmes@52722
   271
      var i
boehmes@52722
   272
        int
boehmes@52722
   273
      attribute qid 1
boehmes@52722
   274
        string-attr BoogieMa.5:19
boehmes@52722
   275
      attribute uniqueId 1
boehmes@52722
   276
        string-attr 1
boehmes@52722
   277
      attribute bvZ3Native 1
boehmes@52722
   278
        string-attr False
boehmes@52722
   279
    implies
boehmes@52722
   280
    and 2
boehmes@52722
   281
    <=
boehmes@52722
   282
    int-num 0
boehmes@52722
   283
    var i
boehmes@52722
   284
      int
boehmes@52722
   285
    <
boehmes@52722
   286
    var i
boehmes@52722
   287
      int
boehmes@52722
   288
    var length
boehmes@52722
   289
      int
boehmes@52722
   290
    =
boehmes@52722
   291
    select 2
boehmes@52722
   292
    var array
boehmes@52722
   293
      array 2
boehmes@52722
   294
        int
boehmes@52722
   295
        int
boehmes@52722
   296
    var i
boehmes@52722
   297
      int
boehmes@52722
   298
    var max@4
boehmes@52722
   299
      int
boehmes@52722
   300
    and 2
boehmes@52722
   301
    label neg 4 3
boehmes@52722
   302
    forall 1 0 3
boehmes@52722
   303
      var i
boehmes@52722
   304
        int
boehmes@52722
   305
      attribute qid 1
boehmes@52722
   306
        string-attr BoogieMa.4:19
boehmes@52722
   307
      attribute uniqueId 1
boehmes@52722
   308
        string-attr 0
boehmes@52722
   309
      attribute bvZ3Native 1
boehmes@52722
   310
        string-attr False
boehmes@52722
   311
    implies
boehmes@52722
   312
    and 2
boehmes@52722
   313
    <=
boehmes@52722
   314
    int-num 0
boehmes@52722
   315
    var i
boehmes@52722
   316
      int
boehmes@52722
   317
    <
boehmes@52722
   318
    var i
boehmes@52722
   319
      int
boehmes@52722
   320
    var length
boehmes@52722
   321
      int
boehmes@52722
   322
    <=
boehmes@52722
   323
    select 2
boehmes@52722
   324
    var array
boehmes@52722
   325
      array 2
boehmes@52722
   326
        int
boehmes@52722
   327
        int
boehmes@52722
   328
    var i
boehmes@52722
   329
      int
boehmes@52722
   330
    var max@4
boehmes@52722
   331
      int
boehmes@52722
   332
    implies
boehmes@52722
   333
    forall 1 0 3
boehmes@52722
   334
      var i
boehmes@52722
   335
        int
boehmes@52722
   336
      attribute qid 1
boehmes@52722
   337
        string-attr BoogieMa.4:19
boehmes@52722
   338
      attribute uniqueId 1
boehmes@52722
   339
        string-attr 0
boehmes@52722
   340
      attribute bvZ3Native 1
boehmes@52722
   341
        string-attr False
boehmes@52722
   342
    implies
boehmes@52722
   343
    and 2
boehmes@52722
   344
    <=
boehmes@52722
   345
    int-num 0
boehmes@52722
   346
    var i
boehmes@52722
   347
      int
boehmes@52722
   348
    <
boehmes@52722
   349
    var i
boehmes@52722
   350
      int
boehmes@52722
   351
    var length
boehmes@52722
   352
      int
boehmes@52722
   353
    <=
boehmes@52722
   354
    select 2
boehmes@52722
   355
    var array
boehmes@52722
   356
      array 2
boehmes@52722
   357
        int
boehmes@52722
   358
        int
boehmes@52722
   359
    var i
boehmes@52722
   360
      int
boehmes@52722
   361
    var max@4
boehmes@52722
   362
      int
boehmes@52722
   363
    true
boehmes@52722
   364
    implies
boehmes@52722
   365
    label pos 17 5
boehmes@52722
   366
    true
boehmes@52722
   367
    implies
boehmes@52722
   368
    and 2
boehmes@52722
   369
    <=
boehmes@52722
   370
    int-num 0
boehmes@52722
   371
    var k@0
boehmes@52722
   372
      int
boehmes@52722
   373
    <=
boehmes@52722
   374
    int-num 1
boehmes@52722
   375
    var p@0
boehmes@52722
   376
      int
boehmes@52722
   377
    implies
boehmes@52722
   378
    <
boehmes@52722
   379
    var p@0
boehmes@52722
   380
      int
boehmes@52722
   381
    var length
boehmes@52722
   382
      int
boehmes@52722
   383
    implies
boehmes@52722
   384
    and 2
boehmes@52722
   385
    <=
boehmes@52722
   386
    int-num 0
boehmes@52722
   387
    var k@0
boehmes@52722
   388
      int
boehmes@52722
   389
    <=
boehmes@52722
   390
    int-num 1
boehmes@52722
   391
    var p@0
boehmes@52722
   392
      int
boehmes@52722
   393
    and 2
boehmes@52722
   394
    implies
boehmes@52722
   395
    label pos 17 31
boehmes@52722
   396
    true
boehmes@52722
   397
    implies
boehmes@52722
   398
    and 2
boehmes@52722
   399
    <=
boehmes@52722
   400
    int-num 0
boehmes@52722
   401
    var k@0
boehmes@52722
   402
      int
boehmes@52722
   403
    <=
boehmes@52722
   404
    int-num 1
boehmes@52722
   405
    var p@0
boehmes@52722
   406
      int
boehmes@52722
   407
    implies
boehmes@52722
   408
    >
boehmes@52722
   409
    select 2
boehmes@52722
   410
    var array
boehmes@52722
   411
      array 2
boehmes@52722
   412
        int
boehmes@52722
   413
        int
boehmes@52722
   414
    var p@0
boehmes@52722
   415
      int
boehmes@52722
   416
    var max@1
boehmes@52722
   417
      int
boehmes@52722
   418
    implies
boehmes@52722
   419
    =
boehmes@52722
   420
    var max@2
boehmes@52722
   421
      int
boehmes@52722
   422
    select 2
boehmes@52722
   423
    var array
boehmes@52722
   424
      array 2
boehmes@52722
   425
        int
boehmes@52722
   426
        int
boehmes@52722
   427
    var p@0
boehmes@52722
   428
      int
boehmes@52722
   429
    implies
boehmes@52722
   430
    and 2
boehmes@52722
   431
    <=
boehmes@52722
   432
    int-num 1
boehmes@52722
   433
    var p@0
boehmes@52722
   434
      int
boehmes@52722
   435
    <=
boehmes@52722
   436
    int-num 1
boehmes@52722
   437
    var p@0
boehmes@52722
   438
      int
boehmes@52722
   439
    implies
boehmes@52722
   440
    label pos 0 0
boehmes@52722
   441
    true
boehmes@52722
   442
    implies
boehmes@52722
   443
    =
boehmes@52722
   444
    var k@1
boehmes@52722
   445
      int
boehmes@52722
   446
    var p@0
boehmes@52722
   447
      int
boehmes@52722
   448
    implies
boehmes@52722
   449
    =
boehmes@52722
   450
    var max@3
boehmes@52722
   451
      int
boehmes@52722
   452
    var max@2
boehmes@52722
   453
      int
boehmes@52722
   454
    implies
boehmes@52722
   455
    label pos 18 7
boehmes@52722
   456
    true
boehmes@52722
   457
    implies
boehmes@52722
   458
    and 2
boehmes@52722
   459
    <=
boehmes@52722
   460
    int-num 0
boehmes@52722
   461
    var k@1
boehmes@52722
   462
      int
boehmes@52722
   463
    <=
boehmes@52722
   464
    int-num 1
boehmes@52722
   465
    var p@0
boehmes@52722
   466
      int
boehmes@52722
   467
    implies
boehmes@52722
   468
    =
boehmes@52722
   469
    var p@1
boehmes@52722
   470
      int
boehmes@52722
   471
    +
boehmes@52722
   472
    var p@0
boehmes@52722
   473
      int
boehmes@52722
   474
    int-num 1
boehmes@52722
   475
    implies
boehmes@52722
   476
    and 2
boehmes@52722
   477
    <=
boehmes@52722
   478
    int-num 0
boehmes@52722
   479
    var k@1
boehmes@52722
   480
      int
boehmes@52722
   481
    <=
boehmes@52722
   482
    int-num 2
boehmes@52722
   483
    var p@1
boehmes@52722
   484
      int
boehmes@52722
   485
    implies
boehmes@52722
   486
    label pos 0 0
boehmes@52722
   487
    true
boehmes@52722
   488
    and 2
boehmes@52722
   489
    label neg 14 5
boehmes@52722
   490
    forall 1 0 3
boehmes@52722
   491
      var i
boehmes@52722
   492
        int
boehmes@52722
   493
      attribute qid 1
boehmes@52722
   494
        string-attr BoogieMa.14:23
boehmes@52722
   495
      attribute uniqueId 1
boehmes@52722
   496
        string-attr 2
boehmes@52722
   497
      attribute bvZ3Native 1
boehmes@52722
   498
        string-attr False
boehmes@52722
   499
    implies
boehmes@52722
   500
    and 2
boehmes@52722
   501
    <=
boehmes@52722
   502
    int-num 0
boehmes@52722
   503
    var i
boehmes@52722
   504
      int
boehmes@52722
   505
    <
boehmes@52722
   506
    var i
boehmes@52722
   507
      int
boehmes@52722
   508
    var p@1
boehmes@52722
   509
      int
boehmes@52722
   510
    <=
boehmes@52722
   511
    select 2
boehmes@52722
   512
    var array
boehmes@52722
   513
      array 2
boehmes@52722
   514
        int
boehmes@52722
   515
        int
boehmes@52722
   516
    var i
boehmes@52722
   517
      int
boehmes@52722
   518
    var max@3
boehmes@52722
   519
      int
boehmes@52722
   520
    implies
boehmes@52722
   521
    forall 1 0 3
boehmes@52722
   522
      var i
boehmes@52722
   523
        int
boehmes@52722
   524
      attribute qid 1
boehmes@52722
   525
        string-attr BoogieMa.14:23
boehmes@52722
   526
      attribute uniqueId 1
boehmes@52722
   527
        string-attr 2
boehmes@52722
   528
      attribute bvZ3Native 1
boehmes@52722
   529
        string-attr False
boehmes@52722
   530
    implies
boehmes@52722
   531
    and 2
boehmes@52722
   532
    <=
boehmes@52722
   533
    int-num 0
boehmes@52722
   534
    var i
boehmes@52722
   535
      int
boehmes@52722
   536
    <
boehmes@52722
   537
    var i
boehmes@52722
   538
      int
boehmes@52722
   539
    var p@1
boehmes@52722
   540
      int
boehmes@52722
   541
    <=
boehmes@52722
   542
    select 2
boehmes@52722
   543
    var array
boehmes@52722
   544
      array 2
boehmes@52722
   545
        int
boehmes@52722
   546
        int
boehmes@52722
   547
    var i
boehmes@52722
   548
      int
boehmes@52722
   549
    var max@3
boehmes@52722
   550
      int
boehmes@52722
   551
    and 2
boehmes@52722
   552
    label neg 15 5
boehmes@52722
   553
    =
boehmes@52722
   554
    select 2
boehmes@52722
   555
    var array
boehmes@52722
   556
      array 2
boehmes@52722
   557
        int
boehmes@52722
   558
        int
boehmes@52722
   559
    var k@1
boehmes@52722
   560
      int
boehmes@52722
   561
    var max@3
boehmes@52722
   562
      int
boehmes@52722
   563
    implies
boehmes@52722
   564
    =
boehmes@52722
   565
    select 2
boehmes@52722
   566
    var array
boehmes@52722
   567
      array 2
boehmes@52722
   568
        int
boehmes@52722
   569
        int
boehmes@52722
   570
    var k@1
boehmes@52722
   571
      int
boehmes@52722
   572
    var max@3
boehmes@52722
   573
      int
boehmes@52722
   574
    implies
boehmes@52722
   575
    false
boehmes@52722
   576
    true
boehmes@52722
   577
    implies
boehmes@52722
   578
    label pos 17 5
boehmes@52722
   579
    true
boehmes@52722
   580
    implies
boehmes@52722
   581
    and 2
boehmes@52722
   582
    <=
boehmes@52722
   583
    int-num 0
boehmes@52722
   584
    var k@0
boehmes@52722
   585
      int
boehmes@52722
   586
    <=
boehmes@52722
   587
    int-num 1
boehmes@52722
   588
    var p@0
boehmes@52722
   589
      int
boehmes@52722
   590
    implies
boehmes@52722
   591
    <=
boehmes@52722
   592
    select 2
boehmes@52722
   593
    var array
boehmes@52722
   594
      array 2
boehmes@52722
   595
        int
boehmes@52722
   596
        int
boehmes@52722
   597
    var p@0
boehmes@52722
   598
      int
boehmes@52722
   599
    var max@1
boehmes@52722
   600
      int
boehmes@52722
   601
    implies
boehmes@52722
   602
    and 2
boehmes@52722
   603
    <=
boehmes@52722
   604
    int-num 0
boehmes@52722
   605
    var k@0
boehmes@52722
   606
      int
boehmes@52722
   607
    <=
boehmes@52722
   608
    int-num 1
boehmes@52722
   609
    var p@0
boehmes@52722
   610
      int
boehmes@52722
   611
    implies
boehmes@52722
   612
    label pos 0 0
boehmes@52722
   613
    true
boehmes@52722
   614
    implies
boehmes@52722
   615
    =
boehmes@52722
   616
    var k@1
boehmes@52722
   617
      int
boehmes@52722
   618
    var k@0
boehmes@52722
   619
      int
boehmes@52722
   620
    implies
boehmes@52722
   621
    =
boehmes@52722
   622
    var max@3
boehmes@52722
   623
      int
boehmes@52722
   624
    var max@1
boehmes@52722
   625
      int
boehmes@52722
   626
    implies
boehmes@52722
   627
    label pos 18 7
boehmes@52722
   628
    true
boehmes@52722
   629
    implies
boehmes@52722
   630
    and 2
boehmes@52722
   631
    <=
boehmes@52722
   632
    int-num 0
boehmes@52722
   633
    var k@1
boehmes@52722
   634
      int
boehmes@52722
   635
    <=
boehmes@52722
   636
    int-num 1
boehmes@52722
   637
    var p@0
boehmes@52722
   638
      int
boehmes@52722
   639
    implies
boehmes@52722
   640
    =
boehmes@52722
   641
    var p@1
boehmes@52722
   642
      int
boehmes@52722
   643
    +
boehmes@52722
   644
    var p@0
boehmes@52722
   645
      int
boehmes@52722
   646
    int-num 1
boehmes@52722
   647
    implies
boehmes@52722
   648
    and 2
boehmes@52722
   649
    <=
boehmes@52722
   650
    int-num 0
boehmes@52722
   651
    var k@1
boehmes@52722
   652
      int
boehmes@52722
   653
    <=
boehmes@52722
   654
    int-num 2
boehmes@52722
   655
    var p@1
boehmes@52722
   656
      int
boehmes@52722
   657
    implies
boehmes@52722
   658
    label pos 0 0
boehmes@52722
   659
    true
boehmes@52722
   660
    and 2
boehmes@52722
   661
    label neg 14 5
boehmes@52722
   662
    forall 1 0 3
boehmes@52722
   663
      var i
boehmes@52722
   664
        int
boehmes@52722
   665
      attribute qid 1
boehmes@52722
   666
        string-attr BoogieMa.14:23
boehmes@52722
   667
      attribute uniqueId 1
boehmes@52722
   668
        string-attr 2
boehmes@52722
   669
      attribute bvZ3Native 1
boehmes@52722
   670
        string-attr False
boehmes@52722
   671
    implies
boehmes@52722
   672
    and 2
boehmes@52722
   673
    <=
boehmes@52722
   674
    int-num 0
boehmes@52722
   675
    var i
boehmes@52722
   676
      int
boehmes@52722
   677
    <
boehmes@52722
   678
    var i
boehmes@52722
   679
      int
boehmes@52722
   680
    var p@1
boehmes@52722
   681
      int
boehmes@52722
   682
    <=
boehmes@52722
   683
    select 2
boehmes@52722
   684
    var array
boehmes@52722
   685
      array 2
boehmes@52722
   686
        int
boehmes@52722
   687
        int
boehmes@52722
   688
    var i
boehmes@52722
   689
      int
boehmes@52722
   690
    var max@3
boehmes@52722
   691
      int
boehmes@52722
   692
    implies
boehmes@52722
   693
    forall 1 0 3
boehmes@52722
   694
      var i
boehmes@52722
   695
        int
boehmes@52722
   696
      attribute qid 1
boehmes@52722
   697
        string-attr BoogieMa.14:23
boehmes@52722
   698
      attribute uniqueId 1
boehmes@52722
   699
        string-attr 2
boehmes@52722
   700
      attribute bvZ3Native 1
boehmes@52722
   701
        string-attr False
boehmes@52722
   702
    implies
boehmes@52722
   703
    and 2
boehmes@52722
   704
    <=
boehmes@52722
   705
    int-num 0
boehmes@52722
   706
    var i
boehmes@52722
   707
      int
boehmes@52722
   708
    <
boehmes@52722
   709
    var i
boehmes@52722
   710
      int
boehmes@52722
   711
    var p@1
boehmes@52722
   712
      int
boehmes@52722
   713
    <=
boehmes@52722
   714
    select 2
boehmes@52722
   715
    var array
boehmes@52722
   716
      array 2
boehmes@52722
   717
        int
boehmes@52722
   718
        int
boehmes@52722
   719
    var i
boehmes@52722
   720
      int
boehmes@52722
   721
    var max@3
boehmes@52722
   722
      int
boehmes@52722
   723
    and 2
boehmes@52722
   724
    label neg 15 5
boehmes@52722
   725
    =
boehmes@52722
   726
    select 2
boehmes@52722
   727
    var array
boehmes@52722
   728
      array 2
boehmes@52722
   729
        int
boehmes@52722
   730
        int
boehmes@52722
   731
    var k@1
boehmes@52722
   732
      int
boehmes@52722
   733
    var max@3
boehmes@52722
   734
      int
boehmes@52722
   735
    implies
boehmes@52722
   736
    =
boehmes@52722
   737
    select 2
boehmes@52722
   738
    var array
boehmes@52722
   739
      array 2
boehmes@52722
   740
        int
boehmes@52722
   741
        int
boehmes@52722
   742
    var k@1
boehmes@52722
   743
      int
boehmes@52722
   744
    var max@3
boehmes@52722
   745
      int
boehmes@52722
   746
    implies
boehmes@52722
   747
    false
boehmes@52722
   748
    true