diff --git a/creusot/tests/should_succeed/100doors/why3session.xml b/creusot/tests/should_succeed/100doors/why3session.xml index 6688971c2..60fe04907 100644 --- a/creusot/tests/should_succeed/100doors/why3session.xml +++ b/creusot/tests/should_succeed/100doors/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/100doors/why3shapes.gz b/creusot/tests/should_succeed/100doors/why3shapes.gz index 1b88a2a40..ba4a74b36 100644 Binary files a/creusot/tests/should_succeed/100doors/why3shapes.gz and b/creusot/tests/should_succeed/100doors/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/all_zero/why3session.xml b/creusot/tests/should_succeed/all_zero/why3session.xml index d2ba41cbc..d01bdef72 100644 --- a/creusot/tests/should_succeed/all_zero/why3session.xml +++ b/creusot/tests/should_succeed/all_zero/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bdd/why3session.xml b/creusot/tests/should_succeed/bdd/why3session.xml index 73f9d9820..a3650a77f 100644 --- a/creusot/tests/should_succeed/bdd/why3session.xml +++ b/creusot/tests/should_succeed/bdd/why3session.xml @@ -2,9 +2,7 @@ - - @@ -17,7 +15,7 @@ - + @@ -27,7 +25,7 @@ - + @@ -42,12 +40,12 @@ - + - + @@ -537,7 +535,7 @@ - + @@ -551,13 +549,13 @@ - + - + - + @@ -575,10 +573,10 @@ - + - + @@ -589,7 +587,7 @@ - + @@ -666,10 +664,10 @@ - + - + @@ -681,10 +679,10 @@ - + - + @@ -696,7 +694,7 @@ - + @@ -704,7 +702,7 @@ - + @@ -716,7 +714,7 @@ - + @@ -742,7 +740,7 @@ - + @@ -754,22 +752,22 @@ - + - + - + - + @@ -779,12 +777,12 @@ - + - + @@ -794,7 +792,7 @@ - + diff --git a/creusot/tests/should_succeed/binary_search/why3session.xml b/creusot/tests/should_succeed/binary_search/why3session.xml index a8a0859d3..7ab8b6421 100644 --- a/creusot/tests/should_succeed/binary_search/why3session.xml +++ b/creusot/tests/should_succeed/binary_search/why3session.xml @@ -2,95 +2,95 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/bug/173/why3session.xml b/creusot/tests/should_succeed/bug/173/why3session.xml index 59a9756fe..e8330ec9e 100644 --- a/creusot/tests/should_succeed/bug/173/why3session.xml +++ b/creusot/tests/should_succeed/bug/173/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/206/why3session.xml b/creusot/tests/should_succeed/bug/206/why3session.xml index ed9cac8dd..ffa6864da 100644 --- a/creusot/tests/should_succeed/bug/206/why3session.xml +++ b/creusot/tests/should_succeed/bug/206/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/bug/206/why3shapes.gz b/creusot/tests/should_succeed/bug/206/why3shapes.gz index 8f5cb41b3..6bd50039a 100644 Binary files a/creusot/tests/should_succeed/bug/206/why3shapes.gz and b/creusot/tests/should_succeed/bug/206/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/bug/217/why3session.xml b/creusot/tests/should_succeed/bug/217/why3session.xml index 84cd5ba6f..626a388c9 100644 --- a/creusot/tests/should_succeed/bug/217/why3session.xml +++ b/creusot/tests/should_succeed/bug/217/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/217/why3shapes.gz b/creusot/tests/should_succeed/bug/217/why3shapes.gz index e3e9d69c2..9ade06dda 100644 Binary files a/creusot/tests/should_succeed/bug/217/why3shapes.gz and b/creusot/tests/should_succeed/bug/217/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/bug/235/why3session.xml b/creusot/tests/should_succeed/bug/235/why3session.xml index ce6959ec8..b9ec902f1 100644 --- a/creusot/tests/should_succeed/bug/235/why3session.xml +++ b/creusot/tests/should_succeed/bug/235/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/273/why3session.xml b/creusot/tests/should_succeed/bug/273/why3session.xml index 0ec6d430e..58a649c88 100644 --- a/creusot/tests/should_succeed/bug/273/why3session.xml +++ b/creusot/tests/should_succeed/bug/273/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/395/why3session.xml b/creusot/tests/should_succeed/bug/395/why3session.xml index 3ee736c29..947eb7e8f 100644 --- a/creusot/tests/should_succeed/bug/395/why3session.xml +++ b/creusot/tests/should_succeed/bug/395/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/463/why3session.xml b/creusot/tests/should_succeed/bug/463/why3session.xml index be56cb995..5cab4bbae 100644 --- a/creusot/tests/should_succeed/bug/463/why3session.xml +++ b/creusot/tests/should_succeed/bug/463/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/bug/545/why3session.xml b/creusot/tests/should_succeed/bug/545/why3session.xml index cbf628359..3e92c6a07 100644 --- a/creusot/tests/should_succeed/bug/545/why3session.xml +++ b/creusot/tests/should_succeed/bug/545/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/552/why3session.xml b/creusot/tests/should_succeed/bug/552/why3session.xml index 5afa7e31c..bba975ab4 100644 --- a/creusot/tests/should_succeed/bug/552/why3session.xml +++ b/creusot/tests/should_succeed/bug/552/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/bug/682/why3session.xml b/creusot/tests/should_succeed/bug/682/why3session.xml index 112c4a975..243670953 100644 --- a/creusot/tests/should_succeed/bug/682/why3session.xml +++ b/creusot/tests/should_succeed/bug/682/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/bug/874/why3session.xml b/creusot/tests/should_succeed/bug/874/why3session.xml index 507eab598..d01aeea11 100644 --- a/creusot/tests/should_succeed/bug/874/why3session.xml +++ b/creusot/tests/should_succeed/bug/874/why3session.xml @@ -2,33 +2,37 @@ - - + + - + - + - + - + - + - + - + + + + + diff --git a/creusot/tests/should_succeed/bug/874/why3shapes.gz b/creusot/tests/should_succeed/bug/874/why3shapes.gz index 4d962f2ae..f409e6a0a 100644 Binary files a/creusot/tests/should_succeed/bug/874/why3shapes.gz and b/creusot/tests/should_succeed/bug/874/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/bug/eq_panic/why3session.xml b/creusot/tests/should_succeed/bug/eq_panic/why3session.xml index 907d1302e..b36230b2b 100644 --- a/creusot/tests/should_succeed/bug/eq_panic/why3session.xml +++ b/creusot/tests/should_succeed/bug/eq_panic/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml b/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml index 00ca672f4..51a7a8ca2 100644 --- a/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml +++ b/creusot/tests/should_succeed/bug/minus_assoc/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/pure_neq/why3session.xml b/creusot/tests/should_succeed/bug/pure_neq/why3session.xml index c3d6179cd..58a8feb93 100644 --- a/creusot/tests/should_succeed/bug/pure_neq/why3session.xml +++ b/creusot/tests/should_succeed/bug/pure_neq/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/two_phase/why3session.xml b/creusot/tests/should_succeed/bug/two_phase/why3session.xml index 21d4f35d6..310ef881c 100644 --- a/creusot/tests/should_succeed/bug/two_phase/why3session.xml +++ b/creusot/tests/should_succeed/bug/two_phase/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz b/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz index 78e58f241..83a203c16 100644 Binary files a/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz and b/creusot/tests/should_succeed/bug/two_phase/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/cell/01/why3session.xml b/creusot/tests/should_succeed/cell/01/why3session.xml index 2cef2f2d4..ae42d1aaa 100644 --- a/creusot/tests/should_succeed/cell/01/why3session.xml +++ b/creusot/tests/should_succeed/cell/01/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/cell/02/why3session.xml b/creusot/tests/should_succeed/cell/02/why3session.xml index f12072433..a7ff0749c 100644 --- a/creusot/tests/should_succeed/cell/02/why3session.xml +++ b/creusot/tests/should_succeed/cell/02/why3session.xml @@ -2,65 +2,64 @@ - - - + + - + - + - + - - + + - - + + - + - + - + - + - + - + - + - + - + - + @@ -69,7 +68,7 @@ - + @@ -80,10 +79,10 @@ - + - + @@ -92,28 +91,28 @@ - - + + - + - - + + - + - + - - + + - + diff --git a/creusot/tests/should_succeed/cell/02/why3shapes.gz b/creusot/tests/should_succeed/cell/02/why3shapes.gz index bb2b0a24c..74d9335ca 100644 Binary files a/creusot/tests/should_succeed/cell/02/why3shapes.gz and b/creusot/tests/should_succeed/cell/02/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/checked_ops/why3session.xml b/creusot/tests/should_succeed/checked_ops/why3session.xml index 08b8b7fdc..ac3172c6f 100644 --- a/creusot/tests/should_succeed/checked_ops/why3session.xml +++ b/creusot/tests/should_succeed/checked_ops/why3session.xml @@ -2,7 +2,7 @@ - + @@ -64,12 +64,12 @@ - + - + @@ -144,12 +144,12 @@ - + - + diff --git a/creusot/tests/should_succeed/clones/02/why3session.xml b/creusot/tests/should_succeed/clones/02/why3session.xml index f9de16def..4234c5f14 100644 --- a/creusot/tests/should_succeed/clones/02/why3session.xml +++ b/creusot/tests/should_succeed/clones/02/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/clones/03/why3session.xml b/creusot/tests/should_succeed/clones/03/why3session.xml index f49407661..694690e97 100644 --- a/creusot/tests/should_succeed/clones/03/why3session.xml +++ b/creusot/tests/should_succeed/clones/03/why3session.xml @@ -2,13 +2,13 @@ - + - + diff --git a/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml b/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml index 2596febb8..980623ad9 100644 --- a/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml +++ b/creusot/tests/should_succeed/closures/06_fn_specs/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -18,7 +18,7 @@ - + @@ -33,7 +33,7 @@ - + diff --git a/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml b/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml index 279be367c..50360b73d 100644 --- a/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml +++ b/creusot/tests/should_succeed/closures/07_mutable_capture/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/constrained_types/why3session.xml b/creusot/tests/should_succeed/constrained_types/why3session.xml index 9472fd004..039941142 100644 --- a/creusot/tests/should_succeed/constrained_types/why3session.xml +++ b/creusot/tests/should_succeed/constrained_types/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/drop_pair/why3session.xml b/creusot/tests/should_succeed/drop_pair/why3session.xml index d12ee4a34..b1e6a301c 100644 --- a/creusot/tests/should_succeed/drop_pair/why3session.xml +++ b/creusot/tests/should_succeed/drop_pair/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/filter_positive/why3session.xml b/creusot/tests/should_succeed/filter_positive/why3session.xml index 8b6befada..436d60ab3 100644 --- a/creusot/tests/should_succeed/filter_positive/why3session.xml +++ b/creusot/tests/should_succeed/filter_positive/why3session.xml @@ -2,29 +2,28 @@ - - - + + - + - + - + - + diff --git a/creusot/tests/should_succeed/filter_positive/why3shapes.gz b/creusot/tests/should_succeed/filter_positive/why3shapes.gz index 71e53ebdb..8154971b2 100644 Binary files a/creusot/tests/should_succeed/filter_positive/why3shapes.gz and b/creusot/tests/should_succeed/filter_positive/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/hashmap/why3session.xml b/creusot/tests/should_succeed/hashmap/why3session.xml index b4e5cd3df..67686ec0b 100644 --- a/creusot/tests/should_succeed/hashmap/why3session.xml +++ b/creusot/tests/should_succeed/hashmap/why3session.xml @@ -2,73 +2,71 @@ - + - - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -80,61 +78,61 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -151,24 +149,24 @@ - + - + - + - + @@ -183,13 +181,13 @@ - + - + - + @@ -203,21 +201,21 @@ - + - + - + @@ -234,7 +232,7 @@ - + @@ -249,7 +247,7 @@ - + @@ -260,85 +258,85 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -347,183 +345,183 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/hashmap/why3shapes.gz b/creusot/tests/should_succeed/hashmap/why3shapes.gz index 21841afd8..06a7a43d5 100644 Binary files a/creusot/tests/should_succeed/hashmap/why3shapes.gz and b/creusot/tests/should_succeed/hashmap/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/heapsort_generic/why3session.xml b/creusot/tests/should_succeed/heapsort_generic/why3session.xml index 6a7e391b4..4c89e63b4 100644 --- a/creusot/tests/should_succeed/heapsort_generic/why3session.xml +++ b/creusot/tests/should_succeed/heapsort_generic/why3session.xml @@ -2,204 +2,203 @@ - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -208,7 +207,7 @@ - + @@ -219,20 +218,20 @@ - + - + - + - + @@ -241,13 +240,13 @@ - + - + - + @@ -256,115 +255,115 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -377,7 +376,7 @@ - + @@ -390,16 +389,16 @@ - + - + - + - + diff --git a/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz b/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz index e697d1f0a..254a8e071 100644 Binary files a/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz and b/creusot/tests/should_succeed/heapsort_generic/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/hillel/why3session.xml b/creusot/tests/should_succeed/hillel/why3session.xml index 738919c0a..e09019425 100644 --- a/creusot/tests/should_succeed/hillel/why3session.xml +++ b/creusot/tests/should_succeed/hillel/why3session.xml @@ -3,11 +3,8 @@ "http://why3.lri.fr/why3session.dtd"> - - - - - + + @@ -17,125 +14,125 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -144,7 +141,7 @@ - + @@ -156,12 +153,12 @@ - + - + @@ -171,113 +168,113 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/hillel/why3shapes.gz b/creusot/tests/should_succeed/hillel/why3shapes.gz index c0716c812..abf3c6521 100644 Binary files a/creusot/tests/should_succeed/hillel/why3shapes.gz and b/creusot/tests/should_succeed/hillel/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/index_range/why3session.xml b/creusot/tests/should_succeed/index_range/why3session.xml index ab65e191b..5fee4bbaa 100644 --- a/creusot/tests/should_succeed/index_range/why3session.xml +++ b/creusot/tests/should_succeed/index_range/why3session.xml @@ -2,198 +2,198 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/index_range/why3shapes.gz b/creusot/tests/should_succeed/index_range/why3shapes.gz index 4bac77746..832f93d12 100644 Binary files a/creusot/tests/should_succeed/index_range/why3shapes.gz and b/creusot/tests/should_succeed/index_range/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml b/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml index 9b15505cd..71aca0aaf 100644 --- a/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml +++ b/creusot/tests/should_succeed/inplace_list_reversal/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/ite_normalize/why3session.xml b/creusot/tests/should_succeed/ite_normalize/why3session.xml index d9463c87a..9f8f80153 100644 --- a/creusot/tests/should_succeed/ite_normalize/why3session.xml +++ b/creusot/tests/should_succeed/ite_normalize/why3session.xml @@ -2,7 +2,7 @@ - + @@ -19,7 +19,7 @@ - + @@ -44,7 +44,7 @@ - + diff --git a/creusot/tests/should_succeed/iterators/01_range/why3session.xml b/creusot/tests/should_succeed/iterators/01_range/why3session.xml index 2e3e237a6..cd5427ea3 100644 --- a/creusot/tests/should_succeed/iterators/01_range/why3session.xml +++ b/creusot/tests/should_succeed/iterators/01_range/why3session.xml @@ -2,43 +2,43 @@ - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz b/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz index 9e56edc7f..f906967c8 100644 Binary files a/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz and b/creusot/tests/should_succeed/iterators/01_range/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml index 8da874725..ab02f40f5 100644 --- a/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml +++ b/creusot/tests/should_succeed/iterators/02_iter_mut/why3session.xml @@ -2,100 +2,100 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/02_iter_mut/why3shapes.gz b/creusot/tests/should_succeed/iterators/02_iter_mut/why3shapes.gz index 58d6bdfa4..0d75a0266 100644 Binary files a/creusot/tests/should_succeed/iterators/02_iter_mut/why3shapes.gz and b/creusot/tests/should_succeed/iterators/02_iter_mut/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml b/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml index e9654e3b1..9abeace1f 100644 --- a/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml +++ b/creusot/tests/should_succeed/iterators/03_std_iterators/why3session.xml @@ -2,186 +2,186 @@ - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - - - - + + + + + - + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + - - + + diff --git a/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz b/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz index 8aabb4955..b3b40f4a7 100644 Binary files a/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz and b/creusot/tests/should_succeed/iterators/03_std_iterators/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml index 3c04a0e1b..f26037cfc 100644 --- a/creusot/tests/should_succeed/iterators/04_skip/why3session.xml +++ b/creusot/tests/should_succeed/iterators/04_skip/why3session.xml @@ -3,37 +3,37 @@ "http://why3.lri.fr/why3session.dtd"> - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz b/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz index 20b994c37..b12488535 100644 Binary files a/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz and b/creusot/tests/should_succeed/iterators/04_skip/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/05_map/why3session.xml b/creusot/tests/should_succeed/iterators/05_map/why3session.xml index 455d817c0..ccf52ff00 100644 --- a/creusot/tests/should_succeed/iterators/05_map/why3session.xml +++ b/creusot/tests/should_succeed/iterators/05_map/why3session.xml @@ -2,10 +2,10 @@ - - + + @@ -19,7 +19,7 @@ - + @@ -38,51 +38,51 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -111,25 +111,25 @@ - + - + - + - + - + @@ -144,7 +144,7 @@ - + @@ -159,13 +159,13 @@ - + - + - + @@ -176,58 +176,58 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz b/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz index 388bb90dc..11885880a 100644 Binary files a/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz and b/creusot/tests/should_succeed/iterators/05_map/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml index ff670a8ab..7edf883d5 100644 --- a/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml +++ b/creusot/tests/should_succeed/iterators/06_map_precond/why3session.xml @@ -2,9 +2,7 @@ - - - + @@ -12,7 +10,7 @@ - + @@ -25,7 +23,7 @@ - + @@ -40,25 +38,25 @@ - + - + - + - + - + @@ -67,25 +65,25 @@ - + - + - + - + - + - + - + @@ -94,7 +92,7 @@ - + @@ -109,7 +107,7 @@ - + @@ -140,25 +138,25 @@ - + - + - + - + - + @@ -167,37 +165,37 @@ - + - + - + - + - + - + - + - + - + @@ -216,7 +214,7 @@ - + @@ -231,13 +229,13 @@ - + - + - + @@ -248,43 +246,43 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -294,70 +292,70 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz index 48584ee07..f14f993e7 100644 Binary files a/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz and b/creusot/tests/should_succeed/iterators/06_map_precond/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml b/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml index 3441e96b9..1747bd15e 100644 --- a/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml +++ b/creusot/tests/should_succeed/iterators/07_fuse/why3session.xml @@ -2,18 +2,18 @@ + - - + - + @@ -26,7 +26,7 @@ - + @@ -39,23 +39,23 @@ - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/07_fuse/why3shapes.gz b/creusot/tests/should_succeed/iterators/07_fuse/why3shapes.gz index 96d2692c5..7b1105150 100644 Binary files a/creusot/tests/should_succeed/iterators/07_fuse/why3shapes.gz and b/creusot/tests/should_succeed/iterators/07_fuse/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml b/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml index fef94b7c8..2dc2ffb91 100644 --- a/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml +++ b/creusot/tests/should_succeed/iterators/08_collect_extend/why3session.xml @@ -2,83 +2,83 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -87,79 +87,79 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz b/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz index b5dd105c7..a9db487dd 100644 Binary files a/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz and b/creusot/tests/should_succeed/iterators/08_collect_extend/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/09_empty/why3session.xml b/creusot/tests/should_succeed/iterators/09_empty/why3session.xml index ce9f8a66d..17e60e574 100644 --- a/creusot/tests/should_succeed/iterators/09_empty/why3session.xml +++ b/creusot/tests/should_succeed/iterators/09_empty/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/09_empty/why3shapes.gz b/creusot/tests/should_succeed/iterators/09_empty/why3shapes.gz index 9812fa9ae..18ae5acbd 100644 Binary files a/creusot/tests/should_succeed/iterators/09_empty/why3shapes.gz and b/creusot/tests/should_succeed/iterators/09_empty/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/10_once/why3session.xml b/creusot/tests/should_succeed/iterators/10_once/why3session.xml index 6fc2952e6..f80e28433 100644 --- a/creusot/tests/should_succeed/iterators/10_once/why3session.xml +++ b/creusot/tests/should_succeed/iterators/10_once/why3session.xml @@ -2,12 +2,12 @@ - + - + @@ -20,7 +20,7 @@ - + @@ -33,18 +33,18 @@ - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/10_once/why3shapes.gz b/creusot/tests/should_succeed/iterators/10_once/why3shapes.gz index a9dc0f9ff..996d94df3 100644 Binary files a/creusot/tests/should_succeed/iterators/10_once/why3shapes.gz and b/creusot/tests/should_succeed/iterators/10_once/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml b/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml index b959ae478..4559255de 100644 --- a/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml +++ b/creusot/tests/should_succeed/iterators/11_repeat/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/11_repeat/why3shapes.gz b/creusot/tests/should_succeed/iterators/11_repeat/why3shapes.gz index e787d5c31..b651106bf 100644 Binary files a/creusot/tests/should_succeed/iterators/11_repeat/why3shapes.gz and b/creusot/tests/should_succeed/iterators/11_repeat/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/12_zip/why3session.xml b/creusot/tests/should_succeed/iterators/12_zip/why3session.xml index 625fd2bdd..24abbb018 100644 --- a/creusot/tests/should_succeed/iterators/12_zip/why3session.xml +++ b/creusot/tests/should_succeed/iterators/12_zip/why3session.xml @@ -2,13 +2,13 @@ - - + + - + @@ -31,25 +31,25 @@ - + - + - + - + - + - + - + @@ -72,18 +72,18 @@ - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz b/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz index ddf925bd5..289137742 100644 Binary files a/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz and b/creusot/tests/should_succeed/iterators/12_zip/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml b/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml index bec43bdf8..273f287cb 100644 --- a/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml +++ b/creusot/tests/should_succeed/iterators/13_cloned/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/13_cloned/why3shapes.gz b/creusot/tests/should_succeed/iterators/13_cloned/why3shapes.gz index 67a078ee9..f6d3269db 100644 Binary files a/creusot/tests/should_succeed/iterators/13_cloned/why3shapes.gz and b/creusot/tests/should_succeed/iterators/13_cloned/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/14_copied/why3session.xml b/creusot/tests/should_succeed/iterators/14_copied/why3session.xml index 7f3b4dac9..ec701e690 100644 --- a/creusot/tests/should_succeed/iterators/14_copied/why3session.xml +++ b/creusot/tests/should_succeed/iterators/14_copied/why3session.xml @@ -2,33 +2,33 @@ - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz b/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz index f54c3e28b..5e972159e 100644 Binary files a/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz and b/creusot/tests/should_succeed/iterators/14_copied/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml b/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml index 23178b610..b1dc56c17 100644 --- a/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml +++ b/creusot/tests/should_succeed/iterators/15_enumerate/why3session.xml @@ -2,67 +2,67 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz b/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz index a7cee1ca1..f356beaf7 100644 Binary files a/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz and b/creusot/tests/should_succeed/iterators/15_enumerate/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/iterators/16_take/why3session.xml b/creusot/tests/should_succeed/iterators/16_take/why3session.xml index ca91def84..df447a949 100644 --- a/creusot/tests/should_succeed/iterators/16_take/why3session.xml +++ b/creusot/tests/should_succeed/iterators/16_take/why3session.xml @@ -2,34 +2,33 @@ - - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz b/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz index d1e1dccf8..d6461803a 100644 Binary files a/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz and b/creusot/tests/should_succeed/iterators/16_take/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/knapsack/why3session.xml b/creusot/tests/should_succeed/knapsack/why3session.xml index 27f9bc085..de3fbe681 100644 --- a/creusot/tests/should_succeed/knapsack/why3session.xml +++ b/creusot/tests/should_succeed/knapsack/why3session.xml @@ -2,293 +2,292 @@ - - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/knapsack/why3shapes.gz b/creusot/tests/should_succeed/knapsack/why3shapes.gz index f23922353..50912efcb 100644 Binary files a/creusot/tests/should_succeed/knapsack/why3shapes.gz and b/creusot/tests/should_succeed/knapsack/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/knapsack_full/why3session.xml b/creusot/tests/should_succeed/knapsack_full/why3session.xml index 83eeaddb4..f8985689c 100644 --- a/creusot/tests/should_succeed/knapsack_full/why3session.xml +++ b/creusot/tests/should_succeed/knapsack_full/why3session.xml @@ -3,383 +3,382 @@ "http://why3.lri.fr/why3session.dtd"> - - - - + + + - + - + - + - + - + - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -390,7 +389,7 @@ - + diff --git a/creusot/tests/should_succeed/knapsack_full/why3shapes.gz b/creusot/tests/should_succeed/knapsack_full/why3shapes.gz index a8c285a20..d2c69afb5 100644 Binary files a/creusot/tests/should_succeed/knapsack_full/why3shapes.gz and b/creusot/tests/should_succeed/knapsack_full/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/lang/modules/why3session.xml b/creusot/tests/should_succeed/lang/modules/why3session.xml index f929acf6f..d4edf9a30 100644 --- a/creusot/tests/should_succeed/lang/modules/why3session.xml +++ b/creusot/tests/should_succeed/lang/modules/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/lang/unary_op/why3session.xml b/creusot/tests/should_succeed/lang/unary_op/why3session.xml index 996f05129..0c082c6da 100644 --- a/creusot/tests/should_succeed/lang/unary_op/why3session.xml +++ b/creusot/tests/should_succeed/lang/unary_op/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/lang/while_let/why3session.xml b/creusot/tests/should_succeed/lang/while_let/why3session.xml index e3c1ac806..a13acc940 100644 --- a/creusot/tests/should_succeed/lang/while_let/why3session.xml +++ b/creusot/tests/should_succeed/lang/while_let/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/list_index_mut/why3session.xml b/creusot/tests/should_succeed/list_index_mut/why3session.xml index 255a3f908..86798025c 100644 --- a/creusot/tests/should_succeed/list_index_mut/why3session.xml +++ b/creusot/tests/should_succeed/list_index_mut/why3session.xml @@ -2,22 +2,22 @@ - + - + - + - + diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml index 5593d71e0..d67072bb8 100644 --- a/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml +++ b/creusot/tests/should_succeed/list_reversal_lasso/why3session.xml @@ -3,62 +3,62 @@ "http://why3.lri.fr/why3session.dtd"> - - - + + + - - - + + + - - - + + + - - - + + + - - - - - + + + + + - - + + - - + + - + - - + + - + - + - + - + - - + + - + @@ -87,23 +87,23 @@ - - - - - + + + + + - - + + - - + + - - + + - + @@ -165,31 +165,31 @@ - + - - + + - + - + - + - + - - + + - + - + @@ -218,38 +218,38 @@ - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + - + - - - - + + + + - + @@ -284,7 +284,7 @@ - + @@ -293,25 +293,25 @@ - + - + - + - + - + - - + + - - + + @@ -340,8 +340,8 @@ - - + + @@ -533,42 +533,42 @@ - - - + + + - + - + - + - + - + - + - + - + - + @@ -595,14 +595,14 @@ - + - + diff --git a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz index d00043363..f86ee3d4c 100644 Binary files a/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz and b/creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/mapping_test/why3session.xml b/creusot/tests/should_succeed/mapping_test/why3session.xml index c11e6a928..5b6168876 100644 --- a/creusot/tests/should_succeed/mapping_test/why3session.xml +++ b/creusot/tests/should_succeed/mapping_test/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/match_int/why3session.xml b/creusot/tests/should_succeed/match_int/why3session.xml index 400838f97..87c3b9806 100644 --- a/creusot/tests/should_succeed/match_int/why3session.xml +++ b/creusot/tests/should_succeed/match_int/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/mc91/why3session.xml b/creusot/tests/should_succeed/mc91/why3session.xml index 733e63d20..a1957f31e 100644 --- a/creusot/tests/should_succeed/mc91/why3session.xml +++ b/creusot/tests/should_succeed/mc91/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/mutex/why3session.xml b/creusot/tests/should_succeed/mutex/why3session.xml index 243ab338b..6dac3181c 100644 --- a/creusot/tests/should_succeed/mutex/why3session.xml +++ b/creusot/tests/should_succeed/mutex/why3session.xml @@ -4,12 +4,12 @@ - + - + diff --git a/creusot/tests/should_succeed/option/why3session.xml b/creusot/tests/should_succeed/option/why3session.xml index 51bab34c4..0e34268e6 100644 --- a/creusot/tests/should_succeed/option/why3session.xml +++ b/creusot/tests/should_succeed/option/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/ord_trait/why3session.xml b/creusot/tests/should_succeed/ord_trait/why3session.xml index 963905d91..2b9e14eeb 100644 --- a/creusot/tests/should_succeed/ord_trait/why3session.xml +++ b/creusot/tests/should_succeed/ord_trait/why3session.xml @@ -2,13 +2,13 @@ - + - + diff --git a/creusot/tests/should_succeed/projection_toggle/why3session.xml b/creusot/tests/should_succeed/projection_toggle/why3session.xml index df1fbf31a..2504fe914 100644 --- a/creusot/tests/should_succeed/projection_toggle/why3session.xml +++ b/creusot/tests/should_succeed/projection_toggle/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/resolve_uninit/why3session.xml b/creusot/tests/should_succeed/resolve_uninit/why3session.xml index 3a292395a..80d3400f8 100644 --- a/creusot/tests/should_succeed/resolve_uninit/why3session.xml +++ b/creusot/tests/should_succeed/resolve_uninit/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml index bb35d3531..c441b1b2b 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_max/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max_3/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_max_3/why3session.xml index bbf5feac9..7fd8fe4c4 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max_3/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_max_3/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml index 398e74165..aca5fccba 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_max_many/why3session.xml @@ -2,7 +2,7 @@ - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml index 4f024b61d..a4ec1bf37 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3session.xml @@ -2,18 +2,18 @@ - - + + - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3shapes.gz b/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3shapes.gz index 56bbacf6c..d8ac22421 100644 Binary files a/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3shapes.gz and b/creusot/tests/should_succeed/rusthorn/inc_max_repeat/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml index c8bb688dc..3735010cb 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_list/why3session.xml @@ -2,8 +2,8 @@ + - @@ -13,7 +13,7 @@ - + @@ -23,7 +23,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml index 2ac088923..cfe68cf19 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_2_tree/why3session.xml @@ -2,7 +2,7 @@ - + @@ -13,17 +13,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml index 57dd42f5d..96dfd3274 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_list/why3session.xml @@ -2,8 +2,8 @@ - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml index cd17b7232..acd099faa 100644 --- a/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml +++ b/creusot/tests/should_succeed/rusthorn/inc_some_tree/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -13,12 +13,12 @@ - + - + diff --git a/creusot/tests/should_succeed/selection_sort_generic/why3session.xml b/creusot/tests/should_succeed/selection_sort_generic/why3session.xml index 3c4f0f778..d4d47b5b2 100644 --- a/creusot/tests/should_succeed/selection_sort_generic/why3session.xml +++ b/creusot/tests/should_succeed/selection_sort_generic/why3session.xml @@ -2,107 +2,106 @@ - - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -111,27 +110,27 @@ - + - + - + - + - + @@ -142,49 +141,49 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz b/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz index bc9853f37..98e3e8a1b 100644 Binary files a/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz and b/creusot/tests/should_succeed/selection_sort_generic/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/slices/01/why3session.xml b/creusot/tests/should_succeed/slices/01/why3session.xml index f92d50c77..70ba52aa1 100644 --- a/creusot/tests/should_succeed/slices/01/why3session.xml +++ b/creusot/tests/should_succeed/slices/01/why3session.xml @@ -2,23 +2,23 @@ - - + + - + - + - + diff --git a/creusot/tests/should_succeed/slices/01/why3shapes.gz b/creusot/tests/should_succeed/slices/01/why3shapes.gz index 6e4381aa0..3d7ed1a93 100644 Binary files a/creusot/tests/should_succeed/slices/01/why3shapes.gz and b/creusot/tests/should_succeed/slices/01/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/slices/02_std/why3session.xml b/creusot/tests/should_succeed/slices/02_std/why3session.xml index e597d67f8..93d83d0dc 100644 --- a/creusot/tests/should_succeed/slices/02_std/why3session.xml +++ b/creusot/tests/should_succeed/slices/02_std/why3session.xml @@ -2,36 +2,36 @@ - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/slices/02_std/why3shapes.gz b/creusot/tests/should_succeed/slices/02_std/why3shapes.gz index 3da06821c..6aae85d5b 100644 Binary files a/creusot/tests/should_succeed/slices/02_std/why3shapes.gz and b/creusot/tests/should_succeed/slices/02_std/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/sparse_array/why3session.xml b/creusot/tests/should_succeed/sparse_array/why3session.xml index 22d3b951f..eb761eb3d 100644 --- a/creusot/tests/should_succeed/sparse_array/why3session.xml +++ b/creusot/tests/should_succeed/sparse_array/why3session.xml @@ -2,40 +2,40 @@ - + - - + + - + - - - - - - - - - - - + + + + + + + + + + + - + - + @@ -52,95 +52,95 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/sparse_array/why3shapes.gz b/creusot/tests/should_succeed/sparse_array/why3shapes.gz index ab0eac4e7..0b93af0a3 100644 Binary files a/creusot/tests/should_succeed/sparse_array/why3shapes.gz and b/creusot/tests/should_succeed/sparse_array/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/specification/division/why3session.xml b/creusot/tests/should_succeed/specification/division/why3session.xml index f43b14509..f03c368a6 100644 --- a/creusot/tests/should_succeed/specification/division/why3session.xml +++ b/creusot/tests/should_succeed/specification/division/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/specification/forall/why3session.xml b/creusot/tests/should_succeed/specification/forall/why3session.xml index f8454789d..9334ba099 100644 --- a/creusot/tests/should_succeed/specification/forall/why3session.xml +++ b/creusot/tests/should_succeed/specification/forall/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/specification/logic_call/why3session.xml b/creusot/tests/should_succeed/specification/logic_call/why3session.xml index 74a416b52..5c642dfa8 100644 --- a/creusot/tests/should_succeed/specification/logic_call/why3session.xml +++ b/creusot/tests/should_succeed/specification/logic_call/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/specification/logic_functions/why3session.xml b/creusot/tests/should_succeed/specification/logic_functions/why3session.xml index 31fd57ec1..f169c0e85 100644 --- a/creusot/tests/should_succeed/specification/logic_functions/why3session.xml +++ b/creusot/tests/should_succeed/specification/logic_functions/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/specification/trusted/why3session.xml b/creusot/tests/should_succeed/specification/trusted/why3session.xml index e7ba70514..66d895702 100644 --- a/creusot/tests/should_succeed/specification/trusted/why3session.xml +++ b/creusot/tests/should_succeed/specification/trusted/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/sum/why3session.xml b/creusot/tests/should_succeed/sum/why3session.xml index bfa8cce7c..1be18dcbc 100644 --- a/creusot/tests/should_succeed/sum/why3session.xml +++ b/creusot/tests/should_succeed/sum/why3session.xml @@ -4,38 +4,39 @@ - + + - + - + - + - + - + - + - + - + - + @@ -49,7 +50,7 @@ - + @@ -60,18 +61,18 @@ - + - + - + - + diff --git a/creusot/tests/should_succeed/sum/why3shapes.gz b/creusot/tests/should_succeed/sum/why3shapes.gz index 345b44b36..f466c413c 100644 Binary files a/creusot/tests/should_succeed/sum/why3shapes.gz and b/creusot/tests/should_succeed/sum/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/sum_of_odds/why3session.xml b/creusot/tests/should_succeed/sum_of_odds/why3session.xml index 851f75bef..ae9d697fb 100644 --- a/creusot/tests/should_succeed/sum_of_odds/why3session.xml +++ b/creusot/tests/should_succeed/sum_of_odds/why3session.xml @@ -2,8 +2,9 @@ - + + @@ -13,53 +14,53 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/sum_of_odds/why3shapes.gz b/creusot/tests/should_succeed/sum_of_odds/why3shapes.gz index 14e25fd2d..cbe4d366d 100644 Binary files a/creusot/tests/should_succeed/sum_of_odds/why3shapes.gz and b/creusot/tests/should_succeed/sum_of_odds/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/swap_borrows/why3session.xml b/creusot/tests/should_succeed/swap_borrows/why3session.xml index cfdf672bf..1c6808ca9 100644 --- a/creusot/tests/should_succeed/swap_borrows/why3session.xml +++ b/creusot/tests/should_succeed/swap_borrows/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/syntax/02_operators/why3session.xml b/creusot/tests/should_succeed/syntax/02_operators/why3session.xml index d4359928e..ef97012d8 100644 --- a/creusot/tests/should_succeed/syntax/02_operators/why3session.xml +++ b/creusot/tests/should_succeed/syntax/02_operators/why3session.xml @@ -3,8 +3,8 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -29,7 +29,7 @@ - + @@ -44,7 +44,7 @@ - + diff --git a/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml b/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml index 6508257e7..c2fa7ab82 100644 --- a/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml +++ b/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3session.xml @@ -2,18 +2,19 @@ - + + - + - + diff --git a/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3shapes.gz b/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3shapes.gz index fcd3aae4f..c74f2acb9 100644 Binary files a/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3shapes.gz and b/creusot/tests/should_succeed/syntax/06_logic_function_contracts/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml b/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml index 2ac0f7371..7c9316231 100644 --- a/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml +++ b/creusot/tests/should_succeed/syntax/09_maintains/why3session.xml @@ -2,9 +2,9 @@ - + @@ -19,7 +19,7 @@ - + diff --git a/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml b/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml index 36cbb722a..f98e5c9b6 100644 --- a/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml +++ b/creusot/tests/should_succeed/syntax/11_array_types/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/syntax/11_array_types/why3shapes.gz b/creusot/tests/should_succeed/syntax/11_array_types/why3shapes.gz index f5066d0ec..c3ff302a4 100644 Binary files a/creusot/tests/should_succeed/syntax/11_array_types/why3shapes.gz and b/creusot/tests/should_succeed/syntax/11_array_types/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml b/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml index d39f4ff35..b1871b20b 100644 --- a/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml +++ b/creusot/tests/should_succeed/syntax/12_ghost_code/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz b/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz index 69b0082f9..679b70d37 100644 Binary files a/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz and b/creusot/tests/should_succeed/syntax/12_ghost_code/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml b/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml index 058e693b7..3116ab6db 100644 --- a/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml +++ b/creusot/tests/should_succeed/syntax/13_vec_macro/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz b/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz index 5e7503b75..6b7d909af 100644 Binary files a/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz and b/creusot/tests/should_succeed/syntax/13_vec_macro/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml b/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml index 9770112e8..ffb4def5a 100644 --- a/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml +++ b/creusot/tests/should_succeed/syntax/derive_macros/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -18,7 +18,7 @@ - + @@ -33,7 +33,7 @@ - + diff --git a/creusot/tests/should_succeed/take_first_mut/why3session.xml b/creusot/tests/should_succeed/take_first_mut/why3session.xml index efe891a4d..b15625318 100644 --- a/creusot/tests/should_succeed/take_first_mut/why3session.xml +++ b/creusot/tests/should_succeed/take_first_mut/why3session.xml @@ -7,7 +7,7 @@ - + diff --git a/creusot/tests/should_succeed/take_first_mut/why3shapes.gz b/creusot/tests/should_succeed/take_first_mut/why3shapes.gz index e3a3c70d2..6a0a7abcf 100644 Binary files a/creusot/tests/should_succeed/take_first_mut/why3shapes.gz and b/creusot/tests/should_succeed/take_first_mut/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/traits/02/why3session.xml b/creusot/tests/should_succeed/traits/02/why3session.xml index e58a464ab..69068c8ae 100644 --- a/creusot/tests/should_succeed/traits/02/why3session.xml +++ b/creusot/tests/should_succeed/traits/02/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/traits/12_default_method/why3session.xml b/creusot/tests/should_succeed/traits/12_default_method/why3session.xml index 2ba371719..327f395a9 100644 --- a/creusot/tests/should_succeed/traits/12_default_method/why3session.xml +++ b/creusot/tests/should_succeed/traits/12_default_method/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml b/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml index cad38239b..0116e0197 100644 --- a/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml +++ b/creusot/tests/should_succeed/traits/13_assoc_types/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml b/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml index 226d56a98..724789b50 100644 --- a/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml +++ b/creusot/tests/should_succeed/traits/16_impl_cloning/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/traits/16_impl_cloning/why3shapes.gz b/creusot/tests/should_succeed/traits/16_impl_cloning/why3shapes.gz index 3492c69cb..549b88642 100644 Binary files a/creusot/tests/should_succeed/traits/16_impl_cloning/why3shapes.gz and b/creusot/tests/should_succeed/traits/16_impl_cloning/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml b/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml index b634bb7f6..aa25bfb00 100644 --- a/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml +++ b/creusot/tests/should_succeed/traits/18_trait_laws/why3session.xml @@ -2,8 +2,8 @@ - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/type_invariants/generated/why3session.xml b/creusot/tests/should_succeed/type_invariants/generated/why3session.xml index 4834550de..374444741 100644 --- a/creusot/tests/should_succeed/type_invariants/generated/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/generated/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml b/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml index a5abb58de..027b856ed 100644 --- a/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/non_zero/why3session.xml @@ -2,8 +2,8 @@ - + @@ -18,7 +18,7 @@ - + diff --git a/creusot/tests/should_succeed/type_invariants/quant/why3session.xml b/creusot/tests/should_succeed/type_invariants/quant/why3session.xml index 2a92ba966..5438d54dd 100644 --- a/creusot/tests/should_succeed/type_invariants/quant/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/quant/why3session.xml @@ -3,7 +3,7 @@ "http://why3.lri.fr/why3session.dtd"> - + @@ -13,7 +13,7 @@ - + diff --git a/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml b/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml index 613aedc3f..7a558ad90 100644 --- a/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/type_invariants/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml b/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml index dc17e0f11..92135c671 100644 --- a/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml +++ b/creusot/tests/should_succeed/type_invariants/vec_inv/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz b/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz index 51da37f82..db78d5985 100644 Binary files a/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz and b/creusot/tests/should_succeed/type_invariants/vec_inv/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/unnest/why3session.xml b/creusot/tests/should_succeed/unnest/why3session.xml index 136eb15df..103f7cd78 100644 --- a/creusot/tests/should_succeed/unnest/why3session.xml +++ b/creusot/tests/should_succeed/unnest/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/unused_in_loop/why3session.xml b/creusot/tests/should_succeed/unused_in_loop/why3session.xml index 3231342ce..8a832490b 100644 --- a/creusot/tests/should_succeed/unused_in_loop/why3session.xml +++ b/creusot/tests/should_succeed/unused_in_loop/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/vecdeque/why3session.xml b/creusot/tests/should_succeed/vecdeque/why3session.xml index 62b682d9f..b0bba52d8 100644 --- a/creusot/tests/should_succeed/vecdeque/why3session.xml +++ b/creusot/tests/should_succeed/vecdeque/why3session.xml @@ -2,111 +2,111 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/vecdeque/why3shapes.gz b/creusot/tests/should_succeed/vecdeque/why3shapes.gz index f0e291fc3..b3c323509 100644 Binary files a/creusot/tests/should_succeed/vecdeque/why3shapes.gz and b/creusot/tests/should_succeed/vecdeque/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/01/why3session.xml b/creusot/tests/should_succeed/vector/01/why3session.xml index 158c1776f..6848a3884 100644 --- a/creusot/tests/should_succeed/vector/01/why3session.xml +++ b/creusot/tests/should_succeed/vector/01/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/vector/01/why3shapes.gz b/creusot/tests/should_succeed/vector/01/why3shapes.gz index cf570080d..562528e1e 100644 Binary files a/creusot/tests/should_succeed/vector/01/why3shapes.gz and b/creusot/tests/should_succeed/vector/01/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/02_gnome/why3session.xml b/creusot/tests/should_succeed/vector/02_gnome/why3session.xml index 0f176444f..3c2be9c18 100644 --- a/creusot/tests/should_succeed/vector/02_gnome/why3session.xml +++ b/creusot/tests/should_succeed/vector/02_gnome/why3session.xml @@ -2,106 +2,106 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz b/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz index e1d2ead2c..95bf9d8a1 100644 Binary files a/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz and b/creusot/tests/should_succeed/vector/02_gnome/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3session.xml b/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3session.xml index 5d71019b5..8c8daba04 100644 --- a/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3session.xml +++ b/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz b/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz index 55927ee97..a56287781 100644 Binary files a/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz and b/creusot/tests/should_succeed/vector/03_knuth_shuffle/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/04_binary_search/why3session.xml b/creusot/tests/should_succeed/vector/04_binary_search/why3session.xml index 85a37fc43..2dfab7153 100644 --- a/creusot/tests/should_succeed/vector/04_binary_search/why3session.xml +++ b/creusot/tests/should_succeed/vector/04_binary_search/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz b/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz index 96bfe0f2e..5d7bf11dd 100644 Binary files a/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz and b/creusot/tests/should_succeed/vector/04_binary_search/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml index df588d00c..9f01f219a 100644 --- a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml +++ b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3session.xml @@ -2,118 +2,118 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz index e09a15023..ca4cd7cbd 100644 Binary files a/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz and b/creusot/tests/should_succeed/vector/05_binary_search_generic/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml b/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml index 4a1abc4bf..c3527f26a 100644 --- a/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml +++ b/creusot/tests/should_succeed/vector/06_knights_tour/why3session.xml @@ -2,87 +2,87 @@ + - - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -95,7 +95,7 @@ - + @@ -110,7 +110,7 @@ - + @@ -133,7 +133,7 @@ - + @@ -148,7 +148,7 @@ - + @@ -161,25 +161,25 @@ - + - + - + - + - + @@ -188,7 +188,7 @@ - + @@ -197,28 +197,28 @@ - + - + - + - + - + - + - + - + @@ -229,7 +229,7 @@ - + @@ -248,14 +248,14 @@ - + - + @@ -272,103 +272,103 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -383,7 +383,7 @@ - + @@ -398,7 +398,7 @@ - + @@ -421,7 +421,7 @@ - + @@ -436,7 +436,7 @@ - + @@ -449,43 +449,43 @@ - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz b/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz index 3a6bd76c9..574aed745 100644 Binary files a/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz and b/creusot/tests/should_succeed/vector/06_knights_tour/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/07_read_write/why3session.xml b/creusot/tests/should_succeed/vector/07_read_write/why3session.xml index 68f3e78f7..4d6b40519 100644 --- a/creusot/tests/should_succeed/vector/07_read_write/why3session.xml +++ b/creusot/tests/should_succeed/vector/07_read_write/why3session.xml @@ -2,12 +2,12 @@ - + - + diff --git a/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz b/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz index a9a5b1dee..7eaf167fb 100644 Binary files a/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz and b/creusot/tests/should_succeed/vector/07_read_write/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3session.xml b/creusot/tests/should_succeed/vector/08_haystack/why3session.xml index 90a474bd5..9ebd25945 100644 --- a/creusot/tests/should_succeed/vector/08_haystack/why3session.xml +++ b/creusot/tests/should_succeed/vector/08_haystack/why3session.xml @@ -2,118 +2,118 @@ - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz b/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz index 68991feb1..3611e1c8a 100644 Binary files a/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz and b/creusot/tests/should_succeed/vector/08_haystack/why3shapes.gz differ diff --git a/creusot/tests/should_succeed/vector/09_capacity/why3session.xml b/creusot/tests/should_succeed/vector/09_capacity/why3session.xml index b4d02c4c5..185c194ba 100644 --- a/creusot/tests/should_succeed/vector/09_capacity/why3session.xml +++ b/creusot/tests/should_succeed/vector/09_capacity/why3session.xml @@ -2,17 +2,17 @@ - + - + - + diff --git a/creusot/tests/should_succeed/vector/09_capacity/why3shapes.gz b/creusot/tests/should_succeed/vector/09_capacity/why3shapes.gz index cc7bc69a4..641262ce7 100644 Binary files a/creusot/tests/should_succeed/vector/09_capacity/why3shapes.gz and b/creusot/tests/should_succeed/vector/09_capacity/why3shapes.gz differ