--- a/src/HOL/Boogie/Examples/Boogie_Max.b2i Tue Jul 23 13:14:14 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,748 +0,0 @@
-vc max 1
- implies
- label pos 10 7
- true
- implies
- <
- int-num 0
- var length
- int
- implies
- true
- implies
- =
- var max@0
- int
- select 2
- var array
- array 2
- int
- int
- int-num 0
- implies
- and 4
- <=
- int-num 0
- int-num 0
- <=
- int-num 0
- int-num 0
- <=
- int-num 1
- int-num 1
- <=
- int-num 1
- int-num 1
- and 2
- label neg 14 5
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.14:23
- attribute uniqueId 1
- string-attr 2
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- int-num 1
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@0
- int
- implies
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.14:23
- attribute uniqueId 1
- string-attr 2
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- int-num 1
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@0
- int
- and 2
- label neg 15 5
- =
- select 2
- var array
- array 2
- int
- int
- int-num 0
- var max@0
- int
- implies
- =
- select 2
- var array
- array 2
- int
- int
- int-num 0
- var max@0
- int
- implies
- label pos 13 3
- true
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.14:23
- attribute uniqueId 1
- string-attr 2
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var p@0
- int
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@1
- int
- implies
- =
- select 2
- var array
- array 2
- int
- int
- var k@0
- int
- var max@1
- int
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- and 2
- implies
- label pos 13 3
- true
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- >=
- var p@0
- int
- var length
- int
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- label pos 0 0
- true
- implies
- =
- var k@2
- int
- var k@0
- int
- implies
- =
- var max@4
- int
- var max@1
- int
- implies
- =
- var p@2
- int
- var p@0
- int
- implies
- label pos 0 0
- true
- and 2
- label neg 5 3
- exists 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.5:19
- attribute uniqueId 1
- string-attr 1
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var length
- int
- =
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@4
- int
- implies
- exists 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.5:19
- attribute uniqueId 1
- string-attr 1
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var length
- int
- =
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@4
- int
- and 2
- label neg 4 3
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.4:19
- attribute uniqueId 1
- string-attr 0
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var length
- int
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@4
- int
- implies
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.4:19
- attribute uniqueId 1
- string-attr 0
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var length
- int
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@4
- int
- true
- implies
- label pos 17 5
- true
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- <
- var p@0
- int
- var length
- int
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- and 2
- implies
- label pos 17 31
- true
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- >
- select 2
- var array
- array 2
- int
- int
- var p@0
- int
- var max@1
- int
- implies
- =
- var max@2
- int
- select 2
- var array
- array 2
- int
- int
- var p@0
- int
- implies
- and 2
- <=
- int-num 1
- var p@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- label pos 0 0
- true
- implies
- =
- var k@1
- int
- var p@0
- int
- implies
- =
- var max@3
- int
- var max@2
- int
- implies
- label pos 18 7
- true
- implies
- and 2
- <=
- int-num 0
- var k@1
- int
- <=
- int-num 1
- var p@0
- int
- implies
- =
- var p@1
- int
- +
- var p@0
- int
- int-num 1
- implies
- and 2
- <=
- int-num 0
- var k@1
- int
- <=
- int-num 2
- var p@1
- int
- implies
- label pos 0 0
- true
- and 2
- label neg 14 5
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.14:23
- attribute uniqueId 1
- string-attr 2
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var p@1
- int
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@3
- int
- implies
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.14:23
- attribute uniqueId 1
- string-attr 2
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var p@1
- int
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@3
- int
- and 2
- label neg 15 5
- =
- select 2
- var array
- array 2
- int
- int
- var k@1
- int
- var max@3
- int
- implies
- =
- select 2
- var array
- array 2
- int
- int
- var k@1
- int
- var max@3
- int
- implies
- false
- true
- implies
- label pos 17 5
- true
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- <=
- select 2
- var array
- array 2
- int
- int
- var p@0
- int
- var max@1
- int
- implies
- and 2
- <=
- int-num 0
- var k@0
- int
- <=
- int-num 1
- var p@0
- int
- implies
- label pos 0 0
- true
- implies
- =
- var k@1
- int
- var k@0
- int
- implies
- =
- var max@3
- int
- var max@1
- int
- implies
- label pos 18 7
- true
- implies
- and 2
- <=
- int-num 0
- var k@1
- int
- <=
- int-num 1
- var p@0
- int
- implies
- =
- var p@1
- int
- +
- var p@0
- int
- int-num 1
- implies
- and 2
- <=
- int-num 0
- var k@1
- int
- <=
- int-num 2
- var p@1
- int
- implies
- label pos 0 0
- true
- and 2
- label neg 14 5
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.14:23
- attribute uniqueId 1
- string-attr 2
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var p@1
- int
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@3
- int
- implies
- forall 1 0 3
- var i
- int
- attribute qid 1
- string-attr BoogieMa.14:23
- attribute uniqueId 1
- string-attr 2
- attribute bvZ3Native 1
- string-attr False
- implies
- and 2
- <=
- int-num 0
- var i
- int
- <
- var i
- int
- var p@1
- int
- <=
- select 2
- var array
- array 2
- int
- int
- var i
- int
- var max@3
- int
- and 2
- label neg 15 5
- =
- select 2
- var array
- array 2
- int
- int
- var k@1
- int
- var max@3
- int
- implies
- =
- select 2
- var array
- array 2
- int
- int
- var k@1
- int
- var max@3
- int
- implies
- false
- true