src/HOL/SMT_Examples/Boogie_Dijkstra.b2i
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 52722 2c81f7baf8c4
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     1 type-decl Vertex 0 0
     2 fun-decl G 1 0
     3     array 3
     4       type-con Vertex 0
     5       type-con Vertex 0
     6       int
     7 fun-decl Infinity 1 0
     8     int
     9 fun-decl Source 1 0
    10     type-con Vertex 0
    11 axiom 0
    12     forall 2 0 3
    13       var x
    14         type-con Vertex 0
    15       var y
    16         type-con Vertex 0
    17       attribute qid 1
    18         string-attr BoogieDi.3:15
    19       attribute uniqueId 1
    20         string-attr 0
    21       attribute bvZ3Native 1
    22         string-attr False
    23     implies
    24     not
    25     =
    26     var x
    27       type-con Vertex 0
    28     var y
    29       type-con Vertex 0
    30     <
    31     int-num 0
    32     select 3
    33     fun G 0
    34     var x
    35       type-con Vertex 0
    36     var y
    37       type-con Vertex 0
    38 axiom 0
    39     forall 2 0 3
    40       var x
    41         type-con Vertex 0
    42       var y
    43         type-con Vertex 0
    44       attribute qid 1
    45         string-attr BoogieDi.4:15
    46       attribute uniqueId 1
    47         string-attr 1
    48       attribute bvZ3Native 1
    49         string-attr False
    50     implies
    51     =
    52     var x
    53       type-con Vertex 0
    54     var y
    55       type-con Vertex 0
    56     =
    57     select 3
    58     fun G 0
    59     var x
    60       type-con Vertex 0
    61     var y
    62       type-con Vertex 0
    63     int-num 0
    64 axiom 0
    65     <
    66     int-num 0
    67     fun Infinity 0
    68 var-decl SP 0
    69     array 2
    70       type-con Vertex 0
    71       int
    72 vc Dijkstra 1
    73     implies
    74     label pos 26 3
    75     true
    76     implies
    77     true
    78     implies
    79     forall 1 0 3
    80       var x
    81         type-con Vertex 0
    82       attribute qid 1
    83         string-attr BoogieDi.27:18
    84       attribute uniqueId 1
    85         string-attr 5
    86       attribute bvZ3Native 1
    87         string-attr False
    88     implies
    89     =
    90     var x
    91       type-con Vertex 0
    92     fun Source 0
    93     =
    94     select 2
    95     var SP@0
    96       array 2
    97         type-con Vertex 0
    98         int
    99     var x
   100       type-con Vertex 0
   101     int-num 0
   102     implies
   103     forall 1 0 3
   104       var x
   105         type-con Vertex 0
   106       attribute qid 1
   107         string-attr BoogieDi.28:18
   108       attribute uniqueId 1
   109         string-attr 6
   110       attribute bvZ3Native 1
   111         string-attr False
   112     implies
   113     not
   114     =
   115     var x
   116       type-con Vertex 0
   117     fun Source 0
   118     =
   119     select 2
   120     var SP@0
   121       array 2
   122         type-con Vertex 0
   123         int
   124     var x
   125       type-con Vertex 0
   126     fun Infinity 0
   127     implies
   128     forall 1 0 3
   129       var x
   130         type-con Vertex 0
   131       attribute qid 1
   132         string-attr BoogieDi.31:18
   133       attribute uniqueId 1
   134         string-attr 7
   135       attribute bvZ3Native 1
   136         string-attr False
   137     not
   138     select 2
   139     var Visited@0
   140       array 2
   141         type-con Vertex 0
   142         bool
   143     var x
   144       type-con Vertex 0
   145     implies
   146     true
   147     and 2
   148     label neg 34 5
   149     =
   150     select 2
   151     var SP@0
   152       array 2
   153         type-con Vertex 0
   154         int
   155     fun Source 0
   156     int-num 0
   157     implies
   158     =
   159     select 2
   160     var SP@0
   161       array 2
   162         type-con Vertex 0
   163         int
   164     fun Source 0
   165     int-num 0
   166     and 2
   167     label neg 35 5
   168     forall 1 0 3
   169       var x
   170         type-con Vertex 0
   171       attribute qid 1
   172         string-attr BoogieDi.35:23
   173       attribute uniqueId 1
   174         string-attr 9
   175       attribute bvZ3Native 1
   176         string-attr False
   177     >=
   178     select 2
   179     var SP@0
   180       array 2
   181         type-con Vertex 0
   182         int
   183     var x
   184       type-con Vertex 0
   185     int-num 0
   186     implies
   187     forall 1 0 3
   188       var x
   189         type-con Vertex 0
   190       attribute qid 1
   191         string-attr BoogieDi.35:23
   192       attribute uniqueId 1
   193         string-attr 9
   194       attribute bvZ3Native 1
   195         string-attr False
   196     >=
   197     select 2
   198     var SP@0
   199       array 2
   200         type-con Vertex 0
   201         int
   202     var x
   203       type-con Vertex 0
   204     int-num 0
   205     and 2
   206     label neg 36 5
   207     forall 2 0 3
   208       var y
   209         type-con Vertex 0
   210       var z
   211         type-con Vertex 0
   212       attribute qid 1
   213         string-attr BoogieDi.36:23
   214       attribute uniqueId 1
   215         string-attr 10
   216       attribute bvZ3Native 1
   217         string-attr False
   218     implies
   219     and 2
   220     not
   221     select 2
   222     var Visited@0
   223       array 2
   224         type-con Vertex 0
   225         bool
   226     var z
   227       type-con Vertex 0
   228     select 2
   229     var Visited@0
   230       array 2
   231         type-con Vertex 0
   232         bool
   233     var y
   234       type-con Vertex 0
   235     <=
   236     select 2
   237     var SP@0
   238       array 2
   239         type-con Vertex 0
   240         int
   241     var y
   242       type-con Vertex 0
   243     select 2
   244     var SP@0
   245       array 2
   246         type-con Vertex 0
   247         int
   248     var z
   249       type-con Vertex 0
   250     implies
   251     forall 2 0 3
   252       var y
   253         type-con Vertex 0
   254       var z
   255         type-con Vertex 0
   256       attribute qid 1
   257         string-attr BoogieDi.36:23
   258       attribute uniqueId 1
   259         string-attr 10
   260       attribute bvZ3Native 1
   261         string-attr False
   262     implies
   263     and 2
   264     not
   265     select 2
   266     var Visited@0
   267       array 2
   268         type-con Vertex 0
   269         bool
   270     var z
   271       type-con Vertex 0
   272     select 2
   273     var Visited@0
   274       array 2
   275         type-con Vertex 0
   276         bool
   277     var y
   278       type-con Vertex 0
   279     <=
   280     select 2
   281     var SP@0
   282       array 2
   283         type-con Vertex 0
   284         int
   285     var y
   286       type-con Vertex 0
   287     select 2
   288     var SP@0
   289       array 2
   290         type-con Vertex 0
   291         int
   292     var z
   293       type-con Vertex 0
   294     and 2
   295     label neg 38 5
   296     forall 2 0 3
   297       var z
   298         type-con Vertex 0
   299       var y
   300         type-con Vertex 0
   301       attribute qid 1
   302         string-attr BoogieDi.38:23
   303       attribute uniqueId 1
   304         string-attr 11
   305       attribute bvZ3Native 1
   306         string-attr False
   307     implies
   308     and 2
   309     select 2
   310     var Visited@0
   311       array 2
   312         type-con Vertex 0
   313         bool
   314     var y
   315       type-con Vertex 0
   316     <
   317     select 3
   318     fun G 0
   319     var y
   320       type-con Vertex 0
   321     var z
   322       type-con Vertex 0
   323     fun Infinity 0
   324     <=
   325     select 2
   326     var SP@0
   327       array 2
   328         type-con Vertex 0
   329         int
   330     var z
   331       type-con Vertex 0
   332     +
   333     select 2
   334     var SP@0
   335       array 2
   336         type-con Vertex 0
   337         int
   338     var y
   339       type-con Vertex 0
   340     select 3
   341     fun G 0
   342     var y
   343       type-con Vertex 0
   344     var z
   345       type-con Vertex 0
   346     implies
   347     forall 2 0 3
   348       var z
   349         type-con Vertex 0
   350       var y
   351         type-con Vertex 0
   352       attribute qid 1
   353         string-attr BoogieDi.38:23
   354       attribute uniqueId 1
   355         string-attr 11
   356       attribute bvZ3Native 1
   357         string-attr False
   358     implies
   359     and 2
   360     select 2
   361     var Visited@0
   362       array 2
   363         type-con Vertex 0
   364         bool
   365     var y
   366       type-con Vertex 0
   367     <
   368     select 3
   369     fun G 0
   370     var y
   371       type-con Vertex 0
   372     var z
   373       type-con Vertex 0
   374     fun Infinity 0
   375     <=
   376     select 2
   377     var SP@0
   378       array 2
   379         type-con Vertex 0
   380         int
   381     var z
   382       type-con Vertex 0
   383     +
   384     select 2
   385     var SP@0
   386       array 2
   387         type-con Vertex 0
   388         int
   389     var y
   390       type-con Vertex 0
   391     select 3
   392     fun G 0
   393     var y
   394       type-con Vertex 0
   395     var z
   396       type-con Vertex 0
   397     and 2
   398     label neg 40 5
   399     forall 1 0 3
   400       var z
   401         type-con Vertex 0
   402       attribute qid 1
   403         string-attr BoogieDi.40:23
   404       attribute uniqueId 1
   405         string-attr 13
   406       attribute bvZ3Native 1
   407         string-attr False
   408     implies
   409     and 2
   410     not
   411     =
   412     var z
   413       type-con Vertex 0
   414     fun Source 0
   415     <
   416     select 2
   417     var SP@0
   418       array 2
   419         type-con Vertex 0
   420         int
   421     var z
   422       type-con Vertex 0
   423     fun Infinity 0
   424     exists 1 0 3
   425       var y
   426         type-con Vertex 0
   427       attribute qid 1
   428         string-attr BoogieDi.41:15
   429       attribute uniqueId 1
   430         string-attr 12
   431       attribute bvZ3Native 1
   432         string-attr False
   433     and 3
   434     <
   435     select 2
   436     var SP@0
   437       array 2
   438         type-con Vertex 0
   439         int
   440     var y
   441       type-con Vertex 0
   442     select 2
   443     var SP@0
   444       array 2
   445         type-con Vertex 0
   446         int
   447     var z
   448       type-con Vertex 0
   449     select 2
   450     var Visited@0
   451       array 2
   452         type-con Vertex 0
   453         bool
   454     var y
   455       type-con Vertex 0
   456     =
   457     select 2
   458     var SP@0
   459       array 2
   460         type-con Vertex 0
   461         int
   462     var z
   463       type-con Vertex 0
   464     +
   465     select 2
   466     var SP@0
   467       array 2
   468         type-con Vertex 0
   469         int
   470     var y
   471       type-con Vertex 0
   472     select 3
   473     fun G 0
   474     var y
   475       type-con Vertex 0
   476     var z
   477       type-con Vertex 0
   478     implies
   479     forall 1 0 3
   480       var z
   481         type-con Vertex 0
   482       attribute qid 1
   483         string-attr BoogieDi.40:23
   484       attribute uniqueId 1
   485         string-attr 13
   486       attribute bvZ3Native 1
   487         string-attr False
   488     implies
   489     and 2
   490     not
   491     =
   492     var z
   493       type-con Vertex 0
   494     fun Source 0
   495     <
   496     select 2
   497     var SP@0
   498       array 2
   499         type-con Vertex 0
   500         int
   501     var z
   502       type-con Vertex 0
   503     fun Infinity 0
   504     exists 1 0 3
   505       var y
   506         type-con Vertex 0
   507       attribute qid 1
   508         string-attr BoogieDi.41:15
   509       attribute uniqueId 1
   510         string-attr 12
   511       attribute bvZ3Native 1
   512         string-attr False
   513     and 3
   514     <
   515     select 2
   516     var SP@0
   517       array 2
   518         type-con Vertex 0
   519         int
   520     var y
   521       type-con Vertex 0
   522     select 2
   523     var SP@0
   524       array 2
   525         type-con Vertex 0
   526         int
   527     var z
   528       type-con Vertex 0
   529     select 2
   530     var Visited@0
   531       array 2
   532         type-con Vertex 0
   533         bool
   534     var y
   535       type-con Vertex 0
   536     =
   537     select 2
   538     var SP@0
   539       array 2
   540         type-con Vertex 0
   541         int
   542     var z
   543       type-con Vertex 0
   544     +
   545     select 2
   546     var SP@0
   547       array 2
   548         type-con Vertex 0
   549         int
   550     var y
   551       type-con Vertex 0
   552     select 3
   553     fun G 0
   554     var y
   555       type-con Vertex 0
   556     var z
   557       type-con Vertex 0
   558     implies
   559     label pos 33 3
   560     true
   561     implies
   562     true
   563     implies
   564     =
   565     select 2
   566     var SP@1
   567       array 2
   568         type-con Vertex 0
   569         int
   570     fun Source 0
   571     int-num 0
   572     implies
   573     forall 1 0 3
   574       var x
   575         type-con Vertex 0
   576       attribute qid 1
   577         string-attr BoogieDi.35:23
   578       attribute uniqueId 1
   579         string-attr 9
   580       attribute bvZ3Native 1
   581         string-attr False
   582     >=
   583     select 2
   584     var SP@1
   585       array 2
   586         type-con Vertex 0
   587         int
   588     var x
   589       type-con Vertex 0
   590     int-num 0
   591     implies
   592     forall 2 0 3
   593       var y
   594         type-con Vertex 0
   595       var z
   596         type-con Vertex 0
   597       attribute qid 1
   598         string-attr BoogieDi.36:23
   599       attribute uniqueId 1
   600         string-attr 10
   601       attribute bvZ3Native 1
   602         string-attr False
   603     implies
   604     and 2
   605     not
   606     select 2
   607     var Visited@1
   608       array 2
   609         type-con Vertex 0
   610         bool
   611     var z
   612       type-con Vertex 0
   613     select 2
   614     var Visited@1
   615       array 2
   616         type-con Vertex 0
   617         bool
   618     var y
   619       type-con Vertex 0
   620     <=
   621     select 2
   622     var SP@1
   623       array 2
   624         type-con Vertex 0
   625         int
   626     var y
   627       type-con Vertex 0
   628     select 2
   629     var SP@1
   630       array 2
   631         type-con Vertex 0
   632         int
   633     var z
   634       type-con Vertex 0
   635     implies
   636     forall 2 0 3
   637       var z
   638         type-con Vertex 0
   639       var y
   640         type-con Vertex 0
   641       attribute qid 1
   642         string-attr BoogieDi.38:23
   643       attribute uniqueId 1
   644         string-attr 11
   645       attribute bvZ3Native 1
   646         string-attr False
   647     implies
   648     and 2
   649     select 2
   650     var Visited@1
   651       array 2
   652         type-con Vertex 0
   653         bool
   654     var y
   655       type-con Vertex 0
   656     <
   657     select 3
   658     fun G 0
   659     var y
   660       type-con Vertex 0
   661     var z
   662       type-con Vertex 0
   663     fun Infinity 0
   664     <=
   665     select 2
   666     var SP@1
   667       array 2
   668         type-con Vertex 0
   669         int
   670     var z
   671       type-con Vertex 0
   672     +
   673     select 2
   674     var SP@1
   675       array 2
   676         type-con Vertex 0
   677         int
   678     var y
   679       type-con Vertex 0
   680     select 3
   681     fun G 0
   682     var y
   683       type-con Vertex 0
   684     var z
   685       type-con Vertex 0
   686     implies
   687     forall 1 0 3
   688       var z
   689         type-con Vertex 0
   690       attribute qid 1
   691         string-attr BoogieDi.40:23
   692       attribute uniqueId 1
   693         string-attr 13
   694       attribute bvZ3Native 1
   695         string-attr False
   696     implies
   697     and 2
   698     not
   699     =
   700     var z
   701       type-con Vertex 0
   702     fun Source 0
   703     <
   704     select 2
   705     var SP@1
   706       array 2
   707         type-con Vertex 0
   708         int
   709     var z
   710       type-con Vertex 0
   711     fun Infinity 0
   712     exists 1 0 3
   713       var y
   714         type-con Vertex 0
   715       attribute qid 1
   716         string-attr BoogieDi.41:15
   717       attribute uniqueId 1
   718         string-attr 12
   719       attribute bvZ3Native 1
   720         string-attr False
   721     and 3
   722     <
   723     select 2
   724     var SP@1
   725       array 2
   726         type-con Vertex 0
   727         int
   728     var y
   729       type-con Vertex 0
   730     select 2
   731     var SP@1
   732       array 2
   733         type-con Vertex 0
   734         int
   735     var z
   736       type-con Vertex 0
   737     select 2
   738     var Visited@1
   739       array 2
   740         type-con Vertex 0
   741         bool
   742     var y
   743       type-con Vertex 0
   744     =
   745     select 2
   746     var SP@1
   747       array 2
   748         type-con Vertex 0
   749         int
   750     var z
   751       type-con Vertex 0
   752     +
   753     select 2
   754     var SP@1
   755       array 2
   756         type-con Vertex 0
   757         int
   758     var y
   759       type-con Vertex 0
   760     select 3
   761     fun G 0
   762     var y
   763       type-con Vertex 0
   764     var z
   765       type-con Vertex 0
   766     implies
   767     true
   768     and 2
   769     implies
   770     label pos 33 3
   771     true
   772     implies
   773     true
   774     implies
   775     not
   776     exists 1 0 3
   777       var x
   778         type-con Vertex 0
   779       attribute qid 1
   780         string-attr BoogieDi.33:18
   781       attribute uniqueId 1
   782         string-attr 8
   783       attribute bvZ3Native 1
   784         string-attr False
   785     and 2
   786     not
   787     select 2
   788     var Visited@1
   789       array 2
   790         type-con Vertex 0
   791         bool
   792     var x
   793       type-con Vertex 0
   794     <
   795     select 2
   796     var SP@1
   797       array 2
   798         type-con Vertex 0
   799         int
   800     var x
   801       type-con Vertex 0
   802     fun Infinity 0
   803     implies
   804     true
   805     implies
   806     label pos 0 0
   807     true
   808     implies
   809     =
   810     var Visited@3
   811       array 2
   812         type-con Vertex 0
   813         bool
   814     var Visited@1
   815       array 2
   816         type-con Vertex 0
   817         bool
   818     implies
   819     =
   820     var v@2
   821       type-con Vertex 0
   822     var v@0
   823       type-con Vertex 0
   824     implies
   825     =
   826     var SP@3
   827       array 2
   828         type-con Vertex 0
   829         int
   830     var SP@1
   831       array 2
   832         type-con Vertex 0
   833         int
   834     implies
   835     =
   836     var oldSP@1
   837       array 2
   838         type-con Vertex 0
   839         int
   840     var oldSP@0
   841       array 2
   842         type-con Vertex 0
   843         int
   844     implies
   845     label pos 0 0
   846     true
   847     and 2
   848     label neg 17 3
   849     forall 1 0 3
   850       var z
   851         type-con Vertex 0
   852       attribute qid 1
   853         string-attr BoogieDi.17:19
   854       attribute uniqueId 1
   855         string-attr 4
   856       attribute bvZ3Native 1
   857         string-attr False
   858     implies
   859     and 2
   860     not
   861     =
   862     var z
   863       type-con Vertex 0
   864     fun Source 0
   865     <
   866     select 2
   867     var SP@3
   868       array 2
   869         type-con Vertex 0
   870         int
   871     var z
   872       type-con Vertex 0
   873     fun Infinity 0
   874     exists 1 0 3
   875       var y
   876         type-con Vertex 0
   877       attribute qid 1
   878         string-attr BoogieDi.18:13
   879       attribute uniqueId 1
   880         string-attr 3
   881       attribute bvZ3Native 1
   882         string-attr False
   883     and 2
   884     <
   885     select 2
   886     var SP@3
   887       array 2
   888         type-con Vertex 0
   889         int
   890     var y
   891       type-con Vertex 0
   892     select 2
   893     var SP@3
   894       array 2
   895         type-con Vertex 0
   896         int
   897     var z
   898       type-con Vertex 0
   899     =
   900     select 2
   901     var SP@3
   902       array 2
   903         type-con Vertex 0
   904         int
   905     var z
   906       type-con Vertex 0
   907     +
   908     select 2
   909     var SP@3
   910       array 2
   911         type-con Vertex 0
   912         int
   913     var y
   914       type-con Vertex 0
   915     select 3
   916     fun G 0
   917     var y
   918       type-con Vertex 0
   919     var z
   920       type-con Vertex 0
   921     implies
   922     forall 1 0 3
   923       var z
   924         type-con Vertex 0
   925       attribute qid 1
   926         string-attr BoogieDi.17:19
   927       attribute uniqueId 1
   928         string-attr 4
   929       attribute bvZ3Native 1
   930         string-attr False
   931     implies
   932     and 2
   933     not
   934     =
   935     var z
   936       type-con Vertex 0
   937     fun Source 0
   938     <
   939     select 2
   940     var SP@3
   941       array 2
   942         type-con Vertex 0
   943         int
   944     var z
   945       type-con Vertex 0
   946     fun Infinity 0
   947     exists 1 0 3
   948       var y
   949         type-con Vertex 0
   950       attribute qid 1
   951         string-attr BoogieDi.18:13
   952       attribute uniqueId 1
   953         string-attr 3
   954       attribute bvZ3Native 1
   955         string-attr False
   956     and 2
   957     <
   958     select 2
   959     var SP@3
   960       array 2
   961         type-con Vertex 0
   962         int
   963     var y
   964       type-con Vertex 0
   965     select 2
   966     var SP@3
   967       array 2
   968         type-con Vertex 0
   969         int
   970     var z
   971       type-con Vertex 0
   972     =
   973     select 2
   974     var SP@3
   975       array 2
   976         type-con Vertex 0
   977         int
   978     var z
   979       type-con Vertex 0
   980     +
   981     select 2
   982     var SP@3
   983       array 2
   984         type-con Vertex 0
   985         int
   986     var y
   987       type-con Vertex 0
   988     select 3
   989     fun G 0
   990     var y
   991       type-con Vertex 0
   992     var z
   993       type-con Vertex 0
   994     and 2
   995     label neg 15 3
   996     forall 2 0 3
   997       var z
   998         type-con Vertex 0
   999       var y
  1000         type-con Vertex 0
  1001       attribute qid 1
  1002         string-attr BoogieDi.15:19
  1003       attribute uniqueId 1
  1004         string-attr 2
  1005       attribute bvZ3Native 1
  1006         string-attr False
  1007     implies
  1008     and 2
  1009     <
  1010     select 2
  1011     var SP@3
  1012       array 2
  1013         type-con Vertex 0
  1014         int
  1015     var y
  1016       type-con Vertex 0
  1017     fun Infinity 0
  1018     <
  1019     select 3
  1020     fun G 0
  1021     var y
  1022       type-con Vertex 0
  1023     var z
  1024       type-con Vertex 0
  1025     fun Infinity 0
  1026     <=
  1027     select 2
  1028     var SP@3
  1029       array 2
  1030         type-con Vertex 0
  1031         int
  1032     var z
  1033       type-con Vertex 0
  1034     +
  1035     select 2
  1036     var SP@3
  1037       array 2
  1038         type-con Vertex 0
  1039         int
  1040     var y
  1041       type-con Vertex 0
  1042     select 3
  1043     fun G 0
  1044     var y
  1045       type-con Vertex 0
  1046     var z
  1047       type-con Vertex 0
  1048     implies
  1049     forall 2 0 3
  1050       var z
  1051         type-con Vertex 0
  1052       var y
  1053         type-con Vertex 0
  1054       attribute qid 1
  1055         string-attr BoogieDi.15:19
  1056       attribute uniqueId 1
  1057         string-attr 2
  1058       attribute bvZ3Native 1
  1059         string-attr False
  1060     implies
  1061     and 2
  1062     <
  1063     select 2
  1064     var SP@3
  1065       array 2
  1066         type-con Vertex 0
  1067         int
  1068     var y
  1069       type-con Vertex 0
  1070     fun Infinity 0
  1071     <
  1072     select 3
  1073     fun G 0
  1074     var y
  1075       type-con Vertex 0
  1076     var z
  1077       type-con Vertex 0
  1078     fun Infinity 0
  1079     <=
  1080     select 2
  1081     var SP@3
  1082       array 2
  1083         type-con Vertex 0
  1084         int
  1085     var z
  1086       type-con Vertex 0
  1087     +
  1088     select 2
  1089     var SP@3
  1090       array 2
  1091         type-con Vertex 0
  1092         int
  1093     var y
  1094       type-con Vertex 0
  1095     select 3
  1096     fun G 0
  1097     var y
  1098       type-con Vertex 0
  1099     var z
  1100       type-con Vertex 0
  1101     and 2
  1102     label neg 14 3
  1103     =
  1104     select 2
  1105     var SP@3
  1106       array 2
  1107         type-con Vertex 0
  1108         int
  1109     fun Source 0
  1110     int-num 0
  1111     implies
  1112     =
  1113     select 2
  1114     var SP@3
  1115       array 2
  1116         type-con Vertex 0
  1117         int
  1118     fun Source 0
  1119     int-num 0
  1120     true
  1121     implies
  1122     label pos 44 5
  1123     true
  1124     implies
  1125     true
  1126     implies
  1127     exists 1 0 3
  1128       var x
  1129         type-con Vertex 0
  1130       attribute qid 1
  1131         string-attr BoogieDi.33:18
  1132       attribute uniqueId 1
  1133         string-attr 8
  1134       attribute bvZ3Native 1
  1135         string-attr False
  1136     and 2
  1137     not
  1138     select 2
  1139     var Visited@1
  1140       array 2
  1141         type-con Vertex 0
  1142         bool
  1143     var x
  1144       type-con Vertex 0
  1145     <
  1146     select 2
  1147     var SP@1
  1148       array 2
  1149         type-con Vertex 0
  1150         int
  1151     var x
  1152       type-con Vertex 0
  1153     fun Infinity 0
  1154     implies
  1155     not
  1156     select 2
  1157     var Visited@1
  1158       array 2
  1159         type-con Vertex 0
  1160         bool
  1161     var v@1
  1162       type-con Vertex 0
  1163     implies
  1164     <
  1165     select 2
  1166     var SP@1
  1167       array 2
  1168         type-con Vertex 0
  1169         int
  1170     var v@1
  1171       type-con Vertex 0
  1172     fun Infinity 0
  1173     implies
  1174     forall 1 0 3
  1175       var x
  1176         type-con Vertex 0
  1177       attribute qid 1
  1178         string-attr BoogieDi.47:20
  1179       attribute uniqueId 1
  1180         string-attr 14
  1181       attribute bvZ3Native 1
  1182         string-attr False
  1183     implies
  1184     not
  1185     select 2
  1186     var Visited@1
  1187       array 2
  1188         type-con Vertex 0
  1189         bool
  1190     var x
  1191       type-con Vertex 0
  1192     <=
  1193     select 2
  1194     var SP@1
  1195       array 2
  1196         type-con Vertex 0
  1197         int
  1198     var v@1
  1199       type-con Vertex 0
  1200     select 2
  1201     var SP@1
  1202       array 2
  1203         type-con Vertex 0
  1204         int
  1205     var x
  1206       type-con Vertex 0
  1207     implies
  1208     =
  1209     var Visited@2
  1210       array 2
  1211         type-con Vertex 0
  1212         bool
  1213     store 3
  1214     var Visited@1
  1215       array 2
  1216         type-con Vertex 0
  1217         bool
  1218     var v@1
  1219       type-con Vertex 0
  1220     true
  1221     implies
  1222     forall 1 0 3
  1223       var u
  1224         type-con Vertex 0
  1225       attribute qid 1
  1226         string-attr BoogieDi.53:20
  1227       attribute uniqueId 1
  1228         string-attr 15
  1229       attribute bvZ3Native 1
  1230         string-attr False
  1231     implies
  1232     and 2
  1233     <
  1234     select 3
  1235     fun G 0
  1236     var v@1
  1237       type-con Vertex 0
  1238     var u
  1239       type-con Vertex 0
  1240     fun Infinity 0
  1241     <
  1242     +
  1243     select 2
  1244     var SP@1
  1245       array 2
  1246         type-con Vertex 0
  1247         int
  1248     var v@1
  1249       type-con Vertex 0
  1250     select 3
  1251     fun G 0
  1252     var v@1
  1253       type-con Vertex 0
  1254     var u
  1255       type-con Vertex 0
  1256     select 2
  1257     var SP@1
  1258       array 2
  1259         type-con Vertex 0
  1260         int
  1261     var u
  1262       type-con Vertex 0
  1263     =
  1264     select 2
  1265     var SP@2
  1266       array 2
  1267         type-con Vertex 0
  1268         int
  1269     var u
  1270       type-con Vertex 0
  1271     +
  1272     select 2
  1273     var SP@1
  1274       array 2
  1275         type-con Vertex 0
  1276         int
  1277     var v@1
  1278       type-con Vertex 0
  1279     select 3
  1280     fun G 0
  1281     var v@1
  1282       type-con Vertex 0
  1283     var u
  1284       type-con Vertex 0
  1285     implies
  1286     forall 1 0 3
  1287       var u
  1288         type-con Vertex 0
  1289       attribute qid 1
  1290         string-attr BoogieDi.56:20
  1291       attribute uniqueId 1
  1292         string-attr 16
  1293       attribute bvZ3Native 1
  1294         string-attr False
  1295     implies
  1296     not
  1297     and 2
  1298     <
  1299     select 3
  1300     fun G 0
  1301     var v@1
  1302       type-con Vertex 0
  1303     var u
  1304       type-con Vertex 0
  1305     fun Infinity 0
  1306     <
  1307     +
  1308     select 2
  1309     var SP@1
  1310       array 2
  1311         type-con Vertex 0
  1312         int
  1313     var v@1
  1314       type-con Vertex 0
  1315     select 3
  1316     fun G 0
  1317     var v@1
  1318       type-con Vertex 0
  1319     var u
  1320       type-con Vertex 0
  1321     select 2
  1322     var SP@1
  1323       array 2
  1324         type-con Vertex 0
  1325         int
  1326     var u
  1327       type-con Vertex 0
  1328     =
  1329     select 2
  1330     var SP@2
  1331       array 2
  1332         type-con Vertex 0
  1333         int
  1334     var u
  1335       type-con Vertex 0
  1336     select 2
  1337     var SP@1
  1338       array 2
  1339         type-con Vertex 0
  1340         int
  1341     var u
  1342       type-con Vertex 0
  1343     and 2
  1344     label neg 59 5
  1345     forall 1 0 3
  1346       var z
  1347         type-con Vertex 0
  1348       attribute qid 1
  1349         string-attr BoogieDi.59:20
  1350       attribute uniqueId 1
  1351         string-attr 17
  1352       attribute bvZ3Native 1
  1353         string-attr False
  1354     <=
  1355     select 2
  1356     var SP@2
  1357       array 2
  1358         type-con Vertex 0
  1359         int
  1360     var z
  1361       type-con Vertex 0
  1362     select 2
  1363     var SP@1
  1364       array 2
  1365         type-con Vertex 0
  1366         int
  1367     var z
  1368       type-con Vertex 0
  1369     implies
  1370     forall 1 0 3
  1371       var z
  1372         type-con Vertex 0
  1373       attribute qid 1
  1374         string-attr BoogieDi.59:20
  1375       attribute uniqueId 1
  1376         string-attr 17
  1377       attribute bvZ3Native 1
  1378         string-attr False
  1379     <=
  1380     select 2
  1381     var SP@2
  1382       array 2
  1383         type-con Vertex 0
  1384         int
  1385     var z
  1386       type-con Vertex 0
  1387     select 2
  1388     var SP@1
  1389       array 2
  1390         type-con Vertex 0
  1391         int
  1392     var z
  1393       type-con Vertex 0
  1394     and 2
  1395     label neg 60 5
  1396     forall 1 0 3
  1397       var y
  1398         type-con Vertex 0
  1399       attribute qid 1
  1400         string-attr BoogieDi.60:20
  1401       attribute uniqueId 1
  1402         string-attr 18
  1403       attribute bvZ3Native 1
  1404         string-attr False
  1405     implies
  1406     select 2
  1407     var Visited@2
  1408       array 2
  1409         type-con Vertex 0
  1410         bool
  1411     var y
  1412       type-con Vertex 0
  1413     =
  1414     select 2
  1415     var SP@2
  1416       array 2
  1417         type-con Vertex 0
  1418         int
  1419     var y
  1420       type-con Vertex 0
  1421     select 2
  1422     var SP@1
  1423       array 2
  1424         type-con Vertex 0
  1425         int
  1426     var y
  1427       type-con Vertex 0
  1428     implies
  1429     forall 1 0 3
  1430       var y
  1431         type-con Vertex 0
  1432       attribute qid 1
  1433         string-attr BoogieDi.60:20
  1434       attribute uniqueId 1
  1435         string-attr 18
  1436       attribute bvZ3Native 1
  1437         string-attr False
  1438     implies
  1439     select 2
  1440     var Visited@2
  1441       array 2
  1442         type-con Vertex 0
  1443         bool
  1444     var y
  1445       type-con Vertex 0
  1446     =
  1447     select 2
  1448     var SP@2
  1449       array 2
  1450         type-con Vertex 0
  1451         int
  1452     var y
  1453       type-con Vertex 0
  1454     select 2
  1455     var SP@1
  1456       array 2
  1457         type-con Vertex 0
  1458         int
  1459     var y
  1460       type-con Vertex 0
  1461     implies
  1462     true
  1463     implies
  1464     label pos 0 0
  1465     true
  1466     and 2
  1467     label neg 34 5
  1468     =
  1469     select 2
  1470     var SP@2
  1471       array 2
  1472         type-con Vertex 0
  1473         int
  1474     fun Source 0
  1475     int-num 0
  1476     implies
  1477     =
  1478     select 2
  1479     var SP@2
  1480       array 2
  1481         type-con Vertex 0
  1482         int
  1483     fun Source 0
  1484     int-num 0
  1485     and 2
  1486     label neg 35 5
  1487     forall 1 0 3
  1488       var x
  1489         type-con Vertex 0
  1490       attribute qid 1
  1491         string-attr BoogieDi.35:23
  1492       attribute uniqueId 1
  1493         string-attr 9
  1494       attribute bvZ3Native 1
  1495         string-attr False
  1496     >=
  1497     select 2
  1498     var SP@2
  1499       array 2
  1500         type-con Vertex 0
  1501         int
  1502     var x
  1503       type-con Vertex 0
  1504     int-num 0
  1505     implies
  1506     forall 1 0 3
  1507       var x
  1508         type-con Vertex 0
  1509       attribute qid 1
  1510         string-attr BoogieDi.35:23
  1511       attribute uniqueId 1
  1512         string-attr 9
  1513       attribute bvZ3Native 1
  1514         string-attr False
  1515     >=
  1516     select 2
  1517     var SP@2
  1518       array 2
  1519         type-con Vertex 0
  1520         int
  1521     var x
  1522       type-con Vertex 0
  1523     int-num 0
  1524     and 2
  1525     label neg 36 5
  1526     forall 2 0 3
  1527       var y
  1528         type-con Vertex 0
  1529       var z
  1530         type-con Vertex 0
  1531       attribute qid 1
  1532         string-attr BoogieDi.36:23
  1533       attribute uniqueId 1
  1534         string-attr 10
  1535       attribute bvZ3Native 1
  1536         string-attr False
  1537     implies
  1538     and 2
  1539     not
  1540     select 2
  1541     var Visited@2
  1542       array 2
  1543         type-con Vertex 0
  1544         bool
  1545     var z
  1546       type-con Vertex 0
  1547     select 2
  1548     var Visited@2
  1549       array 2
  1550         type-con Vertex 0
  1551         bool
  1552     var y
  1553       type-con Vertex 0
  1554     <=
  1555     select 2
  1556     var SP@2
  1557       array 2
  1558         type-con Vertex 0
  1559         int
  1560     var y
  1561       type-con Vertex 0
  1562     select 2
  1563     var SP@2
  1564       array 2
  1565         type-con Vertex 0
  1566         int
  1567     var z
  1568       type-con Vertex 0
  1569     implies
  1570     forall 2 0 3
  1571       var y
  1572         type-con Vertex 0
  1573       var z
  1574         type-con Vertex 0
  1575       attribute qid 1
  1576         string-attr BoogieDi.36:23
  1577       attribute uniqueId 1
  1578         string-attr 10
  1579       attribute bvZ3Native 1
  1580         string-attr False
  1581     implies
  1582     and 2
  1583     not
  1584     select 2
  1585     var Visited@2
  1586       array 2
  1587         type-con Vertex 0
  1588         bool
  1589     var z
  1590       type-con Vertex 0
  1591     select 2
  1592     var Visited@2
  1593       array 2
  1594         type-con Vertex 0
  1595         bool
  1596     var y
  1597       type-con Vertex 0
  1598     <=
  1599     select 2
  1600     var SP@2
  1601       array 2
  1602         type-con Vertex 0
  1603         int
  1604     var y
  1605       type-con Vertex 0
  1606     select 2
  1607     var SP@2
  1608       array 2
  1609         type-con Vertex 0
  1610         int
  1611     var z
  1612       type-con Vertex 0
  1613     and 2
  1614     label neg 38 5
  1615     forall 2 0 3
  1616       var z
  1617         type-con Vertex 0
  1618       var y
  1619         type-con Vertex 0
  1620       attribute qid 1
  1621         string-attr BoogieDi.38:23
  1622       attribute uniqueId 1
  1623         string-attr 11
  1624       attribute bvZ3Native 1
  1625         string-attr False
  1626     implies
  1627     and 2
  1628     select 2
  1629     var Visited@2
  1630       array 2
  1631         type-con Vertex 0
  1632         bool
  1633     var y
  1634       type-con Vertex 0
  1635     <
  1636     select 3
  1637     fun G 0
  1638     var y
  1639       type-con Vertex 0
  1640     var z
  1641       type-con Vertex 0
  1642     fun Infinity 0
  1643     <=
  1644     select 2
  1645     var SP@2
  1646       array 2
  1647         type-con Vertex 0
  1648         int
  1649     var z
  1650       type-con Vertex 0
  1651     +
  1652     select 2
  1653     var SP@2
  1654       array 2
  1655         type-con Vertex 0
  1656         int
  1657     var y
  1658       type-con Vertex 0
  1659     select 3
  1660     fun G 0
  1661     var y
  1662       type-con Vertex 0
  1663     var z
  1664       type-con Vertex 0
  1665     implies
  1666     forall 2 0 3
  1667       var z
  1668         type-con Vertex 0
  1669       var y
  1670         type-con Vertex 0
  1671       attribute qid 1
  1672         string-attr BoogieDi.38:23
  1673       attribute uniqueId 1
  1674         string-attr 11
  1675       attribute bvZ3Native 1
  1676         string-attr False
  1677     implies
  1678     and 2
  1679     select 2
  1680     var Visited@2
  1681       array 2
  1682         type-con Vertex 0
  1683         bool
  1684     var y
  1685       type-con Vertex 0
  1686     <
  1687     select 3
  1688     fun G 0
  1689     var y
  1690       type-con Vertex 0
  1691     var z
  1692       type-con Vertex 0
  1693     fun Infinity 0
  1694     <=
  1695     select 2
  1696     var SP@2
  1697       array 2
  1698         type-con Vertex 0
  1699         int
  1700     var z
  1701       type-con Vertex 0
  1702     +
  1703     select 2
  1704     var SP@2
  1705       array 2
  1706         type-con Vertex 0
  1707         int
  1708     var y
  1709       type-con Vertex 0
  1710     select 3
  1711     fun G 0
  1712     var y
  1713       type-con Vertex 0
  1714     var z
  1715       type-con Vertex 0
  1716     and 2
  1717     label neg 40 5
  1718     forall 1 0 3
  1719       var z
  1720         type-con Vertex 0
  1721       attribute qid 1
  1722         string-attr BoogieDi.40:23
  1723       attribute uniqueId 1
  1724         string-attr 13
  1725       attribute bvZ3Native 1
  1726         string-attr False
  1727     implies
  1728     and 2
  1729     not
  1730     =
  1731     var z
  1732       type-con Vertex 0
  1733     fun Source 0
  1734     <
  1735     select 2
  1736     var SP@2
  1737       array 2
  1738         type-con Vertex 0
  1739         int
  1740     var z
  1741       type-con Vertex 0
  1742     fun Infinity 0
  1743     exists 1 0 3
  1744       var y
  1745         type-con Vertex 0
  1746       attribute qid 1
  1747         string-attr BoogieDi.41:15
  1748       attribute uniqueId 1
  1749         string-attr 12
  1750       attribute bvZ3Native 1
  1751         string-attr False
  1752     and 3
  1753     <
  1754     select 2
  1755     var SP@2
  1756       array 2
  1757         type-con Vertex 0
  1758         int
  1759     var y
  1760       type-con Vertex 0
  1761     select 2
  1762     var SP@2
  1763       array 2
  1764         type-con Vertex 0
  1765         int
  1766     var z
  1767       type-con Vertex 0
  1768     select 2
  1769     var Visited@2
  1770       array 2
  1771         type-con Vertex 0
  1772         bool
  1773     var y
  1774       type-con Vertex 0
  1775     =
  1776     select 2
  1777     var SP@2
  1778       array 2
  1779         type-con Vertex 0
  1780         int
  1781     var z
  1782       type-con Vertex 0
  1783     +
  1784     select 2
  1785     var SP@2
  1786       array 2
  1787         type-con Vertex 0
  1788         int
  1789     var y
  1790       type-con Vertex 0
  1791     select 3
  1792     fun G 0
  1793     var y
  1794       type-con Vertex 0
  1795     var z
  1796       type-con Vertex 0
  1797     implies
  1798     forall 1 0 3
  1799       var z
  1800         type-con Vertex 0
  1801       attribute qid 1
  1802         string-attr BoogieDi.40:23
  1803       attribute uniqueId 1
  1804         string-attr 13
  1805       attribute bvZ3Native 1
  1806         string-attr False
  1807     implies
  1808     and 2
  1809     not
  1810     =
  1811     var z
  1812       type-con Vertex 0
  1813     fun Source 0
  1814     <
  1815     select 2
  1816     var SP@2
  1817       array 2
  1818         type-con Vertex 0
  1819         int
  1820     var z
  1821       type-con Vertex 0
  1822     fun Infinity 0
  1823     exists 1 0 3
  1824       var y
  1825         type-con Vertex 0
  1826       attribute qid 1
  1827         string-attr BoogieDi.41:15
  1828       attribute uniqueId 1
  1829         string-attr 12
  1830       attribute bvZ3Native 1
  1831         string-attr False
  1832     and 3
  1833     <
  1834     select 2
  1835     var SP@2
  1836       array 2
  1837         type-con Vertex 0
  1838         int
  1839     var y
  1840       type-con Vertex 0
  1841     select 2
  1842     var SP@2
  1843       array 2
  1844         type-con Vertex 0
  1845         int
  1846     var z
  1847       type-con Vertex 0
  1848     select 2
  1849     var Visited@2
  1850       array 2
  1851         type-con Vertex 0
  1852         bool
  1853     var y
  1854       type-con Vertex 0
  1855     =
  1856     select 2
  1857     var SP@2
  1858       array 2
  1859         type-con Vertex 0
  1860         int
  1861     var z
  1862       type-con Vertex 0
  1863     +
  1864     select 2
  1865     var SP@2
  1866       array 2
  1867         type-con Vertex 0
  1868         int
  1869     var y
  1870       type-con Vertex 0
  1871     select 3
  1872     fun G 0
  1873     var y
  1874       type-con Vertex 0
  1875     var z
  1876       type-con Vertex 0
  1877     implies
  1878     false
  1879     true