diff --git a/examples/add_list/why3shapes.gz b/examples/add_list/why3shapes.gz index 0825d877eaf1794b1c1091ccd5cace4f05ca1768..22d009e04d471853bbee144ac66a72256622ab87 100644 Binary files a/examples/add_list/why3shapes.gz and b/examples/add_list/why3shapes.gz differ diff --git a/examples/add_list_vc_sp/why3shapes.gz b/examples/add_list_vc_sp/why3shapes.gz index a402960436e5f78719d78d40667e209d503aad57..72d12e85523689b8bd118bb3c472f6d87e6d66dc 100644 Binary files a/examples/add_list_vc_sp/why3shapes.gz and b/examples/add_list_vc_sp/why3shapes.gz differ diff --git a/examples/algo63/why3shapes.gz b/examples/algo63/why3shapes.gz index 24a2e7896c7d134fd2e4a87589b24a92e5cc1871..822cfbddd551f499c304801771048a0e4561f85a 100644 Binary files a/examples/algo63/why3shapes.gz and b/examples/algo63/why3shapes.gz differ diff --git a/examples/algo63_fastwp/why3shapes.gz b/examples/algo63_fastwp/why3shapes.gz index e799ade0b435e183bf6608c8a5192a3903ac4d31..903cc413ee49de71234211326bd241f1544f9792 100644 Binary files a/examples/algo63_fastwp/why3shapes.gz and b/examples/algo63_fastwp/why3shapes.gz differ diff --git a/examples/algo64/why3shapes.gz b/examples/algo64/why3shapes.gz index 7914338d6e17d32207ddc7e4bbb3ad76c407354f..8782aaaaf07e8a6e47776d0ee47ff67a5e6aae6d 100644 Binary files a/examples/algo64/why3shapes.gz and b/examples/algo64/why3shapes.gz differ diff --git a/examples/algo65/why3shapes.gz b/examples/algo65/why3shapes.gz index 749b13f067f921eb92e97b547598a61005b79b88..862258c397644dc1e402177611d81a1d34752d8a 100644 Binary files a/examples/algo65/why3shapes.gz and b/examples/algo65/why3shapes.gz differ diff --git a/examples/all_distinct/why3shapes.gz b/examples/all_distinct/why3shapes.gz index 45ee2046efb9aae52152a99719c5fe055d9b09ad..f72c5ac9ac54ebd24044973cfe918037a100ef2d 100644 Binary files a/examples/all_distinct/why3shapes.gz and b/examples/all_distinct/why3shapes.gz differ diff --git a/examples/arm/why3shapes.gz b/examples/arm/why3shapes.gz index ccbb8ee5527f459bfc02f9d53cc2aca16aef8fda..5f03b75dae4c68c6b52e7bcb94825d462bbd71ff 100644 Binary files a/examples/arm/why3shapes.gz and b/examples/arm/why3shapes.gz differ diff --git a/examples/assigning_meanings_to_programs/why3shapes.gz b/examples/assigning_meanings_to_programs/why3shapes.gz index f5c62bc40f6094971f543a56dcfb116e5646cfc9..67dd05daaae01e0e3e502788e45ae3486f86662b 100644 Binary files a/examples/assigning_meanings_to_programs/why3shapes.gz and b/examples/assigning_meanings_to_programs/why3shapes.gz differ diff --git a/examples/avl/avl/why3shapes.gz b/examples/avl/avl/why3shapes.gz index 4ad4f7bb5c2828fbe9b1f204ee95255eebde0e27..b98c89f03562d346101887cb12647c92b283f56f 100644 Binary files a/examples/avl/avl/why3shapes.gz and b/examples/avl/avl/why3shapes.gz differ diff --git a/examples/avl/priority_queue/why3shapes.gz b/examples/avl/priority_queue/why3shapes.gz index 03b493d71ab6b3c4d464c93b12077ec01abfb08b..d9a774fbecfd65194af9a00cd7f51ca3e54912b1 100644 Binary files a/examples/avl/priority_queue/why3shapes.gz and b/examples/avl/priority_queue/why3shapes.gz differ diff --git a/examples/avl/ral/why3shapes.gz b/examples/avl/ral/why3shapes.gz index 1a9e26ed1f2e98971c36a7ee4436c1a76be7b2ec..c2702ab2d42316c8ca05a03e0d0248cf29c1d1b5 100644 Binary files a/examples/avl/ral/why3shapes.gz and b/examples/avl/ral/why3shapes.gz differ diff --git a/examples/avl/tables/why3shapes.gz b/examples/avl/tables/why3shapes.gz index 566195b04746fc6f9681e710c085675e55363e94..0a0229843d5ae4fb66f5a58599285a068d5d19bf 100644 Binary files a/examples/avl/tables/why3shapes.gz and b/examples/avl/tables/why3shapes.gz differ diff --git a/examples/bag/why3shapes.gz b/examples/bag/why3shapes.gz index 3538642d2c4d9be204d228a70538bdf0f779d029..b176f8a080d62cfc548e67ab858420e8920c954b 100644 Binary files a/examples/bag/why3shapes.gz and b/examples/bag/why3shapes.gz differ diff --git a/examples/balance/why3shapes.gz b/examples/balance/why3shapes.gz index 8214d667115e524523860dd522982bbe6bd1353c..f220720694273cc4d805b92733f9a2769aecc8de 100644 Binary files a/examples/balance/why3shapes.gz and b/examples/balance/why3shapes.gz differ diff --git a/examples/bellman_ford/why3shapes.gz b/examples/bellman_ford/why3shapes.gz index aae0dbb068440773e38f9def9734851a9bc928c8..2ffc192e979a674a7aa7c21e373db6afb3c93aa6 100644 Binary files a/examples/bellman_ford/why3shapes.gz and b/examples/bellman_ford/why3shapes.gz differ diff --git a/examples/binary_multiplication/why3shapes.gz b/examples/binary_multiplication/why3shapes.gz index 19fbaf73bb766963a93b79809302c9e2d1afa9e2..ed0eca5dc909fb0cd8b5817b05ef40131fc590e6 100644 Binary files a/examples/binary_multiplication/why3shapes.gz and b/examples/binary_multiplication/why3shapes.gz differ diff --git a/examples/binary_search/why3shapes.gz b/examples/binary_search/why3shapes.gz index 392886c58cb72fe65b82a6e6270ee5e1d34e54fc..86f68e24539e185d0b5c50f6ed9fc082e567591b 100644 Binary files a/examples/binary_search/why3shapes.gz and b/examples/binary_search/why3shapes.gz differ diff --git a/examples/binary_search_vc_sp/why3shapes.gz b/examples/binary_search_vc_sp/why3shapes.gz index 35d47ecd4a8d781a0f3a9b2e4045f90c10836f52..bb8c4d5e8a97a055e7dde6f008a552308a0f779d 100644 Binary files a/examples/binary_search_vc_sp/why3shapes.gz and b/examples/binary_search_vc_sp/why3shapes.gz differ diff --git a/examples/binary_sort/why3shapes.gz b/examples/binary_sort/why3shapes.gz index 4c2d7dd0892ff6eeb51b2f72b03f6db1d866eae3..877250d631083f728204597d7b93afb40bef2550 100644 Binary files a/examples/binary_sort/why3shapes.gz and b/examples/binary_sort/why3shapes.gz differ diff --git a/examples/binomial_heap/why3shapes.gz b/examples/binomial_heap/why3shapes.gz index 65e0441946adfe835e73075fea834b5c6f5fd9d1..013cc0e8283d8c48087956247b62f647c1c23aa0 100644 Binary files a/examples/binomial_heap/why3shapes.gz and b/examples/binomial_heap/why3shapes.gz differ diff --git a/examples/bitcount/why3session.xml b/examples/bitcount/why3session.xml index 17e2a89c7aa034a5df88b975d749be5758339268..a55c5de2e9225d6bbf6c6bd9d8ea43cde3ae57d4 100644 --- a/examples/bitcount/why3session.xml +++ b/examples/bitcount/why3session.xml @@ -300,7 +300,7 @@ - + diff --git a/examples/bitcount/why3shapes.gz b/examples/bitcount/why3shapes.gz index b9d96838ab17634c68b10850a57bb75f8fc8ab98..5df61f340eab96c4cf074f4c40b09376a96a4a6b 100644 Binary files a/examples/bitcount/why3shapes.gz and b/examples/bitcount/why3shapes.gz differ diff --git a/examples/bitvector_examples/why3shapes.gz b/examples/bitvector_examples/why3shapes.gz index 98440c42f47e5b9e974a8c62956cbff198843eff..94d7df2ca0e646e8d7b2f38adfa13cdba23f3158 100644 Binary files a/examples/bitvector_examples/why3shapes.gz and b/examples/bitvector_examples/why3shapes.gz differ diff --git a/examples/bitwalker/why3session.xml b/examples/bitwalker/why3session.xml index 804182a4abdc30f39a93a30c946ba65b6a085194..fd7d8150762d734267e7913fdc72e0e32c64493a 100644 --- a/examples/bitwalker/why3session.xml +++ b/examples/bitwalker/why3session.xml @@ -269,7 +269,7 @@ - + @@ -284,7 +284,7 @@ - + @@ -293,13 +293,13 @@ - + - + diff --git a/examples/bitwalker/why3shapes.gz b/examples/bitwalker/why3shapes.gz index 3635ad168e4e573e92fc3a1a323bb6784c51d982..b36e61b115f0c09c4aded420a30e54160a752174 100644 Binary files a/examples/bitwalker/why3shapes.gz and b/examples/bitwalker/why3shapes.gz differ diff --git a/examples/bresenham/why3shapes.gz b/examples/bresenham/why3shapes.gz index cb64a1de0e15a7a539f38775b450e37d3ff2763d..adc20c3ef61752247a0a1c79cd16c14b8020a00b 100644 Binary files a/examples/bresenham/why3shapes.gz and b/examples/bresenham/why3shapes.gz differ diff --git a/examples/bts/116_array_access/why3shapes.gz b/examples/bts/116_array_access/why3shapes.gz index 219f4310b2e720abf022bc433c36b99251330f8c..526c9451769c8a1db2174ceb20b3217ec025aff9 100644 Binary files a/examples/bts/116_array_access/why3shapes.gz and b/examples/bts/116_array_access/why3shapes.gz differ diff --git a/examples/bts/16972/why3shapes.gz b/examples/bts/16972/why3shapes.gz index 5c499295c8218b81d569ba1d5f5e7b15133c6d7e..13820155aaaa79d70d22bc004c078aa7e2cd9c41 100644 Binary files a/examples/bts/16972/why3shapes.gz and b/examples/bts/16972/why3shapes.gz differ diff --git a/examples/bubble_sort/why3shapes.gz b/examples/bubble_sort/why3shapes.gz index 5d19a34474b930dbd926bc9cd91689f272d6322f..c588b6ac71cfaa58be8f5f8fde1dc3299eda3922 100644 Binary files a/examples/bubble_sort/why3shapes.gz and b/examples/bubble_sort/why3shapes.gz differ diff --git a/examples/checking_a_large_routine/why3shapes.gz b/examples/checking_a_large_routine/why3shapes.gz index 10bc23d7d45cadb00fac30269bef0a9f2e56eb87..a2a318fbab25bc5a7e8424704b9f2ff50f5a4d83 100644 Binary files a/examples/checking_a_large_routine/why3shapes.gz and b/examples/checking_a_large_routine/why3shapes.gz differ diff --git a/examples/coincidence_count/why3shapes.gz b/examples/coincidence_count/why3shapes.gz index d110ef01aea5f3a3871c50435e19e257fd762c10..7aa33a168f373828d99d2adfb081a73dc10e25c1 100644 Binary files a/examples/coincidence_count/why3shapes.gz and b/examples/coincidence_count/why3shapes.gz differ diff --git a/examples/conjugate/why3shapes.gz b/examples/conjugate/why3shapes.gz index 91a114765c1048268b78df56d54070033334e0e7..164b569f3df85e8f0030c4a9201bfa9b04056435 100644 Binary files a/examples/conjugate/why3shapes.gz and b/examples/conjugate/why3shapes.gz differ diff --git a/examples/counting_sort/why3session.xml b/examples/counting_sort/why3session.xml index 0ff71a2986c487528c65b244c826e96079c8ac7f..9188c8c05d72158cbdb46c95d7e64e62f6a5f01c 100644 --- a/examples/counting_sort/why3session.xml +++ b/examples/counting_sort/why3session.xml @@ -77,7 +77,7 @@ - + @@ -179,7 +179,7 @@ - + diff --git a/examples/counting_sort/why3shapes.gz b/examples/counting_sort/why3shapes.gz index 3be22db9561f777ed68a86bde1001429130b13b5..3a96bb16a2b9fd6a27397e2559707f5dc3863526 100644 Binary files a/examples/counting_sort/why3shapes.gz and b/examples/counting_sort/why3shapes.gz differ diff --git a/examples/cubic_root/why3shapes.gz b/examples/cubic_root/why3shapes.gz index d9d48263eeb6c412f4ce2297606525a851cd0d7e..a7b15dd131156629bcf839b53e0d38f6985bc505 100644 Binary files a/examples/cubic_root/why3shapes.gz and b/examples/cubic_root/why3shapes.gz differ diff --git a/examples/cursor_examples/why3shapes.gz b/examples/cursor_examples/why3shapes.gz index a9b1b1d5c2231072d92eb43e972ae41e3527b4d8..724b501cc9945a3626cf2b8b8f58f4be5286c033 100644 Binary files a/examples/cursor_examples/why3shapes.gz and b/examples/cursor_examples/why3shapes.gz differ diff --git a/examples/decrease1/why3shapes.gz b/examples/decrease1/why3shapes.gz index 8abd528cd157a02c76fb399f34e148a89742623e..64ff5a176aa8fe4f1a4532b8c80809f7b6acb6e8 100644 Binary files a/examples/decrease1/why3shapes.gz and b/examples/decrease1/why3shapes.gz differ diff --git a/examples/dfa_example/why3shapes.gz b/examples/dfa_example/why3shapes.gz index a3d1f7f0612943ef2eb2c72ccf96184b32b3927f..977a1a24188f7f4f3cd31503a7f612a0128d435f 100644 Binary files a/examples/dfa_example/why3shapes.gz and b/examples/dfa_example/why3shapes.gz differ diff --git a/examples/dfs/why3shapes.gz b/examples/dfs/why3shapes.gz index 6b744b8d457ce03628108963c1bb1732eb1f4430..7894998924252503c548b95d1f122da60a15613c 100644 Binary files a/examples/dfs/why3shapes.gz and b/examples/dfs/why3shapes.gz differ diff --git a/examples/dijkstra/why3session.xml b/examples/dijkstra/why3session.xml index 35dbaae45039647ae06cfd065552b335d2f87a7d..63cc89e01ae099e0f1ad982ad50cf5bf5586c5c2 100644 --- a/examples/dijkstra/why3session.xml +++ b/examples/dijkstra/why3session.xml @@ -16,13 +16,13 @@ - + - + @@ -108,7 +108,7 @@ - + diff --git a/examples/dijkstra/why3shapes.gz b/examples/dijkstra/why3shapes.gz index 9a19d1ae061a28b9c2e090edd82d31cc5b22e268..01294fe7c25d60fb6903b5fb5f355bbac473175d 100644 Binary files a/examples/dijkstra/why3shapes.gz and b/examples/dijkstra/why3shapes.gz differ diff --git a/examples/division/why3shapes.gz b/examples/division/why3shapes.gz index 5d3a5a8b9a2b2694629233aace78dae4bb5ca4a0..ae20351b1585f82610c5834d8a73ed28f6ea9f08 100644 Binary files a/examples/division/why3shapes.gz and b/examples/division/why3shapes.gz differ diff --git a/examples/double_wp/compiler/why3shapes.gz b/examples/double_wp/compiler/why3shapes.gz index ae3bc85cd1b8358190a06ac7c0ef97a7aa0fe752..8748c2b7b76a977ef6ef087ab30d9a068b9c67bd 100644 Binary files a/examples/double_wp/compiler/why3shapes.gz and b/examples/double_wp/compiler/why3shapes.gz differ diff --git a/examples/double_wp/logic/why3shapes.gz b/examples/double_wp/logic/why3shapes.gz index 00a9240904a8fa63c268e22c249ed7c583902499..79c300677ca3a681be30551b1deec00952708e5d 100644 Binary files a/examples/double_wp/logic/why3shapes.gz and b/examples/double_wp/logic/why3shapes.gz differ diff --git a/examples/double_wp/specs/why3shapes.gz b/examples/double_wp/specs/why3shapes.gz index df70a68b434e8472e206d0c505d6d9f0818005be..1b3217592ebdd6df39094de516c8c517a17321ca 100644 Binary files a/examples/double_wp/specs/why3shapes.gz and b/examples/double_wp/specs/why3shapes.gz differ diff --git a/examples/dyck/why3shapes.gz b/examples/dyck/why3shapes.gz index 05bdbe6d581096555163dbb21fceb0698803aef8..0bdbc3bcceea06db79148dafca6d4379b6769983 100644 Binary files a/examples/dyck/why3shapes.gz and b/examples/dyck/why3shapes.gz differ diff --git a/examples/edit_distance/why3shapes.gz b/examples/edit_distance/why3shapes.gz index 9498a416c52966fd01fdbe419344a9f71bfc24de..ff6975de2e5a6ed67287affae80110ea36012705 100644 Binary files a/examples/edit_distance/why3shapes.gz and b/examples/edit_distance/why3shapes.gz differ diff --git a/examples/esterel/why3shapes.gz b/examples/esterel/why3shapes.gz index f4941acde086dd97bae6427a4f254db1caea5051..b11ba638e69480154e658c357845fe11e71352f4 100644 Binary files a/examples/esterel/why3shapes.gz and b/examples/esterel/why3shapes.gz differ diff --git a/examples/euler002/why3shapes.gz b/examples/euler002/why3shapes.gz index e535a4df402619e02ec34935f7998940f9f9bb04..48e958ef47bf9172681852724f5b53d57dfb4f3a 100644 Binary files a/examples/euler002/why3shapes.gz and b/examples/euler002/why3shapes.gz differ diff --git a/examples/euler011/why3shapes.gz b/examples/euler011/why3shapes.gz index 1818c0fa09f8e229c50a3a6bd8939a5c709bdd2e..8faf912fbfdd9b08514dff58a2a47fdec6ee0a70 100644 Binary files a/examples/euler011/why3shapes.gz and b/examples/euler011/why3shapes.gz differ diff --git a/examples/ewd673/why3shapes.gz b/examples/ewd673/why3shapes.gz index 5290ed0e0cb52509bc686fc4bb4fcef11e025bce..e6ab71a8268d91c46fc3fa1ff00174e371bab5d6 100644 Binary files a/examples/ewd673/why3shapes.gz and b/examples/ewd673/why3shapes.gz differ diff --git a/examples/fact/why3shapes.gz b/examples/fact/why3shapes.gz index 6957641d79ddeb052bd684c274c47584f302fc22..30afc277df1204d21263e601fa12981d34f59f74 100644 Binary files a/examples/fact/why3shapes.gz and b/examples/fact/why3shapes.gz differ diff --git a/examples/fact_vc_sp/why3shapes.gz b/examples/fact_vc_sp/why3shapes.gz index c4765bb754f538206b4b9f1c71cb863b6c6493ad..99a84844961b386e3493651ea5f05b047ecff063 100644 Binary files a/examples/fact_vc_sp/why3shapes.gz and b/examples/fact_vc_sp/why3shapes.gz differ diff --git a/examples/fenwick/why3shapes.gz b/examples/fenwick/why3shapes.gz index 19d3268b1f343170e503c4848ec99652c4fdfa50..9cdeabefc4dcffc5e123aa4ed044059ec02ced1a 100644 Binary files a/examples/fenwick/why3shapes.gz and b/examples/fenwick/why3shapes.gz differ diff --git a/examples/fib_memo/why3shapes.gz b/examples/fib_memo/why3shapes.gz index df54397533c71c7a1716abbf01ac17ff8e777e3c..b0f332a5a4599ca5321f850451fde79aaad345e7 100644 Binary files a/examples/fib_memo/why3shapes.gz and b/examples/fib_memo/why3shapes.gz differ diff --git a/examples/fibonacci/why3shapes.gz b/examples/fibonacci/why3shapes.gz index 9459899954935e044818cfcc49fb17bc6a9a7770..8fe05302c341c0b6527c515b8be1349393fb4e3d 100644 Binary files a/examples/fibonacci/why3shapes.gz and b/examples/fibonacci/why3shapes.gz differ diff --git a/examples/fill/why3shapes.gz b/examples/fill/why3shapes.gz index 245bdcaef3e70bc428fc97482c31e96f3b4b3e1b..f3395ae68ece01bab72ede559230a266f176d9fb 100644 Binary files a/examples/fill/why3shapes.gz and b/examples/fill/why3shapes.gz differ diff --git a/examples/find/why3shapes.gz b/examples/find/why3shapes.gz index 8aaf5492f4d577b13e4bd3a1699d20f0779d19b0..37bc78444d699826ec3ceec215e484688dcde147 100644 Binary files a/examples/find/why3shapes.gz and b/examples/find/why3shapes.gz differ diff --git a/examples/finite_tarski/why3shapes.gz b/examples/finite_tarski/why3shapes.gz index 439b743a92c8031dc0bbd9430307f43564e221fd..4053518c96d124362bbacd67b05def4a5bf41a06 100644 Binary files a/examples/finite_tarski/why3shapes.gz and b/examples/finite_tarski/why3shapes.gz differ diff --git a/examples/flag/why3shapes.gz b/examples/flag/why3shapes.gz index bf5cdc64b252e9f02441c84518390e500ed2f523..57623b88c537aa2d0050268c559ff005ec0104a0 100644 Binary files a/examples/flag/why3shapes.gz and b/examples/flag/why3shapes.gz differ diff --git a/examples/flag2/why3shapes.gz b/examples/flag2/why3shapes.gz index fd1dc48e494a096e72b1d29dd5948b3467da576d..dcce63cd050c7823e460339efeeea0dcbb69968b 100644 Binary files a/examples/flag2/why3shapes.gz and b/examples/flag2/why3shapes.gz differ diff --git a/examples/foveoos11-cm/array_max/why3shapes.gz b/examples/foveoos11-cm/array_max/why3shapes.gz index 2dee980fb5caf0f0602117d7c2396c363388b9e7..b44ea14b32ccb8039c5dcb53fb1735c4e48ff20e 100644 Binary files a/examples/foveoos11-cm/array_max/why3shapes.gz and b/examples/foveoos11-cm/array_max/why3shapes.gz differ diff --git a/examples/foveoos11-cm/duplets/why3shapes.gz b/examples/foveoos11-cm/duplets/why3shapes.gz index 5efe8a524916c33f80b339a7b5883468bf98f4e6..86d6e414c38fb46c2d46ba1afe0c48ac69242b41 100644 Binary files a/examples/foveoos11-cm/duplets/why3shapes.gz and b/examples/foveoos11-cm/duplets/why3shapes.gz differ diff --git a/examples/foveoos11_challenge1/why3shapes.gz b/examples/foveoos11_challenge1/why3shapes.gz index f585d2b271936041acdcc0fdec3fa2a7a621f58f..a7031ecf2e91796b2d00e2ac6ce95f55a512b4f7 100644 Binary files a/examples/foveoos11_challenge1/why3shapes.gz and b/examples/foveoos11_challenge1/why3shapes.gz differ diff --git a/examples/foveoos11_challenge3/why3session.xml b/examples/foveoos11_challenge3/why3session.xml index 5f76463e342f557eca21424b5a246bf3cfc54bf6..30f02ab8aade806692185a2cbd54cefcce43cdef 100644 --- a/examples/foveoos11_challenge3/why3session.xml +++ b/examples/foveoos11_challenge3/why3session.xml @@ -157,7 +157,7 @@ - + diff --git a/examples/foveoos11_challenge3/why3shapes.gz b/examples/foveoos11_challenge3/why3shapes.gz index 1f8c65f62cee927fb73b7844bcc2ad7c6e2076c7..ef86bd8d265cd1a123116319a7814c53fa5109f4 100644 Binary files a/examples/foveoos11_challenge3/why3shapes.gz and b/examples/foveoos11_challenge3/why3shapes.gz differ diff --git a/examples/gcd/why3shapes.gz b/examples/gcd/why3shapes.gz index 8cbe3f430dd7d9d65cf5b2074c9c159362ef8663..e45167c1d5589d00f9c4c2de6a2bcc6fa425ba03 100644 Binary files a/examples/gcd/why3shapes.gz and b/examples/gcd/why3shapes.gz differ diff --git a/examples/gcd_bezout/why3shapes.gz b/examples/gcd_bezout/why3shapes.gz index 1dcb90577d6f1debc6d32b51ae7960467084ca60..9dac9ec5446be1a439033ed96644a4ac5183b90b 100644 Binary files a/examples/gcd_bezout/why3shapes.gz and b/examples/gcd_bezout/why3shapes.gz differ diff --git a/examples/gcd_bezout_vc_sp/why3shapes.gz b/examples/gcd_bezout_vc_sp/why3shapes.gz index 9e6b0d7e583dd2bd6ab8adb7accc5eeebee0991a..e72d4c2c7e37153f451fe2f64db49eed737b0e95 100644 Binary files a/examples/gcd_bezout_vc_sp/why3shapes.gz and b/examples/gcd_bezout_vc_sp/why3shapes.gz differ diff --git a/examples/gcd_vc_sp/why3shapes.gz b/examples/gcd_vc_sp/why3shapes.gz index 5f831c44e4e80659d21cc9de69b971b94c15a17c..b152c509b48868503ef5f3b833ec634eaa85aa5a 100644 Binary files a/examples/gcd_vc_sp/why3shapes.gz and b/examples/gcd_vc_sp/why3shapes.gz differ diff --git a/examples/generate_all_trees/why3session.xml b/examples/generate_all_trees/why3session.xml index bf464180125c955752f75f4e4201b02514b6f41e..fc8efa21db8e72cb1abc02e8b1b6f316ed8c2749 100644 --- a/examples/generate_all_trees/why3session.xml +++ b/examples/generate_all_trees/why3session.xml @@ -19,10 +19,10 @@ - + - + diff --git a/examples/generate_all_trees/why3shapes.gz b/examples/generate_all_trees/why3shapes.gz index 49041fce15159b534eeb10438bf08c838ac72ad8..5d8e01ee3bd3b524493da5b47eed101e4229a372 100644 Binary files a/examples/generate_all_trees/why3shapes.gz and b/examples/generate_all_trees/why3shapes.gz differ diff --git a/examples/gnome_sort/why3shapes.gz b/examples/gnome_sort/why3shapes.gz index c7531a7d87b0974fa11702ba8ac8a31e43759327..a588f14057296076f257d028e1ce2ca0f810e93d 100644 Binary files a/examples/gnome_sort/why3shapes.gz and b/examples/gnome_sort/why3shapes.gz differ diff --git a/examples/hashtbl_impl/why3shapes.gz b/examples/hashtbl_impl/why3shapes.gz index 7cdf03ca1c4b078742a0388ded7482da8ce28284..0ffdd015aea13af1bf04e620c47a07cd599e1e82 100644 Binary files a/examples/hashtbl_impl/why3shapes.gz and b/examples/hashtbl_impl/why3shapes.gz differ diff --git a/examples/hillel_challenge/why3shapes.gz b/examples/hillel_challenge/why3shapes.gz index ce8d8ff4ab873b7d70c75954b5d24d994ebac8a7..8c88c66d842b5dbe6da53cbb2b59fae65fd55df6 100644 Binary files a/examples/hillel_challenge/why3shapes.gz and b/examples/hillel_challenge/why3shapes.gz differ diff --git a/examples/induction/why3shapes.gz b/examples/induction/why3shapes.gz index d358f61203e0e95f3db4a39ec9e28846fabf770c..02194c0415997a543c1a01c63355f406d009b043 100644 Binary files a/examples/induction/why3shapes.gz and b/examples/induction/why3shapes.gz differ diff --git a/examples/insertion_sort/why3shapes.gz b/examples/insertion_sort/why3shapes.gz index d6e5a10cb38edd9a7923f040e775715dcd56d802..32531a932b8124d4e7958357e3a79d3af19bf52b 100644 Binary files a/examples/insertion_sort/why3shapes.gz and b/examples/insertion_sort/why3shapes.gz differ diff --git a/examples/insertion_sort_naive/why3shapes.gz b/examples/insertion_sort_naive/why3shapes.gz index 14a86eb7a3ab2309c390140f41ade93dca8a6ac6..5f15aff2d2b8f1ba90cdf0686ecbb8f58ae4e3c2 100644 Binary files a/examples/insertion_sort_naive/why3shapes.gz and b/examples/insertion_sort_naive/why3shapes.gz differ diff --git a/examples/inverse_in_place/why3shapes.gz b/examples/inverse_in_place/why3shapes.gz index 312e38aed87f713774273ea6682498cd6171a763..6fe9e9715df0858ed81c6c6d9c383d73c9f58c3f 100644 Binary files a/examples/inverse_in_place/why3shapes.gz and b/examples/inverse_in_place/why3shapes.gz differ diff --git a/examples/isqrt/why3shapes.gz b/examples/isqrt/why3shapes.gz index 0222c55a9f060148fe6cfb7332f835b1aa67d893..ba4e6affee7a3859168db1d29b1251b4050f83cb 100644 Binary files a/examples/isqrt/why3shapes.gz and b/examples/isqrt/why3shapes.gz differ diff --git a/examples/isqrt_von_neumann/why3session.xml b/examples/isqrt_von_neumann/why3session.xml index a775d2c6cbcdcf4d4cdfcf85dea947aafd933bf8..3a1b7194a016d73c713758d28aab43f79313b7d2 100644 --- a/examples/isqrt_von_neumann/why3session.xml +++ b/examples/isqrt_von_neumann/why3session.xml @@ -380,7 +380,7 @@ - + @@ -401,7 +401,7 @@ - + @@ -611,7 +611,7 @@ - + @@ -650,7 +650,7 @@ - + @@ -674,12 +674,12 @@ - + - + diff --git a/examples/isqrt_von_neumann/why3shapes.gz b/examples/isqrt_von_neumann/why3shapes.gz index e50bb999ef82ad47019191559f8881fcc98e675f..83fa0615ae259989e353ea2bff7ba5e42f4aa4b7 100644 Binary files a/examples/isqrt_von_neumann/why3shapes.gz and b/examples/isqrt_von_neumann/why3shapes.gz differ diff --git a/examples/kmp/why3shapes.gz b/examples/kmp/why3shapes.gz index fe66136443237e4fc4e35a8c8b31dfd140026df4..9551927e2294110682615127e703f43f8e8de997 100644 Binary files a/examples/kmp/why3shapes.gz and b/examples/kmp/why3shapes.gz differ diff --git a/examples/knuth_prime_numbers/why3shapes.gz b/examples/knuth_prime_numbers/why3shapes.gz index 4a11c6a45b48b1497b94a3e26678d6b8285d4ad3..2aa6421520a42661922d79a4bc1fe550aa90a376 100644 Binary files a/examples/knuth_prime_numbers/why3shapes.gz and b/examples/knuth_prime_numbers/why3shapes.gz differ diff --git a/examples/koda_ruskey/why3session.xml b/examples/koda_ruskey/why3session.xml index 3bf0b82418133a945652c3bca153c1b3fe963ab8..e5c8b3615fc1427d160087f5a77964f0ddeca268 100644 --- a/examples/koda_ruskey/why3session.xml +++ b/examples/koda_ruskey/why3session.xml @@ -549,7 +549,7 @@ - + diff --git a/examples/koda_ruskey/why3shapes.gz b/examples/koda_ruskey/why3shapes.gz index 0cb378996e34231bc9715edfaf93676e03a1c9d5..9a48b49cb06abebbe45a991ae5d4ac954c0b940d 100644 Binary files a/examples/koda_ruskey/why3shapes.gz and b/examples/koda_ruskey/why3shapes.gz differ diff --git a/examples/largest_prime_factor/why3shapes.gz b/examples/largest_prime_factor/why3shapes.gz index 57bdc96b4727927812b48352e7f9d166e0066734..2c6403344e3cf5a0985d267ff83cb4777d767ae2 100644 Binary files a/examples/largest_prime_factor/why3shapes.gz and b/examples/largest_prime_factor/why3shapes.gz differ diff --git a/examples/lcp/why3shapes.gz b/examples/lcp/why3shapes.gz index 3d8fe58f67ea1f53c86c8adf3a8d8b0dcc1609b0..ecd07ceec8944ba79409c27a79e9a5dca12a370a 100644 Binary files a/examples/lcp/why3shapes.gz and b/examples/lcp/why3shapes.gz differ diff --git a/examples/linear_probing/why3session.xml b/examples/linear_probing/why3session.xml index 02e4d0f14c67a4731aecc54aaca5f2dc8bc564c9..ce596d73cf79687d5c061d851f110cc44bfdf0d5 100644 --- a/examples/linear_probing/why3session.xml +++ b/examples/linear_probing/why3session.xml @@ -487,7 +487,7 @@ - + diff --git a/examples/linear_probing/why3shapes.gz b/examples/linear_probing/why3shapes.gz index 474c1e323d16b340140e8f064376300675908030..6ab58c8b43f3fbec857155957bfec3d81fca97c4 100644 Binary files a/examples/linear_probing/why3shapes.gz and b/examples/linear_probing/why3shapes.gz differ diff --git a/examples/linked_list_rev/why3session.xml b/examples/linked_list_rev/why3session.xml index 215c6e691b3a7810c351f38586cd33cb79a4ad0a..fd8cf4f9a53c09ff50d3fdf985ec30e450ebe5de 100644 --- a/examples/linked_list_rev/why3session.xml +++ b/examples/linked_list_rev/why3session.xml @@ -378,7 +378,7 @@ - + diff --git a/examples/linked_list_rev/why3shapes.gz b/examples/linked_list_rev/why3shapes.gz index 869f5edd92432f8d80a0e36e5f00c5460099ea53..d28808847117fcd6937c373a9ab1364fd554834d 100644 Binary files a/examples/linked_list_rev/why3shapes.gz and b/examples/linked_list_rev/why3shapes.gz differ diff --git a/examples/max_matrix/why3session.xml b/examples/max_matrix/why3session.xml index 14030af3ddb8d572523b4083c9d59163757490c5..14d0cadc24106856e5dd46fdd09dfe0a2cfc7717 100644 --- a/examples/max_matrix/why3session.xml +++ b/examples/max_matrix/why3session.xml @@ -32,7 +32,7 @@ - + diff --git a/examples/max_matrix/why3shapes.gz b/examples/max_matrix/why3shapes.gz index 4a7359b901f9109e16eb36d19fab95a3b6ef0d52..d967ec925c57119c7a04430ff2c6c9efc8f1a1ba 100644 Binary files a/examples/max_matrix/why3shapes.gz and b/examples/max_matrix/why3shapes.gz differ diff --git a/examples/maximum_subarray/why3shapes.gz b/examples/maximum_subarray/why3shapes.gz index d28fc921bed1c1541267df1b03e46618cf25d4ec..bda91078e51623d47097e285408cd7b673e744e9 100644 Binary files a/examples/maximum_subarray/why3shapes.gz and b/examples/maximum_subarray/why3shapes.gz differ diff --git a/examples/mccarthy/why3shapes.gz b/examples/mccarthy/why3shapes.gz index 2b485ff2f85112cbc08f54fa27e72afb44740297..00bb287278dab5f38196389dbc195343be4d32b6 100644 Binary files a/examples/mccarthy/why3shapes.gz and b/examples/mccarthy/why3shapes.gz differ diff --git a/examples/mccarthy_vc_sp/why3shapes.gz b/examples/mccarthy_vc_sp/why3shapes.gz index 618b7426d4e27517a79b31d098f171cc5a387ea1..fc1b78c8e5ee4f75d3e4f5576c084e29d4842957 100644 Binary files a/examples/mccarthy_vc_sp/why3shapes.gz and b/examples/mccarthy_vc_sp/why3shapes.gz differ diff --git a/examples/mergesort_array/why3session.xml b/examples/mergesort_array/why3session.xml index 8a7d0c61db0a2c1524695099387a7b31370982d8..24b845603d7fdcc2996cdff574c42b21a9e5048d 100644 --- a/examples/mergesort_array/why3session.xml +++ b/examples/mergesort_array/why3session.xml @@ -28,7 +28,7 @@ - + @@ -145,7 +145,7 @@ - + @@ -185,7 +185,7 @@ - + @@ -514,7 +514,7 @@ - + @@ -529,7 +529,7 @@ - + @@ -541,7 +541,7 @@ - + diff --git a/examples/mergesort_array/why3shapes.gz b/examples/mergesort_array/why3shapes.gz index cbe933adc0590a2157037844fe82b8d611c33f41..164da48f2aac777cfce9487ef0b969a037d3d2d7 100644 Binary files a/examples/mergesort_array/why3shapes.gz and b/examples/mergesort_array/why3shapes.gz differ diff --git a/examples/mergesort_queue/why3shapes.gz b/examples/mergesort_queue/why3shapes.gz index 08893f89588b837793ba9e9c25a6db864cc623cb..09560d93d23fdd53d31f8b500b0d0add0fd1309c 100644 Binary files a/examples/mergesort_queue/why3shapes.gz and b/examples/mergesort_queue/why3shapes.gz differ diff --git a/examples/mex/why3shapes.gz b/examples/mex/why3shapes.gz index 1218c5e5c01c0d1c5b57a948a3427380b4caaa9d..ec2f818cbb98866aeaa2eb38b0606b9a2612be78 100644 Binary files a/examples/mex/why3shapes.gz and b/examples/mex/why3shapes.gz differ diff --git a/examples/mjrty/why3shapes.gz b/examples/mjrty/why3shapes.gz index 0e6d022ce992d063f1475f633720586bc9ff762f..0462eb8090b6cb2bccb30bebf18517982d91746f 100644 Binary files a/examples/mjrty/why3shapes.gz and b/examples/mjrty/why3shapes.gz differ diff --git a/examples/muller/why3shapes.gz b/examples/muller/why3shapes.gz index 16811ce29b5911d02d61ce9b0149522e5c99a79f..c3304fe3d200a9abe0d2b367edd40eedf74b60ae 100644 Binary files a/examples/muller/why3shapes.gz and b/examples/muller/why3shapes.gz differ diff --git a/examples/multiprecision/add/why3session.xml b/examples/multiprecision/add/why3session.xml index 074aa882364fcda0fab08bc147d03739a9770b2b..9b680b7103fbf6c65e804bad0388c6e88b7248cb 100644 --- a/examples/multiprecision/add/why3session.xml +++ b/examples/multiprecision/add/why3session.xml @@ -747,7 +747,7 @@ - + @@ -1264,7 +1264,7 @@ - + @@ -1286,7 +1286,7 @@ - + @@ -1295,16 +1295,16 @@ - + - + - + @@ -1337,7 +1337,7 @@ - + @@ -1354,12 +1354,12 @@ - + - + @@ -1368,16 +1368,16 @@ - + - + - + diff --git a/examples/multiprecision/add/why3shapes.gz b/examples/multiprecision/add/why3shapes.gz index 0b23389ab5441b2455b66926903f31d0b6acd747..09d12f2598b6acefc24cc204ac3672b2b233a138 100644 Binary files a/examples/multiprecision/add/why3shapes.gz and b/examples/multiprecision/add/why3shapes.gz differ diff --git a/examples/multiprecision/compare/why3shapes.gz b/examples/multiprecision/compare/why3shapes.gz index aa12c16ca6ea0c812fa1b1a70147d408bdfaf2e6..6407aea33980c8f6b162b4646e8eb3695d9a71db 100644 Binary files a/examples/multiprecision/compare/why3shapes.gz and b/examples/multiprecision/compare/why3shapes.gz differ diff --git a/examples/multiprecision/lemmas/why3shapes.gz b/examples/multiprecision/lemmas/why3shapes.gz index 305092a368a35e4ccd283ffd59f5f767440ae659..95fa3a62c4a51f60399579a1724aac8990010e29 100644 Binary files a/examples/multiprecision/lemmas/why3shapes.gz and b/examples/multiprecision/lemmas/why3shapes.gz differ diff --git a/examples/multiprecision/logical/why3session.xml b/examples/multiprecision/logical/why3session.xml index 61a8f04443b56c264857236e2b6cabbc340dd565..0717b81942c518e63cabf5c38c2295eb5baaf9f0 100644 --- a/examples/multiprecision/logical/why3session.xml +++ b/examples/multiprecision/logical/why3session.xml @@ -1110,7 +1110,7 @@ - + @@ -1128,7 +1128,7 @@ - + @@ -1176,7 +1176,7 @@ - + @@ -1221,7 +1221,7 @@ - + @@ -1236,10 +1236,10 @@ - + - + @@ -1248,10 +1248,10 @@ - + - + @@ -1269,7 +1269,7 @@ - + @@ -1302,7 +1302,7 @@ - + @@ -1367,10 +1367,10 @@ - + - + diff --git a/examples/multiprecision/logical/why3shapes.gz b/examples/multiprecision/logical/why3shapes.gz index 5954186c16cff7ad57435e7c0167f500c489429e..4452534ad2bef6dca32e14d6a98ccca005cbed32 100644 Binary files a/examples/multiprecision/logical/why3shapes.gz and b/examples/multiprecision/logical/why3shapes.gz differ diff --git a/examples/multiprecision/mul/why3session.xml b/examples/multiprecision/mul/why3session.xml index 5b6ef244214940488b9d70e8761d5c421ef20478..cbc6e12ae030d44d84b8eee562b404650580f386 100644 --- a/examples/multiprecision/mul/why3session.xml +++ b/examples/multiprecision/mul/why3session.xml @@ -111,10 +111,10 @@ - + - + @@ -161,10 +161,10 @@ - + - + @@ -205,7 +205,7 @@ - + @@ -234,7 +234,7 @@ - + @@ -645,7 +645,7 @@ - + @@ -654,7 +654,7 @@ - + @@ -1071,7 +1071,7 @@ - + @@ -1086,7 +1086,7 @@ - + @@ -1110,7 +1110,7 @@ - + @@ -1209,7 +1209,7 @@ - + @@ -1293,7 +1293,7 @@ - + @@ -1308,7 +1308,7 @@ - + diff --git a/examples/multiprecision/mul/why3shapes.gz b/examples/multiprecision/mul/why3shapes.gz index 686074a68b75ff7260c71dfda19e247d75a7b7f3..07892ef8b3e08896be87e1d805add55e9de480b7 100644 Binary files a/examples/multiprecision/mul/why3shapes.gz and b/examples/multiprecision/mul/why3shapes.gz differ diff --git a/examples/multiprecision/sub/why3session.xml b/examples/multiprecision/sub/why3session.xml index 37c614231a6ed2b4dacdeaea093da64c9ac6aa96..8278786c8af1fe57a4ed04828c84dbfaa4c701c5 100644 --- a/examples/multiprecision/sub/why3session.xml +++ b/examples/multiprecision/sub/why3session.xml @@ -400,10 +400,10 @@ - + - + @@ -725,7 +725,7 @@ - + @@ -752,10 +752,10 @@ - + - + @@ -784,7 +784,7 @@ - + @@ -1070,7 +1070,7 @@ - + @@ -1085,7 +1085,7 @@ - + @@ -1102,7 +1102,7 @@ - + @@ -1272,38 +1272,19 @@ - + - - - - - - - - - - - - - - - - - - - - + - + - + @@ -1348,19 +1329,38 @@ - + - + + + + + + + + + + + + + + + + + + + + - + - + @@ -1492,7 +1492,7 @@ - + @@ -1504,7 +1504,7 @@ - + diff --git a/examples/multiprecision/sub/why3shapes.gz b/examples/multiprecision/sub/why3shapes.gz index a6fd73319b4b34bb8230e508ee26b44bf79d7925..d64454f49cfff4ec7a49547f7dfd1ba350911b30 100644 Binary files a/examples/multiprecision/sub/why3shapes.gz and b/examples/multiprecision/sub/why3shapes.gz differ diff --git a/examples/multiprecision/util/why3shapes.gz b/examples/multiprecision/util/why3shapes.gz index bed1d45efc090a9b6cd18bb86e42f409774914fe..4b9bf42b7d429c4f1de0850ee98d448de6205555 100644 Binary files a/examples/multiprecision/util/why3shapes.gz and b/examples/multiprecision/util/why3shapes.gz differ diff --git a/examples/nistonacci/why3shapes.gz b/examples/nistonacci/why3shapes.gz index 749d04f7896e2a7a1898a38642898b3f8a6bc3bd..548f875d6145f675eb1cdb12844969fef2b7e84d 100644 Binary files a/examples/nistonacci/why3shapes.gz and b/examples/nistonacci/why3shapes.gz differ diff --git a/examples/optimal_replay/why3shapes.gz b/examples/optimal_replay/why3shapes.gz index 37752287e7ca1da8d0e81c62f031bb3342c4caef..a59e89c6e73644e8436a256eebb1bc61643f28d9 100644 Binary files a/examples/optimal_replay/why3shapes.gz and b/examples/optimal_replay/why3shapes.gz differ diff --git a/examples/pancake_sorting/why3shapes.gz b/examples/pancake_sorting/why3shapes.gz index 91bb54badc8d34ae6b5ac2488d14af61fee0135c..2a81d42c61a4c62ecce3220f9efe9d45a503d089 100644 Binary files a/examples/pancake_sorting/why3shapes.gz and b/examples/pancake_sorting/why3shapes.gz differ diff --git a/examples/patience/why3shapes.gz b/examples/patience/why3shapes.gz index 8bc2e7c0332476279b979437cbff1e807c9012f8..08ce54c53b16240915fb063bd7d9739970dd6ea8 100644 Binary files a/examples/patience/why3shapes.gz and b/examples/patience/why3shapes.gz differ diff --git a/examples/pigeonhole/why3shapes.gz b/examples/pigeonhole/why3shapes.gz index f577795ad7917cbdda8a39652cff2a6a754be5f0..5900e2f6ed7edf36eb24605445dde3075f5df4ea 100644 Binary files a/examples/pigeonhole/why3shapes.gz and b/examples/pigeonhole/why3shapes.gz differ diff --git a/examples/power/why3shapes.gz b/examples/power/why3shapes.gz index fa88b6396b2089e674c2e80dde7e3f476ed8d088..d477215a1f030293392bbb1e761ea51b67d351ae 100644 Binary files a/examples/power/why3shapes.gz and b/examples/power/why3shapes.gz differ diff --git a/examples/power_vc_sp/why3shapes.gz b/examples/power_vc_sp/why3shapes.gz index 91f508f9bed1aa64306c323c8fd63a2c407e4d71..7e81e6d8122713f42afc628e695f7eb48af53de3 100644 Binary files a/examples/power_vc_sp/why3shapes.gz and b/examples/power_vc_sp/why3shapes.gz differ diff --git a/examples/prover/BacktrackArray/why3shapes.gz b/examples/prover/BacktrackArray/why3shapes.gz index 07f944bc2787153d565e33d0c63fd9af8c7e0821..7c83e0b7053df48b9377106104479cd4e8f37b84 100644 Binary files a/examples/prover/BacktrackArray/why3shapes.gz and b/examples/prover/BacktrackArray/why3shapes.gz differ diff --git a/examples/prover/Firstorder_formula_impl/why3session.xml b/examples/prover/Firstorder_formula_impl/why3session.xml index 49b1971d0d76b77dfc7b8ecf3c865fcc94ac77d5..fdf03ef6000d63414635bc8a03f16324f35b4550 100644 --- a/examples/prover/Firstorder_formula_impl/why3session.xml +++ b/examples/prover/Firstorder_formula_impl/why3session.xml @@ -85,7 +85,7 @@ - + @@ -115,7 +115,7 @@ - + @@ -289,7 +289,7 @@ - + @@ -388,7 +388,7 @@ - + @@ -502,13 +502,13 @@ - + - + - + @@ -538,13 +538,13 @@ - + - + - + @@ -665,7 +665,7 @@ - + @@ -701,7 +701,7 @@ - + @@ -843,10 +843,10 @@ - + - + @@ -891,7 +891,7 @@ - + @@ -900,7 +900,7 @@ - + @@ -972,10 +972,10 @@ - + - + @@ -1039,16 +1039,16 @@ - + - + - + - + @@ -1069,16 +1069,16 @@ - + - + - + - + @@ -1093,16 +1093,16 @@ - + - + - + - + @@ -1123,16 +1123,16 @@ - + - + - + @@ -1156,13 +1156,13 @@ - + - + - + @@ -1183,16 +1183,16 @@ - + - + - + @@ -1243,7 +1243,7 @@ - + @@ -1349,16 +1349,16 @@ - + - + - + @@ -1391,16 +1391,16 @@ - + - + - + @@ -1503,7 +1503,7 @@ - + @@ -1527,7 +1527,7 @@ - + @@ -1542,13 +1542,13 @@ - + - + - + @@ -1563,19 +1563,19 @@ - + - + - + - + @@ -1584,19 +1584,19 @@ - + - + - + - + @@ -1611,19 +1611,19 @@ - + - + - + - + @@ -1662,10 +1662,10 @@ - + - + @@ -1705,7 +1705,7 @@ - + @@ -1760,7 +1760,7 @@ - + @@ -1775,7 +1775,7 @@ - + @@ -1830,7 +1830,7 @@ - + @@ -1874,13 +1874,36 @@ - + + + + + + + + + + + + + + + + + + + + + + + + - + @@ -1906,40 +1929,48 @@ - + - + + + + + + + + + - + - + - + - + - + - + - + @@ -1963,36 +1994,13 @@ - - - - - - - - - - - - - - - - - - - - - - - - + - + @@ -2013,48 +2021,40 @@ - + - - - - - - - - - + - + - + - + - + - + - + - + @@ -2167,7 +2167,7 @@ - + @@ -2265,7 +2265,7 @@ - + @@ -2277,19 +2277,19 @@ - + - + - + @@ -2297,16 +2297,16 @@ - + - + - + @@ -2314,30 +2314,34 @@ - + - + - + - + - + - + - + - + - + + + + + @@ -2403,7 +2407,7 @@ - + @@ -2415,19 +2419,19 @@ - + - + - + @@ -2435,16 +2439,16 @@ - + - + - + @@ -2452,34 +2456,30 @@ - + - + - + - + - + - + - + - + - - - - - + @@ -2532,13 +2532,13 @@ - + - + - + @@ -2562,7 +2562,7 @@ - + @@ -2574,19 +2574,19 @@ - + - + - + @@ -2643,13 +2643,13 @@ - + - + - + @@ -2673,7 +2673,7 @@ - + @@ -2685,19 +2685,19 @@ - + - + - + diff --git a/examples/prover/Firstorder_formula_impl/why3shapes.gz b/examples/prover/Firstorder_formula_impl/why3shapes.gz index 938b79ca8af3ef484fa7036d2ed5e2b05fde7516..1f4b2ae3082640627919699d98e00725805639f9 100644 Binary files a/examples/prover/Firstorder_formula_impl/why3shapes.gz and b/examples/prover/Firstorder_formula_impl/why3shapes.gz differ diff --git a/examples/prover/Firstorder_formula_list_impl/why3session.xml b/examples/prover/Firstorder_formula_list_impl/why3session.xml index df6114663a9a794dfcc9cf46e033deea40544ba2..14755b8e15c6d78886ed4adf096d26aef06cac22 100644 --- a/examples/prover/Firstorder_formula_list_impl/why3session.xml +++ b/examples/prover/Firstorder_formula_list_impl/why3session.xml @@ -347,7 +347,7 @@ - + diff --git a/examples/prover/Firstorder_formula_list_impl/why3shapes.gz b/examples/prover/Firstorder_formula_list_impl/why3shapes.gz index f3a021e6c2aa19696ecdfa07078e2f7b050f45f4..4e6f601373b98930a181248261d730dc9f8df7cd 100644 Binary files a/examples/prover/Firstorder_formula_list_impl/why3shapes.gz and b/examples/prover/Firstorder_formula_list_impl/why3shapes.gz differ diff --git a/examples/prover/Firstorder_semantics/why3shapes.gz b/examples/prover/Firstorder_semantics/why3shapes.gz index 2f1b0fc905bf40c49ab2f2ce5cadfd365713ee46..76e56f9b15b0d4b1a64dcd7a5206a928fa9508df 100644 Binary files a/examples/prover/Firstorder_semantics/why3shapes.gz and b/examples/prover/Firstorder_semantics/why3shapes.gz differ diff --git a/examples/prover/Firstorder_symbol_impl/why3shapes.gz b/examples/prover/Firstorder_symbol_impl/why3shapes.gz index 651ac268f314c4e6323c17df19d5fe6fa3cf382d..97e765590a0e62f929983d16f069d1f3084b600c 100644 Binary files a/examples/prover/Firstorder_symbol_impl/why3shapes.gz and b/examples/prover/Firstorder_symbol_impl/why3shapes.gz differ diff --git a/examples/prover/Firstorder_tableau_impl/why3session.xml b/examples/prover/Firstorder_tableau_impl/why3session.xml index 1ac95fd67f1f8efcd155dbcffb8d848e61ec0f6d..5e38ad5023c32f8c7ddde9d1b1a036f58fde274b 100644 --- a/examples/prover/Firstorder_tableau_impl/why3session.xml +++ b/examples/prover/Firstorder_tableau_impl/why3session.xml @@ -42,7 +42,7 @@ - + @@ -97,7 +97,7 @@ - + @@ -106,7 +106,7 @@ - + diff --git a/examples/prover/Firstorder_tableau_impl/why3shapes.gz b/examples/prover/Firstorder_tableau_impl/why3shapes.gz index 8736c8185509f2fe1fba3d7ec04173090031177b..cf3a8a010b67841d1b925f1e93b8310b1dde075e 100644 Binary files a/examples/prover/Firstorder_tableau_impl/why3shapes.gz and b/examples/prover/Firstorder_tableau_impl/why3shapes.gz differ diff --git a/examples/prover/Firstorder_term_impl/why3shapes.gz b/examples/prover/Firstorder_term_impl/why3shapes.gz index 065c6fd8875920ab1948a4953fd33e5ba02b6ce7..198c8ee5957fc98a034baf57f4461eec57b9fa9a 100644 Binary files a/examples/prover/Firstorder_term_impl/why3shapes.gz and b/examples/prover/Firstorder_term_impl/why3shapes.gz differ diff --git a/examples/prover/FormulaTransformations/why3session.xml b/examples/prover/FormulaTransformations/why3session.xml index c38d666c2dbcf1a2ee1d1a497065261f5fdcf853..0872178636544844bbac772697efaedffca054bf 100644 --- a/examples/prover/FormulaTransformations/why3session.xml +++ b/examples/prover/FormulaTransformations/why3session.xml @@ -288,7 +288,7 @@ - + @@ -1425,7 +1425,7 @@ - + @@ -1528,7 +1528,7 @@ - + @@ -2229,7 +2229,7 @@ - + diff --git a/examples/prover/FormulaTransformations/why3shapes.gz b/examples/prover/FormulaTransformations/why3shapes.gz index 9225d5cb62dca25505fcecf1a34ecfc18295a6e1..f44491e6f3dfdd67480958ca9867d28ca40ffede 100644 Binary files a/examples/prover/FormulaTransformations/why3shapes.gz and b/examples/prover/FormulaTransformations/why3shapes.gz differ diff --git a/examples/prover/Prover/why3session.xml b/examples/prover/Prover/why3session.xml index 67c5fefead198d7fce0ec740e5b701df89009cd9..5ca4c6782534f1d4cfb60ab5b4a8bfa58bef6831 100644 --- a/examples/prover/Prover/why3session.xml +++ b/examples/prover/Prover/why3session.xml @@ -1980,7 +1980,7 @@ - + @@ -5156,7 +5156,7 @@ - + diff --git a/examples/prover/Prover/why3shapes.gz b/examples/prover/Prover/why3shapes.gz index fe55b6ae1ba3b27f6baa6506d4584c6af35ea9b5..580add4206d8dea1e026094ade0aad34e5fa157e 100644 Binary files a/examples/prover/Prover/why3shapes.gz and b/examples/prover/Prover/why3shapes.gz differ diff --git a/examples/prover/ProverMain/why3shapes.gz b/examples/prover/ProverMain/why3shapes.gz index 882ac36d30b054aa834f023602b812cfacb4bb23..9893193725841a42e062f4b4ffa96767de1777e9 100644 Binary files a/examples/prover/ProverMain/why3shapes.gz and b/examples/prover/ProverMain/why3shapes.gz differ diff --git a/examples/prover/ProverTest/why3shapes.gz b/examples/prover/ProverTest/why3shapes.gz index 022ef2096371963f617ad4442e331767c75c01cc..edeaedff91c6d25abd8906e5ebf36ddbe77b85b6 100644 Binary files a/examples/prover/ProverTest/why3shapes.gz and b/examples/prover/ProverTest/why3shapes.gz differ diff --git a/examples/prover/Unification/why3session.xml b/examples/prover/Unification/why3session.xml index 74b4f81210ccb78285c3cadd4a0c5ad27718b1ba..6fb8138fd4c8c0112548a0af8abcd1c753e169b3 100644 --- a/examples/prover/Unification/why3session.xml +++ b/examples/prover/Unification/why3session.xml @@ -1065,10 +1065,10 @@ - + - + @@ -1110,19 +1110,19 @@ - + - + - + @@ -1171,7 +1171,7 @@ - + @@ -1180,7 +1180,7 @@ - + @@ -1225,7 +1225,7 @@ - + @@ -1255,10 +1255,10 @@ - + - + @@ -1302,19 +1302,19 @@ - + - + - + @@ -1429,13 +1429,13 @@ - + - + - + @@ -1486,7 +1486,7 @@ - + @@ -1495,7 +1495,7 @@ - + @@ -1561,7 +1561,7 @@ - + @@ -1609,13 +1609,13 @@ - + - + - + diff --git a/examples/prover/Unification/why3shapes.gz b/examples/prover/Unification/why3shapes.gz index 21322c85fa8961763eb14f9b47731f3fcc0f7e5a..53648b5a6f476c65e53a3dcdee624a2c536bc7be 100644 Binary files a/examples/prover/Unification/why3shapes.gz and b/examples/prover/Unification/why3shapes.gz differ diff --git a/examples/queens_bv/why3shapes.gz b/examples/queens_bv/why3shapes.gz index 3cfab83922176c7d50b3e089e3bb3ed864ac2384..db3478e0503e0d5033714d82a0275c6dadc9a1b8 100644 Binary files a/examples/queens_bv/why3shapes.gz and b/examples/queens_bv/why3shapes.gz differ diff --git a/examples/quicksort/why3shapes.gz b/examples/quicksort/why3shapes.gz index 52cfcfc2322dcfd741346844273d9643abe29bc4..0a2534696209d394e13692effcf15cf44dccf42d 100644 Binary files a/examples/quicksort/why3shapes.gz and b/examples/quicksort/why3shapes.gz differ diff --git a/examples/random_access_list/why3shapes.gz b/examples/random_access_list/why3shapes.gz index ba811f8fe4d5680d96cfd9ed8f99df995c0c0735..ebfe7eb30bd8f778dcc0a36a38c7267f896e25eb 100644 Binary files a/examples/random_access_list/why3shapes.gz and b/examples/random_access_list/why3shapes.gz differ diff --git a/examples/register_allocation/why3shapes.gz b/examples/register_allocation/why3shapes.gz index 859946e923dbf30773b3bd1c248bb336ee73a111..509e547c454a809e904b110031ca87f4f4b08791 100644 Binary files a/examples/register_allocation/why3shapes.gz and b/examples/register_allocation/why3shapes.gz differ diff --git a/examples/relabel/why3session.xml b/examples/relabel/why3session.xml index 1d8dec74fd548b9615bbcd847552269be4d9680e..8860d34a8faa83497dbccf23a1886a856e40a2ca 100644 --- a/examples/relabel/why3session.xml +++ b/examples/relabel/why3session.xml @@ -12,7 +12,7 @@ - + diff --git a/examples/relabel/why3shapes.gz b/examples/relabel/why3shapes.gz index c6852b8ccae627f37a359f5d45e0a4a12cd02ae9..6fca4c9b50c31a82878e1c20bc1914398298aff7 100644 Binary files a/examples/relabel/why3shapes.gz and b/examples/relabel/why3shapes.gz differ diff --git a/examples/remove_duplicate/why3session.xml b/examples/remove_duplicate/why3session.xml index 7f9b6cb71216d986ef486f8b9ef5bdb7c41ec8b7..20fdee903e18f5f84859264d9c7b3083ff099459 100644 --- a/examples/remove_duplicate/why3session.xml +++ b/examples/remove_duplicate/why3session.xml @@ -30,7 +30,7 @@ - + diff --git a/examples/remove_duplicate/why3shapes.gz b/examples/remove_duplicate/why3shapes.gz index 8d603152f2ddcf23752e669a06593b049b3fd1db..d6a3a1eb7bdc8a785403cc8b6d4b1a00ca4b9ef6 100644 Binary files a/examples/remove_duplicate/why3shapes.gz and b/examples/remove_duplicate/why3shapes.gz differ diff --git a/examples/remove_duplicate_hash/why3shapes.gz b/examples/remove_duplicate_hash/why3shapes.gz index 73a0da6adf3c7dd2c68099bb77c88c5793096235..fc667e0c8f80fb78a5c6e353d110b4382b39e5ba 100644 Binary files a/examples/remove_duplicate_hash/why3shapes.gz and b/examples/remove_duplicate_hash/why3shapes.gz differ diff --git a/examples/resizable_array/why3shapes.gz b/examples/resizable_array/why3shapes.gz index 593a1ac5f0e070107b33eb195e5ed9a857f07d28..5c7822b2cf306337f498156d8bf24805efabe37b 100644 Binary files a/examples/resizable_array/why3shapes.gz and b/examples/resizable_array/why3shapes.gz differ diff --git a/examples/rightmostbittrick/why3shapes.gz b/examples/rightmostbittrick/why3shapes.gz index a19a28b81e86d28cd124514173a55c65912c0208..b4c1cf6089e0c7ed3270103d0c6e4dee29c5cdef 100644 Binary files a/examples/rightmostbittrick/why3shapes.gz and b/examples/rightmostbittrick/why3shapes.gz differ diff --git a/examples/ropes/why3shapes.gz b/examples/ropes/why3shapes.gz index f3514018154ac6206236d870bb47521801cc57c9..e15bea38b2029867a3607b363d62e6fe6320a503 100644 Binary files a/examples/ropes/why3shapes.gz and b/examples/ropes/why3shapes.gz differ diff --git a/examples/schorr_waite/why3session.xml b/examples/schorr_waite/why3session.xml index 6ec7fb6251bd72caae2ddb1d275f0f42039e8a99..51a38cf194ae0951e0333b7700851f7d4c0a3b9d 100644 --- a/examples/schorr_waite/why3session.xml +++ b/examples/schorr_waite/why3session.xml @@ -62,13 +62,13 @@ - + - + @@ -86,7 +86,7 @@ - + @@ -171,13 +171,13 @@ - - + - + + @@ -185,11 +185,11 @@ - + + - - + @@ -397,13 +397,13 @@ - + - + - + @@ -415,7 +415,7 @@ - + @@ -424,10 +424,10 @@ - + - + @@ -487,13 +487,13 @@ - + - + - + @@ -505,7 +505,7 @@ - + @@ -514,7 +514,7 @@ - + diff --git a/examples/schorr_waite/why3shapes.gz b/examples/schorr_waite/why3shapes.gz index de5dba6463cc1244b25f25a109fd84e12fab7499..a25b41562a978fa5613a4cbe1e651e215ee8d733 100644 Binary files a/examples/schorr_waite/why3shapes.gz and b/examples/schorr_waite/why3shapes.gz differ diff --git a/examples/schorr_waite_via_recursion/why3session.xml b/examples/schorr_waite_via_recursion/why3session.xml index 682b477ef4527f7b991a3a181d4f1380df4cee32..c39fc21e1c8bc037dad1df4fc735646c6861cf25 100644 --- a/examples/schorr_waite_via_recursion/why3session.xml +++ b/examples/schorr_waite_via_recursion/why3session.xml @@ -135,7 +135,7 @@ - + @@ -147,7 +147,7 @@ - + @@ -294,7 +294,7 @@ - + diff --git a/examples/schorr_waite_via_recursion/why3shapes.gz b/examples/schorr_waite_via_recursion/why3shapes.gz index 025203d35052542a4f35a31f514380efab4e77cc..648be5d286158438e727e32b3d13731437907434 100644 Binary files a/examples/schorr_waite_via_recursion/why3shapes.gz and b/examples/schorr_waite_via_recursion/why3shapes.gz differ diff --git a/examples/selection_sort/why3shapes.gz b/examples/selection_sort/why3shapes.gz index 805961e01b7e6caf4103db78ce03dc8180d91955..60cd8fe1ad00a0de9424425b0f46607984101594 100644 Binary files a/examples/selection_sort/why3shapes.gz and b/examples/selection_sort/why3shapes.gz differ diff --git a/examples/sf/why3shapes.gz b/examples/sf/why3shapes.gz index 8b70a927ce5073c9908ffc8d5c61ed6b5e719898..174f376e87ec917565a899f3b0341d31a302eb76 100644 Binary files a/examples/sf/why3shapes.gz and b/examples/sf/why3shapes.gz differ diff --git a/examples/sieve/why3shapes.gz b/examples/sieve/why3shapes.gz index f3efc45693b209bacfb931407fe593eb98d486f7..af1e0aa47d430f3893708ad3ec887aca1091c93a 100644 Binary files a/examples/sieve/why3shapes.gz and b/examples/sieve/why3shapes.gz differ diff --git a/examples/simple_queue/why3shapes.gz b/examples/simple_queue/why3shapes.gz index b7caefda01c689e89545368f74a21341481ba6e3..d906611ed03fd200b0d00300f79ee34ef7b1bb8c 100644 Binary files a/examples/simple_queue/why3shapes.gz and b/examples/simple_queue/why3shapes.gz differ diff --git a/examples/skew_heaps/why3shapes.gz b/examples/skew_heaps/why3shapes.gz index 7d34e5cc69992eed2e40c6b00efd2494dac8212e..46f496342ddfddae36ece6eda262c884ddf49ca3 100644 Binary files a/examples/skew_heaps/why3shapes.gz and b/examples/skew_heaps/why3shapes.gz differ diff --git a/examples/snapshotable_trees/why3shapes.gz b/examples/snapshotable_trees/why3shapes.gz index 0f36449d396e5ce9a93bd0094d54d3428de9475b..7a005ac8b9e977f93976afad87c84712e1d0ea56 100644 Binary files a/examples/snapshotable_trees/why3shapes.gz and b/examples/snapshotable_trees/why3shapes.gz differ diff --git a/examples/stdlib/array/why3session.xml b/examples/stdlib/array/why3session.xml index ffe2f50680464b239dc95519c092b43d19a77b95..b420f1e766b0689f186b6599646183f9a71e7271 100644 --- a/examples/stdlib/array/why3session.xml +++ b/examples/stdlib/array/why3session.xml @@ -188,7 +188,7 @@ - + diff --git a/examples/stdlib/array/why3shapes.gz b/examples/stdlib/array/why3shapes.gz index cc5d1393e4228bacb65f934aa31d8f75f03bb9c5..4df411db58d3f00a6815d5f0c9341e94a2ca0666 100644 Binary files a/examples/stdlib/array/why3shapes.gz and b/examples/stdlib/array/why3shapes.gz differ diff --git a/examples/sudoku/why3shapes.gz b/examples/sudoku/why3shapes.gz index 1c90490f6081650dd841fc79bc6d3d9d7b1c9e52..04e5771940995664b77519b9eab19cc521615034 100644 Binary files a/examples/sudoku/why3shapes.gz and b/examples/sudoku/why3shapes.gz differ diff --git a/examples/sumrange/why3session.xml b/examples/sumrange/why3session.xml index 7f83a9080e86bc014b0b2ef50d599556bbdf654c..fe2d1709f175c2c15bb54601cc63f3bb7b750b6f 100644 --- a/examples/sumrange/why3session.xml +++ b/examples/sumrange/why3session.xml @@ -182,20 +182,20 @@ - + - + - + - + @@ -291,10 +291,10 @@ - + - + diff --git a/examples/sumrange/why3shapes.gz b/examples/sumrange/why3shapes.gz index 179179605f34de6eb6850e67e6edab48d051930f..1d44cb967ba19c8aea49d666003aa232296c658f 100644 Binary files a/examples/sumrange/why3shapes.gz and b/examples/sumrange/why3shapes.gz differ diff --git a/examples/swap/why3shapes.gz b/examples/swap/why3shapes.gz index 7700ef8e91443a32f384dcf1db44bc59c8af2081..f33d5383bc6413f2618cf42e87cb7db7376fed1a 100644 Binary files a/examples/swap/why3shapes.gz and b/examples/swap/why3shapes.gz differ diff --git a/examples/topological_sorting/why3shapes.gz b/examples/topological_sorting/why3shapes.gz index 752bcb159e83cdd614fd232a4e33944752f7ce07..2c38ac25f467304ff2d9d2b8d5fc3bdafce0c860 100644 Binary files a/examples/topological_sorting/why3shapes.gz and b/examples/topological_sorting/why3shapes.gz differ diff --git a/examples/tortoise_and_hare/why3shapes.gz b/examples/tortoise_and_hare/why3shapes.gz index d0c1884a3ad63159210449fd59bd670db03cfe02..4588cd7103014e788565c0b643780761d22410f3 100644 Binary files a/examples/tortoise_and_hare/why3shapes.gz and b/examples/tortoise_and_hare/why3shapes.gz differ diff --git a/examples/tower_of_hanoi/why3session.xml b/examples/tower_of_hanoi/why3session.xml index ec925649dce2cd66094ca506a992b0eb8c0a1192..a1d77cb2dbe8a9f5268e42fa3c740260aa65a14f 100644 --- a/examples/tower_of_hanoi/why3session.xml +++ b/examples/tower_of_hanoi/why3session.xml @@ -75,7 +75,7 @@ - + @@ -182,7 +182,7 @@ - + diff --git a/examples/tower_of_hanoi/why3shapes.gz b/examples/tower_of_hanoi/why3shapes.gz index 049aa7ed70bc50e1956209571130c9ef7ab2abc6..e753b843ea9663c9a6dedac7d03cc047b49f76bf 100644 Binary files a/examples/tower_of_hanoi/why3shapes.gz and b/examples/tower_of_hanoi/why3shapes.gz differ diff --git a/examples/tree_height/why3shapes.gz b/examples/tree_height/why3shapes.gz index d5641df7a4942451b29a3cac86e5d9062248e45e..07ed4649ddc1ef06d392001631f5744876fb38b8 100644 Binary files a/examples/tree_height/why3shapes.gz and b/examples/tree_height/why3shapes.gz differ diff --git a/examples/tree_of_array/why3shapes.gz b/examples/tree_of_array/why3shapes.gz index 5856fcb03a342b072312f9ebf3a42a5de515b6f6..98af3b2e8864f1af4b82e0cdc42a4f08cdd9f41d 100644 Binary files a/examples/tree_of_array/why3shapes.gz and b/examples/tree_of_array/why3shapes.gz differ diff --git a/examples/unraveling_a_card_trick/why3shapes.gz b/examples/unraveling_a_card_trick/why3shapes.gz index dcec540c8acf8bdf973383cd8feacaccf2c601b1..4887e4edc7dc6fa53fe64a41caa49f756f5b8c3e 100644 Binary files a/examples/unraveling_a_card_trick/why3shapes.gz and b/examples/unraveling_a_card_trick/why3shapes.gz differ diff --git a/examples/vacid_0_binary_heaps/proofs/why3shapes.gz b/examples/vacid_0_binary_heaps/proofs/why3shapes.gz index bd8c008f39b6324635d87550bb057619a5393279..f04ecbb17bcea5c0d0c33e54a4ffeb30b045638b 100644 Binary files a/examples/vacid_0_binary_heaps/proofs/why3shapes.gz and b/examples/vacid_0_binary_heaps/proofs/why3shapes.gz differ diff --git a/examples/vacid_0_build_maze/why3shapes.gz b/examples/vacid_0_build_maze/why3shapes.gz index 4afb5bdf73336d540f47bee369dfde7bda7ab2eb..9d2ea3c023812df56d61abf2b0d1cd318011bb09 100644 Binary files a/examples/vacid_0_build_maze/why3shapes.gz and b/examples/vacid_0_build_maze/why3shapes.gz differ diff --git a/examples/vacid_0_red_black_trees/why3shapes.gz b/examples/vacid_0_red_black_trees/why3shapes.gz index 94ba810619915869ed950fe53fed04ad77d147df..5e40c094f22ad012aaff40e357107e8102cedcb9 100644 Binary files a/examples/vacid_0_red_black_trees/why3shapes.gz and b/examples/vacid_0_red_black_trees/why3shapes.gz differ diff --git a/examples/vacid_0_sparse_array/why3shapes.gz b/examples/vacid_0_sparse_array/why3shapes.gz index 68aa4aef12654466b2c971319d6c2294d1102424..8b119ecf9654aa098be619ea710237ce657a4b2b 100644 Binary files a/examples/vacid_0_sparse_array/why3shapes.gz and b/examples/vacid_0_sparse_array/why3shapes.gz differ diff --git a/examples/verifythis_2015_dancing_links/why3shapes.gz b/examples/verifythis_2015_dancing_links/why3shapes.gz index 6950633fe32aa5961e81fbd2b8bd475512c44b95..09aad95f1b41f3680b1b55049bf755e7f7941772 100644 Binary files a/examples/verifythis_2015_dancing_links/why3shapes.gz and b/examples/verifythis_2015_dancing_links/why3shapes.gz differ diff --git a/examples/verifythis_2015_parallel_gcd/why3shapes.gz b/examples/verifythis_2015_parallel_gcd/why3shapes.gz index 07d772e82e20210ca96b12caa93f64ce93e0e47a..698dc0af9a3b9d8ef245dd23b7f12a6e89046423 100644 Binary files a/examples/verifythis_2015_parallel_gcd/why3shapes.gz and b/examples/verifythis_2015_parallel_gcd/why3shapes.gz differ diff --git a/examples/verifythis_2015_relaxed_prefix/why3shapes.gz b/examples/verifythis_2015_relaxed_prefix/why3shapes.gz index 042a586c3e42accfbdd76aa86a1b02e83e6fea1b..e37cefba9adb8b51d23e8b42e79475ac8a441062 100644 Binary files a/examples/verifythis_2015_relaxed_prefix/why3shapes.gz and b/examples/verifythis_2015_relaxed_prefix/why3shapes.gz differ diff --git a/examples/verifythis_2016_matrix_multiplication/matrices_ring_simp/why3shapes.gz b/examples/verifythis_2016_matrix_multiplication/matrices_ring_simp/why3shapes.gz index 446c005fcb7df76e8693661fe3733700d33fa0b2..8cbf941638ef6a55ea7773e9b7404fd056aaf222 100644 Binary files a/examples/verifythis_2016_matrix_multiplication/matrices_ring_simp/why3shapes.gz and b/examples/verifythis_2016_matrix_multiplication/matrices_ring_simp/why3shapes.gz differ diff --git a/examples/verifythis_2016_matrix_multiplication/naive/why3session.xml b/examples/verifythis_2016_matrix_multiplication/naive/why3session.xml index ea65c07965a57f530d953b57cd54cb472af535c1..acea6f5f66ada4b2cb03e0563fcb725dd6a4f83f 100644 --- a/examples/verifythis_2016_matrix_multiplication/naive/why3session.xml +++ b/examples/verifythis_2016_matrix_multiplication/naive/why3session.xml @@ -17,13 +17,13 @@ - + - + diff --git a/examples/verifythis_2016_matrix_multiplication/naive/why3shapes.gz b/examples/verifythis_2016_matrix_multiplication/naive/why3shapes.gz index 9a2875aad12dbb7f3e2c7748f4db8e449f85ede8..662ad0e9dd07505035de8a412bae1a8aacce768c 100644 Binary files a/examples/verifythis_2016_matrix_multiplication/naive/why3shapes.gz and b/examples/verifythis_2016_matrix_multiplication/naive/why3shapes.gz differ diff --git a/examples/verifythis_2016_tree_traversal/why3session.xml b/examples/verifythis_2016_tree_traversal/why3session.xml index b64e48e115623ceafe20c56fbfd9855dc348b75f..76b2e501a98ff234766446059ae5d14eb6145fb3 100644 --- a/examples/verifythis_2016_tree_traversal/why3session.xml +++ b/examples/verifythis_2016_tree_traversal/why3session.xml @@ -191,7 +191,7 @@ - + diff --git a/examples/verifythis_2016_tree_traversal/why3shapes.gz b/examples/verifythis_2016_tree_traversal/why3shapes.gz index 91299536654ca1d64f192069d6f4102e97ef8df1..fbda93de07886d25461812ab899c5476c63f283f 100644 Binary files a/examples/verifythis_2016_tree_traversal/why3shapes.gz and b/examples/verifythis_2016_tree_traversal/why3shapes.gz differ diff --git a/examples/verifythis_2017_maximum_sum_submatrix/why3shapes.gz b/examples/verifythis_2017_maximum_sum_submatrix/why3shapes.gz index fed14fcfd9fbcf3a30b04140ae76515fe30364e5..f6cf032a39f1de32b4af88a74367e586494c3973 100644 Binary files a/examples/verifythis_2017_maximum_sum_submatrix/why3shapes.gz and b/examples/verifythis_2017_maximum_sum_submatrix/why3shapes.gz differ diff --git a/examples/verifythis_2017_odd_even_sort_rearranging/why3session.xml b/examples/verifythis_2017_odd_even_sort_rearranging/why3session.xml index 9333f75696bee20150d60a99fd026ab47d516155..c7444ee66921601ce84c3ff743e3966ad8f9e5a0 100644 --- a/examples/verifythis_2017_odd_even_sort_rearranging/why3session.xml +++ b/examples/verifythis_2017_odd_even_sort_rearranging/why3session.xml @@ -219,7 +219,7 @@ - + diff --git a/examples/verifythis_2017_odd_even_sort_rearranging/why3shapes.gz b/examples/verifythis_2017_odd_even_sort_rearranging/why3shapes.gz index 58f0dc7e4d5f89150422c303e8296d8630fc38d6..06f337423fb69bc7fe48fae557e7a13441c64d53 100644 Binary files a/examples/verifythis_2017_odd_even_sort_rearranging/why3shapes.gz and b/examples/verifythis_2017_odd_even_sort_rearranging/why3shapes.gz differ diff --git a/examples/verifythis_2017_odd_even_transposition_sort/why3shapes.gz b/examples/verifythis_2017_odd_even_transposition_sort/why3shapes.gz index ff605d02fac822e4b237b49d282fb6f64501e227..d4d6955aa63de899fd551acd782cfd8b96709f59 100644 Binary files a/examples/verifythis_2017_odd_even_transposition_sort/why3shapes.gz and b/examples/verifythis_2017_odd_even_transposition_sort/why3shapes.gz differ diff --git a/examples/verifythis_2017_pair_insertion_sort/why3shapes.gz b/examples/verifythis_2017_pair_insertion_sort/why3shapes.gz index bc04306731a2ca7b8d64685cf4d3273774516e03..6baf731698b6d2fe4ee2b3c73b6925abb12f71cb 100644 Binary files a/examples/verifythis_2017_pair_insertion_sort/why3shapes.gz and b/examples/verifythis_2017_pair_insertion_sort/why3shapes.gz differ diff --git a/examples/verifythis_2017_tree_buffer/why3shapes.gz b/examples/verifythis_2017_tree_buffer/why3shapes.gz index aefd7f488c7572ed29ed2ff0d5422e580cec0ec6..466b83acd816c2de8faed3e3670c590f640d22cd 100644 Binary files a/examples/verifythis_2017_tree_buffer/why3shapes.gz and b/examples/verifythis_2017_tree_buffer/why3shapes.gz differ diff --git a/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml b/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml index b2de094d565c7a37b6b5b8d06c49c982d6346b90..57aad2fd0258c392d0af3cbd18c94f2c846a8f93 100644 --- a/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml +++ b/examples/verifythis_2018_array_based_queuing_lock_1/why3session.xml @@ -227,7 +227,7 @@ - + @@ -308,7 +308,7 @@ - + @@ -455,13 +455,13 @@ - + - + diff --git a/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz b/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz index c07f4e35f4a714f127df7d39750a97c95e43a3dc..08360b1822019887b451488015a4808f8d133b11 100644 Binary files a/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz and b/examples/verifythis_2018_array_based_queuing_lock_1/why3shapes.gz differ diff --git a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml index da0f799af970d6ec0d0ae794e67abc4adaa33ecb..c2e1fc1ca6b6c2f84aef2ef5723d57481a7e70a1 100644 --- a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml +++ b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3session.xml @@ -627,7 +627,7 @@ - + diff --git a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz index 300331cf5371a0e736c34b2df7b8ca9d8120d2ce..3dfbe82cc7460a93e89adb0a9031dec5bc8e4b2e 100644 Binary files a/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz and b/examples/verifythis_2018_le_rouge_et_le_noir_1/why3shapes.gz differ diff --git a/examples/verifythis_2018_le_rouge_et_le_noir_2/why3shapes.gz b/examples/verifythis_2018_le_rouge_et_le_noir_2/why3shapes.gz index ad8eccaaaa2b283165801c101142422643296fd9..2c5fc3b4ac19b2da54dfece912a6ac61b111d1e3 100644 Binary files a/examples/verifythis_2018_le_rouge_et_le_noir_2/why3shapes.gz and b/examples/verifythis_2018_le_rouge_et_le_noir_2/why3shapes.gz differ diff --git a/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz b/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz index 1f1525f0bd8c61dce51cb3af1977c8afdcec43e1..23d3aaf99e6b28e3f557056c381b730eb874c6e5 100644 Binary files a/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz and b/examples/verifythis_2018_mind_the_gap_1/why3shapes.gz differ diff --git a/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz b/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz index a785d104cd3d3a08e33b37faa2867d146a055ca9..869a32710d97471bffcc2e15934ab57e19442494 100644 Binary files a/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz and b/examples/verifythis_2018_mind_the_gap_2/why3shapes.gz differ diff --git a/examples/verifythis_PrefixSumRec/why3shapes.gz b/examples/verifythis_PrefixSumRec/why3shapes.gz index fccd5b1d63ce37c64c9401157b9a856f267a174f..7bd1fcd8f9b47cddc5d25d72d206b3db65f0c550 100644 Binary files a/examples/verifythis_PrefixSumRec/why3shapes.gz and b/examples/verifythis_PrefixSumRec/why3shapes.gz differ diff --git a/examples/verifythis_fm2012_LRS/why3session.xml b/examples/verifythis_fm2012_LRS/why3session.xml index f819db2282a2aa77484879aa73a737795187a8dc..4f81aa8af899c9f44c1231e42fe782533403b0b2 100644 --- a/examples/verifythis_fm2012_LRS/why3session.xml +++ b/examples/verifythis_fm2012_LRS/why3session.xml @@ -28,7 +28,7 @@ - + diff --git a/examples/verifythis_fm2012_LRS/why3shapes.gz b/examples/verifythis_fm2012_LRS/why3shapes.gz index bb8b2b77e18f92384bde5cc69178ad061f1ca6bf..8a7215f1ecc6fca86475d2457af5424a6e86fbe8 100644 Binary files a/examples/verifythis_fm2012_LRS/why3shapes.gz and b/examples/verifythis_fm2012_LRS/why3shapes.gz differ diff --git a/examples/verifythis_fm2012_treedel/why3session.xml b/examples/verifythis_fm2012_treedel/why3session.xml index 54874172b3d60cc4807a78d0926bccc8a42ad3ec..c8589d874bac108a30c1239eec2e56594a4c06ad 100644 --- a/examples/verifythis_fm2012_treedel/why3session.xml +++ b/examples/verifythis_fm2012_treedel/why3session.xml @@ -185,7 +185,7 @@ - + @@ -209,7 +209,7 @@ - + @@ -236,7 +236,7 @@ - + diff --git a/examples/verifythis_fm2012_treedel/why3shapes.gz b/examples/verifythis_fm2012_treedel/why3shapes.gz index dac3583eb60730bc4ac11db28b0b46340ce29592..ad3819b5dd3d711147caa47a2e7463753d46b51b 100644 Binary files a/examples/verifythis_fm2012_treedel/why3shapes.gz and b/examples/verifythis_fm2012_treedel/why3shapes.gz differ diff --git a/examples/vstte10_aqueue/why3shapes.gz b/examples/vstte10_aqueue/why3shapes.gz index 59cdab845fb20b2cad78166dcdcf4d8ccfaaad0f..d7aa9960f8ad9ff371b9661a9103b4b4a46812e5 100644 Binary files a/examples/vstte10_aqueue/why3shapes.gz and b/examples/vstte10_aqueue/why3shapes.gz differ diff --git a/examples/vstte10_inverting/why3shapes.gz b/examples/vstte10_inverting/why3shapes.gz index b5149280e9c204d7cba967e0fb9ee345dbd81b31..a24e97f8fd4eca0db3afc4718937dbf38c1162d6 100644 Binary files a/examples/vstte10_inverting/why3shapes.gz and b/examples/vstte10_inverting/why3shapes.gz differ diff --git a/examples/vstte10_max_sum/why3shapes.gz b/examples/vstte10_max_sum/why3shapes.gz index 550537d73d5a3f345efb2f92e38c5ef650d258ae..b21abe6abc6fae602c0f17411e7b896c9e8fc523 100644 Binary files a/examples/vstte10_max_sum/why3shapes.gz and b/examples/vstte10_max_sum/why3shapes.gz differ diff --git a/examples/vstte10_queens/why3shapes.gz b/examples/vstte10_queens/why3shapes.gz index 1427372e49876e79da6c20a8e8d7b555d16e53ef..d41fedf8377816efd078ee2cd5f9e42a1df3b96c 100644 Binary files a/examples/vstte10_queens/why3shapes.gz and b/examples/vstte10_queens/why3shapes.gz differ diff --git a/examples/vstte10_search_list/why3shapes.gz b/examples/vstte10_search_list/why3shapes.gz index d14db283fdfdd538e65d43bf2f3d3fd02411bf89..a7a9894429b30840becae2606783d721526aa8d0 100644 Binary files a/examples/vstte10_search_list/why3shapes.gz and b/examples/vstte10_search_list/why3shapes.gz differ diff --git a/examples/vstte12_bfs/why3shapes.gz b/examples/vstte12_bfs/why3shapes.gz index e527853c720d47628756151f91b2708ec0d264b3..c47a8f10669f874d82ed041a1988cb8afca6bb23 100644 Binary files a/examples/vstte12_bfs/why3shapes.gz and b/examples/vstte12_bfs/why3shapes.gz differ diff --git a/examples/vstte12_ring_buffer/why3session.xml b/examples/vstte12_ring_buffer/why3session.xml index d8cc10aeaaa99ce9a598f7b7cd83b5c249a876a3..f5987c2d630a9889ca2c5861389e605acdf1b91c 100644 --- a/examples/vstte12_ring_buffer/why3session.xml +++ b/examples/vstte12_ring_buffer/why3session.xml @@ -146,7 +146,7 @@ - + diff --git a/examples/vstte12_ring_buffer/why3shapes.gz b/examples/vstte12_ring_buffer/why3shapes.gz index cb33e5024593ca8ef260ee3d6b42d5b9c60bee05..0fe69534781b5f251707e7d497cfd9f8f673f0be 100644 Binary files a/examples/vstte12_ring_buffer/why3shapes.gz and b/examples/vstte12_ring_buffer/why3shapes.gz differ diff --git a/examples/vstte12_two_way_sort/why3shapes.gz b/examples/vstte12_two_way_sort/why3shapes.gz index d4a77cb16cf4f3174698028d3c3c2c018e9b64e4..5f62a822792a0ac63970a237880068dfbafc6e1a 100644 Binary files a/examples/vstte12_two_way_sort/why3shapes.gz and b/examples/vstte12_two_way_sort/why3shapes.gz differ diff --git a/examples/warshall_algorithm/why3shapes.gz b/examples/warshall_algorithm/why3shapes.gz index 4458c899e7bbe434c28f6930968c405a87351765..05506b36d083b5da88ae0ecf1beb194b4a85faa6 100644 Binary files a/examples/warshall_algorithm/why3shapes.gz and b/examples/warshall_algorithm/why3shapes.gz differ diff --git a/examples/white_and_black_balls/why3shapes.gz b/examples/white_and_black_balls/why3shapes.gz index b4aa54318b29c861b1a687da4b09a4846ecf7ec0..bd172b022fafe1d73c6c49359e9ce8e21fe738bf 100644 Binary files a/examples/white_and_black_balls/why3shapes.gz and b/examples/white_and_black_balls/why3shapes.gz differ diff --git a/examples/zeros/why3shapes.gz b/examples/zeros/why3shapes.gz index 20f33b0915c03c374503c8d04cca85ecb4088a12..f6b9fb5930aafd70b5fbeb625cff227f2bee6e66 100644 Binary files a/examples/zeros/why3shapes.gz and b/examples/zeros/why3shapes.gz differ