boehmes@52722: vc max 1
boehmes@52722:     implies
boehmes@52722:     label pos 10 7
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     <
boehmes@52722:     int-num 0
boehmes@52722:     var length
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var max@0
boehmes@52722:       int
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     int-num 0
boehmes@52722:     implies
boehmes@52722:     and 4
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     int-num 0
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     int-num 0
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     int-num 1
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     int-num 1
boehmes@52722:     and 2
boehmes@52722:     label neg 14 5
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.14:23
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 2
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     int-num 1
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.14:23
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 2
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     int-num 1
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@0
boehmes@52722:       int
boehmes@52722:     and 2
boehmes@52722:     label neg 15 5
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     int-num 0
boehmes@52722:     var max@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     int-num 0
boehmes@52722:     var max@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 13 3
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.14:23
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 2
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     var max@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     and 2
boehmes@52722:     implies
boehmes@52722:     label pos 13 3
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     >=
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     var length
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 0 0
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var k@2
boehmes@52722:       int
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var max@4
boehmes@52722:       int
boehmes@52722:     var max@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var p@2
boehmes@52722:       int
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 0 0
boehmes@52722:     true
boehmes@52722:     and 2
boehmes@52722:     label neg 5 3
boehmes@52722:     exists 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.5:19
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 1
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var length
boehmes@52722:       int
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@4
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     exists 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.5:19
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 1
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var length
boehmes@52722:       int
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@4
boehmes@52722:       int
boehmes@52722:     and 2
boehmes@52722:     label neg 4 3
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.4:19
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 0
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var length
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@4
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.4:19
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 0
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var length
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@4
boehmes@52722:       int
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     label pos 17 5
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     <
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     var length
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     and 2
boehmes@52722:     implies
boehmes@52722:     label pos 17 31
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     >
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     var max@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var max@2
boehmes@52722:       int
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 0 0
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     var max@2
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 18 7
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     +
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     int-num 1
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 2
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 0 0
boehmes@52722:     true
boehmes@52722:     and 2
boehmes@52722:     label neg 14 5
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.14:23
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 2
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.14:23
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 2
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     and 2
boehmes@52722:     label neg 15 5
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     false
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     label pos 17 5
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     var max@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 0 0
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     var k@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     var max@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 18 7
boehmes@52722:     true
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 1
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     +
boehmes@52722:     var p@0
boehmes@52722:       int
boehmes@52722:     int-num 1
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     int-num 2
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     label pos 0 0
boehmes@52722:     true
boehmes@52722:     and 2
boehmes@52722:     label neg 14 5
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.14:23
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 2
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     forall 1 0 3
boehmes@52722:       var i
boehmes@52722:         int
boehmes@52722:       attribute qid 1
boehmes@52722:         string-attr BoogieMa.14:23
boehmes@52722:       attribute uniqueId 1
boehmes@52722:         string-attr 2
boehmes@52722:       attribute bvZ3Native 1
boehmes@52722:         string-attr False
boehmes@52722:     implies
boehmes@52722:     and 2
boehmes@52722:     <=
boehmes@52722:     int-num 0
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     <
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var p@1
boehmes@52722:       int
boehmes@52722:     <=
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var i
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     and 2
boehmes@52722:     label neg 15 5
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     =
boehmes@52722:     select 2
boehmes@52722:     var array
boehmes@52722:       array 2
boehmes@52722:         int
boehmes@52722:         int
boehmes@52722:     var k@1
boehmes@52722:       int
boehmes@52722:     var max@3
boehmes@52722:       int
boehmes@52722:     implies
boehmes@52722:     false
boehmes@52722:     true